trianglehMapOfHomotopy — Mathlib

English

The triangle map between φ and itself is the identity in the homotopy/triangulated context.

Русский

Карта треугольника между φ и φ есть тождество в гомотопическом/триангульном контексте.

LaTeX

$$$triangle φ \\to triangle φ = id$$$

Lean4

/-- The morphism `triangleh φ₁ ⟶ triangleh φ₂` that is induced by a square that
is commutative up to homotopy. -/
@[simps]
noncomputable def trianglehMapOfHomotopy : triangleh φ₁ ⟶ triangleh φ₂
    where
  hom₁ := (HomotopyCategory.quotient _ _).map a
  hom₂ := (HomotopyCategory.quotient _ _).map b
  hom₃ := (HomotopyCategory.quotient _ _).map (mapOfHomotopy H)
  comm₁ := by
    dsimp
    simp only [← Functor.map_comp]
    exact HomotopyCategory.eq_of_homotopy _ _ H
  comm₂ := by
    dsimp
    simp only [← Functor.map_comp, triangleMapOfHomotopy_comm₂]
  comm₃ := by
    dsimp
    rw [← Functor.map_comp_assoc, triangleMapOfHomotopy_comm₃, Functor.map_comp, assoc, assoc]
    simp

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