hasRightHomology_iff_unop — Mathlib

English

For S : ShortComplex Cᵒᵖ, S.HasRightHomology is equivalent to S.unop.HasLeftHomology.

Русский

Для S в категории Cᵒᵖ правая гомология эквивалентна левой гомологии у S.unop.

LaTeX

$$$ HasRightHomology(S^{\mathrm{op}}) \iff HasLeftHomology(S^{\mathrm{unop}}) $$$

Lean4

theorem hasRightHomology_iff_unop (S : ShortComplex Cᵒᵖ) : S.HasRightHomology ↔ S.unop.HasLeftHomology :=
  S.unop.hasLeftHomology_iff_op.symm

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