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} [Fintype α] {B : CompHaus} {X : α → CompHaus} (π : (a : α) → X a ⟶ B) : Setoid ↑(CompHaus.finiteCoproduct X).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.

def CompHaus.EffectiveEpiFamily.ιFun {α : Type} [Fintype α] {B : CompHaus} {X : α → CompHaus} (π : (a : α) → X a ⟶ B) : Quotient (CompHaus.EffectiveEpiFamily.relation π) → ↑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.

theorem CompHaus.EffectiveEpiFamily.ιFun_continuous {α : Type} [Fintype α] {B : CompHaus} {X : α → CompHaus} (π : (a : α) → X a ⟶ B) : Continuous (CompHaus.EffectiveEpiFamily.ιFun π)

theorem CompHaus.EffectiveEpiFamily.ιFun_injective {α : Type} [Fintype α] {B : CompHaus} {X : α → CompHaus} (π : (a : α) → X a ⟶ B) : Function.Injective (CompHaus.EffectiveEpiFamily.ιFun π)

def CompHaus.EffectiveEpiFamily.QB {α : Type} [Fintype α] {B : CompHaus} {X : α → CompHaus} (π : (a : α) → X a ⟶ B) : CompHaus

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

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

The function ι_fun, considered as a morphism.

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

Implementation: The promised isomorphism between QB and B.

def CompHaus.EffectiveEpiFamily.π' {α : Type} [Fintype α] {B : CompHaus} {X : α → CompHaus} (π : (a : α) → X a ⟶ B) (a : α) : X a ⟶ CompHaus.EffectiveEpiFamily.QB π

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

def CompHaus.EffectiveEpiFamily.structAux {α : Type} [Fintype α] {B : CompHaus} {X : α → CompHaus} (π : (a : α) → X a ⟶ B) : CategoryTheory.EffectiveEpiFamilyStruct X (CompHaus.EffectiveEpiFamily.π' π)

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

theorem CompHaus.EffectiveEpiFamily.π'_comp_ι_hom_assoc {α : Type} [Fintype α] {B : CompHaus} {X : α → CompHaus} (π : (a : α) → X a ⟶ B) (surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b) (a : α) {Z : CompHaus} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CompHaus.EffectiveEpiFamily.π' π a) (CategoryTheory.CategoryStruct.comp (CompHaus.EffectiveEpiFamily.ι (fun a => π a) surj).hom h) = CategoryTheory.CategoryStruct.comp (π a) h

theorem CompHaus.EffectiveEpiFamily.π'_comp_ι_hom {α : Type} [Fintype α] {B : CompHaus} {X : α → CompHaus} (π : (a : α) → X a ⟶ B) (surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b) (a : α) : CategoryTheory.CategoryStruct.comp (CompHaus.EffectiveEpiFamily.π' π a) (CompHaus.EffectiveEpiFamily.ι (fun a => π a) surj).hom = π a

theorem CompHaus.EffectiveEpiFamily.π_comp_ι_inv_assoc {α : Type} [Fintype α] {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) : CategoryTheory.CategoryStruct.comp (π a) (CategoryTheory.CategoryStruct.comp (CompHaus.EffectiveEpiFamily.ι (fun a => π a) surj).inv h) = CategoryTheory.CategoryStruct.comp (CompHaus.EffectiveEpiFamily.π' π a) h

theorem CompHaus.EffectiveEpiFamily.π_comp_ι_inv {α : Type} [Fintype α] {B : CompHaus} {X : α → CompHaus} (π : (a : α) → X a ⟶ B) (surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b) (a : α) : CategoryTheory.CategoryStruct.comp (π a) (CompHaus.EffectiveEpiFamily.ι (fun a => π a) surj).inv = CompHaus.EffectiveEpiFamily.π' π a

noncomputable def CompHaus.EffectiveEpiFamily.struct {α : Type} [Fintype α] {B : CompHaus} {X : α → CompHaus} (π : (a : α) → X a ⟶ B) (surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b) : CategoryTheory.EffectiveEpiFamilyStruct X π

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

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

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

instance CompHaus.precoherent : CategoryTheory.Precoherent CompHaus