Documentation Verification Report

ShortExact

📁 Source: Mathlib/Algebra/Homology/DerivedCategory/ShortExact.lean

Statistics

Metric	Count
Definitions `triangleOfSES`, `map`, `triangleOfSESIso`, `triangleOfSESδ`	4
Theorems `map_hom₁`, `map_hom₂`, `map_hom₃`, `triangleOfSES_distinguished`, `triangleOfSES_mor₁`, `triangleOfSES_mor₂`, `triangleOfSES_mor₃`, `triangleOfSES_obj₁`, `triangleOfSES_obj₂`, `triangleOfSES_obj₃`	10
Total	14

DerivedCategory

Definitions

Name	Category	Theorems
`triangleOfSES` 📖	CompOp	16 math math: `CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁`, `triangleOfSES_mor₁`, `triangleOfSES_obj₃`, `CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂`, `triangleOfSES.map_hom₁`, `CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₃`, `triangleOfSES_obj₁`, `CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃`, `CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁`, `triangleOfSES.map_hom₃`, `triangleOfSES_mor₃`, `triangleOfSES_distinguished`, `triangleOfSES.map_hom₂`, `CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂`, `triangleOfSES_obj₂`, `triangleOfSES_mor₂`
`triangleOfSESIso` 📖	CompOp	—
`triangleOfSESδ` 📖	CompOp	1 math math: `triangleOfSES_mor₃`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`triangleOfSES_distinguished` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instHasZeroMorphisms`	`CategoryTheory.Pretriangulated.Triangle` `DerivedCategory` `instCategoryDerivedCategory` `instHasShiftInt` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `instHasZeroObject` `instPreadditive` `instAdditiveShiftFunctorInt` `instPretriangulated` `triangleOfSES`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `instHasZeroObject` `instAdditiveShiftFunctorInt` `CategoryTheory.Abelian.hasBinaryBiproducts` `mem_distTriang_iff`
`triangleOfSES_mor₁` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instHasZeroMorphisms`	`CategoryTheory.Pretriangulated.Triangle.mor₁` `DerivedCategory` `instCategoryDerivedCategory` `instHasShiftInt` `triangleOfSES` `CategoryTheory.Functor.map` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `Q` `CategoryTheory.ShortComplex.X₁` `HomologicalComplex.instHasZeroMorphisms` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.ShortComplex.f`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`triangleOfSES_mor₂` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instHasZeroMorphisms`	`CategoryTheory.Pretriangulated.Triangle.mor₂` `DerivedCategory` `instCategoryDerivedCategory` `instHasShiftInt` `triangleOfSES` `CategoryTheory.Functor.map` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `Q` `CategoryTheory.ShortComplex.X₂` `HomologicalComplex.instHasZeroMorphisms` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.g`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`triangleOfSES_mor₃` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instHasZeroMorphisms`	`CategoryTheory.Pretriangulated.Triangle.mor₃` `DerivedCategory` `instCategoryDerivedCategory` `instHasShiftInt` `triangleOfSES` `triangleOfSESδ`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`triangleOfSES_obj₁` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instHasZeroMorphisms`	`CategoryTheory.Pretriangulated.Triangle.obj₁` `DerivedCategory` `instCategoryDerivedCategory` `instHasShiftInt` `triangleOfSES` `CategoryTheory.Functor.obj` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `Q` `CategoryTheory.ShortComplex.X₁` `HomologicalComplex.instHasZeroMorphisms`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`triangleOfSES_obj₂` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instHasZeroMorphisms`	`CategoryTheory.Pretriangulated.Triangle.obj₂` `DerivedCategory` `instCategoryDerivedCategory` `instHasShiftInt` `triangleOfSES` `CategoryTheory.Functor.obj` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `Q` `CategoryTheory.ShortComplex.X₂` `HomologicalComplex.instHasZeroMorphisms`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`triangleOfSES_obj₃` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instHasZeroMorphisms`	`CategoryTheory.Pretriangulated.Triangle.obj₃` `DerivedCategory` `instCategoryDerivedCategory` `instHasShiftInt` `triangleOfSES` `CategoryTheory.Functor.obj` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `Q` `CategoryTheory.ShortComplex.X₃` `HomologicalComplex.instHasZeroMorphisms`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`

DerivedCategory.triangleOfSES

Definitions

Name	Category	Theorems
`map` 📖	CompOp	3 math math: `map_hom₁`, `map_hom₃`, `map_hom₂`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_hom₁` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instHasZeroMorphisms`	`CategoryTheory.Pretriangulated.TriangleMorphism.hom₁` `DerivedCategory` `instCategoryDerivedCategory` `DerivedCategory.instHasShiftInt` `DerivedCategory.triangleOfSES` `map` `CategoryTheory.Functor.map` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `DerivedCategory.Q` `CategoryTheory.ShortComplex.X₁` `HomologicalComplex.instHasZeroMorphisms` `CategoryTheory.ShortComplex.Hom.τ₁`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`map_hom₂` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instHasZeroMorphisms`	`CategoryTheory.Pretriangulated.TriangleMorphism.hom₂` `DerivedCategory` `instCategoryDerivedCategory` `DerivedCategory.instHasShiftInt` `DerivedCategory.triangleOfSES` `map` `CategoryTheory.Functor.map` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `DerivedCategory.Q` `CategoryTheory.ShortComplex.X₂` `HomologicalComplex.instHasZeroMorphisms` `CategoryTheory.ShortComplex.Hom.τ₂`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`map_hom₃` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instHasZeroMorphisms`	`CategoryTheory.Pretriangulated.TriangleMorphism.hom₃` `DerivedCategory` `instCategoryDerivedCategory` `DerivedCategory.instHasShiftInt` `DerivedCategory.triangleOfSES` `map` `CategoryTheory.Functor.map` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `DerivedCategory.Q` `CategoryTheory.ShortComplex.X₃` `HomologicalComplex.instHasZeroMorphisms` `CategoryTheory.ShortComplex.Hom.τ₃`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`

---

← Back to Index