mathlib documentation

algebra.group.units_hom

Lift monoid homomorphisms to group homomorphisms of their units subgroups. #

source
def units.map {M : Type u} {N : Type v} [monoid M] [monoid N] (f : M →* N) :
units M →* units N

The group homomorphism on units induced by a monoid_hom.

Equations
source
def add_units.map {M : Type u} {N : Type v} [add_monoid M] [add_monoid N] (f : M →+ N) :
add_units M →+ add_units N

The add_group homomorphism on add_units induced by an add_monoid_hom.

Equations
source
@[simp]
theorem units.coe_map {M : Type u} {N : Type v} [monoid M] [monoid N] (f : M →* N) (x : units M) :
↑(⇑(units.map f) x) = ⇑f ↑x
source
@[simp]
theorem add_units.coe_map {M : Type u} {N : Type v} [add_monoid M] [add_monoid N] (f : M →+ N) (x : add_units M) :
↑(⇑(add_units.map f) x) = ⇑f ↑x
source
@[simp]
theorem add_units.coe_map_neg {M : Type u} {N : Type v} [add_monoid M] [add_monoid N] (f : M →+ N) (u : add_units M) :
↑-⇑(add_units.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 : units M) :
↑(⇑(units.map f) u)⁻¹ = ⇑f ↑u⁻¹
source
@[simp]
theorem add_units.map_comp {M : Type u} {N : Type v} {P : Type w} [add_monoid M] [add_monoid N] [add_monoid P] (f : M →+ N) (g : N →+ P) :
add_units.map (g.comp f) = (add_units.map g).comp (add_units.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 (g.comp f) = (units.map g).comp (units.map f)
source
@[simp]
theorem units.map_id (M : Type u) [monoid M] :
units.map (monoid_hom.id M) = monoid_hom.id (units M)
source
@[simp]
theorem add_units.map_id (M : Type u) [add_monoid M] :
add_units.map (add_monoid_hom.id M) = add_monoid_hom.id (add_units M)
source
def units.coe_hom (M : Type u) [monoid M] :
units M →* M

Coercion units M → M as a monoid homomorphism.

Equations
source
def add_units.coe_hom (M : Type u) [add_monoid M] :
add_units M →+ M

Coercion add_units M → M as an add_monoid homomorphism.

Equations
source
@[simp]
theorem units.coe_hom_apply {M : Type u} [monoid M] (x : units M) :
⇑(units.coe_hom M) x = ↑x
source
@[simp]
theorem add_units.coe_hom_apply {M : Type u} [add_monoid M] (x : add_units M) :
⇑(add_units.coe_hom M) x = ↑x
source
def units.lift_right {M : Type u} {N : Type v} [monoid M] [monoid N] (f : M →* N) (g : M → units N) (h : ∀ (x : M), ↑(g x) = ⇑f x) :
M →* units N

If a map g : M → units N agrees with a homomorphism f : M →* N, then this map is a monoid homomorphism too.

Equations
source
def add_units.lift_right {M : Type u} {N : Type v} [add_monoid M] [add_monoid N] (f : M →+ N) (g : M → add_units N) (h : ∀ (x : M), ↑(g x) = ⇑f x) :
M →+ add_units N

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

Equations
source
@[simp]
theorem add_units.coe_lift_right {M : Type u} {N : Type v} [add_monoid M] [add_monoid N] {f : M →+ N} {g : M → add_units N} (h : ∀ (x : M), ↑(g x) = ⇑f x) (x : M) :
↑(⇑(add_units.lift_right f g h) x) = ⇑f x
source
@[simp]
theorem units.coe_lift_right {M : Type u} {N : Type v} [monoid M] [monoid N] {f : M →* N} {g : M → units N} (h : ∀ (x : M), ↑(g x) = ⇑f x) (x : M) :
↑(⇑(units.lift_right f g h) x) = ⇑f x
source
@[simp]
theorem add_units.add_lift_right_neg {M : Type u} {N : Type v} [add_monoid M] [add_monoid N] {f : M →+ N} {g : M → add_units N} (h : ∀ (x : M), ↑(g x) = ⇑f x) (x : M) :
⇑f x + ↑-⇑(add_units.lift_right f g h) x = 0
source
@[simp]
theorem units.mul_lift_right_inv {M : Type u} {N : Type v} [monoid M] [monoid N] {f : M →* N} {g : M → units N} (h : ∀ (x : M), ↑(g x) = ⇑f x) (x : M) :
(⇑f x) * ↑(⇑(units.lift_right f g h) x)⁻¹ = 1
source
@[simp]
theorem add_units.lift_right_neg_add {M : Type u} {N : Type v} [add_monoid M] [add_monoid N] {f : M →+ N} {g : M → add_units N} (h : ∀ (x : M), ↑(g x) = ⇑f x) (x : M) :
↑-⇑(add_units.lift_right f g h) x + ⇑f x = 0
source
@[simp]
theorem units.lift_right_inv_mul {M : Type u} {N : Type v} [monoid M] [monoid N] {f : M →* N} {g : M → units N} (h : ∀ (x : M), ↑(g x) = ⇑f x) (x : M) :
(↑(⇑(units.lift_right f g h) x)⁻¹) * ⇑f x = 1
source
def add_monoid_hom.to_hom_units {G : Type u_1} {M : Type u_2} [add_group G] [add_monoid M] (f : G →+ M) :
G →+ add_units M

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

Equations
source
def monoid_hom.to_hom_units {G : Type u_1} {M : Type u_2} [group G] [monoid M] (f : G →* M) :
G →* units 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.to_hom_units is the corresponding monoid homomorphism from G to units M.

Equations
source
@[simp]
theorem monoid_hom.coe_to_hom_units {G : Type u_1} {M : Type u_2} [group G] [monoid M] (f : G →* M) (g : G) :
↑(⇑(f.to_hom_units) g) = ⇑f g
source
theorem is_unit.map {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (f : M →* N) {x : M} (h : is_unit x) :
is_unit (⇑f x)
source
theorem is_add_unit.map {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (f : M →+ N) {x : M} (h : is_add_unit x) :
is_add_unit (⇑f x)
source
noncomputable def is_unit.lift_right {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (f : M →* N) (hf : ∀ (x : M), is_unit (⇑f x)) :
M →* units N

If a homomorphism f : M →* N sends each element to an is_unit, then it can be lifted to f : M →* units N. See also units.lift_right for a computable version.

Equations
source
noncomputable def is_add_unit.lift_right {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (f : M →+ N) (hf : ∀ (x : M), is_add_unit (⇑f x)) :
M →+ add_units N

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

Equations
source
theorem is_unit.coe_lift_right {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (f : M →* N) (hf : ∀ (x : M), is_unit (⇑f x)) (x : M) :
↑(⇑(is_unit.lift_right f hf) x) = ⇑f x
source
theorem is_add_unit.coe_lift_right {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (f : M →+ N) (hf : ∀ (x : M), is_add_unit (⇑f x)) (x : M) :
↑(⇑(is_add_unit.lift_right f hf) x) = ⇑f x
source
@[simp]
theorem is_unit.mul_lift_right_inv {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (f : M →* N) (h : ∀ (x : M), is_unit (⇑f x)) (x : M) :
(⇑f x) * ↑(⇑(is_unit.lift_right f h) x)⁻¹ = 1
source
@[simp]
theorem is_add_unit.add_lift_right_neg {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (f : M →+ N) (h : ∀ (x : M), is_add_unit (⇑f x)) (x : M) :
⇑f x + ↑-⇑(is_add_unit.lift_right f h) x = 0
source
@[simp]
theorem is_unit.lift_right_inv_mul {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (f : M →* N) (h : ∀ (x : M), is_unit (⇑f x)) (x : M) :
(↑(⇑(is_unit.lift_right f h) x)⁻¹) * ⇑f x = 1
source
@[simp]
theorem is_add_unit.lift_right_neg_add {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (f : M →+ N) (h : ∀ (x : M), is_add_unit (⇑f x)) (x : M) :
↑-⇑(is_add_unit.lift_right f h) x + ⇑f x = 0