Theorems · Theorem · linear algebra

Submodule.biSup_eq_range_dfinsupp_lsum

∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : Module R N]
  [inst_3 : DecidableEq ι] (p : ι → Prop) [inst_4 : DecidablePred p] (S : ι → Submodule R N),
  ⨆ i, ⨆ (_ : p i), S i =
    (((DFinsupp.lsum ℕ) fun i => (S i).subtype) ∘ₗ DFinsupp.filterLinearMap R (fun i => ↥(S i)) p).range

The bounded supremum of a family of commutative additive submonoids is equal to the range of DFinsupp.sumAddHom composed with DFinsupp.filter_add_monoid_hom; that is, every element in the bounded iSup can be produced from taking a finite number of non-zero elements from the S i that satisfy p i, coercing them to γ, and summing them.

Defined in

Mathlib.LinearAlgebra.DFinsupp

Cited by

1 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAddCommMonoidModuleDecidableEqDecidablePred