LeanPool.WhiteheadTheorem.RelHomotopyGroup.LongExactSeq

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

theorem RelHomotopyGroup.ker_jStar_supset_im_iStar (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) (a : ↑A) (f : HomotopyGroup.Pi (n + 1) X ↑a) : (∃ (g : HomotopyGroup.Pi (n + 1) (↑A) a), iStar (n + 1) X A a g = f) → jStar (n + 1) X A a f = default

Ker j* ⊇ Im i* (for n ≥ 1) in ⋯ πₙ(A, a) ---i*ₙ---> πₙ(X, a) ---j*ₙ---> πₙ(X, A, a) ⋯

The long exact sequences ends with π₁(X, A, a) ---∂--> π₀(A, a) ---i*--> π₀(X, a). It is possible to extend the sequence to ⋯ π₀(X, a) ---j*--> π₀(X, A, a) -----> 0 by re-defining π₀(X, A, a) as the quotient of π₀(X, a) by the set i*(π₀(X, a)), i.e., π₀(X, A, a) would be in bijection with the quotient of the path components of X by those path components that intersect with A.

But this extension is not implemented in this Whitehead theorem project.

reference: https://math.stackexchange.com/questions/1302389/meaning-of-n-connected-pairs

theorem RelHomotopyGroup.ker_jStar_subset_im_iStar (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) (a : ↑A) (f : HomotopyGroup.Pi n X ↑a) : jStar n X A a f = default → ∃ (g : HomotopyGroup.Pi n (↑A) a), iStar n X A a g = f

Ker j* ⊆ Im i* in ⋯ πₙ(A, a) ---i*ₙ---> πₙ(X, a) ---j*ₙ---> πₙ(X, A, a) ⋯

theorem RelHomotopyGroup.isExactAt_iStar_jStar (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) (a : ↑A) : ExactSeq.IsExactAt (iStar (n + 1) X A a) (jStar (n + 1) X A a)

Ker j* = Im i* (for n ≥ 1) in ⋯ πₙ(A, a) ---i*ₙ---> πₙ(X, a) ---j*ₙ---> πₙ(X, A, a) ⋯

theorem RelHomotopyGroup.ker_bd_supset_im_jStar (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) (a : ↑A) (f : RelHomotopyGroup (n + 1) X A a) : (∃ (g : HomotopyGroup.Pi (n + 1) X ↑a), jStar (n + 1) X A a g = f) → bd n X A a f = default

Ker ∂ ⊇ Im j* in ⋯ πₙ₊₁(X, a) ---j*ₙ---> πₙ₊₁(X, A, a) ---∂ₙ---> πₙ(A, a) ⋯

noncomputable def RelHomotopyGroup.kerBdSubsetImJStar.g'' (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) (a : ↑A) (f' : ↑(RelGenLoop (n + 1) X A a)) (hf0 : bd' n X A a f' = ⟦GenLoop.const⟧) : C(↑unitInterval × (Fin n → ↑unitInterval), X)

g'' (yₙ, (y₀, y₁, …, yₙ₋₁)) = if yₙ ≤ 1/2 then f' (y₀, y₁, …, yₙ₋₁, 2 * yₙ) else H (2 * yₙ - 1, (y₀, y₁, …, yₙ₋₁))

Equations

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

noncomputable def RelHomotopyGroup.kerBdSubsetImJStar.g' (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) (a : ↑A) (f' : ↑(RelGenLoop (n + 1) X A a)) (hf0 : bd' n X A a f' = ⟦GenLoop.const⟧) : ↑(GenLoop (Fin (n + 1)) X ↑a)

g'' is an element of Ω^ (Fin (n+1)) X a, i.e., it sends the boundary to a.

Equations

• RelHomotopyGroup.kerBdSubsetImJStar.g' n X A a f' hf0 = ⟨(RelHomotopyGroup.kerBdSubsetImJStar.g'' n X A a f' hf0).comp ↑Cube.splitAtLast, ⋯⟩

noncomputable def RelHomotopyGroup.kerBdSubsetImJStar.G'' (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) (a : ↑A) (f' : ↑(RelGenLoop (n + 1) X A a)) (hf0 : bd' n X A a f' = ⟦GenLoop.const⟧) : C(↑unitInterval × ↑unitInterval × (Fin n → ↑unitInterval), X)

G'' (t, (yₙ, (y₀, y₁, …, yₙ₋₁))) = if yₙ ≤ (1 + t) / 2 then f' (y₀, y₁, …, yₙ₋₁, (2 / (1 + t)) * yₙ) else H (2 * yₙ - (1 + t), (y₀, y₁, …, yₙ₋₁))

Equations

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

theorem RelHomotopyGroup.kerBdSubsetImJStar (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) (a : ↑A) (f : RelHomotopyGroup (n + 1) X A a) : bd n X A a f = default → ∃ (g : HomotopyGroup.Pi (n + 1) X ↑a), jStar (n + 1) X A a g = f

Ker ∂ ⊆ Im j* in ⋯ πₙ₊₁(X, a) ---j*ₙ---> πₙ₊₁(X, A, a) ---∂ₙ---> πₙ(A, a) ⋯

theorem RelHomotopyGroup.isExactAt_jStar_bd (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) (a : ↑A) : ExactSeq.IsExactAt (jStar (n + 1) X A a) (bd n X A a)

Ker ∂ = Im j* in ⋯ πₙ₊₁(X, a) ---j*ₙ---> πₙ₊₁(X, A, a) ---∂ₙ---> πₙ(A, a) ⋯

theorem RelHomotopyGroup.ker_iStar_supset_im_bd (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) (a : ↑A) (f : HomotopyGroup.Pi n (↑A) a) : (∃ (g : RelHomotopyGroup (n + 1) X A a), bd n X A a g = f) → iStar n X A a f = default

Ker i* ⊇ Im ∂ in ⋯ πₙ₊₁(X, A, a) ---∂ₙ---> πₙ(A, a) ---i*ₙ--> πₙ(X, a) ⋯

theorem RelHomotopyGroup.ker_iStar_subset_im_bd (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) (a : ↑A) (f : HomotopyGroup.Pi n (↑A) a) : iStar n X A a f = default → ∃ (g : RelHomotopyGroup (n + 1) X A a), bd n X A a g = f

Ker i* ⊆ Im ∂ in ⋯ πₙ₊₁(X, A, a) ---∂ₙ---> πₙ(A, a) ---i*ₙ--> πₙ(X, a) ⋯

theorem RelHomotopyGroup.isExactAt_bd_iStar (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) (a : ↑A) : ExactSeq.IsExactAt (bd n X A a) (iStar n X A a)

Ker i* = Im ∂ in ⋯ πₙ₊₁(X, A, a) ---∂ₙ---> πₙ(A, a) ---i*ₙ--> πₙ(X, a) ⋯

theorem RelHomotopyGroup.unique_relHomotopyGroup_of_bijective_iStar {X : TopCat} {A : Set ↑X} (a : ↑A) (hbi : ∀ (n : ℕ), Function.Bijective (iStar n (↑X) A a)) (n : ℕ) : Nonempty (Unique (RelHomotopyGroup (n + 1) (↑X) A a))