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 βˣ.
• IsLocalHom: A predicate on monoid maps, requiring that it maps nonunits to nonunits. For local rings, this means that the image of the unique maximal ideal is again contained in the unique maximal ideal. This is developed earlier, and in the generality of monoids, as it allows its use in non-local-ring related contexts, but it does have the strange consequence that it does not require local rings, or even rings.

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.

Add a @[to_additive] version of IsLocalHom.

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 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 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 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_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 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 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 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.

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Units.map_mk {M : Type u} {N : Type v} [Monoid M] [Monoid N] (f : M →* N) (val inv : M) (val_inv : val * inv = 1) (inv_val : inv * val = 1) : (map f) { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val } = { val := f val, inv := f inv, val_inv := ⋯, inv_val := ⋯ }

@[simp]

theorem AddUnits.map_mk {M : Type u} {N : Type v} [AddMonoid M] [AddMonoid N] (f : M →+ N) (val inv : M) (val_inv : val + inv = 0) (inv_val : inv + val = 0) : (map f) { val := val, neg := inv, val_neg := val_inv, neg_val := inv_val } = { val := f val, neg := f inv, val_neg := ⋯, neg_val := ⋯ }

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem AddUnits.val_zsmul_eq_zsmul_val {α : Type u_1} [SubtractionMonoid α] (u : AddUnits α) (n : ℤ) : ↑(n • u) = n • ↑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)⁻¹

@[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

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

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

@[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) : ↑((liftRight f g h) x) = f x

@[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) : ↑((liftRight f g h) x) = f x

@[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 * ↑((liftRight f g h) x)⁻¹ = 1

@[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 + ↑(-(liftRight f g h) 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) : ↑((liftRight f g h) x)⁻¹ * f 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) : ↑(-(liftRight f g h) x) + f x = 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 := ⋯ }) ⋯

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

@[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

@[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

theorem IsUnit.map {F : Type u_1} {M : Type u_3} {N : Type u_4} [FunLike F M N] [Monoid M] [Monoid N] [MonoidHomClass F M N] (f : F) {x : M} (h : IsUnit x) : IsUnit (f x)

theorem IsAddUnit.map {F : Type u_1} {M : Type u_3} {N : Type u_4} [FunLike F M N] [AddMonoid M] [AddMonoid N] [AddMonoidHomClass F M N] (f : F) {x : M} (h : IsAddUnit x) : IsAddUnit (f x)

theorem IsUnit.of_leftInverse {F : Type u_1} {G : Type u_2} {M : Type u_3} {N : Type u_4} [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.of_leftInverse {F : Type u_1} {G : Type u_2} {M : Type u_3} {N : Type u_4} [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_map_of_leftInverse {F : Type u_1} {G : Type u_2} {M : Type u_3} {N : Type u_4} [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

Prefer IsLocalHom.of_leftInverse, but we can't get rid of this because of ToAdditive.

theorem isAddUnit_map_of_leftInverse {F : Type u_1} {G : Type u_2} {M : Type u_3} {N : Type u_4} [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

noncomputable def IsUnit.liftRight {M : Type u_3} {N : Type u_4} [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) ⋯

noncomputable def IsAddUnit.liftRight {M : Type u_3} {N : Type u_4} [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) ⋯

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

class IsLocalHom {R : Type u_2} {S : Type u_3} {F : Type u_5} [Monoid R] [Monoid S] [FunLike F R S] (f : F) : Prop

A local ring homomorphism is a map f between monoids such that a in the domain is a unit if f a is a unit for any a. See IsLocalRing.local_hom_TFAE for other equivalent definitions in the local ring case - from where this concept originates, but it is useful in other contexts, so we allow this generalisation in mathlib.

• map_nonunit (a : R) : IsUnit (f a) → IsUnit a

  A local homomorphism f : R ⟶ S will send nonunits of R to nonunits of S.

@[simp]

theorem IsUnit.of_map {R : Type u_2} {S : Type u_3} {F : Type u_5} [Monoid R] [Monoid S] [FunLike F R S] (f : F) [IsLocalHom f] (a : R) (h : IsUnit (f a)) : IsUnit a

theorem isUnit_of_map_unit {R : Type u_2} {S : Type u_3} {F : Type u_5} [Monoid R] [Monoid S] [FunLike F R S] (f : F) [IsLocalHom f] (a : R) (h : IsUnit (f a)) : IsUnit a

Alias of IsUnit.of_map.

@[simp]

theorem isUnit_map_iff {R : Type u_2} {S : Type u_3} {F : Type u_5} [Monoid R] [Monoid S] [FunLike F R S] [MonoidHomClass F R S] (f : F) [IsLocalHom f] (a : R) : IsUnit (f a) ↔ IsUnit a

theorem isLocalHom_of_leftInverse {G : Type u_1} {R : Type u_2} {S : Type u_3} {F : Type u_5} [Monoid R] [Monoid S] [FunLike F R S] [MonoidHomClass F R S] [FunLike G S R] [MonoidHomClass G S R] {f : F} (g : G) (hfg : Function.LeftInverse ⇑g ⇑f) : IsLocalHom f

instance MonoidHom.isLocalHom_comp {R : Type u_2} {S : Type u_3} {T : Type u_4} [Monoid R] [Monoid S] [Monoid T] (g : S →* T) (f : R →* S) [IsLocalHom g] [IsLocalHom f] : IsLocalHom (g.comp f)

@[instance 100]

instance isLocalHom_toMonoidHom {R : Type u_2} {S : Type u_3} {F : Type u_5} [Monoid R] [Monoid S] [FunLike F R S] [MonoidHomClass F R S] (f : F) [IsLocalHom f] : IsLocalHom ↑f

theorem MonoidHom.isLocalHom_of_comp {R : Type u_2} {S : Type u_3} {T : Type u_4} [Monoid R] [Monoid S] [Monoid T] (f : R →* S) (g : S →* T) [IsLocalHom (g.comp f)] : IsLocalHom f