simplify explicit coproducts

Author: dagurtomas

LeanCondensed/Mathlib/Topology/Category/CompHausLike/Limits.lean

@@ -1,7 +1,7 @@
 import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
 import Mathlib.Topology.Category.LightProfinite.Limits
 
-open CategoryTheory Topology
+open CategoryTheory Topology Limits
 
 namespace CompHausLike
 
@@ -11,107 +11,19 @@ section BinaryCoproducts
 
 variable {P : TopCat.{u} → Prop} (X Y : CompHausLike P)
 
-/--
-A typeclass describing the property that forming the disjoint union is stable under the
-property `P`.
--/
-abbrev HasExplicitBinaryCoproduct := HasProp P (X ⊕ Y)
+section Coproduct
 
-variable [HasExplicitBinaryCoproduct X Y]
+variable [HasProp P (X ⊕ Y)]
 
-/--
-The coproduct of two objects in `CompHausLike`, constructed as the disjoint
-union with its usual topology.
--/
-def coprod : CompHausLike P := CompHausLike.of P (X ⊕ Y)
+def coproductCocone : BinaryCofan X Y := BinaryCofan.mk (P := CompHausLike.of P (X ⊕ Y))
+  (TopCat.ofHom { toFun := Sum.inl }) (TopCat.ofHom { toFun := Sum.inr })
 
-/--
-The inclusion of the left factor into the explicit binary coproduct.
--/
-def coprod.inl : X ⟶ coprod X Y := ofHom _ { toFun := fun x ↦ Sum.inl x }
-
-/--
-The inclusion of the right factor into the explicit binary coproduct.
--/
-def coprod.inr : Y ⟶ coprod X Y := ofHom _ { toFun := fun x ↦ Sum.inr x }
-
-variable {X Y}
-
-/--
-To construct a morphism from the explicit finite coproduct, it suffices to
-specify a morphism from each of its factors.
-This is essentially the universal property of the coproduct.
--/
-def coprod.desc {B : CompHausLike P} (l : X ⟶ B) (r : Y ⟶ B) : coprod X Y ⟶ B :=
-  ofHom _ { toFun := Sum.elim l r }
-
-@[reassoc (attr := simp)]
-lemma coprod.inl_desc {B : CompHausLike P} (l : X ⟶ B) (r : Y ⟶ B) :
-    coprod.inl X Y ≫ coprod.desc l r = l := rfl
-
-@[reassoc (attr := simp)]
-lemma coprod.inr_desc {B : CompHausLike P} (l : X ⟶ B) (r : Y ⟶ B) :
-    coprod.inr X Y ≫ coprod.desc l r = r := rfl
-
-@[ext]
-lemma coprod.hom_ext {B : CompHausLike P} (f g : coprod X Y ⟶ B)
-    (hl : coprod.inl X Y ≫ f = coprod.inl X Y ≫ g) (hr : coprod.inr X Y ≫ f = coprod.inr X Y ≫ g) :
-    f = g := by
+def coproductIsColimit : IsColimit (coproductCocone X Y) := by
+  refine BinaryCofan.isColimitMk (fun s ↦ ofHom _ { toFun := Sum.elim s.inl s.inr })
+    (by cat_disch) (by cat_disch) fun _ _ h₁ h₂ ↦ ?_
   ext ⟨⟩
-  exacts [ConcreteCategory.congr_hom hl _, ConcreteCategory.congr_hom hr _]
-
-variable (X Y)
-
-/-- The coproduct cocone associated to the explicit finite coproduct. -/
-abbrev coprod.binaryCofan : Limits.BinaryCofan X Y :=
-  Limits.BinaryCofan.mk (coprod.inl X Y) (coprod.inr X Y)
-
-/-- The explicit finite coproduct cocone is a colimit cocone. -/
-def coprod.isColimit : Limits.IsColimit (coprod.binaryCofan X Y) := by
-  refine Limits.BinaryCofan.isColimitMk (fun s ↦ ofHom _ { toFun := Sum.elim s.inl s.inr }) ?_ ?_ ?_
-  all_goals cat_disch
-
-lemma coprod.inl_injective : Function.Injective (coprod.inl X Y) :=
-  Sum.inl_injective
-
-lemma coprod.inr_injective : Function.Injective (coprod.inr X Y) :=
-  Sum.inr_injective
-
-lemma coprod.inl_inr_jointly_surjective (r : coprod X Y) :
-    (∃ x : X, r = coprod.inl _ _ x) ∨ (∃ y : Y, r = coprod.inr _ _ y) := by
-  obtain (r | r) := r
-  exacts [Or.inl ⟨r, rfl⟩, Or.inr ⟨r, rfl⟩]
-
--- lemma finiteCoproduct.ι_desc_apply {B : CompHausLike P} {π : (a : α) → X a ⟶ B} (a : α) :
---     ∀ x, finiteCoproduct.desc X π (finiteCoproduct.ι X a x) = π a x := by
---   tauto
-
-instance : Limits.HasBinaryCoproduct X Y where
-  exists_colimit := ⟨coprod.binaryCofan X Y, coprod.isColimit X Y⟩
-
-variable (P) in
-/--
-A typeclass describing the property that forming all finite disjoint unions is stable under the
-property `P`.
--/
-class HasExplicitBinaryCoproducts : Prop where
-  hasProp (X Y : CompHausLike.{u} P) : HasExplicitBinaryCoproduct X Y
-
-attribute [instance] HasExplicitBinaryCoproducts.hasProp
-
-instance [HasExplicitBinaryCoproducts P] : Limits.HasBinaryCoproducts (CompHausLike P) :=
-  Limits.hasBinaryCoproducts_of_hasColimit_pair _
-
-/-- The inclusion maps into the explicit finite coproduct are open embeddings. -/
-lemma coprod.isOpenEmbedding_inl : IsOpenEmbedding (coprod.inl X Y) :=
-  IsOpenEmbedding.inl
-
-/-- The inclusion maps into the explicit finite coproduct are open embeddings. -/
-lemma coprod.isOpenEmbedding_inr : IsOpenEmbedding (coprod.inr X Y) :=
-  IsOpenEmbedding.inr
+  exacts [ConcreteCategory.congr_hom h₁ _, ConcreteCategory.congr_hom h₂ _]
 
-instance : HasExplicitBinaryCoproducts
-    (fun X ↦ TotallyDisconnectedSpace X ∧ SecondCountableTopology X) where
-  hasProp _ _ := { hasProp := ⟨inferInstance, inferInstance⟩ }
+end Coproduct
 
 end BinaryCoproducts

LeanCondensed/Projects/Proj.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jonas van der Schaaf
 -/
 import Mathlib.Condensed.Light.InternallyProjective
+import Mathlib.Topology.FiberPartition
 import LeanCondensed.Projects.LightProfiniteInjective
 import LeanCondensed.Projects.PreservesCoprod
 import LeanCondensed.Projects.Epi
@@ -180,16 +181,14 @@ lemma refinedCover {S T : LightProfinite} (π : T ⟶ S ⊗ ℕ∪{∞}) [Epi π
     have : Function.Surjective π := by rwa [← LightProfinite.epi_iff_surjective]
     let p (s : S) (n : ℕ∪{∞}) : T := (this (s, n)).choose
     have hp (s : S) (n : ℕ∪{∞}) : π (p s n) = (s, n) := (this (s, n)).choose_spec
-    refine ⟨⟨fun n ↦ ⟨p y n, ?_⟩, ?_⟩, ?_⟩
-    · simp [hp]; rfl
-    · simp [hp]
-    · simp [y', hp]
+    exact ⟨⟨fun n ↦ ⟨p y n, by simp [hp]; rfl⟩, by simp [hp]⟩, by simp [y', hp]⟩
   · simp [π_tilde, CompHausLike.pullback.condition]
-  · exact ⟨⟨⟨sectionOfFibreIncl π_tilde σ' hσ', .subtype_mk (.subtype_mk (by fun_prop) _) _⟩⟩, rfl⟩
+  · exact ⟨TopCat.ofHom ⟨(sectionOfFibreIncl π_tilde σ' hσ'),
+      (.subtype_mk (.subtype_mk (by fun_prop) _) _)⟩, rfl⟩
   · rw [LightProfinite.epi_iff_surjective]
     exact smartCoverToFun_surjective _ _ hσ hσ'
 
-private lemma comm_sq {X Y : LightCondMod R} (p : X ⟶ Y) [hp : Epi p] {S : LightProfinite}
+lemma comm_sq {X Y : LightCondMod R} (p : X ⟶ Y) [hp : Epi p] {S : LightProfinite}
     (f : (free R).obj (S).toCondensed ⟶ Y) :
       ∃ (T : LightProfinite) (π : T ⟶ S) (g : ((free R).obj T.toCondensed) ⟶ X),
         Epi π ∧ (lightProfiniteToLightCondSet ⋙ (free R)).map π ≫ f = g ≫ p := by
@@ -232,22 +231,23 @@ noncomputable def c {X : LightCondMod R} {S T : LightProfinite} (π : T ⟶ (S 
     refine parallelPairNatTrans (_ ≫ g_tilde) g_tilde ?_ rfl
     rw [← cancel_epi ((lightProfiniteToLightCondSet ⋙ (free R)).map <| smartCoverNew π)]
     apply (isColimitOfPreserves (lightProfiniteToLightCondSet ⋙ (free R))
-        (CompHausLike.coprod.isColimit _ _)).hom_ext
+        (CompHausLike.coproductIsColimit _ _)).hom_ext
     rintro ⟨⟨⟩⟩
     · simp [← Functor.map_comp_assoc, ← Functor.map_comp]
       rfl
-    · simp only [comp_obj, pair_obj_right, const_obj_obj, mapCocone_pt, BinaryCofan.mk_pt,
-        mapCocone_ι_app, BinaryCofan.mk_inr, Functor.comp_map, parallelPair_obj_zero,
-        parallelPair_obj_one, parallelPair_map_left, ← map_comp_assoc, ← Functor.map_comp,
-        parallelPair_map_right, const_obj_map, Category.comp_id]
-      have : smartCoverNew π =
-          CompHausLike.coprod.desc (CompHausLike.pullback.lift _ _ (𝟙 T) (𝟙 T) (by simp))
-            (CompHausLike.pullback.lift _ _ ((CompHausLike.pullback.fst _ _) ≫ fibre_incl _ _)
-              ((CompHausLike.pullback.snd _ _) ≫ fibre_incl _ _)
-              (by simp [CompHausLike.pullback.condition])) := rfl
-      simp only [this, CompHausLike.coprod.inr_desc_assoc, CompHausLike.pullback.lift_fst, comp_obj,
-        Functor.comp_map, Preadditive.comp_add, Preadditive.comp_sub, ← map_comp_assoc,
-        ← Functor.map_comp, Category.assoc, CompHausLike.pullback.lift_snd, g_tilde]
+    · simp only [comp_obj, pair_obj_right, const_obj_obj, mapCocone_pt, mapCocone_ι_app,
+        Functor.comp_map, parallelPair_obj_zero, parallelPair_obj_one, parallelPair_map_left,
+        ← map_comp_assoc, ← Functor.map_comp, parallelPair_map_right, const_obj_map, Category.comp_id]
+      have : smartCoverNew π = (BinaryCofan.IsColimit.desc' (CompHausLike.coproductIsColimit _ _)
+          (CompHausLike.pullback.lift _ _ (𝟙 T) (𝟙 T) (by simp))
+          (CompHausLike.pullback.lift _ _ ((CompHausLike.pullback.fst _ _) ≫ fibre_incl _ _)
+            ((CompHausLike.pullback.snd _ _) ≫ fibre_incl _ _)
+            (by simp [CompHausLike.pullback.condition]))).val := rfl
+      simp only [this, pair_obj_left, const_obj_obj, pair_obj_right,
+        BinaryCofan.IsColimit.desc'_coe, IsColimit.fac_assoc, BinaryCofan.mk_pt, BinaryCofan.mk_inr,
+        CompHausLike.pullback.lift_fst, comp_obj, Functor.comp_map, Preadditive.comp_add,
+        Preadditive.comp_sub, ← map_comp_assoc, ← Functor.map_comp, Category.assoc,
+        CompHausLike.pullback.lift_snd, g_tilde]
       simp only [← Functor.comp_map, ← Category.assoc, hr, Category.id_comp, sub_self, zero_add]
       simp [CompHausLike.pullback.condition]