TopCat.pullback_map_embedding_of_embeddings
theorem TopCat.pullback_map_embedding_of_embeddings :
∀ {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},
Embedding ⇑i₁ →
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₂)
This theorem, `TopCat.pullback_map_embedding_of_embeddings`, states that in the category of topological spaces (`TopCat`), given any two topological spaces `W, X, Y, Z, S, T` and morphisms `f₁ : W ⟶ S, f₂ : X ⟶ S, g₁ : Y ⟶ T, g₂ : Z ⟶ T, i₁ : W ⟶ Y, i₂ : X ⟶ Z, i₃ : S ⟶ T` such that `f₁` followed by `i₃` is the same as `i₁` followed by `g₁` and similarly `f₂` followed by `i₃` is the same as `i₂` followed by `g₂` (i.e., `f₁ ≫ i₃ = i₁ ≫ g₁` and `f₂ ≫ i₃ = i₂ ≫ g₂`), if the morphisms `i₁` and `i₂` are embeddings (i.e., injective and induce topological embeddings), then the induced morphism from the pullback of `f₁, f₂` along `g₁, g₂` to the pullback of `i₁, i₂` along `g₁, g₂` is also an embedding.
This is a property relating the concept of pullbacks in category theory and embeddings in topology, essentially stating that the pullback of embeddings is also an embedding, under certain conditions.
More concisely: Given topological spaces W, X, Y, Z, S, T and embeddings i₁ : W ⟶ Y, i₂ : X ⟶ Z, morphisms f₁ : W ⟶ S, f₂ : X ⟶ S, g₁ : Y ⟶ T, g₂ : Z ⟶ T, and if f₁ ≫ i₃ = i₁ ≫ g₁ and f₂ ≫ i₃ = i₂ ≫ g₂ hold, then the induced morphism from the pullback of f₁, f₂ along g₁, g₂ to the pullback of i₁, i₂ along g₁, g₂ is also an embedding.
|
TopCat.openEmbedding_of_pullback_open_embeddings
theorem TopCat.openEmbedding_of_pullback_open_embeddings :
∀ {X Y S : TopCat} {f : X ⟶ S} {g : Y ⟶ S},
OpenEmbedding ⇑f →
OpenEmbedding ⇑g →
OpenEmbedding
⇑(CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g)
CategoryTheory.Limits.WalkingCospan.one)
This theorem states that if we have two open embeddings from topological spaces `X` and `Y` to a topological space `S` (represented as morphisms `f` : `X ⟶ S` and `g` : `Y ⟶ S` in category theory), then the projection from the limit of the cospan of `f` and `g` to the central point of the walking cospan is also an open embedding.
In simpler terms, it shows that if two sets `X` and `Y` are both open in a topological space `S` (i.e., they are embedded in `S` in such a way that `S` possesses a certain topological structure), then their product in the category of topological spaces, denoted as `X ×ₛ Y`, also possesses a similar open embedding into `S`. This is a property related to pullbacks in category theory and open sets in topology.
More concisely: If `f : X ⟶ S` and `g : Y ⟶ S` are open embeddings in a topological space `S`, then the projection from the limit of their cospan to the central point of the walking cospan is an open embedding.
|
TopCat.range_pullback_map
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.Limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) =
⇑CategoryTheory.Limits.pullback.fst ⁻¹' Set.range ⇑i₁ ∩ ⇑CategoryTheory.Limits.pullback.snd ⁻¹' Set.range ⇑i₂
This theorem states that in the category of topological spaces (`TopCat`), given spaces `W`, `X`, `Y`, `Z`, `S`, and `T`, morphisms `f₁ : W ⟶ S`, `f₂ : X ⟶ S`, `g₁ : Y ⟶ T`, `g₂ : Z ⟶ T`, `i₁ : W ⟶ Y`, `i₂ : X ⟶ Z`, `i₃ : S ⟶ T`, and the assumption that `i₃` is monic (an injective map), if the compositions `f₁ ≫ i₃` and `i₁ ≫ g₁` are equal, and `f₂ ≫ i₃` and `i₂ ≫ g₂` are equal, then the range of the map from the pullback of `f₁` and `f₂` to the pullback of `g₁` and `g₂` is equal to the intersection of the preimage of the range of `i₁` under the first projection of the pullback and the preimage of the range of `i₂` under the second projection of the pullback.
In simpler terms, this theorem describes a property of the image of a map between pullbacks in the category of topological spaces in terms of the ranges of two other maps and their interaction with certain pullback projections, assuming a certain equality condition between composed morphisms.
More concisely: Given topological spaces `W`, `X`, `Y`, `Z`, `S`, `T`, morphisms `f₁ : W ⟶ S`, `f₂ : X ⟶ S`, `g₁ : Y �re� T`, `g₂ : Z ⟶ T`, `i₁ : W ⟶ Y`, `i₂ : X ⟶ Z`, `i₃ : S ⟶ T` monic, if `f₁ ≫ i₃ = i₁ ≫ g₁` and `f₂ ≫ i₃ = i₂ ≫ g₂`, then the pullback of `f₁` and `f₂` is contained in the pullback of `g₁` and `g₂`, and their ranges intersect only in the pullback.
|
TopCat.snd_openEmbedding_of_left_openEmbedding
theorem TopCat.snd_openEmbedding_of_left_openEmbedding :
∀ {X Y S : TopCat} {f : X ⟶ S},
OpenEmbedding ⇑f → ∀ (g : Y ⟶ S), OpenEmbedding ⇑CategoryTheory.Limits.pullback.snd
This theorem states that for any three topological spaces `X`, `Y`, and `S` in the category of topological spaces (`TopCat`), given a morphism `f` from `X` to `S`, if `f` is an open embedding then for any morphism `g` from `Y` to `S`, the second projection of the pullback of `f` and `g` is also an open embedding. In other words, if `f` is an open embedding in a pullback diagram, it ensures that the pullback of `f` and any map `g` from `Y` to `S` has its second projection as an open embedding.
More concisely: If `f: X → S` is an open embedding in the category of topological spaces, then the second projection of the pullback of `f` with any morphism `g: Y → S` is an open embedding.
|
TopCat.pullback_map_openEmbedding_of_open_embeddings
theorem TopCat.pullback_map_openEmbedding_of_open_embeddings :
∀ {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},
OpenEmbedding ⇑i₁ →
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₂)
This theorem states that in the category of topological spaces, if there exists a commutative diagram with morphisms `W ⟶ Y` and `X ⟶ Z` being open embeddings, and `S ⟶ T` being a monomorphism (an injective morphism), then the induced morphism from the product of `W` and `X` to the product of `Y` and `Z` (denoted `W ×ₛ X ⟶ Y ×ₜ Z`) is also an open embedding. In other words, it assures that the property of being an open embedding is preserved under this specific limit operation in the category of topological spaces.
More concisely: In the category of topological spaces, if `W ⟶ Y`, `X ⟶ Z` are open embeddings and `S ⟶ T` is a monomorphism, then the induced morphism from `W × X` to `Y × Z` is an open embedding.
|