Documentation

Mathlib.Topology.Category.TopCat.Limits.Products

Products and coproducts in the category of topological spaces #

@[reducible, inline]
abbrev TopCat.piπ {ι : Type v} (α : ιTopCat) (i : ι) :
TopCat.of ((i : ι) → (α i)) α i

The projection from the product as a bundled continuous map.

Equations
  • TopCat.piπ α i = { toFun := fun (f : (TopCat.of ((i : ι) → (α i)))) => f i, continuous_toFun := }
Instances For
    @[simp]
    theorem TopCat.piFan_pt {ι : Type v} (α : ιTopCat) :
    (TopCat.piFan α).pt = TopCat.of ((i : ι) → (α i))
    @[simp]
    theorem TopCat.piFan_π_app {ι : Type v} (α : ιTopCat) (X : CategoryTheory.Discrete ι) :
    (TopCat.piFan α).app X = TopCat.piπ α X.as
    def TopCat.piFan {ι : Type v} (α : ιTopCat) :

    The explicit fan of a family of topological spaces given by the pi type.

    Equations
    Instances For

      The constructed fan is indeed a limit

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def TopCat.piIsoPi {ι : Type v} (α : ιTopCat) :
        α TopCat.of ((i : ι) → (α i))

        The product is homeomorphic to the product of the underlying spaces, equipped with the product topology.

        Equations
        Instances For
          @[simp]
          theorem TopCat.piIsoPi_inv_π_apply {ι : Type v} (α : ιTopCat) (i : ι) (x : (i : ι) → (α i)) :
          @[simp]
          theorem TopCat.piIsoPi_hom_apply {ι : Type v} (α : ιTopCat) (i : ι) (x : ( α)) :
          @[reducible, inline]
          abbrev TopCat.sigmaι {ι : Type v} (α : ιTopCat) (i : ι) :
          α i TopCat.of ((i : ι) × (α i))

          The inclusion to the coproduct as a bundled continuous map.

          Equations
          Instances For
            @[simp]
            theorem TopCat.sigmaCofan_pt {ι : Type v} (α : ιTopCat) :
            (TopCat.sigmaCofan α).pt = TopCat.of ((i : ι) × (α i))
            @[simp]
            theorem TopCat.sigmaCofan_ι_app {ι : Type v} (α : ιTopCat) (X : CategoryTheory.Discrete ι) :
            (TopCat.sigmaCofan α).app X = TopCat.sigmaι α X.as

            The explicit cofan of a family of topological spaces given by the sigma type.

            Equations
            Instances For

              The constructed cofan is indeed a colimit

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def TopCat.sigmaIsoSigma {ι : Type v} (α : ιTopCat) :
                α TopCat.of ((i : ι) × (α i))

                The coproduct is homeomorphic to the disjoint union of the topological spaces.

                Equations
                Instances For
                  @[simp]
                  theorem TopCat.sigmaIsoSigma_hom_ι_apply {ι : Type v} (α : ιTopCat) (i : ι) (x : (α i)) :
                  @[simp]
                  theorem TopCat.sigmaIsoSigma_inv_apply {ι : Type v} (α : ιTopCat) (i : ι) (x : (α i)) :
                  @[reducible, inline]
                  abbrev TopCat.prodFst {X : TopCat} {Y : TopCat} :
                  TopCat.of (X × Y) X

                  The first projection from the product.

                  Equations
                  • TopCat.prodFst = { toFun := Prod.fst, continuous_toFun := }
                  Instances For
                    @[reducible, inline]
                    abbrev TopCat.prodSnd {X : TopCat} {Y : TopCat} :
                    TopCat.of (X × Y) Y

                    The second projection from the product.

                    Equations
                    • TopCat.prodSnd = { toFun := Prod.snd, continuous_toFun := }
                    Instances For

                      The explicit binary cofan of X, Y given by X × Y.

                      Equations
                      Instances For

                        The constructed binary fan is indeed a limit

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          def TopCat.prodIsoProd (X : TopCat) (Y : TopCat) :
                          X Y TopCat.of (X × Y)

                          The homeomorphism between X ⨯ Y and the set-theoretic product of X and Y, equipped with the product topology.

                          Equations
                          Instances For
                            @[simp]
                            theorem TopCat.prodIsoProd_hom_fst_assoc (X : TopCat) (Y : TopCat) {Z : TopCat} (h : X Z) :
                            CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).hom (CategoryTheory.CategoryStruct.comp TopCat.prodFst h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h
                            @[simp]
                            theorem TopCat.prodIsoProd_hom_fst (X : TopCat) (Y : TopCat) :
                            CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).hom TopCat.prodFst = CategoryTheory.Limits.prod.fst
                            @[simp]
                            theorem TopCat.prodIsoProd_hom_snd_assoc (X : TopCat) (Y : TopCat) {Z : TopCat} (h : Y Z) :
                            CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).hom (CategoryTheory.CategoryStruct.comp TopCat.prodSnd h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h
                            @[simp]
                            theorem TopCat.prodIsoProd_hom_snd (X : TopCat) (Y : TopCat) :
                            CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).hom TopCat.prodSnd = CategoryTheory.Limits.prod.snd
                            @[simp]
                            theorem TopCat.prodIsoProd_hom_apply {X : TopCat} {Y : TopCat} (x : (X Y)) :
                            (X.prodIsoProd Y).hom x = (CategoryTheory.Limits.prod.fst x, CategoryTheory.Limits.prod.snd x)
                            @[simp]
                            theorem TopCat.prodIsoProd_inv_fst_assoc (X : TopCat) (Y : TopCat) {Z : TopCat} (h : X Z) :
                            CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) = CategoryTheory.CategoryStruct.comp TopCat.prodFst h
                            theorem TopCat.prodIsoProd_inv_fst_apply (X : TopCat) (Y : TopCat) (x : (CategoryTheory.forget TopCat).obj (TopCat.of (X × Y))) :
                            CategoryTheory.Limits.prod.fst ((X.prodIsoProd Y).inv x) = TopCat.prodFst x
                            @[simp]
                            theorem TopCat.prodIsoProd_inv_fst (X : TopCat) (Y : TopCat) :
                            CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).inv CategoryTheory.Limits.prod.fst = TopCat.prodFst
                            @[simp]
                            theorem TopCat.prodIsoProd_inv_snd_assoc (X : TopCat) (Y : TopCat) {Z : TopCat} (h : Y Z) :
                            CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h) = CategoryTheory.CategoryStruct.comp TopCat.prodSnd h
                            theorem TopCat.prodIsoProd_inv_snd_apply (X : TopCat) (Y : TopCat) (x : (CategoryTheory.forget TopCat).obj (TopCat.of (X × Y))) :
                            CategoryTheory.Limits.prod.snd ((X.prodIsoProd Y).inv x) = TopCat.prodSnd x
                            @[simp]
                            theorem TopCat.prodIsoProd_inv_snd (X : TopCat) (Y : TopCat) :
                            CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).inv CategoryTheory.Limits.prod.snd = TopCat.prodSnd
                            theorem TopCat.prod_topology {X : TopCat} {Y : TopCat} :
                            (X Y).str = TopologicalSpace.induced (CategoryTheory.Limits.prod.fst) X.str TopologicalSpace.induced (CategoryTheory.Limits.prod.snd) Y.str
                            theorem TopCat.range_prod_map {W : TopCat} {X : TopCat} {Y : TopCat} {Z : TopCat} (f : W Y) (g : X Z) :
                            Set.range (CategoryTheory.Limits.prod.map f g) = CategoryTheory.Limits.prod.fst ⁻¹' Set.range f CategoryTheory.Limits.prod.snd ⁻¹' Set.range g
                            theorem TopCat.inducing_prod_map {W : TopCat} {X : TopCat} {Y : TopCat} {Z : TopCat} {f : W X} {g : Y Z} (hf : Inducing f) (hg : Inducing g) :
                            theorem TopCat.embedding_prod_map {W : TopCat} {X : TopCat} {Y : TopCat} {Z : TopCat} {f : W X} {g : Y Z} (hf : Embedding f) (hg : Embedding g) :

                            The binary coproduct cofan in TopCat.

                            Equations
                            Instances For

                              The constructed binary coproduct cofan in TopCat is the coproduct.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For