mappingConeCompHomotopyEquiv_comm₂

English

The commutativity relation for the second component of mappingConeCompHomotopyEquiv establishes a compatibility condition with the third morphism mor3 of the corresponding triangle.

Русский

Свойство совместимости второй компоненты mappingConeCompHomotopyEquiv с третьим морфизмом mor3 соответствующего треугольника.

LaTeX

$$$(\text{mappingConeCompHomotopyEquiv}(f,g).hom) \circ (\text{triangle}(\text{mappingConeCompTriangle}(f,g).mor_1).mor_3) = (\text{mappingConeCompTriangle}(f,g).mor_3)$$$

Lean4

@[reassoc]
theorem mappingConeCompHomotopyEquiv_comm₂ :
    (mappingConeCompHomotopyEquiv f g).hom ≫ (triangle (mappingConeCompTriangle f g).mor₁).mor₃ =
      (mappingConeCompTriangle f g).mor₃ :=
  by
  ext n
  simp [map, mappingConeCompHomotopyEquiv, MappingConeCompHomotopyEquiv.hom, lift_f _ _ _ _ _ (n + 1) rfl,
    ext_from_iff _ (n + 1) _ rfl]

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