Path.Homotopic.comp_prod_eq_prod_comp
theorem Path.Homotopic.comp_prod_eq_prod_comp :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {a₁ a₂ a₃ : α}
{b₁ b₂ b₃ : β} (q₁ : Path.Homotopic.Quotient a₁ a₂) (q₂ : Path.Homotopic.Quotient b₁ b₂)
(r₁ : Path.Homotopic.Quotient a₂ a₃) (r₂ : Path.Homotopic.Quotient b₂ b₃),
(Path.Homotopic.prod q₁ q₂).comp (Path.Homotopic.prod r₁ r₂) = Path.Homotopic.prod (q₁.comp r₁) (q₂.comp r₂)
The theorem `Path.Homotopic.comp_prod_eq_prod_comp` states that in any topological spaces `α` and `β`, for any three points `a₁`, `a₂`, `a₃` in `α`, and any three points `b₁`, `b₂`, `b₃` in `β`, the composition of the path products `q₁` and `q₂`, and `r₁` and `r₂`, is the same as the product of the composed paths `q₁.comp r₁` and `q₂.comp r₂`. Here, the paths `q₁` and `r₁` are between points `a₁`, `a₂`, `a₃` respectively and the paths `q₂` and `r₂` are between points `b₁`, `b₂`, `b₃` respectively. This is a descent to the quotient of the statement that products commute with path composition.
More concisely: For any topological spaces `α` and `β`, and points `a₁, a₂, a₃ in α` and `b₁, b₂, b₃ in β`, the path products `q₁ : a₁ ┼ a₂ ┼ a₃` and `q₂ : b₁ ┼ b₂ ┼ b₃` satisfy `(q₁ ⊤ r₁) ⊤ (q₂ ⊤ r₂) = (q₁ ⊗ q₂) ⊤ (r₁ ⊗ r₂)`, where `q₁ ⊤ r₁` and `q₂ ⊤ r₂` are the compositions of the paths and `q₁ ⊗ q₂` and `r₁ ⊗ r₂` are the path products.
|
Path.Homotopic.projLeft_prod
theorem Path.Homotopic.projLeft_prod :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {a₁ a₂ : α} {b₁ b₂ : β}
(q₁ : Path.Homotopic.Quotient a₁ a₂) (q₂ : Path.Homotopic.Quotient b₁ b₂),
Path.Homotopic.projLeft (Path.Homotopic.prod q₁ q₂) = q₁
This theorem states that for any two topological spaces, `α` and `β`, and any two pairs of points `(a₁, a₂)` in `α` and `(b₁, b₂)` in `β`, the projection onto the left coordinate of the product of path classes `q₁` and `q₂` is equal to the path class `q₁`. Here, `q₁` is a path class in `α` from `a₁` to `a₂`, and `q₂` is a path class in `β` from `b₁` to `b₂`. The path classes are equivalence classes of paths under the homotopy relation. The product of path classes is a path class in the product space. Essentially, this theorem asserts that projecting out the first component after forming the path product recovers the original path class in the first space.
More concisely: For any paths $q\_1$ in topological space $\alpha$ and $q\_2$ in topological space $\beta$ from points $a\_1$, $a\_2$ in $\alpha$ and $b\_1$, $b\_2$ in $\beta$ respectively, the projection of the product path class $[q\_1] \times [q\_2]$ in the product space onto its first coordinate is equal to the path class $[q\_1]$ in $\alpha$.
|
Path.Homotopic.comp_pi_eq_pi_comp
theorem Path.Homotopic.comp_pi_eq_pi_comp :
∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {as bs cs : (i : ι) → X i}
(γ₀ : (i : ι) → Path.Homotopic.Quotient (as i) (bs i)) (γ₁ : (i : ι) → Path.Homotopic.Quotient (bs i) (cs i)),
(Path.Homotopic.pi γ₀).comp (Path.Homotopic.pi γ₁) = Path.Homotopic.pi fun i => (γ₀ i).comp (γ₁ i)
This theorem, `Path.Homotopic.comp_pi_eq_pi_comp`, states that composition and products commute in the context of path homotopy classes. Specifically, for any types `ι` and `X` indexed by `ι`, and for any three families of elements `as`, `bs`, and `cs` of the spaces `X i` (for every `i` in `ι`), if we have two families of path homotopy classes `γ₀` and `γ₁` from `as i` to `bs i` and from `bs i` to `cs i` respectively, then the composition of the path homotopy product of `γ₀` with the path homotopy product of `γ₁` is equal to the path homotopy product of the compositions of `γ₀ i` and `γ₁ i`. In other words, when working with path homotopy classes, we can either first take products and then compose, or first compose and then take products, and we'll end up with the same result.
More concisely: Given families of elements and their path homotopy classes in a space indexed by a type, the composition of their path homotopy products is equal to the path homotopy product of their compositions.
|
Path.Homotopic.proj_pi
theorem Path.Homotopic.proj_pi :
∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {as bs : (i : ι) → X i} (i : ι)
(paths : (i : ι) → Path.Homotopic.Quotient (as i) (bs i)),
Path.Homotopic.proj i (Path.Homotopic.pi paths) = paths i
This theorem, named `Path.Homotopic.proj_pi`, states that for all types `ι` and `as`, `bs` functions from `ι` to some type `X` (where each `X i` is a topological space), and any index `i` in `ι`, when we take a family of path homotopy classes `paths` (each path being from `as i` to `bs i` for some `i` in `ι`), and form a product of these path homotopy classes using the `Path.Homotopic.pi` function, projecting back to the `i`th coordinate using the `Path.Homotopic.proj` function gives us the original path homotopy class at `i` in the `paths` family. In other words, the projection operation is the inverse of the pi operation in the context of path homotopy classes.
More concisely: The `Path.Homotopic.proj_pi` theorem in Lean 4 asserts that the projection of the product of path homotopy classes, obtained using `Path.Homotopic.pi`, is equal to the original path homotopy class in each coordinate.
|
Path.Homotopic.pi_lift
theorem Path.Homotopic.pi_lift :
∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {as bs : (i : ι) → X i}
(γ : (i : ι) → Path (as i) (bs i)), (Path.Homotopic.pi fun i => ⟦γ i⟧) = ⟦Path.pi γ⟧
The theorem `Path.Homotopic.pi_lift` asserts that for any indexed type `ι`, any function `X` assigning a specific type to each index `ι`, any instances of topological spaces for each `X i`, and any two functions `as` and `bs` from index `ι` to the corresponding type, if we have a function `γ` assigning a path from `as i` to `bs i` for each index `i`, then the homotopy class of the pointwise product path (obtained from the product of homotopy classes of each path `γ i`) equals the homotopy class of the path obtained from the pointwise product of each path `γ i`. In other words, the process of forming the homotopy class commutes with the process of forming the pointwise product path.
More concisely: The homotopy classes of pointwise product paths between functions from an indexed type to topological spaces equal the pointwise product of their individual homotopy classes.
|