English
Given a bicomplex K with total complex, totalDesc constructs a morphism from the total complex (K.total c12).X i12 to an object A from a chosen family of maps f: (i1,i2) ↦ (K.X i1).X i2 → A that are compatible with the total structure.
Русский
Для бикомплекса K с общим комплексом totalDesc строит морфизм из общего комплекса (K.total c12).X i12 в объект A, заданный семейством отображений f: (K.X i1).X i2 → A, совместимым с общей структурой.
LaTeX
$$$\text{totalDesc} = K.toGradedObject.descMapObj (c_1 \;\pi\; c_2 \; c_{12}) \, (\lambda \langle i_1,i_2\rangle. f i_1 i_2 \;\text{ hi})$$$
Lean4
/-- Given a bicomplex `K`, this is a constructor for morphisms from `(K.total c₁₂).X i₁₂`. -/
noncomputable def totalDesc : (K.total c₁₂).X i₁₂ ⟶ A :=
K.toGradedObject.descMapObj _ (fun ⟨i₁, i₂⟩ hi => f i₁ i₂ hi)
