Documentation

Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Pullbacks and pushouts in the category of topological spaces #

source
๐Ÿ”ธ coverage
@[reducible, inline]
abbrev TopCat.pullbackFst {X Y Z : TopCat} (f : X โŸถ Z) (g : Y โŸถ Z) :
{ carrier := { p : โ†‘X ร— โ†‘Y // (CategoryTheory.ConcreteCategory.hom f) p.1 = (CategoryTheory.ConcreteCategory.hom g) p.2 }, str := instTopologicalSpaceSubtype } โŸถ X

The first projection from the pullback.

Equations
    Instances For
      source
      ๐Ÿ“ coverage
      theorem TopCat.pullbackFst_apply {X Y Z : TopCat} (f : X โŸถ Z) (g : Y โŸถ Z) (x : โ†‘{ carrier := { p : โ†‘X ร— โ†‘Y // (CategoryTheory.ConcreteCategory.hom f) p.1 = (CategoryTheory.ConcreteCategory.hom g) p.2 }, str := instTopologicalSpaceSubtype }) :
      (CategoryTheory.ConcreteCategory.hom (pullbackFst f g)) x = (โ†‘x).1
      source
      ๐Ÿ”ธ coverage
      @[reducible, inline]
      abbrev TopCat.pullbackSnd {X Y Z : TopCat} (f : X โŸถ Z) (g : Y โŸถ Z) :
      { carrier := { p : โ†‘X ร— โ†‘Y // (CategoryTheory.ConcreteCategory.hom f) p.1 = (CategoryTheory.ConcreteCategory.hom g) p.2 }, str := instTopologicalSpaceSubtype } โŸถ Y

      The second projection from the pullback.

      Equations
        Instances For
          source
          ๐Ÿ“ coverage
          theorem TopCat.pullbackSnd_apply {X Y Z : TopCat} (f : X โŸถ Z) (g : Y โŸถ Z) (x : โ†‘{ carrier := { p : โ†‘X ร— โ†‘Y // (CategoryTheory.ConcreteCategory.hom f) p.1 = (CategoryTheory.ConcreteCategory.hom g) p.2 }, str := instTopologicalSpaceSubtype }) :
          (CategoryTheory.ConcreteCategory.hom (pullbackSnd f g)) x = (โ†‘x).2
          source
          ๐Ÿ”ธ coverage
          def TopCat.pullbackCone {X Y Z : TopCat} (f : X โŸถ Z) (g : Y โŸถ Z) :
          CategoryTheory.Limits.PullbackCone f g

          The explicit pullback cone of X, Y given by { p : X ร— Y // f p.1 = g p.2 }.

          Equations
            Instances For
              source
              ๐Ÿ”ธ coverage
              def TopCat.pullbackConeIsLimit {X Y Z : TopCat} (f : X โŸถ Z) (g : Y โŸถ Z) :
              CategoryTheory.Limits.IsLimit (pullbackCone f g)

              The constructed cone is a limit.

              Equations
                Instances For
                  source
                  ๐Ÿ”ธ coverage
                  def TopCat.pullbackIsoProdSubtype {X Y Z : TopCat} (f : X โŸถ Z) (g : Y โŸถ Z) :
                  CategoryTheory.Limits.pullback f g โ‰… { carrier := { p : โ†‘X ร— โ†‘Y // (CategoryTheory.ConcreteCategory.hom f) p.1 = (CategoryTheory.ConcreteCategory.hom g) p.2 }, str := instTopologicalSpaceSubtype }

                  The pullback of two maps can be identified as a subspace of X ร— Y.

                  Equations
                    Instances For
                      source
                      ๐Ÿ“ coverage
                      @[simp]
                      theorem TopCat.pullbackIsoProdSubtype_inv_fst {X Y Z : TopCat} (f : X โŸถ Z) (g : Y โŸถ Z) :
                      CategoryTheory.CategoryStruct.comp (pullbackIsoProdSubtype f g).inv (CategoryTheory.Limits.pullback.fst f g) = pullbackFst f g
                      source
                      ๐Ÿ“ coverage
                      @[simp]
                      theorem TopCat.pullbackIsoProdSubtype_inv_fst_assoc {X Y Z : TopCat} (f : X โŸถ Z) (g : Y โŸถ Z) {Zโœ : TopCat} (h : X โŸถ Zโœ) :
                      CategoryTheory.CategoryStruct.comp (pullbackIsoProdSubtype f g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h) = CategoryTheory.CategoryStruct.comp (pullbackFst f g) h
                      source
                      ๐Ÿ“ coverage
                      theorem TopCat.pullbackIsoProdSubtype_inv_fst_apply {X Y Z : TopCat} (f : X โŸถ Z) (g : Y โŸถ Z) (x : { p : โ†‘X ร— โ†‘Y // (CategoryTheory.ConcreteCategory.hom f) p.1 = (CategoryTheory.ConcreteCategory.hom g) p.2 }) :
                      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g)) ((CategoryTheory.ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) x) = (โ†‘x).1
                      source
                      ๐Ÿ“ coverage
                      @[simp]
                      theorem TopCat.pullbackIsoProdSubtype_inv_snd {X Y Z : TopCat} (f : X โŸถ Z) (g : Y โŸถ Z) :
                      CategoryTheory.CategoryStruct.comp (pullbackIsoProdSubtype f g).inv (CategoryTheory.Limits.pullback.snd f g) = pullbackSnd f g
                      source
                      ๐Ÿ“ coverage
                      @[simp]
                      theorem TopCat.pullbackIsoProdSubtype_inv_snd_assoc {X Y Z : TopCat} (f : X โŸถ Z) (g : Y โŸถ Z) {Zโœ : TopCat} (h : Y โŸถ Zโœ) :
                      CategoryTheory.CategoryStruct.comp (pullbackIsoProdSubtype f g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h) = CategoryTheory.CategoryStruct.comp (pullbackSnd f g) h
                      source
                      ๐Ÿ“ coverage
                      theorem TopCat.pullbackIsoProdSubtype_inv_snd_apply {X Y Z : TopCat} (f : X โŸถ Z) (g : Y โŸถ Z) (x : { p : โ†‘X ร— โ†‘Y // (CategoryTheory.ConcreteCategory.hom f) p.1 = (CategoryTheory.ConcreteCategory.hom g) p.2 }) :
                      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g)) ((CategoryTheory.ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) x) = (โ†‘x).2
                      source
                      ๐Ÿ“ coverage
                      theorem TopCat.pullbackIsoProdSubtype_hom_fst {X Y Z : TopCat} (f : X โŸถ Z) (g : Y โŸถ Z) :
                      CategoryTheory.CategoryStruct.comp (pullbackIsoProdSubtype f g).hom (pullbackFst f g) = CategoryTheory.Limits.pullback.fst f g
                      source
                      ๐Ÿ“ coverage
                      theorem TopCat.pullbackIsoProdSubtype_hom_snd {X Y Z : TopCat} (f : X โŸถ Z) (g : Y โŸถ Z) :
                      CategoryTheory.CategoryStruct.comp (pullbackIsoProdSubtype f g).hom (pullbackSnd f g) = CategoryTheory.Limits.pullback.snd f g
                      source
                      ๐Ÿ“ coverage
                      theorem TopCat.pullbackIsoProdSubtype_hom_apply {X Y Z : TopCat} {f : X โŸถ Z} {g : Y โŸถ Z} (x : โ†‘(CategoryTheory.Limits.pullback f g)) :
                      (CategoryTheory.ConcreteCategory.hom (pullbackIsoProdSubtype f g).hom) x = โŸจ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g)) x, (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g)) x), โ‹ฏโŸฉ
                      source
                      ๐Ÿ“ coverage
                      theorem TopCat.pullback_topology {X Y Z : TopCat} (f : X โŸถ Z) (g : Y โŸถ Z) :
                      (CategoryTheory.Limits.pullback f g).str = TopologicalSpace.induced (โ‡‘(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g))) X.str โŠ“ TopologicalSpace.induced (โ‡‘(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g))) Y.str
                      source
                      ๐Ÿ“ coverage
                      theorem TopCat.range_pullback_to_prod {X Y Z : TopCat} (f : X โŸถ Z) (g : Y โŸถ Z) :
                      Set.range โ‡‘(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.snd f g))) = {x : โ†‘(X โจฏ Y) | (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst f)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd g)) x}
                      source
                      ๐Ÿ”ธ coverage
                      noncomputable def TopCat.pullbackHomeoPreimage {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : X โ†’ Z) (hf : Continuous f) (g : Y โ†’ Z) (hg : Topology.IsEmbedding g) :
                      { p : X ร— Y // f p.1 = g p.2 } โ‰ƒโ‚œ โ†‘(f โปยน' Set.range g)

                      The pullback along an embedding is (isomorphic to) the preimage.

                      Equations
                        Instances For
                          source
                          ๐Ÿ“ coverage
                          theorem TopCat.isInducing_pullback_to_prod {X Y Z : TopCat} (f : X โŸถ Z) (g : Y โŸถ Z) :
                          Topology.IsInducing โ‡‘(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.snd f g)))
                          source
                          ๐Ÿ“ coverage
                          theorem TopCat.isEmbedding_pullback_to_prod {X Y Z : TopCat} (f : X โŸถ Z) (g : Y โŸถ Z) :
                          Topology.IsEmbedding โ‡‘(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.snd f g)))
                          source
                          ๐Ÿ“ coverage
                          theorem TopCat.range_pullback_map {W X Y Z S T : TopCat} (fโ‚ : W โŸถ S) (fโ‚‚ : X โŸถ S) (gโ‚ : Y โŸถ T) (gโ‚‚ : Z โŸถ T) (iโ‚ : W โŸถ Y) (iโ‚‚ : X โŸถ Z) (iโ‚ƒ : S โŸถ T) [Hโ‚ƒ : CategoryTheory.Mono iโ‚ƒ] (eqโ‚ : CategoryTheory.CategoryStruct.comp fโ‚ iโ‚ƒ = CategoryTheory.CategoryStruct.comp iโ‚ gโ‚) (eqโ‚‚ : CategoryTheory.CategoryStruct.comp fโ‚‚ iโ‚ƒ = CategoryTheory.CategoryStruct.comp iโ‚‚ gโ‚‚) :
                          Set.range โ‡‘(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.map fโ‚ fโ‚‚ gโ‚ gโ‚‚ iโ‚ iโ‚‚ iโ‚ƒ eqโ‚ eqโ‚‚)) = โ‡‘(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst gโ‚ gโ‚‚)) โปยน' Set.range โ‡‘(CategoryTheory.ConcreteCategory.hom iโ‚) โˆฉ โ‡‘(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd gโ‚ gโ‚‚)) โปยน' Set.range โ‡‘(CategoryTheory.ConcreteCategory.hom iโ‚‚)

                          If the map S โŸถ T is mono, then there is a description of the image of W ร—โ‚› X โŸถ Y ร—โ‚œ Z.

                          source
                          ๐Ÿ“ coverage
                          theorem TopCat.pullback_fst_range {X Y S : TopCat} (f : X โŸถ S) (g : Y โŸถ S) :
                          Set.range โ‡‘(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g)) = {x : โ†‘X | โˆƒ (y : โ†‘Y), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) y}
                          source
                          ๐Ÿ“ coverage
                          theorem TopCat.pullback_snd_range {X Y S : TopCat} (f : X โŸถ S) (g : Y โŸถ S) :
                          Set.range โ‡‘(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g)) = {y : โ†‘Y | โˆƒ (x : โ†‘X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) y}
                          source
                          ๐Ÿ“ coverage
                          theorem TopCat.pullback_map_isEmbedding {W X Y Z S T : TopCat} (fโ‚ : W โŸถ S) (fโ‚‚ : X โŸถ S) (gโ‚ : Y โŸถ T) (gโ‚‚ : Z โŸถ T) {iโ‚ : W โŸถ Y} {iโ‚‚ : X โŸถ Z} (Hโ‚ : Topology.IsEmbedding โ‡‘(CategoryTheory.ConcreteCategory.hom iโ‚)) (Hโ‚‚ : Topology.IsEmbedding โ‡‘(CategoryTheory.ConcreteCategory.hom iโ‚‚)) (iโ‚ƒ : S โŸถ T) (eqโ‚ : CategoryTheory.CategoryStruct.comp fโ‚ iโ‚ƒ = CategoryTheory.CategoryStruct.comp iโ‚ gโ‚) (eqโ‚‚ : CategoryTheory.CategoryStruct.comp fโ‚‚ iโ‚ƒ = CategoryTheory.CategoryStruct.comp iโ‚‚ gโ‚‚) :
                          Topology.IsEmbedding โ‡‘(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.map fโ‚ fโ‚‚ gโ‚ gโ‚‚ iโ‚ iโ‚‚ iโ‚ƒ eqโ‚ eqโ‚‚))

                          If there is a diagram where the morphisms W โŸถ Y and X โŸถ Z are embeddings, then the induced morphism W ร—โ‚› X โŸถ Y ร—โ‚œ Z is also an embedding.

                          W โŸถ Y
 โ†˜   โ†˜
  S โŸถ T
 โ†—   โ†—
X โŸถ Z
                          source
                          ๐Ÿ“ coverage
                          theorem TopCat.pullback_map_isOpenEmbedding {W X Y Z S T : TopCat} (fโ‚ : W โŸถ S) (fโ‚‚ : X โŸถ S) (gโ‚ : Y โŸถ T) (gโ‚‚ : Z โŸถ T) {iโ‚ : W โŸถ Y} {iโ‚‚ : X โŸถ Z} (Hโ‚ : Topology.IsOpenEmbedding โ‡‘(CategoryTheory.ConcreteCategory.hom iโ‚)) (Hโ‚‚ : Topology.IsOpenEmbedding โ‡‘(CategoryTheory.ConcreteCategory.hom iโ‚‚)) (iโ‚ƒ : S โŸถ T) [Hโ‚ƒ : CategoryTheory.Mono iโ‚ƒ] (eqโ‚ : CategoryTheory.CategoryStruct.comp fโ‚ iโ‚ƒ = CategoryTheory.CategoryStruct.comp iโ‚ gโ‚) (eqโ‚‚ : CategoryTheory.CategoryStruct.comp fโ‚‚ iโ‚ƒ = CategoryTheory.CategoryStruct.comp iโ‚‚ gโ‚‚) :
                          Topology.IsOpenEmbedding โ‡‘(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.map fโ‚ fโ‚‚ gโ‚ gโ‚‚ iโ‚ iโ‚‚ iโ‚ƒ eqโ‚ eqโ‚‚))

                          If there is a diagram where the morphisms W โŸถ Y and X โŸถ Z are open embeddings, and S โŸถ T is mono, then the induced morphism W ร—โ‚› X โŸถ Y ร—โ‚œ Z is also an open embedding.

                          W โŸถ Y
 โ†˜   โ†˜
  S โŸถ T
 โ†—   โ†—
X โŸถ Z
                          source
                          ๐Ÿ“ coverage
                          theorem TopCat.snd_isEmbedding_of_left {X Y S : TopCat} {f : X โŸถ S} (H : Topology.IsEmbedding โ‡‘(CategoryTheory.ConcreteCategory.hom f)) (g : Y โŸถ S) :
                          Topology.IsEmbedding โ‡‘(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g))
                          source
                          ๐Ÿ“ coverage
                          theorem TopCat.fst_isEmbedding_of_right {X Y S : TopCat} (f : X โŸถ S) {g : Y โŸถ S} (H : Topology.IsEmbedding โ‡‘(CategoryTheory.ConcreteCategory.hom g)) :
                          Topology.IsEmbedding โ‡‘(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g))
                          source
                          ๐Ÿ“ coverage
                          theorem TopCat.isEmbedding_of_pullback {X Y S : TopCat} {f : X โŸถ S} {g : Y โŸถ S} (Hโ‚ : Topology.IsEmbedding โ‡‘(CategoryTheory.ConcreteCategory.hom f)) (Hโ‚‚ : Topology.IsEmbedding โ‡‘(CategoryTheory.ConcreteCategory.hom g)) :
                          Topology.IsEmbedding โ‡‘(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.ฯ€ (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.one))
                          source
                          ๐Ÿ“ coverage
                          theorem TopCat.snd_isOpenEmbedding_of_left {X Y S : TopCat} {f : X โŸถ S} (H : Topology.IsOpenEmbedding โ‡‘(CategoryTheory.ConcreteCategory.hom f)) (g : Y โŸถ S) :
                          Topology.IsOpenEmbedding โ‡‘(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g))
                          source
                          ๐Ÿ“ coverage
                          theorem TopCat.fst_isOpenEmbedding_of_right {X Y S : TopCat} (f : X โŸถ S) {g : Y โŸถ S} (H : Topology.IsOpenEmbedding โ‡‘(CategoryTheory.ConcreteCategory.hom g)) :
                          Topology.IsOpenEmbedding โ‡‘(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g))
                          source
                          ๐Ÿ“ coverage
                          theorem TopCat.isOpenEmbedding_of_pullback {X Y S : TopCat} {f : X โŸถ S} {g : Y โŸถ S} (Hโ‚ : Topology.IsOpenEmbedding โ‡‘(CategoryTheory.ConcreteCategory.hom f)) (Hโ‚‚ : Topology.IsOpenEmbedding โ‡‘(CategoryTheory.ConcreteCategory.hom g)) :
                          Topology.IsOpenEmbedding โ‡‘(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.ฯ€ (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.one))

                          If X โŸถ S, Y โŸถ S are open embeddings, then so is X ร—โ‚› Y โŸถ S.

                          source
                          ๐Ÿ“ coverage
                          theorem TopCat.fst_iso_of_right_embedding_range_subset {X Y S : TopCat} (f : X โŸถ S) {g : Y โŸถ S} (hg : Topology.IsEmbedding โ‡‘(CategoryTheory.ConcreteCategory.hom g)) (H : Set.range โ‡‘(CategoryTheory.ConcreteCategory.hom f) โŠ† Set.range โ‡‘(CategoryTheory.ConcreteCategory.hom g)) :
                          CategoryTheory.IsIso (CategoryTheory.Limits.pullback.fst f g)
                          source
                          ๐Ÿ“ coverage
                          theorem TopCat.snd_iso_of_left_embedding_range_subset {X Y S : TopCat} {f : X โŸถ S} (hf : Topology.IsEmbedding โ‡‘(CategoryTheory.ConcreteCategory.hom f)) (g : Y โŸถ S) (H : Set.range โ‡‘(CategoryTheory.ConcreteCategory.hom g) โŠ† Set.range โ‡‘(CategoryTheory.ConcreteCategory.hom f)) :
                          CategoryTheory.IsIso (CategoryTheory.Limits.pullback.snd f g)
                          source
                          ๐Ÿ“ coverage
                          theorem TopCat.pullback_snd_image_fst_preimage {X Y Z : TopCat} (f : X โŸถ Z) (g : Y โŸถ Z) (U : Set โ†‘X) :
                          โ‡‘(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g)) '' (โ‡‘(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g)) โปยน' U) = โ‡‘(CategoryTheory.ConcreteCategory.hom g) โปยน' (โ‡‘(CategoryTheory.ConcreteCategory.hom f) '' U)
                          source
                          ๐Ÿ“ coverage
                          theorem TopCat.pullback_fst_image_snd_preimage {X Y Z : TopCat} (f : X โŸถ Z) (g : Y โŸถ Z) (U : Set โ†‘Y) :
                          โ‡‘(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g)) '' (โ‡‘(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g)) โปยน' U) = โ‡‘(CategoryTheory.ConcreteCategory.hom f) โปยน' (โ‡‘(CategoryTheory.ConcreteCategory.hom g) '' U)
                          source
                          ๐Ÿ“ coverage
                          theorem TopCat.isOpen_iff_of_isColimit_cofork {X Y : TopCat} {f g : X โŸถ Y} (c : CategoryTheory.Limits.Cofork f g) (hc : CategoryTheory.Limits.IsColimit c) (U : Set โ†‘c.pt) :
                          IsOpen U โ†” IsOpen (โ‡‘(CategoryTheory.ConcreteCategory.hom c.ฯ€) โปยน' U)
                          source
                          ๐Ÿ“ coverage
                          theorem TopCat.isQuotientMap_of_isColimit_cofork {X Y : TopCat} {f g : X โŸถ Y} (c : CategoryTheory.Limits.Cofork f g) (hc : CategoryTheory.Limits.IsColimit c) :
                          Topology.IsQuotientMap โ‡‘(CategoryTheory.ConcreteCategory.hom c.ฯ€)
                          source
                          ๐Ÿ“ coverage
                          theorem TopCat.coequalizer_isOpen_iff {X Y : TopCat} {f g : X โŸถ Y} (U : Set โ†‘(CategoryTheory.Limits.coequalizer f g)) :
                          IsOpen U โ†” IsOpen (โ‡‘(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.coequalizer.ฯ€ f g)) โปยน' U)