LoopTracks.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TorsionFreeZeroDivisors.LoopTracks.pathOfHomotopy line 15
Source documentation
A genuine relative path homotopy is a path in the compact-open path space.
```
def pathOfHomotopy {p q : Path x y} (H : p.Homotopy q) : Path p q where
…
```
def OAI.TorsionFreeZeroDivisors.LoopTracks.homotopyOfPath line 21
Source documentation
Conversely: no quotient or merely formal track is used here.
```
def homotopyOfPath {p q : Path x y} (h : Path p q) : p.Homotopy q where
…
```
lemma OAI.TorsionFreeZeroDivisors.LoopTracks.homotopic_iff_joined line 27
def OAI.TorsionFreeZeroDivisors.LoopTracks.piOneHomeo line 32
def OAI.TorsionFreeZeroDivisors.LoopTracks.uniqueLoopHomeo line 52
lemma OAI.TorsionFreeZeroDivisors.LoopTracks.loopGroup_comm line 65
Source documentation
The loop-space fundamental group is genuinely commutative (Eckmann-Hilton). This is the coefficient group of two-cell homotopy-extension obstructions.
```
lemma loopGroup_comm (x : X) : ∀a b : FundamentalGroup (Path x x) (Path.refl x), a*b=b*a := by
…
```