algebra.hom.equiv.units.basic

source

def to_units {G : Type u_10} [group G] :

G ≃* Gˣ

A group is isomorphic to its group of units.

Equations

to_units = {to_fun := λ (x : G), {val := x, inv := x⁻¹, val_inv := _, inv_val := _}, inv_fun := coe coe_to_lift, left_inv := _, right_inv := _, map_mul' := _}

source

def to_add_units {G : Type u_10} [add_group G] :

G ≃+ add_units G

An additive group is isomorphic to its group of additive units

Equations

to_add_units = {to_fun := λ (x : G), {val := x, neg := -x, val_neg := _, neg_val := _}, inv_fun := coe coe_to_lift, left_inv := _, right_inv := _, map_add' := _}

source

@[simp]

theorem coe_to_units {G : Type u_10} [group G] (g : G) :

↑(⇑to_units g) = g

source

@[simp]

theorem coe_to_add_units {G : Type u_10} [add_group G] (g : G) :

↑(⇑to_add_units g) = g

source

def units.map_equiv {M : Type u_6} {N : Type u_7} [monoid M] [monoid N] (h : M ≃* N) :

Mˣ ≃* Nˣ

A multiplicative equivalence of monoids defines a multiplicative equivalence of their groups of units.

Equations

units.map_equiv h = {to_fun := (units.map h.to_monoid_hom).to_fun, inv_fun := ⇑(units.map h.symm.to_monoid_hom), left_inv := _, right_inv := _, map_mul' := _}

source

@[simp]

theorem units.map_equiv_symm {M : Type u_6} {N : Type u_7} [monoid M] [monoid N] (h : M ≃* N) :

(units.map_equiv h).symm = units.map_equiv h.symm

source

@[simp]

theorem units.coe_map_equiv {M : Type u_6} {N : Type u_7} [monoid M] [monoid N] (h : M ≃* N) (x : Mˣ) :

↑(⇑(units.map_equiv h) x) = ⇑h ↑x

source

def units.mul_left {M : Type u_6} [monoid M] (u : Mˣ) :

equiv.perm M

Left multiplication by a unit of a monoid is a permutation of the underlying type.

Equations

u.mul_left = {to_fun := λ (x : M), ↑u * x, inv_fun := λ (x : M), ↑u⁻¹ * x, left_inv := _, right_inv := _}

source

@[simp]

theorem add_units.add_left_apply {M : Type u_6} [add_monoid M] (u : add_units M) :

⇑(u.add_left) = λ (x : M), ↑u + x

source

@[simp]

theorem units.mul_left_apply {M : Type u_6} [monoid M] (u : Mˣ) :

⇑(u.mul_left) = λ (x : M), ↑u * x

source

def add_units.add_left {M : Type u_6} [add_monoid M] (u : add_units M) :

equiv.perm M

Left addition of an additive unit is a permutation of the underlying type.

Equations

u.add_left = {to_fun := λ (x : M), ↑u + x, inv_fun := λ (x : M), ↑-u + x, left_inv := _, right_inv := _}

source

@[simp]

theorem units.mul_left_symm {M : Type u_6} [monoid M] (u : Mˣ) :

equiv.symm u.mul_left = u⁻¹.mul_left

source

@[simp]

theorem add_units.add_left_symm {M : Type u_6} [add_monoid M] (u : add_units M) :

equiv.symm u.add_left = (-u).add_left

source

theorem units.mul_left_bijective {M : Type u_6} [monoid M] (a : Mˣ) :

function.bijective (has_mul.mul ↑a)

source

theorem add_units.add_left_bijective {M : Type u_6} [add_monoid M] (a : add_units M) :

function.bijective (has_add.add ↑a)

source

@[simp]

theorem units.mul_right_apply {M : Type u_6} [monoid M] (u : Mˣ) :

⇑(u.mul_right) = λ (x : M), x * ↑u

source

@[simp]

theorem add_units.add_right_apply {M : Type u_6} [add_monoid M] (u : add_units M) :

⇑(u.add_right) = λ (x : M), x + ↑u

source

def units.mul_right {M : Type u_6} [monoid M] (u : Mˣ) :

equiv.perm M

Right multiplication by a unit of a monoid is a permutation of the underlying type.

Equations

u.mul_right = {to_fun := λ (x : M), x * ↑u, inv_fun := λ (x : M), x * ↑u⁻¹, left_inv := _, right_inv := _}

source

def add_units.add_right {M : Type u_6} [add_monoid M] (u : add_units M) :

equiv.perm M

Right addition of an additive unit is a permutation of the underlying type.

Equations

u.add_right = {to_fun := λ (x : M), x + ↑u, inv_fun := λ (x : M), x + ↑-u, left_inv := _, right_inv := _}

source

@[simp]

theorem units.mul_right_symm {M : Type u_6} [monoid M] (u : Mˣ) :

equiv.symm u.mul_right = u⁻¹.mul_right

source

@[simp]

theorem add_units.add_right_symm {M : Type u_6} [add_monoid M] (u : add_units M) :

equiv.symm u.add_right = (-u).add_right

source

theorem units.mul_right_bijective {M : Type u_6} [monoid M] (a : Mˣ) :

function.bijective (λ (_x : M), _x * ↑a)

source

theorem add_units.add_right_bijective {M : Type u_6} [add_monoid M] (a : add_units M) :

function.bijective (λ (_x : M), _x + ↑a)

source

@[protected]

def equiv.add_left {G : Type u_10} [add_group G] (a : G) :

equiv.perm G

Left addition in an add_group is a permutation of the underlying type.

Equations

equiv.add_left a = (⇑to_add_units a).add_left

source

@[protected]

def equiv.mul_left {G : Type u_10} [group G] (a : G) :

equiv.perm G

Left multiplication in a group is a permutation of the underlying type.

Equations

equiv.mul_left a = (⇑to_units a).mul_left

source

@[simp]

theorem equiv.coe_mul_left {G : Type u_10} [group G] (a : G) :

⇑(equiv.mul_left a) = has_mul.mul a

source

@[simp]

theorem equiv.coe_add_left {G : Type u_10} [add_group G] (a : G) :

⇑(equiv.add_left a) = has_add.add a

source

@[simp, nolint]

theorem equiv.add_left_symm_apply {G : Type u_10} [add_group G] (a : G) :

⇑(equiv.symm (equiv.add_left a)) = has_add.add (-a)

Extra simp lemma that dsimp can use. simp will never use this.

source

@[simp, nolint]

theorem equiv.mul_left_symm_apply {G : Type u_10} [group G] (a : G) :

⇑(equiv.symm (equiv.mul_left a)) = has_mul.mul a⁻¹

Extra simp lemma that dsimp can use. simp will never use this.

source

@[simp]

theorem equiv.mul_left_symm {G : Type u_10} [group G] (a : G) :

equiv.symm (equiv.mul_left a) = equiv.mul_left a⁻¹

source

@[simp]

theorem equiv.add_left_symm {G : Type u_10} [add_group G] (a : G) :

equiv.symm (equiv.add_left a) = equiv.add_left (-a)

source

theorem group.mul_left_bijective {G : Type u_10} [group G] (a : G) :

function.bijective (has_mul.mul a)

source

theorem add_group.add_left_bijective {G : Type u_10} [add_group G] (a : G) :

function.bijective (has_add.add a)

source

@[protected]

def equiv.mul_right {G : Type u_10} [group G] (a : G) :

equiv.perm G

Right multiplication in a group is a permutation of the underlying type.

Equations

equiv.mul_right a = (⇑to_units a).mul_right

source

@[protected]

def equiv.add_right {G : Type u_10} [add_group G] (a : G) :

equiv.perm G

Right addition in an add_group is a permutation of the underlying type.

Equations

equiv.add_right a = (⇑to_add_units a).add_right

source

@[simp]

theorem equiv.coe_add_right {G : Type u_10} [add_group G] (a : G) :

⇑(equiv.add_right a) = λ (x : G), x + a

source

@[simp]

theorem equiv.coe_mul_right {G : Type u_10} [group G] (a : G) :

⇑(equiv.mul_right a) = λ (x : G), x * a

source

@[simp]

theorem equiv.add_right_symm {G : Type u_10} [add_group G] (a : G) :

equiv.symm (equiv.add_right a) = equiv.add_right (-a)

source

@[simp]

theorem equiv.mul_right_symm {G : Type u_10} [group G] (a : G) :

equiv.symm (equiv.mul_right a) = equiv.mul_right a⁻¹

source

@[simp, nolint]

theorem equiv.add_right_symm_apply {G : Type u_10} [add_group G] (a : G) :

⇑(equiv.symm (equiv.add_right a)) = λ (x : G), x + -a

Extra simp lemma that dsimp can use. simp will never use this.

source

@[simp, nolint]

theorem equiv.mul_right_symm_apply {G : Type u_10} [group G] (a : G) :

⇑(equiv.symm (equiv.mul_right a)) = λ (x : G), x * a⁻¹

Extra simp lemma that dsimp can use. simp will never use this.

source

theorem add_group.add_right_bijective {G : Type u_10} [add_group G] (a : G) :

function.bijective (λ (_x : G), _x + a)

source

theorem group.mul_right_bijective {G : Type u_10} [group G] (a : G) :

function.bijective (λ (_x : G), _x * a)

source

@[protected]

def equiv.sub_left {G : Type u_10} [add_group G] (a : G) :

G ≃ G

A version of equiv.add_left a (-b) that is defeq to a - b.

Equations

equiv.sub_left a = {to_fun := λ (b : G), a - b, inv_fun := λ (b : G), -b + a, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.div_left_symm_apply {G : Type u_10} [group G] (a b : G) :

⇑((equiv.div_left a).symm) b = b⁻¹ * a

source

@[simp]

theorem equiv.div_left_apply {G : Type u_10} [group G] (a b : G) :

⇑(equiv.div_left a) b = a / b

source

@[simp]

theorem equiv.sub_left_symm_apply {G : Type u_10} [add_group G] (a b : G) :

⇑((equiv.sub_left a).symm) b = -b + a

source

@[protected]

def equiv.div_left {G : Type u_10} [group G] (a : G) :

G ≃ G

A version of equiv.mul_left a b⁻¹ that is defeq to a / b.

Equations

equiv.div_left a = {to_fun := λ (b : G), a / b, inv_fun := λ (b : G), b⁻¹ * a, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.sub_left_apply {G : Type u_10} [add_group G] (a b : G) :

⇑(equiv.sub_left a) b = a - b

source

theorem equiv.div_left_eq_inv_trans_mul_left {G : Type u_10} [group G] (a : G) :

equiv.div_left a = equiv.trans (equiv.inv G) (equiv.mul_left a)

source

theorem equiv.sub_left_eq_neg_trans_add_left {G : Type u_10} [add_group G] (a : G) :

equiv.sub_left a = equiv.trans (equiv.neg G) (equiv.add_left a)

source

@[simp]

theorem equiv.div_right_apply {G : Type u_10} [group G] (a b : G) :

⇑(equiv.div_right a) b = b / a

source

@[simp]

theorem equiv.sub_right_symm_apply {G : Type u_10} [add_group G] (a b : G) :

⇑((equiv.sub_right a).symm) b = b + a

source

@[simp]

theorem equiv.sub_right_apply {G : Type u_10} [add_group G] (a b : G) :

⇑(equiv.sub_right a) b = b - a

source

@[protected]

def equiv.sub_right {G : Type u_10} [add_group G] (a : G) :

G ≃ G

A version of equiv.add_right (-a) b that is defeq to b - a.

Equations

equiv.sub_right a = {to_fun := λ (b : G), b - a, inv_fun := λ (b : G), b + a, left_inv := _, right_inv := _}

source

@[protected]

def equiv.div_right {G : Type u_10} [group G] (a : G) :

G ≃ G

A version of equiv.mul_right a⁻¹ b that is defeq to b / a.

Equations

equiv.div_right a = {to_fun := λ (b : G), b / a, inv_fun := λ (b : G), b * a, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.div_right_symm_apply {G : Type u_10} [group G] (a b : G) :

⇑((equiv.div_right a).symm) b = b * a

source

theorem equiv.sub_right_eq_add_right_neg {G : Type u_10} [add_group G] (a : G) :

equiv.sub_right a = equiv.add_right (-a)

source

theorem equiv.div_right_eq_mul_right_inv {G : Type u_10} [group G] (a : G) :

equiv.div_right a = equiv.mul_right a⁻¹

source

def add_equiv.neg (G : Type u_1) [subtraction_comm_monoid G] :

G ≃+ G

When the add_group is commutative, equiv.neg is an add_equiv.

Equations

add_equiv.neg G = {to_fun := has_neg.neg (sub_neg_monoid.to_has_neg G), inv_fun := has_neg.neg (sub_neg_monoid.to_has_neg G), left_inv := _, right_inv := _, map_add' := _}

source

@[simp]

theorem add_equiv.neg_apply (G : Type u_1) [subtraction_comm_monoid G] (ᾰ : G) :

⇑(add_equiv.neg G) ᾰ = -ᾰ

source

def mul_equiv.inv (G : Type u_1) [division_comm_monoid G] :

G ≃* G

In a division_comm_monoid, equiv.inv is a mul_equiv. There is a variant of this mul_equiv.inv' G : G ≃* Gᵐᵒᵖ for the non-commutative case.

Equations

mul_equiv.inv G = {to_fun := has_inv.inv (div_inv_monoid.to_has_inv G), inv_fun := has_inv.inv (div_inv_monoid.to_has_inv G), left_inv := _, right_inv := _, map_mul' := _}

source

@[simp]

theorem mul_equiv.inv_apply (G : Type u_1) [division_comm_monoid G] (ᾰ : G) :

⇑(mul_equiv.inv G) ᾰ = ᾰ⁻¹

source

@[simp]

theorem mul_equiv.inv_symm (G : Type u_1) [division_comm_monoid G] :

(mul_equiv.inv G).symm = mul_equiv.inv G

mathlib3 documentation

Multiplicative and additive equivalence acting on units. #