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:

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

Projects #

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

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

    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
      def CompHaus.EffectiveEpiFamily.QB {α : Type} [Fintype α] {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} [Fintype α] {B : CompHaus} {X : αCompHaus} (π : (a : α) → X a B) :

        The function ι_fun, considered as a morphism.

        Instances For
          noncomputable def CompHaus.EffectiveEpiFamily.ι {α : Type} [Fintype α] {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} [Fintype α] {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

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

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