Reducing modules and linear maps modulo an ideal

An R-linear map f : M → N carries I • M into I • N for every ideal I of a commutative ring R, so it induces an R ⧸ I-linear map M ⧸ I • M → N ⧸ I • N. This is Mathlib's QuotSMulTop.map, which treats the principal case M ⧸ x • M as an R-linear map, made linear over the quotient ring and extended to an arbitrary ideal.

Reduction modulo I is right exact. When I = (x) and x is regular on the last term, it also preserves injectivity on the left, so it carries a short exact sequence 0 → K → P → M → 0 to a short exact sequence 0 → K ⧸ x K → P ⧸ x P → M ⧸ x M → 0.

Mathlib makes QuotSMulTop x M = M ⧸ x M a module over R ⧸ (x); this action is induced by the R-action on M, the analogue for x • ⊤ of Mathlib's Module.Quotient.mk_smul_mk for I • ⊤.

Reductions of cyclic modules commute: (R ⧸ (s)) ⧸ r (R ⧸ (s)) and (R ⧸ (r)) ⧸ s (R ⧸ (r)) are both R ⧸ (r, s). For an R-algebra A and an A-module N, reducing modulo the image of r : R in A is reducing the underlying R-module modulo r. A finite free R-module of rank d reduces modulo r to (R ⧸ (r)) ^ d, so it has #(R ⧸ (r)) ^ d elements. Finally, in a domain, an element r not divisible by a prime π is regular on R ⧸ (π ^ m).

Main definitions

• Ideal.mapQSMulTop: the R ⧸ I-linear map M ⧸ I • M → N ⧸ I • N induced by f : M →ₗ[R] N.
• QuotSMulTop.quotSpanSingletonComm: (R ⧸ (s)) ⧸ r (R ⧸ (s)) ≃ (R ⧸ (r)) ⧸ s (R ⧸ (r)).
• QuotSMulTop.restrictScalarsEquiv: N ⧸ (algebraMap R A r) N ≃ N ⧸ r N as R-modules.

Main results

• QuotSMulTop.mk_smul_mk: [r] • [m] = [r • m] in M ⧸ x M.
• QuotSMulTop.subsingleton_of_isUnit: M ⧸ x M is trivial for a unit x.
• Ideal.mapQSMulTop_id and Ideal.mapQSMulTop_comp: reduction modulo I is functorial.
• Ideal.mapQSMulTop_surjective and Ideal.mapQSMulTop_exact: reduction modulo I preserves surjectivity and exactness at the middle of M → N → P → 0.
• QuotSMulTop.map_comp_quotEquivOfEq: for I = (x), the reduction is QuotSMulTop.map x f, up to the identification of (x) • ⊤ with x • ⊤.
• Ideal.mapQSMulTop_span_singleton_injective: reduction modulo (x) preserves injectivity of the first map of a short exact sequence whose last term is x-regular.
• QuotSMulTop.ker_mapQ_mkQ and QuotSMulTop.mapQ_mkQ_surjective: for an ideal I and y : R, the map N ⧸ I N → (N ⧸ y N) ⧸ I (N ⧸ y N) is surjective with kernel y (N ⧸ I N), so that quotienting by I and by y may be done in either order.
• QuotSMulTop.natCard_eq_pow_finrank: a finite free R-module M has #(M ⧸ r M) = #(R ⧸ (r)) ^ finrank R M.
• Prime.isSMulRegular_quotient_span_pow: in a domain, if the prime π does not divide r, then r is regular on R ⧸ (π ^ m).

noncomputable def Ideal.mapQSMulTop {R : Type u_1} [CommRing R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (I : Ideal R) (f : M →ₗ[R] N) : M ⧸ I • ⊤ →ₗ[R ⧸ I] N ⧸ I • ⊤

The R ⧸ I-linear map M ⧸ I • M → N ⧸ I • N induced by an R-linear map M → N.

@[simp]

theorem Ideal.mapQSMulTop_mk {R : Type u_1} [CommRing R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (I : Ideal R) (f : M →ₗ[R] N) (m : M) : (I.mapQSMulTop f) (Submodule.Quotient.mk m) = Submodule.Quotient.mk (f m)

@[simp]

theorem Ideal.mapQSMulTop_id {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (I : Ideal R) : I.mapQSMulTop LinearMap.id = LinearMap.id

@[simp]

theorem Ideal.mapQSMulTop_comp {R : Type u_1} [CommRing R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P] (I : Ideal R) (g : N →ₗ[R] P) (f : M →ₗ[R] N) : I.mapQSMulTop (g ∘ₗ f) = I.mapQSMulTop g ∘ₗ I.mapQSMulTop f

theorem Ideal.mapQSMulTop_surjective {R : Type u_1} [CommRing R] {N : Type u_3} {P : Type u_4} [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P] (I : Ideal R) {g : N →ₗ[R] P} (hg : Function.Surjective ⇑g) : Function.Surjective ⇑(I.mapQSMulTop g)

Reduction modulo an ideal preserves surjectivity.

theorem Ideal.mapQSMulTop_exact {R : Type u_1} [CommRing R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P] (I : Ideal R) {f : M →ₗ[R] N} {g : N →ₗ[R] P} (hfg : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g) : Function.Exact ⇑(I.mapQSMulTop f) ⇑(I.mapQSMulTop g)

Reduction modulo an ideal is right exact: it carries an exact sequence M → N → P → 0 to an exact sequence M ⧸ I • M → N ⧸ I • N → P ⧸ I • P → 0.

@[simp]

theorem QuotSMulTop.mk_smul_mk {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {x : R} (r : R) (m : M) : (Ideal.Quotient.mk (Ideal.span {x})) r • Submodule.Quotient.mk m = Submodule.Quotient.mk (r • m)

The R ⧸ (x)-action on M ⧸ x M is induced by the R-action on M.

theorem QuotSMulTop.subsingleton_of_isUnit {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {x : R} (hx : IsUnit x) : Subsingleton (QuotSMulTop x M)

Modulo a unit, every module is trivial: x • ⊤ = ⊤ for a unit x.

theorem QuotSMulTop.map_comp_quotEquivOfEq {R : Type u_1} [CommRing R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (x : R) (f : M →ₗ[R] N) : (map x) f ∘ₗ ↑((Ideal.span {x} • ⊤).quotEquivOfEq (x • ⊤) ⋯) = ↑((Ideal.span {x} • ⊤).quotEquivOfEq (x • ⊤) ⋯) ∘ₗ ↑R ((Ideal.span {x}).mapQSMulTop f)

Ideal.mapQSMulTop (x) f is Mathlib's QuotSMulTop.map x f, up to the identification of (x) • ⊤ with x • ⊤.

theorem Ideal.mapQSMulTop_span_singleton_injective {R : Type u_1} [CommRing R] {K : Type u_2} {N : Type u_3} {M : Type u_4} [AddCommGroup K] [Module R K] [AddCommGroup N] [Module R N] [AddCommGroup M] [Module R M] {x : R} {f : K →ₗ[R] N} {g : N →ₗ[R] M} (hfg : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (hM : IsSMulRegular M x) : Function.Injective ⇑((span {x}).mapQSMulTop f)

Reducing a short exact sequence 0 → K → N → M → 0 modulo an element x that is regular on M keeps the first map injective: K ⧸ x K → N ⧸ x N is injective.

theorem QuotSMulTop.ker_mapQ_mkQ {S : Type u_1} {N : Type u_2} [CommRing S] [AddCommGroup N] [Module S N] (I : Ideal S) (y : S) : ((I • ⊤).mapQ (I • ⊤) (y • ⊤).mkQ ⋯).ker = y • ⊤

For an ideal I of S, the map N ⧸ I N → (N ⧸ y N) ⧸ I (N ⧸ y N) has kernel y (N ⧸ I N): both are N ⧸ (I N + y N).

theorem QuotSMulTop.mapQ_mkQ_surjective {S : Type u_1} {N : Type u_2} [CommRing S] [AddCommGroup N] [Module S N] (I : Ideal S) (y : S) : Function.Surjective ⇑((I • ⊤).mapQ (I • ⊤) (y • ⊤).mkQ ⋯)

The map N ⧸ I N → (N ⧸ y N) ⧸ I (N ⧸ y N) is surjective.

noncomputable def QuotSMulTop.quotSpanSingletonComm {R : Type u_1} [CommRing R] (r s : R) : QuotSMulTop r (R ⧸ Ideal.span {s}) ≃ₗ[R] QuotSMulTop s (R ⧸ Ideal.span {r})

Reducing R ⧸ (s) modulo r is reducing R ⧸ (r) modulo s: both are R ⧸ (r, s).

@[simp]

theorem QuotSMulTop.quotSpanSingletonComm_mk_mk {R : Type u_1} [CommRing R] (r s x : R) : (quotSpanSingletonComm r s) (Submodule.Quotient.mk ((Ideal.Quotient.mk (Ideal.span {s})) x)) = Submodule.Quotient.mk ((Ideal.Quotient.mk (Ideal.span {r})) x)

quotSpanSingletonComm sends the class of x to the class of x.

noncomputable def QuotSMulTop.restrictScalarsEquiv {R : Type u_1} [CommRing R] {A : Type u_2} {N : Type u_3} [CommRing A] [Algebra R A] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] (r : R) : QuotSMulTop ((algebraMap R A) r) N ≃ₗ[R] QuotSMulTop r N

Reducing an A-module N modulo the image of r : R in A is reducing the underlying R-module modulo r.

@[simp]

theorem QuotSMulTop.restrictScalarsEquiv_mk {R : Type u_1} [CommRing R] {A : Type u_2} {N : Type u_3} [CommRing A] [Algebra R A] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] (r : R) (x : N) : (restrictScalarsEquiv r) (Submodule.Quotient.mk x) = Submodule.Quotient.mk x

restrictScalarsEquiv sends the class of x to the class of x.

theorem QuotSMulTop.natCard_eq_pow_finrank {R : Type u_1} [CommRing R] (r : R) (M : Type u_4) [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] : Nat.card (QuotSMulTop r M) = Nat.card (R ⧸ Ideal.span {r}) ^ Module.finrank R M

The reduction of a finite free module. A finite free R-module M reduces modulo r to (R ⧸ (r)) ^ finrank R M, so M ⧸ r M has #(R ⧸ (r)) ^ finrank R M elements.

theorem Prime.isSMulRegular_quotient_span_pow {R : Type u_1} [CommRing R] [IsDomain R] {π r : R} (hπ : Prime π) (hr : ¬π ∣ r) (m : ℕ) : IsSMulRegular (R ⧸ Ideal.span {π ^ m}) r

In a domain, if the prime π does not divide r, then r is regular on R ⧸ (π ^ m): π ^ m ∣ r x forces π ^ m ∣ x.