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 : ι) :
of ((i : ι) → (α i)) α i

The projection from the product as a bundled continuous map.

Equations
Instances For
    def TopCat.piFan {ι : Type v} (α : ιTopCat) :

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

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

      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) :
        ∏ᶜ α of ((i : ι) → (α i))

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

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

          The inclusion to the coproduct as a bundled continuous map.

          Equations
          Instances For

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

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

              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) :
                α of ((i : ι) × (α i))

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

                Equations
                Instances For
                  @[reducible, inline]
                  abbrev TopCat.prodFst {X Y : TopCat} :
                  of (X × Y) X

                  The first projection from the product.

                  Equations
                  Instances For
                    @[reducible, inline]
                    abbrev TopCat.prodSnd {X Y : TopCat} :
                    of (X × Y) Y

                    The second projection from the product.

                    Equations
                    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 Y : TopCat) :
                          X Y 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

                            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