InjectiveDimension

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

Statistics

Metric	Count
Definitions	0
Theorems hasInjectiveDimensionLE_iff_forall_maximalSpectrum, hasInjectiveDimensionLE_iff_forall_primeSpectrum, injectiveDimension_eq_iSup_localizedModule_maximal, injectiveDimension_eq_iSup_localizedModule_prime, injectiveDimension_le_injectiveDimension_of_isLocalizedModule, instPreservesInjectiveObjectsLocalizationLocalizedModuleFunctorOfIsNoetherianRing, localizedModule_hasInjectiveDimensionLE	7
Total	7

ModuleCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasInjectiveDimensionLE_iff_forall_maximalSpectrum 📖	mathematical	—	CategoryTheory.HasInjectiveDimensionLE 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 Module.injective_module_of_injective_object Module.injective_iff_injective_object Module.injective_of_isLocalizedModule instIsScalarTowerLocalizationCarrierLocalizedModule Localization.isLocalization localizedModule_isLocalizedModule Module.injective_of_localization_maximal Module.Baer.iff_injective UnivLE.small univLE_of_max UnivLE.self Module.Baer.of_equiv IsScalarTower.left IsScalarTower.right OreLocalization.instIsScalarTower_1 localizedModuleIsLocalizedModule instEnoughInjectivesModuleCatOfSmall CategoryTheory.EnoughInjectives.presentation HasColimit.instHasColimit AddCommGrpCat.hasColimit CategoryTheory.Limits.cokernel.condition CategoryTheory.ShortComplex.exact_cokernel CategoryTheory.Limits.coequalizer.π_epi CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditiveLocalizationLocalizedModuleFunctor CategoryTheory.ShortComplex.ShortExact.map_of_exact instPreservesFiniteLimitsLocalizationLocalizedModuleFunctor instPreservesFiniteColimitsLocalizationLocalizedModuleFunctor CategoryTheory.ShortComplex.ShortExact.hasInjectiveDimensionLT_X₃_iff CategoryTheory.Functor.injective_obj instPreservesInjectiveObjectsLocalizationLocalizedModuleFunctorOfIsNoetherianRing
hasInjectiveDimensionLE_iff_forall_primeSpectrum 📖	mathematical	—	CategoryTheory.HasInjectiveDimensionLE 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_hasInjectiveDimensionLE Ideal.IsMaximal.isPrime' MaximalSpectrum.isMaximal hasInjectiveDimensionLE_iff_forall_maximalSpectrum
injectiveDimension_eq_iSup_localizedModule_maximal 📖	mathematical	—	CategoryTheory.injectiveDimension 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 hasInjectiveDimensionLE_iff_forall_maximalSpectrum eq_of_forall_ge_iff Equiv.subsingleton_congr LocalizedModule.instSubsingleton Module.subsingleton_of_localization_maximal IsScalarTower.left IsScalarTower.right localizedModuleIsLocalizedModule
injectiveDimension_eq_iSup_localizedModule_prime 📖	mathematical	—	CategoryTheory.injectiveDimension 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 hasInjectiveDimensionLE_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
injectiveDimension_le_injectiveDimension_of_isLocalizedModule 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat CategoryTheory.injectiveDimension ModuleCat Localization CommRing.toCommMonoid OreLocalization.instRing CommRing.toRing OreLocalization.oreSetComm moduleCategory abelian localizedModule	—	localizedModule_hasInjectiveDimensionLE le_of_forall_ge Equiv.subsingleton_congr LocalizedModule.instSubsingleton
instPreservesInjectiveObjectsLocalizationLocalizedModuleFunctorOfIsNoetherianRing 📖	mathematical	—	CategoryTheory.Functor.PreservesInjectiveObjects ModuleCat CommRing.toRing moduleCategory Localization CommRing.toCommMonoid OreLocalization.instRing OreLocalization.oreSetComm localizedModuleFunctor	—	small_of_surjective small_prod small_subtype Localization.mkHom_surjective Module.injective_iff_injective_object Module.injective_of_isLocalizedModule instIsScalarTowerLocalizationCarrierLocalizedModule Localization.isLocalization localizedModule_isLocalizedModule
localizedModule_hasInjectiveDimensionLE 📖	mathematical	—	CategoryTheory.HasInjectiveDimensionLE 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 Module.injective_iff_injective_object Module.injective_of_isLocalizedModule instIsScalarTowerLocalizationCarrierLocalizedModule Localization.isLocalization localizedModule_isLocalizedModule instEnoughInjectivesModuleCatOfSmall CategoryTheory.EnoughInjectives.presentation HasColimit.instHasColimit AddCommGrpCat.hasColimit UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.cokernel.condition CategoryTheory.ShortComplex.exact_cokernel CategoryTheory.Limits.coequalizer.π_epi CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact CategoryTheory.ShortComplex.ShortExact.exact smulCommClass_self IsLocalizedModule.map_exact CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditiveLocalizationLocalizedModuleFunctor CategoryTheory.ShortComplex.ShortExact.map_of_exact instPreservesFiniteLimitsLocalizationLocalizedModuleFunctor instPreservesFiniteColimitsLocalizationLocalizedModuleFunctor CategoryTheory.ShortComplex.ShortExact.hasInjectiveDimensionLT_X₃_iff CategoryTheory.Functor.injective_obj instPreservesInjectiveObjectsLocalizationLocalizedModuleFunctorOfIsNoetherianRing

---

← Back to Index