Documentation

Mathlib.Topology.Category.Profinite.Limits

Explicit limits and colimits #

This file collects some constructions of explicit limits and colimits in Profinite, which may be useful due to their definitional properties.

Main definitions #

def Profinite.pullback {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) :

The pullback of two morphisms f, g in Profinite, constructed explicitly as the set of pairs (x, y) such that f x = g y, with the topology induced by the product.

Instances For
    def Profinite.pullback.fst {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) :

    The projection from the pullback to the first component.

    Instances For
      def Profinite.pullback.snd {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) :

      The projection from the pullback to the second component.

      Instances For

        Construct a morphism to the explicit pullback given morphisms to the factors which are compatible with the maps to the base. This is essentially the universal property of the pullback.

        Instances For
          @[simp]
          theorem Profinite.pullback.cone_pt {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) :

          The pullback cone whose cone point is the explicit pullback.

          Instances For

            The explicit pullback cone is a limit cone.

            Instances For

              The isomorphism from the explicit pullback to the abstract pullback.

              Instances For
                noncomputable def Profinite.pullbackHomeoPullback {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) :
                (Profinite.pullback f g).toCompHaus.toTop ≃ₜ (CategoryTheory.Limits.pullback f g).toCompHaus.toTop

                The homeomorphism from the explicit pullback to the abstract pullback.

                Instances For
                  theorem Profinite.pullback_fst_eq {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) :
                  theorem Profinite.pullback_snd_eq {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) :

                  The coproduct of a finite family of objects in Profinite, constructed as the disjoint union with its usual topology.

                  Instances For

                    The inclusion of one of the factors into the explicit finite coproduct.

                    Instances For
                      def Profinite.finiteCoproduct.desc {α : Type} [Fintype α] (X : αProfinite) {B : Profinite} (e : (a : α) → X a B) :

                      To construct a morphism from the explicit finite coproduct, it suffices to specify a morphism from each of its factors. This is essentially the universal property of the coproduct.

                      Instances For

                        The coproduct cocone associated to the explicit finite coproduct.

                        Instances For

                          The explicit finite coproduct cocone is a colimit cocone.

                          Instances For

                            The isomorphism from the explicit finite coproducts to the abstract coproduct.

                            Instances For
                              noncomputable def Profinite.coproductHomeoCoproduct {α : Type} [Fintype α] (X : αProfinite) :
                              (Profinite.finiteCoproduct X).toCompHaus.toTop ≃ₜ ( X).toCompHaus.toTop

                              The homeomorphism from the explicit finite coproducts to the abstract coproduct.

                              Instances For
                                theorem Profinite.finiteCoproduct.ι_jointly_surjective {α : Type} [Fintype α] (X : αProfinite) (R : (Profinite.finiteCoproduct X).toCompHaus.toTop) :
                                a r, R = ↑(Profinite.finiteCoproduct.ι X a) r
                                theorem Profinite.finiteCoproduct.ι_desc_apply {α : Type} [Fintype α] (X : αProfinite) {B : Profinite} {π : (a : α) → X a B} (a : α) (x : (CategoryTheory.forget Profinite).obj (X a)) :