Documentation

Mathlib.Topology.Category.CompHaus.Limits

Explicit limits and colimits #

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

So far, we have the following:

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

The pullback of two morphisms f,g in CompHaus, 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 CompHaus.pullback.fst {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X B) (g : Y B) :

    The projection from the pullback to the first component.

    Instances For
      def CompHaus.pullback.snd {X : CompHaus} {Y : CompHaus} {B : CompHaus} (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 CompHaus.pullback.cone_pt {X : CompHaus} {Y : CompHaus} {B : CompHaus} (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
              noncomputable def CompHaus.pullbackIsoPullback {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X B) (g : Y B) :

              The isomorphism from the explicit pullback to the abstract pullback.

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

                The homeomorphism from the explicit pullback to the abstract pullback.

                Instances For
                  theorem CompHaus.pullback_fst_eq {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X B) (g : Y B) :
                  theorem CompHaus.pullback_snd_eq {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X B) (g : Y B) :
                  def CompHaus.finiteCoproduct {α : Type} [Fintype α] (X : αCompHaus) :

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

                  Instances For
                    def CompHaus.finiteCoproduct.ι {α : Type} [Fintype α] (X : αCompHaus) (a : α) :

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

                    Instances For
                      def CompHaus.finiteCoproduct.desc {α : Type} [Fintype α] (X : αCompHaus) {B : CompHaus} (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
                        @[simp]

                        The coproduct cocone associated to the explicit finite coproduct.

                        Instances For

                          The explicit finite coproduct cocone is a colimit cocone.

                          Instances For
                            noncomputable def CompHaus.coproductIsoCoproduct {α : Type} [Fintype α] (X : αCompHaus) :

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

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

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

                              Instances For
                                theorem CompHaus.finiteCoproduct.ι_desc_apply {α : Type} [Fintype α] (X : αCompHaus) {B : CompHaus} {π : (a : α) → X a B} (a : α) (x : (CategoryTheory.forget CompHaus).obj (X a)) :