# 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 the local rings, that is, applied to their multiplicative monoids, 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`.

source
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⁻¹`.

source
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`.

source
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⁻¹`.

source
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`.

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

Instances For

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

The additive homomorphism on `AddUnit`s 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 := ⋯ }) ⋯

Instances For

source
@[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
source
@[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
source
@[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⁻¹
source
@[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)
source
@[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 := ⋯ }
source
@[simp]
theorem AddUnits.map_mk {M : Type u} {N : Type v} [AddMonoid M] [AddMonoid N] (f : M →+ N) (val neg : M) (val_neg : val + neg = 0) (neg_val : neg + val = 0) :
(map f) { val := val, neg := neg, val_neg := val_neg, neg_val := neg_val } = { val := f val, neg := f neg, val_neg := ⋯, neg_val := ⋯ }
source
@[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)
source
@[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)
source
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)
source
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)
source
@[simp]
theorem Units.map_id (M : Type u) [Monoid M] :
map (MonoidHom.id M) = MonoidHom.id M ˣ
source
@[simp]
theorem AddUnits.map_id (M : Type u) [AddMonoid M] :
map (AddMonoidHom.id M) = AddMonoidHom.id (AddUnits M)
source
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' := ⋯ }

Instances For

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

Instances For

source
@[simp]
theorem Units.coeHom_apply {M : Type u} [Monoid M] (x : M ˣ) :
(coeHom M) x = ↑x
source
@[simp]
theorem AddUnits.coeHom_apply {M : Type u} [AddMonoid M] (x : AddUnits M) :
(coeHom M) x = ↑x
source
theorem Units.coeHom_injective {M : Type u} [Monoid M] :
Function.Injective ⇑(coeHom M)
source
theorem AddUnits.coeHom_injective {M : Type u} [AddMonoid M] :
Function.Injective ⇑(coeHom M)
source
@[simp]
theorem Units.val_zpow_eq_zpow_val {α : Type u_1} [DivisionMonoid α] (u : α ˣ) (n : ℤ) :
↑(u ^ n) = ↑u ^ n
source
@[simp]
theorem AddUnits.val_zsmul_eq_zsmul_val {α : Type u_1} [SubtractionMonoid α] (u : AddUnits α) (n : ℤ) :
↑(n • u) = n • ↑u
source
@[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)⁻¹
source
@[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
source
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' := ⋯ }

Instances For

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

Instances For

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

Instances For

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

Instances For

source
@[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
source
@[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
source
@[simp]
theorem MonoidHom.toHomUnits_mul {G : Type u_1} {M : Type u_2} [Group G] [CommMonoid M] (f g : G →* M) :
(f * g).toHomUnits = f.toHomUnits * g.toHomUnits
source
def MonoidHom.toHomUnitsMulEquiv {G : Type u_1} {M : Type u_2} [Group G] [CommMonoid M] :
(G →* M) ≃* (G →* M ˣ)

`MonoidHom.toHomUnits` as a `MulEquiv`.

Equations

- MonoidHom.toHomUnitsMulEquiv = { toFun := MonoidHom.toHomUnits, invFun := fun (f : G →* M ˣ) => (Units.coeHom M).comp f, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

Instances For

source
@[simp]
theorem MonoidHom.toHomUnitsMulEquiv_apply {G : Type u_1} {M : Type u_2} [Group G] [CommMonoid M] (f : G →* M) :
toHomUnitsMulEquiv f = f.toHomUnits
source
@[simp]
theorem MonoidHom.toHomUnitsMulEquiv_symm_apply {G : Type u_1} {M : Type u_2} [Group G] [CommMonoid M] (f : G →* M ˣ) :
toHomUnitsMulEquiv.symm f = (Units.coeHom M).comp f
source
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)
source
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)
source
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
source
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
source
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`.

source
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
source
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) ⋯

Instances For

source
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) ⋯

Instances For

source
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
source
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
source
@[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
source
@[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
source
@[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
source
@[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
source
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 map `f` between monoids is local if any `a` in the domain is a unit whenever `f a` is a unit. 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`.

Instances

source
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
source
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`.

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