# mathlibdocumentation

data.equiv.transfer_instance

# Transfer algebraic structures across equivs #

In this file we prove theorems of the following form: if β has a group structure and α ≃ β then α has a group structure, and similarly for monoids, semigroups, rings, integral domains, fields and so on.

Note that most of these constructions can also be obtained using the transport tactic.

## Tags #

equiv, group, ring, field, module, algebra

@[protected]
def equiv.has_one {α : Type u} {β : Type v} (e : α β) [has_one β] :

Transfer has_one across an equiv

Equations
@[protected]
def equiv.has_zero {α : Type u} {β : Type v} (e : α β) [has_zero β] :

Transfer has_zero across an equiv

theorem equiv.one_def {α : Type u} {β : Type v} (e : α β) [has_one β] :
1 = (e.symm) 1
theorem equiv.zero_def {α : Type u} {β : Type v} (e : α β) [has_zero β] :
0 = (e.symm) 0
@[protected]
def equiv.has_add {α : Type u} {β : Type v} (e : α β) [has_add β] :

Transfer has_add across an equiv

@[protected]
def equiv.has_mul {α : Type u} {β : Type v} (e : α β) [has_mul β] :

Transfer has_mul across an equiv

Equations
theorem equiv.add_def {α : Type u} {β : Type v} (e : α β) [has_add β] (x y : α) :
x + y = (e.symm) (e x + e y)
theorem equiv.mul_def {α : Type u} {β : Type v} (e : α β) [has_mul β] (x y : α) :
x * y = (e.symm) ((e x) * e y)
@[protected]
def equiv.has_sub {α : Type u} {β : Type v} (e : α β) [has_sub β] :

Transfer has_sub across an equiv

@[protected]
def equiv.has_div {α : Type u} {β : Type v} (e : α β) [has_div β] :

Transfer has_div across an equiv

Equations
theorem equiv.div_def {α : Type u} {β : Type v} (e : α β) [has_div β] (x y : α) :
x / y = (e.symm) (e x / e y)
theorem equiv.sub_def {α : Type u} {β : Type v} (e : α β) [has_sub β] (x y : α) :
x - y = (e.symm) (e x - e y)
@[protected]
def equiv.has_neg {α : Type u} {β : Type v} (e : α β) [has_neg β] :

Transfer has_neg across an equiv

@[protected]
def equiv.has_inv {α : Type u} {β : Type v} (e : α β) [has_inv β] :

Transfer has_inv across an equiv

Equations
theorem equiv.inv_def {α : Type u} {β : Type v} (e : α β) [has_inv β] (x : α) :
theorem equiv.neg_def {α : Type u} {β : Type v} (e : α β) [has_neg β] (x : α) :
-x = (e.symm) (-e x)
@[protected]
def equiv.has_scalar {α : Type u} {β : Type v} (e : α β) {R : Type u_1} [ β] :
α

Transfer has_scalar across an equiv

Equations
theorem equiv.smul_def {α : Type u} {β : Type v} (e : α β) {R : Type u_1} [ β] (r : R) (x : α) :
r x = (e.symm) (r e x)
def equiv.mul_equiv {α : Type u} {β : Type v} (e : α β) [has_mul β] :
let _inst : := e.has_mul in α ≃* β

An equivalence e : α ≃ β gives a multiplicative equivalence α ≃* β where the multiplicative structure on α is the one obtained by transporting a multiplicative structure on β back along e.

Equations
def equiv.add_equiv {α : Type u} {β : Type v} (e : α β) [has_add β] :
let _inst : := e.has_add in α ≃+ β

An equivalence e : α ≃ β gives a additive equivalence α ≃+ β where the additive structure on α is the one obtained by transporting an additive structure on β back along e.

@[simp]
theorem equiv.mul_equiv_apply {α : Type u} {β : Type v} (e : α β) [has_mul β] (a : α) :
(e.mul_equiv) a = e a
@[simp]
theorem equiv.add_equiv_apply {α : Type u} {β : Type v} (e : α β) [has_add β] (a : α) :
theorem equiv.add_equiv_symm_apply {α : Type u} {β : Type v} (e : α β) [has_add β] (b : β) :
let _inst : := e.has_add in b = (e.symm) b
theorem equiv.mul_equiv_symm_apply {α : Type u} {β : Type v} (e : α β) [has_mul β] (b : β) :
let _inst : := e.has_mul in b = (e.symm) b
def equiv.ring_equiv {α : Type u} {β : Type v} (e : α β) [has_add β] [has_mul β] :
let _inst : := e.has_add, _inst_3 : := e.has_mul in α ≃+* β

An equivalence e : α ≃ β gives a ring equivalence α ≃+* β where the ring structure on α is the one obtained by transporting a ring structure on β back along e.

Equations
@[simp]
theorem equiv.ring_equiv_apply {α : Type u} {β : Type v} (e : α β) [has_add β] [has_mul β] (a : α) :
theorem equiv.ring_equiv_symm_apply {α : Type u} {β : Type v} (e : α β) [has_add β] [has_mul β] (b : β) :
let _inst : := e.has_add, _inst_3 : := e.has_mul in = (e.symm) b
@[protected]
def equiv.add_semigroup {α : Type u} {β : Type v} (e : α β)  :

Transfer add_semigroup across an equiv

@[protected]
def equiv.semigroup {α : Type u} {β : Type v} (e : α β) [semigroup β] :

Transfer semigroup across an equiv

Equations
@[protected]
def equiv.semigroup_with_zero {α : Type u} {β : Type v} (e : α β)  :

Transfer semigroup_with_zero across an equiv

Equations
@[protected]
def equiv.comm_semigroup {α : Type u} {β : Type v} (e : α β)  :

Transfer comm_semigroup across an equiv

Equations
@[protected]
def equiv.add_comm_semigroup {α : Type u} {β : Type v} (e : α β)  :

Transfer add_comm_semigroup across an equiv

@[protected]
def equiv.mul_zero_class {α : Type u} {β : Type v} (e : α β)  :

Transfer mul_zero_class across an equiv

Equations
@[protected]
def equiv.mul_one_class {α : Type u} {β : Type v} (e : α β)  :

Transfer mul_one_class across an equiv

Equations
@[protected]
def equiv.add_zero_class {α : Type u} {β : Type v} (e : α β)  :

Transfer add_zero_class across an equiv

@[protected]
def equiv.mul_zero_one_class {α : Type u} {β : Type v} (e : α β)  :

Transfer mul_zero_one_class across an equiv

Equations
@[protected]
def equiv.add_monoid {α : Type u} {β : Type v} (e : α β) [add_monoid β] :

Transfer add_monoid across an equiv

@[protected]
def equiv.monoid {α : Type u} {β : Type v} (e : α β) [monoid β] :

Transfer monoid across an equiv

Equations
@[protected]
def equiv.comm_monoid {α : Type u} {β : Type v} (e : α β) [comm_monoid β] :

Transfer comm_monoid across an equiv

Equations
@[protected]
def equiv.add_comm_monoid {α : Type u} {β : Type v} (e : α β)  :

Transfer add_comm_monoid across an equiv

@[protected]
def equiv.group {α : Type u} {β : Type v} (e : α β) [group β] :

Transfer group across an equiv

Equations
@[protected]
def equiv.add_group {α : Type u} {β : Type v} (e : α β) [add_group β] :

Transfer add_group across an equiv

@[protected]
def equiv.add_comm_group {α : Type u} {β : Type v} (e : α β)  :

Transfer add_comm_group across an equiv

@[protected]
def equiv.comm_group {α : Type u} {β : Type v} (e : α β) [comm_group β] :

Transfer comm_group across an equiv

Equations
@[protected]
def equiv.semiring {α : Type u} {β : Type v} (e : α β) [semiring β] :

Transfer semiring across an equiv

Equations
@[protected]
def equiv.comm_semiring {α : Type u} {β : Type v} (e : α β)  :

Transfer comm_semiring across an equiv

Equations
@[protected]
def equiv.ring {α : Type u} {β : Type v} (e : α β) [ring β] :
ring α

Transfer ring across an equiv

Equations
@[protected]
def equiv.comm_ring {α : Type u} {β : Type v} (e : α β) [comm_ring β] :

Transfer comm_ring across an equiv

Equations
@[protected]
theorem equiv.nontrivial {α : Type u} {β : Type v} (e : α β) [nontrivial β] :

Transfer nonzero across an equiv

@[protected]
def equiv.domain {α : Type u} {β : Type v} (e : α β) [domain β] :

Transfer domain across an equiv

Equations
@[protected]
def equiv.integral_domain {α : Type u} {β : Type v} (e : α β)  :

Transfer integral_domain across an equiv

Equations
@[protected]
def equiv.division_ring {α : Type u} {β : Type v} (e : α β)  :

Transfer division_ring across an equiv

Equations
@[protected]
def equiv.field {α : Type u} {β : Type v} (e : α β) [field β] :

Transfer field across an equiv

Equations
@[protected]
def equiv.mul_action {α : Type u} {β : Type v} (R : Type u_1) [monoid R] (e : α β) [ β] :
α

Transfer mul_action across an equiv

Equations
@[protected]
def equiv.distrib_mul_action {α : Type u} {β : Type v} (R : Type u_1) [monoid R] (e : α β)  :
let _inst : := e.add_comm_monoid in Π [_inst_3 : ,

Transfer distrib_mul_action across an equiv

Equations
@[protected]
def equiv.module {α : Type u} {β : Type v} (R : Type u_1) [semiring R] (e : α β)  :
let _inst : := e.add_comm_monoid in Π [_inst_3 : β], α

Transfer module across an equiv

Equations
def equiv.linear_equiv {α : Type u} {β : Type v} (R : Type u_1) [semiring R] (e : α β) [ β] :
let _inst : := e.add_comm_monoid, _inst_4 : α := e in α ≃ₗ[R] β

An equivalence e : α ≃ β gives a linear equivalence α ≃ₗ[R] β where the R-module structure on α is the one obtained by transporting an R-module structure on β back along e.

Equations
@[protected]
def equiv.algebra {α : Type u} {β : Type v} (R : Type u_1) (e : α β) [semiring β] :
let _inst : := e.semiring in Π [_inst_3 : β], α

Transfer algebra across an equiv

Equations
def equiv.alg_equiv {α : Type u} {β : Type v} (R : Type u_1) (e : α β) [semiring β] [ β] :
let _inst : := e.semiring, _inst_4 : α := in α ≃ₐ[R] β

An equivalence e : α ≃ β gives an algebra equivalence α ≃ₐ[R] β where the R-algebra structure on α is the one obtained by transporting an R-algebra structure on β back along e.

Equations
@[protected]
theorem ring_equiv.local_ring {A : Type u_1} {B : Type u_2} [comm_ring A] [local_ring A] [comm_ring B] (e : A ≃+* B) :