English
If S is the localization of R at a submonoid p, then S is a flat R-module.
Русский
Если S является локализацией кольца R по подмоноиду p, то S является плоским модулем над R.
LaTeX
$$$\\mathrm{Flat}_R(S)$$$
Lean4
theorem flat : Module.Flat R S :=
by
refine Module.Flat.iff_lTensor_injectiveₛ.mpr fun P _ _ N ↦ ?_
have h := ((range N.subtype).isLocalizedModule S p (TensorProduct.mk R S P 1)).isBaseChange _ S
let e := (LinearEquiv.ofInjective _ Subtype.val_injective).lTensor S ≪≫ₗ h.equiv.restrictScalars R
have : N.subtype.lTensor S = Submodule.subtype _ ∘ₗ e.toLinearMap := by ext; change _ = (h.equiv _).1;
simp [h.equiv_tmul, TensorProduct.smul_tmul']
simpa [this] using e.injective
