English
The sum-closure (as an AddSubmonoid) of the supremum over a set of submodules equals the supremum of the corresponding AddSubmonoids.
Русский
Замыкание суммы (как AddSubmonoid) над верхней границей множества подмодулей равно верхней границе AddSubmonoids, соответствующей этому множеству.
LaTeX
$$$\\text{toAddSubmonoid }(sSup\, S) = sSup\\bigl(\\text{toAddSubmonoid } '' S\\bigr)$$$
Lean4
@[simp]
theorem toAddSubmonoid_sSup (s : Set (Submodule R M)) : (sSup s).toAddSubmonoid = sSup (toAddSubmonoid '' s) :=
by
let p : Submodule R M :=
{ toAddSubmonoid := sSup (toAddSubmonoid '' s)
smul_mem' := fun t {m} h ↦
by
simp_rw [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, sSup_eq_iSup'] at h ⊢
induction h using AddSubmonoid.iSup_induction' with
| mem p x hx =>
obtain ⟨-, ⟨p : Submodule R M, hp : p ∈ s, rfl⟩⟩ := p
suffices p.toAddSubmonoid ≤ ⨆ q : toAddSubmonoid '' s, (q : AddSubmonoid M) by exact this (smul_mem p t hx)
apply le_sSup
rw [Subtype.range_coe_subtype]
exact ⟨p, hp, rfl⟩
| zero => simpa only [smul_zero] using zero_mem _
| add _ _ _ _ mx my => revert mx my; simp_rw [smul_add]; exact add_mem }
refine le_antisymm (?_ : sSup s ≤ p) ?_
· exact sSup_le fun q hq ↦ le_sSup <| Set.mem_image_of_mem toAddSubmonoid hq
· exact sSup_le fun _ ⟨q, hq, hq'⟩ ↦ hq'.symm ▸ le_sSup hq
