Submodule

📁 Source: Mathlib/Algebra/Module/LocalizedModule/Submodule.lean

Statistics

Metric	Count
Definitions toKerIsLocalized, localized, localized', localized'FrameHom, localized'gi, localizedEquiv, localized₀, localized₀FrameHom, toLocalized, toLocalized', toLocalizedQuotient, toLocalizedQuotient', toLocalized₀, localizedQuotientEquiv	14
Theorems toLocalizedQuotient', ker_localizedMap_eq_localized'_ker, ker_localizedMap_eq_localized₀_ker, localized'_ker_eq_ker_localizedMap, localized'_range_eq_range_localizedMap, range_localizedMap_eq_localized₀_range, toKerIsLocalized_apply_coe, toKerLocalized_isLocalizedModule, localized'FrameHom_apply, localized₀FrameHom_apply, instIsLocalizedModuleSubtypeMemLocalized₀ToLocalized₀, isLocalizedModule, localized'_bot, localized'_eq_span, localized'_iSup, localized'_inf, localized'_le_localized'_of_smul_le, localized'_smul, localized'_span, localized'_top, localized₀_bot, localized₀_iSup, localized₀_inf, localized₀_le_localized₀_of_smul_le, localized₀_smul, localized₀_top, map_le_localized₀, mem_localized', mem_localized₀, restrictScalars_localized', restrictScalars_localized'_smul, toLocalized'_apply_coe, toLocalizedQuotient'_mk, toLocalized₀_apply_coe, instIsLocalizedModuleQuotientSubmoduleLocalizedModuleLocalizationLocalizedToLocalizedQuotient	35
Total	49

IsLocalizedModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toLocalizedQuotient' 📖	mathematical	—	IsLocalizedModule CommRing.toCommSemiring HasQuotient.Quotient Submodule CommSemiring.toSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient CommRing.toRing Submodule.localized' Submodule.Quotient.addCommGroup Submodule.Quotient.module Submodule.Quotient.module' Algebra.toSMul Submodule.toLocalizedQuotient'	—	smulCommClass_self IsScalarTower.left Module.End.isUnit_iff Submodule.Quotient.mk_surjective Submodule.smul_mem Submodule.Quotient.eq one_smul IsLocalization.mk'_self' IsLocalization.smul_mk'_one smul_assoc SMulCommClass.smul_comm IsScalarTower.to_smulCommClass' Module.algebraMap_end_apply Submodule.Quotient.isScalarTower mk'_surjective mk'_cancel' map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass exists_of_eq LinearMap.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul Submonoid.isScalarTower SemigroupAction.mul_smul SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass

LinearMap

Definitions

Name	Category	Theorems
toKerIsLocalized 📖	CompOp	2 math math: toKerLocalized_isLocalizedModule, toKerIsLocalized_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ker_localizedMap_eq_localized'_ker 📖	mathematical	—	ker CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearMap addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike IsLocalizedModule.map Submodule.restrictScalars Algebra.toSMul Submodule.localized'	—	Submodule.ext smulCommClass_self Submodule.restrictScalars.congr_simp localized'_ker_eq_ker_localizedMap
ker_localizedMap_eq_localized₀_ker 📖	mathematical	—	ker CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearMap addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike IsLocalizedModule.map Submodule.localized₀	—	Submodule.ext smulCommClass_self IsLocalizedModule.mk'_surjective IsLocalizedModule.map_mk' IsLocalizedModule.eq_zero_iff map_smul_of_tower IsScalarTower.compatibleSMul Submonoid.isScalarTower IsScalarTower.left IsLocalizedModule.mk'_cancel_left IsLocalizedModule.mk'.congr_simp IsLocalizedModule.mk'_zero
localized'_ker_eq_ker_localizedMap 📖	mathematical	—	Submodule.localized' ker CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring extendScalarsOfIsLocalization DFunLike.coe LinearMap addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike IsLocalizedModule.map	—	SetLike.ext smulCommClass_self SetLike.ext_iff ker_localizedMap_eq_localized₀_ker
localized'_range_eq_range_localizedMap 📖	mathematical	—	Submodule.localized' range CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids extendScalarsOfIsLocalization DFunLike.coe LinearMap addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike IsLocalizedModule.map	—	SetLike.ext RingHomSurjective.ids smulCommClass_self SetLike.ext_iff range_localizedMap_eq_localized₀_range
range_localizedMap_eq_localized₀_range 📖	mathematical	—	range CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids DFunLike.coe LinearMap addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike IsLocalizedModule.map Submodule.localized₀	—	Submodule.ext RingHomSurjective.ids smulCommClass_self Function.Surjective.exists IsLocalizedModule.mk'_surjective IsLocalizedModule.map_mk'
toKerIsLocalized_apply_coe 📖	mathematical	—	Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike ker RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearMap addCommMonoid module instFunLike IsLocalizedModule.map smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Submodule.addCommMonoid Submodule.module toKerIsLocalized	—	smulCommClass_self
toKerLocalized_isLocalizedModule 📖	mathematical	—	IsLocalizedModule Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike ker RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearMap addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike IsLocalizedModule.map Submodule.addCommMonoid Submodule.module toKerIsLocalized	—	RingHomInvPair.ids smulCommClass_self localized'_ker_eq_ker_localizedMap IsLocalizedModule.of_linearEquiv IsScalarTower.compatibleSMul Submodule.isScalarTower' Submodule.isLocalizedModule

Submodule

Definitions

Name	Category	Theorems
localized 📖	CompOp	1 math math: instIsLocalizedModuleQuotientSubmoduleLocalizedModuleLocalizationLocalizedToLocalizedQuotient
localized' 📖	CompOp	20 math math: mem_localized', LinearMap.ker_localizedMap_eq_localized'_ker, localized'_top, Ideal.localized'_eq_map, localized'_iSup, localized'_inf, LinearMap.localized'_range_eq_range_localizedMap, LinearMap.localized'_ker_eq_ker_localizedMap, isLocalizedModule, localized'_span, IsLocalizedModule.toLocalizedQuotient', localized'_eq_span, IsLocalizedModule.localized'FrameHom_apply, toLocalizedQuotient'_mk, restrictScalars_localized', toLocalized'_apply_coe, localized'_smul, localized'_bot, localized'_le_localized'_of_smul_le, restrictScalars_localized'_smul
localized'FrameHom 📖	CompOp	1 math math: IsLocalizedModule.localized'FrameHom_apply
localized'gi 📖	CompOp	—
localizedEquiv 📖	CompOp	—
localized₀ 📖	CompOp	19 math math: Algebra.idealMap_eq_ofEq_comp_toLocalized₀, localized₀_top, LinearMap.ker_localizedMap_eq_localized₀_ker, IsMinimalPrimaryDecomposition.comap_localized₀_eq_iInf, toLocalized₀_apply_coe, localized₀_bot, localized₀_smul, IsLocalizedModule.localized₀FrameHom_apply, localized₀_le_localized₀_of_smul_le, Ideal.localized₀_eq_restrictScalars_map, IsMinimalPrimaryDecomposition.comap_localized₀_eq_ite, mem_localized₀, localized₀_iSup, restrictScalars_localized', toLocalized'_apply_coe, map_le_localized₀, localized₀_inf, instIsLocalizedModuleSubtypeMemLocalized₀ToLocalized₀, LinearMap.range_localizedMap_eq_localized₀_range
localized₀FrameHom 📖	CompOp	1 math math: IsLocalizedModule.localized₀FrameHom_apply
toLocalized 📖	CompOp	—
toLocalized' 📖	CompOp	2 math math: isLocalizedModule, toLocalized'_apply_coe
toLocalizedQuotient 📖	CompOp	1 math math: instIsLocalizedModuleQuotientSubmoduleLocalizedModuleLocalizationLocalizedToLocalizedQuotient
toLocalizedQuotient' 📖	CompOp	2 math math: IsLocalizedModule.toLocalizedQuotient', toLocalizedQuotient'_mk
toLocalized₀ 📖	CompOp	3 math math: Algebra.idealMap_eq_ofEq_comp_toLocalized₀, toLocalized₀_apply_coe, instIsLocalizedModuleSubtypeMemLocalized₀ToLocalized₀

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsLocalizedModuleSubtypeMemLocalized₀ToLocalized₀ 📖	mathematical	—	IsLocalizedModule Submodule CommSemiring.toSemiring SetLike.instMembership setLike localized₀ addCommMonoid module toLocalized₀	—	smulCommClass_self IsScalarTower.left IsLocalizedModule.smul_injective Module.algebraMap_end_apply smulMemClass SetLike.val_smul_of_tower IsLocalizedModule.mk'_smul Submonoid.smul_def IsLocalizedModule.mk'_cancel_right IsLocalizedModule.mk'_cancel' IsLocalizedModule.exists_of_eq
isLocalizedModule 📖	mathematical	—	IsLocalizedModule Submodule CommSemiring.toSemiring SetLike.instMembership setLike localized' addCommMonoid module module' Algebra.toSMul toLocalized'	—	—
localized'_bot 📖	mathematical	—	localized' Bot.bot Submodule CommSemiring.toSemiring instBot	—	SetLike.ext' SetLike.ext'_iff localized₀_bot
localized'_eq_span 📖	mathematical	—	localized' span CommSemiring.toSemiring Set.image DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike SetLike.coe Submodule setLike	—	le_antisymm one_smul mul_one IsLocalizedModule.mk'_smul_mk' smul_mem subset_span IsLocalizedModule.mk'_one span_le
localized'_iSup 📖	mathematical	—	localized' iSup Submodule CommSemiring.toSemiring ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice	—	GaloisConnection.l_iSup GaloisInsertion.gc
localized'_inf 📖	mathematical	—	localized' Submodule CommSemiring.toSemiring instMin	—	SetLike.ext' SetLike.ext'_iff localized₀_inf
localized'_le_localized'_of_smul_le 📖	mathematical	Submodule CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder instPartialOrder Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero pointwiseDistribMulAction Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid	Submodule CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder instPartialOrder localized'	—	smulCommClass_self localized₀_le_localized₀_of_smul_le
localized'_smul 📖	mathematical	—	localized' Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule instSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toModule IsScalarTower.right Algebra.linearMap instIsLocalizedModuleLinearMapOfIsLocalization	—	restrictScalars_injective IsScalarTower.left IsScalarTower.right instIsLocalizedModuleLinearMapOfIsLocalization restrictScalars_localized'_smul localized₀_smul
localized'_span 📖	mathematical	—	localized' span CommSemiring.toSemiring Set.image DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	localized'_eq_span RingHomSurjective.ids map_coe map_span span_span_of_tower
localized'_top 📖	mathematical	—	localized' Top.top Submodule CommSemiring.toSemiring instTop	—	SetLike.ext' SetLike.ext'_iff localized₀_top
localized₀_bot 📖	mathematical	—	localized₀ Bot.bot Submodule CommSemiring.toSemiring instBot	—	le_bot_iff IsLocalizedModule.mk'_zero
localized₀_iSup 📖	mathematical	—	localized₀ iSup Submodule CommSemiring.toSemiring ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice	—	Localization.isLocalization IsScalarTower.right IsLocalizedModule.isScalarTower_module restrictScalars_iSup localized'_iSup
localized₀_inf 📖	mathematical	—	localized₀ Submodule CommSemiring.toSemiring instMin	—	IsLocalizedModule.mk'_eq_mk'_iff smul_of_tower_mem Submonoid.isScalarTower IsScalarTower.left SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass SemigroupAction.mul_smul smul_smul IsLocalizedModule.mk'_cancel_left
localized₀_le_localized₀_of_smul_le 📖	mathematical	Submodule CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder instPartialOrder Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero pointwiseDistribMulAction Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid	Submodule CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder instPartialOrder localized₀	—	smulCommClass_self IsLocalizedModule.mk'_cancel_left
localized₀_smul 📖	mathematical	—	localized₀ Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule instSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	le_antisymm IsScalarTower.left smul_induction_on IsLocalizedModule.mk'_smul smul_mem_smul IsLocalizedModule.mk'_add AddSubmonoidClass.toAddMemClass addSubmonoidClass smul_le
localized₀_top 📖	mathematical	—	localized₀ Top.top Submodule CommSemiring.toSemiring instTop	—	top_le_iff IsLocalizedModule.mk'_surjective
map_le_localized₀ 📖	mathematical	—	Submodule CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder instPartialOrder map RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids localized₀	—	RingHomSurjective.ids mem_localized₀ IsLocalizedModule.mk'_one
mem_localized' 📖	mathematical	—	Submodule CommSemiring.toSemiring SetLike.instMembership setLike localized' Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Submonoid.instSetLike IsLocalizedModule.mk'	—	—
mem_localized₀ 📖	mathematical	—	Submodule CommSemiring.toSemiring SetLike.instMembership setLike localized₀ Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Submonoid.instSetLike IsLocalizedModule.mk'	—	—
restrictScalars_localized' 📖	mathematical	—	restrictScalars CommSemiring.toSemiring Algebra.toSMul localized' localized₀	—	—
restrictScalars_localized'_smul 📖	mathematical	—	restrictScalars CommSemiring.toSemiring Algebra.toSMul Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule instSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction localized' Algebra.toModule IsScalarTower.right Algebra.linearMap instIsLocalizedModuleLinearMapOfIsLocalization	—	le_antisymm IsScalarTower.left IsScalarTower.right instIsLocalizedModuleLinearMapOfIsLocalization smul_induction_on restrictScalars_mem IsLocalization.mk'_eq_mk' IsLocalization.mk'_eq_mul_mk'_one SemigroupAction.mul_smul algebraMap_smul smul_mem_smul smul_mem AddMemClass.add_mem AddSubmonoidClass.toAddMemClass addSubmonoidClass smul_le IsLocalizedModule.mk'_one
toLocalized'_apply_coe 📖	mathematical	—	Submodule CommSemiring.toSemiring SetLike.instMembership setLike localized₀ DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring localized' addCommMonoid module module' Algebra.toSMul LinearMap.instFunLike toLocalized'	—	—
toLocalizedQuotient'_mk 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid hasQuotient CommRing.toRing localized' Quotient.addCommGroup Quotient.module Quotient.module' Algebra.toSMul LinearMap.instFunLike toLocalizedQuotient'	—	—
toLocalized₀_apply_coe 📖	mathematical	—	Submodule CommSemiring.toSemiring SetLike.instMembership setLike localized₀ DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring addCommMonoid module LinearMap.instFunLike toLocalized₀	—	—

Submodule.IsLocalizedModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
localized'FrameHom_apply 📖	mathematical	—	DFunLike.coe FrameHom Submodule CommSemiring.toSemiring Submodule.completeLattice FrameHom.instFunLike Submodule.localized'FrameHom Submodule.localized'	—	—
localized₀FrameHom_apply 📖	mathematical	—	DFunLike.coe FrameHom Submodule CommSemiring.toSemiring Submodule.completeLattice FrameHom.instFunLike Submodule.localized₀FrameHom Submodule.localized₀	—	—

(root)

Definitions

Name	Category	Theorems
localizedQuotientEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsLocalizedModuleQuotientSubmoduleLocalizedModuleLocalizationLocalizedToLocalizedQuotient 📖	mathematical	—	IsLocalizedModule CommRing.toCommSemiring HasQuotient.Quotient Submodule CommSemiring.toSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient CommRing.toRing LocalizedModule Localization CommSemiring.toCommMonoid OreLocalization.instSemiring OreLocalization.oreSetComm OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction OreLocalization.instModule OreLocalization.instRing OreLocalization.instAddCommGroup Submodule.localized Submodule.Quotient.addCommGroup Submodule.Quotient.module Submodule.Quotient.module' OreLocalization.instSMulOfIsScalarTower CommMonoid.toMonoid Monoid.toMulAction Algebra.toSMul Algebra.id IsScalarTower.right OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid OreLocalization.instIsScalarTower_1 SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Submodule.toLocalizedQuotient	—	IsLocalizedModule.toLocalizedQuotient'

---

← Back to Index