English
Assume G acts on α and α acts on β in a tower fashion, so that g • (a • b) = (g • a) • b. Then stabilizer of a is contained in stabilizer of a • b: if g fixes a, it fixes a • b as well.
Русский
Пусть G действует на α и α действует на β, образуя тензор скаляров. Тогда стабилизатор a в G содержится в стабилизаторе a•b: если g фиксирует a, то фиксирует и a•b.
LaTeX
$$\operatorname{Stab}_G(a) \le \operatorname{Stab}_G(a \cdot b)$$
Lean4
@[to_additive]
theorem le_stabilizer_smul_left [SMul α β] [IsScalarTower G α β] (a : α) (b : β) :
stabilizer G a ≤ stabilizer G (a • b) := by simp_rw [SetLike.le_def, mem_stabilizer_iff, ← smul_assoc]; rintro a h;
rw [h]
-- This lemma does not need `MulAction G α`, only `SMul G α`.
-- We use `G'` instead of `G` to locally reduce the typeclass assumptions.
