Documentation Verification Report

Orthogonal

📁 Source: Mathlib/CategoryTheory/Triangulated/Orthogonal.lean

Statistics

Metric	Count
Definitions	0
Theorems `instIsStableUnderShiftLeftOrthogonal`, `instIsStableUnderShiftRightOrthogonal`, `instIsTriangulatedClosed₂LeftOrthogonal`, `instIsTriangulatedClosed₂RightOrthogonal`, `instIsTriangulatedLeftOrthogonalOfIsStableUnderShiftInt`, `instIsTriangulatedRightOrthogonalOfIsStableUnderShiftInt`, `isColocal_trW`, `isLocal_trW`, `map_bijective_of_isTriangulated`, `map_bijective_of_isTriangulated`	10
Total	10

CategoryTheory.ObjectProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsStableUnderShiftLeftOrthogonal` 📖	mathematical	—	`IsStableUnderShift` `leftOrthogonal` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`Equiv.surjective` `le_shift` `IsStableUnderShift.isStableUnderShiftBy` `CategoryTheory.Adjunction.homEquiv_counit` `CategoryTheory.Functor.map_zero` `CategoryTheory.Functor.preservesZeroMorphisms_of_full` `CategoryTheory.Functor.IsEquivalence.full` `CategoryTheory.instIsEquivalenceShiftFunctor` `CategoryTheory.Limits.zero_comp`
`instIsStableUnderShiftRightOrthogonal` 📖	mathematical	—	`IsStableUnderShift` `rightOrthogonal` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`Equiv.surjective` `le_shift` `IsStableUnderShift.isStableUnderShiftBy` `CategoryTheory.Adjunction.homEquiv_unit` `CategoryTheory.Functor.map_zero` `CategoryTheory.Functor.preservesZeroMorphisms_of_full` `CategoryTheory.Functor.IsEquivalence.full` `CategoryTheory.instIsEquivalenceShiftFunctor` `CategoryTheory.Limits.comp_zero`
`instIsTriangulatedClosed₂LeftOrthogonal` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`IsTriangulatedClosed₂` `leftOrthogonal` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	—	`IsTriangulatedClosed₂.mk'` `instIsClosedUnderIsomorphismsLeftOrthogonal` `CategoryTheory.Pretriangulated.Triangle.yoneda_exact₂` `CategoryTheory.Limits.comp_zero`
`instIsTriangulatedClosed₂RightOrthogonal` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`IsTriangulatedClosed₂` `rightOrthogonal` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	—	`IsTriangulatedClosed₂.mk'` `instIsClosedUnderIsomorphismsRightOrthogonal` `CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂` `CategoryTheory.Limits.zero_comp`
`instIsTriangulatedLeftOrthogonalOfIsStableUnderShiftInt` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`IsTriangulated` `leftOrthogonal` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	—	`instContainsZeroLeftOrthogonalOfHasZeroObject` `instIsStableUnderShiftLeftOrthogonal` `instIsTriangulatedClosed₂LeftOrthogonal`
`instIsTriangulatedRightOrthogonalOfIsStableUnderShiftInt` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`IsTriangulated` `rightOrthogonal` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	—	`instContainsZeroRightOrthogonalOfHasZeroObject` `instIsStableUnderShiftRightOrthogonal` `instIsTriangulatedClosed₂RightOrthogonal`
`isColocal_trW` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.MorphismProperty.isColocal` `trW` `leftOrthogonal` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	—	`Function.Bijective.injective` `CategoryTheory.Pretriangulated.contractible_distinguished₂` `le_shift` `IsStableUnderShift.isStableUnderShiftBy` `IsTriangulated.toIsStableUnderShift` `CategoryTheory.Limits.comp_zero` `trW_iff'` `CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂` `CategoryTheory.Limits.zero_comp` `CategoryTheory.Preadditive.sub_comp` `CategoryTheory.Pretriangulated.rot_of_distTriang`
`isLocal_trW` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.MorphismProperty.isLocal` `trW` `rightOrthogonal` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	—	`Function.Bijective.injective` `CategoryTheory.Pretriangulated.contractible_distinguished₁` `CategoryTheory.Limits.zero_comp` `CategoryTheory.Limits.comp_zero` `CategoryTheory.Pretriangulated.Triangle.yoneda_exact₂` `CategoryTheory.Preadditive.comp_sub` `CategoryTheory.Pretriangulated.inv_rot_of_distTriang` `le_shift` `IsStableUnderShift.isStableUnderShiftBy` `IsTriangulated.toIsStableUnderShift`

CategoryTheory.ObjectProperty.leftOrthogonal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_bijective_of_isTriangulated` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.ObjectProperty.leftOrthogonal` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	`Function.Bijective` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	—	`CategoryTheory.MorphismProperty.map_eq_iff_postcomp` `CategoryTheory.ObjectProperty.instHasLeftCalculusOfFractionsTrWOfIsTriangulatedOfIsTriangulated` `CategoryTheory.ObjectProperty.isColocal_trW` `CategoryTheory.Localization.inverts` `CategoryTheory.Localization.exists_leftFraction` `CategoryTheory.MorphismProperty.LeftFraction.hs` `CategoryTheory.cancel_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s` `CategoryTheory.Functor.map_comp`

CategoryTheory.ObjectProperty.rightOrthogonal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_bijective_of_isTriangulated` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.ObjectProperty.rightOrthogonal` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	`Function.Bijective` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	—	`CategoryTheory.MorphismProperty.map_eq_iff_precomp` `CategoryTheory.ObjectProperty.instHasRightCalculusOfFractionsTrWOfIsTriangulatedOfIsTriangulated` `CategoryTheory.ObjectProperty.isLocal_trW` `CategoryTheory.Localization.inverts` `CategoryTheory.Localization.exists_rightFraction` `CategoryTheory.MorphismProperty.RightFraction.hs` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.MorphismProperty.RightFraction.map_s_comp_map` `CategoryTheory.Functor.map_comp`

---

← Back to Index