The quotient map from `R ⧸ I ^ m` to `R ⧸ I ^ n` where `m ≥ n` #

In this file we define the canonical quotient linear map from M ⧸ I ^ m • ⊤ to M ⧸ I ^ n • ⊤ and canonical quotient ring map from R ⧸ I ^ m to R ⧸ I ^ n. These definitions will be used in theorems related to IsAdicComplete to find a lift element from compatible sequences in the quotients. We also include results about the relation between quotients of submodules and quotients of ideals here.

Main definitions #

Submodule.factorPow: the linear map from M ⧸ I ^ m • ⊤ to M ⧸ I ^ n • ⊤ induced by the natural inclusion I ^ n • ⊤ → I ^ m • ⊤.
Ideal.Quotient.factorPow: the ring homomorphism from R ⧸ I ^ m to R ⧸ I ^ n induced by the natural inclusion I ^ n → I ^ m.

Main results #

source

theorem Ideal.Quotient.factor_ker {R : Type u_1} [Ring R] {I J : Ideal R} (H : I ≤ J) [I.IsTwoSided] [J.IsTwoSided] :

RingHom.ker (factor H) = map (mk I) J

source

@[simp]

theorem Submodule.mapQ_eq_factor {R : Type u_1} [Ring R] {I J : Ideal R} (h : I ≤ J) (x : R ⧸ I) :

(mapQ I J LinearMap.id h) x = (factor h) x

source

theorem Submodule.pow_smul_top_le {R : Type u_1} [Ring R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] {m n : ℕ} (h : m ≤ n) :

I ^ n • ⊤ ≤ I ^ m • ⊤

source

@[reducible, inline]

abbrev Submodule.factorPow {R : Type u_1} [Ring R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] {m n : ℕ} (le : m ≤ n) :

M ⧸ I ^ n • ⊤ →ₗ[R] M ⧸ I ^ m • ⊤

The linear map from M ⧸ I ^ m • ⊤ to M ⧸ I ^ n • ⊤ induced by the natural inclusion I ^ n • ⊤ → I ^ m • ⊤.

To future contributors: Before adding lemmas related to Submodule.factorPow, please check whether it can be generalized to Submodule.factor and whether the corresponding (more general) lemma for Submodule.factor already exists.

Equations

Submodule.factorPow I M le = Submodule.factor ⋯

Instances For

source

@[reducible, inline]

abbrev Submodule.factorPowSucc {R : Type u_1} [Ring R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] (m : ℕ) :

M ⧸ I ^ (m + 1) • ⊤ →ₗ[R] M ⧸ I ^ m • ⊤

factorPow for n = m + 1

Equations

Submodule.factorPowSucc I M m = Submodule.factorPow I M ⋯

Instances For

source

@[reducible, inline]

abbrev Ideal.Quotient.factorPow {R : Type u_1} [Ring R] (I : Ideal R) [I.IsTwoSided] {m n : ℕ} (le : n ≤ m) :

R ⧸ I ^ m →+* R ⧸ I ^ n

The ring homomorphism from R ⧸ I ^ m to R ⧸ I ^ n induced by the natural inclusion I ^ n → I ^ m.

To future contributors: Before adding lemmas related to Ideal.factorPow, please check whether it can be generalized to Ideal.factor and whether the corresponding (more general) lemma for Ideal.factor already exists.

Equations