TopCat.prodIsoProd_hom_fst
theorem TopCat.prodIsoProd_hom_fst :
∀ (X Y : TopCat),
CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).hom TopCat.prodFst = CategoryTheory.Limits.prod.fst
This theorem states that for every pair of topological spaces, `X` and `Y`, in the category of topological spaces `TopCat`, the composition of the morphism from the categorical product `X ⨯ Y` to the set-theoretic product `↑X × ↑Y` (represented by `(TopCat.prodIsoProd X Y).hom`) and the first projection function `TopCat.prodFst` from this set-theoretic product back to `X` is equal to the first projection function `CategoryTheory.Limits.prod.fst` in the category of topological spaces. In other words, it asserts the compatibility of these mappings with respect to the categorical and set-theoretic notions of products in the category of topological spaces.
More concisely: For every pair of topological spaces X and Y, the morphism from the topological product X ⨯ Y to the set-theoretic product ↑X × ↑Y, followed by the first projection function from the set-theoretic product, equals the first projection function of the topological product in the category of topological spaces.
|
TopCat.prodIsoProd_hom_snd
theorem TopCat.prodIsoProd_hom_snd :
∀ (X Y : TopCat),
CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).hom TopCat.prodSnd = CategoryTheory.Limits.prod.snd
The theorem `TopCat.prodIsoProd_hom_snd` states that for any two topological spaces `X` and `Y`, the composition of the homeomorphism from the categorical product `X ⨯ Y` to the set-theoretic product equipped with the product topology and the second projection from the set-theoretic product equals the second projection from the categorical product. In other words, if we first map the categorical product to the set-theoretic product (using the homeomorphism) and then project to the second component, this is the same as projecting to the second component in the category of topological spaces.
More concisely: The homeomorphism from the categorical product of topological spaces X and Y to their set-theoretic product with product topology preserves the second projection, that is, the second projection of the categorical product equals the composition of the homeomorphism with the second projection of the set-theoretic product.
|
Mathlib.Topology.Category.TopCat.Limits.Products._auxLemma.1
theorem Mathlib.Topology.Category.TopCat.Limits.Products._auxLemma.1 :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) {f : X ⟶ Z} {g : Y ⟶ Z},
(CategoryTheory.CategoryStruct.comp α.hom g = f) = (g = CategoryTheory.CategoryStruct.comp α.inv f)
The theorem states that, for any category `C` and objects `X`, `Y`, and `Z` in `C`, given an isomorphism `α` from `X` to `Y` and morphisms `f` from `X` to `Z` and `g` from `Y` to `Z`, the composition of the isomorphism's forward map `α.hom` with `g` being equal to `f` is equivalent to `g` being equal to the composition of the isomorphism's inverse map `α.inv` with `f`.
More concisely: For any category C, objects X, Y, Z, isomorphism α from X to Y, and morphisms f from X to Z and g from Y to Z, the equality of α.hom ∘ g with f is equivalent to the equality of g with α.inv ∘ f.
|
Mathlib.Topology.Category.TopCat.Limits.Products._auxLemma.2
theorem Mathlib.Topology.Category.TopCat.Limits.Products._auxLemma.2 :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) {f : X ⟶ Z} {g : Y ⟶ Z},
(CategoryTheory.CategoryStruct.comp α.inv f = g) = (f = CategoryTheory.CategoryStruct.comp α.hom g)
This theorem states that for any category `C` and objects `X`, `Y`, `Z` in `C`, and an isomorphism `α` from `X` to `Y`, as well as morphisms `f` from `X` to `Z` and `g` from `Y` to `Z`, the statement that the composition of the inverse of `α` and `f` equals `g` is equivalent to the statement that `f` equals the composition of `α` and `g`.
In other words, if you have an isomorphism between two objects in a category and you map one of these objects to a third object, you can "reverse" the isomorphism and then perform the mapping to achieve the same result as if you had performed the mapping first and then applied the isomorphism.
More concisely: For any category C, isomorphism α from X to Y, and morphisms f: X → Z and g: Y → Z, the equality of α⁻¹ ∘ f and g is equivalent to the equality of f and α ∘ g.
|