Documentation Verification Report

Opposite

📁 Source: Mathlib/CategoryTheory/Preadditive/Opposite.lean

Statistics

Metric	Count
Definitions `homSelfLinearEquivEndMulOpposite`, `instPreadditiveOpposite`, `moduleEndLeft`, `opHom`, `unopHom`	5
Theorems `leftOp_additive`, `op_additive`, `rightOp_additive`, `unop_additive`, `homSelfLinearEquivEndMulOpposite_apply`, `homSelfLinearEquivEndMulOpposite_symm_apply`, `opHom_apply`, `op_add`, `op_neg`, `op_sub`, `op_sum`, `op_zsmul`, `unopHom_apply`, `unop_add`, `unop_neg`, `unop_sub`, `unop_sum`, `unop_zsmul`	18
Total	23

CategoryTheory

Definitions

Name	Category	Theorems
`instPreadditiveOpposite` 📖	CompOp	53 math math: `opHom_apply`, `additive_yonedaObj`, `ShortComplex.Splitting.op_r`, `Pretriangulated.instIsTriangulatedOppositeOpOpEquivalence`, `ShiftedHom.opEquiv_symm_add`, `ShortComplex.Homotopy.unop_h₂`, `ShortComplex.Homotopy.op_h₀`, `AlgebraicTopology.AlternatingCofaceMapComplex.d_eq_unop_d`, `ShortComplex.Homotopy.op_h₂`, `CochainComplex.homotopyUnop_hom_eq`, `ShortComplex.Homotopy.unop_h₃`, `Pretriangulated.instIsTriangulatedOppositeOpOp`, `Pretriangulated.instIsHomologicalOppositeAddCommGrpCatObjFunctorPreadditiveYoneda`, `additive_yonedaObj'`, `Pretriangulated.op_distinguished`, `ShortComplex.Splitting.unop_r`, `unop_neg`, `Pretriangulated.mem_distTriang_op_iff`, `unop_add`, `CochainComplex.homotopyOp_hom_eq`, `unopHom_apply`, `Pretriangulated.mem_distTriang_op_iff'`, `Functor.leftOp_additive`, `Pretriangulated.Opposite.functor_isTriangulated_op`, `ShortComplex.Homotopy.op_h₃`, `op_add`, `Abelian.instAdditiveOppositeFunctorAddCommGrpCatExtFunctor`, `ShortComplex.Homotopy.unop_h₁`, `preservesHomology_preadditiveYonedaObj_of_injective`, `linearYoneda_obj_additive`, `op_sum`, `ShortComplex.Splitting.op_s`, `ShiftedHom.opEquiv'_symm_add`, `Functor.op_isTriangulated_iff`, `op_zsmul`, `ShortComplex.Homotopy.op_h₁`, `Functor.rightOp_additive`, `unop_zsmul`, `Pretriangulated.Opposite.instAdditiveOppositeShiftFunctorInt`, `op_neg`, `op_sub`, `ShortComplex.Homotopy.unop_h₀`, `HomologicalComplex.opFunctor_additive`, `Pretriangulated.Opposite.instIsTriangulatedOpposite`, `ShortComplex.Splitting.unop_s`, `Pretriangulated.preadditiveYoneda_map_distinguished`, `Pretriangulated.Opposite.rotate_distinguished_triangle`, `unop_sub`, `Functor.op_additive`, `Functor.map_distinguished_op_exact`, `HomologicalComplex.unopFunctor_additive`, `Pretriangulated.instIsTriangulatedOppositeUnopUnop`, `unop_sum`
`moduleEndLeft` 📖	CompOp	6 math math: `IsGrothendieckAbelian.GabrielPopescuAux.ι_d`, `preadditiveCoyonedaObj_map`, `Preadditive.homSelfLinearEquivEndMulOpposite_apply`, `Preadditive.homSelfLinearEquivEndMulOpposite_symm_apply`, `preadditiveCoyonedaObj_obj_isModule`, `IsGrothendieckAbelian.GabrielPopescuAux.ι_d_assoc`
`opHom` 📖	CompOp	1 math math: `opHom_apply`
`unopHom` 📖	CompOp	1 math math: `unopHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`opHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Opposite` `Quiver.opposite` `Opposite.op` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Preadditive.homGroup` `Category.opposite` `instPreadditiveOpposite` `AddMonoidHom.instFunLike` `opHom` `Quiver.Hom.op`	—	—
`op_add` 📖	mathematical	—	`Quiver.Hom.op` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Quiver.Hom` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `Preadditive.homGroup` `Opposite` `Quiver.opposite` `Opposite.op` `Category.opposite` `instPreadditiveOpposite`	—	—
`op_neg` 📖	mathematical	—	`Quiver.Hom.op` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Quiver.Hom` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Preadditive.homGroup` `Opposite` `Quiver.opposite` `Opposite.op` `Category.opposite` `instPreadditiveOpposite`	—	—
`op_sub` 📖	mathematical	—	`Quiver.Hom.op` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Quiver.Hom` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Preadditive.homGroup` `Opposite` `Quiver.opposite` `Opposite.op` `Category.opposite` `instPreadditiveOpposite`	—	—
`op_sum` 📖	mathematical	—	`Quiver.Hom.op` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Finset.sum` `Quiver.Hom` `AddCommGroup.toAddCommMonoid` `Preadditive.homGroup` `Opposite` `Quiver.opposite` `Opposite.op` `Category.opposite` `instPreadditiveOpposite`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`op_zsmul` 📖	mathematical	—	`Quiver.Hom.op` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Quiver.Hom` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Preadditive.homGroup` `Opposite` `Quiver.opposite` `Opposite.op` `Category.opposite` `instPreadditiveOpposite`	—	—
`unopHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Quiver.Hom` `Opposite` `Quiver.opposite` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Opposite.unop` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Preadditive.homGroup` `Category.opposite` `instPreadditiveOpposite` `AddMonoidHom.instFunLike` `unopHom` `Quiver.Hom.unop`	—	—
`unop_add` 📖	mathematical	—	`Quiver.Hom.unop` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Quiver.Hom` `Opposite` `Quiver.opposite` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `Preadditive.homGroup` `Category.opposite` `instPreadditiveOpposite` `Opposite.unop`	—	—
`unop_neg` 📖	mathematical	—	`Quiver.Hom.unop` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Quiver.Hom` `Opposite` `Quiver.opposite` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Preadditive.homGroup` `Category.opposite` `instPreadditiveOpposite` `Opposite.unop`	—	—
`unop_sub` 📖	mathematical	—	`Quiver.Hom.unop` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Quiver.Hom` `Opposite` `Quiver.opposite` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Preadditive.homGroup` `Category.opposite` `instPreadditiveOpposite` `Opposite.unop`	—	—
`unop_sum` 📖	mathematical	—	`Quiver.Hom.unop` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Finset.sum` `Quiver.Hom` `Opposite` `Quiver.opposite` `AddCommGroup.toAddCommMonoid` `Preadditive.homGroup` `Category.opposite` `instPreadditiveOpposite` `Opposite.unop`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`unop_zsmul` 📖	mathematical	—	`Quiver.Hom.unop` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Quiver.Hom` `Opposite` `Quiver.opposite` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Preadditive.homGroup` `Category.opposite` `instPreadditiveOpposite` `Opposite.unop`	—	—

CategoryTheory.Functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`leftOp_additive` 📖	mathematical	—	`Additive` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.instPreadditiveOpposite` `leftOp`	—	`map_add`
`op_additive` 📖	mathematical	—	`Additive` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.instPreadditiveOpposite` `op`	—	`map_add`
`rightOp_additive` 📖	mathematical	—	`Additive` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.instPreadditiveOpposite` `rightOp`	—	`map_add`
`unop_additive` 📖	mathematical	—	`Additive` `unop`	—	`map_add`

CategoryTheory.Preadditive

Definitions

Name	Category	Theorems
`homSelfLinearEquivEndMulOpposite` 📖	CompOp	2 math math: `homSelfLinearEquivEndMulOpposite_apply`, `homSelfLinearEquivEndMulOpposite_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homSelfLinearEquivEndMulOpposite_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `MulOpposite` `CategoryTheory.End` `CategoryTheory.Category.toCategoryStruct` `MulOpposite.instSemiring` `instSemiringEnd` `RingHom.id` `MulOpposite.instNonAssocSemiring` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `AddCommGroup.toAddCommMonoid` `homGroup` `MulOpposite.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingEnd` `CategoryTheory.moduleEndLeft` `MulOpposite.instModule` `Semiring.toOppositeModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `homSelfLinearEquivEndMulOpposite` `PreOpposite.op'`	—	`RingHomInvPair.ids`
`homSelfLinearEquivEndMulOpposite_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `MulOpposite` `CategoryTheory.End` `CategoryTheory.Category.toCategoryStruct` `MulOpposite.instSemiring` `instSemiringEnd` `RingHom.id` `Semiring.toNonAssocSemiring` `MulOpposite.instNonAssocSemiring` `RingHomInvPair.ids` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `MulOpposite.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingEnd` `AddCommGroup.toAddCommMonoid` `homGroup` `MulOpposite.instModule` `Semiring.toOppositeModule` `CategoryTheory.moduleEndLeft` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `homSelfLinearEquivEndMulOpposite`	—	`RingHomInvPair.ids`

---

← Back to Index