Epimorphisms of condensed objects

This file characterises epimorphisms of condensed sets and condensed R-modules for any ring R, as those morphisms which are objectwise surjective on Stonean (see CondensedSet.epi_iff_surjective_on_stonean and CondensedMod.epi_iff_surjective_on_stonean).

theorem Condensed.epi_iff_locallySurjective_on_compHaus (A : Type u') [CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type v'} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization A] {X Y : Condensed A} (f : X ⟶ Y) [(CategoryTheory.coherentTopology CompHaus).WEqualsLocallyBijective A] [CategoryTheory.HasSheafify (CategoryTheory.coherentTopology CompHaus) A] [(CategoryTheory.coherentTopology CompHaus).HasSheafCompose (CategoryTheory.forget A)] [CategoryTheory.Balanced (CategoryTheory.Sheaf (CategoryTheory.coherentTopology CompHaus) A)] [CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget A)] : CategoryTheory.Epi f ↔ ∀ (S : CompHaus) (y : CategoryTheory.ToType (Y.val.obj (Opposite.op S))), ∃ (S' : CompHaus) (φ : S' ⟶ S) (_ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom φ)) (x : CategoryTheory.ToType (X.val.obj (Opposite.op S'))), (CategoryTheory.ConcreteCategory.hom (f.val.app (Opposite.op S'))) x = (CategoryTheory.ConcreteCategory.hom (Y.val.map (Opposite.op φ))) y

theorem Condensed.epi_iff_surjective_on_stonean (A : Type u') [CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type v'} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization A] {X Y : Condensed A} (f : X ⟶ Y) [CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget A)] [∀ (X : CompHausᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X Stonean.toCompHaus.op) A] [(CategoryTheory.extensiveTopology Stonean).WEqualsLocallyBijective A] [CategoryTheory.HasSheafify (CategoryTheory.extensiveTopology Stonean) A] [(CategoryTheory.extensiveTopology Stonean).HasSheafCompose (CategoryTheory.forget A)] [CategoryTheory.Balanced (CategoryTheory.Sheaf (CategoryTheory.extensiveTopology Stonean) A)] : CategoryTheory.Epi f ↔ ∀ (S : Stonean), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (f.val.app (Opposite.op S.compHaus)))

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

theorem CondensedSet.epi_iff_surjective_on_stonean {X Y : CondensedSet} (f : X ⟶ Y) : CategoryTheory.Epi f ↔ ∀ (S : Stonean), Function.Surjective (f.val.app (Opposite.op S.compHaus))

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

theorem CondensedMod.epi_iff_surjective_on_stonean (R : Type (u + 1)) [Ring R] {X Y : CondensedMod R} (f : X ⟶ Y) : CategoryTheory.Epi f ↔ ∀ (S : Stonean), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (f.val.app (Opposite.op S.compHaus)))