Documentation Verification Report

CommSq

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

Statistics

Metric	Count
Definitions `cokernelCofork`, `isColimitEquivIsColimitCokernelCofork`, `isLimitEquivIsLimitKernelFork`, `kernelFork`, `shortComplex`, `shortComplex'`, `isLimitKernelFork`, `isColimitCokernelCofork`	8
Theorems `shortComplex'_X₁`, `shortComplex'_X₂`, `shortComplex'_X₃`, `shortComplex'_f`, `shortComplex'_g`, `shortComplex_X₁`, `shortComplex_X₂`, `shortComplex_X₃`, `shortComplex_f`, `shortComplex_g`, `mono_shortComplex'_f`, `epi_shortComplex_g`	12
Total	20

CategoryTheory.CommSq

Definitions

Name	Category	Theorems
`cokernelCofork` 📖	CompOp	—
`isColimitEquivIsColimitCokernelCofork` 📖	CompOp	—
`isLimitEquivIsLimitKernelFork` 📖	CompOp	—
`kernelFork` 📖	CompOp	—
`shortComplex` 📖	CompOp	7 math math: `shortComplex_g`, `shortComplex_f`, `CategoryTheory.IsPushout.epi_shortComplex_g`, `shortComplex_X₃`, `CategoryTheory.IsPushout.exact_shortComplex`, `shortComplex_X₁`, `shortComplex_X₂`
`shortComplex'` 📖	CompOp	7 math math: `CategoryTheory.IsPullback.exact_shortComplex'`, `CategoryTheory.IsPullback.mono_shortComplex'_f`, `shortComplex'_X₁`, `shortComplex'_X₂`, `shortComplex'_g`, `shortComplex'_f`, `shortComplex'_X₃`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`shortComplex'_X₁` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.ShortComplex.X₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `shortComplex'`	—	—
`shortComplex'_X₂` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `shortComplex'` `CategoryTheory.Limits.biprod`	—	—
`shortComplex'_X₃` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.ShortComplex.X₃` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `shortComplex'`	—	—
`shortComplex'_f` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.ShortComplex.f` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `shortComplex'` `CategoryTheory.Limits.biprod.lift`	—	—
`shortComplex'_g` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.ShortComplex.g` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `shortComplex'` `CategoryTheory.Limits.biprod.desc` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `CategoryTheory.Preadditive.homGroup`	—	—
`shortComplex_X₁` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.ShortComplex.X₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `shortComplex`	—	—
`shortComplex_X₂` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `shortComplex` `CategoryTheory.Limits.biprod`	—	—
`shortComplex_X₃` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.ShortComplex.X₃` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `shortComplex`	—	—
`shortComplex_f` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.ShortComplex.f` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `shortComplex` `CategoryTheory.Limits.biprod.lift` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `CategoryTheory.Preadditive.homGroup`	—	—
`shortComplex_g` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.ShortComplex.g` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `shortComplex` `CategoryTheory.Limits.biprod.desc`	—	—

CategoryTheory.IsPullback

Definitions

Name	Category	Theorems
`isLimitKernelFork` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mono_shortComplex'_f` 📖	mathematical	`CategoryTheory.IsPullback`	`CategoryTheory.Mono` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.CommSq.shortComplex'` `toCommSq` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.ShortComplex.f`	—	`toCommSq` `CategoryTheory.Preadditive.mono_iff_cancel_zero` `CategoryTheory.Limits.Fork.IsLimit.hom_ext` `CategoryTheory.Limits.zero_comp`

CategoryTheory.IsPushout

Definitions

Name	Category	Theorems
`isColimitCokernelCofork` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi_shortComplex_g` 📖	mathematical	`CategoryTheory.IsPushout`	`CategoryTheory.Epi` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.CommSq.shortComplex` `toCommSq` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.g`	—	`toCommSq` `CategoryTheory.Preadditive.epi_iff_cancel_zero` `CategoryTheory.Limits.Cofork.IsColimit.hom_ext` `CategoryTheory.Limits.comp_zero`

---

← Back to Index