English
Bijective ring homomorphisms are FaithfullyFlat.
Русский
Biективные кольцевые гомоморфизмы FaithfullyFlat.
LaTeX
$$$\\operatorname{of\\_bijective}\\;hf \\Rightarrow f^{\\mathrm{FaithfullyFlat}}$$$
Lean4
/-- If `S` is a finite `R`-algebra, then `S' = M⁻¹S` is a finite `R' = M⁻¹R`-algebra. -/
theorem finite_localizationPreserves : RingHom.LocalizationPreserves @RingHom.Finite :=
by
introv R hf
letI := f.toAlgebra
letI := ((algebraMap S S').comp f).toAlgebra
let f' : R' →+* S' := IsLocalization.map S' f (Submonoid.le_comap_map M)
letI := f'.toAlgebra
have : IsScalarTower R R' S' := IsScalarTower.of_algebraMap_eq' (IsLocalization.map_comp M.le_comap_map).symm
have : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' rfl
have : IsLocalization (Algebra.algebraMapSubmonoid S M) S' := by
rwa [Algebra.algebraMapSubmonoid, RingHom.algebraMap_toAlgebra]
have : Module.Finite R S := hf
exact .of_isLocalization R S M
