ι_D₂ — Mathlib

English

Inclusion after applying the second differential equals the second differential applied to the inclusion target.

Русский

Включение после применения второго дифференциала равно второму дифференциалу, применённому к цели включения.

LaTeX

$$$\\iotaTotal c_{12} i_1 i_2 i_{12} h \\circ D_2 c_{12} i_{12} i_{12}' = d_2 c_{12} i_1 i_2 i_{12}'$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_D₂ (i₁₂ i₁₂' : I₁₂) (i₁ : I₁) (i₂ : I₂) (h : ComplexShape.π c₁ c₂ c₁₂ ⟨i₁, i₂⟩ = i₁₂) :
    K.ιTotal c₁₂ i₁ i₂ i₁₂ h ≫ K.D₂ c₁₂ i₁₂ i₁₂' = K.d₂ c₁₂ i₁ i₂ i₁₂' := by apply totalAux.ιMapObj_D₂

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