dgoEquivHomologicalComplexUnitIso

English

Symmetric extensionality lemma: if φ and φ' are morphisms from K to HomologicalComplex.double f hi, equality on i0 and i1 implies φ = φ'.

Русский

Симметричный лемм об экстенсиональности: если φ и φ' — морфизмы из K к HomologicalComplex.double f hi, равенство на i0 и i1 влечёт φ = φ'.

LaTeX

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

Lean4

/-- The unit isomorphism for `dgoEquivHomologicalComplex`.
-/
@[simps!]
def dgoEquivHomologicalComplexUnitIso :
    𝟭 (DifferentialObject ℤ (GradedObjectWithShift b V)) ≅ dgoToHomologicalComplex b V ⋙ homologicalComplexToDGO b V :=
  NatIso.ofComponents
    (fun X =>
      { hom := { f := fun i => 𝟙 (X.obj i) }
        inv := { f := fun i => 𝟙 (X.obj i) } })

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