Epimorphisms of light condensed objects

This file characterises epimorphisms in light condensed sets and modules as the locally surjective morphisms. Here, the condition of locally surjective is phrased in terms of continuous surjections of light profinite sets.

Further, we prove that the functor lim : Discrete ℕ ⥤ LightCondMod R preserves epimorphisms.

theorem LightCondensed.isLocallySurjective_iff_locallySurjective_on_lightProfinite (A : Type u') [CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget A)] {X Y : LightCondensed A} (f : X ⟶ Y) : CategoryTheory.Sheaf.IsLocallySurjective f ↔ ∀ (S : LightProfinite) (y : CategoryTheory.ToType (Y.obj.obj (Opposite.op S))), ∃ (S' : LightProfinite) (φ : S' ⟶ S) (_ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom φ)) (x : CategoryTheory.ToType (X.obj.obj (Opposite.op S'))), (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op S'))) x = (CategoryTheory.ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y

theorem LightCondSet.epi_iff_locallySurjective_on_lightProfinite {X Y : LightCondSet} (f : X ⟶ Y) : CategoryTheory.Epi f ↔ ∀ (S : LightProfinite) (y : Y.obj.obj (Opposite.op S)), ∃ (S' : LightProfinite) (φ : S' ⟶ S) (_ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom φ)) (x : X.obj.obj (Opposite.op S')), (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op S'))) x = (CategoryTheory.ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y

theorem LightCondMod.epi_iff_locallySurjective_on_lightProfinite (R : Type u) [Ring R] {X Y : LightCondMod R} (f : X ⟶ Y) : CategoryTheory.Epi f ↔ ∀ (S : LightProfinite) (y : ↑(Y.obj.obj (Opposite.op S))), ∃ (S' : LightProfinite) (φ : S' ⟶ S) (_ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom φ)) (x : ↑(X.obj.obj (Opposite.op S'))), (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op S'))) x = (CategoryTheory.ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y

instance LightCondMod.instReflectsEpimorphismsLightCondSetForget (R : Type u) [Ring R] : (LightCondensed.forget R).ReflectsEpimorphisms

instance LightCondMod.instPreservesEpimorphismsLightCondSetForget (R : Type u) [Ring R] : (LightCondensed.forget R).PreservesEpimorphisms

theorem LightCondMod.factorsThru_lightProfinite_epi_of_epi (R : Type u) [Ring R] {X Y : LightCondMod R} (f : X ⟶ Y) [CategoryTheory.Epi f] {S : LightProfinite} (p : (LightCondensed.free R).obj S.toCondensed ⟶ Y) : ∃ (T : LightProfinite) (π : T ⟶ S) (g : (LightCondensed.free R).obj T.toCondensed ⟶ X), CategoryTheory.Epi π ∧ CategoryTheory.CategoryStruct.comp ((lightProfiniteToLightCondSet.comp (LightCondensed.free R)).map π) p = CategoryTheory.CategoryStruct.comp g f

theorem LightCondensed.epi_π_app_zero_of_epi (R : Type u_1) [Ring R] {F : CategoryTheory.Functor ℕᵒᵖ (LightCondMod R)} {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (hF : ∀ (n : ℕ), CategoryTheory.Epi (F.map (CategoryTheory.homOfLE ⋯).op)) : CategoryTheory.Epi (c.π.app (Opposite.op 0))

instance LightCondensed.instEpiLightCondModMapNat {R : Type u} [Ring R] {M N : ℕ → LightCondMod R} (f : (n : ℕ) → M n ⟶ N n) [∀ (n : ℕ), CategoryTheory.Epi (f n)] : CategoryTheory.Epi (CategoryTheory.Limits.Pi.map f)

instance LightCondensed.instPreservesEpimorphismsFunctorDiscreteNatLightCondModLim {R : Type u} [Ring R] : CategoryTheory.Limits.lim.PreservesEpimorphisms