totalFlipIso_hom_f_D₂ — Mathlib

English

Similarly, in the total-flip construction, the hom component of the totalFlipIso commutes with the D2 differential: (K.totalFlipIso c).hom.f j ≫ K.D2 c j j' = K.flip.D1 c j j' ≫ (K.totalFlipIso c).hom.f j'.

Русский

Аналогично: компонентом гомоморфизма в totalFlipIso удовлетворяется commutativity с D2.

LaTeX

$$$(K.totalFlipIso c).hom.f j \; \circ\; K.D_2 c j j' = K.flip.D_1 c j j' \circ (K.totalFlipIso c).hom.f j'$$$

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₂

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