Documentation

Mathlib.Topology.Category.TopCat.Limits.Products

Products and coproducts in the category of topological spaces #

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

The projection from the product as a bundled continuous map.

Instances For
    source
    def TopCat.piFan {ι : Type v} (α : ι → TopCat) :
    CategoryTheory.Limits.Fan α

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

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

      The constructed fan is indeed a limit

      Instances For
        source
        noncomputable 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.

        Instances For
          source
          @[simp]
          theorem TopCat.piIsoPi_inv_π {ι : Type v} (α : ι → TopCat) (i : ι) :
          CategoryTheory.CategoryStruct.comp (piIsoPi α).inv (CategoryTheory.Limits.Pi.π α i) = piπ α i
          source
          @[simp]
          theorem TopCat.piIsoPi_inv_π_assoc {ι : Type v} (α : ι → TopCat) (i : ι) {Z : TopCat} (h : α i ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (piIsoPi α).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π α i) h) = CategoryTheory.CategoryStruct.comp (piπ α i) h
          source
          theorem TopCat.piIsoPi_inv_π_apply {ι : Type v} (α : ι → TopCat) (i : ι) (x : (i : ι) → ↑(α i)) :
          (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π α i)) ((CategoryTheory.ConcreteCategory.hom (piIsoPi α).inv) x) = x i
          source
          theorem TopCat.piIsoPi_hom_apply {ι : Type v} (α : ι → TopCat) (i : ι) (x : ↑(∏ᶜ α)) :
          (CategoryTheory.ConcreteCategory.hom (piIsoPi α).hom) x i = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π α i)) x
          source
          @[reducible, inline]
          abbrev TopCat.sigmaι {ι : Type v} (α : ι → TopCat) (i : ι) :
          α i ⟶ of ((i : ι) × ↑(α i))

          The inclusion to the coproduct as a bundled continuous map.

          Instances For
            source
            def TopCat.sigmaCofan {ι : Type v} (α : ι → TopCat) :
            CategoryTheory.Limits.Cofan α

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

            Instances For
              source
              @[simp]
              theorem TopCat.sigmaCofan_pt {ι : Type v} (α : ι → TopCat) :
              (sigmaCofan α).pt = of ((i : ι) × ↑(α i))
              source
              @[simp]
              theorem TopCat.sigmaCofan_ι_app {ι : Type v} (α : ι → TopCat) (X : CategoryTheory.Discrete ι) :
              (sigmaCofan α).ι.app X = sigmaι α X.as
              source
              def TopCat.sigmaCofanIsColimit {ι : Type v} (β : ι → TopCat) :
              CategoryTheory.Limits.IsColimit (sigmaCofan β)

              The constructed cofan is indeed a colimit

              Instances For
                source
                noncomputable def TopCat.sigmaIsoSigma {ι : Type v} (α : ι → TopCat) :
                ∐ α ≅ of ((i : ι) × ↑(α i))

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

                Instances For
                  source
                  @[simp]
                  theorem TopCat.sigmaIsoSigma_hom_ι {ι : Type v} (α : ι → TopCat) (i : ι) :
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι α i) (sigmaIsoSigma α).hom = sigmaι α i
                  source
                  @[simp]
                  theorem TopCat.sigmaIsoSigma_hom_ι_assoc {ι : Type v} (α : ι → TopCat) (i : ι) {Z : TopCat} (h : of ((i : ι) × ↑(α i)) ⟶ Z) :
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι α i) (CategoryTheory.CategoryStruct.comp (sigmaIsoSigma α).hom h) = CategoryTheory.CategoryStruct.comp (sigmaι α i) h
                  source
                  theorem TopCat.sigmaIsoSigma_hom_ι_apply {ι : Type v} (α : ι → TopCat) (i : ι) (x : ↑(α i)) :
                  (CategoryTheory.ConcreteCategory.hom (sigmaIsoSigma α).hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Sigma.ι α i)) x) = ⟨i, x⟩
                  source
                  theorem TopCat.sigmaIsoSigma_inv_apply {ι : Type v} (α : ι → TopCat) (i : ι) (x : ↑(α i)) :
                  (CategoryTheory.ConcreteCategory.hom (sigmaIsoSigma α).inv) ⟨i, x⟩ = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Sigma.ι α i)) x
                  source
                  @[reducible, inline]
                  abbrev TopCat.prodFst {X Y : TopCat} :
                  of (↑X × ↑Y) ⟶ X

                  The first projection from the product.

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

                    The second projection from the product.

                    Instances For
                      source
                      def TopCat.prodBinaryFan (X Y : TopCat) :
                      CategoryTheory.Limits.BinaryFan X Y

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

                      Instances For
                        source
                        def TopCat.prodBinaryFanIsLimit (X Y : TopCat) :
                        CategoryTheory.Limits.IsLimit (X.prodBinaryFan Y)

                        The constructed binary fan is indeed a limit

                        Instances For
                          source
                          noncomputable 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.

                          Instances For
                            source
                            @[simp]
                            theorem TopCat.prodIsoProd_hom_fst (X Y : TopCat) :
                            CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).hom prodFst = CategoryTheory.Limits.prod.fst
                            source
                            @[simp]
                            theorem TopCat.prodIsoProd_hom_fst_assoc (X Y : TopCat) {Z : TopCat} (h : X ⟶ Z) :
                            CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).hom (CategoryTheory.CategoryStruct.comp prodFst h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h
                            source
                            @[simp]
                            theorem TopCat.prodIsoProd_hom_snd (X Y : TopCat) :
                            CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).hom prodSnd = CategoryTheory.Limits.prod.snd
                            source
                            @[simp]
                            theorem TopCat.prodIsoProd_hom_snd_assoc (X Y : TopCat) {Z : TopCat} (h : Y ⟶ Z) :
                            CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).hom (CategoryTheory.CategoryStruct.comp prodSnd h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h
                            source
                            theorem TopCat.prodIsoProd_hom_apply {X Y : TopCat} (x : ↑(X ⨯ Y)) :
                            (CategoryTheory.ConcreteCategory.hom (X.prodIsoProd Y).hom) x = ((CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.fst) x, (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.snd) x)
                            source
                            @[simp]
                            theorem TopCat.prodIsoProd_inv_fst (X Y : TopCat) :
                            CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).inv CategoryTheory.Limits.prod.fst = prodFst
                            source
                            @[simp]
                            theorem TopCat.prodIsoProd_inv_fst_assoc (X 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 prodFst h
                            source
                            theorem TopCat.prodIsoProd_inv_fst_apply (X Y : TopCat) (x : ↑X × ↑Y) :
                            (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.fst) ((CategoryTheory.ConcreteCategory.hom (X.prodIsoProd Y).inv) x) = x.1
                            source
                            @[simp]
                            theorem TopCat.prodIsoProd_inv_snd (X Y : TopCat) :
                            CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).inv CategoryTheory.Limits.prod.snd = prodSnd
                            source
                            @[simp]
                            theorem TopCat.prodIsoProd_inv_snd_assoc (X 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 prodSnd h
                            source
                            theorem TopCat.prodIsoProd_inv_snd_apply (X Y : TopCat) (x : ↑X × ↑Y) :
                            (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.snd) ((CategoryTheory.ConcreteCategory.hom (X.prodIsoProd Y).inv) x) = x.2
                            source
                            theorem TopCat.prod_topology {X Y : TopCat} :
                            (X ⨯ Y).str = TopologicalSpace.induced (⇑(CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.fst)) X.str ⊓ TopologicalSpace.induced (⇑(CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.snd)) Y.str
                            source
                            theorem TopCat.range_prod_map {W X Y Z : TopCat} (f : W ⟶ Y) (g : X ⟶ Z) :
                            Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.map f g)) = ⇑(CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.fst) ⁻¹' Set.range ⇑(CategoryTheory.ConcreteCategory.hom f) ∩ ⇑(CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.snd) ⁻¹' Set.range ⇑(CategoryTheory.ConcreteCategory.hom g)
                            source
                            theorem TopCat.isInducing_prodMap {W X Y Z : TopCat} {f : W ⟶ X} {g : Y ⟶ Z} (hf : Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f)) (hg : Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom g)) :
                            Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.map f g))
                            source
                            theorem TopCat.isEmbedding_prodMap {W X Y Z : TopCat} {f : W ⟶ X} {g : Y ⟶ Z} (hf : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (hg : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom g)) :
                            Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.map f g))
                            source
                            def TopCat.binaryCofan (X Y : TopCat) :
                            CategoryTheory.Limits.BinaryCofan X Y

                            The binary coproduct cofan in TopCat.

                            Instances For
                              source
                              def TopCat.binaryCofanIsColimit (X Y : TopCat) :
                              CategoryTheory.Limits.IsColimit (X.binaryCofan Y)

                              The constructed binary coproduct cofan in TopCat is the coproduct.

                              Instances For
                                source
                                theorem TopCat.binaryCofan_isColimit_iff {X Y : TopCat} (c : CategoryTheory.Limits.BinaryCofan X Y) :
                                Nonempty (CategoryTheory.Limits.IsColimit c) ↔ Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom c.inl) ∧ Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom c.inr) ∧ IsCompl (Set.range ⇑(CategoryTheory.ConcreteCategory.hom c.inl)) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom c.inr))