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 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 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 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
instance
LightCondMod.instReflectsEpimorphismsLightCondSetForget
(R : Type u)
[Ring R]
:
(LightCondensed.forget R).ReflectsEpimorphisms
Equations
- ⋯ = ⋯
instance
LightCondMod.instPreservesEpimorphismsLightCondSetForget
(R : Type u)
[Ring R]
:
(LightCondensed.forget R).PreservesEpimorphisms
Equations
- ⋯ = ⋯
theorem
LightCondensed.epi_π_app_zero_of_epi
(R : Type u_1)
[Ring R]
{F : CategoryTheory.Functor ℕᵒᵖ (LightCondMod R)}
{c : CategoryTheory.Limits.Cone F}
(hc : CategoryTheory.Limits.IsLimit c)
(hF : ∀ (n : ℕ), CategoryTheory.Epi (F.map (CategoryTheory.homOfLE ⋯).op))
:
CategoryTheory.Epi (c.π.app (Opposite.op 0))