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
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)))