iff_flat_and_ideal_smul_eq_top — Mathlib

English

Faithfully flatness of M is equivalent to flatness plus a condition on ideals I: if I times the top submodule equals the top, then I must be the top ideal.

Русский

Плоскость через идеалы: если I · ⊤ = ⊤, то I = ⊤.

LaTeX

$$FaithfullyFlat R M ↔ (Flat R M ∧ ∀ I, I ≠ ⊤ → I · ⊤ ≠ ⊤)$$

Lean4

theorem iff_flat_and_ideal_smul_eq_top :
    FaithfullyFlat R M ↔ (Flat R M ∧ ∀ (I : Ideal R), I • (⊤ : Submodule R M) = ⊤ → I = ⊤) :=
  iff_flat_and_proper_ideal R M |>.trans <|
    and_congr_right_iff.2 fun _ => iff_of_eq <| forall_congr fun I => eq_iff_iff.2 <| by tauto

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