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
is_unit.eq_on_inv
{F : Type u_1}
{G : Type u_2}
{N : Type u_3}
[division_monoid G]
[monoid N]
[monoid_hom_class F G 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}
[subtraction_monoid G]
[add_monoid N]
[add_monoid_hom_class F G N]
{x : G}
(hx : is_add_unit x)
(f g : F)
(h : ⇑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.
The add_group homomorphism on add_units induced by an add_monoid_hom.
@[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
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) :
add_units.map (g.comp f) = (add_units.map g).comp (add_units.map f)
@[simp]
@[simp]
Coercion Mˣ → M as a monoid homomorphism.
Equations
- units.coe_hom M = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _}
Coercion add_units M → M as an add_monoid homomorphism.
Equations
- add_units.coe_hom M = {to_fun := coe coe_to_lift, map_zero' := _, map_add' := _}
@[simp]
@[simp]
theorem
add_units.coe_hom_apply
{M : Type u}
[add_monoid M]
(x : add_units M) :
⇑(add_units.coe_hom M) x = ↑x
@[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) :
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.
@[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) :
↑(⇑(add_units.lift_right f 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 → add_units 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) :
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.
@[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) :
↑(⇑(f.to_hom_add_units) g) = ⇑f g
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) :
is_add_unit (⇑f 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)) :
is_unit 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) :
is_add_unit (⇑f x) ↔ is_add_unit x
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)) :
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
- is_unit.lift_right f hf = units.lift_right f (λ (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)) :
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
- is_add_unit.lift_right f hf = add_units.lift_right f (λ (x : M), _.add_unit) _
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) :
↑(⇑(is_add_unit.lift_right f hf) x) = ⇑f x
@[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_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]
@[simp]
@[simp]
theorem
is_add_unit.coe_neg_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.
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.
@[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 : α) :
@[protected, simp]
theorem
is_unit.mul_inv_cancel_left
{α : Type u_3}
[division_monoid α]
{a : α}
(h : is_unit a)
(b : α) :
@[protected, simp]
theorem
is_add_unit.neg_add_cancel_left
{α : Type u_3}
[subtraction_monoid α]
{a : α}
(h : is_add_unit a)
(b : α) :
@[protected, simp]
theorem
is_unit.inv_mul_cancel_left
{α : Type u_3}
[division_monoid α]
{a : α}
(h : is_unit a)
(b : α) :
@[protected, simp]
theorem
is_unit.mul_inv_cancel_right
{α : Type u_3}
[division_monoid α]
{b : α}
(h : is_unit b)
(a : α) :
@[protected, simp]
theorem
is_add_unit.add_neg_cancel_right
{α : Type u_3}
[subtraction_monoid α]
{b : α}
(h : is_add_unit b)
(a : α) :
@[protected, simp]
theorem
is_unit.inv_mul_cancel_right
{α : Type u_3}
[division_monoid α]
{b : α}
(h : is_unit b)
(a : α) :
@[protected, simp]
theorem
is_add_unit.neg_add_cancel_right
{α : Type u_3}
[subtraction_monoid α]
{b : α}
(h : is_add_unit b)
(a : α) :
@[protected]
@[protected]
@[protected]
theorem
is_add_unit.eq_add_neg_iff_add_eq
{α : Type u_3}
[subtraction_monoid α]
{a b c : α}
(h : is_add_unit 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) :
@[protected]
theorem
is_add_unit.neg_add_eq_iff_eq_add
{α : Type u_3}
[subtraction_monoid α]
{a b c : α}
(h : is_add_unit a) :
@[protected]
theorem
is_add_unit.add_neg_eq_iff_eq_add
{α : Type u_3}
[subtraction_monoid α]
{a b c : α}
(h : is_add_unit b) :
@[protected]
@[protected]
theorem
is_add_unit.add_neg_eq_zero
{α : Type u_3}
[subtraction_monoid α]
{a b : α}
(h : is_add_unit b) :
@[protected]
theorem
is_add_unit.neg_add_eq_zero
{α : Type u_3}
[subtraction_monoid α]
{a b : α}
(h : is_add_unit a) :
@[protected]
@[protected]
theorem
is_add_unit.add_eq_zero_iff_eq_neg
{α : Type u_3}
[subtraction_monoid α]
{a b : α}
(h : is_add_unit b) :
@[protected]
theorem
is_unit.mul_eq_one_iff_eq_inv
{α : Type u_3}
[division_monoid α]
{a b : α}
(h : is_unit b) :
@[protected]
theorem
is_unit.mul_eq_one_iff_inv_eq
{α : Type u_3}
[division_monoid α]
{a b : α}
(h : is_unit a) :
@[protected]
theorem
is_add_unit.add_eq_zero_iff_neg_eq
{α : Type u_3}
[subtraction_monoid α]
{a b : α}
(h : is_add_unit a) :
@[protected, simp]
@[protected, simp]
theorem
is_add_unit.sub_add_cancel
{α : Type u_3}
[subtraction_monoid α]
{b : α}
(h : is_add_unit b)
(a : α) :
@[protected, simp]
@[protected, simp]
theorem
is_add_unit.add_sub_cancel
{α : Type u_3}
[subtraction_monoid α]
{b : α}
(h : is_add_unit b)
(a : α) :
@[protected]
@[protected]
theorem
is_add_unit.add_zero_sub_cancel
{α : Type u_3}
[subtraction_monoid α]
{a : α}
(h : is_add_unit a) :
@[protected]
@[protected]
theorem
is_add_unit.zero_sub_add_cancel
{α : Type u_3}
[subtraction_monoid α]
{a : α}
(h : is_add_unit a) :
theorem
is_add_unit.neg
{α : Type u_3}
[subtraction_monoid α]
{a : α} :
is_add_unit a → is_add_unit (-a)
theorem
is_add_unit.sub
{α : Type u_3}
[subtraction_monoid α]
{a b : α}
(ha : is_add_unit a)
(hb : is_add_unit b) :
is_add_unit (a - b)
theorem
is_unit.div
{α : Type u_3}
[division_monoid α]
{a b : α}
(ha : is_unit a)
(hb : is_unit b) :
@[protected]
@[protected]
theorem
is_add_unit.sub_left_inj
{α : Type u_3}
[subtraction_monoid α]
{a b c : α}
(h : is_add_unit c) :
@[protected]
theorem
is_add_unit.sub_eq_iff
{α : Type u_3}
[subtraction_monoid α]
{a b c : α}
(h : is_add_unit b) :
@[protected]
@[protected]
theorem
is_add_unit.eq_sub_iff
{α : Type u_3}
[subtraction_monoid α]
{a b c : α}
(h : is_add_unit c) :
@[protected]
@[protected]
@[protected]
theorem
is_add_unit.sub_eq_of_eq_add
{α : Type u_3}
[subtraction_monoid α]
{a b c : α}
(h : is_add_unit b) :
@[protected]
@[protected]
theorem
is_add_unit.eq_sub_of_add_eq
{α : Type u_3}
[subtraction_monoid α]
{a b c : α}
(h : is_add_unit c) :
@[protected]
@[protected]
theorem
is_add_unit.sub_eq_zero_iff_eq
{α : Type u_3}
[subtraction_monoid α]
{a b : α}
(h : is_add_unit b) :
@[protected]
The group version of this lemma is div_mul_cancel'''
@[protected]
theorem
is_add_unit.sub_add_left
{α : Type u_3}
[subtraction_monoid α]
{a b : α}
(h : is_add_unit b) :
The add_group version of this lemma is sub_add_cancel''
@[protected]
theorem
is_unit.mul_div_mul_right
{α : Type u_3}
[division_monoid α]
{c : α}
(h : is_unit 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 : α) :
@[protected]
theorem
is_add_unit.add_add_sub
{α : Type u_3}
[subtraction_monoid α]
{b : α}
(a : α)
(h : is_add_unit b) :
@[protected]
@[protected]
theorem
is_unit.div_mul_right
{α : Type u_3}
[division_comm_monoid α]
{a : α}
(h : is_unit a)
(b : α) :
@[protected]
theorem
is_add_unit.sub_add_right
{α : Type u_3}
[subtraction_comm_monoid α]
{a : α}
(h : is_add_unit a)
(b : α) :
@[protected]
theorem
is_unit.mul_div_cancel_left
{α : Type u_3}
[division_comm_monoid α]
{a : α}
(h : is_unit a)
(b : α) :
@[protected]
theorem
is_add_unit.add_sub_cancel_left
{α : Type u_3}
[subtraction_comm_monoid α]
{a : α}
(h : is_add_unit a)
(b : α) :
@[protected]
theorem
is_add_unit.add_sub_cancel'
{α : Type u_3}
[subtraction_comm_monoid α]
{a : α}
(h : is_add_unit a)
(b : α) :
@[protected]
theorem
is_unit.mul_div_cancel'
{α : Type u_3}
[division_comm_monoid α]
{a : α}
(h : is_unit a)
(b : α) :
@[protected]
theorem
is_unit.mul_div_mul_left
{α : Type u_3}
[division_comm_monoid α]
{c : α}
(h : is_unit c)
(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 : α) :
@[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) :
@[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) :
@[protected]
@[protected]
theorem
is_add_unit.sub_sub_cancel
{α : Type u_3}
[subtraction_comm_monoid α]
{a b : α}
(h : is_add_unit a) :
@[protected]
theorem
is_add_unit.sub_sub_cancel_left
{α : Type u_3}
[subtraction_comm_monoid α]
{a b : α}
(h : is_add_unit a) :
@[protected]
theorem
is_unit.div_div_cancel_left
{α : Type u_3}
[division_comm_monoid α]
{a b : α}
(h : is_unit a) :