feat (IsCoherentWith) : families of maps from a coherent collection of subspaces lift uniquely to maps from the total space

Author: robertmaxton42

Mathlib/Data/Set/UnionLift.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
 import Mathlib.Data.Set.Lattice
+import Mathlib.Data.Set.Subset
 import Mathlib.Order.Directed
 
 /-!
@@ -39,6 +40,7 @@ directed union, directed supremum, glue, gluing
 variable {α : Type*} {ι β : Sort _}
 
 namespace Set
+open Set.Notation
 
 section UnionLift
 
@@ -82,6 +84,10 @@ theorem preimage_iUnionLift (t : Set β) :
     obtain rfl : y = x := congr_arg Subtype.val hxy
     rwa [iUnionLift_of_mem x hi]
 
+theorem iUnionLift_restrict {i : ι} :
+    restrict (T ↓∩ S i) (iUnionLift S f hf T hT) = f i ∘ preimageValInclusion T (S i) := by
+  ext ⟨⟨x, hxT⟩, hxS⟩; simp at hxS; simp [iUnionLift_of_mem ⟨x, hxT⟩ hxS]
+
 /-- `iUnionLift_const` is useful for proving that `iUnionLift` is a homomorphism
   of algebraic structures when defined on the Union of algebraic subobjects.
   For example, it could be used to prove that the lift of a collection
@@ -165,4 +171,8 @@ theorem preimage_liftCover (t : Set β) : liftCover S f hf hS ⁻¹' t = ⋃ i,
   rw [preimage_comp, preimage_iUnionLift]
   ext; simp
 
+@[simp]
+theorem liftCover_restrict {i : ι} : (S i).restrict (liftCover S f hf hS) = f i := by ext x; simp
+
+
 end Set

Mathlib/Topology/Coherent.lean

@@ -31,7 +31,7 @@ and provide the others as corollaries.
   then we have `IsCoherentWith S`;
 -/
 
-open Filter Set
+open Filter Set Set.Notation
 
 variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
   {S : Set (Set X)} {t : Set X} {x : X}
@@ -115,4 +115,118 @@ lemma isQuotientMap_sigma_desc (hX : IsCoherentWith S) (hS : ⋃₀ S = univ) :
   IsCoherentWith.isQuotientMap_sigma_desc' (S := ((↑) : S → Set X))
     (h ▸ hX) (sUnion_eq_iUnion ▸ hS)
 
+variable {S : Set (Set X)} (hS : IsCoherentWith S) (surj : ⋃₀ S = Set.univ) (F : ∀ s ∈ S, C(s, Y))
+  (hF : ∀ (s) (hs : s ∈ S) (t) (ht : t ∈ S) (x : X) (hxs : x ∈ s) (hxt : x ∈ t),
+    F s hs ⟨x, hxs⟩ = F t ht ⟨x, hxt⟩)
+
+/-- A family `F s` of continuous maps `C(s, Y)`, where (1) the domains `s` are taken from a set `S`
+of sets in `X` which are jointly surjective and coherent with `X` and (2) the functions `F s` agree
+pairwise on intersections, can be glued to construct a continuous map `C(X, Y)`. -/
+noncomputable def liftCover : C(X, Y) where
+  toFun := Set.liftCover ((↑) : S → Set X) (fun s ↦ F s s.2) (fun s t ↦ hF s s.2 t t.2)
+    (by simp [sUnion_eq_iUnion, ← surj])
+  continuous_toFun := by
+    rw [hS.continuous_iff, Subtype.forall']
+    intro s
+    rw [continuousOn_iff_continuous_restrict, Set.liftCover_restrict]
+    exact (F s s.2).continuous
+
+variable {hS surj F hF}
+
+@[simp]
+theorem liftCover_coe {s : S} (x : (s : Set X)) : hS.liftCover surj F hF x = F s s.2 x := by
+  simp [IsCoherentWith.liftCover]
+
+@[simp]
+theorem liftCover_of_mem_coe {s : Set X} (hs : s ∈ S) (x : s) :
+    hS.liftCover surj F hF x = F s hs x :=
+  hS.liftCover_coe (s := ⟨s, hs⟩) x
+
+theorem liftCover_of_mem {s : Set X} (hs : s ∈ S) {x : X} (hx : x ∈ s) :
+    hS.liftCover surj F hF x = F s hs ⟨x, hx⟩ :=
+  hS.liftCover_of_mem_coe hs ⟨x, hx⟩
+
+theorem preimage_liftCover (t : Set Y) :
+    hS.liftCover surj F hF ⁻¹' t = ⋃ s : S, (↑) '' (F s s.2 ⁻¹' t) := by
+  simp only [IsCoherentWith.liftCover, ContinuousMap.coe_mk]
+  rw [Set.preimage_liftCover]
+
+@[simp]
+theorem liftCover_restrict (s : Set X) (hs : s ∈ S) :
+    s.restrict (hS.liftCover surj F hF) = F s hs := by
+  ext x; simp [hs]
+
+variable (hS surj) in
+/-- When `X` is coherent with a set of subspaces `S`, every continuous map out of `X` can be
+written as a `liftCover`. -/
+@[simps]
+noncomputable def liftEquiv :
+    { F : ∀ s ∈ S, C(s, Y) // ∀ s (hs : s ∈ S) t (ht : t ∈ S) x (hxs : x ∈ s) (hxt : x ∈ t),
+       F s hs ⟨x, hxs⟩ = F t ht ⟨x, hxt⟩ } ≃ C(X, Y) where
+  toFun F := hS.liftCover surj F F.2
+  invFun f := ⟨fun s hs ↦ f.restrict s, fun s hs t ht x hxs hxt ↦ by simp⟩
+  left_inv := by rintro ⟨F, hF⟩; ext s hs x; simp [hs]
+  right_inv f := by
+    ext x
+    rw [sUnion_eq_univ_iff] at surj
+    obtain ⟨s, hs, hxs⟩ := surj x
+    simp [liftCover_of_mem hs hxs]
+
+/-- A version of `liftEquiv_apply` that is more convenient when rewriting. -/
+lemma liftEquiv_apply' : hS.liftCover surj F hF = hS.liftEquiv surj ⟨F, hF⟩ := by rfl
+
+variable {ι} {S : ι → Set X} (hS : IsCoherentWith (range S)) (surj : ⋃ i, S i = Set.univ)
+  (φ : (i : ι) → C(S i, Y))
+  (hφ : ∀ i j x (hxi : x ∈ S i) (hxj : x ∈ S j), φ i ⟨x, hxi⟩ = φ j ⟨x, hxj⟩)
+
+/-- A family `φ i` of continuous maps `(i : ι) → C(S i, Y)`, where (1) the domains `S i` are taken
+from a family `S` of sets in `X` which are jointly surjective and coherent with `X` and (2) the
+functions `φ` agree pairwise on intersections, can be glued to construct a continuous map
+`C(X, Y)`. -/
+noncomputable def liftCover' : C(X, Y) where
+  toFun := Set.liftCover S (φ ·) hφ surj
+  continuous_toFun := by
+    rw [hS.continuous_iff, forall_mem_range]
+    intro i
+    rw [continuousOn_iff_continuous_restrict, Set.liftCover_restrict]
+    exact (φ i).continuous
+
+variable {hS surj φ hφ}
+variable {i : ι}
+
+@[simp]
+theorem liftCover'_coe (x : S i) : hS.liftCover' surj φ hφ x = φ i x := by
+  simp [IsCoherentWith.liftCover']
+
+@[simp]
+theorem liftCover'_of_mem {x : X} (hx : x ∈ S i) : hS.liftCover' surj φ hφ x = φ i ⟨x, hx⟩ :=
+  hS.liftCover'_coe ⟨x, hx⟩
+
+theorem preimage_liftCover' (t : Set Y) :
+    hS.liftCover' surj φ hφ ⁻¹' t = ⋃ i, (↑) '' (φ i ⁻¹' t) := by
+  simp only [IsCoherentWith.liftCover', ContinuousMap.coe_mk]
+  rw [Set.preimage_liftCover]
+
+@[simp]
+theorem liftCover'_restrict : (S i).restrict (hS.liftCover' surj φ hφ) = φ i := by ext x; simp
+
+variable (hS surj) in
+/-- When `X` is coherent with a family of subspaces `S i`, every continuous map out of `X` can be
+written as a `liftCover'`. -/
+@[simps]
+noncomputable def liftEquiv' :
+    { φ : (i : ι) → C(S i, Y) // ∀ i j x (hxi : x ∈ S i) (hxj : x ∈ S j),
+       φ i ⟨x, hxi⟩ = φ j ⟨x, hxj⟩ } ≃ C(X, Y) where
+  toFun φ := hS.liftCover' surj φ φ.2
+  invFun f := ⟨fun i ↦ f.restrict (S i), fun i j x hxi hxj ↦ by simp⟩
+  left_inv := by rintro ⟨φ, hφ⟩; ext i x; simp
+  right_inv f := by
+    ext x
+    rw [iUnion_eq_univ_iff] at surj
+    obtain ⟨i, hxi⟩ := surj x
+    simp [liftCover'_of_mem hxi]
+
+/-- A version of `liftEquiv'_apply` that is more convenient when rewriting. -/
+lemma liftEquiv'_apply' : hS.liftCover' surj φ hφ = hS.liftEquiv' surj ⟨φ, hφ⟩ := by rfl
+
 end Topology.IsCoherentWith