Effective epimorphisms in Stonean

This file proves that EffectiveEpi, Epi and Surjective are all equivalent in Stonean. As a consequence we deduce from the material in Mathlib/Topology/Category/CompHausLike/EffectiveEpi.lean that Stonean is Preregular and Precoherent.

We also prove that for a finite family of morphisms in Stonean with fixed target, the conditions jointly surjective, jointly epimorphic and effective epimorphic are all equivalent.

theorem Stonean.effectiveEpi_tfae {B X : Stonean} (π : X ⟶ B) : [CategoryTheory.EffectiveEpi π, CategoryTheory.Epi π, Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π)].TFAE

instance Stonean.instPreservesEffectiveEpisCompHausToCompHaus : toCompHaus.PreservesEffectiveEpis

instance Stonean.instReflectsEffectiveEpisCompHausToCompHaus : toCompHaus.ReflectsEffectiveEpis

noncomputable def Stonean.stoneanToCompHausEffectivePresentation (X : CompHaus) : toCompHaus.EffectivePresentation X

An effective presentation of an X : CompHaus with respect to the inclusion functor from Stonean

Equations

• Stonean.stoneanToCompHausEffectivePresentation X = { p := X.presentation, f := CompHaus.presentation.π X, effectiveEpi := ⋯ }

instance Stonean.instEffectivelyEnoughCompHausToCompHaus : toCompHaus.EffectivelyEnough

instance Stonean.instPreregular : CategoryTheory.Preregular Stonean

theorem Stonean.effectiveEpiFamily_tfae {α : Type} [Finite α] {B : Stonean} (X : α → Stonean) (π : (a : α) → X a ⟶ B) : [CategoryTheory.EffectiveEpiFamily X π, CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc π), ∀ (b : ↑B.toTop), ∃ (a : α) (x : ↑(X a).toTop), (CategoryTheory.ConcreteCategory.hom (π a)) x = b].TFAE

theorem Stonean.effectiveEpiFamily_of_jointly_surjective {α : Type} [Finite α] {B : Stonean} (X : α → Stonean) (π : (a : α) → X a ⟶ B) (surj : ∀ (b : ↑B.toTop), ∃ (a : α) (x : ↑(X a).toTop), (CategoryTheory.ConcreteCategory.hom (π a)) x = b) : CategoryTheory.EffectiveEpiFamily X π