feat(Topology): étalé space associated to a predicate on sections

Mathlib.lean

@@ -6909,6 +6909,7 @@ public import Mathlib.Topology.EMetricSpace.Lipschitz
 public import Mathlib.Topology.EMetricSpace.PairReduction
 public import Mathlib.Topology.EMetricSpace.Paracompact
 public import Mathlib.Topology.EMetricSpace.Pi
+public import Mathlib.Topology.EtaleSpace
 public import Mathlib.Topology.ExtendFrom
 public import Mathlib.Topology.Exterior
 public import Mathlib.Topology.ExtremallyDisconnected

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean

@@ -80,7 +80,7 @@ The predicate `IsFraction` is "prelocal", in the sense that if it holds on `U` i
 subset `V` of `U`.
 -/
 def isFractionPrelocal : PrelocalPredicate fun x : ProjectiveSpectrum.top 𝒜 => at x where
-  pred f := IsFraction f
+  pred U := IsFraction
   res := by rintro V U i f ⟨j, r, s, h, w⟩; exact ⟨j, r, s, (h <| i ·), (w <| i ·)⟩
 
 /-- We will define the structure sheaf as the subsheaf of all dependent functions in

Mathlib/Data/Set/Operations.lean

@@ -302,6 +302,26 @@ abbrev RightInvOn (g : β → α) (f : α → β) (t : Set β) : Prop := LeftInv
 def InvOn (g : β → α) (f : α → β) (s : Set α) (t : Set β) : Prop :=
   LeftInvOn g f s ∧ RightInvOn g f t
 
+section Section
+
+variable {α β : Type*} {p : β → Prop} {f : α → β} {s s' : Subtype p → α}
+
+theorem injOn_range_subtype_section (hs : f ∘ s = Subtype.val) : (Set.range s).InjOn f := by
+  rintro _ ⟨b, rfl⟩ _ ⟨b', rfl⟩ eq
+  cases (hs ▸ Subtype.val_injective) eq
+  rfl
+
+theorem subtype_section_ext (hs : f ∘ s = Subtype.val) (hs' : f ∘ s' = Subtype.val)
+    (eq : Set.range s = Set.range s') : s = s' := by
+  ext a
+  obtain ⟨b, eq⟩ := eq.symm ▸ Set.mem_range_self a
+  have := congr_arg f eq
+  rw [← f.comp_apply, ← f.comp_apply, hs, hs'] at this
+  cases Subtype.ext this
+  exact eq
+
+end Section
+
 section image2
 
 /-- The image of a binary function `f : α → β → γ` as a function `Set α → Set β → Set γ`.

Mathlib/Geometry/Manifold/Sheaf/Smooth.lean

@@ -106,12 +106,12 @@ lemma smoothSheaf.obj_eq (U : (Opens (TopCat.of M))ᵒᵖ) :
 /-- Canonical map from the stalk of `smoothSheaf IM I M N` at `x` to `N`, given by evaluating
 sections at `x`. -/
 def smoothSheaf.eval (x : M) : (smoothSheaf IM I M N).presheaf.stalk x → N :=
-  TopCat.stalkToFiber (StructureGroupoid.LocalInvariantProp.localPredicate M N _) x
+  TopCat.stalkToFiber (StructureGroupoid.LocalInvariantProp.localPredicate M N _).1 x
 
 /-- Canonical map from the stalk of `smoothSheaf IM I M N` at `x` to `N`, given by evaluating
 sections at `x`, considered as a morphism in the category of types. -/
 def smoothSheaf.evalHom (x : TopCat.of M) : (smoothSheaf IM I M N).presheaf.stalk x ⟶ N :=
-  TopCat.stalkToFiber (StructureGroupoid.LocalInvariantProp.localPredicate M N _) x
+  TopCat.stalkToFiber (StructureGroupoid.LocalInvariantProp.localPredicate M N _).1 x
 
 open CategoryTheory Limits
 
@@ -125,7 +125,7 @@ def smoothSheaf.evalAt (x : TopCat.of M) (U : OpenNhds x)
     colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheaf IM I M N).val) U ≫
     smoothSheaf.evalHom IM I N x =
     smoothSheaf.evalAt _ _ _ _ _ :=
-  colimit.ι_desc _ _
+  funext fun _ ↦ TopCat.stalkToFiber_germ ..
 
 /-- The `eval` map is surjective at `x`. -/
 lemma smoothSheaf.eval_surjective (x : M) : Function.Surjective (smoothSheaf.eval IM I N x) := by
@@ -141,7 +141,7 @@ variable {IM I N}
 @[simp] lemma smoothSheaf.eval_germ (U : Opens M) (x : M) (hx : x ∈ U)
     (f : (smoothSheaf IM I M N).presheaf.obj (op U)) :
     smoothSheaf.eval IM I N (x : M) ((smoothSheaf IM I M N).presheaf.germ U x hx f) = f ⟨x, hx⟩ :=
-  TopCat.stalkToFiber_germ ((contDiffWithinAt_localInvariantProp ∞).localPredicate M N) _ _ _ _
+  TopCat.stalkToFiber_germ ((contDiffWithinAt_localInvariantProp ∞).localPredicate M N).1 _ _ _ _
 
 lemma smoothSheaf.contMDiff_section {U : (Opens (TopCat.of M))ᵒᵖ}
     (f : (smoothSheaf IM I M N).presheaf.obj U) :

Mathlib/Logic/Equiv/Basic.lean

@@ -396,19 +396,51 @@ def sigmaOptionEquivOfSome {α} (p : Option α → Type v) (h : p none → False
     · intro n
       exfalso
       exact h n
-    · intro _
-      exact rfl
+    · intro
+      rfl
   (sigmaSubtypeEquivOfSubset _ _ h').symm.trans (sigmaCongrLeft' (optionIsSomeEquiv α))
 
+section Sigma
+
+variable {α ι : Type*} {π : ι → Type*} {p : ι → Prop}
+
+/-- Functions to a `Sigma` type are in bijection with a `Sigma` type of dependent functions. -/
+def arrowSigma : (α → Σ i, π i) ≃ Σ i : α → ι, ∀ x, π (i x) where
+  toFun f := ⟨Sigma.fst ∘ f, fun x ↦ (f x).2⟩
+  invFun f a := .mk _ (f.2 a)
+
+/-- The `Sigma` type indexed by a subtype can be canonically identified with a subtype of the
+`Sigma` type indexed by the whole type. -/
+def sigmaSubtypeComm : (Σ i : Subtype p, π i) ≃ { f : Σ i, π i // p f.1 } where
+  toFun f := ⟨⟨_, f.2⟩, f.1.2⟩
+  invFun f := ⟨⟨_, f.2⟩, f.1.2⟩
+
+variable (ι π) in
 /-- The `Pi`-type `∀ i, π i` is equivalent to the type of sections `f : ι → Σ i, π i` of the
 `Sigma` type such that for all `i` we have `(f i).fst = i`. -/
-def piEquivSubtypeSigma (ι) (π : ι → Type*) :
-    (∀ i, π i) ≃ { f : ι → Σ i, π i // ∀ i, (f i).1 = i } where
-  toFun := fun f => ⟨fun i => ⟨i, f i⟩, fun _ => rfl⟩
-  invFun := fun f i => by rw [← f.2 i]; exact (f.1 i).2
-  right_inv := fun ⟨f, hf⟩ =>
-    Subtype.ext <| funext fun i =>
-      Sigma.eq (hf i).symm <| eq_of_heq <| rec_heq_of_heq _ <| by simp
+def piEquivSubtypeSigma : (∀ i, π i) ≃ { f : ι → Σ i, π i // ∀ i, (f i).1 = i } where
+  toFun f := ⟨fun i ↦ .mk _ (f i), fun _ ↦ rfl⟩
+  invFun f i := cast (congr_arg π (f.2 i)) (f.1 i).2
+  right_inv f := Subtype.ext <| funext fun i ↦ Sigma.ext (f.2 i).symm <| by simp
+
+/-- The `Pi`-type `∀ i : Subtype p, π i` indexed by a subtype is equivalent to the type of
+sections of the `Sigma` type `Σ i, π i` over the subtype. -/
+def piSubtypeEquivSubtypeSigma :
+    (∀ i : Subtype p, π i) ≃ { f : Subtype p → Σ i, π i // Sigma.fst ∘ f = (↑) } :=
+  (piEquivSubtypeSigma ..).trans <| .trans
+    (subtypeEquivOfSubtype' (arrowCongr (.refl _) sigmaSubtypeComm))
+    { toFun f := ⟨val ∘ f.1, funext (congr_arg val <| f.2 ·)⟩
+      invFun f := ⟨fun i ↦ ⟨_, by apply congr_fun f.2 i ▸ i.2⟩, (Subtype.ext <| congr_fun f.2 ·)⟩ }
+
+lemma mk_piEquivSubtypeSigma_symm {f : {f : ι → Σ i, π i // ∀ i, (f i).1 = i}} {i : ι} :
+    Sigma.mk _ ((piEquivSubtypeSigma ι π).symm f i) = f.1 i :=
+  congr_fun (congr_arg val ((piEquivSubtypeSigma ..).right_inv f)) i
+
+lemma mk_piSubtypeEquivSubtypeSigma {f : {f : Subtype p → Σ i, π i // Sigma.fst ∘ f = val}}
+    {i : Subtype p} : Sigma.mk _ (piSubtypeEquivSubtypeSigma.symm f i) = f.1 i :=
+  congr_fun (congr_arg val (piSubtypeEquivSubtypeSigma.right_inv f)) i
+
+end Sigma
 
 /-- The type of functions `f : ∀ a, β a` such that for all `a` we have `p a (f a)` is equivalent
 to the type of functions `∀ a, {b : β a // p a b}`. -/