HomotopyGroup.mul_spec
theorem HomotopyGroup.mul_spec :
∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] [inst_2 : Nonempty N]
{i : N} {p q : ↑(GenLoop N X x)}, (fun x_1 x_2 => x_1 * x_2) ⟦p⟧ ⟦q⟧ = ⟦GenLoop.transAt i q p⟧
This theorem, named "HomotopyGroup.mul_spec", characterizes the multiplication operation in the context of homotopy groups. Given a type `N`, a topological space `X`, a point `x` in `X`, a decidable equality on `N`, and an instance to show `N` is non-empty, the theorem states that for any `N`, `i`, and any two generalized loops `p` and `q` based at `x` in `X`, the multiplication of equivalence classes of `p` and `q` is equal to the equivalence class of the generalized loop obtained by invoking the `GenLoop.transAt` operation with `i`, `q`, and `p`. Here, the `GenLoop.transAt` operation represents a specific transition in the loop space. Essentially, this theorem formalizes a property of the multiplication operation in the homotopy group context, connecting it with the manipulation of generalized loops.
More concisely: Given a topological space X, a point x, and a type N with a decidable equality and non-empty instance, the multiplication of homotopy classes of generalized loops based at x in X is equal to the homotopy class of the loop obtained by composing them using the GenLoop.transAt operation.
|
HomotopyGroup.one_def
theorem HomotopyGroup.one_def :
∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] [inst_2 : Nonempty N],
1 = ⟦GenLoop.const⟧
This theorem establishes the characterization of multiplicative identity in the context of homotopy groups. Given any types `N` and `X`, with `X` being a topological space, and any instance `x : X`, and ensuring that equality in `N` is decidable and `N` is nonempty, it states that the multiplicative identity `1` is equivalent to the equivalence class of the constant generalized loop at `x` (denoted by `GenLoop.const`). In essence, the unit of multiplication in this homotopy group context is given by the class of constant loops.
More concisely: In the context of homotopy groups, the multiplicative identity is equivalent to the equivalence class of constant loops for any topological space X and point x in X, under the assumption of decidable equality and nonempty N.
|
HomotopyGroup.inv_spec
theorem HomotopyGroup.inv_spec :
∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] [inst_2 : Nonempty N]
{i : N} {p : ↑(GenLoop N X x)}, (⟦p⟧)⁻¹ = ⟦GenLoop.symmAt i p⟧
The theorem `HomotopyGroup.inv_spec` characterizes the multiplicative inverse in a homotopy group. Specifically, for any type `N`, topological space `X`, point `x` in `X`, decidable equality instance on `N`, nonempty instance on `N`, an element `i` of `N`, and a generalized loop `p` based at `x` in `X`, it states that the multiplicative inverse of the homotopy class of `p` is equal to the homotopy class of the reversed loop `GenLoop.symmAt i p` where the reversal is done along the `i`th coordinate. In other words, taking the multiplicative inverse in the homotopy group corresponds to reversing the loop along one of its coordinates.
More concisely: The multiplicative inverse of a loop's homotopy class in the homotopy group is equal to the homotopy class of its reversed loop along a specific coordinate.
|
GenLoop.ext
theorem GenLoop.ext :
∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} (f g : ↑(GenLoop N X x)),
(∀ (y : N → ↑unitInterval), f y = g y) → f = g
The theorem `GenLoop.ext` states that for all types `N` and `X`, where `X` is a topological space, and for all points `x` in `X`, if `f` and `g` are elements of the generalized loops based at `x`, then if `f` and `g` are equal on every point `y` in `N` mapping to the unit interval `[0,1]`, then `f` and `g` are indeed the same function. This means that two generalized loops are considered identical if they match on every point in their domain.
More concisely: If two generalized loops based at a point in a topological space agree on every point mapping to the unit interval, then they are equal as functions.
|
Cube.insertAt_boundary
theorem Cube.insertAt_boundary :
∀ {N : Type u_1} [inst : DecidableEq N] (i : N) {t₀ : ↑unitInterval} {t : { j // j ≠ i } → ↑unitInterval},
(t₀ = 0 ∨ t₀ = 1) ∨ t ∈ Cube.boundary { j // j ≠ i } → (Cube.insertAt i) (t₀, t) ∈ Cube.boundary N
This theorem, `Cube.insertAt_boundary`, states that for any type `N` with decidable equality and any element `i` of type `N`, if a pair `(t₀, t)` is such that `t₀` is either 0 or 1, or `t` is on the boundary of the cube `{ j // j ≠ i }`, then the image of `(t₀, t)` under the homeomorphism `Cube.insertAt i` is on the boundary of the cube `N`. In simple terms, it says that the boundary of a lower-dimensional cube maps to the boundary of a higher-dimensional cube under a certain homeomorphism.
More concisely: If `i` is an element of type `N` and `(t₀, t)` is either `(0, t)`, `(1, t)`, or `t` is on the boundary of the cube `{ j // j ≠ i }`, then `Cube.insertAt i (t₀, t)` is a boundary point of `N`.
|