Effective epimorphic families in Profinite

Let π a : X a ⟶ B be a family of morphisms in Profinite 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.

Main results

• Profinite.effectiveEpiFamily_tfae: characterise being an effective epimorphic family.
• Profinite.instPrecoherent: Profinite is precoherent.

Implementation notes

The entire section EffectiveEpiFamily comprises exclusively a technical construction for the main proof and does not contain any statements that would be useful in other contexts.

This section contains exclusively technical definitions and results that are used in the proof of Profinite.effectiveEpiFamily_of_jointly_surjective.

The construction of QB as a quotient of the maps X a → B is analoguous to the construction in the file CompHaus.EffectiveEpi, but one has to start with an equivalence relation on Profinite instead.

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

Implementation: ιFun is continous.

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

Implementation: ιFun is injective.

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

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

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

Implementation: The function ιFun, considered as a morphism in CompHaus.

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

Implementation: ιFun as isomorphism in CompHaus.

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

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

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

Implementation: The function ιFun, considered as a morphism in Profinite.

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

Implementation: ιFun as an isomorphism in Profinite.

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

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

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

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

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

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

Implementation: ιIso ∘ (π' a) : X a → QB → B is exactly π a.

theorem Profinite.EffectiveEpiFamily.π_comp_ι_inv_assoc {α : Type} [Fintype α] {B : Profinite} {X : α → Profinite} (π : (a : α) → X a ⟶ B) (surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b) (a : α) {Z : Profinite} (h : Profinite.EffectiveEpiFamily.QB π surj ⟶ Z) : CategoryTheory.CategoryStruct.comp (π a) (CategoryTheory.CategoryStruct.comp (Profinite.EffectiveEpiFamily.ιIso π surj).inv h) = CategoryTheory.CategoryStruct.comp (Profinite.EffectiveEpiFamily.π' π surj a) h

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

Implementation: ιIso⁻¹ ∘ (π a) : X a → B → QB is exactly π' a.

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

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

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

One direction of Profinite.effectiveEpiFamily_tfae

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

For a finite family of profinite spaces π a : X a → B the following are equivalent:

• π is an effective epimorphic family
• the map ∐ π a ⟶ B is an epimorphism
• π is jointly surjective

instance Profinite.instPrecoherent : CategoryTheory.Precoherent Profinite

The category of profinite spaces is precoherent