rank_le_one_of_commute_of_flat_of_self

English

If M and N are linearly disjoint and one is flat, then the rank of the intersection M ⊓ N is at most 1 under compatible commuting conditions.

Русский

Если M и N линейно раздельны и хотя бы один из них плоский, то ранг пересечения M ⊓ N не превышает 1 при совместном коммутировании элементов.

LaTeX

$$Module.rank R ↥(M ⊓ N) ≤ 1$$

Lean4

/-- If `M` and itself are linearly disjoint, if `M` is flat,
if any two elements of `M` are commutative, then the rank of `M` is at most one. -/
theorem rank_le_one_of_commute_of_flat_of_self (H : M.LinearDisjoint M) [Module.Flat R M]
    (hc : ∀ (m n : M), Commute m.1 n.1) : Module.rank R M ≤ 1 :=
  by
  rw [← inf_of_le_left (le_refl M)] at hc ⊢
  exact H.rank_inf_le_one_of_commute_of_flat_left hc

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