English
If A is commutative, then for Subalgebras S,T of A, the equality (S.toSubmodule)*(T.toSubmodule) = (S ⊔ T).toSubmodule holds.
Русский
Если A коммутативно, то для подалгебр S и T верно равенство подмодулей: (S.⋅T) = (S ⊔ T).
LaTeX
$$(toSubmodule S) * (toSubmodule T) = toSubmodule(S ⊔ T)$$
Lean4
/-- When `A` is commutative, `Subalgebra.mul_toSubmodule_le` is strict. -/
theorem mul_toSubmodule {R : Type*} {A : Type*} [CommSemiring R] [CommSemiring A] [Algebra R A] (S T : Subalgebra R A) :
(Subalgebra.toSubmodule S) * (Subalgebra.toSubmodule T) = Subalgebra.toSubmodule (S ⊔ T) :=
by
refine le_antisymm (mul_toSubmodule_le _ _) ?_
rintro x (hx : x ∈ Algebra.adjoin R (S ∪ T : Set A))
refine
Algebra.adjoin_induction (fun x hx => ?_) (fun r => ?_) (fun _ _ _ _ => Submodule.add_mem _)
(fun x y _ _ hx hy => ?_) hx
· rcases hx with hxS | hxT
· rw [← mul_one x]
exact Submodule.mul_mem_mul hxS (show (1 : A) ∈ T from one_mem T)
· rw [← one_mul x]
exact Submodule.mul_mem_mul (show (1 : A) ∈ S from one_mem S) hxT
· rw [← one_mul (algebraMap _ _ _)]
exact Submodule.mul_mem_mul (show (1 : A) ∈ S from one_mem S) (algebraMap_mem T _)
have := Submodule.mul_mem_mul hx hy
rwa [mul_assoc, mul_comm _ (Subalgebra.toSubmodule T), ← mul_assoc _ _ (Subalgebra.toSubmodule S),
isIdempotentElem_toSubmodule, mul_comm T.toSubmodule, ← mul_assoc, isIdempotentElem_toSubmodule] at this
