Documentation Verification Report

Orthogonal

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

Statistics

Metric	Count
Definitions `leftOrthogonal`, `rightOrthogonal`	2
Theorems `instContainsZeroLeftOrthogonalOfHasZeroObject`, `instContainsZeroRightOrthogonalOfHasZeroObject`, `instIsClosedUnderIsomorphismsLeftOrthogonal`, `instIsClosedUnderIsomorphismsRightOrthogonal`, `leftOrthogonal_iff`, `rightOrthogonal_iff`	6
Total	8

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
`leftOrthogonal` 📖	CompOp	9 math math: `instIsTriangulatedLeftOrthogonalOfIsStableUnderShiftInt`, `isColocal_trW`, `instIsTriangulatedClosed₂LeftOrthogonal`, `CochainComplex.IsKProjective.leftOrthogonal`, `CochainComplex.isKProjective_iff_leftOrthogonal`, `instIsStableUnderShiftLeftOrthogonal`, `instContainsZeroLeftOrthogonalOfHasZeroObject`, `instIsClosedUnderIsomorphismsLeftOrthogonal`, `leftOrthogonal_iff`
`rightOrthogonal` 📖	CompOp	9 math math: `instContainsZeroRightOrthogonalOfHasZeroObject`, `CochainComplex.IsKInjective.rightOrthogonal`, `instIsStableUnderShiftRightOrthogonal`, `instIsTriangulatedClosed₂RightOrthogonal`, `instIsClosedUnderIsomorphismsRightOrthogonal`, `instIsTriangulatedRightOrthogonalOfIsStableUnderShiftInt`, `rightOrthogonal_iff`, `CochainComplex.isKInjective_iff_rightOrthogonal`, `isLocal_trW`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instContainsZeroLeftOrthogonalOfHasZeroObject` 📖	mathematical	—	`ContainsZero` `leftOrthogonal`	—	`CategoryTheory.Limits.isZero_zero` `CategoryTheory.Limits.HasZeroObject.from_zero_ext`
`instContainsZeroRightOrthogonalOfHasZeroObject` 📖	mathematical	—	`ContainsZero` `rightOrthogonal`	—	`CategoryTheory.Limits.isZero_zero` `CategoryTheory.Limits.HasZeroObject.to_zero_ext`
`instIsClosedUnderIsomorphismsLeftOrthogonal` 📖	mathematical	—	`IsClosedUnderIsomorphisms` `leftOrthogonal`	—	`CategoryTheory.cancel_epi` `CategoryTheory.epi_of_strongEpi` `CategoryTheory.strongEpi_of_isIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Limits.comp_zero`
`instIsClosedUnderIsomorphismsRightOrthogonal` 📖	mathematical	—	`IsClosedUnderIsomorphisms` `rightOrthogonal`	—	`CategoryTheory.cancel_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.strongMono_of_isIso` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.Limits.zero_comp`
`leftOrthogonal_iff` 📖	mathematical	—	`leftOrthogonal` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	—
`rightOrthogonal_iff` 📖	mathematical	—	`rightOrthogonal` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	—

---

← Back to Index