English
Construct a bicomplex from a graded object X with horizontal differentials d1 and vertical differentials d2 satisfying the usual shape, nilpotence, and commutativity relations. The data (X, d1, d2, shape1, shape2, d1_comp_d1, d2_comp_d2, comm) determine a HomologicalComplex₂ C c1 c2.
Русский
С помощью данных градуированного объекта X и горизонтальных дифференциалов d1 и вертикальных дифференциалов d2, удовлетворяющих нормам формы, нулевого квадрата и коммутативности, задаётся биокомплекс.
LaTeX
$$$\text{ofGradedObject}: (c_1,c_2,X,d_1,d_2,shape_1,shape_2,d_1\_comp\_d\_1,d_2\_comp\_d\_2,comm) \mapsto \mathrm{HomologicalComplex}_2(C;c_1,c_2)$$$
Lean4
/-- Constructor for bicomplexes taking as inputs a graded object, horizontal differentials
and vertical differentials satisfying suitable relations. -/
@[simps]
def ofGradedObject : HomologicalComplex₂ C c₁ c₂
where
X
i₁ :=
{ X := fun i₂ => X ⟨i₁, i₂⟩
d := fun i₂ i₂' => d₂ i₁ i₂ i₂'
shape := shape₂ i₁
d_comp_d' := by intros; apply d₂_comp_d₂ }
d i₁
i₁' :=
{ f := fun i₂ => d₁ i₁ i₁' i₂
comm' := by intros; apply comm }
shape i₁ i₁'
h := by
ext i₂
exact shape₁ i₁ i₁' h i₂
d_comp_d' i₁ i₁' i₁'' _ _ := by ext i₂; apply d₁_comp_d₁
