ι_D₁ — Mathlib

English

Inclusion after applying the first differential is the same as the first differential applied to the inclusion target.

Русский

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

LaTeX

$$$\\iotaTotal c_{12} i_1 i_2 i_{12} h \\circ D_1 c_{12} i_{12} i_{12}' = d_1 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₁

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