Documentation

Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Pullbacks and pushouts in the category of topological spaces #

@[reducible, inline]
abbrev TopCat.pullbackFst {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Z) (g : Y Z) :
TopCat.of { p : X × Y // f p.1 = g p.2 } X

The first projection from the pullback.

Equations
Instances For
    theorem TopCat.pullbackFst_apply {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Z) (g : Y Z) (x : (TopCat.of { p : X × Y // f p.1 = g p.2 })) :
    (TopCat.pullbackFst f g) x = (x).1
    @[reducible, inline]
    abbrev TopCat.pullbackSnd {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Z) (g : Y Z) :
    TopCat.of { p : X × Y // f p.1 = g p.2 } Y

    The second projection from the pullback.

    Equations
    Instances For
      theorem TopCat.pullbackSnd_apply {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Z) (g : Y Z) (x : (TopCat.of { p : X × Y // f p.1 = g p.2 })) :
      (TopCat.pullbackSnd f g) x = (x).2
      def TopCat.pullbackCone {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Z) (g : Y Z) :

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

      Equations
      Instances For

        The constructed cone is a limit.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def TopCat.pullbackIsoProdSubtype {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Z) (g : Y Z) :
          CategoryTheory.Limits.pullback f g TopCat.of { p : X × Y // f p.1 = g p.2 }

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

          Equations
          Instances For
            theorem TopCat.pullbackIsoProdSubtype_inv_fst_apply {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Z) (g : Y Z) (x : { p : X × Y // f p.1 = g p.2 }) :
            theorem TopCat.pullbackIsoProdSubtype_inv_snd_apply {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Z) (g : Y Z) (x : { p : X × Y // f p.1 = g p.2 }) :
            theorem TopCat.pullbackIsoProdSubtype_hom_apply {X : TopCat} {Y : TopCat} {Z : TopCat} {f : X Z} {g : Y Z} (x : CategoryTheory.ConcreteCategory.forget.obj (CategoryTheory.Limits.pullback f g)) :
            theorem TopCat.range_pullback_to_prod {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Z) (g : Y Z) :
            noncomputable def TopCat.pullbackHomeoPreimage {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : XZ) (hf : Continuous f) (g : YZ) (hg : Embedding 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
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem TopCat.range_pullback_map {W : TopCat} {X : TopCat} {Y : TopCat} {Z : TopCat} {S : TopCat} {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.Limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) = (CategoryTheory.Limits.pullback.fst g₁ g₂) ⁻¹' Set.range i₁ (CategoryTheory.Limits.pullback.snd g₁ g₂) ⁻¹' Set.range i₂

              If the map S ⟶ T is mono, then there is a description of the image of W ×ₛ X ⟶ Y ×ₜ Z.

              theorem TopCat.pullback_fst_range {X : TopCat} {Y : TopCat} {S : TopCat} (f : X S) (g : Y S) :
              Set.range (CategoryTheory.Limits.pullback.fst f g) = {x : X | ∃ (y : Y), f x = g y}
              theorem TopCat.pullback_snd_range {X : TopCat} {Y : TopCat} {S : TopCat} (f : X S) (g : Y S) :
              Set.range (CategoryTheory.Limits.pullback.snd f g) = {y : Y | ∃ (x : X), f x = g y}
              theorem TopCat.pullback_map_embedding_of_embeddings {W : TopCat} {X : TopCat} {Y : TopCat} {Z : TopCat} {S : TopCat} {T : TopCat} (f₁ : W S) (f₂ : X S) (g₁ : Y T) (g₂ : Z T) {i₁ : W Y} {i₂ : X Z} (H₁ : Embedding i₁) (H₂ : Embedding 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₂) :
              Embedding (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
              
              theorem TopCat.pullback_map_openEmbedding_of_open_embeddings {W : TopCat} {X : TopCat} {Y : TopCat} {Z : TopCat} {S : TopCat} {T : TopCat} (f₁ : W S) (f₂ : X S) (g₁ : Y T) (g₂ : Z T) {i₁ : W Y} {i₂ : X Z} (H₁ : OpenEmbedding i₁) (H₂ : OpenEmbedding 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₂) :
              OpenEmbedding (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
              

              If X ⟶ S, Y ⟶ S are open embeddings, then so is X ×ₛ Y ⟶ S.

              theorem TopCat.pullback_snd_image_fst_preimage {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Z) (g : Y Z) (U : Set X) :
              theorem TopCat.pullback_fst_image_snd_preimage {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Z) (g : Y Z) (U : Set Y) :