Effective epimorphisms in CompHaus

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

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

Projects

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

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

instance CompHaus.instPreregular : CategoryTheory.Preregular CompHaus

theorem CompHaus.effectiveEpiFamily_tfae {α : Type} [Finite α] {B : CompHaus} (X : α → CompHaus) (π : (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 CompHaus.effectiveEpiFamily_of_jointly_surjective {α : Type} [Finite α] {B : CompHaus} (X : α → CompHaus) (π : (a : α) → X a ⟶ B) (surj : ∀ (b : ↑B.toTop), ∃ (a : α) (x : ↑(X a).toTop), (CategoryTheory.ConcreteCategory.hom (π a)) x = b) : CategoryTheory.EffectiveEpiFamily X π