ofGradedObject_toGradedObject — Mathlib

English

If one builds a bicomplex from a graded object X via ofGradedObject and then takes its associated graded object, one recovers X.

Русский

Если построить биокамплекс из градуированного объекта X с помощью ofGradedObject и затем взять соответствующий градуированный объект, то восстанавливается X.

LaTeX

$$$\big(\mathrm{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)\big).toGradedObject = X$$$

Lean4

@[simp]
theorem ofGradedObject_toGradedObject :
    (ofGradedObject c₁ c₂ X d₁ d₂ shape₁ shape₂ d₁_comp_d₁ d₂_comp_d₂ comm).toGradedObject = X :=
  rfl

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