Documentation Verification Report

Dimension

📁 Source: Mathlib/CategoryTheory/Abelian/Projective/Dimension.lean

Statistics

Metric	Count
Definitions `HasProjectiveDimensionLE`, `HasProjectiveDimensionLT`, `projectiveDimension`	3
Theorems `eq_zero_of_hasProjectiveDimensionLT`, `mk`, `subsingleton`, `subsingleton'`, `hasProjectiveDimensionLT_zero`, `hasProjectiveDimensionLT`, `projectiveDimension_le`, `hasProjectiveDimensionLT_X₁`, `hasProjectiveDimensionLT_X₂`, `hasProjectiveDimensionLT_X₃`, `hasProjectiveDimensionLT_X₃_iff`, `hasProjectiveDimensionLT_iff`, `hasProjectiveDimensionLT_of_ge`, `hasProjectiveDimensionLT_of_iso`, `hasProjectiveDimensionLT_zero_iff_isZero`, `instHasProjectiveDimensionLTBiprod`, `instHasProjectiveDimensionLTHAddNat`, `instHasProjectiveDimensionLTHAddNat_1`, `instHasProjectiveDimensionLTOfNatNat`, `instHasProjectiveDimensionLTOfNatNatOfProjective`, `instHasProjectiveDimensionLTSucc`, `isZero_of_hasProjectiveDimensionLT_zero`, `projectiveDimension_eq_bot_iff`, `projectiveDimension_eq_of_iso`, `projectiveDimension_ge_iff`, `projectiveDimension_le_iff`, `projectiveDimension_lt_iff`, `projectiveDimension_ne_top_iff`, `projective_iff_hasProjectiveDimensionLT_one`, `projective_iff_subsingleton_ext_one`	30
Total	33

CategoryTheory

Definitions

Name	Category	Theorems
`HasProjectiveDimensionLE` 📖	MathDef	2 math math: `projectiveDimension_ne_top_iff`, `projectiveDimension_le_iff`
`HasProjectiveDimensionLT` 📖	CompData	20 math math: `instHasProjectiveDimensionLTOfNatNat`, `ShortComplex.ShortExact.hasProjectiveDimensionLT_X₁`, `instHasProjectiveDimensionLTHAddNat_1`, `Limits.IsZero.hasProjectiveDimensionLT_zero`, `ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃_iff`, `hasProjectiveDimensionLT_of_ge`, `instHasProjectiveDimensionLTHAddNat`, `instHasProjectiveDimensionLTOfNatNatOfProjective`, `projectiveDimension_lt_iff`, `instHasProjectiveDimensionLTSucc`, `projectiveDimension_ge_iff`, `instHasProjectiveDimensionLTBiprod`, `ShortComplex.ShortExact.hasProjectiveDimensionLT_X₂`, `ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃`, `HasProjectiveDimensionLT.mk`, `hasProjectiveDimensionLT_zero_iff_isZero`, `hasProjectiveDimensionLT_iff`, `hasProjectiveDimensionLT_of_iso`, `Retract.hasProjectiveDimensionLT`, `projective_iff_hasProjectiveDimensionLT_one`
`projectiveDimension` 📖	CompOp	6 math math: `projectiveDimension_lt_iff`, `projectiveDimension_eq_of_iso`, `projectiveDimension_le_iff`, `projectiveDimension_ge_iff`, `projectiveDimension_eq_bot_iff`, `Retract.projectiveDimension_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasProjectiveDimensionLT_iff` 📖	mathematical	`HasExt`	`HasProjectiveDimensionLT` `Abelian.Ext` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Abelian.Ext.instAddCommGroup`	—	`Abelian.Ext.eq_zero_of_hasProjectiveDimensionLT`
`hasProjectiveDimensionLT_of_ge` 📖	mathematical	—	`HasProjectiveDimensionLT`	—	`HasExt.standard` `hasProjectiveDimensionLT_iff` `Abelian.Ext.eq_zero_of_hasProjectiveDimensionLT`
`hasProjectiveDimensionLT_of_iso` 📖	mathematical	—	`HasProjectiveDimensionLT`	—	`Retract.hasProjectiveDimensionLT`
`hasProjectiveDimensionLT_zero_iff_isZero` 📖	mathematical	—	`HasProjectiveDimensionLT` `Limits.IsZero`	—	`isZero_of_hasProjectiveDimensionLT_zero` `Limits.IsZero.hasProjectiveDimensionLT_zero`
`instHasProjectiveDimensionLTBiprod` 📖	mathematical	—	`HasProjectiveDimensionLT` `Limits.biprod` `Preadditive.preadditiveHasZeroMorphisms` `Abelian.toPreadditive` `Limits.HasBinaryBiproducts.has_binary_biproduct` `Abelian.hasBinaryBiproducts`	—	`ShortComplex.ShortExact.hasProjectiveDimensionLT_X₂` `Limits.HasBinaryBiproducts.has_binary_biproduct` `Abelian.hasBinaryBiproducts` `ShortComplex.Splitting.shortExact` `Abelian.hasZeroObject`
`instHasProjectiveDimensionLTHAddNat` 📖	mathematical	—	`HasProjectiveDimensionLT`	—	`hasProjectiveDimensionLT_of_ge`
`instHasProjectiveDimensionLTHAddNat_1` 📖	mathematical	—	`HasProjectiveDimensionLT`	—	`hasProjectiveDimensionLT_of_ge`
`instHasProjectiveDimensionLTOfNatNat` 📖	mathematical	—	`HasProjectiveDimensionLT` `Limits.HasZeroObject.zero'` `Abelian.hasZeroObject`	—	`Limits.IsZero.hasProjectiveDimensionLT_zero` `Abelian.hasZeroObject` `Limits.isZero_zero`
`instHasProjectiveDimensionLTOfNatNatOfProjective` 📖	mathematical	—	`HasProjectiveDimensionLT`	—	`HasExt.standard` `hasProjectiveDimensionLT_iff` `Nat.instCanonicallyOrderedAdd` `Abelian.Ext.eq_zero_of_projective`
`instHasProjectiveDimensionLTSucc` 📖	mathematical	—	`HasProjectiveDimensionLT`	—	`instHasProjectiveDimensionLTHAddNat`
`isZero_of_hasProjectiveDimensionLT_zero` 📖	mathematical	—	`Limits.IsZero`	—	`Limits.IsZero.iff_id_eq_zero` `Equiv.injective` `HasExt.standard` `Abelian.Ext.mk₀_zero` `Abelian.Ext.eq_zero_of_hasProjectiveDimensionLT` `le_refl`
`projectiveDimension_eq_bot_iff` 📖	mathematical	—	`projectiveDimension` `Bot.bot` `WithBot` `ENat` `WithBot.bot` `Limits.IsZero`	—	`hasProjectiveDimensionLT_zero_iff_isZero` `projectiveDimension_lt_iff` `Nat.cast_zero` `WithBot.lt_coe_bot` `bot_eq_zero'` `WithBot.coe_zero`
`projectiveDimension_eq_of_iso` 📖	mathematical	—	`projectiveDimension`	—	`hasProjectiveDimensionLT_of_iso`
`projectiveDimension_ge_iff` 📖	mathematical	—	`WithBot` `ENat` `Preorder.toLE` `WithBot.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `projectiveDimension` `HasProjectiveDimensionLT`	—	`Mathlib.Tactic.Contrapose.contrapose_iff₃` `projectiveDimension_lt_iff`
`projectiveDimension_le_iff` 📖	mathematical	—	`WithBot` `ENat` `Preorder.toLE` `WithBot.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `projectiveDimension` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `HasProjectiveDimensionLE`	—	`Nat.cast_add` `Nat.cast_one`
`projectiveDimension_lt_iff` 📖	mathematical	—	`WithBot` `ENat` `Preorder.toLT` `WithBot.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `projectiveDimension` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `HasProjectiveDimensionLT`	—	`csInf_mem` `WithBot.instWellFoundedLT` `instIsEmptyFalse` `sInf_lt_iff` `hasProjectiveDimensionLT_of_ge` `Nat.instCanonicallyOrderedAdd` `Nat.instNoMaxOrder` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `IsOrderedRing.toZeroLEOneClass` `WithBot.charZero` `Nat.cast_add` `Nat.cast_one`
`projectiveDimension_ne_top_iff` 📖	mathematical	—	`HasProjectiveDimensionLE`	—	`WithBot.nontrivial` `CharP.cast_eq_zero` `CharP.ofCharZero` `WithBot.charZero` `ENat.coe_ne_top` `WithBot.coe_eq_coe` `top_le_iff` `WithBot.coe_top` `projectiveDimension_le_iff` `Eq.le`
`projective_iff_hasProjectiveDimensionLT_one` 📖	mathematical	—	`Projective` `HasProjectiveDimensionLT`	—	`instHasProjectiveDimensionLTOfNatNatOfProjective` `HasExt.standard` `projective_iff_subsingleton_ext_one` `HasProjectiveDimensionLT.subsingleton` `le_refl`
`projective_iff_subsingleton_ext_one` 📖	mathematical	`HasExt`	`Projective` `Abelian.Ext`	—	`HasProjectiveDimensionLT.subsingleton` `instHasProjectiveDimensionLTOfNatNatOfProjective` `le_refl` `Limits.HasKernels.has_limit` `Abelian.has_kernels` `add_zero` `Abelian.Ext.covariant_sequence_exact₃` `ShortComplex.exact_kernel` `Limits.equalizer.ι_mono` `zero_add` `Equiv.surjective` `Equiv.injective` `Abelian.Ext.mk₀_comp_mk₀`

CategoryTheory.Abelian.Ext

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_zero_of_hasProjectiveDimensionLT` 📖	mathematical	`CategoryTheory.HasExt`	`CategoryTheory.Abelian.Ext` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroup`	—	`CategoryTheory.HasProjectiveDimensionLT.subsingleton`

CategoryTheory.HasProjectiveDimensionLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk` 📖	mathematical	`CategoryTheory.HasExt` `CategoryTheory.Abelian.Ext` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `CategoryTheory.Abelian.Ext.instAddCommGroup`	`CategoryTheory.HasProjectiveDimensionLT`	—	`Equiv.subsingleton` `CategoryTheory.HasExt.standard`
`subsingleton` 📖	mathematical	`CategoryTheory.HasExt`	`CategoryTheory.Abelian.Ext`	—	`CategoryTheory.HasExt.standard` `subsingleton'` `Equiv.subsingleton`
`subsingleton'` 📖	mathematical	—	`CategoryTheory.Abelian.Ext` `CategoryTheory.HasExt.standard`	—	—

CategoryTheory.Limits.IsZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasProjectiveDimensionLT_zero` 📖	mathematical	`CategoryTheory.Limits.IsZero`	`CategoryTheory.HasProjectiveDimensionLT`	—	`CategoryTheory.HasExt.standard` `CategoryTheory.hasProjectiveDimensionLT_iff` `zero_add` `CategoryTheory.Abelian.Ext.mk₀_id_comp` `eq_of_src` `CategoryTheory.Abelian.Ext.mk₀_zero` `CategoryTheory.Abelian.Ext.zero_comp`

CategoryTheory.Retract

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasProjectiveDimensionLT` 📖	mathematical	—	`CategoryTheory.HasProjectiveDimensionLT`	—	`CategoryTheory.HasExt.standard` `CategoryTheory.hasProjectiveDimensionLT_iff` `zero_add` `CategoryTheory.Abelian.Ext.mk₀_id_comp` `retract` `CategoryTheory.Abelian.Ext.mk₀_comp_mk₀` `add_zero` `CategoryTheory.Abelian.Ext.comp_assoc_of_second_deg_zero` `CategoryTheory.Abelian.Ext.eq_zero_of_hasProjectiveDimensionLT` `CategoryTheory.Abelian.Ext.comp_zero`
`projectiveDimension_le` 📖	mathematical	—	`WithBot` `ENat` `Preorder.toLE` `WithBot.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `CategoryTheory.projectiveDimension`	—	`sInf_le_sInf_of_subset_insert_top` `Set.insert_eq_of_mem` `instIsEmptyFalse` `hasProjectiveDimensionLT`

CategoryTheory.ShortComplex.ShortExact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasProjectiveDimensionLT_X₁` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	`CategoryTheory.HasProjectiveDimensionLT` `CategoryTheory.ShortComplex.X₁`	—	`CategoryTheory.HasExt.standard` `CategoryTheory.hasProjectiveDimensionLT_iff` `zero_add` `CategoryTheory.Abelian.Ext.contravariant_sequence_exact₁` `add_comm` `CategoryTheory.Abelian.Ext.eq_zero_of_hasProjectiveDimensionLT` `CategoryTheory.Abelian.Ext.comp_zero`
`hasProjectiveDimensionLT_X₂` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	`CategoryTheory.HasProjectiveDimensionLT` `CategoryTheory.ShortComplex.X₂`	—	`CategoryTheory.HasExt.standard` `CategoryTheory.hasProjectiveDimensionLT_iff` `zero_add` `CategoryTheory.Abelian.Ext.contravariant_sequence_exact₂` `CategoryTheory.Abelian.Ext.eq_zero_of_hasProjectiveDimensionLT` `CategoryTheory.Abelian.Ext.comp_zero`
`hasProjectiveDimensionLT_X₃` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	`CategoryTheory.HasProjectiveDimensionLT` `CategoryTheory.ShortComplex.X₃`	—	`CategoryTheory.HasExt.standard` `CategoryTheory.hasProjectiveDimensionLT_iff` `Nat.instCanonicallyOrderedAdd` `add_comm` `CategoryTheory.Abelian.Ext.contravariant_sequence_exact₃` `CategoryTheory.Abelian.Ext.eq_zero_of_hasProjectiveDimensionLT` `zero_add` `CategoryTheory.Abelian.Ext.comp_zero`
`hasProjectiveDimensionLT_X₃_iff` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	`CategoryTheory.HasProjectiveDimensionLT` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.X₁`	—	`hasProjectiveDimensionLT_X₁` `CategoryTheory.instHasProjectiveDimensionLTHAddNat_1` `CategoryTheory.instHasProjectiveDimensionLTOfNatNatOfProjective` `hasProjectiveDimensionLT_X₃`

---

← Back to Index