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} [SubtractionMonoid G] [AddMonoid N] [FunLike F G N] [AddMonoidHomClass F G N] {x : G} (hx : IsAddUnit x) (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} [DivisionMonoid G] [Monoid N] [FunLike F G N] [MonoidHomClass F G N] {x : G} (hx : IsUnit x) (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} [AddGroup G] [AddMonoid M] [FunLike F G M] [AddMonoidHomClass 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} [Group G] [Monoid M] [FunLike F G M] [MonoidHomClass 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} [AddMonoid M] [AddMonoid N] (f : M →+ N) (x : AddUnits M) (y : AddUnits M) : (fun (u : AddUnits M) => { val := f ↑u, neg := f u.neg, val_neg := ⋯, neg_val := ⋯ }) (x + y) = (fun (u : AddUnits M) => { val := f ↑u, neg := f u.neg, val_neg := ⋯, neg_val := ⋯ }) x + (fun (u : AddUnits M) => { val := f ↑u, neg := f u.neg, val_neg := ⋯, neg_val := ⋯ }) y

theorem AddUnits.map.proof_2 {M : Type u_2} {N : Type u_1} [AddMonoid M] [AddMonoid N] (f : M →+ N) (u : AddUnits M) : f u.neg + f ↑u = 0

theorem AddUnits.map.proof_1 {M : Type u_2} {N : Type u_1} [AddMonoid M] [AddMonoid N] (f : M →+ N) (u : AddUnits M) : f ↑u + f u.neg = 0

def AddUnits.map {M : Type u} {N : Type v} [AddMonoid M] [AddMonoid N] (f : M →+ N) : AddUnits M →+ AddUnits N

The additive homomorphism on AddUnits induced by an AddMonoidHom.

Equations

• AddUnits.map f = AddMonoidHom.mk' (fun (u : AddUnits M) => { val := f ↑u, neg := f u.neg, val_neg := ⋯, neg_val := ⋯ }) ⋯

def Units.map {M : Type u} {N : Type v} [Monoid M] [Monoid N] (f : M →* N) : Mˣ →* Nˣ

The group homomorphism on units induced by a MonoidHom.

Equations

• Units.map f = MonoidHom.mk' (fun (u : Mˣ) => { val := f ↑u, inv := f u.inv, val_inv := ⋯, inv_val := ⋯ }) ⋯

@[simp]

theorem AddUnits.coe_map {M : Type u} {N : Type v} [AddMonoid M] [AddMonoid N] (f : M →+ N) (x : AddUnits M) : ↑((AddUnits.map f) x) = f ↑x

@[simp]

theorem Units.coe_map {M : Type u} {N : Type v} [Monoid M] [Monoid N] (f : M →* N) (x : Mˣ) : ↑((Units.map f) x) = f ↑x

@[simp]

theorem AddUnits.coe_map_neg {M : Type u} {N : Type v} [AddMonoid M] [AddMonoid N] (f : M →+ N) (u : AddUnits M) : ↑(-(AddUnits.map f) u) = f ↑(-u)

@[simp]

theorem Units.coe_map_inv {M : Type u} {N : Type v} [Monoid M] [Monoid N] (f : M →* N) (u : Mˣ) : ↑((Units.map f) u)⁻¹ = f ↑u⁻¹

@[simp]

theorem AddUnits.map_comp {M : Type u} {N : Type v} {P : Type w} [AddMonoid M] [AddMonoid N] [AddMonoid P] (f : M →+ N) (g : N →+ P) : AddUnits.map (g.comp f) = (AddUnits.map g).comp (AddUnits.map f)

@[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) : Units.map (g.comp f) = (Units.map g).comp (Units.map f)

theorem AddUnits.map_injective {M : Type u} {N : Type v} [AddMonoid M] [AddMonoid N] {f : M →+ N} (hf : Function.Injective ⇑f) : Function.Injective ⇑(AddUnits.map f)

theorem Units.map_injective {M : Type u} {N : Type v} [Monoid M] [Monoid N] {f : M →* N} (hf : Function.Injective ⇑f) : Function.Injective ⇑(Units.map f)

@[simp]

theorem AddUnits.map_id (M : Type u) [AddMonoid M] : AddUnits.map (AddMonoidHom.id M) = AddMonoidHom.id (AddUnits M)

@[simp]

theorem Units.map_id (M : Type u) [Monoid M] : Units.map (MonoidHom.id M) = MonoidHom.id Mˣ

def AddUnits.coeHom (M : Type u) [AddMonoid M] : AddUnits M →+ M

Coercion AddUnits M → M as an AddMonoid homomorphism.

Equations

• AddUnits.coeHom M = { toFun := AddUnits.val, map_zero' := ⋯, map_add' := ⋯ }

def Units.coeHom (M : Type u) [Monoid M] : Mˣ →* M

Coercion Mˣ → M as a monoid homomorphism.

Equations

• Units.coeHom M = { toFun := Units.val, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem AddUnits.coeHom_apply {M : Type u} [AddMonoid M] (x : AddUnits M) : (AddUnits.coeHom M) x = ↑x

@[simp]

theorem Units.coeHom_apply {M : Type u} [Monoid M] (x : Mˣ) : (Units.coeHom M) x = ↑x

@[simp]

theorem AddUnits.val_zsmul_eq_zsmul_val {α : Type u_1} [SubtractionMonoid α] (u : AddUnits α) (n : ℤ) : ↑(n • u) = n • ↑u

@[simp]

theorem Units.val_zpow_eq_zpow_val {α : Type u_1} [DivisionMonoid α] (u : αˣ) (n : ℤ) : ↑(u ^ n) = ↑u ^ n

@[simp]

theorem map_addUnits_neg {α : Type u_1} {M : Type u} [AddMonoid M] [SubtractionMonoid α] {F : Type u_2} [FunLike F M α] [AddMonoidHomClass F M α] (f : F) (u : AddUnits M) : f ↑(-u) = -f ↑u

@[simp]

theorem map_units_inv {α : Type u_1} {M : Type u} [Monoid M] [DivisionMonoid α] {F : Type u_2} [FunLike F M α] [MonoidHomClass F M α] (f : F) (u : Mˣ) : f ↑u⁻¹ = (f ↑u)⁻¹

def AddUnits.liftRight {M : Type u} {N : Type v} [AddMonoid M] [AddMonoid N] (f : M →+ N) (g : M → AddUnits N) (h : ∀ (x : M), ↑(g x) = f x) : M →+ AddUnits N

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

Equations

• AddUnits.liftRight f g h = { toFun := g, map_zero' := ⋯, map_add' := ⋯ }

theorem AddUnits.liftRight.proof_2 {M : Type u_2} {N : Type u_1} [AddMonoid M] [AddMonoid N] (f : M →+ N) (g : M → AddUnits N) (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} [AddMonoid M] [AddMonoid N] (f : M →+ N) (g : M → AddUnits N) (h : ∀ (x : M), ↑(g x) = f x) : g 0 = 0

def Units.liftRight {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

• Units.liftRight f g h = { toFun := g, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem AddUnits.coe_liftRight {M : Type u} {N : Type v} [AddMonoid M] [AddMonoid N] {f : M →+ N} {g : M → AddUnits N} (h : ∀ (x : M), ↑(g x) = f x) (x : M) : ↑((AddUnits.liftRight f g h) x) = f x

@[simp]

theorem Units.coe_liftRight {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) : ↑((Units.liftRight f g h) x) = f x

@[simp]

theorem AddUnits.add_liftRight_neg {M : Type u} {N : Type v} [AddMonoid M] [AddMonoid N] {f : M →+ N} {g : M → AddUnits N} (h : ∀ (x : M), ↑(g x) = f x) (x : M) : f x + ↑(-(AddUnits.liftRight f g h) x) = 0

@[simp]

theorem Units.mul_liftRight_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 * ↑((Units.liftRight f g h) x)⁻¹ = 1

@[simp]

theorem AddUnits.liftRight_neg_add {M : Type u} {N : Type v} [AddMonoid M] [AddMonoid N] {f : M →+ N} {g : M → AddUnits N} (h : ∀ (x : M), ↑(g x) = f x) (x : M) : ↑(-(AddUnits.liftRight f g h) x) + f x = 0

@[simp]

theorem Units.liftRight_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) : ↑((Units.liftRight f g h) x)⁻¹ * f x = 1

theorem AddMonoidHom.toHomAddUnits.proof_3 {G : Type u_2} {M : Type u_1} [AddGroup G] [AddMonoid M] (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 AddMonoidHom.toHomAddUnits {G : Type u_1} {M : Type u_2} [AddGroup G] [AddMonoid M] (f : G →+ M) : G →+ AddUnits M

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 := ⋯ }) ⋯

theorem AddMonoidHom.toHomAddUnits.proof_2 {G : Type u_2} {M : Type u_1} [AddGroup G] [AddMonoid M] (f : G →+ M) (g : G) : f (-g) + f g = 0

theorem AddMonoidHom.toHomAddUnits.proof_1 {G : Type u_2} {M : Type u_1} [AddGroup G] [AddMonoid M] (f : G →+ M) (g : G) : f g + f (-g) = 0

def MonoidHom.toHomUnits {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.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 := ⋯ }) ⋯

@[simp]

theorem AddMonoidHom.coe_toHomAddUnits {G : Type u_1} {M : Type u_2} [AddGroup G] [AddMonoid M] (f : G →+ M) (g : G) : ↑(f.toHomAddUnits g) = f g

@[simp]

theorem MonoidHom.coe_toHomUnits {G : Type u_1} {M : Type u_2} [Group G] [Monoid M] (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] [AddMonoid M] [AddMonoid N] [AddMonoidHomClass F M N] (f : F) {x : M} (h : IsAddUnit x) : IsAddUnit (f x)

theorem IsUnit.map {F : Type u_1} {M : Type u_4} {N : Type u_5} [FunLike F M N] [Monoid M] [Monoid N] [MonoidHomClass F M N] (f : F) {x : M} (h : IsUnit x) : 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] [AddMonoid M] [AddMonoid N] [AddMonoidHomClass G N M] {f : F} {x : M} (g : G) (hfg : Function.LeftInverse ⇑g ⇑f) (h : IsAddUnit (f x)) : IsAddUnit 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] [Monoid M] [Monoid N] [MonoidHomClass G N M] {f : F} {x : M} (g : G) (hfg : Function.LeftInverse ⇑g ⇑f) (h : IsUnit (f x)) : IsUnit 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] [AddMonoid M] [AddMonoid N] [AddMonoidHomClass F M N] [AddMonoidHomClass G N M] {f : F} {x : M} (g : G) (hfg : Function.LeftInverse ⇑g ⇑f) : IsAddUnit (f x) ↔ IsAddUnit x

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] [Monoid M] [Monoid N] [MonoidHomClass F M N] [MonoidHomClass G N M] {f : F} {x : M} (g : G) (hfg : Function.LeftInverse ⇑g ⇑f) : IsUnit (f x) ↔ IsUnit x

theorem IsAddUnit.liftRight.proof_1 {M : Type u_2} {N : Type u_1} [AddMonoid M] [AddMonoid N] (f : M →+ N) (hf : ∀ (x : M), IsAddUnit (f x)) : ∀ (x : M), ↑⋯.addUnit = ↑⋯.addUnit

noncomputable def IsAddUnit.liftRight {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] (f : M →+ N) (hf : ∀ (x : M), IsAddUnit (f x)) : M →+ AddUnits N

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

• IsAddUnit.liftRight f hf = AddUnits.liftRight f (fun (x : M) => ⋯.addUnit) ⋯

noncomputable def IsUnit.liftRight {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] (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

• IsUnit.liftRight f hf = Units.liftRight f (fun (x : M) => ⋯.unit) ⋯

theorem IsAddUnit.coe_liftRight {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] (f : M →+ N) (hf : ∀ (x : M), IsAddUnit (f x)) (x : M) : ↑((IsAddUnit.liftRight f hf) x) = f x

theorem IsUnit.coe_liftRight {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] (f : M →* N) (hf : ∀ (x : M), IsUnit (f x)) (x : M) : ↑((IsUnit.liftRight f hf) x) = f x

@[simp]

theorem IsAddUnit.add_liftRight_neg {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] (f : M →+ N) (h : ∀ (x : M), IsAddUnit (f x)) (x : M) : f x + ↑(-(IsAddUnit.liftRight f h) x) = 0

@[simp]

theorem IsUnit.mul_liftRight_inv {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] (f : M →* N) (h : ∀ (x : M), IsUnit (f x)) (x : M) : f x * ↑((IsUnit.liftRight f h) x)⁻¹ = 1

@[simp]

theorem IsAddUnit.liftRight_neg_add {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] (f : M →+ N) (h : ∀ (x : M), IsAddUnit (f x)) (x : M) : ↑(-(IsAddUnit.liftRight f h) x) + f x = 0

@[simp]

theorem IsUnit.liftRight_inv_mul {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] (f : M →* N) (h : ∀ (x : M), IsUnit (f x)) (x : M) : ↑((IsUnit.liftRight f h) x)⁻¹ * f x = 1