Reduction of endomorphisms modulo I • M

An endomorphism of a module M carries I • M into itself, so it descends to the quotient M ⧸ I • M, and the descent is a ring homomorphism Ideal.endMapQ I M. This file constructs that reduction map and proves the two properties that make idempotents lift along it: it is surjective when M is projective, and its kernel consists of nilpotent elements when I is nilpotent.

The kernel is characterized by Ideal.mem_ker_endMapQ_iff: an endomorphism dies under reduction exactly when its image lies in I • M. Iterating that containment is what makes the kernel nil, the image of the k-th power lying in I ^ k • M. When I is generated by the image of a central scalar r and M is projective, the kernel is r • End(M) (Ideal.endMapQ_span_algebraMap_eq_zero_iff); this is the form in which idempotents lift along the reduction map over an (r)-adically complete base, where the kernel is not nil.

Main definitions

• Ideal.endMapQ: reduction of endomorphisms modulo I • M, as a ring homomorphism Module.End R M →+* Module.End R (M ⧸ I • ⊤).

Main results

• Ideal.mem_ker_endMapQ_iff: the kernel of the reduction map consists of the endomorphisms with image inside I • M.
• Ideal.endMapQ_surjective: reduction is onto when M is projective.
• Ideal.endMapQ_span_algebraMap_eq_zero_iff: for a projective module and the ideal generated by a central scalar r, the kernel of the reduction map is r • End(M).
• Ideal.range_pow_le_of_mem_ker_endMapQ and Ideal.isNilpotent_of_mem_ker_endMapQ: an endomorphism killed by reduction has k-th power with image inside I ^ k • M, hence is nilpotent as soon as I is.

def Ideal.endMapQ {R : Type u} [Ring R] (I : Ideal R) (M : Type v) [AddCommGroup M] [Module R M] : Module.End R M →+* Module.End R (M ⧸ I • ⊤)

Reduction of endomorphisms modulo I • M. An endomorphism of M carries I • M into itself, so it descends to the quotient M ⧸ I • M, and the descent is a ring homomorphism.

Equations

• I.endMapQ M = { toFun := fun (f : Module.End R M) => (I • ⊤).mapQ (I • ⊤) f ⋯, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Ideal.endMapQ_mk {R : Type u} [Ring R] (I : Ideal R) (M : Type v) [AddCommGroup M] [Module R M] (f : Module.End R M) (x : M) : ((I.endMapQ M) f) (Submodule.Quotient.mk x) = Submodule.Quotient.mk (f x)

theorem Ideal.endMapQ_surjective {R : Type u} [Ring R] (I : Ideal R) (M : Type v) [AddCommGroup M] [Module R M] [Module.Projective R M] : Function.Surjective ⇑(I.endMapQ M)

Every endomorphism of M ⧸ I • M is the reduction of an endomorphism of M, provided M is projective: lift the composite M ↠ M ⧸ I • M → M ⧸ I • M through the quotient map.

theorem Ideal.mem_ker_endMapQ_iff {R : Type u} [Ring R] (I : Ideal R) (M : Type v) [AddCommGroup M] [Module R M] {f : Module.End R M} : f ∈ RingHom.ker (I.endMapQ M) ↔ LinearMap.range f ≤ I • ⊤

The kernel of the reduction map. An endomorphism reduces to zero exactly when its image lies in I • M, membership in the kernel being tested on the classes of M ⧸ I • M.

theorem Ideal.range_pow_le_of_mem_ker_endMapQ {R : Type u} [Ring R] (I : Ideal R) (M : Type v) [AddCommGroup M] [Module R M] {f : Module.End R M} (hf : f ∈ RingHom.ker (I.endMapQ M)) (k : ℕ) : LinearMap.range (f ^ k) ≤ I ^ k • ⊤

An endomorphism killed by the reduction map has image inside I • M, hence k-th power with image inside I ^ k • M.

theorem Ideal.isNilpotent_of_mem_ker_endMapQ {R : Type u} [Ring R] (I : Ideal R) (M : Type v) [AddCommGroup M] [Module R M] (hI : IsNilpotent I) {f : Module.End R M} (hf : f ∈ RingHom.ker (I.endMapQ M)) : IsNilpotent f

The kernel of the reduction map is nil when I is nilpotent: an endomorphism with image in I • M has a vanishing power, because I ^ k • M vanishes.

theorem Ideal.endMapQ_span_algebraMap_eq_zero_iff {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (r : R) {N : Type u_3} [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] [Module.Projective A N] (f : Module.End A N) : ((span {(algebraMap R A) r}).endMapQ N) f = 0 ↔ ∃ (g : Module.End A N), r • g = f

The kernel of reduction modulo r. An endomorphism of a projective A-module N reduces to zero on N ⧸ r • N exactly when it is r times an endomorphism of N.