Effective epimorphisms and finite effective epimorphic families in CompHaus

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

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

Main results

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

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

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

Projects

• Define regular categories, and show that CompHaus is regular.
• Define coherent categories, and show that CompHaus is actually coherent.

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

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

Equations

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

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

instance CompHaus.instPreregularCompHausCategory : CategoryTheory.Preregular CompHaus

Equations

• CompHaus.instPreregularCompHausCategory = (_ : CategoryTheory.Preregular CompHaus)

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

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