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 #

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

Projects #

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

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

  • One or more equations did not get rendered due to their size.
Instances For
    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) :