mathlib documentation

deprecated.group

Unbundled monoid and group homomorphisms #

This file defines predicates for unbundled monoid and group homomorphisms. Though bundled morphisms are preferred in mathlib, these unbundled predicates are still occasionally 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)

Tags #

is_group_hom, is_monoid_hom

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

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

source
theorem is_add_hom.id {α : Type u} [has_add α] :
is_add_hom id

The identity map preserves addition

source
theorem is_mul_hom.id {α : Type u} [has_mul α] :
is_mul_hom id

The identity map preserves multiplication.

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

The composition of addition preserving maps also preserves addition

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

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

source
theorem is_mul_hom.mul {α : Type u_1} {β : Type u_2} [semigroup α] [comm_semigroup β] {f g : α → β} (hf : is_mul_hom f) (hg : 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.

source
theorem is_add_hom.add {α : Type u_1} {β : Type u_2} [add_semigroup α] [add_comm_semigroup β] {f g : α → β} (hf : is_add_hom f) (hg : is_add_hom g) :
is_add_hom (λ (a : α), f a + g a)
source
theorem is_mul_hom.inv {α : Type u_1} {β : Type u_2} [has_mul α] [comm_group β] {f : α → β} (hf : 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.

source
theorem is_add_hom.neg {α : Type u_1} {β : Type u_2} [has_add α] [add_comm_group β] {f : α → β} (hf : is_add_hom f) :
is_add_hom (λ (a : α), -f a)
source
structure is_add_monoid_hom {α : Type u} {β : Type v} [add_zero_class α] [add_zero_class β] (f : α → β) :
Prop

Predicate for add_monoid homomorphisms (deprecated -- use the bundled monoid_hom version).

source
structure is_monoid_hom {α : Type u} {β : Type v} [mul_one_class α] [mul_one_class β] (f : α → β) :
Prop

Predicate for monoid homomorphisms (deprecated -- use the bundled monoid_hom version).

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

Equations
source
@[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} (hf : is_monoid_hom f) :
⇑(monoid_hom.of hf) = f
source
@[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} (hf : is_add_monoid_hom f) :
⇑(add_monoid_hom.of hf) = f
source
theorem add_monoid_hom.is_add_monoid_hom_coe {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
source
theorem monoid_hom.is_monoid_hom_coe {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
source
theorem mul_equiv.is_mul_hom {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (h : M ≃* N) :
is_mul_hom ⇑h

A multiplicative isomorphism preserves multiplication (deprecated).

source
theorem add_equiv.is_add_hom {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (h : M ≃+ N) :
is_add_hom ⇑h
source
theorem 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) :
is_add_monoid_hom ⇑h
source
theorem mul_equiv.is_monoid_hom {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (h : M ≃* N) :
is_monoid_hom ⇑h

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

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

A monoid homomorphism preserves multiplication.

source
theorem is_add_monoid_hom.map_add {α : Type u} {β : Type v} [add_zero_class α] [add_zero_class β] {f : α → β} (hf : is_add_monoid_hom f) (x y : α) :
f (x + y) = f x + f y
source
theorem is_monoid_hom.inv {α : Type u_1} {β : Type u_2} [mul_one_class α] [comm_group β] {f : α → β} (hf : is_monoid_hom f) :
is_monoid_hom (λ (a : α), (f a)⁻¹)

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

source
theorem is_add_monoid_hom.neg {α : Type u_1} {β : Type u_2} [add_zero_class α] [add_comm_group β] {f : α → β} (hf : is_add_monoid_hom f) :
is_add_monoid_hom (λ (a : α), -f a)
source
theorem is_mul_hom.to_is_monoid_hom {α : Type u} {β : Type v} [mul_one_class α] [group β] {f : α → β} (hf : is_mul_hom f) :
is_monoid_hom f

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

source
theorem is_add_hom.to_is_add_monoid_hom {α : Type u} {β : Type v} [add_zero_class α] [add_group β] {f : α → β} (hf : is_add_hom f) :
is_add_monoid_hom f
source
theorem is_monoid_hom.id {α : Type u} [mul_one_class α] :
is_monoid_hom id

The identity map is a monoid homomorphism.

source
theorem is_add_monoid_hom.id {α : Type u} [add_zero_class α] :
is_add_monoid_hom id
source
theorem is_add_monoid_hom.comp {α : Type u} {β : Type v} [add_zero_class α] [add_zero_class β] {f : α → β} (hf : is_add_monoid_hom f) {γ : Type u_1} [add_zero_class γ] {g : β → γ} (hg : is_add_monoid_hom g) :
is_add_monoid_hom (g ∘ f)
source
theorem is_monoid_hom.comp {α : Type u} {β : Type v} [mul_one_class α] [mul_one_class β] {f : α → β} (hf : is_monoid_hom f) {γ : Type u_1} [mul_one_class γ] {g : β → γ} (hg : is_monoid_hom g) :
is_monoid_hom (g ∘ f)

The composite of two monoid homomorphisms is a monoid homomorphism.

source
theorem 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.

source
theorem is_add_monoid_hom.is_add_monoid_hom_mul_right {γ : Type u_1} [non_unital_non_assoc_semiring γ] (x : γ) :
is_add_monoid_hom (λ (y : γ), y * x)

Right multiplication in a ring is an additive monoid morphism.

source
structure is_add_group_hom {α : Type u} {β : Type v} [add_group α] [add_group β] (f : α → β) :
Prop

Predicate for additive group homomorphism (deprecated -- use bundled monoid_hom).

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

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

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

Construct is_group_hom from its only hypothesis.

source
theorem is_group_hom.map_mul {α : Type u} {β : Type v} [group α] [group β] {f : α → β} (hf : is_group_hom f) (x y : α) :
f (x * y) = (f x) * f y
source
theorem is_add_group_hom.to_is_add_monoid_hom {α : Type u} {β : Type v} [add_group α] [add_group β] {f : α → β} (hf : is_add_group_hom f) :
is_add_monoid_hom f
source
theorem is_group_hom.to_is_monoid_hom {α : Type u} {β : Type v} [group α] [group β] {f : α → β} (hf : is_group_hom f) :
is_monoid_hom f

A group homomorphism is a monoid homomorphism.

source
theorem is_add_group_hom.map_zero {α : Type u} {β : Type v} [add_group α] [add_group β] {f : α → β} (hf : is_add_group_hom f) :
f 0 = 0
source
theorem is_group_hom.map_one {α : Type u} {β : Type v} [group α] [group β] {f : α → β} (hf : is_group_hom f) :
f 1 = 1

A group homomorphism sends 1 to 1.

source
theorem is_add_group_hom.map_neg {α : Type u} {β : Type v} [add_group α] [add_group β] {f : α → β} (hf : is_add_group_hom f) (a : α) :
f (-a) = -f a
source
theorem is_group_hom.map_inv {α : Type u} {β : Type v} [group α] [group β] {f : α → β} (hf : is_group_hom f) (a : α) :
f a⁻¹ = (f a)⁻¹

A group homomorphism sends inverses to inverses.

source
theorem is_group_hom.id {α : Type u} [group α] :
is_group_hom id

The identity is a group homomorphism.

source
theorem is_add_group_hom.id {α : Type u} [add_group α] :
is_add_group_hom id
source
theorem is_add_group_hom.comp {α : Type u} {β : Type v} [add_group α] [add_group β] {f : α → β} (hf : is_add_group_hom f) {γ : Type u_1} [add_group γ] {g : β → γ} (hg : is_add_group_hom g) :
is_add_group_hom (g ∘ f)
source
theorem is_group_hom.comp {α : Type u} {β : Type v} [group α] [group β] {f : α → β} (hf : is_group_hom f) {γ : Type u_1} [group γ] {g : β → γ} (hg : is_group_hom g) :
is_group_hom (g ∘ f)

The composition of two group homomorphisms is a group homomorphism.

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

A group homomorphism is injective iff its kernel is trivial.

source
theorem is_add_group_hom.injective_iff {α : Type u} {β : Type v} [add_group α] [add_group β] {f : α → β} (hf : is_add_group_hom f) :
function.injective f ↔ ∀ (a : α), f a = 0 → a = 0
source
theorem is_group_hom.mul {α : Type u_1} {β : Type u_2} [group α] [comm_group β] {f g : α → β} (hf : is_group_hom f) (hg : 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.

source
theorem is_add_group_hom.add {α : Type u_1} {β : Type u_2} [add_group α] [add_comm_group β] {f g : α → β} (hf : is_add_group_hom f) (hg : is_add_group_hom g) :
is_add_group_hom (λ (a : α), f a + g a)
source
theorem is_add_group_hom.neg {α : Type u_1} {β : Type u_2} [add_group α] [add_comm_group β] {f : α → β} (hf : is_add_group_hom f) :
is_add_group_hom (λ (a : α), -f a)
source
theorem is_group_hom.inv {α : Type u_1} {β : Type u_2} [group α] [comm_group β] {f : α → β} (hf : 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.

source
theorem ring_hom.to_is_monoid_hom {R : Type u_1} {S : Type u_2} [non_assoc_semiring R] [non_assoc_semiring S] (f : R →+* S) :
is_monoid_hom ⇑f
source
theorem ring_hom.to_is_add_monoid_hom {R : Type u_1} {S : Type u_2} [non_assoc_semiring R] [non_assoc_semiring S] (f : R →+* S) :
is_add_monoid_hom ⇑f
source
theorem ring_hom.to_is_add_group_hom {R : Type u_1} {S : Type u_2} [ring R] [ring S] (f : R →+* S) :
is_add_group_hom ⇑f
source
theorem inv.is_group_hom {α : Type u} [comm_group α] :
is_group_hom has_inv.inv

Inversion is a group homomorphism if the group is commutative.

source
theorem neg.is_add_group_hom {α : Type u} [add_comm_group α] :
is_add_group_hom has_neg.neg

Negation is an add_group homomorphism if the add_group is commutative.

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

Additive group homomorphisms commute with subtraction.

source
theorem is_add_group_hom.sub {α : Type u_1} {β : Type u_2} [add_group α] [add_comm_group β] {f g : α → β} (hf : is_add_group_hom f) (hg : 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.

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

The group homomorphism on units induced by a multiplicative morphism.

Equations
source
@[simp]
theorem units.coe_map' {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] {f : M → N} (hf : is_monoid_hom f) (x : Mˣ) :
↑(⇑(units.map' hf) x) = f ↑x
source
theorem units.coe_is_monoid_hom {M : Type u_1} [monoid M] :
is_monoid_hom coe
source
theorem is_unit.map' {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] {f : M → N} (hf : is_monoid_hom f) {x : M} (h : is_unit x) :
is_unit (f x)
source
theorem additive.is_add_hom {α : Type u} {β : Type v} [has_mul α] [has_mul β] {f : α → β} (hf : is_mul_hom f) :
is_add_hom f
source
theorem multiplicative.is_mul_hom {α : Type u} {β : Type v} [has_add α] [has_add β] {f : α → β} (hf : is_add_hom f) :
is_mul_hom f
source
theorem additive.is_add_monoid_hom {α : Type u} {β : Type v} [mul_one_class α] [mul_one_class β] {f : α → β} (hf : is_monoid_hom f) :
is_add_monoid_hom f
source
theorem multiplicative.is_monoid_hom {α : Type u} {β : Type v} [add_zero_class α] [add_zero_class β] {f : α → β} (hf : is_add_monoid_hom f) :
is_monoid_hom f
source
theorem additive.is_add_group_hom {α : Type u} {β : Type v} [group α] [group β] {f : α → β} (hf : is_group_hom f) :
is_add_group_hom f
source
theorem multiplicative.is_group_hom {α : Type u} {β : Type v} [add_group α] [add_group β] {f : α → β} (hf : is_add_group_hom f) :
is_group_hom f