equivSubZero — Mathlib

English

Equivalence expresses that two morphisms are homotopic iff their difference is homotopic to zero: Homotopy φ1 φ2 ≃ Homotopy (φ1−φ2) 0.

Русский

Эквивалентность выражает, что две морфизмы гомотопны тогда и только тогда, когда их разность гомотопна к нулю.

LaTeX

$$$\mathrm{Homotopy}(\varphi_1,\varphi_2) \simeq \mathrm{Homotopy}(\varphi_1-\varphi_2,0)$$$

Lean4

/-- Equivalence expressing that two morphisms are homotopic iff
their difference is homotopic to zero. -/
@[simps]
def equivSubZero : Homotopy φ₁ φ₂ ≃ Homotopy (φ₁ - φ₂) 0
    where
  toFun h := (h.sub (refl φ₂)).trans (ofEq (sub_self φ₂))
  invFun h := ((ofEq (sub_add_cancel φ₁ φ₂).symm).trans (h.add (refl φ₂))).trans (ofEq (zero_add φ₂))
  left_inv := by cat_disch
  right_inv := by cat_disch

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