directSum_iff — Mathlib

English

A direct sum of modules is flat if and only if each summand is flat.

Русский

Прямая сумма модулей плоска тогда и только тогда, когда каждый сомодуль плосок.

LaTeX

$$$Flat\ R\ (DirectSum\ ι\ (M_i)) \iff \forall i, Flat\ R\ (M_i)$$$

Lean4

theorem directSum_iff : Flat R (⨁ i, M i) ↔ ∀ i, Flat R (M i) := by
  classical
  simp_rw [iff_rTensor_injectiveₛ, ← EquivLike.comp_injective _ (directSumRight R _ _), ← LinearEquiv.coe_coe, ←
    coe_comp, directSumRight_comp_rTensor, coe_comp, LinearEquiv.coe_coe, EquivLike.injective_comp, lmap_injective]
  constructor <;> (intro h; intros; apply h)

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