Dimension

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

Statistics

Metric	Count
Definitions HasInjectiveDimensionLE, HasInjectiveDimensionLT, injectiveDimension	3
Theorems eq_zero_of_hasInjectiveDimensionLT, mk, subsingleton, subsingleton', hasInjectiveDimensionLT_zero, hasInjectiveDimensionLT, injectiveDimension_le, hasInjectiveDimensionLT_X₁, hasInjectiveDimensionLT_X₂, hasInjectiveDimensionLT_X₃, hasInjectiveDimensionLT_X₃_iff, hasInjectiveDimensionLT_iff, hasInjectiveDimensionLT_of_ge, hasInjectiveDimensionLT_of_iso, hasInjectiveDimensionLT_zero_iff_isZero, injectiveDimension_eq_bot_iff, injectiveDimension_eq_of_iso, injectiveDimension_ge_iff, injectiveDimension_le_iff, injectiveDimension_lt_iff, injectiveDimension_ne_top_iff, injective_iff_hasInjectiveDimensionLT_one, injective_iff_subsingleton_ext_one, instHasInjectiveDimensionLTBiprod, instHasInjectiveDimensionLTHAddNat, instHasInjectiveDimensionLTHAddNat_1, instHasInjectiveDimensionLTOfNatNat, instHasInjectiveDimensionLTOfNatNatOfInjective, instHasInjectiveDimensionLTSucc, isZero_of_hasInjectiveDimensionLT_zero	30
Total	33

CategoryTheory

Definitions

Name	Category	Theorems
HasInjectiveDimensionLE 📖	MathDef	2 math math: injectiveDimension_le_iff, injectiveDimension_ne_top_iff
HasInjectiveDimensionLT 📖	CompData	20 math math: ShortComplex.ShortExact.hasInjectiveDimensionLT_X₁, instHasInjectiveDimensionLTOfNatNatOfInjective, instHasInjectiveDimensionLTSucc, instHasInjectiveDimensionLTHAddNat_1, Limits.IsZero.hasInjectiveDimensionLT_zero, injectiveDimension_ge_iff, instHasInjectiveDimensionLTBiprod, hasInjectiveDimensionLT_of_ge, HasInjectiveDimensionLT.mk, instHasInjectiveDimensionLTOfNatNat, injectiveDimension_lt_iff, Retract.hasInjectiveDimensionLT, ShortComplex.ShortExact.hasInjectiveDimensionLT_X₂, ShortComplex.ShortExact.hasInjectiveDimensionLT_X₃, hasInjectiveDimensionLT_of_iso, injective_iff_hasInjectiveDimensionLT_one, instHasInjectiveDimensionLTHAddNat, ShortComplex.ShortExact.hasInjectiveDimensionLT_X₃_iff, hasInjectiveDimensionLT_zero_iff_isZero, hasInjectiveDimensionLT_iff
injectiveDimension 📖	CompOp	6 math math: Retract.injectiveDimension_le, injectiveDimension_le_iff, injectiveDimension_ge_iff, injectiveDimension_eq_of_iso, injectiveDimension_lt_iff, injectiveDimension_eq_bot_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasInjectiveDimensionLT_iff 📖	mathematical	HasExt	HasInjectiveDimensionLT Abelian.Ext NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Abelian.Ext.instAddCommGroup	—	Abelian.Ext.eq_zero_of_hasInjectiveDimensionLT
hasInjectiveDimensionLT_of_ge 📖	mathematical	—	HasInjectiveDimensionLT	—	HasExt.standard hasInjectiveDimensionLT_iff Abelian.Ext.eq_zero_of_hasInjectiveDimensionLT
hasInjectiveDimensionLT_of_iso 📖	mathematical	—	HasInjectiveDimensionLT	—	Retract.hasInjectiveDimensionLT
hasInjectiveDimensionLT_zero_iff_isZero 📖	mathematical	—	HasInjectiveDimensionLT Limits.IsZero	—	isZero_of_hasInjectiveDimensionLT_zero Limits.IsZero.hasInjectiveDimensionLT_zero
injectiveDimension_eq_bot_iff 📖	mathematical	—	injectiveDimension Bot.bot WithBot ENat WithBot.bot Limits.IsZero	—	hasInjectiveDimensionLT_zero_iff_isZero injectiveDimension_lt_iff Nat.cast_zero WithBot.lt_coe_bot bot_eq_zero' WithBot.coe_zero
injectiveDimension_eq_of_iso 📖	mathematical	—	injectiveDimension	—	hasInjectiveDimensionLT_of_iso
injectiveDimension_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 injectiveDimension HasInjectiveDimensionLT	—	Mathlib.Tactic.Contrapose.contrapose_iff₃ injectiveDimension_lt_iff
injectiveDimension_le_iff 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat injectiveDimension AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat HasInjectiveDimensionLE	—	Nat.cast_add Nat.cast_one
injectiveDimension_lt_iff 📖	mathematical	—	WithBot ENat Preorder.toLT WithBot.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat injectiveDimension AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat HasInjectiveDimensionLT	—	csInf_mem WithBot.instWellFoundedLT instIsEmptyFalse sInf_lt_iff hasInjectiveDimensionLT_of_ge Nat.instCanonicallyOrderedAdd Nat.instNoMaxOrder WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid WithBot.zeroLEOneClass IsOrderedRing.toZeroLEOneClass WithBot.charZero Nat.cast_add Nat.cast_one
injectiveDimension_ne_top_iff 📖	mathematical	—	HasInjectiveDimensionLE	—	WithBot.nontrivial CharP.cast_eq_zero CharP.ofCharZero WithBot.charZero ENat.coe_ne_top WithBot.coe_eq_coe top_le_iff WithBot.coe_top injectiveDimension_le_iff Eq.le
injective_iff_hasInjectiveDimensionLT_one 📖	mathematical	—	Injective HasInjectiveDimensionLT	—	instHasInjectiveDimensionLTOfNatNatOfInjective HasExt.standard injective_iff_subsingleton_ext_one HasInjectiveDimensionLT.subsingleton le_refl
injective_iff_subsingleton_ext_one 📖	mathematical	HasExt	Injective Abelian.Ext	—	HasInjectiveDimensionLT.subsingleton instHasInjectiveDimensionLTOfNatNatOfInjective le_refl Limits.HasCokernels.has_colimit Abelian.has_cokernels zero_add Abelian.Ext.contravariant_sequence_exact₁ ShortComplex.exact_cokernel Limits.coequalizer.π_epi Equiv.surjective Equiv.injective Abelian.Ext.mk₀_comp_mk₀
instHasInjectiveDimensionLTBiprod 📖	mathematical	—	HasInjectiveDimensionLT Limits.biprod Preadditive.preadditiveHasZeroMorphisms Abelian.toPreadditive Limits.HasBinaryBiproducts.has_binary_biproduct Abelian.hasBinaryBiproducts	—	ShortComplex.ShortExact.hasInjectiveDimensionLT_X₂ Limits.HasBinaryBiproducts.has_binary_biproduct Abelian.hasBinaryBiproducts ShortComplex.Splitting.shortExact Abelian.hasZeroObject
instHasInjectiveDimensionLTHAddNat 📖	mathematical	—	HasInjectiveDimensionLT	—	hasInjectiveDimensionLT_of_ge
instHasInjectiveDimensionLTHAddNat_1 📖	mathematical	—	HasInjectiveDimensionLT	—	hasInjectiveDimensionLT_of_ge
instHasInjectiveDimensionLTOfNatNat 📖	mathematical	—	HasInjectiveDimensionLT Limits.HasZeroObject.zero' Abelian.hasZeroObject	—	Limits.IsZero.hasInjectiveDimensionLT_zero Abelian.hasZeroObject Limits.isZero_zero
instHasInjectiveDimensionLTOfNatNatOfInjective 📖	mathematical	—	HasInjectiveDimensionLT	—	HasExt.standard hasInjectiveDimensionLT_iff Nat.instCanonicallyOrderedAdd Abelian.Ext.eq_zero_of_injective
instHasInjectiveDimensionLTSucc 📖	mathematical	—	HasInjectiveDimensionLT	—	instHasInjectiveDimensionLTHAddNat
isZero_of_hasInjectiveDimensionLT_zero 📖	mathematical	—	Limits.IsZero	—	Limits.IsZero.iff_id_eq_zero Equiv.injective HasExt.standard Abelian.Ext.mk₀_zero Abelian.Ext.eq_zero_of_hasInjectiveDimensionLT le_refl

CategoryTheory.Abelian.Ext

Theorems

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

CategoryTheory.HasInjectiveDimensionLT

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.HasInjectiveDimensionLT	—	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
hasInjectiveDimensionLT_zero 📖	mathematical	CategoryTheory.Limits.IsZero	CategoryTheory.HasInjectiveDimensionLT	—	CategoryTheory.HasExt.standard CategoryTheory.hasInjectiveDimensionLT_iff add_zero CategoryTheory.Abelian.Ext.comp_mk₀_id eq_zero_of_tgt CategoryTheory.Abelian.Ext.mk₀_zero CategoryTheory.Abelian.Ext.comp_zero

CategoryTheory.Retract

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasInjectiveDimensionLT 📖	mathematical	—	CategoryTheory.HasInjectiveDimensionLT	—	CategoryTheory.HasExt.standard CategoryTheory.hasInjectiveDimensionLT_iff add_zero CategoryTheory.Abelian.Ext.comp_mk₀_id retract zero_add CategoryTheory.Abelian.Ext.mk₀_comp_mk₀ CategoryTheory.Abelian.Ext.comp_assoc_of_second_deg_zero CategoryTheory.Abelian.Ext.eq_zero_of_hasInjectiveDimensionLT CategoryTheory.Abelian.Ext.zero_comp
injectiveDimension_le 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat CategoryTheory.injectiveDimension	—	sInf_le_sInf_of_subset_insert_top Set.insert_eq_of_mem instIsEmptyFalse hasInjectiveDimensionLT

CategoryTheory.ShortComplex.ShortExact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasInjectiveDimensionLT_X₁ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.HasInjectiveDimensionLT CategoryTheory.ShortComplex.X₁	—	CategoryTheory.HasExt.standard CategoryTheory.hasInjectiveDimensionLT_iff Nat.instCanonicallyOrderedAdd CategoryTheory.Abelian.Ext.covariant_sequence_exact₁ CategoryTheory.Abelian.Ext.eq_zero_of_hasInjectiveDimensionLT add_zero CategoryTheory.Abelian.Ext.zero_comp
hasInjectiveDimensionLT_X₂ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.HasInjectiveDimensionLT CategoryTheory.ShortComplex.X₂	—	CategoryTheory.HasExt.standard CategoryTheory.hasInjectiveDimensionLT_iff add_zero CategoryTheory.Abelian.Ext.covariant_sequence_exact₂ CategoryTheory.Abelian.Ext.eq_zero_of_hasInjectiveDimensionLT CategoryTheory.Abelian.Ext.zero_comp
hasInjectiveDimensionLT_X₃ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.HasInjectiveDimensionLT CategoryTheory.ShortComplex.X₃	—	CategoryTheory.HasExt.standard CategoryTheory.hasInjectiveDimensionLT_iff add_zero CategoryTheory.Abelian.Ext.covariant_sequence_exact₃ add_comm CategoryTheory.Abelian.Ext.eq_zero_of_hasInjectiveDimensionLT CategoryTheory.Abelian.Ext.zero_comp
hasInjectiveDimensionLT_X₃_iff 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.HasInjectiveDimensionLT CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.X₁	—	hasInjectiveDimensionLT_X₁ CategoryTheory.instHasInjectiveDimensionLTHAddNat_1 CategoryTheory.instHasInjectiveDimensionLTOfNatNatOfInjective hasInjectiveDimensionLT_X₃

---

← Back to Index