nullHomotopicMap_eq — Mathlib

English

If a functor inverts homotopy equivalences, then it sends the two cylinder inclusions ι0K and ι1K to the same map: H.map(ι0 K) = H.map(ι1 K).

Русский

Если функтор инвертирует гомотопийные эквивалентности, то он отображает обе включения цилиндра одинаково: H.map(ι0 K) = H.map(ι1 K).

LaTeX

$$$H.map(\iota_0 K) = H.map(\iota_1 K)$$$

Lean4

theorem nullHomotopicMap_eq : nullHomotopicMap K = π K ≫ ι₀ K - 𝟙 _ :=
  by
  ext i
  by_cases hi : c.Rel i (c.next i)
  ·
    exact
      homotopyCofiber.ext_from_X (biprod.lift (𝟙 K) (-𝟙 K)) (c.next i) i hi (inlX_nullHomotopy_f _ _ _ _)
        (inrX_nullHomotopy_f _ hc _)
  · exact homotopyCofiber.ext_from_X' (biprod.lift (𝟙 K) (-𝟙 K)) _ hi (inrX_nullHomotopy_f _ hc _)

Похожие утверждения