Internal projectivity of the sequence space

LeanCondensed.lean

@@ -2,7 +2,6 @@ import LeanCondensed.LightCondensed.Small
 import LeanCondensed.LightCondensed.Yoneda
 import LeanCondensed.Mathlib.CategoryTheory.Localization.Bifunctor
 import LeanCondensed.Mathlib.CategoryTheory.Localization.Monoidal.Braided
-import LeanCondensed.Mathlib.CategoryTheory.Monoidal.Braided.Transport
 import LeanCondensed.Mathlib.CategoryTheory.Sites.DirectImage
 import LeanCondensed.Mathlib.CategoryTheory.Sites.Monoidal
 import LeanCondensed.Mathlib.Condensed.Adjunctions

LeanCondensed/LightCondensed/Small.lean

@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2025 Dagur Asgeirsson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Dagur Asgeirsson
+-/
 import Mathlib.CategoryTheory.Sites.Coherent.Equivalence
 import Mathlib.Condensed.Light.Module
 

LeanCondensed/LightCondensed/Yoneda.lean

@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2025 Dagur Asgeirsson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Dagur Asgeirsson
+-/
 import Mathlib.Condensed.Light.Functors
 import Mathlib.Condensed.Light.Module
 

LeanCondensed/Mathlib/CategoryTheory/Countable.lean

@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2025 Jonas van der Schaaf. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jonas van der Schaaf
+-/
+import Mathlib.CategoryTheory.Countable
+
+universe u
+
+noncomputable section
+
+open CategoryTheory Quiver Countable
+
+instance {J : Type u} [Countable J] [Category J] [Quiver.IsThin J] :
+    CountableCategory J :=
+  CountableCategory.mk inferInstance (fun _ _ ↦ ⟨fun _ ↦ 0, fun _ _ _ ↦ Subsingleton.elim _ _⟩)
+
+noncomputable instance {J : Type u} [Finite J] [Category J] [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,30 @@
+/-
+Copyright (c) 2025 Jonas van der Schaaf. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jonas van der Schaaf
+-/
+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)) [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) [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

LeanCondensed/Mathlib/CategoryTheory/Localization/Bifunctor.lean

@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2025 Dagur Asgeirsson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Dagur Asgeirsson
+-/
 import Mathlib.CategoryTheory.Localization.Bifunctor
 
 namespace CategoryTheory

LeanCondensed/Mathlib/Condensed/Light/Monoidal.lean

@@ -5,9 +5,9 @@ Authors: Dagur Asgeirsson
 -/
 import Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
 import Mathlib.CategoryTheory.Monoidal.Braided.Reflection
+import Mathlib.CategoryTheory.Monoidal.Braided.Transport
 import Mathlib.Condensed.Discrete.Module
 import Mathlib.Condensed.Light.CartesianClosed
-import LeanCondensed.Mathlib.CategoryTheory.Monoidal.Braided.Transport
 import LeanCondensed.Mathlib.CategoryTheory.Sites.Monoidal
 import LeanCondensed.Mathlib.Condensed.Light.Small
 import LeanCondensed.Projects.SheafMonoidal
@@ -156,8 +156,8 @@ instance : (free R).Monoidal := by
               Functor.leftUnitor _
         · intros
           ext
-          simp [equivSmall, Equivalence.sheafCongr,
-            Equivalence.sheafCongr.functor, Equivalence.sheafCongr.inverse]
+          simp [Equivalence.sheafCongr, Equivalence.sheafCongr.functor,
+            Equivalence.sheafCongr.inverse]
       · refine ?_ ≪≫ (Functor.associator _ _ _)
         refine (Functor.associator _ _ _).symm ≪≫ ?_
         refine (Functor.associator _ _ _).symm ≪≫ ?_
@@ -182,7 +182,7 @@ instance : (free R).Monoidal := by
             Functor.associator_inv_app, Functor.associator_hom_app, Functor.id_obj, NatTrans.op_app,
             Functor.leftUnitor_hom_app, CategoryTheory.Functor.map_id, Category.comp_id,
             Category.id_comp, Category.assoc]
-          simp [← Functor.map_comp, ← Functor.map_comp_assoc]
+          simp [← Functor.map_comp]
   exact monoidalTransport i.symm
 
 attribute [local instance] monoidalCategory in

LeanCondensed/Projects/Epi.lean

@@ -0,0 +1,160 @@
+/-
+Copyright (c) 2025 Jonas van der Schaaf. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jonas van der Schaaf
+-/
+import Mathlib.CategoryTheory.EffectiveEpi.RegularEpi
+import Mathlib.Combinatorics.Quiver.ReflQuiver
+import Mathlib.Condensed.Light.Epi
+import Mathlib.Condensed.Light.Explicit
+import Mathlib.Condensed.Light.Functors
+import Mathlib.Topology.Compactness.PseudometrizableLindelof
+import Mathlib.Topology.Connected.Separation
+import Mathlib.Topology.Spectral.Prespectral
+
+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 only [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⟩ }
+
+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
+  rw [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]
+  have h := regularLift_prop π cone
+  rwa [Subtype.ext_iff] at h
+
+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