# 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 MonoidHom.

## Main declarations #

• Units.map: Turn a homomorphism from α to β monoids into a homomorphism from αˣ to βˣ.
• MonoidHom.toHomUnits: Turn a homomorphism from a group α to β into a homomorphism from α to βˣ.
theorem IsAddUnit.eq_on_neg {F : Type u_1} {G : Type u_2} {N : Type u_3} [] [FunLike F G N] [] {x : G} (hx : ) (f : 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 IsUnit.eq_on_inv {F : Type u_1} {G : Type u_2} {N : Type u_3} [] [] [FunLike F G N] [] {x : G} (hx : ) (f : F) (g : F) (h : f x = g x) :
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 eq_on_neg {F : Type u_1} {G : Type u_2} {M : Type u_3} [] [] [FunLike F G M] [] (f : 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} [] [] [FunLike F G M] [] (f : F) (g : F) {x : G} (h : f x = g x) :
f x⁻¹ = g x⁻¹

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

theorem AddUnits.map.proof_3 {M : Type u_1} {N : Type u_2} [] [] (f : M →+ N) (x : ) (y : ) :
(fun (u : ) => { val := f u, neg := f u.neg, val_neg := , neg_val := }) (x + y) = (fun (u : ) => { val := f u, neg := f u.neg, val_neg := , neg_val := }) x + (fun (u : ) => { val := f u, neg := f u.neg, val_neg := , neg_val := }) y
theorem AddUnits.map.proof_1 {M : Type u_2} {N : Type u_1} [] [] (f : M →+ N) (u : ) :
f u + f u.neg = 0
def AddUnits.map {M : Type u} {N : Type v} [] [] (f : M →+ N) :

The additive homomorphism on AddUnits induced by an AddMonoidHom.

Equations
• = AddMonoidHom.mk' (fun (u : ) => { val := f u, neg := f u.neg, val_neg := , neg_val := })
Instances For
theorem AddUnits.map.proof_2 {M : Type u_2} {N : Type u_1} [] [] (f : M →+ N) (u : ) :
f u.neg + f u = 0
def Units.map {M : Type u} {N : Type v} [] [] (f : M →* N) :

The group homomorphism on units induced by a MonoidHom.

Equations
• = MonoidHom.mk' (fun (u : Mˣ) => { val := f u, inv := f u.inv, val_inv := , inv_val := })
Instances For
@[simp]
theorem AddUnits.coe_map {M : Type u} {N : Type v} [] [] (f : M →+ N) (x : ) :
(() x) = f x
@[simp]
theorem Units.coe_map {M : Type u} {N : Type v} [] [] (f : M →* N) (x : Mˣ) :
(() x) = f x
@[simp]
theorem AddUnits.coe_map_neg {M : Type u} {N : Type v} [] [] (f : M →+ N) (u : ) :
(-() u) = f (-u)
@[simp]
theorem Units.coe_map_inv {M : Type u} {N : Type v} [] [] (f : M →* N) (u : Mˣ) :
(() u)⁻¹ = f u⁻¹
@[simp]
theorem AddUnits.map_comp {M : Type u} {N : Type v} {P : Type w} [] [] [] (f : M →+ N) (g : N →+ P) :
AddUnits.map (g.comp f) = ().comp ()
@[simp]
theorem Units.map_comp {M : Type u} {N : Type v} {P : Type w} [] [] [] (f : M →* N) (g : N →* P) :
Units.map (g.comp f) = ().comp ()
theorem AddUnits.map_injective {M : Type u} {N : Type v} [] [] {f : M →+ N} (hf : ) :
theorem Units.map_injective {M : Type u} {N : Type v} [] [] {f : M →* N} (hf : ) :
@[simp]
theorem AddUnits.map_id (M : Type u) [] :
@[simp]
theorem Units.map_id (M : Type u) [] :
def AddUnits.coeHom (M : Type u) [] :
→+ M

Coercion AddUnits M → M as an AddMonoid homomorphism.

Equations
• = { toFun := AddUnits.val, map_zero' := , map_add' := }
Instances For
def Units.coeHom (M : Type u) [] :
Mˣ →* M

Coercion Mˣ → M as a monoid homomorphism.

Equations
• = { toFun := Units.val, map_one' := , map_mul' := }
Instances For
@[simp]
theorem AddUnits.coeHom_apply {M : Type u} [] (x : ) :
() x = x
@[simp]
theorem Units.coeHom_apply {M : Type u} [] (x : Mˣ) :
() x = x
@[simp]
theorem AddUnits.val_zsmul_eq_zsmul_val {α : Type u_1} (u : ) (n : ) :
(n u) = n u
@[simp]
theorem Units.val_zpow_eq_zpow_val {α : Type u_1} [] (u : αˣ) (n : ) :
(u ^ n) = u ^ n
@[simp]
theorem map_addUnits_neg {α : Type u_1} {M : Type u} [] {F : Type u_2} [FunLike F M α] [] (f : F) (u : ) :
f (-u) = -f u
@[simp]
theorem map_units_inv {α : Type u_1} {M : Type u} [] [] {F : Type u_2} [FunLike F M α] [] (f : F) (u : Mˣ) :
f u⁻¹ = (f u)⁻¹
theorem AddUnits.liftRight.proof_2 {M : Type u_2} {N : Type u_1} [] [] (f : M →+ N) (g : M) (h : ∀ (x : M), (g x) = f x) (x : M) (y : M) :
{ toFun := g, map_zero' := }.toFun (x + y) = { toFun := g, map_zero' := }.toFun x + { toFun := g, map_zero' := }.toFun y
theorem AddUnits.liftRight.proof_1 {M : Type u_2} {N : Type u_1} [] [] (f : M →+ N) (g : M) (h : ∀ (x : M), (g x) = f x) :
g 0 = 0
def AddUnits.liftRight {M : Type u} {N : Type v} [] [] (f : M →+ N) (g : M) (h : ∀ (x : M), (g x) = f x) :
M →+

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

Equations
• = { toFun := g, map_zero' := , map_add' := }
Instances For
def Units.liftRight {M : Type u} {N : Type v} [] [] (f : M →* N) (g : MNˣ) (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
• = { toFun := g, map_one' := , map_mul' := }
Instances For
@[simp]
theorem AddUnits.coe_liftRight {M : Type u} {N : Type v} [] [] {f : M →+ N} {g : M} (h : ∀ (x : M), (g x) = f x) (x : M) :
(() x) = f x
@[simp]
theorem Units.coe_liftRight {M : Type u} {N : Type v} [] [] {f : M →* N} {g : MNˣ} (h : ∀ (x : M), (g x) = f x) (x : M) :
(() x) = f x
@[simp]
theorem AddUnits.add_liftRight_neg {M : Type u} {N : Type v} [] [] {f : M →+ N} {g : M} (h : ∀ (x : M), (g x) = f x) (x : M) :
f x + (-() x) = 0
@[simp]
theorem Units.mul_liftRight_inv {M : Type u} {N : Type v} [] [] {f : M →* N} {g : MNˣ} (h : ∀ (x : M), (g x) = f x) (x : M) :
f x * (() x)⁻¹ = 1
@[simp]
theorem AddUnits.liftRight_neg_add {M : Type u} {N : Type v} [] [] {f : M →+ N} {g : M} (h : ∀ (x : M), (g x) = f x) (x : M) :
(-() x) + f x = 0
@[simp]
theorem Units.liftRight_inv_mul {M : Type u} {N : Type v} [] [] {f : M →* N} {g : MNˣ} (h : ∀ (x : M), (g x) = f x) (x : M) :
(() x)⁻¹ * f x = 1
theorem AddMonoidHom.toHomAddUnits.proof_2 {G : Type u_2} {M : Type u_1} [] [] (f : G →+ M) (g : G) :
f (-g) + f g = 0
def AddMonoidHom.toHomAddUnits {G : Type u_1} {M : Type u_2} [] [] (f : G →+ M) :
G →+

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

Equations
• f.toHomAddUnits = AddUnits.liftRight f (fun (g : G) => { val := f g, neg := f (-g), val_neg := , neg_val := })
Instances For
theorem AddMonoidHom.toHomAddUnits.proof_1 {G : Type u_2} {M : Type u_1} [] [] (f : G →+ M) (g : G) :
f g + f (-g) = 0
theorem AddMonoidHom.toHomAddUnits.proof_3 {G : Type u_2} {M : Type u_1} [] [] (f : G →+ M) :
∀ (x : G), ((fun (g : G) => { val := f g, neg := f (-g), val_neg := , neg_val := }) x) = ((fun (g : G) => { val := f g, neg := f (-g), val_neg := , neg_val := }) x)
def MonoidHom.toHomUnits {G : Type u_1} {M : Type u_2} [] [] (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.toHomUnits is the corresponding monoid homomorphism from G to Mˣ.

Equations
• f.toHomUnits = Units.liftRight f (fun (g : G) => { val := f g, inv := f g⁻¹, val_inv := , inv_val := })
Instances For
@[simp]
theorem AddMonoidHom.coe_toHomAddUnits {G : Type u_1} {M : Type u_2} [] [] (f : G →+ M) (g : G) :
@[simp]
theorem MonoidHom.coe_toHomUnits {G : Type u_1} {M : Type u_2} [] [] (f : G →* M) (g : G) :
(f.toHomUnits g) = f g
theorem IsAddUnit.map {F : Type u_1} {M : Type u_4} {N : Type u_5} [FunLike F M N] [] [] [] (f : F) {x : M} (h : ) :
theorem IsUnit.map {F : Type u_1} {M : Type u_4} {N : Type u_5} [FunLike F M N] [] [] [] (f : F) {x : M} (h : ) :
IsUnit (f x)
theorem IsAddUnit.of_leftInverse {F : Type u_1} {G : Type u_2} {M : Type u_4} {N : Type u_5} [FunLike F M N] [FunLike G N M] [] [] [] {f : F} {x : M} (g : G) (hfg : ) (h : IsAddUnit (f x)) :
theorem IsUnit.of_leftInverse {F : Type u_1} {G : Type u_2} {M : Type u_4} {N : Type u_5} [FunLike F M N] [FunLike G N M] [] [] [] {f : F} {x : M} (g : G) (hfg : ) (h : IsUnit (f x)) :
theorem isAddUnit_map_of_leftInverse {F : Type u_1} {G : Type u_2} {M : Type u_4} {N : Type u_5} [FunLike F M N] [FunLike G N M] [] [] [] [] {f : F} {x : M} (g : G) (hfg : ) :
theorem isUnit_map_of_leftInverse {F : Type u_1} {G : Type u_2} {M : Type u_4} {N : Type u_5} [FunLike F M N] [FunLike G N M] [] [] [] [] {f : F} {x : M} (g : G) (hfg : ) :
IsUnit (f x)
theorem IsAddUnit.liftRight.proof_1 {M : Type u_2} {N : Type u_1} [] [] (f : M →+ N) (hf : ∀ (x : M), IsAddUnit (f x)) :
noncomputable def IsAddUnit.liftRight {M : Type u_4} {N : Type u_5} [] [] (f : M →+ N) (hf : ∀ (x : M), IsAddUnit (f x)) :
M →+

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

Equations
Instances For
noncomputable def IsUnit.liftRight {M : Type u_4} {N : Type u_5} [] [] (f : M →* N) (hf : ∀ (x : M), IsUnit (f x)) :
M →* Nˣ

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

Equations
Instances For
theorem IsAddUnit.coe_liftRight {M : Type u_4} {N : Type u_5} [] [] (f : M →+ N) (hf : ∀ (x : M), IsAddUnit (f x)) (x : M) :
(() x) = f x
theorem IsUnit.coe_liftRight {M : Type u_4} {N : Type u_5} [] [] (f : M →* N) (hf : ∀ (x : M), IsUnit (f x)) (x : M) :
(() x) = f x
@[simp]
theorem IsAddUnit.add_liftRight_neg {M : Type u_4} {N : Type u_5} [] [] (f : M →+ N) (h : ∀ (x : M), IsAddUnit (f x)) (x : M) :
f x + (-() x) = 0
@[simp]
theorem IsUnit.mul_liftRight_inv {M : Type u_4} {N : Type u_5} [] [] (f : M →* N) (h : ∀ (x : M), IsUnit (f x)) (x : M) :
f x * (() x)⁻¹ = 1
@[simp]
theorem IsAddUnit.liftRight_neg_add {M : Type u_4} {N : Type u_5} [] [] (f : M →+ N) (h : ∀ (x : M), IsAddUnit (f x)) (x : M) :
(-() x) + f x = 0
@[simp]
theorem IsUnit.liftRight_inv_mul {M : Type u_4} {N : Type u_5} [] [] (f : M →* N) (h : ∀ (x : M), IsUnit (f x)) (x : M) :
(() x)⁻¹ * f x = 1