Group actions on and by Mˣ #
This file provides the action of a unit on a type α, SMul Mˣ α, in the presence of
SMul M α, with the obvious definition stated in Units.smul_def. This definition preserves
MulAction and DistribMulAction structures too.
Additionally, a MulAction G M for some group G satisfying some additional properties admits a
MulAction G Mˣ structure, again with the obvious definition stated in Units.coe_smul.
These instances use a primed name.
The results are repeated for AddUnits and VAdd where relevant.
Equations
Equations
Equations
Equations
Action of a group G on units of M #
If an action G associates and commutes with multiplication on M, then it lifts to an
action on Mˣ. Notably, this provides MulAction Mˣ Nˣ under suitable conditions.
Equations
Equations
Note that this lemma exists more generally as the global smul_inv
Transfer SMulCommClass G H M to SMulCommClass G H Mˣ.
Transfer VAddCommClass G H M to VAddCommClass G H (AddUnits M).
Transfer IsScalarTower G H M to IsScalarTower G H Mˣ.
Transfer VAddAssocClass G H M to VAddAssocClass G H (AddUnits M).
Transfer IsScalarTower G M α to IsScalarTower G Mˣ α.
Transfer VAddAssocClass G M α to VAddAssocClass G (AddUnits M) α.
Note this has different defeqs than Units.mulAction', but doesn't create a diamond
with it in non-degenerate situations. Indeed, to get a diamond on MulDistribMulAction G Mˣ,
we would need both instances to fire. But Units.mulAction' assumes SMulCommClass G M M,
i.e. ∀ (g : G) (m₁ m₂ : M), g • (m₁ * m₂) = m₁ * g • m₂), while
Units.instMulDistribMulActionRight assumes MulDistribMulAction G M,
i.e. ∀ (g : G) (m₁ m₂ : M), g • (m₁ * m₂) = g • m₁ * g • m₂.
In particular, if M is cancellative, then we obtain ∀ (g : G) (m : M), g • m = m,
i.e. the action is trivial!
This however does create a (propeq) diamond for MulDistribMulAction (ConjAct Mˣ) Mˣ with
ConjAct.unitsMulDistribMulAction and ConjAct.instMulDistribMulAction. Indeed, if we go down
one way then u • v := ⟨ofConjAct u * v * ofConjAct u⁻¹, ofConjAct u * v⁻¹ * ofConjAct u⁻¹, _, _⟩,
while the other way is
u • v := ⟨ofConjAct u * v * ofConjAct u⁻¹, ofConjAct u * (v⁻¹ * ofConjAct u⁻¹), _, _⟩.