Commit 2024-11-30 00:03 e1064d2a

View on Github →

feat(Algebra/Homology): more duality results (#19559) Given an homological complex K, we introduce duality isomorphisms like cyclesOpIso : K.op.cycles i ≅ op (K.opcycles i) and study their naturality.

Estimated changes

Modified Mathlib/Algebra/Homology/Opposite.lean

added def HomologicalComplex.cyclesOpIso

added theorem HomologicalComplex.cyclesOpIso_hom_naturality

added theorem HomologicalComplex.cyclesOpIso_inv_naturality

added def HomologicalComplex.cyclesOpNatIso

added theorem HomologicalComplex.fromOpcycles_op_cyclesOpIso_inv

added def HomologicalComplex.homologyOpNatIso

added theorem HomologicalComplex.homologyOp_hom_naturality

added def HomologicalComplex.opcyclesOpIso

added theorem HomologicalComplex.opcyclesOpIso_hom_naturality

added theorem HomologicalComplex.opcyclesOpIso_hom_toCycles_op

added theorem HomologicalComplex.opcyclesOpIso_inv_naturality

added def HomologicalComplex.opcyclesOpNatIso

Modified Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean

added theorem HomologicalComplex.fromOpcycles_eq_zero

added theorem HomologicalComplex.toCycles_eq_zero

Modified Mathlib/Algebra/Homology/ShortComplex/Homology.lean

added theorem CategoryTheory.ShortComplex.homologyOpIso_hom_naturality

added theorem CategoryTheory.ShortComplex.homologyOpIso_inv_naturality

Modified Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean

added theorem CategoryTheory.ShortComplex.cyclesOpIso_hom_naturality

added theorem CategoryTheory.ShortComplex.cyclesOpIso_inv_naturality

added theorem CategoryTheory.ShortComplex.cyclesOpIso_inv_op_iCycles

added theorem CategoryTheory.ShortComplex.fromOpcycles_op_cyclesOpIso_inv

added theorem CategoryTheory.ShortComplex.op_pOpcycles_opcyclesOpIso_hom

added theorem CategoryTheory.ShortComplex.opcyclesOpIso_hom_naturality

added theorem CategoryTheory.ShortComplex.opcyclesOpIso_hom_toCycles_op

added theorem CategoryTheory.ShortComplex.opcyclesOpIso_inv_naturality