English
The adjoin of the union of the images of s under inl and t under inr equals the product of the adjoins of s and t.
Русский
Замыкание от объединения образов s через inl и t через inr равно произведению замыканий s и t.
LaTeX
$$$ adjoin\ R (LinearMap.inl R A B '' (s \u222a {1}) \cup LinearMap.inr R A B '' (t \u222a {1})) = (adjoin R s).prod (adjoin R t) $$$
Lean4
theorem adjoin_inl_union_inr_eq_prod (s) (t) :
adjoin R (LinearMap.inl R A B '' (s ∪ { 1 }) ∪ LinearMap.inr R A B '' (t ∪ { 1 })) =
(adjoin R s).prod (adjoin R t) :=
by
apply le_antisymm
·
simp only [adjoin_le_iff, Set.insert_subset_iff, Subalgebra.zero_mem, Subalgebra.one_mem, subset_adjoin,
-- the rest comes from `squeeze_simp`
Set.union_subset_iff, LinearMap.coe_inl, Set.mk_preimage_prod_right, Set.image_subset_iff, SetLike.mem_coe,
Set.mk_preimage_prod_left, LinearMap.coe_inr, and_self_iff, Set.union_singleton, Subalgebra.coe_prod]
· rintro ⟨a, b⟩ ⟨ha, hb⟩
let P := adjoin R (LinearMap.inl R A B '' (s ∪ { 1 }) ∪ LinearMap.inr R A B '' (t ∪ { 1 }))
have Ha : (a, (0 : B)) ∈ adjoin R (LinearMap.inl R A B '' (s ∪ { 1 })) :=
mem_adjoin_of_map_mul R LinearMap.inl_map_mul ha
have Hb : ((0 : A), b) ∈ adjoin R (LinearMap.inr R A B '' (t ∪ { 1 })) :=
mem_adjoin_of_map_mul R LinearMap.inr_map_mul hb
replace Ha : (a, (0 : B)) ∈ P := adjoin_mono Set.subset_union_left Ha
replace Hb : ((0 : A), b) ∈ P := adjoin_mono Set.subset_union_right Hb
simpa [P] using Subalgebra.add_mem _ Ha Hb
