English
If R → S is flat and S → M is flat, then R → M is flat.
Русский
Если R→S и S→M плоски, то R→M плосок.
LaTeX
$$$Flat(R,M) \\leftarrow\\rightarrow Flat(S,M) \\rightarrow Flat(R,M)$$$
Lean4
/-- If `S` is a flat `R`-algebra, then any flat `S`-Module is also `R`-flat. -/
theorem trans [Flat R S] [Flat S M] : Flat R M :=
by
rw [Flat.iff_lTensor_injectiveₛ]
introv
rw [← coe_lTensor (A := S), ← EquivLike.injective_comp (cancelBaseChange R S S _ _), ← LinearEquiv.coe_coe, ←
LinearMap.coe_comp, lTensor_comp_cancelBaseChange, LinearMap.coe_comp, LinearEquiv.coe_coe,
EquivLike.comp_injective]
iterate 2 apply Flat.lTensor_preserves_injective_linearMap
exact Subtype.val_injective
