# mathlibdocumentation

algebra.ring.inj_surj

# Pulling back rings along injective maps, and pushing them forward along surjective maps. #

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

### distrib class #

@[protected, reducible]
def function.injective.distrib {R : Type x} {S : Type u_1} [has_mul R] [has_add R] [distrib S] (f : R S) (hf : function.injective f) (add : (x y : R), f (x + y) = f x + f y) (mul : (x y : R), f (x * y) = f x * f y) :

Pullback a distrib instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.distrib {R : Type x} {S : Type u_1} [distrib R] [has_add S] [has_mul S] (f : R S) (hf : function.surjective f) (add : (x y : R), f (x + y) = f x + f y) (mul : (x y : R), f (x * y) = f x * f y) :

Pushforward a distrib instance along a surjective function. See note [reducible non-instances].

Equations

### Semirings #

@[protected, reducible]
def function.injective.non_unital_non_assoc_semiring {β : Type v} [has_zero β] [has_add β] [has_mul β] [ β] {α : Type u} (f : β α) (hf : function.injective f) (zero : f 0 = 0) (add : (x y : β), f (x + y) = f x + f y) (mul : (x y : β), f (x * y) = f x * f y) (nsmul : (x : β) (n : ), f (n x) = n f x) :

Pullback a non_unital_non_assoc_semiring instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.injective.non_unital_semiring {β : Type v} [has_zero β] [has_add β] [has_mul β] [ β] {α : Type u} (f : β α) (hf : function.injective f) (zero : f 0 = 0) (add : (x y : β), f (x + y) = f x + f y) (mul : (x y : β), f (x * y) = f x * f y) (nsmul : (x : β) (n : ), f (n x) = n f x) :

Pullback a non_unital_semiring instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.injective.non_assoc_semiring {α : Type u} {β : Type v} [has_zero β] [has_one β] [has_mul β] [has_add β] [ β] [has_nat_cast β] (f : β α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : β), f (x + y) = f x + f y) (mul : (x y : β), f (x * y) = f x * f y) (nsmul : (x : β) (n : ), f (n x) = n f x) (nat_cast : (n : ), f n = n) :

Pullback a non_assoc_semiring instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.injective.semiring {α : Type u} [semiring α] {β : Type v} [has_zero β] [has_one β] [has_add β] [has_mul β] [ ] [ β] [has_nat_cast β] (f : β α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : β), f (x + y) = f x + f y) (mul : (x y : β), f (x * y) = f x * f y) (nsmul : (x : β) (n : ), f (n x) = n f x) (npow : (x : β) (n : ), f (x ^ n) = f x ^ n) (nat_cast : (n : ), f n = n) :

Pullback a semiring instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.non_unital_non_assoc_semiring {β : Type v} [has_zero β] [has_add β] [has_mul β] [ β] {α : Type u} (f : α β) (hf : function.surjective f) (zero : f 0 = 0) (add : (x y : α), f (x + y) = f x + f y) (mul : (x y : α), f (x * y) = f x * f y) (nsmul : (x : α) (n : ), f (n x) = n f x) :

Pushforward a non_unital_non_assoc_semiring instance along a surjective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.non_unital_semiring {β : Type v} [has_zero β] [has_add β] [has_mul β] [ β] {α : Type u} (f : α β) (hf : function.surjective f) (zero : f 0 = 0) (add : (x y : α), f (x + y) = f x + f y) (mul : (x y : α), f (x * y) = f x * f y) (nsmul : (x : α) (n : ), f (n x) = n f x) :

Pushforward a non_unital_semiring instance along a surjective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.non_assoc_semiring {α : Type u} {β : Type v} [has_zero β] [has_one β] [has_add β] [has_mul β] [ β] [has_nat_cast β] (f : α β) (hf : function.surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : α), f (x + y) = f x + f y) (mul : (x y : α), f (x * y) = f x * f y) (nsmul : (x : α) (n : ), f (n x) = n f x) (nat_cast : (n : ), f n = n) :

Pushforward a non_assoc_semiring instance along a surjective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.semiring {α : Type u} [semiring α] {β : Type v} [has_zero β] [has_one β] [has_add β] [has_mul β] [ ] [ β] [has_nat_cast β] (f : α β) (hf : function.surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : α), f (x + y) = f x + f y) (mul : (x y : α), f (x * y) = f x * f y) (nsmul : (x : α) (n : ), f (n x) = n f x) (npow : (x : α) (n : ), f (x ^ n) = f x ^ n) (nat_cast : (n : ), f n = n) :

Pushforward a semiring instance along a surjective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.injective.non_unital_comm_semiring {α : Type u} {γ : Type w} [has_zero γ] [has_add γ] [has_mul γ] [ γ] (f : γ α) (hf : function.injective f) (zero : f 0 = 0) (add : (x y : γ), f (x + y) = f x + f y) (mul : (x y : γ), f (x * y) = f x * f y) (nsmul : (x : γ) (n : ), f (n x) = n f x) :

Pullback a non_unital_semiring instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.non_unital_comm_semiring {α : Type u} {γ : Type w} [has_zero γ] [has_add γ] [has_mul γ] [ γ] (f : α γ) (hf : function.surjective f) (zero : f 0 = 0) (add : (x y : α), f (x + y) = f x + f y) (mul : (x y : α), f (x * y) = f x * f y) (nsmul : (x : α) (n : ), f (n x) = n f x) :

Pushforward a non_unital_semiring instance along a surjective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.injective.comm_semiring {α : Type u} {γ : Type w} [has_zero γ] [has_one γ] [has_add γ] [has_mul γ] [ γ] [has_nat_cast γ] [ ] (f : γ α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : γ), f (x + y) = f x + f y) (mul : (x y : γ), f (x * y) = f x * f y) (nsmul : (x : γ) (n : ), f (n x) = n f x) (npow : (x : γ) (n : ), f (x ^ n) = f x ^ n) (nat_cast : (n : ), f n = n) :

Pullback a semiring instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.comm_semiring {α : Type u} {γ : Type w} [has_zero γ] [has_one γ] [has_add γ] [has_mul γ] [ γ] [has_nat_cast γ] [ ] (f : α γ) (hf : function.surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : α), f (x + y) = f x + f y) (mul : (x y : α), f (x * y) = f x * f y) (nsmul : (x : α) (n : ), f (n x) = n f x) (npow : (x : α) (n : ), f (x ^ n) = f x ^ n) (nat_cast : (n : ), f n = n) :

Pushforward a semiring instance along a surjective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.injective.has_distrib_neg {α : Type u} {β : Type v} [has_mul α] [has_neg β] [has_mul β] (f : β α) (hf : function.injective f) (neg : (a : β), f (-a) = -f a) (mul : (a b : β), f (a * b) = f a * f b) :

A type endowed with - and * has distributive negation, if it admits an injective map that preserves - and * to a type which has distributive negation.

Equations
@[protected, reducible]
def function.surjective.has_distrib_neg {α : Type u} {β : Type v} [has_mul α] [has_neg β] [has_mul β] (f : α β) (hf : function.surjective f) (neg : (a : α), f (-a) = -f a) (mul : (a b : α), f (a * b) = f a * f b) :

A type endowed with - and * has distributive negation, if it admits a surjective map that preserves - and * from a type which has distributive negation.

Equations
@[protected, instance]
def add_opposite.has_distrib_neg {α : Type u} [has_mul α]  :
Equations

### Rings #

@[protected, reducible]
def function.injective.non_unital_non_assoc_ring {α : Type u} {β : Type v} [has_zero β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ β] [ β] (f : β α) (hf : function.injective f) (zero : f 0 = 0) (add : (x y : β), f (x + y) = f x + f y) (mul : (x y : β), f (x * y) = f x * f y) (neg : (x : β), f (-x) = -f x) (sub : (x y : β), f (x - y) = f x - f y) (nsmul : (x : β) (n : ), f (n x) = n f x) (zsmul : (x : β) (n : ), f (n x) = n f x) :

Pullback a non_unital_non_assoc_ring instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.non_unital_non_assoc_ring {α : Type u} {β : Type v} [has_zero β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ β] [ β] (f : α β) (hf : function.surjective f) (zero : f 0 = 0) (add : (x y : α), f (x + y) = f x + f y) (mul : (x y : α), f (x * y) = f x * f y) (neg : (x : α), f (-x) = -f x) (sub : (x y : α), f (x - y) = f x - f y) (nsmul : (x : α) (n : ), f (n x) = n f x) (zsmul : (x : α) (n : ), f (n x) = n f x) :

Pushforward a non_unital_non_assoc_ring instance along a surjective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.injective.non_unital_ring {α : Type u} {β : Type v} [has_zero β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ β] [ β] (f : β α) (hf : function.injective f) (zero : f 0 = 0) (add : (x y : β), f (x + y) = f x + f y) (mul : (x y : β), f (x * y) = f x * f y) (neg : (x : β), f (-x) = -f x) (sub : (x y : β), f (x - y) = f x - f y) (nsmul : (x : β) (n : ), f (n x) = n f x) (gsmul : (x : β) (n : ), f (n x) = n f x) :

Pullback a non_unital_ring instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.non_unital_ring {α : Type u} {β : Type v} [has_zero β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ β] [ β] (f : α β) (hf : function.surjective f) (zero : f 0 = 0) (add : (x y : α), f (x + y) = f x + f y) (mul : (x y : α), f (x * y) = f x * f y) (neg : (x : α), f (-x) = -f x) (sub : (x y : α), f (x - y) = f x - f y) (nsmul : (x : α) (n : ), f (n x) = n f x) (gsmul : (x : α) (n : ), f (n x) = n f x) :

Pushforward a non_unital_ring instance along a surjective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.injective.non_assoc_ring {α : Type u} {β : Type v} [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ β] [ β] [has_nat_cast β] [has_int_cast β] (f : β α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : β), f (x + y) = f x + f y) (mul : (x y : β), f (x * y) = f x * f y) (neg : (x : β), f (-x) = -f x) (sub : (x y : β), f (x - y) = f x - f y) (nsmul : (x : β) (n : ), f (n x) = n f x) (gsmul : (x : β) (n : ), f (n x) = n f x) (nat_cast : (n : ), f n = n) (int_cast : (n : ), f n = n) :

Pullback a non_assoc_ring instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.non_assoc_ring {α : Type u} {β : Type v} [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ β] [ β] [has_nat_cast β] [has_int_cast β] (f : α β) (hf : function.surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : α), f (x + y) = f x + f y) (mul : (x y : α), f (x * y) = f x * f y) (neg : (x : α), f (-x) = -f x) (sub : (x y : α), f (x - y) = f x - f y) (nsmul : (x : α) (n : ), f (n x) = n f x) (gsmul : (x : α) (n : ), f (n x) = n f x) (nat_cast : (n : ), f n = n) (int_cast : (n : ), f n = n) :

Pushforward a non_unital_ring instance along a surjective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.injective.ring {α : Type u} {β : Type v} [ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ β] [ β] [ ] [has_nat_cast β] [has_int_cast β] (f : β α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : β), f (x + y) = f x + f y) (mul : (x y : β), f (x * y) = f x * f y) (neg : (x : β), f (-x) = -f x) (sub : (x y : β), f (x - y) = f x - f y) (nsmul : (x : β) (n : ), f (n x) = n f x) (zsmul : (x : β) (n : ), f (n x) = n f x) (npow : (x : β) (n : ), f (x ^ n) = f x ^ n) (nat_cast : (n : ), f n = n) (int_cast : (n : ), f n = n) :
ring β

Pullback a ring instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.ring {α : Type u} {β : Type v} [ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ β] [ β] [ ] [has_nat_cast β] [has_int_cast β] (f : α β) (hf : function.surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : α), f (x + y) = f x + f y) (mul : (x y : α), f (x * y) = f x * f y) (neg : (x : α), f (-x) = -f x) (sub : (x y : α), f (x - y) = f x - f y) (nsmul : (x : α) (n : ), f (n x) = n f x) (zsmul : (x : α) (n : ), f (n x) = n f x) (npow : (x : α) (n : ), f (x ^ n) = f x ^ n) (nat_cast : (n : ), f n = n) (int_cast : (n : ), f n = n) :
ring β

Pushforward a ring instance along a surjective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.injective.non_unital_comm_ring {α : Type u} {β : Type v} [has_zero β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ β] [ β] (f : β α) (hf : function.injective f) (zero : f 0 = 0) (add : (x y : β), f (x + y) = f x + f y) (mul : (x y : β), f (x * y) = f x * f y) (neg : (x : β), f (-x) = -f x) (sub : (x y : β), f (x - y) = f x - f y) (nsmul : (x : β) (n : ), f (n x) = n f x) (zsmul : (x : β) (n : ), f (n x) = n f x) :

Pullback a comm_ring instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.non_unital_comm_ring {α : Type u} {β : Type v} [has_zero β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ β] [ β] (f : α β) (hf : function.surjective f) (zero : f 0 = 0) (add : (x y : α), f (x + y) = f x + f y) (mul : (x y : α), f (x * y) = f x * f y) (neg : (x : α), f (-x) = -f x) (sub : (x y : α), f (x - y) = f x - f y) (nsmul : (x : α) (n : ), f (n x) = n f x) (zsmul : (x : α) (n : ), f (n x) = n f x) :

Pushforward a non_unital_comm_ring instance along a surjective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.injective.comm_ring {α : Type u} {β : Type v} [comm_ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ β] [ β] [ ] [has_nat_cast β] [has_int_cast β] (f : β α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : β), f (x + y) = f x + f y) (mul : (x y : β), f (x * y) = f x * f y) (neg : (x : β), f (-x) = -f x) (sub : (x y : β), f (x - y) = f x - f y) (nsmul : (x : β) (n : ), f (n x) = n f x) (zsmul : (x : β) (n : ), f (n x) = n f x) (npow : (x : β) (n : ), f (x ^ n) = f x ^ n) (nat_cast : (n : ), f n = n) (int_cast : (n : ), f n = n) :

Pullback a comm_ring instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.comm_ring {α : Type u} {β : Type v} [comm_ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ β] [ β] [ ] [has_nat_cast β] [has_int_cast β] (f : α β) (hf : function.surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : α), f (x + y) = f x + f y) (mul : (x y : α), f (x * y) = f x * f y) (neg : (x : α), f (-x) = -f x) (sub : (x y : α), f (x - y) = f x - f y) (nsmul : (x : α) (n : ), f (n x) = n f x) (zsmul : (x : α) (n : ), f (n x) = n f x) (npow : (x : α) (n : ), f (x ^ n) = f x ^ n) (nat_cast : (n : ), f n = n) (int_cast : (n : ), f n = n) :

Pushforward a comm_ring instance along a surjective function. See note [reducible non-instances].

Equations