LeanPool.WhiteheadTheorem.RelHomotopyGroup.Defs

Imported Lean Pool material for LeanPool.WhiteheadTheorem.RelHomotopyGroup.Defs.

def RelGenLoop (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) (a : ↑A) : Set C(Fin n → ↑unitInterval, X)

relative generalized loops

Equations

• RelGenLoop n X A a = {f : C(Fin n → ↑unitInterval, X) | (∀ y ∈ Cube.boundary (Fin n), f y ∈ A) ∧ ∀ y ∈ Cube.boundaryJar n, f y = ↑a}

def RelGenLoop.const {n : ℕ} {X : Type u_1} [TopologicalSpace X] {A : Set X} {a : ↑A} : ↑(RelGenLoop n X A a)

The constant RelGenLoop at a.

Equations

• RelGenLoop.const = ⟨ContinuousMap.const (Fin n → ↑unitInterval) ↑a, ⋯⟩

@[implicit_reducible]

instance RelGenLoop.inhabited {n : ℕ} {X : Type u_1} [TopologicalSpace X] {A : Set X} {a : ↑A} : Inhabited ↑(RelGenLoop n X A a)

Equations

• RelGenLoop.inhabited = { default := RelGenLoop.const }

@[reducible, inline]

abbrev RelGenLoop.Homotopic {n : ℕ} {X : Type u_1} [TopologicalSpace X] {A : Set X} {a : ↑A} (f g : ↑(RelGenLoop n X A a)) : Prop

A homotopy between two relative generalized loops. The intermediate maps of the homotopy always send ∂I^n into A ⊆ X and ⊔I^n to a ∈ A.

Equations

• RelGenLoop.Homotopic f g = (↑f).HomotopicWith ↑g fun (f : C(Fin n → ↑unitInterval, X)) => f ∈ RelGenLoop n X A a

theorem RelGenLoop.mem_of_boundaryLid_and_boundaryJar {n : ℕ} {X : Type u_1} [TopologicalSpace X] {A : Set X} {a : ↑A} (f : C(Fin n → ↑unitInterval, X)) (hlid : ∀ y ∈ Cube.boundaryLid n, f y ∈ A) (hjar : ∀ y ∈ Cube.boundaryJar n, f y = ↑a) : f ∈ RelGenLoop n X A a

For a continuous function f to be a RelGenLoop, it suffices to show that f send the top face into A ⊆ X and ⊔I^n to a ∈ A. Note: this lemma does not work in dimension 0.

theorem RelGenLoop.Homotopic.refl {n : ℕ} {X : Type u_1} [TopologicalSpace X] {A : Set X} {a : ↑A} {f : ↑(RelGenLoop n X A a)} : Homotopic f f

theorem RelGenLoop.Homotopic.symm {n : ℕ} {X : Type u_1} [TopologicalSpace X] {A : Set X} {a : ↑A} {f g : ↑(RelGenLoop n X A a)} (H : Homotopic f g) : Homotopic g f

theorem RelGenLoop.Homotopic.trans {n : ℕ} {X : Type u_1} [TopologicalSpace X] {A : Set X} {a : ↑A} {f g h : ↑(RelGenLoop n X A a)} (H : Homotopic f g) (G : Homotopic g h) : Homotopic f h

theorem RelGenLoop.Homotopic.equiv {n : ℕ} {X : Type u_1} [TopologicalSpace X] {A : Set X} {a : ↑A} : Equivalence Homotopic

RelGenLoop.Homotopic is an equivalence relationship.

@[implicit_reducible]

instance RelGenLoop.Homotopic.setoid (n : ℕ) (X : Type u_2) [TopologicalSpace X] (A : Set X) (a : ↑A) : Setoid ↑(RelGenLoop n X A a)

Equations

• RelGenLoop.Homotopic.setoid n X A a = { r := RelGenLoop.Homotopic, iseqv := ⋯ }

def RelGenLoop.equivGenLoop (X : Type u_2) [TopologicalSpace X] (A : Set X) (a : ↑A) : ↑(RelGenLoop 0 X A a) ≃ ↑(GenLoop (Fin 0) X ↑a)

The 0-dimensional relative generalized loops based at a are in bijection with the 0-dimensional generalized loops based at a.

Equations

• RelGenLoop.equivGenLoop X A a = { toFun := fun (f : ↑(RelGenLoop 0 X A a)) => ⟨↑f, ⋯⟩, invFun := fun (f : ↑(GenLoop (Fin 0) X ↑a)) => ⟨↑f, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

def RelHomotopyGroup (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) (a : ↑A) : Type u_1

We have defined relative homotopy "groups" as mere sets. The group structure is not needed for the Whitehead theorem.

Equations

• RelHomotopyGroup n X A a = Quotient (RelGenLoop.Homotopic.setoid n X A a)

def Topology.termπ_rel : Lean.ParserDescr

«termπ_rel»

Equations

• Topology.termπ_rel = Lean.ParserDescr.node `Topology.termπ_rel 1024 (Lean.ParserDescr.symbol "π_rel")

@[implicit_reducible]

instance RelHomotopyGroup.inhabited {n : ℕ} {X : Type u_1} [TopologicalSpace X] {A : Set X} {a : ↑A} : Inhabited (RelHomotopyGroup n X A a)

Equations

• RelHomotopyGroup.inhabited = { default := RelHomotopyGroup.inhabited._aux_1 }

def RelHomotopyGroup.equivPi0 (X : Type u_1) [TopologicalSpace X] (A : Set X) (a : ↑A) : RelHomotopyGroup 0 X A a ≃ HomotopyGroup.Pi 0 X ↑a

The 0-th relative homotopy "group" π₀(X, A, a) is in bijection with the 0-th homotopy "group" π₀(X, a).

Equations

• RelHomotopyGroup.equivPi0 X A a = Quotient.congr (RelGenLoop.equivGenLoop X A a) ⋯

def RelHomotopyGroup.iStar' (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) (a : ↑A) (f : ↑(GenLoop (Fin n) (↑A) a)) : HomotopyGroup.Pi n X ↑a

iStar'

Equations

• RelHomotopyGroup.iStar' n X A a f = ⟦⟨{ toFun := Subtype.val ∘ ⇑↑f, continuous_toFun := ⋯ }, ⋯⟩⟧

def RelHomotopyGroup.iStar (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) (a : ↑A) : HomotopyGroup.Pi n (↑A) a → HomotopyGroup.Pi n X ↑a

The inclusion map $i_*$ (of pointed sets) from πₙ(A, a) to πₙ(X, a)

Equations

• RelHomotopyGroup.iStar n X A a = Quotient.lift (RelHomotopyGroup.iStar' n X A a) ⋯

def RelHomotopyGroup.jStar' (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) (a : ↑A) (f : ↑(GenLoop (Fin n) X ↑a)) : RelHomotopyGroup n X A a

jStar'

Equations

• RelHomotopyGroup.jStar' n X A a f = ⟦⟨↑f, ⋯⟩⟧

def RelHomotopyGroup.jStar (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) (a : ↑A) : HomotopyGroup.Pi n X ↑a → RelHomotopyGroup n X A a

The inclusion map $j_*$ (of pointed sets) from πₙ(A, a) to πₙ(X, A, a)

Equations

• RelHomotopyGroup.jStar n X A a = Quotient.lift (RelHomotopyGroup.jStar' n X A a) ⋯

def RelHomotopyGroup.bd' (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) (a : ↑A) (f : ↑(RelGenLoop (n + 1) X A a)) : HomotopyGroup.Pi n (↑A) a

Restrict f : C(I^ Fin (n + 1), X) to the top face (where the last coordinate equals 1).

Equations

• RelHomotopyGroup.bd' n X A a f = ⟦⟨{ toFun := fun (y : Fin n → ↑unitInterval) => ⟨(⇑↑f ∘ ⇑Cube.inclToTop) y, ⋯⟩, continuous_toFun := ⋯ }, ⋯⟩⟧

def RelHomotopyGroup.bd (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) (a : ↑A) : RelHomotopyGroup (n + 1) X A a → HomotopyGroup.Pi n (↑A) a

The boundary map $∂$ (of pointed sets) from πₙ₊₁(X, A, a) to πₙ(A, a)

Equations

• RelHomotopyGroup.bd n X A a = Quotient.lift (RelHomotopyGroup.bd' n X A a) ⋯

The induced maps iStar, jStar, and bd preserve the distinguished point, i.e., they map (the homotopy class of) the constant loop to the constant loop.

instance RelHomotopyGroup.iStar_isPointedMap (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) (a : ↑A) : IsPointedMap (iStar n X A a)

instance RelHomotopyGroup.jStar_isPointedMap (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) (a : ↑A) : IsPointedMap (jStar n X A a)

instance RelHomotopyGroup.bd_isPointedMap (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) (a : ↑A) : IsPointedMap (bd n X A a)

Some useful lemmas for the compression_criterion

def RelGenLoop.ofHomotopyRel {n : ℕ} {X : Type u_2} [TopologicalSpace X] {A : Set X} {a : ↑A} (f : ↑(RelGenLoop n X A a)) (g : C(Fin n → ↑unitInterval, X)) (H : (↑f).HomotopyRel g (Cube.boundary (Fin n))) : ↑(RelGenLoop n X A a)

Let g be a continuous function from I^ Fin n to X. If g is homotopic rel ∂I^n to some f : RelGenLoop n X A a, then g itself can be regarded as a RelGenLoop.

Equations

• RelGenLoop.ofHomotopyRel f g H = ⟨g, ⋯⟩

theorem RelGenLoop.ofHomotopyRel.eq {n : ℕ} {X : Type u_1} [TopologicalSpace X] {A : Set X} {a : ↑A} (f : ↑(RelGenLoop n X A a)) (g : C(Fin n → ↑unitInterval, X)) (H : (↑f).HomotopyRel g (Cube.boundary (Fin n))) : ⟦f⟧ = ⟦ofHomotopyRel f g H⟧