Local properties of modules

In this file, we define local properties of modules in general.

@[reducible, inline]

abbrev IsLocalizedModule.AtPrime {R : Type u_1} {M : Type u_2} {M' : Type u_3} [CommSemiring R] (J : Ideal R) [J.IsPrime] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') : Prop

Equations

• IsLocalizedModule.AtPrime J f = IsLocalizedModule J.primeCompl f

@[reducible, inline]

abbrev LocalizedModule.AtPrime {R : Type u_1} [CommSemiring R] (J : Ideal R) [J.IsPrime] (M : Type u_2) [AddCommMonoid M] [Module R M] : Type (max u_1 u_2)

Equations

• LocalizedModule.AtPrime J M = LocalizedModule J.primeCompl M

Instances For

• instModuleAtPrimeComapRingHomAlgebraMapAtPrime

@[reducible, inline]

abbrev IsLocalizedModule.Away {R : Type u_1} {M : Type u_2} {M' : Type u_3} [CommSemiring R] (x : R) [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') : Prop

Equations

• IsLocalizedModule.Away x f = IsLocalizedModule (Submonoid.powers x) f

@[reducible, inline]

abbrev LocalizedModule.Away {R : Type u_1} [CommSemiring R] (x : R) (M : Type u_2) [AddCommMonoid M] [Module R M] : Type (max u_1 u_2)

Equations

• LocalizedModule.Away x M = LocalizedModule (Submonoid.powers x) M

noncomputable def map' {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : (M →ₗ[R] N) →ₗ[R] LocalizedModule S M →ₗ[Localization S] LocalizedModule S N

Equations

• map' S = { toFun := fun (f : M →ₗ[R] N) => LinearMap.extendScalarsOfIsLocalization S (Localization S) (↑R ((LocalizedModule.map S) f)), map_add' := ⋯, map_smul' := ⋯ }

def IsLocalizedModulePreserves (P : (R : Type u) → (M : Type v) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst : Module R M] → Prop) : Prop

A property P of R-modules is said to be preserved by localization if P holds for p⁻¹M whenever P holds for M.

Equations

• One or more equations did not get rendered due to their size.

def LocalizedModulePreserves (P : (R : Type u) → (M : Type (max u v)) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst : Module R M] → Prop) : Prop

A property P of R-modules is said to be preserved by localization if P holds for p⁻¹M whenever P holds for M.

Equations

• One or more equations did not get rendered due to their size.

def OfLocalizedModuleMaximal (P : (R : Type u) → (M : Type (max u v)) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst : Module R M] → Prop) : Prop

A property P of R-modules satisfies OfLocalizedModuleMaximal if P holds for M whenever P holds for Mₘ for all maximal ideal m.

Equations

• One or more equations did not get rendered due to their size.

def OfLocalizedModuleFiniteSpan (P : (R : Type u) → (M : Type (max u v)) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst : Module R M] → Prop) : Prop

A property P of R-modules satisfies OfLocalizedModuleFiniteSpan if P holds for M whenever there exists a finite set { r } that spans R such that P holds for Mᵣ.

Note that this is equivalent to OfLocalizedModuleSpan via ofLocalizedModuleSpan_iff_finite, but this is easier to prove.

Equations

• One or more equations did not get rendered due to their size.

def OfLocalizedModuleSpan (P : (R : Type u) → (M : Type (max u v)) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst : Module R M] → Prop) : Prop

A property P of R-modules satisfies OfLocalizedModuleSpan if P holds for M whenever there exists a set { r } that spans R such that P holds for Mᵣ.

Note that this is equivalent to OfLocalizedModuleFiniteSpan via ofLocalizedModuleSpan_iff_finite, but this is easier to prove.

Equations

• One or more equations did not get rendered due to their size.

theorem ofLocalizedModuleSpan_iff_finite (P : (R : Type u) → (M : Type (max u v)) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst : Module R M] → Prop) : OfLocalizedModuleSpan P ↔ OfLocalizedModuleFiniteSpan P

def LinearMap.LocalizedModulePreserves (P : {R : Type u} → [inst : CommRing R] → {M : Type v} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {N : Type v'} → [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → (M →ₗ[R] N) → Prop) : Prop

A property P of ring homs is said to be preserved by localization if P holds for M⁻¹R →+* M⁻¹S whenever P holds for R →+* S.

Equations

• One or more equations did not get rendered due to their size.

def OfLocalizedModuleMaximal' (P : (R : Type u) → (M : Type (max u v)) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst : Module R M] → Prop) (Q : (R : Type u) → (M : Type v) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst : Module R M] → Prop) : Prop

A property P of R-modules satisfies OfLocalizedModuleMaximal if P holds for M whenever P holds for Mₘ for all maximal ideal m.

Equations

• One or more equations did not get rendered due to their size.

def OfLocalizedModuleFiniteSpan' (P : (R : Type u) → (M : Type (max u v)) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst : Module R M] → Prop) (Q : (R : Type u) → (M : Type v) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst : Module R M] → Prop) : Prop

A property P of R-modules satisfies OfLocalizedModuleFiniteSpan if P holds for M whenever there exists a finite set { r } that spans R such that P holds for Mᵣ.

Note that this is equivalent to OfLocalizedModuleSpan via ofLocalizedModuleSpan_iff_finite, but this is easier to prove.

Equations

• One or more equations did not get rendered due to their size.

def OfLocalizedModuleSpan' (P : (R : Type u) → (M : Type (max u v)) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst : Module R M] → Prop) (Q : (R : Type u) → (M : Type v) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst : Module R M] → Prop) : Prop

A property P of R-modules satisfies OfLocalizedModuleSpan if P holds for M whenever there exists a set { r } that spans R such that P holds for Mᵣ.

Note that this is equivalent to OfLocalizedModuleFiniteSpan via ofLocalizedModuleSpan_iff_finite, but this is easier to prove.

Equations

• One or more equations did not get rendered due to their size.

theorem ofLocalizedModuleSpan_iff_finite' (P : (R : Type u) → (M : Type (max u v)) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst : Module R M] → Prop) (Q : (R : Type u) → (M : Type v) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst : Module R M] → Prop) : OfLocalizedModuleSpan' P Q ↔ OfLocalizedModuleFiniteSpan' P Q