ιTotal_map — Mathlib

English

Let K and L be double complexes in a preadditive category, and φ: K → L a morphism between them. For every triple of indices i1 ∈ I1, i2 ∈ I2, i12 ∈ I12 with the compatibility h, the totalization maps commute with φ, i.e., the square involving ιTotal and total.map φ is commutative.

Русский

Пусть K и L — двоичные комплексы в преддобавитной категории, и φ: K → L — морфизм между ними. Для любых индексов i1 ∈ I1, i2 ∈ I2, i12 ∈ I12, удовлетворяющих совместимости h, диаграмма, состоящая из ιTotal и total.map φ, приводя к L, коммутирует.

LaTeX

$$$\\forall i_1 \\in I_1, i_2 \\in I_2, i_{12} \\in I_{12},\\hspace{2pt} h: \\pi_{c_1,c_2,c_{12}}(i_1,i_2)=i_{12},\\\\ K.\\iotaTotal\\, c_{12}\\, i_1\\, i_2\\, i_{12}\\, h \\\\ \\quad \\;\\;\\;\\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; ◦ (total.map φ c_{12}).f_{i_{12}} = (φ.f_{i_1}).f_{i_2} \\;\\;\\\\ \\;\\;\\;\\; \\;\\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; \\; L.ιTotal c_{12} i_1 i_2 i_{12} h.$$$

Lean4

@[reassoc (attr := simp)]
theorem ιTotal_map (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) (h : ComplexShape.π c₁ c₂ c₁₂ (i₁, i₂) = i₁₂) :
    K.ιTotal c₁₂ i₁ i₂ i₁₂ h ≫ (total.map φ c₁₂).f i₁₂ = (φ.f i₁).f i₂ ≫ L.ιTotal c₁₂ i₁ i₂ i₁₂ h := by
  simp [total.map, ιTotal]

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