LeanPool.WhiteheadTheorem.HomotopyGroup.ChangeBasePt

Imported Lean Pool material for LeanPool.WhiteheadTheorem.HomotopyGroup.ChangeBasePt.

structure GenLoop.LevelHomotopy {n : ℕ} {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} (f₀ : ↑(GenLoop (Fin n) X x₀)) (f₁ : ↑(GenLoop (Fin n) X x₁)) (p : Path x₀ x₁) extends (↑f₀).Homotopy ↑f₁ : Type u

A level homotopy along a path p is a continuous function H : I × (I^ Fin n) → X such that H ⟨t, y⟩ = p t for all y ∈ ∂I^n. Note: cannot extend HomotopyWith because it would require intermediate maps satisfy a predicate that does not depend on t.

• toFun : ↑unitInterval × (Fin n → ↑unitInterval) → X
• continuous_toFun : Continuous self.toFun
• map_zero_left (x : Fin n → ↑unitInterval) : self.toFun (0, x) = ↑f₀ x
• map_one_left (x : Fin n → ↑unitInterval) : self.toFun (1, x) = ↑f₁ x
• prop' (t : ↑unitInterval) (y : Fin n → ↑unitInterval) : y ∈ Cube.boundary (Fin n) → self.toFun (t, y) = p t

noncomputable def GenLoop.LevelHomotopy.reflOfGenLoopHomotopic {n : ℕ} {X : Type u} [TopologicalSpace X] {x₀ : X} {f₀ g₀ : ↑(GenLoop (Fin n) X x₀)} (H : Homotopic f₀ g₀) : LevelHomotopy f₀ g₀ (Path.refl x₀)

A level homotopy along the constant path

Equations

• GenLoop.LevelHomotopy.reflOfGenLoopHomotopic H = { toHomotopy := (Nonempty.some H).toHomotopy, prop' := ⋯ }

def GenLoop.LevelHomotopy.symm {n : ℕ} {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} {f₀ : ↑(GenLoop (Fin n) X x₀)} {f₁ : ↑(GenLoop (Fin n) X x₁)} {p : Path x₀ x₁} (L : LevelHomotopy f₀ f₁ p) : LevelHomotopy f₁ f₀ p.symm

The reverse of a level homotopy along p, as a level homotopy along the reversed path p.symm

Equations

• L.symm = { toHomotopy := L.symm, prop' := ⋯ }

noncomputable def GenLoop.LevelHomotopy.trans {n : ℕ} {X : Type u} [TopologicalSpace X] {x₀ x₁ x₂ : X} {f₀ : ↑(GenLoop (Fin n) X x₀)} {f₁ : ↑(GenLoop (Fin n) X x₁)} {f₂ : ↑(GenLoop (Fin n) X x₂)} {p : Path x₀ x₁} {q : Path x₁ x₂} (K : LevelHomotopy f₀ f₁ p) (L : LevelHomotopy f₁ f₂ q) : LevelHomotopy f₀ f₂ (p.trans q)

The concatenation of two level homotopies

Equations

• K.trans L = { toHomotopy := K.trans L.toHomotopy, prop' := ⋯ }

def GenLoop.LevelHomotopy.constLoops {n : ℕ} {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} {p : Path x₀ x₁} : LevelHomotopy const const p

A level homotopy whose intermediate maps are constant GenLoops

Equations

• One or more equations did not get rendered due to their size.

def GenLoop.LevelHomotopy.map {n : ℕ} {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] {x₀ x₁ : X} {f₀ : ↑(GenLoop (Fin n) X x₀)} {f₁ : ↑(GenLoop (Fin n) X x₁)} {p : Path x₀ x₁} (g : C(X, Y)) (L : LevelHomotopy f₀ f₁ p) : LevelHomotopy (inducedMap n x₀ g f₀) (inducedMap n x₁ g f₁) (p.map ⋯)

Given a level homotopy from f₀ to f₁, produce a level homotopy from g ∘ f₀ to g ∘ f₁.

Equations

• GenLoop.LevelHomotopy.map g L = { toHomotopy := (ContinuousMap.Homotopy.refl g).comp L.toHomotopy, prop' := ⋯ }

theorem GenLoop.homotopic_of_levelHomotopy_along_null_loop {n : ℕ} {X : Type u} [TopologicalSpace X] {x₀ : X} {f g : ↑(GenLoop (Fin n) X x₀)} {p : LoopSpace X x₀} (H : LevelHomotopy f g p) (pnull : Path.Homotopic p (Path.refl x₀)) : Homotopic f g

If f and g are GenLoops at x₀ such that there is a LevelHomotopy from f to g along a null-homotopic loop p, then f and g are homotopic as GenLoops (i.e., homotopic rel ∂I^n).

theorem GenLoop.homotopic_of_levelHomotopy_along_homotopic_paths {n : ℕ} {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} {f : ↑(GenLoop (Fin n) X x₀)} {g h : ↑(GenLoop (Fin n) X x₁)} {p q : Path x₀ x₁} (K : LevelHomotopy f g p) (L : LevelHomotopy f h q) (pq : p.Homotopic q) : Homotopic g h

Suppose f, g and h are GenLoops, K is a level homotopy from f to g along a path p, and L is a level homotopy from f to h along a path q. If p and q are homotopic as paths (i.e., rel endpoints), then g and h are homotopic as GenLoops (i.e., rel ∂I^n).

structure GenLoop.ChangeBasePt {n : ℕ} {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} (f₀ : ↑(GenLoop (Fin n) X x₀)) (p : Path x₀ x₁) : Type u

ChangeBasePt

• res : ↑(GenLoop (Fin n) X x₁)

  res

• levelHomotopy : LevelHomotopy f₀ self.res p

  levelHomotopy

noncomputable def GenLoop.ChangeBasePt.get {n : ℕ} {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} (f₀ : ↑(GenLoop (Fin n) X x₀)) (p : Path x₀ x₁) : ChangeBasePt f₀ p

get

Equations

• One or more equations did not get rendered due to their size.

def Topology.Homotopy.«term(_#_)» : Lean.ParserDescr

«term(_#_)»

Equations

• One or more equations did not get rendered due to their size.

def Topology.Homotopy.«term(_#~_)» : Lean.ParserDescr

«term(_#~_)»

Equations

• One or more equations did not get rendered due to their size.

theorem GenLoop.ChangeBasePt.homotopic_of_path_homotopic {n : ℕ} {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} {f₀ : ↑(GenLoop (Fin n) X x₀)} {p q : Path x₀ x₁} (pq : p.Homotopic q) : Homotopic (get f₀ p).res (get f₀ q).res

If p and q are homotopic paths (rel endpoints), then p# = q# in the sense that (p # f) and (q # f) are homotopic GenLoops for all f. See also HomotopyGroup.changeBasePt.eq_of_path_homotopic.

theorem GenLoop.ChangeBasePt.apply_const {n : ℕ} {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} {p : Path x₀ x₁} : Homotopic (get const p).res const

p# sends (the homotopy class of) the const loop at x₀ to (the homotopy class of) the const loop at x₁.

theorem GenLoop.ChangeBasePt.along_const {n : ℕ} {X : Type u} [TopologicalSpace X] {x₀ : X} {f : ↑(GenLoop (Fin n) X x₀)} : Homotopic f (get f (Path.refl x₀)).res

Changing base point along the constant path Path.refl _ does nothing.

theorem GenLoop.ChangeBasePt.along_null_path {n : ℕ} {X : Type u} [TopologicalSpace X] {x₀ : X} {f : ↑(GenLoop (Fin n) X x₀)} {p : LoopSpace X x₀} (pnull : Path.Homotopic p (Path.refl x₀)) : Homotopic f (get f p).res

Changing base point along a null-homotopic loop p does nothing.

theorem GenLoop.ChangeBasePt.trans {n : ℕ} {X : Type u} [TopologicalSpace X] {x₀ x₁ x₂ : X} {p : Path x₀ x₁} {q : Path x₁ x₂} {f : ↑(GenLoop (Fin n) X x₀)} : Homotopic (get (get f p).res q).res (get f (p.trans q)).res

(q # (p # f)) ≈ (p.trans q # f)

theorem GenLoop.ChangeBasePt.trans' {n : ℕ} {X : Type u} [TopologicalSpace X] {x₀ x₁ x₂ : X} {p : Path x₀ x₁} {q : Path x₁ x₂} {r : Path x₀ x₂} {f : ↑(GenLoop (Fin n) X x₀)} (r_pq : r.Homotopic (p.trans q)) : Homotopic (get (get f p).res q).res (get f r).res

(q # (p # f)) ≈ (r # f) if r ≈ p.trans q.

theorem GenLoop.map_changeBasePt_homotopic_changeBasePt_map {n : ℕ} {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] {x₀ x₁ : X} {p : Path x₀ x₁} {α : ↑(GenLoop (Fin n) X x₀)} (f : C(X, Y)) : Homotopic (inducedMap n x₁ f (ChangeBasePt.get α p).res) (ChangeBasePt.get (inducedMap n x₀ f α) (p.map ⋯)).res

ChangeBasePt commutes with the induced map, up to homotopy:

Ω^ (Fin n) X x₀  ------ f* ---->  Ω^ (Fin n) Y (f x₀)
      |                                    |
      p#                                (f ∘ p)#
      |                                    |
      v                                    v
Ω^ (Fin n) X x₁  ------ f* ---->  Ω^ (Fin n) Y (f x₁)

See also HomotopyGroup.map_changeBasePt_eq_changeBasePt_map.

noncomputable def HomotopyGroup.changeBasePt {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} (n : ℕ) (p : Path x₀ x₁) : Pi n X x₀ → Pi n X x₁

Transport an element of π_ n X (p 0) along the path p.

Equations

• HomotopyGroup.changeBasePt n p = Quotient.map (fun (f₀ : ↑(GenLoop (Fin n) X x₀)) => (GenLoop.ChangeBasePt.get f₀ p).res) ⋯

noncomputable def FundamentalGroupoid.changeBasePt {X : Type u} [TopologicalSpace X] (n : ℕ) : CategoryTheory.Functor (FundamentalGroupoid X) Pointed

changeBasePt

Equations

• One or more equations did not get rendered due to their size.

instance FundamentalGroupoid.isIso_changeBasePt_map {n : ℕ} {X : Type u} [TopologicalSpace X] {x₀ x₁ : FundamentalGroupoid X} (p : x₀ ⟶ x₁) : CategoryTheory.IsIso ((changeBasePt n).map p)

theorem HomotopyGroup.changeBasePt_eq_of_path_homotopic {n : ℕ} {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} {p q : Path x₀ x₁} (pq : p.Homotopic q) : changeBasePt n p = changeBasePt n q

If p and q are homotopic paths (rel endpoints), then p# and q# are equal as maps from π_ n X x₀ to π_ n X x₁. See also GenLoop.ChangeBasePt.homotopic_of_path_homotopic.

@[reducible, inline]

noncomputable abbrev HomotopyGroup.pointedHomOfPath {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} (n : ℕ) (p : Path x₀ x₁) : Pointed.of default ⟶ Pointed.of default

Change of base point along the path p, as a morphism $F(·, x₀)_{#} : π_n(X, f(x₀)) → π_n(Y, g(x₀))$ in the category Pointed

Equations

• HomotopyGroup.pointedHomOfPath n p = { toFun := HomotopyGroup.changeBasePt n p, map_point := ⋯ }

instance HomotopyGroup.isIso_pointedHomOfPath {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} (n : ℕ) (p : Path x₀ x₁) : CategoryTheory.IsIso (pointedHomOfPath n p)

theorem HomotopyGroup.bijective_changeBasePt {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} (n : ℕ) (p : Path x₀ x₁) : Function.Bijective (changeBasePt n p)

theorem HomotopyGroup.pointedHomOfPath_inducedPointedHom_eq_inducedPointedHom_pointedHomOfPath {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] {x₀ x₁ : X} (n : ℕ) (p : Path x₀ x₁) (f : C(X, Y)) : CategoryTheory.CategoryStruct.comp (pointedHomOfPath n p) (inducedPointedHom n x₁ f) = CategoryTheory.CategoryStruct.comp (inducedPointedHom n x₀ f) (pointedHomOfPath n (p.map ⋯))

ChangeBasePt commutes with the induced map:

π_ n X x₀  ------ f* ---->  π_ n Y (f x₀)
    |                            |
    p#                        (f ∘ p)#
    |                            |
    v                            v
π_ n X x₁  ------ f* ---->  π_ n Y (f x₁)

See also GenLoop.map_changeBasePt_homotopic_changeBasePt_map.

theorem HomotopyGroup.inducedPointedHom_eq_of_path {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] {x₀ x₁ : X} (n : ℕ) (p : Path x₀ x₁) (f : C(X, Y)) : inducedPointedHom n x₀ f = CategoryTheory.CategoryStruct.comp (pointedHomOfPath n p) (CategoryTheory.CategoryStruct.comp (inducedPointedHom n x₁ f) (CategoryTheory.inv (pointedHomOfPath n (p.map ⋯))))

theorem HomotopyGroup.inducedPointedHom_comp_pointedHomOfHomotopy_eq {X : Type u} [TopologicalSpace X] (n : ℕ) (x₀ : X) {f g : C(X, X)} (F : f.Homotopy g) : CategoryTheory.CategoryStruct.comp (inducedPointedHom n x₀ f) (pointedHomOfPath n (F.evalAt x₀)) = inducedPointedHom n x₀ g

theorem HomotopyGroup.injective_toFun_surjective_invFun_of_homotopyEquiv {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (n : ℕ) (x₀ : X) (E : ContinuousMap.HomotopyEquiv X Y) : Function.Injective (inducedPointedHom n x₀ E.toFun).toFun ∧ Function.Surjective (inducedPointedHom n (E.toFun x₀) E.invFun).toFun

theorem HomotopyGroup.isIso_inducedPointedHom_of_isHomotopyEquiv {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (n : ℕ) (x₀ : X) (f : C(X, Y)) (hf : IsHomotopyEquiv f) : CategoryTheory.IsIso (inducedPointedHom n x₀ f)

theorem HomotopyGroup.isIso_inducedPointedHom'_of_isHomotopyEquiv (n : ℕ) {X Y : TopCat} (x₀ : ↑X) (f : X ⟶ Y) (hf : IsHomotopyEquiv (TopCat.Hom.hom f)) : CategoryTheory.IsIso (inducedPointedHom' n x₀ f)

theorem HomotopyGroup.isIso_inducedPointedHom'_of_isHomeomorph (n : ℕ) {X Y : TopCat} (x₀ : ↑X) (f : X ⟶ Y) (hf : IsHomeomorph ⇑(TopCat.Hom.hom f)) : CategoryTheory.IsIso (inducedPointedHom' n x₀ f)