homologicalComplexToDGO — Mathlib

English

If φ and φ' are morphisms from HomologicalComplex.double f hi to K and agree on the i0 and i1 components, then φ = φ'.

Русский

Если φ и φ' — морфизмы из HomologicalComplex.double f hi в K и совпадают на компонентах i0 и i1, то они равны.

LaTeX

$$$\forall (φ φ' : HomologicalComplex.instCategory.Hom (HomologicalComplex.double f hi₀₁) K),\; φ.f i₀ = φ'.f i₀ \land φ.f i₁ = φ'.f i₁ \Rightarrow φ = φ'$$$

Lean4

/-- The functor from homological complexes to differential graded objects.
-/
@[simps]
def homologicalComplexToDGO :
    HomologicalComplex V (ComplexShape.up' b) ⥤ DifferentialObject ℤ (GradedObjectWithShift b V)
    where
  obj
    X :=
    { obj := fun i => X.X i
      d := fun i => X.d i _ }
  map {X Y} f := { f := f.f }

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