ProjectiveDimension

📁 Source: Mathlib/RingTheory/LocalProperties/ProjectiveDimension.lean

Statistics

Metric	Count
Definitions	0
Theorems hasProjectiveDimensionLE_iff_forall_maximalSpectrum, hasProjectiveDimensionLE_iff_forall_primeSpectrum, instPreservesProjectiveObjectsLocalizationLocalizedModuleFunctor, localizedModule_hasProjectiveDimensionLE, projectiveDimension_eq_iSup_localizedModule_maximal, projectiveDimension_eq_iSup_localizedModule_prime, projectiveDimension_le_projectiveDimension_of_isLocalizedModule	7
Total	7

ModuleCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasProjectiveDimensionLE_iff_forall_maximalSpectrum 📖	mathematical	—	CategoryTheory.HasProjectiveDimensionLE ModuleCat CommRing.toRing moduleCategory abelian Localization CommRing.toCommMonoid Ideal.primeCompl CommSemiring.toSemiring CommRing.toCommSemiring MaximalSpectrum.asIdeal Ideal.IsMaximal.isPrime' MaximalSpectrum.isMaximal OreLocalization.instRing OreLocalization.oreSetComm localizedModule	—	Ideal.IsMaximal.isPrime' MaximalSpectrum.isMaximal zero_add small_of_surjective small_prod small_subtype Localization.mkHom_surjective IsProjective.iff_projective Module.projective_of_isLocalizedModule instIsScalarTowerLocalizationCarrierLocalizedModule Localization.isLocalization localizedModule_isLocalizedModule projective_of_module_projective Module.finitePresentation_of_finite Module.projective_of_localization_maximal Module.Projective.of_equiv RingHomInvPair.ids IsScalarTower.left IsScalarTower.right OreLocalization.instIsScalarTower_1 localizedModuleIsLocalizedModule Module.exists_finite_presentation LinearMap.shortExact_shortComplexKer projective_of_categoryTheory_projective Module.Projective.of_free CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditiveLocalizationLocalizedModuleFunctor CategoryTheory.ShortComplex.ShortExact.map_of_exact instPreservesFiniteLimitsLocalizationLocalizedModuleFunctor instPreservesFiniteColimitsLocalizationLocalizedModuleFunctor CategoryTheory.Functor.projective_obj_of_projective instPreservesProjectiveObjectsLocalizationLocalizedModuleFunctor CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃_iff Module.IsNoetherian.finite isNoetherian_submodule' isNoetherian_of_isNoetherianRing_of_finite
hasProjectiveDimensionLE_iff_forall_primeSpectrum 📖	mathematical	—	CategoryTheory.HasProjectiveDimensionLE ModuleCat CommRing.toRing moduleCategory abelian Localization CommRing.toCommMonoid Ideal.primeCompl CommSemiring.toSemiring CommRing.toCommSemiring PrimeSpectrum.asIdeal PrimeSpectrum.isPrime OreLocalization.instRing OreLocalization.oreSetComm localizedModule	—	PrimeSpectrum.isPrime localizedModule_hasProjectiveDimensionLE Ideal.IsMaximal.isPrime' MaximalSpectrum.isMaximal hasProjectiveDimensionLE_iff_forall_maximalSpectrum
instPreservesProjectiveObjectsLocalizationLocalizedModuleFunctor 📖	mathematical	—	CategoryTheory.Functor.PreservesProjectiveObjects ModuleCat CommRing.toRing moduleCategory Localization CommRing.toCommMonoid OreLocalization.instRing OreLocalization.oreSetComm localizedModuleFunctor	—	small_of_surjective small_prod small_subtype Localization.mkHom_surjective IsProjective.iff_projective Module.projective_of_isLocalizedModule instIsScalarTowerLocalizationCarrierLocalizedModule Localization.isLocalization localizedModule_isLocalizedModule
localizedModule_hasProjectiveDimensionLE 📖	mathematical	—	CategoryTheory.HasProjectiveDimensionLE ModuleCat Localization CommRing.toCommMonoid OreLocalization.instRing CommRing.toRing OreLocalization.oreSetComm moduleCategory abelian localizedModule	—	small_of_surjective small_prod small_subtype Localization.mkHom_surjective zero_add CategoryTheory.projective_iff_hasProjectiveDimensionLT_one IsProjective.iff_projective Module.projective_of_isLocalizedModule instIsScalarTowerLocalizationCarrierLocalizedModule Localization.isLocalization localizedModule_isLocalizedModule CategoryTheory.EnoughProjectives.presentation enoughProjectives hasLimit small_Pi UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.kernel.condition CategoryTheory.ShortComplex.exact_kernel CategoryTheory.Limits.equalizer.ι_mono CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditiveLocalizationLocalizedModuleFunctor CategoryTheory.ShortComplex.ShortExact.map_of_exact instPreservesFiniteLimitsLocalizationLocalizedModuleFunctor instPreservesFiniteColimitsLocalizationLocalizedModuleFunctor CategoryTheory.Functor.projective_obj instPreservesProjectiveObjectsLocalizationLocalizedModuleFunctor CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃_iff
projectiveDimension_eq_iSup_localizedModule_maximal 📖	mathematical	—	CategoryTheory.projectiveDimension ModuleCat CommRing.toRing moduleCategory abelian iSup WithBot ENat MaximalSpectrum CommRing.toCommSemiring WithBot.instSupSet instPreorderENat ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat Localization CommRing.toCommMonoid Ideal.primeCompl CommSemiring.toSemiring MaximalSpectrum.asIdeal Ideal.IsMaximal.isPrime' MaximalSpectrum.isMaximal OreLocalization.instRing OreLocalization.oreSetComm localizedModule	—	Ideal.IsMaximal.isPrime' MaximalSpectrum.isMaximal hasProjectiveDimensionLE_iff_forall_maximalSpectrum eq_of_forall_ge_iff Equiv.subsingleton_congr LocalizedModule.instSubsingleton Module.subsingleton_of_localization_maximal IsScalarTower.left IsScalarTower.right localizedModuleIsLocalizedModule
projectiveDimension_eq_iSup_localizedModule_prime 📖	mathematical	—	CategoryTheory.projectiveDimension ModuleCat CommRing.toRing moduleCategory abelian iSup WithBot ENat PrimeSpectrum CommRing.toCommSemiring WithBot.instSupSet instPreorderENat ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat Localization CommRing.toCommMonoid Ideal.primeCompl CommSemiring.toSemiring PrimeSpectrum.asIdeal PrimeSpectrum.isPrime OreLocalization.instRing OreLocalization.oreSetComm localizedModule	—	PrimeSpectrum.isPrime hasProjectiveDimensionLE_iff_forall_primeSpectrum eq_of_forall_ge_iff Equiv.subsingleton_congr LocalizedModule.instSubsingleton Module.subsingleton_of_localization_maximal Ideal.IsMaximal.isPrime' IsScalarTower.left IsScalarTower.right localizedModuleIsLocalizedModule Ideal.IsMaximal.isPrime
projectiveDimension_le_projectiveDimension_of_isLocalizedModule 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat CategoryTheory.projectiveDimension ModuleCat Localization CommRing.toCommMonoid OreLocalization.instRing CommRing.toRing OreLocalization.oreSetComm moduleCategory abelian localizedModule	—	localizedModule_hasProjectiveDimensionLE le_of_forall_ge Equiv.subsingleton_congr LocalizedModule.instSubsingleton

---

← Back to Index