English
Let S ⊆ T be subalgebras of A over R, and X a type with SMul X R, SMul X A, and IsScalarTower X R A. Then the induced action makes IsScalarTower X S T hold; i.e., for all x ∈ X, s ∈ S, t ∈ T, (x • s) • t = x • (s • t).
Русский
Пусть S ⊆ T — подпалгебры A над R, и X множество с действиями SMul X R и SMul X A и условием IsScalarTower X R A. Тогда индуцированное действие задаёт IsScalarTower X S T, то есть для всех x ∈ X, s ∈ S, t ∈ T верно (x • s) • t = x • (s • t).
LaTeX
$$$\forall x \in X,\forall s \in S,\forall t \in T,\ (x \cdot s) \cdot t = x \cdot (s \cdot t)$$$
Lean4
scoped instance isScalarTower_left (X) [SMul X R] [SMul X A] [IsScalarTower X R A] :
letI := (inclusion h).toModule;
IsScalarTower X S T :=
letI := (inclusion h).toModule
⟨fun x s t ↦
Subtype.ext <|
by
rw [← one_smul R s, ← smul_assoc, one_smul, ← one_smul R (s • t), ← smul_assoc, Algebra.smul_def,
Algebra.smul_def]
apply mul_assoc⟩
