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

• Stonean.effectiveEpi_tfae: For a morphism in Stonean, the conditions surjective, epimorphic, and effective epimorphic are all equivalent.

• Stonean.effectiveEpiFamily_tfae: For a finite family of morphisms in Stonean with fixed target in Stonean, the conditions jointly surjective, jointly epimorphic and effective epimorphic are all equivalent.

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

• TODO: Write API for reflecting effective epimorphisms and deduce the contents of this file by abstract nonsense from the corresponding results for CompHaus.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

instance Stonean.instPreregularStoneanInstLargeCategoryStonean : CategoryTheory.Preregular Stonean

Equations

• Stonean.instPreregularStoneanInstLargeCategoryStonean = (_ : CategoryTheory.Preregular Stonean)

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

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) : CategoryTheory.EffectiveEpiFamily X π

theorem CategoryTheory.EffectiveEpiFamily.toCompHaus {α : Type} [Finite α] {B : Stonean} {X : α → Stonean} {π : (a : α) → X a ⟶ B} (H : CategoryTheory.EffectiveEpiFamily X π) : CategoryTheory.EffectiveEpiFamily (fun (x : α) => Stonean.toCompHaus.toPrefunctor.obj (X x)) fun (x : α) => Stonean.toCompHaus.toPrefunctor.map (π x)