Documentation Verification Report

BifunctorFlip

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

Statistics

Metric	Count
Definitions `mapBifunctorFlipIso`	1
Theorems `hasMapBifunctor_flip_iff`, `instHasMapBifunctorFlip`, `mapBifunctorFlipIso_flip`, `mapBifunctorFlipIso_hom_naturality`, `mapBifunctorFlipIso_hom_naturality_assoc`, `ι_mapBifunctorFlipIso_hom`, `ι_mapBifunctorFlipIso_hom_assoc`, `ι_mapBifunctorFlipIso_inv`, `ι_mapBifunctorFlipIso_inv_assoc`	9
Total	10

HomologicalComplex

Definitions

Name	Category	Theorems
`mapBifunctorFlipIso` 📖	CompOp	7 math math: `mapBifunctorFlipIso_hom_naturality_assoc`, `ι_mapBifunctorFlipIso_inv_assoc`, `mapBifunctorFlipIso_hom_naturality`, `mapBifunctorFlipIso_flip`, `ι_mapBifunctorFlipIso_hom`, `ι_mapBifunctorFlipIso_hom_assoc`, `ι_mapBifunctorFlipIso_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasMapBifunctor_flip_iff` 📖	mathematical	`CategoryTheory.Functor.PreservesZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category`	`HasMapBifunctor` `CategoryTheory.Functor.flip` `CategoryTheory.Functor.instPreservesZeroMorphismsFlipOfObj` `CategoryTheory.Functor.instPreservesZeroMorphismsObjFlip`	—	`HomologicalComplex₂.flip_hasTotal_iff`
`instHasMapBifunctorFlip` 📖	mathematical	`CategoryTheory.Functor.PreservesZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `HasMapBifunctor`	`CategoryTheory.Functor.flip` `CategoryTheory.Functor.instPreservesZeroMorphismsFlipOfObj` `CategoryTheory.Functor.instPreservesZeroMorphismsObjFlip`	—	`CategoryTheory.Functor.instPreservesZeroMorphismsFlipOfObj` `CategoryTheory.Functor.instPreservesZeroMorphismsObjFlip` `hasMapBifunctor_flip_iff`
`mapBifunctorFlipIso_flip` 📖	mathematical	`CategoryTheory.Functor.PreservesZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `HasMapBifunctor`	`mapBifunctorFlipIso` `CategoryTheory.Functor.flip` `CategoryTheory.Functor.instPreservesZeroMorphismsFlipOfObj` `CategoryTheory.Functor.instPreservesZeroMorphismsObjFlip` `instHasMapBifunctorFlip` `CategoryTheory.Iso.symm` `HomologicalComplex` `instCategory` `mapBifunctor`	—	`HomologicalComplex₂.flip_totalFlipIso`
`mapBifunctorFlipIso_hom_naturality` 📖	mathematical	`CategoryTheory.Functor.PreservesZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `HasMapBifunctor`	`CategoryTheory.CategoryStruct.comp` `HomologicalComplex` `CategoryTheory.Category.toCategoryStruct` `instCategory` `mapBifunctor` `CategoryTheory.Functor.flip` `CategoryTheory.Functor.instPreservesZeroMorphismsFlipOfObj` `CategoryTheory.Functor.instPreservesZeroMorphismsObjFlip` `instHasMapBifunctorFlip` `mapBifunctorMap` `CategoryTheory.Iso.hom` `mapBifunctorFlipIso`	—	`hom_ext` `CategoryTheory.Functor.instPreservesZeroMorphismsFlipOfObj` `CategoryTheory.Functor.instPreservesZeroMorphismsObjFlip` `instHasMapBifunctorFlip` `mapBifunctor.hom_ext` `ι_mapBifunctorMap_assoc` `ι_mapBifunctorFlipIso_hom` `CategoryTheory.Linear.comp_units_smul` `CategoryTheory.NatTrans.naturality_assoc` `ι_mapBifunctorFlipIso_hom_assoc` `CategoryTheory.Linear.units_smul_comp` `ι_mapBifunctorMap`
`mapBifunctorFlipIso_hom_naturality_assoc` 📖	mathematical	`CategoryTheory.Functor.PreservesZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `HasMapBifunctor`	`CategoryTheory.CategoryStruct.comp` `HomologicalComplex` `CategoryTheory.Category.toCategoryStruct` `instCategory` `mapBifunctor` `CategoryTheory.Functor.flip` `CategoryTheory.Functor.instPreservesZeroMorphismsFlipOfObj` `CategoryTheory.Functor.instPreservesZeroMorphismsObjFlip` `instHasMapBifunctorFlip` `mapBifunctorMap` `CategoryTheory.Iso.hom` `mapBifunctorFlipIso`	—	`CategoryTheory.Functor.instPreservesZeroMorphismsFlipOfObj` `CategoryTheory.Functor.instPreservesZeroMorphismsObjFlip` `instHasMapBifunctorFlip` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `mapBifunctorFlipIso_hom_naturality`
`ι_mapBifunctorFlipIso_hom` 📖	mathematical	`CategoryTheory.Functor.PreservesZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `HasMapBifunctor` `ComplexShape.π`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.flip` `X` `mapBifunctor` `CategoryTheory.Functor.instPreservesZeroMorphismsFlipOfObj` `CategoryTheory.Functor.instPreservesZeroMorphismsObjFlip` `instHasMapBifunctorFlip` `ιMapBifunctor` `Hom.f` `CategoryTheory.Iso.hom` `HomologicalComplex` `instCategory` `mapBifunctorFlipIso` `Units` `Int.instMonoid` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `Units.instSMul` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `ComplexShape.σ`	—	`HomologicalComplex₂.ιTotal_totalFlipIso_f_hom`
`ι_mapBifunctorFlipIso_hom_assoc` 📖	mathematical	`CategoryTheory.Functor.PreservesZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `HasMapBifunctor` `ComplexShape.π`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.flip` `X` `mapBifunctor` `CategoryTheory.Functor.instPreservesZeroMorphismsFlipOfObj` `CategoryTheory.Functor.instPreservesZeroMorphismsObjFlip` `instHasMapBifunctorFlip` `ιMapBifunctor` `Hom.f` `CategoryTheory.Iso.hom` `HomologicalComplex` `instCategory` `mapBifunctorFlipIso` `Units` `Int.instMonoid` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `Units.instSMul` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `ComplexShape.σ`	—	`CategoryTheory.Functor.instPreservesZeroMorphismsFlipOfObj` `CategoryTheory.Functor.instPreservesZeroMorphismsObjFlip` `instHasMapBifunctorFlip` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ι_mapBifunctorFlipIso_hom`
`ι_mapBifunctorFlipIso_inv` 📖	mathematical	`CategoryTheory.Functor.PreservesZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `HasMapBifunctor` `ComplexShape.π`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `X` `mapBifunctor` `CategoryTheory.Functor.flip` `CategoryTheory.Functor.instPreservesZeroMorphismsFlipOfObj` `CategoryTheory.Functor.instPreservesZeroMorphismsObjFlip` `instHasMapBifunctorFlip` `ιMapBifunctor` `Hom.f` `CategoryTheory.Iso.inv` `HomologicalComplex` `instCategory` `mapBifunctorFlipIso` `Units` `Int.instMonoid` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `Units.instSMul` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `ComplexShape.σ`	—	`HomologicalComplex₂.ιTotal_totalFlipIso_f_inv`
`ι_mapBifunctorFlipIso_inv_assoc` 📖	mathematical	`CategoryTheory.Functor.PreservesZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `HasMapBifunctor` `ComplexShape.π`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `X` `mapBifunctor` `ιMapBifunctor` `CategoryTheory.Functor.flip` `CategoryTheory.Functor.instPreservesZeroMorphismsFlipOfObj` `CategoryTheory.Functor.instPreservesZeroMorphismsObjFlip` `instHasMapBifunctorFlip` `Hom.f` `CategoryTheory.Iso.inv` `HomologicalComplex` `instCategory` `mapBifunctorFlipIso` `Units` `Int.instMonoid` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `Units.instSMul` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `ComplexShape.σ`	—	`CategoryTheory.Functor.instPreservesZeroMorphismsFlipOfObj` `CategoryTheory.Functor.instPreservesZeroMorphismsObjFlip` `instHasMapBifunctorFlip` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ι_mapBifunctorFlipIso_inv`

---

← Back to Index