Internal projectivity of the sequence space

LeanCondensed/Mathlib/CategoryTheory/Countable.lean

@@ -0,0 +1,13 @@
+import Mathlib.CategoryTheory.Countable
+
+universe u
+
+noncomputable section
+
+open CategoryTheory Quiver Countable
+
+instance {J : Type u} [ctble : Countable J] [Category J] [thin : Quiver.IsThin J]: CountableCategory J :=
+  CountableCategory.mk ctble (fun _ _ ↦ ⟨fun _ ↦ 0, fun _ _ _ ↦ (thin _ _).elim _ _⟩)
+
+noncomputable instance {J : Type u} [fin : Finite J] [Category J] [thin : Quiver.IsThin J] : FinCategory J := by
+  apply FinCategory.mk (Fintype.ofFinite J) (fun j j' ↦ Fintype.ofFinite (j ⟶ j'))

LeanCondensed/Mathlib/CategoryTheory/Functor/EpiMono.lean

@@ -0,0 +1,27 @@
+import Mathlib
+
+open CategoryTheory
+
+variable {C : Type*} [Category C] {D : Type*} [Category D] {F G : C ⥤ D}
+
+lemma epi_of_Retract {f g : Arrow C} (π : f ⟶ g) [Epi f.hom] [Epi π.right] : Epi g.hom :=
+  have : Epi (π.left ≫ g.hom) := by
+    rw [←Functor.id_map π.left, π.w, Functor.id_map]
+    exact epi_comp f.hom π.right
+  epi_of_epi (π.left) _
+
+lemma preservesEpi_of_Epi (f : F ⟶ G) (hf : ∀ X, Epi (f.app X)) (preserves : F.PreservesEpimorphisms)
+  : G.PreservesEpimorphisms where
+    preserves {X Y} π hπ :=
+      have : Epi (f.app X ≫ G.map π) := by
+        rw [←f.naturality π]
+        exact epi_comp (F.map π) (f.app Y)
+      epi_of_epi (f.app X) (G.map π)
+
+lemma preservesEpi_ofRetract (r : Retract G F) (preserves : F.PreservesEpimorphisms)
+  : G.PreservesEpimorphisms where
+    preserves := (
+      preservesEpi_of_Epi _
+        (fun _ ↦ (SplitEpi.mk (r.i.app _) (by rw [←NatTrans.comp_app, r.retract, NatTrans.id_app])).epi)
+        preserves
+    ).preserves

LeanCondensed/Projects/Epi.lean

@@ -0,0 +1,161 @@
+import Mathlib
+
+import LeanCondensed.Mathlib.CategoryTheory.Countable
+
+open Function CategoryTheory Limits Opposite
+
+universe u
+
+lemma surj_pullback' {X Y Z : LightProfinite.{u}} (f : X ⟶ Z) {g : Y ⟶ Z}
+    (hf : Function.Surjective f) : Function.Surjective ↑(pullback.snd f g) := by
+  intro y
+
+  let point : LightProfinite.{u} := LightProfinite.of PUnit
+  let point_map : point ⟶ Y := TopCat.ofHom ⟨fun _ ↦ y, continuous_const⟩
+
+  rcases hf (g y) with ⟨z, hz⟩
+
+  let point_map' : point ⟶ X := TopCat.ofHom ⟨fun _ ↦ z, continuous_const⟩
+
+  use pullback.lift point_map' point_map (by ext; erw [hz]; rfl) PUnit.unit
+
+  rw [←ConcreteCategory.comp_apply, pullback.lift_snd]
+  rfl
+
+instance surj_widePullback {J : Type*} (B : LightProfinite.{u}) (objs : J → LightProfinite)
+  (arrows: (j : J) → (objs j ⟶ B)) (hepi : ∀ j, Epi (arrows j)) [HasWidePullback B objs arrows]
+    : ∀ j, Epi (WidePullback.π arrows j) := by
+  classical
+  intro i
+  simp [LightProfinite.epi_iff_surjective] at ⊢ hepi
+  intro xi
+  let point : LightProfinite.{u} := LightProfinite.of PUnit
+  let base_pt : B := arrows i xi
+  have choice : ∀ j, ∃ xj, arrows j xj = base_pt := fun j ↦ hepi j base_pt
+  let point_maps : (j : J) → (point ⟶ objs j) := (fun j ↦
+    if h : i = j then
+      CompHausLike.ofHom _ (ContinuousMap.const point (h ▸ xi))
+    else
+      (CompHausLike.ofHom _ (ContinuousMap.const point (choice j).choose))
+  )
+  let lift : point ⟶ widePullback B objs arrows :=
+    WidePullback.lift (CompHausLike.ofHom _ (ContinuousMap.const point base_pt)) point_maps
+    (
+      by
+        intro j
+        unfold point_maps
+        by_cases h : i = j
+        · rw [dif_pos h]
+          subst h
+          rfl
+        · rw [dif_neg h]
+          ext x
+          simp only [ConcreteCategory.comp_apply, CompHausLike.hom_ofHom, ContinuousMap.const_apply]
+          exact (choice j).choose_spec
+    )
+  use lift PUnit.unit
+  rw [←ConcreteCategory.comp_apply, WidePullback.lift_π]
+  simp [point_maps]
+
+
+
+
+instance : lightProfiniteToLightCondSet.PreservesEpimorphisms := {
+  preserves f hf := (LightCondSet.epi_iff_locallySurjective_on_lightProfinite _).mpr
+    fun _ g ↦
+      ⟨
+        pullback f g,
+        pullback.snd _ _,
+        surj_pullback' f ((LightProfinite.epi_iff_surjective f).mp hf),
+        pullback.fst _ _,
+        pullback.condition
+      ⟩
+}
+
+lemma stupid {A : Type u} {s : Set A} {x y : A} {px : x ∈ s} {py : y ∈ s} (h : (⟨x, px⟩ : s) = ⟨y, py⟩) : x = y
+  := by
+    rwa [Subtype.ext_iff] at h
+
+noncomputable def πpair {X Y : LightProfinite} (π : X ⟶ Y) : WalkingParallelPair ⥤ LightCondSet :=
+  parallelPair
+    (lightProfiniteToLightCondSet.map <| pullback.fst π π)
+    (lightProfiniteToLightCondSet.map <| pullback.snd π π)
+
+noncomputable def regular {X Y : LightProfinite} (π : X ⟶ Y)
+    : Cofork (lightProfiniteToLightCondSet.map <| pullback.fst π π) (lightProfiniteToLightCondSet.map <| pullback.snd π π) := Cofork.ofπ (lightProfiniteToLightCondSet.map <| π) (by
+  rw [
+    ←lightProfiniteToLightCondSet.map_comp,
+    ←lightProfiniteToLightCondSet.map_comp,
+    pullback.condition
+  ])
+
+def cfork {X Y : LightProfinite} (π : X ⟶ Y)
+  := Cofork (lightProfiniteToLightCondSet.map (pullback.fst π π)) (lightProfiniteToLightCondSet.map (pullback.snd π π))
+
+noncomputable def regularLiftElem {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π]
+      (cone : cfork π) : cone.pt.val.obj (op Y)
+    :=
+  let fX := yonedaEquiv cone.π.val
+  have : cone.pt.val.map (pullback.fst π π).op fX = cone.pt.val.map (pullback.snd π π).op fX := by
+    have this : (lightProfiniteToLightCondSet.map (pullback.fst π π) ≫ cone.π).val = (yoneda.map (pullback.fst π π) ≫ cone.π.val) := rfl
+    have this' : (lightProfiniteToLightCondSet.map (pullback.snd π π) ≫ cone.π).val = (yoneda.map (pullback.snd π π) ≫ cone.π.val) := rfl
+
+    erw [
+        yonedaEquiv_naturality (F := cone.pt.val) cone.π.val (pullback.fst π π),
+        yonedaEquiv_naturality (F := cone.pt.val) cone.π.val (pullback.snd π π),
+        ←this, ←this',
+        cone.condition,
+    ]
+  (((LightCondensed.equalizerCondition cone.pt).bijective_mapToEqualizer_pullback _ _ _ π).surjective ⟨fX, this⟩).choose
+
+private lemma cone_elem {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π] (cone : cfork π)
+    : cone.pt.val.map (pullback.fst π π).op (yonedaEquiv cone.π.val) = cone.pt.val.map (pullback.snd π π).op (yonedaEquiv cone.π.val) := by
+  have this : (lightProfiniteToLightCondSet.map (pullback.fst π π) ≫ cone.π).val = (yoneda.map (pullback.fst π π) ≫ cone.π.val) := rfl
+  have this' : (lightProfiniteToLightCondSet.map (pullback.snd π π) ≫ cone.π).val = (yoneda.map (pullback.snd π π) ≫ cone.π.val) := rfl
+  erw [
+      yonedaEquiv_naturality (F := cone.pt.val) cone.π.val (pullback.fst π π),
+      yonedaEquiv_naturality (F := cone.pt.val) cone.π.val (pullback.snd π π),
+      ←this, ←this',
+      cone.condition,
+  ]
+
+noncomputable def regularLift {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π] (cone : cfork π) : lightProfiniteToLightCondSet.obj Y ⟶ cone.pt
+  := ⟨ yonedaEquiv.symm (regularLiftElem π cone) ⟩
+
+private lemma regularLift_prop {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π] (cone : cfork π)
+    : regularTopology.MapToEqualizer cone.pt.val π (pullback.fst π π) (pullback.snd π π) pullback.condition (regularLiftElem π cone) = ⟨yonedaEquiv cone.π.val, cone_elem π cone⟩
+  := (((LightCondensed.equalizerCondition cone.pt).bijective_mapToEqualizer_pullback _ _ _ π).surjective ⟨yonedaEquiv cone.π.val, cone_elem π cone⟩).choose_spec
+
+lemma regularLift_comp {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π] (cone : cfork π)
+    : (regular π).π ≫ regularLift π cone = cone.π := by
+  refine Sheaf.Hom.ext (yonedaEquiv.injective ?_)
+  erw [←yonedaEquiv_naturality (F := cone.pt.val), Equiv.apply_symm_apply]
+  exact stupid (s := {x : cone.pt.val.obj (Opposite.op X) | cone.pt.val.map (pullback.fst π π).op x = cone.pt.val.map (pullback.snd π π).op x}) (regularLift_prop π cone)
+
+lemma regularLift_unique {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π] (cone : cfork π)
+      (m : (lightProfiniteToLightCondSet.obj Y) ⟶ cone.pt) (hm : (regular π).π ≫ m = cone.π)
+    : m = regularLift π cone := by
+  erw [Cofork.π_ofπ, ←regularLift_comp π cone] at hm
+  exact Epi.left_cancellation _ _ hm
+
+noncomputable abbrev regular_IsColimit {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π]
+    : IsColimit (regular π)
+  := Cofork.IsColimit.mk _ (regularLift π) (regularLift_comp π) (regularLift_unique π)
+
+noncomputable abbrev regular_RegularEpi {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π]
+    : RegularEpi (lightProfiniteToLightCondSet.map π) where
+  W := lightProfiniteToLightCondSet.obj (pullback π π)
+  left := lightProfiniteToLightCondSet.map (pullback.fst π π)
+  right := lightProfiniteToLightCondSet.map (pullback.snd π π)
+  w := by
+    rw [
+      ←lightProfiniteToLightCondSet.map_comp,
+      ←lightProfiniteToLightCondSet.map_comp,
+      pullback.condition
+    ]
+  isColimit := regular_IsColimit π
+
+instance : lightProfiniteToLightCondSet.PreservesEffectiveEpis where
+  preserves π _ :=
+    have : RegularEpi (lightProfiniteToLightCondSet.map π) := regular_RegularEpi π
+    inferInstance

LeanCondensed/Projects/Initial.lean

@@ -0,0 +1,28 @@
+import Mathlib
+
+open CategoryTheory Limits Condensed
+
+universe u
+
+def empty_elim {p : Sort u} {X : LightProfinite} (hX : ¬Nonempty X) (x : X) : p := (hX ⟨x⟩).elim
+
+def empty_subset {X : LightProfinite} (hX : ¬Nonempty X) (s : Set X) : s = ⊤ := by
+  ext x
+  exact empty_elim hX x
+
+def empty_map {X Y : LightProfinite} (hY : ¬Nonempty Y) (f : X ⟶ Y) : ¬Nonempty X
+  := fun h ↦ h.elim (fun x ↦ hY ⟨f x⟩)
+
+def empty_iso {X Y : LightProfinite} (hY : ¬Nonempty Y) (f : X ⟶ Y) : IsIso f := by
+  let finv : Y ⟶ X := CompHausLike.ofHom _ {
+    toFun y := empty_elim hY y
+    continuous_toFun := by
+      apply Continuous.mk
+      intro s empty_elim
+      rw [empty_subset hY ((fun y ↦ _root_.empty_elim hY y) ⁻¹' s)]
+      exact TopologicalSpace.isOpen_univ
+  }
+  refine IsIso.mk ⟨finv, ?_⟩
+  constructor <;> ext x
+  exact empty_elim hY (f x)
+  exact empty_elim hY x

LeanCondensed/Projects/InternallyProjective.lean

@@ -5,6 +5,7 @@ Authors: Dagur Asgeirsson
 -/
 import Mathlib.Condensed.Light.Epi
 import LeanCondensed.LightCondensed.Yoneda
+import LeanCondensed.Mathlib.CategoryTheory.Functor.EpiMono
 import LeanCondensed.Mathlib.Condensed.Light.Limits
 import LeanCondensed.Mathlib.Condensed.Light.Monoidal
 import LeanCondensed.Mathlib.Topology.Category.LightProfinite.ChosenFiniteProducts
@@ -30,6 +31,16 @@ variable {C : Type*} [Category C] [MonoidalCategory C] [MonoidalClosed C]
 class InternallyProjective (P : C) : Prop where
   preserves_epi : (ihom P).PreservesEpimorphisms
 
+theorem ofRetract {X Y : C} (r : Retract Y X) (proj : InternallyProjective X)
+    : InternallyProjective Y :=
+  haveI : Retract (ihom Y) (ihom X) := {
+    i := MonoidalClosed.pre r.r
+    r := MonoidalClosed.pre r.i
+    retract := by
+      rw [←MonoidalClosed.pre_map, r.retract, MonoidalClosed.pre_id]
+  }
+  InternallyProjective.mk <| preservesEpi_ofRetract this proj.preserves_epi
+
 end InternallyProjective
 
 open CategoryTheory LightProfinite OnePoint Limits LightCondensed MonoidalCategory MonoidalClosed
@@ -48,6 +59,9 @@ def ihomPoints (A B : LightCondMod.{u} R) (S : LightProfinite) :
 -- We have an `R`-module structure on `M ⟶ N` for condensed `R`-modules `M`, `N`,
 -- and this could be made an `≅`. But it's not needed in this proof.
 
+
+lemma tensorLeft_obj (X Y : LightCondMod.{u} R) : (tensorLeft X).obj Y = X ⊗ Y := rfl
+
 lemma ihom_map_val_app (A B P : LightCondMod.{u} R) (S : LightProfinite) (e : A ⟶ B) :
     ∀ x, ConcreteCategory.hom (((ihom P).map e).val.app ⟨S⟩) x =
         (ihomPoints R P B S).symm (ihomPoints R P A S x ≫ e) := by

LeanCondensed/Projects/LightSolid.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Dagur Asgeirsson
 -/
 import LeanCondensed.Projects.InternallyProjective
+import LeanCondensed.Projects.Proj
+import LeanCondensed.Projects.Sequence
 /-!
 
 # Project: light solid abelian groups
@@ -47,7 +49,7 @@ def shift : ℕ∪{∞} ⟶ ℕ∪{∞} := TopCat.ofHom {
     intro U h hU
     simp only [isOpen_iff_of_mem h, isClosed_discrete, isCompact_iff_finite, true_and] at hU
     refine ⟨sSup (Option.some ⁻¹' U)ᶜ + 1, fun n hn ↦ by
-      simpa using not_mem_of_csSup_lt (Nat.succ_le_iff.mp hn) (Set.Finite.bddAbove hU)⟩ }
+      simpa using notMem_of_csSup_lt (Nat.succ_le_iff.mp hn) (Set.Finite.bddAbove hU)⟩ }
 
 end LightProfinite
 
@@ -56,20 +58,10 @@ namespace LightCondensed
 variable (R : Type _) [CommRing R]
 -- might need some more assumptions eventually, finite type over `ℤ`?
 
-def P_map :
-    (free R).obj (LightProfinite.of PUnit.{1}).toCondensed ⟶ (free R).obj (ℕ∪{∞}).toCondensed :=
-  (lightProfiniteToLightCondSet ⋙ free R).map (TopCat.ofHom ⟨fun _ ↦ ∞, continuous_const⟩)
+instance : InternallyProjective ((free R).obj (ℕ∪{∞}).toCondensed) :=
+  internallyProjective_ℕinfty _
 
-def P : LightCondMod R := cokernel (P_map R)
-
-def P_proj : (free R).obj (ℕ∪{∞}).toCondensed ⟶ P R := cokernel.π _
-
-def P_homMk (A : LightCondMod R) (f : (free R).obj (ℕ∪{∞}).toCondensed ⟶ A)
-    (hf : P_map R ≫ f = 0) : P R ⟶ A := cokernel.desc _ f hf
-
-instance : InternallyProjective (P R) := sorry
-
-instance : InternallyProjective ((free R).obj (ℕ∪{∞}).toCondensed) := sorry
+instance : InternallyProjective (P R) := ofRetract (P_retract _) inferInstance
 
 variable (R : Type) [CommRing R]
 
@@ -82,7 +74,9 @@ def oneMinusShift' : (free R).obj (ℕ∪{∞}).toCondensed ⟶ (free R).obj (
 
 def oneMinusShift : P R ⟶ P R := by
   refine P_homMk R _ (oneMinusShift' R) ?_ ≫ P_proj R
-  sorry
+  erw [Preadditive.comp_sub, Category.comp_id]
+  simp only [sub_eq_zero, P_map, ←Functor.map_comp]
+  rfl
 
 variable {R : Type} [CommRing R]
 

LeanCondensed/Projects/LocalizedMonoidal.lean

@@ -93,7 +93,7 @@ def coreMonoidalTransport {F G : C ⥤ D} [F.Monoidal] (i : F ≅ G) : G.CoreMon
     simp only [tensor_whiskerLeft, Functor.LaxMonoidal.associativity, Category.assoc,
       Iso.inv_hom_id_assoc]
     rw [← tensorHom_id, associator_naturality_assoc]
-    simp [← id_tensorHom, ← tensorHom_id, ← tensor_comp, ← tensor_comp_assoc]
+    simp [← id_tensorHom, ← tensorHom_id, ← tensor_comp_assoc]
   left_unitality X := by
     simp only [Iso.trans_hom, εIso_hom, Iso.app_hom, ← tensorHom_id, tensorIso_hom, Iso.symm_hom,
       μIso_hom, Category.assoc, ← tensor_comp_assoc, Iso.hom_inv_id_app, Category.comp_id,