ι_totalDesc — Mathlib

English

The inclusion of a summand into the total complex followed by the total-desc construction recovers the original component map.

Русский

Включение сумманта в суммарный комплекс, за которым следует конструктор total-desc восстанавливает исходное отображение компонента.

LaTeX

$$$K.ιTotal c_{12} i_1 i_2 i_{12} h \\;\\;\\; \\circ \\;K.totalDesc f = f i_1 i_2 h$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_totalDesc (i₁ : I₁) (i₂ : I₂) (hi : ComplexShape.π c₁ c₂ c₁₂ (i₁, i₂) = i₁₂) :
    K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ K.totalDesc f = f i₁ i₂ hi := by simp [totalDesc, ιTotal]

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