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.

instance Units.instSMul {M : Type u_3} {α : Type u_5} [Monoid M] [SMul M α] : SMul Mˣ α

Equations

• Units.instSMul = { smul := fun (m : Mˣ) (a : α) => ↑m • a }

instance AddUnits.instVAdd {M : Type u_3} {α : Type u_5} [AddMonoid M] [VAdd M α] : VAdd (AddUnits M) α

Equations

• AddUnits.instVAdd = { vadd := fun (m : AddUnits M) (a : α) => ↑m +ᵥ a }

theorem Units.smul_def {M : Type u_3} {α : Type u_5} [Monoid M] [SMul M α] (m : Mˣ) (a : α) : m • a = ↑m • a

theorem AddUnits.vadd_def {M : Type u_3} {α : Type u_5} [AddMonoid M] [VAdd M α] (m : AddUnits M) (a : α) : m +ᵥ a = ↑m +ᵥ a

@[simp]

theorem Units.smul_mk_apply {M : Type u_6} {α : Type u_7} [Monoid M] [SMul M α] (m n : M) (h₁ : m * n = 1) (h₂ : n * m = 1) (a : α) : { val := m, inv := n, val_inv := h₁, inv_val := h₂ } • a = m • a

theorem AddUnits.vadd_mk_apply {M : Type u_6} {α : Type u_7} [AddMonoid M] [VAdd M α] (m n : M) (h₁ : m + n = 0) (h₂ : n + m = 0) (a : α) : { val := m, neg := n, val_neg := h₁, neg_val := h₂ } +ᵥ a = m +ᵥ a

@[simp]

theorem Units.smul_isUnit {M : Type u_3} {α : Type u_5} [Monoid M] [SMul M α] {m : M} (hm : IsUnit m) (a : α) : hm.unit • a = m • a

theorem IsUnit.inv_smul {α : Type u_5} [Monoid α] {a : α} (h : IsUnit a) : h.unit⁻¹ • a = 1

theorem IsAddUnit.neg_vadd {α : Type u_5} [AddMonoid α] {a : α} (h : IsAddUnit a) : -h.addUnit +ᵥ a = 0

instance Units.instFaithfulSMul {M : Type u_3} {α : Type u_5} [Monoid M] [SMul M α] [FaithfulSMul M α] : FaithfulSMul Mˣ α

instance AddUnits.instFaithfulVAdd {M : Type u_3} {α : Type u_5} [AddMonoid M] [VAdd M α] [FaithfulVAdd M α] : FaithfulVAdd (AddUnits M) α

instance Units.instMulAction {M : Type u_3} {α : Type u_5} [Monoid M] [MulAction M α] : MulAction Mˣ α

Equations

• Units.instMulAction = { toSMul := Units.instSMul, mul_smul := ⋯, one_smul := ⋯ }

instance AddUnits.instAddAction {M : Type u_3} {α : Type u_5} [AddMonoid M] [AddAction M α] : AddAction (AddUnits M) α

Equations

• AddUnits.instAddAction = { toVAdd := AddUnits.instVAdd, add_vadd := ⋯, zero_vadd := ⋯ }

instance Units.smulCommClass_left {M : Type u_3} {N : Type u_4} {α : Type u_5} [Monoid M] [SMul M α] [SMul N α] [SMulCommClass M N α] : SMulCommClass Mˣ N α

instance AddUnits.vaddCommClass_left {M : Type u_3} {N : Type u_4} {α : Type u_5} [AddMonoid M] [VAdd M α] [VAdd N α] [VAddCommClass M N α] : VAddCommClass (AddUnits M) N α

instance Units.smulCommClass_right {M : Type u_3} {N : Type u_4} {α : Type u_5} [Monoid N] [SMul M α] [SMul N α] [SMulCommClass M N α] : SMulCommClass M Nˣ α

instance AddUnits.vaddCommClass_right {M : Type u_3} {N : Type u_4} {α : Type u_5} [AddMonoid N] [VAdd M α] [VAdd N α] [VAddCommClass M N α] : VAddCommClass M (AddUnits N) α

instance Units.instIsScalarTower {M : Type u_3} {N : Type u_4} {α : Type u_5} [Monoid M] [SMul M N] [SMul M α] [SMul N α] [IsScalarTower M N α] : IsScalarTower Mˣ N α

instance AddUnits.instVAddAssocClass {M : Type u_3} {N : Type u_4} {α : Type u_5} [AddMonoid M] [VAdd M N] [VAdd M α] [VAdd N α] [VAddAssocClass M N α] : VAddAssocClass (AddUnits M) N α

Action of a group G on units of M

instance Units.mulAction' {G : Type u_1} {M : Type u_3} [Group G] [Monoid M] [MulAction G M] [SMulCommClass G M M] [IsScalarTower G M M] : MulAction G 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

• Units.mulAction' = { smul := fun (g : G) (m : Mˣ) => { val := g • ↑m, inv := g⁻¹ • ↑m⁻¹, val_inv := ⋯, inv_val := ⋯ }, mul_smul := ⋯, one_smul := ⋯ }

instance AddUnits.addAction' {G : Type u_1} {M : Type u_3} [AddGroup G] [AddMonoid M] [AddAction G M] [VAddCommClass G M M] [VAddAssocClass G M M] : AddAction G (AddUnits M)

Equations

• AddUnits.addAction' = { vadd := fun (g : G) (m : AddUnits M) => { val := g +ᵥ ↑m, neg := -g +ᵥ ↑(-m), val_neg := ⋯, neg_val := ⋯ }, add_vadd := ⋯, zero_vadd := ⋯ }

@[simp]

theorem Units.smul_eq_mul {M : Type u_6} [CommMonoid M] (u₁ u₂ : Mˣ) : u₁ • u₂ = u₁ * u₂

This is not the usual smul_eq_mul because mulAction' creates a diamond.

Discussed on Zulip.

@[simp]

theorem Units.val_smul {G : Type u_1} {M : Type u_3} [Group G] [Monoid M] [MulAction G M] [SMulCommClass G M M] [IsScalarTower G M M] (g : G) (m : Mˣ) : ↑(g • m) = g • ↑m

@[simp]

theorem AddUnits.val_vadd {G : Type u_1} {M : Type u_3} [AddGroup G] [AddMonoid M] [AddAction G M] [VAddCommClass G M M] [VAddAssocClass G M M] (g : G) (m : AddUnits M) : ↑(g +ᵥ m) = g +ᵥ ↑m

@[simp]

theorem Units.smul_inv {G : Type u_1} {M : Type u_3} [Group G] [Monoid M] [MulAction G M] [SMulCommClass G M M] [IsScalarTower G M M] (g : G) (m : Mˣ) : (g • m)⁻¹ = g⁻¹ • m⁻¹

Note that this lemma exists more generally as the global smul_inv

@[simp]

theorem AddUnits.vadd_neg {G : Type u_1} {M : Type u_3} [AddGroup G] [AddMonoid M] [AddAction G M] [VAddCommClass G M M] [VAddAssocClass G M M] (g : G) (m : AddUnits M) : -(g +ᵥ m) = -g +ᵥ -m

instance Units.smulCommClass' {G : Type u_1} {H : Type u_2} {M : Type u_3} [Group G] [Group H] [Monoid M] [MulAction G M] [SMulCommClass G M M] [MulAction H M] [SMulCommClass H M M] [IsScalarTower G M M] [IsScalarTower H M M] [SMulCommClass G H M] : SMulCommClass G H Mˣ

Transfer SMulCommClass G H M to SMulCommClass G H Mˣ.

instance AddUnits.vaddCommClass' {G : Type u_1} {H : Type u_2} {M : Type u_3} [AddGroup G] [AddGroup H] [AddMonoid M] [AddAction G M] [VAddCommClass G M M] [AddAction H M] [VAddCommClass H M M] [VAddAssocClass G M M] [VAddAssocClass H M M] [VAddCommClass G H M] : VAddCommClass G H (AddUnits M)

Transfer VAddCommClass G H M to VAddCommClass G H (AddUnits M).

instance Units.isScalarTower' {G : Type u_1} {H : Type u_2} {M : Type u_3} [SMul G H] [Group G] [Group H] [Monoid M] [MulAction G M] [SMulCommClass G M M] [MulAction H M] [SMulCommClass H M M] [IsScalarTower G M M] [IsScalarTower H M M] [IsScalarTower G H M] : IsScalarTower G H Mˣ

Transfer IsScalarTower G H M to IsScalarTower G H Mˣ.

instance AddUnits.vaddAssocClass' {G : Type u_1} {H : Type u_2} {M : Type u_3} [VAdd G H] [AddGroup G] [AddGroup H] [AddMonoid M] [AddAction G M] [VAddCommClass G M M] [AddAction H M] [VAddCommClass H M M] [VAddAssocClass G M M] [VAddAssocClass H M M] [VAddAssocClass G H M] : VAddAssocClass G H (AddUnits M)

Transfer VAddAssocClass G H M to VAddAssocClass G H (AddUnits M).

instance Units.isScalarTower'_left {G : Type u_1} {M : Type u_3} {α : Type u_5} [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ˣ α

Transfer IsScalarTower G M α to IsScalarTower G Mˣ α.

instance AddUnits.vaddAssocClass'_left {G : Type u_1} {M : Type u_3} {α : Type u_5} [AddGroup G] [AddMonoid M] [AddAction G M] [VAdd M α] [VAdd G α] [VAddCommClass G M M] [VAddAssocClass G M M] [VAddAssocClass G M α] : VAddAssocClass G (AddUnits M) α

Transfer VAddAssocClass G M α to VAddAssocClass G (AddUnits M) α.

@[reducible, inline]

abbrev Units.mulDistribMulActionRight {M : Type u_6} {N : Type u_7} [Monoid M] [Monoid N] [MulDistribMulAction M N] : MulDistribMulAction M Nˣ

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⁻¹), _, _⟩.

Equations

• Units.mulDistribMulActionRight = { smul := fun (m : M) (u : Nˣ) => { val := m • ↑u, inv := m • ↑u⁻¹, val_inv := ⋯, inv_val := ⋯ }, mul_smul := ⋯, one_smul := ⋯, smul_mul := ⋯, smul_one := ⋯ }

@[simp]

theorem Units.coe_smul {M : Type u_6} {N : Type u_7} [Monoid M] [Monoid N] [MulDistribMulAction M N] (m : M) (u : Nˣ) : ↑(m • u) = m • ↑u

@[simp]

theorem Units.coe_inv_smul {M : Type u_6} {N : Type u_7} [Monoid M] [Monoid N] [MulDistribMulAction M N] (m : M) (u : Nˣ) : ↑(m • u)⁻¹ = m • ↑u⁻¹

theorem IsUnit.smul {G : Type u_1} {M : Type u_3} [Group G] [Monoid M] [MulAction G M] [SMulCommClass G M M] [IsScalarTower G M M] {m : M} (g : G) (h : IsUnit m) : IsUnit (g • m)

theorem IsAddUnit.vadd {G : Type u_1} {M : Type u_3} [AddGroup G] [AddMonoid M] [AddAction G M] [VAddCommClass G M M] [VAddAssocClass G M M] {m : M} (g : G) (h : IsAddUnit m) : IsAddUnit (g +ᵥ m)