Exactness

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

Statistics

Metric	Count
Definitions	0
Theorems map_linearMap_of_isLocalization, of_isLocalized_maximal, bijective_of_isLocalization_isMaximal, bijective_of_isLocalization_of_span_eq_top, bijective_of_isLocalized_maximal, bijective_of_isLocalized_span, bijective_of_localized_maximal, bijective_of_localized_span, exact_of_isLocalized_maximal, exact_of_isLocalized_span, exact_of_localized_maximal, exact_of_localized_span, injective_of_isLocalization_isMaximal, injective_of_isLocalization_of_span_eq_top, injective_of_isLocalized_maximal, injective_of_isLocalized_span, injective_of_localized_maximal, injective_of_localized_span, surjective_of_isLocalization_isMaximal, surjective_of_isLocalization_of_span_eq_top, surjective_of_isLocalized_maximal, surjective_of_isLocalized_span, surjective_of_localized_maximal, surjective_of_localized_span	24
Total	24

IsLocalizedModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_linearMap_of_isLocalization 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.toModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike map Ideal.primeCompl Algebra.linearMap instIsLocalizedModuleLinearMapOfIsLocalization SemilinearMapClass.semilinearMap AlgHom IsScalarTower.toAlgHom AlgHom.funLike NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass LinearMap.restrictScalars LinearMap.IsScalarTower.compatibleSMul' SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass linearMap_ext instIsLocalizedModuleLinearMapOfIsLocalization smulCommClass_self LinearMap.IsScalarTower.compatibleSMul' LinearMap.ext_ring RingHomCompTriple.ids map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_apply

LinearIndependent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isLocalized_maximal 📖	—	IsLocalization.AtPrime Ideal.IsMaximal.isPrime' IsScalarTower Algebra.toSMul CommSemiring.toSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsLocalizedModule.AtPrime LinearIndependent DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	—	Ideal.IsMaximal.isPrime' injective_of_isLocalized_maximal instIsLocalizedModuleFinsuppLinearMap instIsLocalizedModuleLinearMapOfIsLocalization smulCommClass_self LinearMap.CompatibleSMul.finsupp_dom LinearMap.IsScalarTower.compatibleSMul' IsLocalizedModule.map_linearCombination

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijective_of_isLocalization_isMaximal 📖	—	IsScalarTower Algebra.toSMul CommSemiring.toSemiring IsLocalization.AtPrime Ideal.IsMaximal.isPrime' IsLocalizedModule.AtPrime NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule SemilinearMapClass.semilinearMap AlgHom RingHom.id IsScalarTower.toAlgHom AlgHom.funLike NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Function.Bijective DFunLike.coe RingHom RingHom.instFunLike algebraMap	—	—	Ideal.IsMaximal.isPrime' NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass injective_of_isLocalization_isMaximal surjective_of_isLocalization_isMaximal
bijective_of_isLocalization_of_span_eq_top 📖	—	Ideal.span CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalization.Away Set Set.instMembership DFunLike.coe RingHom RingHom.instFunLike Function.Bijective IsLocalization.Away.map	—	—	injective_of_isLocalization_of_span_eq_top surjective_of_isLocalization_of_span_eq_top
bijective_of_isLocalized_maximal 📖	—	IsLocalizedModule.AtPrime Ideal.IsMaximal.isPrime' Function.Bijective DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsLocalizedModule.map Ideal.primeCompl	—	—	Ideal.IsMaximal.isPrime' smulCommClass_self injective_of_isLocalized_maximal surjective_of_isLocalized_maximal
bijective_of_isLocalized_span 📖	—	Ideal.span CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalizedModule.Away Set Set.instMembership Function.Bijective DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsLocalizedModule.map Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	—	smulCommClass_self injective_of_isLocalized_span surjective_of_isLocalized_span
bijective_of_localized_maximal 📖	—	Function.Bijective LocalizedModule Ideal.primeCompl CommSemiring.toSemiring Ideal.IsMaximal.isPrime' DFunLike.coe LinearMap Localization CommSemiring.toCommMonoid OreLocalization.instSemiring OreLocalization.oreSetComm RingHom.id Semiring.toNonAssocSemiring OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction OreLocalization.instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left IsScalarTower.right Algebra.id IsScalarTower.to_smulCommClass' OreLocalization.instAlgebra OreLocalization.instIsScalarTower_1 SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LocalizedModule.map	—	—	Ideal.IsMaximal.isPrime' smulCommClass_self IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 injective_of_localized_maximal surjective_of_localized_maximal
bijective_of_localized_span 📖	—	Ideal.span CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Function.Bijective LocalizedModule Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero Set Set.instMembership DFunLike.coe LinearMap Localization CommSemiring.toCommMonoid OreLocalization.instSemiring OreLocalization.oreSetComm RingHom.id OreLocalization.instAddCommMonoidOreLocalization Module.toDistribMulAction OreLocalization.instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid OreLocalization.instModuleOfIsScalarTower IsScalarTower.left IsScalarTower.right Algebra.id IsScalarTower.to_smulCommClass' OreLocalization.instAlgebra OreLocalization.instIsScalarTower_1 SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Algebra.toModule LocalizedModule.map	—	—	smulCommClass_self IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 injective_of_localized_span surjective_of_localized_span
exact_of_isLocalized_maximal 📖	—	IsLocalizedModule.AtPrime Ideal.IsMaximal.isPrime' Function.Exact DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsLocalizedModule.map Ideal.primeCompl AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	—	Ideal.IsMaximal.isPrime' smulCommClass_self RingHomSurjective.ids Submodule.eq_of_localization₀_maximal LinearMap.range_localizedMap_eq_localized₀_range LinearMap.ker_localizedMap_eq_localized₀_ker SetLike.ext_iff Submodule.ext
exact_of_isLocalized_span 📖	—	Ideal.span CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalizedModule.Away Set Set.instMembership Function.Exact DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsLocalizedModule.map Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	—	smulCommClass_self RingHomSurjective.ids Submodule.eq_of_isLocalized₀_span LinearMap.range_localizedMap_eq_localized₀_range LinearMap.ker_localizedMap_eq_localized₀_ker SetLike.ext_iff Submodule.ext
exact_of_localized_maximal 📖	—	Function.Exact LocalizedModule Ideal.primeCompl CommSemiring.toSemiring Ideal.IsMaximal.isPrime' DFunLike.coe LinearMap Localization CommSemiring.toCommMonoid OreLocalization.instSemiring OreLocalization.oreSetComm RingHom.id Semiring.toNonAssocSemiring OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction OreLocalization.instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left IsScalarTower.right Algebra.id IsScalarTower.to_smulCommClass' OreLocalization.instAlgebra OreLocalization.instIsScalarTower_1 SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LocalizedModule.map OreLocalization.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	—	Ideal.IsMaximal.isPrime' smulCommClass_self IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 exact_of_isLocalized_maximal localizedModuleIsLocalizedModule
exact_of_localized_span 📖	—	Ideal.span CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Function.Exact LocalizedModule Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero Set Set.instMembership DFunLike.coe LinearMap Localization CommSemiring.toCommMonoid OreLocalization.instSemiring OreLocalization.oreSetComm RingHom.id OreLocalization.instAddCommMonoidOreLocalization Module.toDistribMulAction OreLocalization.instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid OreLocalization.instModuleOfIsScalarTower IsScalarTower.left IsScalarTower.right Algebra.id IsScalarTower.to_smulCommClass' OreLocalization.instAlgebra OreLocalization.instIsScalarTower_1 SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Algebra.toModule LocalizedModule.map OreLocalization.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	—	smulCommClass_self IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 exact_of_isLocalized_span localizedModuleIsLocalizedModule
injective_of_isLocalization_isMaximal 📖	—	IsScalarTower Algebra.toSMul CommSemiring.toSemiring IsLocalization.AtPrime Ideal.IsMaximal.isPrime' IsLocalizedModule.AtPrime NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule SemilinearMapClass.semilinearMap AlgHom RingHom.id IsScalarTower.toAlgHom AlgHom.funLike NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass DFunLike.coe RingHom RingHom.instFunLike algebraMap	—	—	Ideal.IsMaximal.isPrime' NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass injective_of_isLocalized_maximal instIsLocalizedModuleLinearMapOfIsLocalization smulCommClass_self LinearMap.IsScalarTower.compatibleSMul' DFunLike.coe_fn_eq IsLocalizedModule.map_linearMap_of_isLocalization
injective_of_isLocalization_of_span_eq_top 📖	—	Ideal.span CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalization.Away Set Set.instMembership DFunLike.coe RingHom RingHom.instFunLike IsLocalization.Away.map	—	—	IsScalarTower.of_algebraMap_eq' IsLocalization.Away.instAlgebraMapSubmonoidPowersOfCoeRingHomAlgebraMap IsScalarTower.of_algebraMap_eq Algebra.algebraMapSubmonoid_powers MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsLocalization.map.congr_simp IsLocalization.map_eq injective_of_isLocalized_span instIsLocalizedModuleLinearMapOfIsLocalization instIsLocalizedModuleToLinearMapToAlgHomOfIsLocalizationAlgebraMapSubmonoid smulCommClass_self instIsLocalizationAlgebraMapSubmonoid Algebra.algebraMapSubmonoid_self Algebra.algebraMapSubmonoid_le_comap LinearMap.IsScalarTower.compatibleSMul' IsScalarTower.left IsScalarTower.right IsLocalization.map_linearMap_eq_toLinearMap_mapₐ
injective_of_isLocalized_maximal 📖	—	IsLocalizedModule.AtPrime Ideal.IsMaximal.isPrime' DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsLocalizedModule.map Ideal.primeCompl	—	—	Ideal.IsMaximal.isPrime' smulCommClass_self Module.eq_of_localization_maximal IsLocalizedModule.map_apply
injective_of_isLocalized_span 📖	—	Ideal.span CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalizedModule.Away Set Set.instMembership DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsLocalizedModule.map Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	—	smulCommClass_self Module.eq_of_isLocalized_span IsLocalizedModule.map_apply
injective_of_localized_maximal 📖	—	LocalizedModule Ideal.primeCompl CommSemiring.toSemiring Ideal.IsMaximal.isPrime' DFunLike.coe LinearMap Localization CommSemiring.toCommMonoid OreLocalization.instSemiring OreLocalization.oreSetComm RingHom.id Semiring.toNonAssocSemiring OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction OreLocalization.instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left IsScalarTower.right Algebra.id IsScalarTower.to_smulCommClass' OreLocalization.instAlgebra OreLocalization.instIsScalarTower_1 SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LocalizedModule.map	—	—	Ideal.IsMaximal.isPrime' smulCommClass_self IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 injective_of_isLocalized_maximal localizedModuleIsLocalizedModule
injective_of_localized_span 📖	—	Ideal.span CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule LocalizedModule Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero Set Set.instMembership DFunLike.coe LinearMap Localization CommSemiring.toCommMonoid OreLocalization.instSemiring OreLocalization.oreSetComm RingHom.id OreLocalization.instAddCommMonoidOreLocalization Module.toDistribMulAction OreLocalization.instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid OreLocalization.instModuleOfIsScalarTower IsScalarTower.left IsScalarTower.right Algebra.id IsScalarTower.to_smulCommClass' OreLocalization.instAlgebra OreLocalization.instIsScalarTower_1 SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Algebra.toModule LocalizedModule.map	—	—	smulCommClass_self IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 injective_of_isLocalized_span localizedModuleIsLocalizedModule
surjective_of_isLocalization_isMaximal 📖	—	IsScalarTower Algebra.toSMul CommSemiring.toSemiring IsLocalization.AtPrime Ideal.IsMaximal.isPrime' IsLocalizedModule.AtPrime NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule SemilinearMapClass.semilinearMap AlgHom RingHom.id IsScalarTower.toAlgHom AlgHom.funLike NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass DFunLike.coe RingHom RingHom.instFunLike algebraMap	—	—	Ideal.IsMaximal.isPrime' NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass surjective_of_isLocalized_maximal instIsLocalizedModuleLinearMapOfIsLocalization smulCommClass_self LinearMap.IsScalarTower.compatibleSMul' DFunLike.coe_fn_eq IsLocalizedModule.map_linearMap_of_isLocalization
surjective_of_isLocalization_of_span_eq_top 📖	—	Ideal.span CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalization.Away Set Set.instMembership DFunLike.coe RingHom RingHom.instFunLike IsLocalization.Away.map	—	—	IsScalarTower.of_algebraMap_eq' IsLocalization.Away.instAlgebraMapSubmonoidPowersOfCoeRingHomAlgebraMap IsScalarTower.of_algebraMap_eq Algebra.algebraMapSubmonoid_powers MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsLocalization.map.congr_simp IsLocalization.map_eq surjective_of_isLocalized_span instIsLocalizedModuleLinearMapOfIsLocalization instIsLocalizedModuleToLinearMapToAlgHomOfIsLocalizationAlgebraMapSubmonoid smulCommClass_self instIsLocalizationAlgebraMapSubmonoid Algebra.algebraMapSubmonoid_self Algebra.algebraMapSubmonoid_le_comap LinearMap.IsScalarTower.compatibleSMul' IsScalarTower.left IsScalarTower.right IsLocalization.map_linearMap_eq_toLinearMap_mapₐ
surjective_of_isLocalized_maximal 📖	—	IsLocalizedModule.AtPrime Ideal.IsMaximal.isPrime' DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsLocalizedModule.map Ideal.primeCompl	—	—	Ideal.IsMaximal.isPrime' smulCommClass_self RingHomSurjective.ids LinearMap.range_eq_top Submodule.eq_top_of_localization₀_maximal LinearMap.range_localizedMap_eq_localized₀_range
surjective_of_isLocalized_span 📖	—	Ideal.span CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalizedModule.Away Set Set.instMembership DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsLocalizedModule.map Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	—	smulCommClass_self RingHomSurjective.ids LinearMap.range_eq_top Submodule.eq_top_of_isLocalized₀_span LinearMap.range_localizedMap_eq_localized₀_range
surjective_of_localized_maximal 📖	—	LocalizedModule Ideal.primeCompl CommSemiring.toSemiring Ideal.IsMaximal.isPrime' DFunLike.coe LinearMap Localization CommSemiring.toCommMonoid OreLocalization.instSemiring OreLocalization.oreSetComm RingHom.id Semiring.toNonAssocSemiring OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction OreLocalization.instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left IsScalarTower.right Algebra.id IsScalarTower.to_smulCommClass' OreLocalization.instAlgebra OreLocalization.instIsScalarTower_1 SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LocalizedModule.map	—	—	Ideal.IsMaximal.isPrime' smulCommClass_self IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 surjective_of_isLocalized_maximal localizedModuleIsLocalizedModule
surjective_of_localized_span 📖	—	Ideal.span CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule LocalizedModule Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero Set Set.instMembership DFunLike.coe LinearMap Localization CommSemiring.toCommMonoid OreLocalization.instSemiring OreLocalization.oreSetComm RingHom.id OreLocalization.instAddCommMonoidOreLocalization Module.toDistribMulAction OreLocalization.instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid OreLocalization.instModuleOfIsScalarTower IsScalarTower.left IsScalarTower.right Algebra.id IsScalarTower.to_smulCommClass' OreLocalization.instAlgebra OreLocalization.instIsScalarTower_1 SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Algebra.toModule LocalizedModule.map	—	—	smulCommClass_self IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 surjective_of_isLocalized_span localizedModuleIsLocalizedModule

---

← Back to Index