English
Independence of a family can be characterized via iSupIndep; the iSupIndep property is equivalent to a family of DFinsupps being independent in sum.
Русский
Независимость семейства может быть охарактеризована через iSupIndep; свойство iSupIndep эквивалентно независимости семейства DFinsupp.
LaTeX
$$$iSupIndep p$ is equivalent to a certain injectivity condition on dfinsupp lsum maps$$
Lean4
/-- 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. -/
theorem biSup_eq_range_dfinsupp_lsum (p : ι → Prop) [DecidablePred p] (S : ι → Submodule R N) :
⨆ (i) (_ : p i), S i =
LinearMap.range (LinearMap.comp (DFinsupp.lsum ℕ (fun i => (S i).subtype)) (DFinsupp.filterLinearMap R _ p)) :=
by
apply le_antisymm
· refine iSup₂_le fun i hi y hy => ⟨DFinsupp.single i ⟨y, hy⟩, ?_⟩
rw [LinearMap.comp_apply, filterLinearMap_apply, filter_single_pos _ _ hi]
simp only [lsum_apply_apply, sumAddHom_single, LinearMap.toAddMonoidHom_coe, coe_subtype]
· rintro x ⟨v, rfl⟩
refine dfinsuppSumAddHom_mem _ _ _ fun i _ => ?_
refine mem_iSup_of_mem i ?_
by_cases hp : p i
· simp [hp]
· simp [hp]
