d₁_mapMap — Mathlib

English

The differential d1 commutes with the map on the graded object level up to the differential in the target.

Русский

Дифференциал d1 коммутирует с отображением на уровне градуированного объекта с поправкой на дифференциал в целевом объекте.

LaTeX

$$$K.d_1 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_1 c_{12} i_1 i_2 i_{12}$$$

Lean4

@[reassoc (attr := simp)]
theorem d₁_mapMap (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) :
    K.d₁ c₁₂ i₁ i₂ i₁₂ ≫ GradedObject.mapMap (toGradedObjectMap φ) _ i₁₂ = (φ.f i₁).f i₂ ≫ L.d₁ c₁₂ i₁ i₂ i₁₂ :=
  by
  by_cases h : c₁.Rel i₁ (c₁.next i₁)
  · simp [totalAux.d₁_eq' _ c₁₂ h]
  · simp [d₁_eq_zero _ c₁₂ i₁ i₂ i₁₂ h]

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