LeanPool.WhiteheadTheorem.RelHomotopyGroup.Compression #
Imported Lean Pool material for LeanPool.WhiteheadTheorem.RelHomotopyGroup.Compression.
theorem
RelHomotopyGroup.compression_criterion_1
(n : ℕ)
(X : Type u_1)
[TopologicalSpace X]
(A : Set X)
(a : ↑A)
(f : ↑(RelGenLoop (n + 1) X A a))
(g : C(Fin (n + 1) → ↑unitInterval, X))
(rg : Set.range ⇑g ⊆ A)
(H : (↑f).HomotopyRel g (Cube.boundary (Fin (n + 1))))
:
For n ≥ 1, if ⟦f⟧ ∈ π_rel n X A a and f is homotopic rel ∂I^n to a map g
whose image is in A, then f represents zero in the relative homotopy group.
theorem
RelHomotopyGroup.compression_criterion_1_subtype
(n : ℕ)
(X : Type u_1)
[TopologicalSpace X]
(A : Set X)
(a : ↑A)
(f : ↑(RelGenLoop (n + 1) X A a))
(g : C(Fin (n + 1) → ↑unitInterval, ↑A))
(H : (↑f).HomotopyRel { toFun := Subtype.val ∘ ⇑g, continuous_toFun := ⋯ } (Cube.boundary (Fin (n + 1))))
:
Same as compression_criterion_1, except that the codomain of g is explicitly A.
theorem
RelHomotopyGroup.compression_criterion_2
(n : ℕ)
(X : Type u_1)
[TopologicalSpace X]
(A : Set X)
(a : ↑A)
(f : ↑(RelGenLoop n X A a))
(fz : ⟦f⟧ = ⟦RelGenLoop.const⟧)
:
∃ (g : C(Fin n → ↑unitInterval, X)), Set.range ⇑g ⊆ A ∧ (↑f).HomotopicRel g (Cube.boundary (Fin n))
If f represents zero in the relative homotopy group π_rel n X A a,
then f is homotopic rel ∂I^n to some map g whose image is in A.
theorem
RelHomotopyGroup.compression_criterion_2_subtype
(n : ℕ)
(X : Type u_1)
[TopologicalSpace X]
(A : Set X)
(a : ↑A)
(f : ↑(RelGenLoop n X A a))
(fz : ⟦f⟧ = ⟦RelGenLoop.const⟧)
:
∃ (g : C(Fin n → ↑unitInterval, ↑A)),
(↑f).HomotopicRel { toFun := Subtype.val ∘ ⇑g, continuous_toFun := ⋯ } (Cube.boundary (Fin n))
Same as compression_criterion_2, except that the codomain of g is explicitly A.