English
If a group G acts on a monoid M and on a scalar target α, and the usual scalar-tower relations hold between G, M, and α, then the tower also holds for the unit group Mˣ acting on α. In other words, the scalar-tower structure transfers from M to its group of units.
Русский
Если группа G действует на моноид M и на множество α, причём выполняются обычные тензорно-скалярные соотношения между G, M и α, то структура скалярной башни переносится на группу обратимых элементов Mˣ, действующих на α. Иными словами, цепь скаляров переходит от M к Mˣ.
LaTeX
$$$\text{If } G \text{ is a group } M \text{ a monoid } α \text{ with } (G \curvearrowright M), (M \curvearrowright α), \text{ and } IsScalarTower(G, M, M), IsScalarTower(G, M, α), \text{ then } IsScalarTower(G, M^{\times}, α).$$$
Lean4
/-- Transfer `IsScalarTower G M α` to `IsScalarTower G Mˣ α`. -/
@[to_additive /-- Transfer `VAddAssocClass G M α` to `VAddAssocClass G (AddUnits M) α`. -/
]
instance isScalarTower'_left [Group G] [Monoid M] [MulAction G M] [SMul M α] [SMul G α] [SMulCommClass G M M]
[IsScalarTower G M M] [IsScalarTower G M α] : IsScalarTower G Mˣ α where
smul_assoc g
m :=
smul_assoc g
(m : M)
-- Just to prove this transfers a particularly useful instance.
