English
Let R be a semiring and M, M′ be AddCommMonoid modules over R. The sum of the first-projection submodule and the second-projection submodule of the product M × M′ equals the whole product; i.e., their join is the top submodule of M × M′.
Русский
Пусть R — полугруппа, M и M′ — модули над R. Сумма подпространств первых и вторых проекций под произведением M × M′ равна всему M × M′; то есть их наибольшая верхняя граница равна верхнему подпространству.
LaTeX
$$$\operatorname{fst} R M M' \sqcup \operatorname{snd} R M M' = \top$$$
Lean4
theorem fst_sup_snd : Submodule.fst R M M₂ ⊔ Submodule.snd R M M₂ = ⊤ :=
by
rw [eq_top_iff]
rintro ⟨m, n⟩ -
rw [show (m, n) = (m, 0) + (0, n) by simp]
apply Submodule.add_mem (Submodule.fst R M M₂ ⊔ Submodule.snd R M M₂)
· exact Submodule.mem_sup_left (Submodule.mem_comap.mpr (by simp))
· exact Submodule.mem_sup_right (Submodule.mem_comap.mpr (by simp))
