ContinuousMap.Homotopy.heq_path_of_eq_image
theorem ContinuousMap.Homotopy.heq_path_of_eq_image :
∀ {X₁ X₂ Y : TopCat} {f : C(↑X₁, ↑Y)} {g : C(↑X₂, ↑Y)} {x₀ x₁ : ↑X₁} {x₂ x₃ : ↑X₂} {p : Path x₀ x₁}
{q : Path x₂ x₃},
(∀ (t : ↑unitInterval), f (p t) = g (q t)) →
HEq ((FundamentalGroupoid.fundamentalGroupoidFunctor.map f).map ⟦p⟧)
((FundamentalGroupoid.fundamentalGroupoidFunctor.map g).map ⟦q⟧)
The theorem `ContinuousMap.Homotopy.heq_path_of_eq_image` states that for any two topological spaces `X₁` and `X₂`, and any other topological space `Y`, given two continuous maps `f: X₁ → Y` and `g: X₂ → Y`, and two paths `p` in `X₁` and `q` in `X₂`, if for every `t` in the unit interval `[0, 1]`, the image of `p(t)` under `f` is equal to the image of `q(t)` under `g`, then the path homotopy classes induced by `f` and `g` are the same, represented by the equivalence of `f(p)` and `g(q)` in the fundamental groupoid of `Y`, despite the fact that they may have different types. This is a homotopy equivalence theorem in the context of topological spaces, continuous maps, and fundamental groupoids.
More concisely: If two continuous maps between topological spaces induce the same image of paths under every point in the unit interval, then their corresponding path homotopy classes in the fundamental groupoid of the target space are equal.
|
ContinuousMap.Homotopy.apply_zero_path
theorem ContinuousMap.Homotopy.apply_zero_path :
∀ {X Y : TopCat} {f g : C(↑X, ↑Y)} (H : f.Homotopy g) {x₀ x₁ : ↑X}
(p : FundamentalGroupoid.fromTop x₀ ⟶ FundamentalGroupoid.fromTop x₁),
(FundamentalGroupoid.fundamentalGroupoidFunctor.map f).map p =
CategoryTheory.CategoryStruct.comp (ContinuousMap.Homotopy.hcast ⋯)
(CategoryTheory.CategoryStruct.comp
((FundamentalGroupoid.fundamentalGroupoidFunctor.map H.uliftMap).map
(ContinuousMap.Homotopy.prodToProdTopI
(CategoryTheory.CategoryStruct.id (FundamentalGroupoid.fromTop { down := 0 })) p))
(ContinuousMap.Homotopy.hcast ⋯))
This theorem, `ContinuousMap.Homotopy.apply_zero_path`, establishes a pivotal equality involving the application of a continuous map to a path in the fundamental groupoid of a topological space. Specifically, for any two topological spaces `X` and `Y`, continuous maps `f` and `g` from `X` to `Y`, a homotopy `H` from `f` to `g`, and a path `p` in the fundamental groupoid of `X` from `x₀` to `x₁`, it proves that the application of the fundamental groupoid functor's map of `f` to `p` is equal to a complicated composition of morphisms involving `H`. This composition includes the casting of equalities to isomorphisms (`ContinuousMap.Homotopy.hcast`), the mapping of a product of paths to a product of topological spaces via `H` (`ContinuousMap.Homotopy.prodToProdTopI`) under the fundamental groupoid functor's map of `H.uliftMap`, and the identity morphism on the fundamental groupoid of `0`.
More concisely: For any continuous maps `f` and `g` between topological spaces `X` and `Y`, a homotopy `H` from `f` to `g`, and a path `p` in the fundamental groupoid of `X`, the application of `f` to `p` under the fundamental groupoid functor is equal to the composition of `H.uliftMap` with the product of the path `p` with the identity path at the basepoint and the casting of the resulting equalities to isomorphisms.
|
ContinuousMap.Homotopy.apply_one_path
theorem ContinuousMap.Homotopy.apply_one_path :
∀ {X Y : TopCat} {f g : C(↑X, ↑Y)} (H : f.Homotopy g) {x₀ x₁ : ↑X}
(p : FundamentalGroupoid.fromTop x₀ ⟶ FundamentalGroupoid.fromTop x₁),
(FundamentalGroupoid.fundamentalGroupoidFunctor.map g).map p =
CategoryTheory.CategoryStruct.comp (ContinuousMap.Homotopy.hcast ⋯)
(CategoryTheory.CategoryStruct.comp
((FundamentalGroupoid.fundamentalGroupoidFunctor.map H.uliftMap).map
(ContinuousMap.Homotopy.prodToProdTopI
(CategoryTheory.CategoryStruct.id (FundamentalGroupoid.fromTop { down := 1 })) p))
(ContinuousMap.Homotopy.hcast ⋯))
This theorem, `ContinuousMap.Homotopy.apply_one_path`, demonstrates that for any two continuous maps `f` and `g` between topological spaces `X` and `Y`, given a homotopy `H` between `f` and `g`, and a path `p` in the fundamental groupoid of `X` from `x₀` to `x₁`, the action of the fundamental groupoid functor on `g` applied to the path `p` is equivalent to a particular composition of morphisms. Specifically, this composition involves two casts (using `ContinuousMap.Homotopy.hcast`) and the mapping under the fundamental groupoid functor of a certain morphism involving `H`, the identity on the fundamental groupoid element representing `1`, and the original path `p`.
More concisely: Given continuous maps `f` and `g` between topological spaces `X` and `Y`, a homotopy `H` between them, and a path `p` in the fundamental groupoid of `X` from `x₀` to `x₁`, the action of the fundamental groupoid functor on `g` applied to `p` is equivalent to the composition of `g` with `H` at `x₀`, the identity on the fundamental groupoid element representing `1`, and the application of `f` to `p`.
|
ContinuousMap.Homotopy.evalAt_eq
theorem ContinuousMap.Homotopy.evalAt_eq :
∀ {X Y : TopCat} {f g : C(↑X, ↑Y)} (H : f.Homotopy g) (x : ↑X),
⟦H.evalAt x⟧ =
CategoryTheory.CategoryStruct.comp (ContinuousMap.Homotopy.hcast ⋯)
(CategoryTheory.CategoryStruct.comp
((FundamentalGroupoid.fundamentalGroupoidFunctor.map H.uliftMap).map
(ContinuousMap.Homotopy.prodToProdTopI unitInterval.uhpath01
(CategoryTheory.CategoryStruct.id (FundamentalGroupoid.fromTop x))))
(ContinuousMap.Homotopy.hcast ⋯))
This theorem states that for any two continuous maps `f` and `g` between topological spaces `X` and `Y`, and any homotopy `H` between `f` and `g`, the equivalence class of the evaluation of `H` at any point `x` in `X` equals the composition of several morphisms in the category of topological spaces.
Specifically, it is the composition of a morphism resulting from a homotopy cast operation (essentially a conversion of equality into a specific form of homotopy), a morphism obtained by applying the functor that sends a topological space to its fundamental groupoid to a particular map from the product of the unit interval and `X` to the product of `Y` and `X`, and another morphism resulting from a similar homotopy cast operation.
In simpler terms, it is relating the evaluation of a homotopy at a point with some complex categorical operations which include the fundamental groupoid of a space, a concept that captures the essential information about paths in the space.
More concisely: For any continuous maps `f` and `g` between topological spaces `X` and `Y` with a homotopy `H` between them, the evaluation of `H` at any point `x` in `X` is equivalent to the composition of the homotopy cast of `H` with the map induced by `H` on the product of the unit interval and `X`, and the homotopy cast of a constant map from `X` to `Y` with the fundamental groupoid of `Y` and the inverse of the fundamental groupoid of `X` applied to the map `x ∈ X mapsto (id_Y, x) ∈ Y × X`.
|