mathlib docs: algebra.group.units

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

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

def monoid_hom.to_hom_units {G : Type u_1} {M : Type u_2} [group G] [monoid M] :

(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

f.to_hom_units = {to_fun := λ (g : G), {val := ⇑f g, inv := ⇑f g⁻¹, val_inv := _, inv_val := _}, map_one' := _, map_mul' := _}

source

def add_monoid_hom.to_hom_units {G : Type u_1} {M : Type u_2} [add_group G] [add_monoid M] :

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

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_add_unit.map {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (f : M →+ N) {x : M} :

is_add_unit x → is_add_unit (⇑f x)

source

theorem is_unit.map {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (f : M →* N) {x : M} :

is_unit x → is_unit (⇑f x)

source

def is_add_unit.lift_right {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (f : M →+ N) :

(∀ (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.

source

def is_unit.lift_right {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (f : M →* N) :

(∀ (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

is_unit.lift_right f hf = units.lift_right f (λ (x : M), classical.some _) _

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

mathlib documentation

algebra.group.units_hom

Lift monoid homomorphisms to group homomorphisms of their units subgroups.

General documentation

Additional documentation

Library

mathlib documentation

algebra.​group.​units_hom

Lift monoid homomorphisms to group homomorphisms of their units subgroups.

General documentation

Additional documentation

Library

algebra.group.units_hom