Documentation Verification Report

CochainComplexOpposite

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

Statistics

Metric	Count
Definitions `cochainComplexEquivalence`, `homotopyOp`, `homotopyOpEquiv`, `homotopyUnop`, `opEquivalence`, `embeddingDownIntUpInt`, `embeddingUpIntDownInt`	7
Theorems `acyclic_op`, `exactAt_op`, `homotopyOp_hom_eq`, `homotopyUnop_hom_eq`, `embeddingDownIntUpInt_f`, `embeddingUpIntDownInt_f`, `instIsRelIffIntEmbeddingDownIntUpInt`, `instIsRelIffIntEmbeddingUpIntDownInt`	8
Total	15

ChainComplex

Definitions

Name	Category	Theorems
`cochainComplexEquivalence` 📖	CompOp	—

CochainComplex

Definitions

Name	Category	Theorems
`homotopyOp` 📖	CompOp	1 math math: `homotopyOp_hom_eq`
`homotopyOpEquiv` 📖	CompOp	—
`homotopyUnop` 📖	CompOp	1 math math: `homotopyUnop_hom_eq`
`opEquivalence` 📖	CompOp	4 math math: `acyclic_op`, `exactAt_op`, `homotopyUnop_hom_eq`, `homotopyOp_hom_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`acyclic_op` 📖	mathematical	`HomologicalComplex.Acyclic` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing`	`Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Limits.hasZeroMorphismsOpposite` `CategoryTheory.Functor.obj` `CochainComplex` `HomologicalComplex.instCategory` `CategoryTheory.Equivalence.functor` `opEquivalence` `Opposite.op`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `exactAt_op`
`exactAt_op` 📖	mathematical	`HomologicalComplex.ExactAt` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing`	`Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Limits.hasZeroMorphismsOpposite` `CategoryTheory.Functor.obj` `CochainComplex` `HomologicalComplex.instCategory` `CategoryTheory.Equivalence.functor` `opEquivalence` `Opposite.op`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.exactAt_iff'` `prev` `next` `CategoryTheory.ShortComplex.exact_unop_iff`
`homotopyOp_hom_eq` 📖	mathematical	—	`Homotopy.hom` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.instPreadditiveOpposite` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.Functor.obj` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomologicalComplex.instCategory` `CategoryTheory.Limits.hasZeroMorphismsOpposite` `CategoryTheory.Equivalence.functor` `opEquivalence` `Opposite.op` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `homotopyOp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.opposite` `HomologicalComplex.X` `ComplexShape.Embedding.f` `ComplexShape.down` `ComplexShape.embeddingUpIntDownInt` `CategoryTheory.Iso.hom` `HomologicalComplex.XIsoOfEq`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`homotopyUnop_hom_eq` 📖	mathematical	—	`Homotopy.hom` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `homotopyUnop` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.Embedding.f` `ComplexShape.down` `ComplexShape.embeddingUpIntDownInt` `CategoryTheory.Iso.hom` `HomologicalComplex.XIsoOfEq` `Opposite.unop` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.instPreadditiveOpposite` `CategoryTheory.Functor.obj` `CochainComplex` `HomologicalComplex.instCategory` `CategoryTheory.Limits.hasZeroMorphismsOpposite` `CategoryTheory.Equivalence.functor` `opEquivalence` `Opposite.op` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Functor.map` `Quiver.Hom.op`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `ComplexShape.instIsRelIffIntEmbeddingUpIntDownInt`

ComplexShape

Definitions

Name	Category	Theorems
`embeddingDownIntUpInt` 📖	CompOp	2 math math: `instIsRelIffIntEmbeddingDownIntUpInt`, `embeddingDownIntUpInt_f`
`embeddingUpIntDownInt` 📖	CompOp	4 math math: `embeddingUpIntDownInt_f`, `CochainComplex.homotopyUnop_hom_eq`, `CochainComplex.homotopyOp_hom_eq`, `instIsRelIffIntEmbeddingUpIntDownInt`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`embeddingDownIntUpInt_f` 📖	mathematical	—	`Embedding.f` `down` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `up` `embeddingDownIntUpInt`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`embeddingUpIntDownInt_f` 📖	mathematical	—	`Embedding.f` `up` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `down` `embeddingUpIntDownInt`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`instIsRelIffIntEmbeddingDownIntUpInt` 📖	mathematical	—	`Embedding.IsRelIff` `down` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `up` `embeddingDownIntUpInt`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`instIsRelIffIntEmbeddingUpIntDownInt` 📖	mathematical	—	`Embedding.IsRelIff` `up` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `down` `embeddingUpIntDownInt`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`

---

← Back to Index