Documentation Verification Report

TotalComplexSymmetry

📁 Source: Mathlib/Algebra/Homology/TotalComplexSymmetry.lean

Statistics

Metric	Count
Definitions `totalFlipIso`, `totalFlipIsoX`	2
Theorems `flip_hasTotal_iff`, `flip_totalFlipIso`, `instHasTotalFlip`, `instHasTotalFlip_1`, `totalFlipIsoX_hom_D₁`, `totalFlipIsoX_hom_D₁_assoc`, `totalFlipIsoX_hom_D₂`, `totalFlipIsoX_hom_D₂_assoc`, `totalFlipIso_hom_f_D₁`, `totalFlipIso_hom_f_D₁_assoc`, `totalFlipIso_hom_f_D₂`, `totalFlipIso_hom_f_D₂_assoc`, `ιTotal_totalFlipIso_f_hom`, `ιTotal_totalFlipIso_f_hom_assoc`, `ιTotal_totalFlipIso_f_inv`, `ιTotal_totalFlipIso_f_inv_assoc`	16
Total	18

HomologicalComplex₂

Definitions

Name	Category	Theorems
`totalFlipIso` 📖	CompOp	9 math math: `totalFlipIso_hom_f_D₁`, `ιTotal_totalFlipIso_f_inv_assoc`, `ιTotal_totalFlipIso_f_hom_assoc`, `totalFlipIso_hom_f_D₂`, `totalFlipIso_hom_f_D₁_assoc`, `flip_totalFlipIso`, `ιTotal_totalFlipIso_f_hom`, `totalFlipIso_hom_f_D₂_assoc`, `ιTotal_totalFlipIso_f_inv`
`totalFlipIsoX` 📖	CompOp	4 math math: `totalFlipIsoX_hom_D₂_assoc`, `totalFlipIsoX_hom_D₁`, `totalFlipIsoX_hom_D₂`, `totalFlipIsoX_hom_D₁_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`flip_hasTotal_iff` 📖	mathematical	—	`HasTotal` `flip` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	—	`instHasTotalFlip`
`flip_totalFlipIso` 📖	mathematical	`HasTotal`	`totalFlipIso` `flip` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instHasTotalFlip` `CategoryTheory.Iso.symm` `HomologicalComplex` `HomologicalComplex.instCategory` `total`	—	`CategoryTheory.Iso.ext` `instHasTotalFlip` `HomologicalComplex.hom_ext` `total.hom_ext` `CategoryTheory.Iso.symm_hom` `ιTotal_totalFlipIso_f_hom` `ιTotal_totalFlipIso_f_inv` `ComplexShape.σ_symm`
`instHasTotalFlip` 📖	mathematical	`HasTotal`	`flip` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	—	`CategoryTheory.Limits.hasCoproduct_of_equiv_of_iso`
`instHasTotalFlip_1` 📖	mathematical	`HasTotal`	`flip` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	—	—
`totalFlipIsoX_hom_D₁` 📖	mathematical	`HasTotal`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `total` `flip` `instHasTotalFlip` `CategoryTheory.GradedObject.mapObj` `toGradedObject` `ComplexShape.π` `CategoryTheory.Iso.hom` `totalFlipIsoX` `D₁` `D₂`	—	`instHasTotalFlip` `total.hom_ext` `ι_totalDesc_assoc` `CategoryTheory.Linear.units_smul_comp` `ι_D₁` `ι_D₂_assoc` `ComplexShape.next_π₂` `ComplexShape.next_eq'` `ComplexShape.π_symm` `d₁_eq` `d₂_eq` `CategoryTheory.Category.assoc` `ι_totalDesc` `CategoryTheory.Linear.comp_units_smul` `smul_smul` `ComplexShape.σ_ε₁` `d₁_eq_zero` `d₂_eq_zero` `smul_zero` `CategoryTheory.Limits.zero_comp` `D₁_shape` `D₂_shape` `CategoryTheory.Limits.comp_zero`
`totalFlipIsoX_hom_D₁_assoc` 📖	mathematical	`HasTotal`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `total` `flip` `instHasTotalFlip` `CategoryTheory.Iso.hom` `totalFlipIsoX` `CategoryTheory.GradedObject.mapObj` `toGradedObject` `ComplexShape.π` `D₁` `D₂`	—	`instHasTotalFlip` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `totalFlipIsoX_hom_D₁`
`totalFlipIsoX_hom_D₂` 📖	mathematical	`HasTotal`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `total` `flip` `instHasTotalFlip` `CategoryTheory.GradedObject.mapObj` `toGradedObject` `ComplexShape.π` `CategoryTheory.Iso.hom` `totalFlipIsoX` `D₂` `D₁`	—	`instHasTotalFlip` `total.hom_ext` `ι_totalDesc_assoc` `CategoryTheory.Linear.units_smul_comp` `ι_D₂` `ι_D₁_assoc` `ComplexShape.next_π₁` `ComplexShape.next_eq'` `ComplexShape.π_symm` `d₂_eq` `d₁_eq` `CategoryTheory.Category.assoc` `ι_totalDesc` `CategoryTheory.Linear.comp_units_smul` `smul_smul` `ComplexShape.σ_ε₂` `d₂_eq_zero` `d₁_eq_zero` `smul_zero` `CategoryTheory.Limits.zero_comp` `D₂_shape` `D₁_shape` `CategoryTheory.Limits.comp_zero`
`totalFlipIsoX_hom_D₂_assoc` 📖	mathematical	`HasTotal`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `total` `flip` `instHasTotalFlip` `CategoryTheory.Iso.hom` `totalFlipIsoX` `CategoryTheory.GradedObject.mapObj` `toGradedObject` `ComplexShape.π` `D₂` `D₁`	—	`instHasTotalFlip` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `totalFlipIsoX_hom_D₂`
`totalFlipIso_hom_f_D₁` 📖	mathematical	`HasTotal`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `total` `flip` `instHasTotalFlip` `CategoryTheory.GradedObject.mapObj` `toGradedObject` `ComplexShape.π` `HomologicalComplex.Hom.f` `CategoryTheory.Iso.hom` `HomologicalComplex` `HomologicalComplex.instCategory` `totalFlipIso` `D₁` `D₂`	—	`totalFlipIsoX_hom_D₁`
`totalFlipIso_hom_f_D₁_assoc` 📖	mathematical	`HasTotal`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `total` `flip` `instHasTotalFlip` `HomologicalComplex.Hom.f` `CategoryTheory.Iso.hom` `HomologicalComplex` `HomologicalComplex.instCategory` `totalFlipIso` `CategoryTheory.GradedObject.mapObj` `toGradedObject` `ComplexShape.π` `D₁` `D₂`	—	`instHasTotalFlip` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `totalFlipIso_hom_f_D₁`
`totalFlipIso_hom_f_D₂` 📖	mathematical	`HasTotal`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `total` `flip` `instHasTotalFlip` `CategoryTheory.GradedObject.mapObj` `toGradedObject` `ComplexShape.π` `HomologicalComplex.Hom.f` `CategoryTheory.Iso.hom` `HomologicalComplex` `HomologicalComplex.instCategory` `totalFlipIso` `D₂` `D₁`	—	`totalFlipIsoX_hom_D₂`
`totalFlipIso_hom_f_D₂_assoc` 📖	mathematical	`HasTotal`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `total` `flip` `instHasTotalFlip` `HomologicalComplex.Hom.f` `CategoryTheory.Iso.hom` `HomologicalComplex` `HomologicalComplex.instCategory` `totalFlipIso` `CategoryTheory.GradedObject.mapObj` `toGradedObject` `ComplexShape.π` `D₂` `D₁`	—	`instHasTotalFlip` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `totalFlipIso_hom_f_D₂`
`ιTotal_totalFlipIso_f_hom` 📖	mathematical	`HasTotal` `ComplexShape.π`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomologicalComplex` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms` `flip` `total` `instHasTotalFlip` `ιTotal` `HomologicalComplex.Hom.f` `CategoryTheory.Iso.hom` `totalFlipIso` `Units` `Int.instMonoid` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `Units.instSMul` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `ComplexShape.σ`	—	`instHasTotalFlip` `ι_totalDesc`
`ιTotal_totalFlipIso_f_hom_assoc` 📖	mathematical	`HasTotal` `ComplexShape.π`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomologicalComplex` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms` `flip` `total` `instHasTotalFlip` `ιTotal` `HomologicalComplex.Hom.f` `CategoryTheory.Iso.hom` `totalFlipIso` `Units` `Int.instMonoid` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `Units.instSMul` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `ComplexShape.σ`	—	`instHasTotalFlip` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ιTotal_totalFlipIso_f_hom`
`ιTotal_totalFlipIso_f_inv` 📖	mathematical	`HasTotal` `ComplexShape.π`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomologicalComplex` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms` `total` `flip` `instHasTotalFlip` `ιTotal` `HomologicalComplex.Hom.f` `CategoryTheory.Iso.inv` `totalFlipIso` `Units` `Int.instMonoid` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `Units.instSMul` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `ComplexShape.σ`	—	`instHasTotalFlip` `ι_totalDesc`
`ιTotal_totalFlipIso_f_inv_assoc` 📖	mathematical	`HasTotal` `ComplexShape.π`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomologicalComplex` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms` `total` `ιTotal` `flip` `instHasTotalFlip` `HomologicalComplex.Hom.f` `CategoryTheory.Iso.inv` `totalFlipIso` `Units` `Int.instMonoid` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `Units.instSMul` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `ComplexShape.σ`	—	`instHasTotalFlip` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ιTotal_totalFlipIso_f_inv`

---

← Back to Index