mathlib documentation

deprecated.group

Unbundled monoid and group homomorphisms (deprecated)

This file defines typeclasses for unbundled monoid and group homomorphisms. Though these classes are deprecated, they are still widely used in mathlib, and probably will not go away before Lean 4 because Lean 3 often fails to coerce a bundled homomorphism to a function.

main definitions

monoid_hom, is_monoid_hom (deprecated), is_group_hom (deprecated)

implementation notes

There's a coercion from bundled homs to fun, and the canonical notation is to use the bundled hom as a function via this coercion.

There is no group_hom -- the idea is that monoid_hom is used. The constructor for monoid_hom needs a proof of map_one as well as map_mul; a separate constructor monoid_hom.mk' will construct group homs (i.e. monoid homs between groups) given only a proof that multiplication is preserved,

Throughout the monoid_hom section implicit {} brackets are often used instead of type class [] brackets. This is done when the instances can be inferred because they are implicit arguments to the type monoid_hom. When they can be inferred from the type it is faster to use this method than to use type class inference.

Tags

is_group_hom, is_monoid_hom, monoid_hom

@[class]
structure is_add_hom {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] :
(α → β) → Prop
  • map_add : ∀ (x y : α), f (x + y) = f x + f y

Predicate for maps which preserve an addition.

Instances
@[class]
structure is_mul_hom {α : Type u_1} {β : Type u_2} [has_mul α] [has_mul β] :
(α → β) → Prop
  • map_mul : ∀ (x y : α), f (x * y) = (f x) * f y

Predicate for maps which preserve a multiplication.

Instances
@[instance]
def is_add_hom.id {α : Type u} [has_add α] :

The identity map preserves addition

@[instance]
def is_mul_hom.id {α : Type u} [has_mul α] :

The identity map preserves multiplication.

theorem is_add_hom.comp {α : Type u} {β : Type v} [has_add α] [has_add β] {γ : Type u_1} [has_add γ] (f : α → β) (g : β → γ) [is_add_hom f] [hg : is_add_hom g] :

The composition of addition preserving maps also preserves addition

theorem is_mul_hom.comp {α : Type u} {β : Type v} [has_mul α] [has_mul β] {γ : Type u_1} [has_mul γ] (f : α → β) (g : β → γ) [is_mul_hom f] [hg : is_mul_hom g] :

The composition of maps which preserve multiplication, also preserves multiplication.

@[instance]
theorem is_mul_hom.mul {α : Type u_1} {β : Type u_2} [semigroup α] [comm_semigroup β] (f g : α → β) [is_mul_hom f] [is_mul_hom g] :
is_mul_hom (λ (a : α), (f a) * g a)

A product of maps which preserve multiplication, preserves multiplication when the target is commutative.

@[instance]
theorem is_add_hom.add {α : Type u_1} {β : Type u_2} [add_semigroup α] [add_comm_semigroup β] (f g : α → β) [is_add_hom f] [is_add_hom g] :
is_add_hom (λ (a : α), f a + g a)

@[instance]
theorem is_mul_hom.inv {α : Type u_1} {β : Type u_2} [has_mul α] [comm_group β] (f : α → β) [is_mul_hom f] :
is_mul_hom (λ (a : α), (f a)⁻¹)

The inverse of a map which preserves multiplication, preserves multiplication when the target is commutative.

@[instance]
theorem is_add_hom.neg {α : Type u_1} {β : Type u_2} [has_add α] [add_comm_group β] (f : α → β) [is_add_hom f] :
is_add_hom (λ (a : α), -f a)

def monoid_hom.of {M : Type u_1} {N : Type u_2} [mM : monoid M] [mN : monoid N] (f : M → N) [h : is_monoid_hom f] :
M →* N

Interpret a map f : M → N as a homomorphism M →* N.

Equations
def add_monoid_hom.of {M : Type u_1} {N : Type u_2} [mM : add_monoid M] [mN : add_monoid N] (f : M → N) [h : is_add_monoid_hom f] :
M →+ N

Interpret a map f : M → N as a homomorphism M →+ N.

@[simp]
theorem monoid_hom.coe_of {M : Type u_1} {N : Type u_2} {mM : monoid M} {mN : monoid N} (f : M → N) [is_monoid_hom f] :

@[simp]
theorem add_monoid_hom.coe_of {M : Type u_1} {N : Type u_2} {mM : add_monoid M} {mN : add_monoid N} (f : M → N) [is_add_monoid_hom f] :

@[instance]
def add_monoid_hom.is_add_monoid_hom {M : Type u_1} {N : Type u_2} {mM : add_monoid M} {mN : add_monoid N} (f : M →+ N) :

@[instance]
def monoid_hom.is_monoid_hom {M : Type u_1} {N : Type u_2} {mM : monoid M} {mN : monoid N} (f : M →* N) :

theorem is_monoid_hom.map_mul {α : Type u} {β : Type v} [monoid α] [monoid β] (f : α → β) [is_monoid_hom f] (x y : α) :
f (x * y) = (f x) * f y

A monoid homomorphism preserves multiplication.

theorem is_add_monoid_hom.map_add {α : Type u} {β : Type v} [add_monoid α] [add_monoid β] (f : α → β) [is_add_monoid_hom f] (x y : α) :
f (x + y) = f x + f y

theorem is_add_monoid_hom.of_add {α : Type u} {β : Type v} [add_monoid α] [add_group β] (f : α → β) [is_add_hom f] :

theorem is_monoid_hom.of_mul {α : Type u} {β : Type v} [monoid α] [group β] (f : α → β) [is_mul_hom f] :

A map to a group preserving multiplication is a monoid homomorphism.

@[instance]
def is_monoid_hom.id {α : Type u} [monoid α] :

The identity map is a monoid homomorphism.

@[instance]

theorem is_add_monoid_hom.comp {α : Type u} {β : Type v} [add_monoid α] [add_monoid β] (f : α → β) [is_add_monoid_hom f] {γ : Type u_1} [add_monoid γ] (g : β → γ) [is_add_monoid_hom g] :

theorem is_monoid_hom.comp {α : Type u} {β : Type v} [monoid α] [monoid β] (f : α → β) [is_monoid_hom f] {γ : Type u_1} [monoid γ] (g : β → γ) [is_monoid_hom g] :

The composite of two monoid homomorphisms is a monoid homomorphism.

@[instance]
def is_add_monoid_hom.is_add_monoid_hom_mul_left {γ : Type u_1} [semiring γ] (x : γ) :
is_add_monoid_hom (λ (y : γ), x * y)

Left multiplication in a ring is an additive monoid morphism.

@[instance]
def is_add_monoid_hom.is_add_monoid_hom_mul_right {γ : Type u_1} [semiring γ] (x : γ) :
is_add_monoid_hom (λ (y : γ), y * x)

Right multiplication in a ring is an additive monoid morphism.

@[instance]
def add_monoid_hom.is_add_group_hom {G : Type u_1} {H : Type u_2} {_x : add_group G} {_x_1 : add_group H} (f : G →+ H) :

@[instance]
def monoid_hom.is_group_hom {G : Type u_1} {H : Type u_2} {_x : group G} {_x_1 : group H} (f : G →* H) :

theorem is_add_group_hom.mk' {α : Type u} {β : Type v} [add_group α] [add_group β] {f : α → β} :
(∀ (x y : α), f (x + y) = f x + f y)is_add_group_hom f

theorem is_group_hom.mk' {α : Type u} {β : Type v} [group α] [group β] {f : α → β} :
(∀ (x y : α), f (x * y) = (f x) * f y)is_group_hom f

Construct is_group_hom from its only hypothesis. The default constructor tries to get is_mul_hom from class instances, and this makes some proofs fail.

@[instance]
def is_add_group_hom.to_is_add_monoid_hom {α : Type u} {β : Type v} [add_group α] [add_group β] (f : α → β) [is_add_group_hom f] :

@[instance]
def is_group_hom.to_is_monoid_hom {α : Type u} {β : Type v} [group α] [group β] (f : α → β) [is_group_hom f] :

A group homomorphism is a monoid homomorphism.

theorem is_add_group_hom.map_zero {α : Type u} {β : Type v} [add_group α] [add_group β] (f : α → β) [is_add_group_hom f] :
f 0 = 0

theorem is_group_hom.map_one {α : Type u} {β : Type v} [group α] [group β] (f : α → β) [is_group_hom f] :
f 1 = 1

A group homomorphism sends 1 to 1.

theorem is_add_group_hom.map_neg {α : Type u} {β : Type v} [add_group α] [add_group β] (f : α → β) [is_add_group_hom f] (a : α) :
f (-a) = -f a

theorem is_group_hom.map_inv {α : Type u} {β : Type v} [group α] [group β] (f : α → β) [is_group_hom f] (a : α) :
f a⁻¹ = (f a)⁻¹

A group homomorphism sends inverses to inverses.

@[instance]
def is_group_hom.id {α : Type u} [group α] :

The identity is a group homomorphism.

@[instance]
def is_add_group_hom.id {α : Type u} [add_group α] :

theorem is_add_group_hom.comp {α : Type u} {β : Type v} [add_group α] [add_group β] (f : α → β) [is_add_group_hom f] {γ : Type u_1} [add_group γ] (g : β → γ) [is_add_group_hom g] :

theorem is_group_hom.comp {α : Type u} {β : Type v} [group α] [group β] (f : α → β) [is_group_hom f] {γ : Type u_1} [group γ] (g : β → γ) [is_group_hom g] :

The composition of two group homomomorphisms is a group homomorphism.

theorem is_group_hom.injective_iff {α : Type u} {β : Type v} [group α] [group β] (f : α → β) [is_group_hom f] :
function.injective f ∀ (a : α), f a = 1a = 1

A group homomorphism is injective iff its kernel is trivial.

theorem is_add_group_hom.injective_iff {α : Type u} {β : Type v} [add_group α] [add_group β] (f : α → β) [is_add_group_hom f] :
function.injective f ∀ (a : α), f a = 0a = 0

@[instance]
theorem is_group_hom.mul {α : Type u_1} {β : Type u_2} [group α] [comm_group β] (f g : α → β) [is_group_hom f] [is_group_hom g] :
is_group_hom (λ (a : α), (f a) * g a)

The product of group homomorphisms is a group homomorphism if the target is commutative.

@[instance]
theorem is_add_group_hom.add {α : Type u_1} {β : Type u_2} [add_group α] [add_comm_group β] (f g : α → β) [is_add_group_hom f] [is_add_group_hom g] :
is_add_group_hom (λ (a : α), f a + g a)

@[instance]
theorem is_add_group_hom.neg {α : Type u_1} {β : Type u_2} [add_group α] [add_comm_group β] (f : α → β) [is_add_group_hom f] :
is_add_group_hom (λ (a : α), -f a)

@[instance]
theorem is_group_hom.inv {α : Type u_1} {β : Type u_2} [group α] [comm_group β] (f : α → β) [is_group_hom f] :
is_group_hom (λ (a : α), (f a)⁻¹)

The inverse of a group homomorphism is a group homomorphism if the target is commutative.

These instances look redundant, because deprecated.ring provides is_ring_hom for a →+*. Nevertheless these are harmless, and helpful for stripping out dependencies on deprecated.ring.

@[instance]
def ring_hom.is_monoid_hom {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (f : R →+* S) :

@[instance]
def ring_hom.is_add_monoid_hom {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (f : R →+* S) :

@[instance]
def ring_hom.is_add_group_hom {R : Type u_1} {S : Type u_2} [ring R] [ring S] (f : R →+* S) :

@[instance]
theorem inv.is_group_hom {α : Type u} [comm_group α] :

Inversion is a group homomorphism if the group is commutative.

@[instance]

theorem is_add_group_hom.map_sub {α : Type u} {β : Type v} [add_group α] [add_group β] (f : α → β) [is_add_group_hom f] (a b : α) :
f (a - b) = f a - f b

Additive group homomorphisms commute with subtraction.

@[instance]
theorem is_add_group_hom.sub {α : Type u_1} {β : Type u_2} [add_group α] [add_comm_group β] (f g : α → β) [is_add_group_hom f] [is_add_group_hom g] :
is_add_group_hom (λ (a : α), f a - g a)

The difference of two additive group homomorphisms is an additive group homomorphism if the target is commutative.

def units.map' {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (f : M → N) [is_monoid_hom f] :

The group homomorphism on units induced by a multiplicative morphism.

Equations
@[simp]
theorem units.coe_map' {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (f : M → N) [is_monoid_hom f] (x : units M) :

@[instance]
def units.coe_is_monoid_hom {M : Type u_1} [monoid M] :

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_monoid_hom f] :
is_unit (f x)

theorem additive.is_add_hom {α : Type u} {β : Type v} [has_mul α] [has_mul β] (f : α → β) [is_mul_hom f] :

theorem multiplicative.is_mul_hom {α : Type u} {β : Type v} [has_add α] [has_add β] (f : α → β) [is_add_hom f] :

theorem additive.is_add_monoid_hom {α : Type u} {β : Type v} [monoid α] [monoid β] (f : α → β) [is_monoid_hom f] :

theorem multiplicative.is_monoid_hom {α : Type u} {β : Type v} [add_monoid α] [add_monoid β] (f : α → β) [is_add_monoid_hom f] :

theorem additive.is_add_group_hom {α : Type u} {β : Type v} [group α] [group β] (f : α → β) [is_group_hom f] :

theorem multiplicative.is_group_hom {α : Type u} {β : Type v} [add_group α] [add_group β] (f : α → β) [is_add_group_hom f] :