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 βˣ.

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 : 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 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⁻¹.

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 : 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

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

source

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 := (_ : f ↑u + f u.neg = 0), neg_val := (_ : f u.neg + f ↑u = 0) }) (x + y) = (fun (u : AddUnits M) => { val := f ↑u, neg := f u.neg, val_neg := (_ : f ↑u + f u.neg = 0), neg_val := (_ : f u.neg + f ↑u = 0) }) x + (fun (u : AddUnits M) => { val := f ↑u, neg := f u.neg, val_neg := (_ : f ↑u + f u.neg = 0), neg_val := (_ : f u.neg + f ↑u = 0) }) y

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 AddUnits induced by an AddMonoidHom.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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

source

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

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

One or more equations did not get rendered due to their size.

Instances For

source

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

source

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

source

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

source

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

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) :

AddUnits.map (AddMonoidHom.comp g f) = AddMonoidHom.comp (AddUnits.map g) (AddUnits.map f)

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) :

Units.map (MonoidHom.comp g f) = MonoidHom.comp (Units.map g) (Units.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 ⇑(AddUnits.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 ⇑(Units.map f)

source

@[simp]

theorem AddUnits.map_id (M : Type u) [AddMonoid M] :

AddUnits.map (AddMonoidHom.id M) = AddMonoidHom.id (AddUnits M)

source

@[simp]

theorem Units.map_id (M : Type u) [Monoid M] :

Units.map (MonoidHom.id M) = MonoidHom.id Mˣ

source

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

AddUnits M →+ M

Coercion AddUnits M → M as an AddMonoid homomorphism.

Equations

AddUnits.coeHom M = { toZeroHom := { toFun := AddUnits.val, map_zero' := (_ : ↑0 = 0) }, map_add' := (_ : ∀ (a b : AddUnits M), ↑(a + b) = ↑a + ↑b) }

Instances For

source

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

Mˣ →* M

Coercion Mˣ → M as a monoid homomorphism.

Equations

Units.coeHom M = { toOneHom := { toFun := Units.val, map_one' := (_ : ↑1 = 1) }, map_mul' := (_ : ∀ (a b : Mˣ), ↑(a * b) = ↑a * ↑b) }

Instances For

source

@[simp]

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

(AddUnits.coeHom M) x = ↑x

source

@[simp]

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

(Units.coeHom M) x = ↑x

source

@[simp]

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

↑(n • u) = n • ↑u

source

@[simp]

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

↑(u ^ n) = ↑u ^ n

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

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

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

One or more equations did not get rendered due to their size.

Instances For

source

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' := (_ : g 0 = 0) }.toFun (x + y) = { toFun := g, map_zero' := (_ : g 0 = 0) }.toFun x + { toFun := g, map_zero' := (_ : g 0 = 0) }.toFun y

source

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

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

One or more equations did not get rendered due to their size.

Instances For

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) :

↑((AddUnits.liftRight f g h) x) = f x

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) :

↑((Units.liftRight f g h) x) = f x

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 + ↑(-(AddUnits.liftRight f g h) x) = 0

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 * ↑((Units.liftRight f g h) 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) :

↑(-(AddUnits.liftRight f g h) x) + f 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) :

↑((Units.liftRight f g h) x)⁻¹ * f x = 1

source

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

source

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

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

One or more equations did not get rendered due to their size.

Instances For

source

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 := (_ : f g + f (-g) = 0), neg_val := (_ : f (-g) + f g = 0) }) x) = ↑((fun (g : G) => { val := f g, neg := f (-g), val_neg := (_ : f g + f (-g) = 0), neg_val := (_ : f (-g) + f g = 0) }) x)

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

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

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

↑((AddMonoidHom.toHomAddUnits f) g) = f g

source

@[simp]

theorem MonoidHom.coe_toHomUnits {G : Type u_1} {M : Type u_2} [Group G] [Monoid M] (f : G →* M) (g : G) :

↑((MonoidHom.toHomUnits f) g) = f g

source

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)

source

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)

source

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

source

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

source

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

source

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

source

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

One or more equations did not get rendered due to their size.

Instances For

source

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), ↑(IsAddUnit.addUnit (_ : IsAddUnit (f x))) = ↑(IsAddUnit.addUnit (_ : IsAddUnit (f x)))

source

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) => IsUnit.unit (_ : IsUnit (f x))) (_ : ∀ (x : M), ↑(IsUnit.unit (_ : IsUnit (f x))) = ↑(IsUnit.unit (_ : IsUnit (f x))))

Instances For

source

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

source

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

source

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

source

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

source

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

source

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

Documentation

Mathlib.Algebra.Group.Units.Hom

Monoid homomorphisms and units #

Main declarations #