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 #

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,

Tags #

is_group_hom, is_monoid_hom, monoid_hom

@[class]
structure is_add_hom {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] (f : α → β) :
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 β] (f : α → β) :
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)

Throughout this section, some mul_one_class arguments are specified with {} instead of []. See note [implicit instance arguments].

def monoid_hom.of {M : Type u_1} {N : Type u_2} [mM : mul_one_class M] [mN : mul_one_class 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_zero_class M] [mN : add_zero_class 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 : mul_one_class M} {mN : mul_one_class 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_zero_class M} {mN : add_zero_class 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_zero_class M} {mN : add_zero_class N} (f : M →+ N) :
@[instance]
def monoid_hom.is_monoid_hom {M : Type u_1} {N : Type u_2} {mM : mul_one_class M} {mN : mul_one_class N} (f : M →* N) :
@[instance]
def mul_equiv.is_mul_hom {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (h : M ≃* N) :

A multiplicative isomorphism preserves multiplication (deprecated).

@[instance]
def add_equiv.is_add_hom {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (h : M ≃+ N) :
@[instance]
def add_equiv.is_add_monoid_hom {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (h : M ≃+ N) :
@[instance]
def mul_equiv.is_monoid_hom {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (h : M ≃* N) :

A multiplicative bijection between two monoids is a monoid hom (deprecated -- use mul_equiv.to_monoid_hom).

theorem is_monoid_hom.map_mul {α : Type u} {β : Type v} [mul_one_class α] [mul_one_class β] (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_zero_class α] [add_zero_class β] (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_zero_class α] [add_group β] (f : α → β) [is_add_hom f] :
theorem is_monoid_hom.of_mul {α : Type u} {β : Type v} [mul_one_class α] [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} [mul_one_class α] :

The identity map is a monoid homomorphism.

@[instance]
theorem is_add_monoid_hom.comp {α : Type u} {β : Type v} [add_zero_class α] [add_zero_class β] (f : α → β) [is_add_monoid_hom f] {γ : Type u_1} [add_zero_class γ] (g : β → γ) [is_add_monoid_hom g] :
theorem is_monoid_hom.comp {α : Type u} {β : Type v} [mul_one_class α] [mul_one_class β] (f : α → β) [is_monoid_hom f] {γ : Type u_1} [mul_one_class γ] (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} [non_unital_non_assoc_semiring γ] (x : γ) :
is_add_monoid_hom (λ (y : γ), x * y)

Left multiplication in a ring is an additive monoid morphism.

@[instance]

Right multiplication in a ring is an additive monoid morphism.

@[class]
structure is_group_hom {α : Type u} {β : Type v} [group α] [group β] (f : α → β) :
Prop

Predicate for group homomorphisms (deprecated -- use bundled monoid_hom).

Instances
@[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) :
@[instance]
def add_equiv.is_add_group_hom {G : Type u_1} {H : Type u_2} {_x : add_group G} {_x_1 : add_group H} (h : G ≃+ H) :
@[instance]
def mul_equiv.is_group_hom {G : Type u_1} {H : Type u_2} {_x : group G} {_x_1 : group H} (h : G ≃* H) :
theorem is_add_group_hom.mk' {α : Type u} {β : Type v} [add_group α] [add_group β] {f : α → β} (hf : ∀ (x y : α), f (x + y) = f x + f y) :
theorem is_group_hom.mk' {α : Type u} {β : Type v} [group α] [group β] {f : α → β} (hf : ∀ (x y : α), f (x * y) = (f x) * f y) :

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 homomorphisms 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} [non_assoc_semiring R] [non_assoc_semiring S] (f : R →+* S) :
@[instance]
def ring_hom.is_add_monoid_hom {R : Type u_1} {S : Type u_2} [non_assoc_semiring R] [non_assoc_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]

Negation is an add_group homomorphism if the add_group is commutative.

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} [mul_one_class α] [mul_one_class β] (f : α → β) [is_monoid_hom f] :
theorem multiplicative.is_monoid_hom {α : Type u} {β : Type v} [add_zero_class α] [add_zero_class β] (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] :