# mathlib3documentation

algebra.hom.units

# Monoid homomorphisms and units #

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

This file allows to lift monoid homomorphisms to group homomorphisms of their units subgroups. It also contains unrelated results about units that depend on monoid_hom.

## Main declarations #

• units.map: Turn an homomorphism from α to β monoids into an homomorphism from αˣ to βˣ.
• monoid_hom.to_hom_units: Turn an homomorphism from a group α to β into an homomorphism from α to βˣ.

## TODO #

The results that don't mention homomorphisms should be proved (earlier?) in a different file and be used to golf the basic group lemmas.

theorem group.is_unit {G : Type u_1} [group G] (g : G) :
theorem is_unit.eq_on_inv {F : Type u_1} {G : Type u_2} {N : Type u_3} [monoid N] [ N] {x : G} (hx : is_unit x) (f g : F) (h : f x = g x) :

If two homomorphisms from a division monoid to a monoid are equal at a unit x, then they are equal at x⁻¹.

theorem is_add_unit.eq_on_neg {F : Type u_1} {G : Type u_2} {N : Type u_3} [add_monoid N] [ N] {x : G} (hx : is_add_unit x) (f g : F) (h : f x = g x) :
f (-x) = g (-x)

If two homomorphisms from a subtraction monoid to an additive monoid are equal at an additive unit x, then they are equal at -x.

theorem eq_on_neg {F : Type u_1} {G : Type u_2} {M : Type u_3} [add_group G] [add_monoid M] [ M] (f g : F) {x : G} (h : f x = g x) :
f (-x) = g (-x)

If two homomorphism from an additive group to an additive monoid are equal at x, then they are equal at -x.

theorem eq_on_inv {F : Type u_1} {G : Type u_2} {M : Type u_3} [group G] [monoid M] [ M] (f g : F) {x : G} (h : f x = g x) :

If two homomorphism from a group to a monoid are equal at x, then they are equal at x⁻¹.

def units.map {M : Type u} {N : Type v} [monoid M] [monoid N] (f : M →* N) :

The group homomorphism on units induced by a monoid_hom.

Equations
def add_units.map {M : Type u} {N : Type v} [add_monoid M] [add_monoid N] (f : M →+ N) :

The add_group homomorphism on add_units induced by an add_monoid_hom.

Equations
@[simp]
theorem units.coe_map {M : Type u} {N : Type v} [monoid M] [monoid N] (f : M →* N) (x : Mˣ) :
@[simp]
theorem add_units.coe_map {M : Type u} {N : Type v} [add_monoid M] [add_monoid N] (f : M →+ N) (x : add_units M) :
( x) = f x
@[simp]
theorem add_units.coe_map_neg {M : Type u} {N : Type v} [add_monoid M] [add_monoid N] (f : M →+ N) (u : add_units M) :
@[simp]
theorem units.coe_map_inv {M : Type u} {N : Type v} [monoid M] [monoid N] (f : M →* N) (u : Mˣ) :
@[simp]
theorem add_units.map_comp {M : Type u} {N : Type v} {P : Type w} [add_monoid M] [add_monoid N] [add_monoid P] (f : M →+ N) (g : N →+ P) :
@[simp]
theorem units.map_comp {M : Type u} {N : Type v} {P : Type w} [monoid M] [monoid N] [monoid P] (f : M →* N) (g : N →* P) :
@[simp]
theorem units.map_id (M : Type u) [monoid M] :
@[simp]
def units.coe_hom (M : Type u) [monoid M] :
Mˣ →* M

Coercion Mˣ → M as a monoid homomorphism.

Equations
→+ M

Coercion add_units M → M as an add_monoid homomorphism.

Equations
@[simp]
theorem units.coe_hom_apply {M : Type u} [monoid M] (x : Mˣ) :
x = x
@[simp]
x = x
@[simp, norm_cast]
(n u) = n u
@[simp, norm_cast]
theorem units.coe_pow {M : Type u} [monoid M] (u : Mˣ) (n : ) :
(u ^ n) = u ^ n
@[simp, norm_cast]
theorem add_units.coe_sub {α : Type u_1} (u₁ u₂ : add_units α) :
(u₁ - u₂) = u₁ - u₂
@[simp, norm_cast]
theorem units.coe_div {α : Type u_1} (u₁ u₂ : αˣ) :
(u₁ / u₂) = u₁ / u₂
@[simp, norm_cast]
theorem units.coe_zpow {α : Type u_1} (u : αˣ) (n : ) :
(u ^ n) = u ^ n
@[simp, norm_cast]
theorem add_units.coe_zsmul {α : Type u_1} (u : add_units α) (n : ) :
(n u) = n u
theorem divp_eq_div {α : Type u_1} (a : α) (u : αˣ) :
a /ₚ u = a / u
@[simp]
theorem map_add_units_neg {α : Type u_1} {M : Type u} [add_monoid M] {F : Type u_2} [ α] (f : F) (u : add_units M) :
f (-u) = -f u
@[simp]
theorem map_units_inv {α : Type u_1} {M : Type u} [monoid M] {F : Type u_2} [ α] (f : F) (u : Mˣ) :
def units.lift_right {M : Type u} {N : Type v} [monoid M] [monoid N] (f : M →* N) (g : M Nˣ) (h : (x : M), (g x) = f x) :
M →* Nˣ

If a map g : M → Nˣ agrees with a homomorphism f : M →* N, then this map is a monoid homomorphism too.

Equations
def add_units.lift_right {M : Type u} {N : Type v} [add_monoid M] [add_monoid N] (f : M →+ N) (g : M ) (h : (x : M), (g x) = f x) :
M →+

If a map g : M → add_units N agrees with a homomorphism f : M →+ N, then this map is an add_monoid homomorphism too.

Equations
@[simp]
theorem add_units.coe_lift_right {M : Type u} {N : Type v} [add_monoid M] [add_monoid N] {f : M →+ N} {g : M } (h : (x : M), (g x) = f x) (x : M) :
( h) x) = f x
@[simp]
theorem units.coe_lift_right {M : Type u} {N : Type v} [monoid M] [monoid N] {f : M →* N} {g : M Nˣ} (h : (x : M), (g x) = f x) (x : M) :
( g h) x) = f x
@[simp]
theorem add_units.add_lift_right_neg {M : Type u} {N : Type v} [add_monoid M] [add_monoid N] {f : M →+ N} {g : M } (h : (x : M), (g x) = f x) (x : M) :
f x + - h) x = 0
@[simp]
theorem units.mul_lift_right_inv {M : Type u} {N : Type v} [monoid M] [monoid N] {f : M →* N} {g : M Nˣ} (h : (x : M), (g x) = f x) (x : M) :
f x * ( g h) x)⁻¹ = 1
@[simp]
theorem add_units.lift_right_neg_add {M : Type u} {N : Type v} [add_monoid M] [add_monoid N] {f : M →+ N} {g : M } (h : (x : M), (g x) = f x) (x : M) :
- h) x + f x = 0
@[simp]
theorem units.lift_right_inv_mul {M : Type u} {N : Type v} [monoid M] [monoid N] {f : M →* N} {g : M Nˣ} (h : (x : M), (g x) = f x) (x : M) :
( g h) x)⁻¹ * f x = 1
G →+

If f is a homomorphism from an additive group G to an additive monoid M, then its image lies in the add_units of M, and f.to_hom_units is the corresponding homomorphism from G to add_units M.

Equations
def monoid_hom.to_hom_units {G : Type u_1} {M : Type u_2} [group G] [monoid M] (f : G →* M) :
G →* Mˣ

If f is a homomorphism from a group G to a monoid M, then its image lies in the units of M, and f.to_hom_units is the corresponding monoid homomorphism from G to Mˣ.

Equations
@[simp]
theorem add_monoid_hom.coe_to_hom_add_units {G : Type u_1} {M : Type u_2} [add_group G] [add_monoid M] (f : G →+ M) (g : G) :
@[simp]
theorem monoid_hom.coe_to_hom_units {G : Type u_1} {M : Type u_2} [group G] [monoid M] (f : G →* M) (g : G) :
theorem is_unit.map {F : Type u_1} {M : Type u_4} {N : Type u_5} [monoid M] [monoid N] [ N] (f : F) {x : M} (h : is_unit x) :
theorem is_add_unit.map {F : Type u_1} {M : Type u_4} {N : Type u_5} [add_monoid M] [add_monoid N] [ N] (f : F) {x : M} (h : is_add_unit x) :
theorem is_add_unit.of_left_inverse {F : Type u_1} {G : Type u_2} {M : Type u_4} {N : Type u_5} [add_monoid M] [add_monoid N] [ N] [ M] {f : F} {x : M} (g : G) (hfg : f) (h : is_add_unit (f x)) :
theorem is_unit.of_left_inverse {F : Type u_1} {G : Type u_2} {M : Type u_4} {N : Type u_5} [monoid M] [monoid N] [ N] [ M] {f : F} {x : M} (g : G) (hfg : f) (h : is_unit (f x)) :
theorem is_unit_map_of_left_inverse {F : Type u_1} {G : Type u_2} {M : Type u_4} {N : Type u_5} [monoid M] [monoid N] [ N] [ M] {f : F} {x : M} (g : G) (hfg : f) :
theorem is_add_unit_map_of_left_inverse {F : Type u_1} {G : Type u_2} {M : Type u_4} {N : Type u_5} [add_monoid M] [add_monoid N] [ N] [ M] {f : F} {x : M} (g : G) (hfg : f) :
noncomputable def is_unit.lift_right {M : Type u_4} {N : Type u_5} [monoid M] [monoid N] (f : M →* N) (hf : (x : M), is_unit (f x)) :
M →* Nˣ

If a homomorphism f : M →* N sends each element to an is_unit, then it can be lifted to f : M →* Nˣ. See also units.lift_right for a computable version.

Equations
• = (λ (x : M), _.unit) _
noncomputable def is_add_unit.lift_right {M : Type u_4} {N : Type u_5} [add_monoid M] [add_monoid N] (f : M →+ N) (hf : (x : M), is_add_unit (f x)) :
M →+

If a homomorphism f : M →+ N sends each element to an is_add_unit, then it can be lifted to f : M →+ add_units N. See also add_units.lift_right for a computable version.

Equations
theorem is_unit.coe_lift_right {M : Type u_4} {N : Type u_5} [monoid M] [monoid N] (f : M →* N) (hf : (x : M), is_unit (f x)) (x : M) :
( hf) x) = f x
theorem is_add_unit.coe_lift_right {M : Type u_4} {N : Type u_5} [add_monoid M] [add_monoid N] (f : M →+ N) (hf : (x : M), is_add_unit (f x)) (x : M) :
( hf) x) = f x
@[simp]
theorem is_unit.mul_lift_right_inv {M : Type u_4} {N : Type u_5} [monoid M] [monoid N] (f : M →* N) (h : (x : M), is_unit (f x)) (x : M) :
f x * ( h) x)⁻¹ = 1
@[simp]
theorem is_add_unit.add_lift_right_neg {M : Type u_4} {N : Type u_5} [add_monoid M] [add_monoid N] (f : M →+ N) (h : (x : M), is_add_unit (f x)) (x : M) :
f x + - x = 0
@[simp]
theorem is_unit.lift_right_inv_mul {M : Type u_4} {N : Type u_5} [monoid M] [monoid N] (f : M →* N) (h : (x : M), is_unit (f x)) (x : M) :
( h) x)⁻¹ * f x = 1
@[simp]
theorem is_add_unit.lift_right_neg_add {M : Type u_4} {N : Type u_5} [add_monoid M] [add_monoid N] (f : M →+ N) (h : (x : M), is_add_unit (f x)) (x : M) :
- x + f x = 0
@[simp]
theorem is_unit.coe_inv_unit' {α : Type u_3} {a : α} (h : is_unit a) :
@[simp]
theorem is_unit.coe_unit' {α : Type u_3} {a : α} (h : is_unit a) :
(h.unit') = a
@[simp]

The element of the additive group of additive units, corresponding to an element of an additive monoid which is an additive unit. As opposed to is_add_unit.add_unit, the negation is computable and comes from the negation on α. This is useful to transfer properties of negation in add_units α to α. See also to_add_units.

Equations
def is_unit.unit' {α : Type u_3} {a : α} (h : is_unit a) :
αˣ

The element of the group of units, corresponding to an element of a monoid which is a unit. As opposed to is_unit.unit, the inverse is computable and comes from the inversion on α. This is useful to transfer properties of inversion in units α to α. See also to_units.

Equations
@[simp]
@[protected, simp]
theorem is_add_unit.add_neg_cancel_left {α : Type u_3} {a : α} (h : is_add_unit a) (b : α) :
a + (-a + b) = b
@[protected, simp]
theorem is_unit.mul_inv_cancel_left {α : Type u_3} {a : α} (h : is_unit a) (b : α) :
a * (a⁻¹ * b) = b
@[protected, simp]
theorem is_add_unit.neg_add_cancel_left {α : Type u_3} {a : α} (h : is_add_unit a) (b : α) :
-a + (a + b) = b
@[protected, simp]
theorem is_unit.inv_mul_cancel_left {α : Type u_3} {a : α} (h : is_unit a) (b : α) :
a⁻¹ * (a * b) = b
@[protected, simp]
theorem is_unit.mul_inv_cancel_right {α : Type u_3} {b : α} (h : is_unit b) (a : α) :
a * b * b⁻¹ = a
@[protected, simp]
theorem is_add_unit.add_neg_cancel_right {α : Type u_3} {b : α} (h : is_add_unit b) (a : α) :
a + b + -b = a
@[protected, simp]
theorem is_unit.inv_mul_cancel_right {α : Type u_3} {b : α} (h : is_unit b) (a : α) :
a * b⁻¹ * b = a
@[protected, simp]
theorem is_add_unit.neg_add_cancel_right {α : Type u_3} {b : α} (h : is_add_unit b) (a : α) :
a + -b + b = a
@[protected]
theorem is_add_unit.sub_self {α : Type u_3} {a : α} (h : is_add_unit a) :
a - a = 0
@[protected]
theorem is_unit.div_self {α : Type u_3} {a : α} (h : is_unit a) :
a / a = 1
@[protected]
theorem is_unit.eq_mul_inv_iff_mul_eq {α : Type u_3} {a b c : α} (h : is_unit c) :
a = b * c⁻¹ a * c = b
@[protected]
a = b + -c a + c = b
@[protected]
theorem is_unit.eq_inv_mul_iff_mul_eq {α : Type u_3} {a b c : α} (h : is_unit b) :
a = b⁻¹ * c b * a = c
@[protected]
a = -b + c b + a = c
@[protected]
-a + b = c b = a + c
@[protected]
theorem is_unit.inv_mul_eq_iff_eq_mul {α : Type u_3} {a b c : α} (h : is_unit a) :
a⁻¹ * b = c b = a * c
@[protected]
theorem is_unit.mul_inv_eq_iff_eq_mul {α : Type u_3} {a b c : α} (h : is_unit b) :
a * b⁻¹ = c a = c * b
@[protected]
a + -b = c a = c + b
@[protected]
theorem is_unit.mul_inv_eq_one {α : Type u_3} {a b : α} (h : is_unit b) :
a * b⁻¹ = 1 a = b
@[protected]
a + -b = 0 a = b
@[protected]
-a + b = 0 a = b
@[protected]
theorem is_unit.inv_mul_eq_one {α : Type u_3} {a b : α} (h : is_unit a) :
a⁻¹ * b = 1 a = b
@[protected]
a + b = 0 a = -b
@[protected]
theorem is_unit.mul_eq_one_iff_eq_inv {α : Type u_3} {a b : α} (h : is_unit b) :
a * b = 1 a = b⁻¹
@[protected]
theorem is_unit.mul_eq_one_iff_inv_eq {α : Type u_3} {a b : α} (h : is_unit a) :
a * b = 1 a⁻¹ = b
@[protected]
a + b = 0 -a = b
@[protected, simp]
theorem is_unit.div_mul_cancel {α : Type u_3} {b : α} (h : is_unit b) (a : α) :
a / b * b = a
@[protected, simp]
theorem is_add_unit.sub_add_cancel {α : Type u_3} {b : α} (h : is_add_unit b) (a : α) :
a - b + b = a
@[protected, simp]
theorem is_unit.mul_div_cancel {α : Type u_3} {b : α} (h : is_unit b) (a : α) :
a * b / b = a
@[protected, simp]
theorem is_add_unit.add_sub_cancel {α : Type u_3} {b : α} (h : is_add_unit b) (a : α) :
a + b - b = a
@[protected]
theorem is_unit.mul_one_div_cancel {α : Type u_3} {a : α} (h : is_unit a) :
a * (1 / a) = 1
@[protected]
a + (0 - a) = 0
@[protected]
theorem is_unit.one_div_mul_cancel {α : Type u_3} {a : α} (h : is_unit a) :
1 / a * a = 1
@[protected]
0 - a + a = 0
theorem is_unit.inv {α : Type u_3} {a : α} :
theorem is_add_unit.neg {α : Type u_3} {a : α} :
theorem is_add_unit.sub {α : Type u_3} {a b : α} (ha : is_add_unit a) (hb : is_add_unit b) :
theorem is_unit.div {α : Type u_3} {a b : α} (ha : is_unit a) (hb : is_unit b) :
is_unit (a / b)
@[protected]
theorem is_unit.div_left_inj {α : Type u_3} {a b c : α} (h : is_unit c) :
a / c = b / c a = b
@[protected]
theorem is_add_unit.sub_left_inj {α : Type u_3} {a b c : α} (h : is_add_unit c) :
a - c = b - c a = b
@[protected]
theorem is_add_unit.sub_eq_iff {α : Type u_3} {a b c : α} (h : is_add_unit b) :
a - b = c a = c + b
@[protected]
theorem is_unit.div_eq_iff {α : Type u_3} {a b c : α} (h : is_unit b) :
a / b = c a = c * b
@[protected]
theorem is_add_unit.eq_sub_iff {α : Type u_3} {a b c : α} (h : is_add_unit c) :
a = b - c a + c = b
@[protected]
theorem is_unit.eq_div_iff {α : Type u_3} {a b c : α} (h : is_unit c) :
a = b / c a * c = b
@[protected]
theorem is_unit.div_eq_of_eq_mul {α : Type u_3} {a b c : α} (h : is_unit b) :
a = c * b a / b = c
@[protected]
a = c + b a - b = c
@[protected]
theorem is_unit.eq_div_of_mul_eq {α : Type u_3} {a b c : α} (h : is_unit c) :
a * c = b a = b / c
@[protected]
a + c = b a = b - c
@[protected]
theorem is_unit.div_eq_one_iff_eq {α : Type u_3} {a b : α} (h : is_unit b) :
a / b = 1 a = b
@[protected]
theorem is_add_unit.sub_eq_zero_iff_eq {α : Type u_3} {a b : α} (h : is_add_unit b) :
a - b = 0 a = b
@[protected]
theorem is_unit.div_mul_left {α : Type u_3} {a b : α} (h : is_unit b) :
b / (a * b) = 1 / a

The group version of this lemma is div_mul_cancel'''

@[protected]
b - (a + b) = 0 - a

The add_group version of this lemma is sub_add_cancel''

@[protected]
theorem is_unit.mul_div_mul_right {α : Type u_3} {c : α} (h : is_unit c) (a b : α) :
a * c / (b * c) = a / b
@[protected]
a + c - (b + c) = a - b
@[protected]
a + b + (0 - b) = a
@[protected]
theorem is_unit.mul_mul_div {α : Type u_3} {b : α} (a : α) (h : is_unit b) :
a * b * (1 / b) = a
@[protected]
theorem is_unit.div_mul_right {α : Type u_3} {a : α} (h : is_unit a) (b : α) :
a / (a * b) = 1 / b
@[protected]
theorem is_add_unit.sub_add_right {α : Type u_3} {a : α} (h : is_add_unit a) (b : α) :
a - (a + b) = 0 - b
@[protected]
theorem is_unit.mul_div_cancel_left {α : Type u_3} {a : α} (h : is_unit a) (b : α) :
a * b / a = b
@[protected]
theorem is_add_unit.add_sub_cancel_left {α : Type u_3} {a : α} (h : is_add_unit a) (b : α) :
a + b - a = b
@[protected]
theorem is_add_unit.add_sub_cancel' {α : Type u_3} {a : α} (h : is_add_unit a) (b : α) :
a + (b - a) = b
@[protected]
theorem is_unit.mul_div_cancel' {α : Type u_3} {a : α} (h : is_unit a) (b : α) :
a * (b / a) = b
@[protected]
theorem is_unit.mul_div_mul_left {α : Type u_3} {c : α} (h : is_unit c) (a b : α) :
c * a / (c * b) = a / b
@[protected]
c + a - (c + b) = a - b
@[protected]
theorem is_add_unit.add_eq_add_of_sub_eq_sub {α : Type u_3} {b d : α} (hb : is_add_unit b) (hd : is_add_unit d) (a c : α) (h : a - b = c - d) :
a + d = c + b
@[protected]
theorem is_unit.mul_eq_mul_of_div_eq_div {α : Type u_3} {b d : α} (hb : is_unit b) (hd : is_unit d) (a c : α) (h : a / b = c / d) :
a * d = c * b
@[protected]
theorem is_unit.div_eq_div_iff {α : Type u_3} {a b c d : α} (hb : is_unit b) (hd : is_unit d) :
a / b = c / d a * d = c * b
@[protected]
theorem is_add_unit.sub_eq_sub_iff {α : Type u_3} {a b c d : α} (hb : is_add_unit b) (hd : is_add_unit d) :
a - b = c - d a + d = c + b
@[protected]
theorem is_unit.div_div_cancel {α : Type u_3} {a b : α} (h : is_unit a) :
a / (a / b) = b
@[protected]
theorem is_add_unit.sub_sub_cancel {α : Type u_3} {a b : α} (h : is_add_unit a) :
a - (a - b) = b
@[protected]
theorem is_add_unit.sub_sub_cancel_left {α : Type u_3} {a b : α} (h : is_add_unit a) :
a - b - a = -b
@[protected]
theorem is_unit.div_div_cancel_left {α : Type u_3} {a b : α} (h : is_unit a) :
a / b / a = b⁻¹