# Documentation

Mathlib.Topology.Category.CompHaus.EffectiveEpi

# Effective epimorphic families in CompHaus#

Let π a : X a ⟶ B be a family of morphisms in CompHaus indexed by a finite type α. In this file, we show that the following are all equivalent:

• The family π is effective epimorphic.
• The induced map ∐ X ⟶ B is epimorphic.
• The family π is jointly surjective. This is the main result of this file, which can be found in CompHaus.effectiveEpiFamily_tfae

As a consequence, we also show that CompHaus is precoherent.

# Projects #

• Define regular categories, and show that CompHaus is regular.
• Define coherent categories, and show that CompHaus is actually coherent.
def CompHaus.EffectiveEpiFamily.relation {α : Type} [] {B : CompHaus} {X : αCompHaus} (π : (a : α) → X a B) :
Setoid ().toTop

Implementation: This is a setoid on the explicit finite coproduct of X whose quotient will be isomorphic to B provided that X a → B is an effective epi family.

Instances For
def CompHaus.EffectiveEpiFamily.ιFun {α : Type} [] {B : CompHaus} {X : αCompHaus} (π : (a : α) → X a B) :
B.toTop

Implementation: the map from the quotient of relation π to B, which will eventually become the function underlying an isomorphism, provided that X a → B is an effective epi family.

Instances For
theorem CompHaus.EffectiveEpiFamily.ιFun_continuous {α : Type} [] {B : CompHaus} {X : αCompHaus} (π : (a : α) → X a B) :
theorem CompHaus.EffectiveEpiFamily.ιFun_injective {α : Type} [] {B : CompHaus} {X : αCompHaus} (π : (a : α) → X a B) :
def CompHaus.EffectiveEpiFamily.QB {α : Type} [] {B : CompHaus} {X : αCompHaus} (π : (a : α) → X a B) :

Implementation: The quotient of relation π, considered as an object of CompHaus.

Instances For
def CompHaus.EffectiveEpiFamily.ιHom {α : Type} [] {B : CompHaus} {X : αCompHaus} (π : (a : α) → X a B) :

The function ι_fun, considered as a morphism.

Instances For
noncomputable def CompHaus.EffectiveEpiFamily.ι {α : Type} [] {B : CompHaus} {X : αCompHaus} (π : (a : α) → X a B) (surj : ∀ (b : B.toTop), a x, ↑(π a) x = b) :

Implementation: The promised isomorphism between QB and B.

Instances For
def CompHaus.EffectiveEpiFamily.π' {α : Type} [] {B : CompHaus} {X : αCompHaus} (π : (a : α) → X a B) (a : α) :

Implementation: The family of morphisms X a ⟶ QB which will be shown to be effective epi.

Instances For
def CompHaus.EffectiveEpiFamily.structAux {α : Type} [] {B : CompHaus} {X : αCompHaus} (π : (a : α) → X a B) :

Implementation: The family of morphisms X a ⟶ QB is an effective epi.

Instances For
theorem CompHaus.EffectiveEpiFamily.π'_comp_ι_hom_assoc {α : Type} [] {B : CompHaus} {X : αCompHaus} (π : (a : α) → X a B) (surj : ∀ (b : B.toTop), a x, ↑(π a) x = b) (a : α) {Z : CompHaus} (h : B Z) :
theorem CompHaus.EffectiveEpiFamily.π'_comp_ι_hom {α : Type} [] {B : CompHaus} {X : αCompHaus} (π : (a : α) → X a B) (surj : ∀ (b : B.toTop), a x, ↑(π a) x = b) (a : α) :
theorem CompHaus.EffectiveEpiFamily.π_comp_ι_inv_assoc {α : Type} [] {B : CompHaus} {X : αCompHaus} (π : (a : α) → X a B) (surj : ∀ (b : B.toTop), a x, ↑(π a) x = b) (a : α) {Z : CompHaus} (h : (CompHaus.EffectiveEpiFamily.QB fun a => π a) Z) :
theorem CompHaus.EffectiveEpiFamily.π_comp_ι_inv {α : Type} [] {B : CompHaus} {X : αCompHaus} (π : (a : α) → X a B) (surj : ∀ (b : B.toTop), a x, ↑(π a) x = b) (a : α) :
noncomputable def CompHaus.EffectiveEpiFamily.struct {α : Type} [] {B : CompHaus} {X : αCompHaus} (π : (a : α) → X a B) (surj : ∀ (b : B.toTop), a x, ↑(π a) x = b) :

Implementation: The family X is an effective epi, provided that π are jointly surjective. The theorem CompHaus.effectiveEpiFamily_tfae should be used instead.

Instances For
theorem CompHaus.effectiveEpiFamily_of_jointly_surjective {α : Type} [] {B : CompHaus} (X : αCompHaus) (π : (a : α) → X a B) (surj : ∀ (b : B.toTop), a x, ↑(π a) x = b) :
theorem CompHaus.effectiveEpiFamily_tfae {α : Type} [] {B : CompHaus} (X : αCompHaus) (π : (a : α) → X a B) :
List.TFAE [, , ∀ (b : B.toTop), a x, ↑(π a) x = b]