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.

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

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

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