Commit 2023-07-20 08:16 cf06ef75

View on Github →

feat: left and right homology data are dual notions (#5674) This PR shows that left and right homology data of short complexes are dual notions.

Estimated changes

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

added def CategoryTheory.ShortComplex.LeftHomologyData.op

added theorem CategoryTheory.ShortComplex.LeftHomologyData.op_g'

added def CategoryTheory.ShortComplex.LeftHomologyData.unop

added theorem CategoryTheory.ShortComplex.LeftHomologyData.unop_g'

added def CategoryTheory.ShortComplex.RightHomologyData.op

added theorem CategoryTheory.ShortComplex.RightHomologyData.op_f'

added def CategoryTheory.ShortComplex.RightHomologyData.unop

added theorem CategoryTheory.ShortComplex.RightHomologyData.unop_f'

added def CategoryTheory.ShortComplex.RightHomologyMapData.comp

added theorem CategoryTheory.ShortComplex.RightHomologyMapData.congr_φH

added theorem CategoryTheory.ShortComplex.RightHomologyMapData.congr_φQ

added def CategoryTheory.ShortComplex.RightHomologyMapData.id

added def CategoryTheory.ShortComplex.RightHomologyMapData.zero

added structure CategoryTheory.ShortComplex.RightHomologyMapData

added theorem CategoryTheory.ShortComplex.hasLeftHomology_iff_op

added theorem CategoryTheory.ShortComplex.hasLeftHomology_iff_unop

added theorem CategoryTheory.ShortComplex.hasRightHomology_iff_op

added theorem CategoryTheory.ShortComplex.hasRightHomology_iff_unop

Modified Mathlib/CategoryTheory/Limits/Opposites.lean

added def CategoryTheory.Limits.CokernelCofork.IsColimit.ofπOp

added def CategoryTheory.Limits.CokernelCofork.IsColimit.ofπUnop

added def CategoryTheory.Limits.KernelFork.IsLimit.ofιOp

added def CategoryTheory.Limits.KernelFork.IsLimit.ofιUnop

Modified Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean

added theorem CategoryTheory.Limits.op_zero

added theorem CategoryTheory.Limits.unop_zero

Modified Mathlib/CategoryTheory/Preadditive/Opposite.lean

deleted theorem CategoryTheory.op_zero

deleted theorem CategoryTheory.unop_zero