# mathlibdocumentation

algebra.group.inj_surj

# Lifting algebraic data classes along injective/surjective maps

This file provides definitions that are meant to deal with situations such as the following:

Suppose that G is a group, and H is a type endowed with has_one H, has_mul H, and has_inv H. Suppose furthermore, that f : G → H is a surjective map that respects the multiplication, and the unit elements. Then H satisfies the group axioms.

The relevant definition in this case is function.surjective.group. Dually, there is also function.injective.group. And there are versions for (additive) (commutative) semigroups/monoids.

### Injective

def function.injective.semigroup {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [semigroup M₂] (f : M₁ → M₂) :
(∀ (x y : M₁), f (x * y) = (f x) * f y)

A type endowed with * is a semigroup, if it admits an injective map that preserves * to a semigroup.

Equations
def function.injective.add_semigroup {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] [add_semigroup M₂] (f : M₁ → M₂) :
(∀ (x y : M₁), f (x + y) = f x + f y)

A type endowed with + is an additive semigroup, if it admits an injective map that preserves + to an additive semigroup.

def function.injective.add_comm_semigroup {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] (f : M₁ → M₂) :
(∀ (x y : M₁), f (x + y) = f x + f y)

A type endowed with + is an additive commutative semigroup, if it admits an injective map that preserves + to an additive commutative semigroup.

def function.injective.comm_semigroup {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [comm_semigroup M₂] (f : M₁ → M₂) :
(∀ (x y : M₁), f (x * y) = (f x) * f y)

A type endowed with * is a commutative semigroup, if it admits an injective map that preserves * to a commutative semigroup.

Equations
def function.injective.left_cancel_semigroup {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] (f : M₁ → M₂) :
(∀ (x y : M₁), f (x * y) = (f x) * f y)

A type endowed with * is a left cancel semigroup, if it admits an injective map that preserves * to a left cancel semigroup.

Equations
def function.injective.add_left_cancel_semigroup {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] (f : M₁ → M₂) :
(∀ (x y : M₁), f (x + y) = f x + f y)

A type endowed with + is an additive left cancel semigroup, if it admits an injective map that preserves + to an additive left cancel semigroup.

def function.injective.right_cancel_semigroup {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] (f : M₁ → M₂) :
(∀ (x y : M₁), f (x * y) = (f x) * f y)

A type endowed with * is a right cancel semigroup, if it admits an injective map that preserves * to a right cancel semigroup.

Equations
def function.injective.add_right_cancel_semigroup {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] (f : M₁ → M₂) :
(∀ (x y : M₁), f (x + y) = f x + f y)

A type endowed with + is an additive right cancel semigroup, if it admits an injective map that preserves + to an additive right cancel semigroup.

def function.injective.add_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] [has_zero M₁] [add_monoid M₂] (f : M₁ → M₂) :
f 0 = 0(∀ (x y : M₁), f (x + y) = f x + f y)

A type endowed with 0 and + is an additive monoid, if it admits an injective map that preserves 0 and + to an additive monoid.

def function.injective.monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [has_one M₁] [monoid M₂] (f : M₁ → M₂) :
f 1 = 1(∀ (x y : M₁), f (x * y) = (f x) * f y)monoid M₁

A type endowed with 1 and * is a monoid, if it admits an injective map that preserves 1 and * to a monoid.

Equations
def function.injective.left_cancel_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [has_one M₁] (f : M₁ → M₂) :
f 1 = 1(∀ (x y : M₁), f (x * y) = (f x) * f y)

A type endowed with 1 and * is a left cancel monoid, if it admits an injective map that preserves 1 and * to a left cancel monoid.

Equations
def function.injective.add_left_cancel_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] [has_zero M₁] (f : M₁ → M₂) :
f 0 = 0(∀ (x y : M₁), f (x + y) = f x + f y)

A type endowed with 0 and + is an additive left cancel monoid, if it admits an injective map that preserves 0 and + to an additive left cancel monoid.

def function.injective.add_comm_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] [has_zero M₁] [add_comm_monoid M₂] (f : M₁ → M₂) :
f 0 = 0(∀ (x y : M₁), f (x + y) = f x + f y)

A type endowed with 0 and + is an additive commutative monoid, if it admits an injective map that preserves 0 and + to an additive commutative monoid.

def function.injective.comm_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [has_one M₁] [comm_monoid M₂] (f : M₁ → M₂) :
f 1 = 1(∀ (x y : M₁), f (x * y) = (f x) * f y)

A type endowed with 1 and * is a commutative monoid, if it admits an injective map that preserves 1 and * to a commutative monoid.

Equations
def function.injective.group {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [has_one M₁] [has_inv M₁] [group M₂] (f : M₁ → M₂) :
f 1 = 1(∀ (x y : M₁), f (x * y) = (f x) * f y)(∀ (x : M₁), f x⁻¹ = (f x)⁻¹)group M₁

A type endowed with 1, * and ⁻¹ is a group, if it admits an injective map that preserves 1, * and ⁻¹ to a group.

Equations
def function.injective.add_group {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] [has_zero M₁] [has_neg M₁] [add_group M₂] (f : M₁ → M₂) :
f 0 = 0(∀ (x y : M₁), f (x + y) = f x + f y)(∀ (x : M₁), f (-x) = -f x)

A type endowed with 0 and + is an additive group, if it admits an injective map that preserves 0 and + to an additive group.

def function.injective.comm_group {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [has_one M₁] [has_inv M₁] [comm_group M₂] (f : M₁ → M₂) :
f 1 = 1(∀ (x y : M₁), f (x * y) = (f x) * f y)(∀ (x : M₁), f x⁻¹ = (f x)⁻¹)

A type endowed with 1, * and ⁻¹ is a commutative group, if it admits an injective map that preserves 1, * and ⁻¹ to a commutative group.

Equations
def function.injective.add_comm_group {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] [has_zero M₁] [has_neg M₁] [add_comm_group M₂] (f : M₁ → M₂) :
f 0 = 0(∀ (x y : M₁), f (x + y) = f x + f y)(∀ (x : M₁), f (-x) = -f x)

A type endowed with 0 and + is an additive commutative group, if it admits an injective map that preserves 0 and + to an additive commutative group.

### Surjective

def function.surjective.add_semigroup {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₂] [add_semigroup M₁] (f : M₁ → M₂) :
(∀ (x y : M₁), f (x + y) = f x + f y)

A type endowed with + is an additive semigroup, if it admits a surjective map that preserves + from an additive semigroup.

def function.surjective.semigroup {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₂] [semigroup M₁] (f : M₁ → M₂) :
(∀ (x y : M₁), f (x * y) = (f x) * f y)

A type endowed with * is a semigroup, if it admits a surjective map that preserves * from a semigroup.

Equations
def function.surjective.comm_semigroup {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₂] [comm_semigroup M₁] (f : M₁ → M₂) :
(∀ (x y : M₁), f (x * y) = (f x) * f y)

A type endowed with * is a commutative semigroup, if it admits a surjective map that preserves * from a commutative semigroup.

Equations
def function.surjective.add_comm_semigroup {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₂] (f : M₁ → M₂) :
(∀ (x y : M₁), f (x + y) = f x + f y)

A type endowed with + is an additive commutative semigroup, if it admits a surjective map that preserves + from an additive commutative semigroup.

def function.surjective.monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₂] [has_one M₂] [monoid M₁] (f : M₁ → M₂) :
f 1 = 1(∀ (x y : M₁), f (x * y) = (f x) * f y)monoid M₂

A type endowed with 1 and * is a monoid, if it admits a surjective map that preserves 1 and * from a monoid.

Equations
def function.surjective.add_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₂] [has_zero M₂] [add_monoid M₁] (f : M₁ → M₂) :
f 0 = 0(∀ (x y : M₁), f (x + y) = f x + f y)

A type endowed with 0 and + is an additive monoid, if it admits a surjective map that preserves 0 and + to an additive monoid.

def function.surjective.add_comm_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₂] [has_zero M₂] [add_comm_monoid M₁] (f : M₁ → M₂) :
f 0 = 0(∀ (x y : M₁), f (x + y) = f x + f y)

A type endowed with 0 and + is an additive commutative monoid, if it admits a surjective map that preserves 0 and + to an additive commutative monoid.

def function.surjective.comm_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₂] [has_one M₂] [comm_monoid M₁] (f : M₁ → M₂) :
f 1 = 1(∀ (x y : M₁), f (x * y) = (f x) * f y)

A type endowed with 1 and * is a commutative monoid, if it admits a surjective map that preserves 1 and * from a commutative monoid.

Equations
def function.surjective.group {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₂] [has_one M₂] [has_inv M₂] [group M₁] (f : M₁ → M₂) :
f 1 = 1(∀ (x y : M₁), f (x * y) = (f x) * f y)(∀ (x : M₁), f x⁻¹ = (f x)⁻¹)group M₂

A type endowed with 1, * and ⁻¹ is a group, if it admits a surjective map that preserves 1, * and ⁻¹ from a group.

Equations
def function.surjective.add_group {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₂] [has_zero M₂] [has_neg M₂] [add_group M₁] (f : M₁ → M₂) :
f 0 = 0(∀ (x y : M₁), f (x + y) = f x + f y)(∀ (x : M₁), f (-x) = -f x)

A type endowed with 0 and + is an additive group, if it admits a surjective map that preserves 0 and + to an additive group.

def function.surjective.comm_group {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₂] [has_one M₂] [has_inv M₂] [comm_group M₁] (f : M₁ → M₂) :
f 1 = 1(∀ (x y : M₁), f (x * y) = (f x) * f y)(∀ (x : M₁), f x⁻¹ = (f x)⁻¹)

A type endowed with 1, * and ⁻¹ is a commutative group, if it admits a surjective map that preserves 1, * and ⁻¹ from a commutative group.

Equations
def function.surjective.add_comm_group {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₂] [has_zero M₂] [has_neg M₂] [add_comm_group M₁] (f : M₁ → M₂) :
f 0 = 0(∀ (x y : M₁), f (x + y) = f x + f y)(∀ (x : M₁), f (-x) = -f x)

A type endowed with 0 and + is an additive commutative group, if it admits a surjective map that preserves 0 and + to an additive commutative group.