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] [CategoryTheory.ConcreteCategory A] [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.forget A).obj (Y.val.obj (Opposite.op S))), ∃ (S' : CompHaus) (φ : 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 Condensed.epi_iff_surjective_on_stonean (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] [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 ⇑(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 ⇑φ) (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 ⇑φ) (x : ↑(X.val.obj (Opposite.op S'))), (f.val.app (Opposite.op S')).hom x = (Y.val.map (Opposite.op φ)).hom 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 ⇑(f.val.app (Opposite.op S.compHaus)).hom