FaithfullyFlat — Mathlib

English

A ring map is faithfully flat if and only if S is faithfully flat as an R-algebra.

Русский

Кольцевое отображение является верно плоским (faithfully flat) тогда и только тогда, когда S является faithfully flat как R–алгебра.

LaTeX

$$$\\text{FaithfullyFlat}(f) \\iff \\operatorname{Module.FaithfullyFlat}(R,S)$$$

Lean4

/-- A ring map `f : R →+* S` is faithfully flat if `S` is faithfully flat as an `R`-algebra. -/
@[stacks 00HB "Part (4)", algebraize Module.FaithfullyFlat]
def FaithfullyFlat {R S : Type*} [CommRing R] [CommRing S] (f : R →+* S) : Prop :=
  letI : Algebra R S := f.toAlgebra
  Module.FaithfullyFlat R S

Похожие утверждения