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:

Main results #

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.

Instances For
    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.

    Instances For

      Implementation: ιFun is continous.

      Implementation: ιFun is injective.

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

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

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

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

        Instances For
          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) :

          Implementation: ιFun as isomorphism in CompHaus.

          Instances For
            def Profinite.EffectiveEpiFamily.QB {α : Type} [Fintype α] {B : Profinite} {X : αProfinite} (π : (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} [Fintype α] {B : Profinite} {X : αProfinite} (π : (a : α) → X a B) (surj : ∀ (b : B.toCompHaus.toTop), a x, ↑(π a) x = b) :

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

              Instances For
                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) :

                Implementation: ιFun as an isomorphism in Profinite.

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

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

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

                      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) :
                      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 : α) :

                      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) :

                      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} [Fintype α] {B : Profinite} (X : αProfinite) (π : (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} [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

                        The category of profinite spaces is precoherent