mathlib3 documentation

group_theory.group_action.units

Group actions on and by Mˣ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides the action of a unit on a type α, has_smul Mˣ α, in the presence of has_smul M α, with the obvious definition stated in units.smul_def. This definition preserves mul_action and distrib_mul_action structures too.

Additionally, a mul_action G M for some group G satisfying some additional properties admits a mul_action G Mˣ structure, again with the obvious definition stated in units.coe_smul. These instances use a primed name.

The results are repeated for add_units and has_vadd where relevant.

Action of the units of M on a type α #

source
@[protected, instance]
def add_units.has_vadd {M : Type u_3} {α : Type u_5} [add_monoid M] [has_vadd M α] :
has_vadd (add_units M) α
Equations
source
@[protected, instance]
def units.has_smul {M : Type u_3} {α : Type u_5} [monoid M] [has_smul M α] :
has_smul Mˣ α
Equations
source
theorem add_units.vadd_def {M : Type u_3} {α : Type u_5} [add_monoid M] [has_vadd M α] (m : add_units M) (a : α) :
m +ᵥ a = ↑m +ᵥ a
source
theorem units.smul_def {M : Type u_3} {α : Type u_5} [monoid M] [has_smul M α] (m : Mˣ) (a : α) :
m • a = ↑m • a
source
@[simp]
theorem units.smul_is_unit {M : Type u_3} {α : Type u_5} [monoid M] [has_smul M α] {m : M} (hm : is_unit m) (a : α) :
hm.unit • a = m • a
source
theorem is_unit.inv_smul {α : Type u_5} [monoid α] {a : α} (h : is_unit a) :
(h.unit)⁻¹ • a = 1
source
@[protected, instance]
def units.has_faithful_smul {M : Type u_3} {α : Type u_5} [monoid M] [has_smul M α] [has_faithful_smul M α] :
has_faithful_smul Mˣ α
source
@[protected, instance]
def add_units.has_faithful_vadd {M : Type u_3} {α : Type u_5} [add_monoid M] [has_vadd M α] [has_faithful_vadd M α] :
has_faithful_vadd (add_units M) α
source
@[protected, instance]
def add_units.add_action {M : Type u_3} {α : Type u_5} [add_monoid M] [add_action M α] :
add_action (add_units M) α
Equations
source
@[protected, instance]
def units.mul_action {M : Type u_3} {α : Type u_5} [monoid M] [mul_action M α] :
mul_action Mˣ α
Equations
source
@[protected, instance]
def units.smul_zero_class {M : Type u_3} {α : Type u_5} [monoid M] [has_zero α] [smul_zero_class M α] :
smul_zero_class Mˣ α
Equations
source
@[protected, instance]
def units.distrib_smul {M : Type u_3} {α : Type u_5} [monoid M] [add_zero_class α] [distrib_smul M α] :
distrib_smul Mˣ α
Equations
source
@[protected, instance]
def units.distrib_mul_action {M : Type u_3} {α : Type u_5} [monoid M] [add_monoid α] [distrib_mul_action M α] :
distrib_mul_action Mˣ α
Equations
source
@[protected, instance]
def units.mul_distrib_mul_action {M : Type u_3} {α : Type u_5} [monoid M] [monoid α] [mul_distrib_mul_action M α] :
mul_distrib_mul_action Mˣ α
Equations
source
@[protected, instance]
def units.smul_comm_class_left {M : Type u_3} {N : Type u_4} {α : Type u_5} [monoid M] [has_smul M α] [has_smul N α] [smul_comm_class M N α] :
smul_comm_class Mˣ N α
source
@[protected, instance]
def units.smul_comm_class_right {M : Type u_3} {N : Type u_4} {α : Type u_5} [monoid N] [has_smul M α] [has_smul N α] [smul_comm_class M N α] :
smul_comm_class M Nˣ α
source
@[protected, instance]
def units.is_scalar_tower {M : Type u_3} {N : Type u_4} {α : Type u_5} [monoid M] [has_smul M N] [has_smul M α] [has_smul N α] [is_scalar_tower M N α] :
is_scalar_tower Mˣ N α

Action of a group G on units of M #

source
@[protected, instance]
def units.mul_action' {G : Type u_1} {M : Type u_3} [group G] [monoid M] [mul_action G M] [smul_comm_class G M M] [is_scalar_tower G M M] :
mul_action G Mˣ

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

Equations
source
@[simp]
theorem units.coe_smul {G : Type u_1} {M : Type u_3} [group G] [monoid M] [mul_action G M] [smul_comm_class G M M] [is_scalar_tower G M M] (g : G) (m : Mˣ) :
↑(g • m) = g • ↑m
source
@[simp]
theorem units.smul_inv {G : Type u_1} {M : Type u_3} [group G] [monoid M] [mul_action G M] [smul_comm_class G M M] [is_scalar_tower G M M] (g : G) (m : Mˣ) :
(g • m)⁻¹ = g⁻¹ • m⁻¹

Note that this lemma exists more generally as the global smul_inv

source
@[protected, instance]
def units.smul_comm_class' {G : Type u_1} {H : Type u_2} {M : Type u_3} [group G] [group H] [monoid M] [mul_action G M] [smul_comm_class G M M] [mul_action H M] [smul_comm_class H M M] [is_scalar_tower G M M] [is_scalar_tower H M M] [smul_comm_class G H M] :
smul_comm_class G H Mˣ

Transfer smul_comm_class G H M to smul_comm_class G H Mˣ

source
@[protected, instance]
def units.is_scalar_tower' {G : Type u_1} {H : Type u_2} {M : Type u_3} [has_smul G H] [group G] [group H] [monoid M] [mul_action G M] [smul_comm_class G M M] [mul_action H M] [smul_comm_class H M M] [is_scalar_tower G M M] [is_scalar_tower H M M] [is_scalar_tower G H M] :
is_scalar_tower G H Mˣ

Transfer is_scalar_tower G H M to is_scalar_tower G H Mˣ

source
@[protected, instance]
def units.is_scalar_tower'_left {G : Type u_1} {M : Type u_3} {α : Type u_5} [group G] [monoid M] [mul_action G M] [has_smul M α] [has_smul G α] [smul_comm_class G M M] [is_scalar_tower G M M] [is_scalar_tower G M α] :
is_scalar_tower G Mˣ α

Transfer is_scalar_tower G M α to is_scalar_tower G Mˣ α

source
@[protected, instance]
def units.mul_distrib_mul_action' {G : Type u_1} {M : Type u_3} [group G] [monoid M] [mul_distrib_mul_action G M] [smul_comm_class G M M] [is_scalar_tower G M M] :
mul_distrib_mul_action G Mˣ

A stronger form of units.mul_action'.

Equations
source
theorem is_unit.smul {G : Type u_1} {M : Type u_3} [group G] [monoid M] [mul_action G M] [smul_comm_class G M M] [is_scalar_tower G M M] {m : M} (g : G) (h : is_unit m) :
is_unit (g • m)