Evaluating concatenations and reversals of generalized loops

Mathlib's GenLoop.transAt i f g concatenates two generalized loops along the i-th cube direction, running f on tᵢ ≤ 1/2 and g on tᵢ ≥ 1/2, each at double speed. Its defining formula clamps the rescaled coordinate with Set.projIcc. This file states the two halves of that formula without the clamp: on each half, the concatenation is f or g evaluated at the point whose i-th coordinate is replaced by any a with the rescaled value. It also evaluates the reversal GenLoop.symmAt i f, and reads Mathlib's HomotopyGroup.mul_spec, HomotopyGroup.inv_spec and HomotopyGroup.one_def in the additive group Additive (HomotopyGroup N X x).

Main declarations

• GenLoop.transAt_apply_of_le: on the first half, transAt i f g runs f at double speed.
• GenLoop.transAt_apply_of_lt: on the second half, transAt i f g runs g at double speed.
• GenLoop.symmAt_apply: symmAt i f runs f backwards in the i-th direction.
• HomotopyGroup.ofMul_transAt, HomotopyGroup.ofMul_symmAt and HomotopyGroup.ofMul_const: concatenation, reversal and the constant loop in Additive (HomotopyGroup N X x).

theorem GenLoop.transAt_apply_of_le {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) (f g : ↑(GenLoop N X x)) {t : N → ↑unitInterval} (h : ↑(t i) ≤ 1 / 2) {a : ↑unitInterval} (ha : ↑a = 2 * ↑(t i)) : (transAt i f g) t = f (Function.update t i a)

On the first half of the i-th direction, transAt i f g runs f at double speed.

theorem GenLoop.transAt_apply_of_lt {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) (f g : ↑(GenLoop N X x)) {t : N → ↑unitInterval} (h : 1 / 2 < ↑(t i)) {a : ↑unitInterval} (ha : ↑a = 2 * ↑(t i) - 1) : (transAt i f g) t = g (Function.update t i a)

On the second half of the i-th direction, transAt i f g runs g at double speed.

@[simp]

theorem GenLoop.symmAt_apply {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] (i : N) (f : ↑(GenLoop N X x)) (t : N → ↑unitInterval) : (symmAt i f) t = f (Function.update t i (unitInterval.symm (t i)))

symmAt i f runs f backwards in the i-th direction.

@[simp]

theorem HomotopyGroup.ofMul_transAt {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] [Nonempty N] (i : N) (p q : ↑(GenLoop N X x)) : Additive.ofMul ⟦GenLoop.transAt i p q⟧ = Additive.ofMul ⟦q⟧ + Additive.ofMul ⟦p⟧

Concatenation in the i-th direction is addition in Additive (HomotopyGroup N X x), with the summands in the order of HomotopyGroup.mul_spec.

@[simp]

theorem HomotopyGroup.ofMul_symmAt {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] [Nonempty N] (i : N) (p : ↑(GenLoop N X x)) : Additive.ofMul ⟦GenLoop.symmAt i p⟧ = -Additive.ofMul ⟦p⟧

Reversal in the i-th direction is negation in Additive (HomotopyGroup N X x).

theorem HomotopyGroup.ofMul_const {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] [Nonempty N] : Additive.ofMul ⟦GenLoop.const⟧ = 0

The class of the constant loop is zero in Additive (HomotopyGroup N X x).