mathlib documentation

algebra.hom.units

Monoid homomorphisms and units #

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 #

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.

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) :
@[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] :
def units.coe_hom (M : Type u) [monoid M] :
Mˣ →* M

Coercion Mˣ → M as a monoid homomorphism.

Equations
def add_units.coe_hom (M : Type u) [add_monoid 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ˣ) :
@[simp]
theorem add_units.coe_hom_apply {M : Type u} [add_monoid M] (x : add_units M) :
@[simp, norm_cast]
theorem add_units.coe_nsmul {M : Type u} [add_monoid M] (u : add_units M) (n : ) :
(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} [subtraction_monoid α] (u₁ u₂ : add_units α) :
(u₁ - u₂) = u₁ - u₂
@[simp, norm_cast]
theorem units.coe_div {α : Type u_1} [division_monoid α] (u₁ u₂ : αˣ) :
(u₁ / u₂) = u₁ / u₂
@[simp, norm_cast]
theorem units.coe_zpow {α : Type u_1} [division_monoid α] (u : αˣ) (n : ) :
(u ^ n) = u ^ n
@[simp, norm_cast]
theorem add_units.coe_zsmul {α : Type u_1} [subtraction_monoid α] (u : add_units α) (n : ) :
(n u) = n u
theorem divp_eq_div {α : Type u_1} [division_monoid α] (a : α) (u : αˣ) :
a /ₚ u = a / u
@[simp]
theorem map_add_units_neg {α : Type u_1} {M : Type u} [add_monoid M] [subtraction_monoid α] {F : Type u_2} [add_monoid_hom_class F M α] (f : F) (u : add_units M) :
f (-u) = -f u
@[simp]
theorem map_units_inv {α : Type u_1} {M : Type u} [monoid M] [division_monoid α] {F : Type u_2} [monoid_hom_class F M α] (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 → add_units N) (h : ∀ (x : M), (g x) = f x) :

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 → add_units N} (h : ∀ (x : M), (g x) = f x) (x : M) :
@[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) :
@[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 → add_units N} (h : ∀ (x : M), (g x) = f x) (x : M) :
@[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) :
@[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 → add_units N} (h : ∀ (x : M), (g x) = f x) (x : M) :
@[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) :
def add_monoid_hom.to_hom_add_units {G : Type u_1} {M : Type u_2} [add_group G] [add_monoid M] (f : G →+ M) :

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 .

Equations
@[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] [monoid_hom_class F M 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] [add_monoid_hom_class F M 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] [add_monoid_hom_class F M N] [add_monoid_hom_class G N M] {f : F} {x : M} (g : G) (hfg : function.left_inverse g 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] [monoid_hom_class F M N] [monoid_hom_class G N M] {f : F} {x : M} (g : G) (hfg : function.left_inverse g 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] [monoid_hom_class F M N] [monoid_hom_class G N M] {f : F} {x : M} (g : G) (hfg : function.left_inverse g 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] [add_monoid_hom_class F M N] [add_monoid_hom_class G N M] {f : F} {x : M} (g : G) (hfg : function.left_inverse g 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
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)) :

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) :
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) :
@[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) :
@[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) :
@[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) :
@[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) :
@[simp]
theorem is_unit.coe_inv_unit' {α : Type u_3} [division_monoid α] {a : α} (h : is_unit a) :
@[simp]
theorem is_unit.coe_unit' {α : Type u_3} [division_monoid α] {a : α} (h : is_unit a) :
(h.unit') = a
@[simp]
theorem is_add_unit.coe_neg_add_unit' {α : Type u_3} [subtraction_monoid α] {a : α} (h : is_add_unit a) :
def is_add_unit.add_unit' {α : Type u_3} [subtraction_monoid α] {a : α} (h : is_add_unit a) :

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} [division_monoid α] {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]
theorem is_add_unit.coe_add_unit' {α : Type u_3} [subtraction_monoid α] {a : α} (h : is_add_unit a) :
@[protected, simp]
theorem is_add_unit.add_neg_cancel_left {α : Type u_3} [subtraction_monoid α] {a : α} (h : is_add_unit a) (b : α) :
a + (-a + b) = b
@[protected, simp]
theorem is_unit.mul_inv_cancel_left {α : Type u_3} [division_monoid α] {a : α} (h : is_unit a) (b : α) :
a * (a⁻¹ * b) = b
@[protected, simp]
theorem is_add_unit.neg_add_cancel_left {α : Type u_3} [subtraction_monoid α] {a : α} (h : is_add_unit a) (b : α) :
-a + (a + b) = b
@[protected, simp]
theorem is_unit.inv_mul_cancel_left {α : Type u_3} [division_monoid α] {a : α} (h : is_unit a) (b : α) :
a⁻¹ * (a * b) = b
@[protected, simp]
theorem is_unit.mul_inv_cancel_right {α : Type u_3} [division_monoid α] {b : α} (h : is_unit b) (a : α) :
a * b * b⁻¹ = a
@[protected, simp]
theorem is_add_unit.add_neg_cancel_right {α : Type u_3} [subtraction_monoid α] {b : α} (h : is_add_unit b) (a : α) :
a + b + -b = a
@[protected, simp]
theorem is_unit.inv_mul_cancel_right {α : Type u_3} [division_monoid α] {b : α} (h : is_unit b) (a : α) :
a * b⁻¹ * b = a
@[protected, simp]
theorem is_add_unit.neg_add_cancel_right {α : Type u_3} [subtraction_monoid α] {b : α} (h : is_add_unit b) (a : α) :
a + -b + b = a
@[protected]
theorem is_add_unit.sub_self {α : Type u_3} [subtraction_monoid α] {a : α} (h : is_add_unit a) :
a - a = 0
@[protected]
theorem is_unit.div_self {α : Type u_3} [division_monoid α] {a : α} (h : is_unit a) :
a / a = 1
@[protected]
theorem is_unit.eq_mul_inv_iff_mul_eq {α : Type u_3} [division_monoid α] {a b c : α} (h : is_unit c) :
a = b * c⁻¹ a * c = b
@[protected]
theorem is_add_unit.eq_add_neg_iff_add_eq {α : Type u_3} [subtraction_monoid α] {a b c : α} (h : is_add_unit c) :
a = b + -c a + c = b
@[protected]
theorem is_unit.eq_inv_mul_iff_mul_eq {α : Type u_3} [division_monoid α] {a b c : α} (h : is_unit b) :
a = b⁻¹ * c b * a = c
@[protected]
theorem is_add_unit.eq_neg_add_iff_add_eq {α : Type u_3} [subtraction_monoid α] {a b c : α} (h : is_add_unit b) :
a = -b + c b + a = c
@[protected]
theorem is_add_unit.neg_add_eq_iff_eq_add {α : Type u_3} [subtraction_monoid α] {a b c : α} (h : is_add_unit a) :
-a + b = c b = a + c
@[protected]
theorem is_unit.inv_mul_eq_iff_eq_mul {α : Type u_3} [division_monoid α] {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} [division_monoid α] {a b c : α} (h : is_unit b) :
a * b⁻¹ = c a = c * b
@[protected]
theorem is_add_unit.add_neg_eq_iff_eq_add {α : Type u_3} [subtraction_monoid α] {a b c : α} (h : is_add_unit b) :
a + -b = c a = c + b
@[protected]
theorem is_unit.mul_inv_eq_one {α : Type u_3} [division_monoid α] {a b : α} (h : is_unit b) :
a * b⁻¹ = 1 a = b
@[protected]
theorem is_add_unit.add_neg_eq_zero {α : Type u_3} [subtraction_monoid α] {a b : α} (h : is_add_unit b) :
a + -b = 0 a = b
@[protected]
theorem is_add_unit.neg_add_eq_zero {α : Type u_3} [subtraction_monoid α] {a b : α} (h : is_add_unit a) :
-a + b = 0 a = b
@[protected]
theorem is_unit.inv_mul_eq_one {α : Type u_3} [division_monoid α] {a b : α} (h : is_unit a) :
a⁻¹ * b = 1 a = b
@[protected]
theorem is_add_unit.add_eq_zero_iff_eq_neg {α : Type u_3} [subtraction_monoid α] {a b : α} (h : is_add_unit b) :
a + b = 0 a = -b
@[protected]
theorem is_unit.mul_eq_one_iff_eq_inv {α : Type u_3} [division_monoid α] {a b : α} (h : is_unit b) :
a * b = 1 a = b⁻¹
@[protected]
theorem is_unit.mul_eq_one_iff_inv_eq {α : Type u_3} [division_monoid α] {a b : α} (h : is_unit a) :
a * b = 1 a⁻¹ = b
@[protected]
theorem is_add_unit.add_eq_zero_iff_neg_eq {α : Type u_3} [subtraction_monoid α] {a b : α} (h : is_add_unit a) :
a + b = 0 -a = b
@[protected, simp]
theorem is_unit.div_mul_cancel {α : Type u_3} [division_monoid α] {b : α} (h : is_unit b) (a : α) :
a / b * b = a
@[protected, simp]
theorem is_add_unit.sub_add_cancel {α : Type u_3} [subtraction_monoid α] {b : α} (h : is_add_unit b) (a : α) :
a - b + b = a
@[protected, simp]
theorem is_unit.mul_div_cancel {α : Type u_3} [division_monoid α] {b : α} (h : is_unit b) (a : α) :
a * b / b = a
@[protected, simp]
theorem is_add_unit.add_sub_cancel {α : Type u_3} [subtraction_monoid α] {b : α} (h : is_add_unit b) (a : α) :
a + b - b = a
@[protected]
theorem is_unit.mul_one_div_cancel {α : Type u_3} [division_monoid α] {a : α} (h : is_unit a) :
a * (1 / a) = 1
@[protected]
theorem is_add_unit.add_zero_sub_cancel {α : Type u_3} [subtraction_monoid α] {a : α} (h : is_add_unit a) :
a + (0 - a) = 0
@[protected]
theorem is_unit.one_div_mul_cancel {α : Type u_3} [division_monoid α] {a : α} (h : is_unit a) :
1 / a * a = 1
@[protected]
theorem is_add_unit.zero_sub_add_cancel {α : Type u_3} [subtraction_monoid α] {a : α} (h : is_add_unit a) :
0 - a + a = 0
theorem is_unit.inv {α : Type u_3} [division_monoid α] {a : α} :
theorem is_add_unit.neg {α : Type u_3} [subtraction_monoid α] {a : α} :
theorem is_add_unit.sub {α : Type u_3} [subtraction_monoid α] {a b : α} (ha : is_add_unit a) (hb : is_add_unit b) :
theorem is_unit.div {α : Type u_3} [division_monoid α] {a b : α} (ha : is_unit a) (hb : is_unit b) :
is_unit (a / b)
@[protected]
theorem is_unit.div_left_inj {α : Type u_3} [division_monoid α] {a b c : α} (h : is_unit c) :
a / c = b / c a = b
@[protected]
theorem is_add_unit.sub_left_inj {α : Type u_3} [subtraction_monoid α] {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} [subtraction_monoid α] {a b c : α} (h : is_add_unit b) :
a - b = c a = c + b
@[protected]
theorem is_unit.div_eq_iff {α : Type u_3} [division_monoid α] {a b c : α} (h : is_unit b) :
a / b = c a = c * b
@[protected]
theorem is_add_unit.eq_sub_iff {α : Type u_3} [subtraction_monoid α] {a b c : α} (h : is_add_unit c) :
a = b - c a + c = b
@[protected]
theorem is_unit.eq_div_iff {α : Type u_3} [division_monoid α] {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} [division_monoid α] {a b c : α} (h : is_unit b) :
a = c * ba / b = c
@[protected]
theorem is_add_unit.sub_eq_of_eq_add {α : Type u_3} [subtraction_monoid α] {a b c : α} (h : is_add_unit b) :
a = c + ba - b = c
@[protected]
theorem is_unit.eq_div_of_mul_eq {α : Type u_3} [division_monoid α] {a b c : α} (h : is_unit c) :
a * c = ba = b / c
@[protected]
theorem is_add_unit.eq_sub_of_add_eq {α : Type u_3} [subtraction_monoid α] {a b c : α} (h : is_add_unit c) :
a + c = ba = b - c
@[protected]
theorem is_unit.div_eq_one_iff_eq {α : Type u_3} [division_monoid α] {a b : α} (h : is_unit b) :
a / b = 1 a = b
@[protected]
theorem is_add_unit.sub_eq_zero_iff_eq {α : Type u_3} [subtraction_monoid α] {a b : α} (h : is_add_unit b) :
a - b = 0 a = b
@[protected]
theorem is_unit.div_mul_left {α : Type u_3} [division_monoid α] {a b : α} (h : is_unit b) :
b / (a * b) = 1 / a
@[protected]
theorem is_add_unit.sub_add_left {α : Type u_3} [subtraction_monoid α] {a b : α} (h : is_add_unit b) :
b - (a + b) = 0 - a
@[protected]
theorem is_unit.mul_div_mul_right {α : Type u_3} [division_monoid α] {c : α} (h : is_unit c) (a b : α) :
a * c / (b * c) = a / b
@[protected]
theorem is_add_unit.add_sub_add_right {α : Type u_3} [subtraction_monoid α] {c : α} (h : is_add_unit c) (a b : α) :
a + c - (b + c) = a - b
@[protected]
theorem is_add_unit.add_add_sub {α : Type u_3} [subtraction_monoid α] {b : α} (a : α) (h : is_add_unit b) :
a + b + (0 - b) = a
@[protected]
theorem is_unit.mul_mul_div {α : Type u_3} [division_monoid α] {b : α} (a : α) (h : is_unit b) :
a * b * (1 / b) = a
@[protected]
theorem is_unit.div_mul_right {α : Type u_3} [division_comm_monoid α] {a : α} (h : is_unit a) (b : α) :
a / (a * b) = 1 / b
@[protected]
theorem is_add_unit.sub_add_right {α : Type u_3} [subtraction_comm_monoid α] {a : α} (h : is_add_unit a) (b : α) :
a - (a + b) = 0 - b
@[protected]
theorem is_unit.mul_div_cancel_left {α : Type u_3} [division_comm_monoid α] {a : α} (h : is_unit a) (b : α) :
a * b / a = b
@[protected]
theorem is_add_unit.add_sub_cancel_left {α : Type u_3} [subtraction_comm_monoid α] {a : α} (h : is_add_unit a) (b : α) :
a + b - a = b
@[protected]
theorem is_add_unit.add_sub_cancel' {α : Type u_3} [subtraction_comm_monoid α] {a : α} (h : is_add_unit a) (b : α) :
a + (b - a) = b
@[protected]
theorem is_unit.mul_div_cancel' {α : Type u_3} [division_comm_monoid α] {a : α} (h : is_unit a) (b : α) :
a * (b / a) = b
@[protected]
theorem is_unit.mul_div_mul_left {α : Type u_3} [division_comm_monoid α] {c : α} (h : is_unit c) (a b : α) :
c * a / (c * b) = a / b
@[protected]
theorem is_add_unit.add_sub_add_left {α : Type u_3} [subtraction_comm_monoid α] {c : α} (h : is_add_unit c) (a b : α) :
c + a - (c + b) = a - b
@[protected]
theorem is_add_unit.add_eq_add_of_sub_eq_sub {α : Type u_3} [subtraction_comm_monoid α] {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} [division_comm_monoid α] {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} [division_comm_monoid α] {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} [subtraction_comm_monoid α] {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} [division_comm_monoid α] {a b : α} (h : is_unit a) :
a / (a / b) = b
@[protected]
theorem is_add_unit.sub_sub_cancel {α : Type u_3} [subtraction_comm_monoid α] {a b : α} (h : is_add_unit a) :
a - (a - b) = b