# Documentation

Mathlib.Topology.Category.Profinite.EffectiveEpi

# 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} [] {B : Profinite} {X : } (π : (a : α) → X a B) :
Setoid ().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.

Instances For
def Profinite.EffectiveEpiFamily.ιFun {α : Type} [] {B : Profinite} {X : } (π : (a : α) → X a B) :
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.

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

Implementation: ιFun is continous.

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

Implementation: ιFun is injective.

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

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

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

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

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

Implementation: ιFun as isomorphism in CompHaus.

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

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

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

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

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

Implementation: ιFun as an isomorphism in Profinite.

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

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

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

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

Instances For
theorem Profinite.EffectiveEpiFamily.π'_comp_ι_hom_assoc {α : Type} [] {B : Profinite} {X : } (π : (a : α) → X a B) (surj : ∀ (b : B.toCompHaus.toTop), a x, ↑(π a) x = b) (a : α) {Z : Profinite} (h : B Z) :
theorem Profinite.EffectiveEpiFamily.π'_comp_ι_hom {α : Type} [] {B : Profinite} {X : } (π : (a : α) → X a B) (surj : ∀ (b : B.toCompHaus.toTop), a x, ↑(π a) x = b) (a : α) :
= π a

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

theorem Profinite.EffectiveEpiFamily.π_comp_ι_inv_assoc {α : Type} [] {B : Profinite} {X : } (π : (a : α) → X a B) (surj : ∀ (b : B.toCompHaus.toTop), a x, ↑(π a) x = b) (a : α) {Z : Profinite} (h : Z) :
theorem Profinite.EffectiveEpiFamily.π_comp_ι_inv {α : Type} [] {B : Profinite} {X : } (π : (a : α) → X a B) (surj : ∀ (b : B.toCompHaus.toTop), a x, ↑(π a) x = b) (a : α) :

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

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

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

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

One direction of Profinite.effectiveEpiFamily_tfae

theorem Profinite.effectiveEpiFamily_tfae {α : Type} [] {B : Profinite} (X : ) (π : (a : α) → X a B) :
List.TFAE [, , ∀ (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

The category of profinite spaces is precoherent