coeAlgHom_of — Mathlib

English

The supremum of submodules indexed by i equals the range of the corresponding DirectSum coercion; equivalently, iSup_eq_toSubmodule_range.

Русский

Супремум подмодулей, индексируемых i, равен диапазону соответствующего DirectSum коэфф.

LaTeX

$$$$\\operatorname{iSup} \\; A = \\operatorname{Submodule}.toSubmodule(\\mathrm{DirectSum.coeAlgHom} A).range.$$$$

Lean4

@[simp]
theorem coeAlgHom_of [AddMonoid ι] [CommSemiring S] [Semiring R] [Algebra S R] (A : ι → Submodule S R)
    [SetLike.GradedMonoid A] (i : ι) (x : A i) : DirectSum.coeAlgHom A (DirectSum.of (fun i => A i) i x) = x :=
  DirectSum.toSemiring_of _ (by rfl) (fun _ _ => (by rfl)) _ _

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