English
The supremum of a family of additive submonoids equals the range of the dfinsupp sumAddHom composed withSubtype maps; every element of the supremum is obtained by a finite linear combination.
Русский
Объединение по верхной границе множества подмоноидов равно образу dfinsupp sumAddHom, получаемому суммированием элементов соответствующего подмножества.
LaTeX
$$$\iSup S = \mathrm{mrange}(\mathrm{sumAddHom}(\lambda i, (S i).subtype))$$$
Lean4
/-- The bounded supremum of a family of commutative additive submonoids is equal to the range of
`DFinsupp.sumAddHom` composed with `DFinsupp.filterAddMonoidHom`; 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 bsupr_eq_mrange_dfinsuppSumAddHom (p : ι → Prop) [DecidablePred p] [AddCommMonoid γ] (S : ι → AddSubmonoid γ) :
⨆ (i) (_ : p i), S i = AddMonoidHom.mrange ((sumAddHom fun i => (S i).subtype).comp (filterAddMonoidHom _ p)) :=
by
apply le_antisymm
· refine iSup₂_le fun i hi y hy => ⟨DFinsupp.single i ⟨y, hy⟩, ?_⟩
rw [AddMonoidHom.comp_apply, filterAddMonoidHom_apply, filter_single_pos _ _ hi]
exact sumAddHom_single _ _ _
· rintro x ⟨v, rfl⟩
refine dfinsuppSumAddHom_mem _ _ _ fun i _ => ?_
refine AddSubmonoid.mem_iSup_of_mem i ?_
by_cases hp : p i
· simp [hp]
· simp [hp]
