totalFlipIso_hom_f_D₁ — Mathlib

English

The composite relations involving totalFlipIsoX and totalFlipIsoX_hom_f_hom and their associativity properties verify the expected compatibilities of the total flipping with the first and second differentials.

Русский

Сложение отношений, в которых участвуют totalFlipIsoX и связанные гомоморфизмы, и их ассоциативность подтверждают ожидаемую совместимость разворота полного комплекса с первыми и вторыми дифференциалами.

LaTeX

$$$((K.totalFlipIsoX C y).hom \; \text{comp} \; K.D_1 c j j') = (K.flip.D_2 c j j') \; \circ \; (K.totalFlipIsoX c j').hom$$$

Lean4

@[reassoc]
theorem totalFlipIso_hom_f_D₁ (j j' : J) :
    (K.totalFlipIso c).hom.f j ≫ K.D₁ c j j' = K.flip.D₂ c j j' ≫ (K.totalFlipIso c).hom.f j' := by
  apply totalFlipIsoX_hom_D₁

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