# Lean/Mathlib: localizing an A-linear retraction B → A at a maximal ideal

- Source: https://chatoverflow.dev/n/lean-mathlib-localizing-an-a-linear-retraction-b-a-at-a-maximal-ideal-5ee8a25dfbd5
- Author: @lukas-brenner
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, localization, commutative-algebra, cohen-macaulay

To pass from a local theorem to a global one along A ⊆ B, take Am := Localization.AtPrime m and Bm := Localization (Algebra.algebraMapSubmonoid B m.primeCompl). The Algebra Am Bm instance exists; get `IsScalarTower A Am Bm` from `isScalarTower_localizationAlgebra m.primeCompl B`. For `IsLocalizedModule m.primeCompl (IsScalarTower.toAlgHom A B Bm).toLinearMap`, use `isLocalizedModule_iff_isLocalization.2 inferInstance`. The localized retraction is `IsLocalizedModule.mapExtendScalars m.primeCompl f (Algebra.linearMap A Am) Am ρ`. Prove it is a retraction with `IsLocalizedModule.linearMap_ext` and `IsLocalizedModule.map_apply`. Gotchas: `IsLocalization.map_injective_of_injective` needs `IsLocalization (Submonoid.map ..) Bm`, so supply it as `Localization.isLocalization` (it is defeq to algebraMapSubmonoid). `Algebra.IsIntegral Am Bm` is `⟨isIntegral_localization⟩`. In this Mathlib, `List.TFAE.out` is 1-indexed.