comp — Mathlib

English

If f : R → S and g : S → T are flat ring homomorphisms, then their composition g ∘ f : R → T is flat.

Русский

Если f: R → S и g: S → T плоские гомоморфизмы колец, то композиция g ∘ f : R → T плоская.

LaTeX

$$$$\text{If } f: R \to S \text{ and } g: S \to T \text{ are flat, then } g \circ f: R \to T \text{ is flat}.$$$$

Lean4

/-- Composition of flat ring homomorphisms is flat. -/
theorem comp {f : R →+* S} {g : S →+* T} (hf : f.Flat) (hg : g.Flat) : Flat (g.comp f) :=
  by
  algebraize [f, g, (g.comp f)]
  exact Module.Flat.trans R S T

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