Effective epimorphic families in Stonean #

This file proves that Stonean is Preregular. Together with the fact that it is FinitaryPreExtensive, this implies that Stonean is Precoherent.

To do this, we need to characterise effective epimorphisms in Stonean. As a consequence, we also get a characterisation of finite effective epimorphic families.

Main results #

As a consequence, we obtain instances that Stonean is precoherent and preregular.

noncomputable def Stonean.struct {B : Stonean} {X : Stonean} (π : X B) (hπ : Function.Surjective π) :

Implementation: If π is a surjective morphism in Stonean, then it is an effective epi. The theorem Stonean.effectiveEpi_tfae should be used instead.

  • One or more equations did not get rendered due to their size.
Instances For
    noncomputable def Stonean.stoneanToCompHausEffectivePresentation (X : CompHaus) :
    Stonean.toCompHaus.EffectivePresentation X

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

    Instances For
      theorem Stonean.effectiveEpiFamily_tfae {α : Type} [Finite α] {B : Stonean} (X : αStonean) (π : (a : α) → X a B) :
      [CategoryTheory.EffectiveEpiFamily X π, CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc π), ∀ (b : CoeSort.coe B), ∃ (a : α) (x : CoeSort.coe (X a)), (π a) x = b].TFAE
      theorem Stonean.effectiveEpiFamily_of_jointly_surjective {α : Type} [Finite α] {B : Stonean} (X : αStonean) (π : (a : α) → X a B) (surj : ∀ (b : CoeSort.coe B), ∃ (a : α) (x : CoeSort.coe (X a)), (π a) x = b) :