English
Let S be a commutative semiring, R a semiring, and M an additive commutative monoid with suitable module structures. The range of the map inlAlgHom together with the algebra generated by the range of inr spans the entire target algebra; i.e., their supremum is the top subalgebra.
Русский
Пусть S — коммутативная полугруппа, R — полугруппа, M — аддитивная коммутативная моноидальная структура, и заданы подходящие модулярные структуры. Образ inlAlgHom и адjoin (range inr) вместе порождают всю целевую алгебру; то есть их верхняя граница достигает максимального подалгебры.
LaTeX
$$$(inlAlgHom\\ S\\ R\\ M).range \\sqcup Algebra.adjoin\\ S\\ (Set.range inr) = (\\top : Subalgebra S (tsze R M))$$$
Lean4
@[simp]
theorem range_inlAlgHom_sup_adjoin_range_inr :
(inlAlgHom S R M).range ⊔ Algebra.adjoin S (Set.range inr) = (⊤ : Subalgebra S (tsze R M)) :=
by
refine top_unique fun x hx => ?_; clear hx
rw [← x.inl_fst_add_inr_snd_eq]
refine add_mem ?_ ?_
· exact le_sup_left (α := Subalgebra S _) <| Set.mem_range_self x.fst
· exact le_sup_right (α := Subalgebra S _) <| Algebra.subset_adjoin <| Set.mem_range_self x.snd
