mathlib3 documentation

deprecated.group

Unbundled monoid and group homomorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file is deprecated, and is no longer imported by anything in mathlib other than other deprecated files, and test files. You should not need to import it.

This file defines predicates for unbundled monoid and group homomorphisms. Instead of using this file, please use monoid_hom, defined in algebra.hom.group, with notation →*, for morphisms between monoids or groups. For example use φ : G →* H to represent a group homomorphism between multiplicative groups, and ψ : A →+ B to represent a group homomorphism between additive groups.

Main Definitions #

is_monoid_hom (deprecated), is_group_hom (deprecated)

Tags #

is_group_hom, is_monoid_hom

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.

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.

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

The identity map preserves addition

theorem 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 : β → γ} (hf : is_add_hom f) (hg : is_add_hom g) :

is_add_hom (g ∘ f)

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 : β → γ} (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.

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.

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)

A sum of maps which preserves addition, preserves addition when the target is commutative.

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.

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)

The negation of a map which preserves addition, preserves addition when the target is commutative.

structure is_add_monoid_hom {α : Type u} {β : Type v} [add_zero_class α] [add_zero_class β] (f : α → β) :

Prop

to_is_add_hom : is_add_hom f
map_zero : f 0 = 0

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

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

Prop

to_is_mul_hom : is_mul_hom f
map_one : f 1 = 1

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

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

monoid_hom.of h = {to_fun := f, map_one' := _, map_mul' := _}

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

add_monoid_hom.of h = {to_fun := f, map_zero' := _, map_add' := _}

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

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

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

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

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

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

An additive isomorphism preserves addition (deprecated).

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

An additive bijection between two additive monoids is an additive monoid hom (deprecated).

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

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.

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

An additive monoid homomorphism preserves addition.

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.

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)

The negation of a map which preserves addition, preserves addition when the target is commutative.

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.

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

A map to an additive group preserving addition is an additive monoid homomorphism.

theorem is_monoid_hom.id {α : Type u} [mul_one_class α] :

is_monoid_hom id

The identity map is a monoid homomorphism.

theorem is_add_monoid_hom.id {α : Type u} [add_zero_class α] :

is_add_monoid_hom id

The identity map is an additive monoid homomorphism.

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)

The composite of two additive monoid homomorphisms is an additive monoid homomorphism.

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.

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.

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.

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

Prop

to_is_add_hom : is_add_hom f

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

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

Prop

to_is_mul_hom : is_mul_hom f

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

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

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

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

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

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

Construct is_add_group_hom from its only hypothesis.

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.

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

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

An additive group homomorphism is an additive monoid homomorphism.

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.

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

An additive group homomorphism sends 0 to 0.

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.

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

An additive group homomorphism sends negations to negations.

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.

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

theorem is_group_hom.map_div {α : Type u} {β : Type v} [group α] [group β] {f : α → β} (hf : is_group_hom f) (a b : α) :

f (a / b) = f a / f b

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

is_group_hom id

The identity is a group homomorphism.

theorem is_add_group_hom.id {α : Type u} [add_group α] :

is_add_group_hom id

The identity is an additive group homomorphism.

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)

The composition of two additive group homomorphisms is an additive group homomorphism.

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.

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.

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

An additive group homomorphism is injective if its kernel is trivial.

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.

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)

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

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)

The negation of an additive group homomorphism is an additive group homomorphism if the target is commutative.

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.

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

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

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

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.

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.

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.

@[reducible]

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

The group homomorphism on units induced by a multiplicative morphism.

Equations

units.map' hf = units.map (monoid_hom.of hf)

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

theorem units.coe_is_monoid_hom {M : Type u_1} [monoid M] :

is_monoid_hom coe

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

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

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

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

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

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

is_add_group_hom f

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