Lifting projective modules from a reduction

Let R be a commutative Noetherian ring, complete with respect to a principal ideal (r), and A an R-algebra, possibly noncommutative, such as the group algebra ℤ_p[G] of a finite group over R = ℤ_p with r = p. Let N be a projective A-module which is finitely generated over R, for instance a finitely generated free A-module when A is finite over R. This file proves that every direct summand of the reduction N ⧸ r • N is the reduction of a direct summand of N. When A is finite over R, a finitely generated projective module over A ⧸ r A is a direct summand of the reduction of a finitely generated free A-module, and is therefore the reduction of a finitely generated projective A-module.

The summand of N ⧸ r • N is cut out by an idempotent endomorphism, which lifts to an idempotent endomorphism of N. Reduction of endomorphisms is onto because N is projective (Ideal.endMapQ_surjective), and its kernel is r • End_A(N) (Ideal.endMapQ_span_algebraMap_eq_zero_iff). The results only assume that the ring End_A(N) is (r)-adically complete, which holds in the setting above because End_A(N) is then finite over R; TauCeti.IsAdicComplete.exists_isIdempotentElem_eq then lifts the idempotent. Over a semiprimary ring the same lifting needs no completeness, the kernel being nil; that case is used in TauCeti/Algebra/Module/ProjectiveCover/Existence.lean.

When r lies in the Jacobson radical of A, the lift is unique up to isomorphism by Ideal.nonempty_linearEquiv_of_quotient_smul_top.

Main results

• TauCeti.exists_isIdempotentElem_endMapQ_eq: idempotent endomorphisms of N ⧸ r • N lift to idempotent endomorphisms of N.
• TauCeti.exists_projective_quotient_smul_top_linearEquiv: every direct summand of N ⧸ r • N is the reduction of a projective submodule of N.

References

• C. W. Curtis, I. Reiner, Methods of Representation Theory, Vol. I, §6.
• T. Y. Lam, A First Course in Noncommutative Rings, §21 and §24.

theorem TauCeti.exists_isIdempotentElem_endMapQ_eq {R : Type u_1} [CommRing R] (r : R) {A : Type u_2} [Ring A] [Algebra R A] {N : Type u_3} [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] [Module.Projective A N] [IsAdicComplete (Ideal.span {r}) (Module.End A N)] {e : Module.End A (N ⧸ Ideal.span {(algebraMap R A) r} • ⊤)} (he : IsIdempotentElem e) : ∃ (f : Module.End A N), IsIdempotentElem f ∧ ((Ideal.span {(algebraMap R A) r}).endMapQ N) f = e

Idempotents lift from the reduction modulo r. For a projective A-module N whose endomorphism ring is (r)-adically complete, every idempotent endomorphism of N ⧸ r • N is the reduction of an idempotent endomorphism of N.

The completeness hypothesis holds when R is Noetherian and (r)-adically complete and N is finitely generated over R, by Module.Finite.linearMap_of_isNoetherianRing and IsAdicComplete.of_finite.

theorem TauCeti.exists_projective_quotient_smul_top_linearEquiv {R : Type u_1} [CommRing R] (r : R) {A : Type u_2} [Ring A] [Algebra R A] {N : Type u_3} [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] [Module.Projective A N] [IsAdicComplete (Ideal.span {r}) (Module.End A N)] {Y : Type u_4} [AddCommGroup Y] [Module A Y] (i : Y →ₗ[A] N ⧸ Ideal.span {(algebraMap R A) r} • ⊤) (q : N ⧸ Ideal.span {(algebraMap R A) r} • ⊤ →ₗ[A] Y) (hqi : q ∘ₗ i = LinearMap.id) : ∃ (X : Submodule A N), Module.Projective A ↥X ∧ Nonempty ((↥X ⧸ Ideal.span {(algebraMap R A) r} • ⊤) ≃ₗ[A] Y)

Direct summands lift from the reduction modulo r. Let N be a projective A-module whose endomorphism ring is (r)-adically complete, and let Y be a direct summand of N ⧸ r • N, given by maps i : Y → N ⧸ r • N and q : N ⧸ r • N → Y with q ∘ i = id. Then Y ≃ X ⧸ r • X for a projective submodule X of N, namely the range of an idempotent lifting i ∘ q.

In particular, when A is finite over R, a finitely generated projective module over A ⧸ r A, which is a direct summand of the reduction of a finitely generated free A-module, is the reduction of a projective A-module, finitely generated when R is Noetherian.