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.

Equations
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.

    Equations
    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.

      Equations
      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.

        Equations
        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.

          Equations
          Instances For
            @[simp]
            theorem Profinite.pullback.isLimit_lift {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) (s : CategoryTheory.Limits.PullbackCone f g) :
            (Profinite.pullback.isLimit f g).lift s = Profinite.pullback.lift f g s.fst s.snd

            The explicit pullback cone is a limit cone.

            Equations
            Instances For

              The isomorphism from the explicit pullback to the abstract pullback.

              Equations
              Instances For
                noncomputable def Profinite.pullbackHomeoPullback {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) :

                The homeomorphism from the explicit pullback to the abstract pullback.

                Equations
                Instances For
                  def Profinite.finiteCoproduct {α : Type w} [Finite α] (X : αProfinite) :

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

                  Equations
                  Instances For
                    def Profinite.finiteCoproduct.ι {α : Type w} [Finite α] (X : αProfinite) (a : α) :

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

                    Equations
                    Instances For
                      def Profinite.finiteCoproduct.desc {α : Type w} [Finite α] (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.

                      Equations
                      Instances For
                        @[simp]
                        @[reducible, inline]

                        The coproduct cocone associated to the explicit finite coproduct.

                        Equations
                        Instances For

                          The explicit finite coproduct cocone is a colimit cocone.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            noncomputable def Profinite.coproductIsoCoproduct {α : Type w} [Finite α] (X : αProfinite) :

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

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

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

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