coeAlgEquiv — Mathlib

English

If A is the ambient algebra and M(i) are submodules giving an internal direct sum, then A is isomorphic to the direct sum of the M(i).

Русский

Если A — окружающая алгебра, а M(i) образуют внутренний прямой сумм, то A изоморфна прямой сумме M(i).

LaTeX

$$$A \cong_R \bigoplus_i M(i)$ when DirectSum.IsInternal M holds.$$

Lean4

/-- The canonical isomorphism of an internal direct sum with the ambient algebra -/
noncomputable def coeAlgEquiv (hM : DirectSum.IsInternal M) : (DirectSum ι fun i => ↥(M i)) ≃ₐ[R] A :=
  { RingEquiv.ofBijective (DirectSum.coeAlgHom M) hM with commutes' := fun r => by simp }

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