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.obj.obj (Opposite.op S))),
∃ (S' : CompHaus) (φ : 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 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.hom.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.obj.obj (Opposite.op S)),
∃ (S' : CompHaus) (φ : 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 CondensedSet.epi_iff_surjective_on_stonean {X Y : CondensedSet} (f : X ⟶ Y) :
CategoryTheory.Epi f ↔ ∀ (S : Stonean), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (f.hom.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.obj.obj (Opposite.op S))),
∃ (S' : CompHaus) (φ : 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 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.hom.app (Opposite.op S.compHaus)))