mapMap_D₂ — Mathlib

English

The d2-mapMap compatibility statement: the differential d2 commutes with the graded map on the target side.

Русский

Совместимость d2 с отображением в градаированном объекте на целевом боку: d2 совместим с mapMap.

LaTeX

$$$K.d_2 c_{12} i_1 i_2 i_{12} \\; \\circ \\; \\mathrm{mapMap} (toGradedObjectMap\\; \\varphi) _ i_{12} = (\\varphi.f i_1).f i_2 \\circ L.d_2 c_{12} i_1 i_2 i_{12}$$$

Lean4

@[reassoc]
theorem mapMap_D₂ (i₁₂ i₁₂' : I₁₂) :
    GradedObject.mapMap (toGradedObjectMap φ) _ i₁₂ ≫ L.D₂ c₁₂ i₁₂ i₁₂' =
      K.D₂ c₁₂ i₁₂ i₁₂' ≫ GradedObject.mapMap (toGradedObjectMap φ) _ i₁₂' :=
  by cat_disch

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