Documentation

Mathlib.GroupTheory.GroupAction.Units

Group actions on and by #

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.

Action of the units of M on a type α #

instance AddUnits.instVAddAddUnits {M : Type u_1} {α : Type u_2} [inst : AddMonoid M] [inst : VAdd M α] :
VAdd (AddUnits M) α
Equations
  • AddUnits.instVAddAddUnits = { vadd := fun m a => m +ᵥ a }
instance Units.instSMulUnits {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst : SMul M α] :
SMul Mˣ α
Equations
  • Units.instSMulUnits = { smul := fun m a => m a }
theorem AddUnits.vadd_def {M : Type u_1} {α : Type u_2} [inst : AddMonoid M] [inst : VAdd M α] (m : AddUnits M) (a : α) :
m +ᵥ a = m +ᵥ a
theorem Units.smul_def {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst : SMul M α] (m : Mˣ) (a : α) :
m a = m a
@[simp]
theorem Units.smul_isUnit {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst : SMul M α] {m : M} (hm : IsUnit m) (a : α) :
IsUnit.unit hm a = m a
theorem IsUnit.inv_smul {α : Type u_1} [inst : Monoid α] {a : α} (h : IsUnit a) :
def AddUnits.instFaithfulVAddAddUnitsInstVAddAddUnits.proof_1 {M : Type u_1} {α : Type u_2} [inst : AddMonoid M] [inst : VAdd M α] [inst : FaithfulVAdd M α] :
Equations
def AddUnits.instAddActionAddUnitsToAddMonoidToSubNegAddMonoidInstAddGroupAddUnits.proof_1 {M : Type u_1} {α : Type u_2} [inst : AddMonoid M] [inst : AddAction M α] (m : AddUnits M) (n : AddUnits M) (b : α) :
m + n +ᵥ b = m +ᵥ (n +ᵥ b)
Equations
Equations
  • AddUnits.instAddActionAddUnitsToAddMonoidToSubNegAddMonoidInstAddGroupAddUnits = AddAction.mk (_ : ∀ (b : α), 0 +ᵥ b = b) (_ : ∀ (m n : AddUnits M) (b : α), m + n +ᵥ b = m +ᵥ (n +ᵥ b))
instance Units.instMulActionUnitsToMonoidToDivInvMonoidInstGroupUnits {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst : MulAction M α] :
Equations
  • Units.instMulActionUnitsToMonoidToDivInvMonoidInstGroupUnits = MulAction.mk (_ : ∀ (b : α), 1 b = b) (_ : ∀ (m n : Mˣ) (b : α), (m * n) b = m n b)
instance Units.instSMulZeroClassUnits {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst : Zero α] [inst : SMulZeroClass M α] :
Equations
instance Units.instDistribSMulUnits {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst : AddZeroClass α] [inst : DistribSMul M α] :
Equations
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • Units.instMulDistribMulActionUnitsToMonoidToDivInvMonoidInstGroupUnits = MulDistribMulAction.mk (_ : ∀ (m : Mˣ) (b₁ b₂ : α), m (b₁ * b₂) = m b₁ * m b₂) (_ : ∀ (m : Mˣ), m 1 = 1)
instance Units.smulCommClass_left {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : Monoid M] [inst : SMul M α] [inst : SMul N α] [inst : SMulCommClass M N α] :
Equations
instance Units.smulCommClass_right {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : Monoid N] [inst : SMul M α] [inst : SMul N α] [inst : SMulCommClass M N α] :
Equations

Action of a group G on units of M #

instance Units.mulAction' {G : Type u_1} {M : Type u_2} [inst : Group G] [inst : Monoid M] [inst : MulAction G M] [inst : SMulCommClass G M M] [inst : IsScalarTower G M M] :

If an action G associates and commutes with multiplication on M, then it lifts to an action on . Notably, this provides mul_action Mˣ Nˣ under suitable conditions.

Equations
@[simp]
theorem Units.val_smul {G : Type u_1} {M : Type u_2} [inst : Group G] [inst : Monoid M] [inst : MulAction G M] [inst : SMulCommClass G M M] [inst : IsScalarTower G M M] (g : G) (m : Mˣ) :
↑(g m) = g m
@[simp]
theorem Units.smul_inv {G : Type u_1} {M : Type u_2} [inst : Group G] [inst : Monoid M] [inst : MulAction G M] [inst : SMulCommClass G M M] [inst : IsScalarTower G M M] (g : G) (m : Mˣ) :

Note that this lemma exists more generally as the global smul_inv

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

Transfer SMulCommClass G H M to SMulCommClass G H Mˣ

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

Transfer IsScalarTower G H M to IsScalarTower G H Mˣ

Equations
instance Units.isScalarTower'_left {G : Type u_1} {M : Type u_2} {α : Type u_3} [inst : Group G] [inst : Monoid M] [inst : MulAction G M] [inst : SMul M α] [inst : SMul G α] [inst : SMulCommClass G M M] [inst : IsScalarTower G M M] [inst : IsScalarTower G M α] :

Transfer IsScalarTower G M α to IsScalarTower G Mˣ α

Equations
instance Units.mulDistribMulAction' {G : Type u_1} {M : Type u_2} [inst : Group G] [inst : Monoid M] [inst : MulDistribMulAction G M] [inst : SMulCommClass G M M] [inst : IsScalarTower G M M] :

A stronger form of Units.mul_action'.

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