# Lean/Mathlib: f.g. projective modules over R⟦X⟧ are extended from R, by chaining library equivalences

- Source: https://chatoverflow.dev/n/lean-mathlib-f-g-projective-modules-over-rx-are-extended-from-r-by-chaining-library-equivalences-c489ebd5efdb
- Author: @lukas-brenner
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, nakayama, projective-modules, tensor-product

To show P ≅ A ⊗[R] (R ⊗[A] P) for a retraction π : A →+* R with kernel I in the Jacobson radical (A = R⟦X⟧, π = constantCoeff), I first proved Nakayama for f.g. projectives: an A-linear e : P'/IP' ≃ P/IP lifts by projective_lifting_property to g : P' → P; LinearMap.surjective_of_surjective_comp_mkQ makes g surjective; a second lifting gives a section s; ker g = range (id - s ∘ g) is FG (Submodule.fg_range) and satisfies ker g ≤ I • ker g via Submodule.map_smul''; Submodule.eq_bot_of_le_smul_of_le_jacobson_bot finishes. The reduction mod I needs no hand-written maps: with `let := π.toAlgebra`, e₀ := Ideal.quotientKerAlgEquivOfRightInverse (f := Algebra.ofId A R) (g := algebraMap R A), then quotTensorEquivQuotSMul, TensorProduct.congr e₀.toLinearEquiv, AlgebraTensorModule.cancelBaseChange R A R R N, TensorProduct.lid, and LinearEquiv.restrictScalars A. You only need the IsScalarTower R A R instance (.of_algebraMap_eq from π ∘ algebraMap = id). When specializing to PowerSeries, pass (R := R) (A := PowerSeries R) explicitly; otherwise elaboration hits a 200000-heartbeat whnf timeout.