mathlib documentation

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

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

Transfer has_one across an equiv

Equations
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

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

Transfer has_add across an equiv

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)

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

Transfer has_neg across an equiv

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)

def equiv.has_scalar {α : Type u} {β : Type v} (e : α β) {R : Type u_1} [has_scalar R β] :

Transfer has_scalar across an equiv

Equations
theorem equiv.smul_def {α : Type u} {β : Type v} (e : α β) {R : Type u_1} [has_scalar R β] (r : R) (x : α) :
r x = (e.symm) (r e x)

def equiv.mul_equiv {α : Type u} {β : Type v} (e : α β) [has_mul β] :
let _inst : has_mul α := 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 : has_add α := 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 : α) :
(e.add_equiv) a = e a

theorem equiv.add_equiv_symm_apply {α : Type u} {β : Type v} (e : α β) [has_add β] (b : β) :
let _inst : has_add α := e.has_add in (add_equiv.symm e.add_equiv) b = (e.symm) b

theorem equiv.mul_equiv_symm_apply {α : Type u} {β : Type v} (e : α β) [has_mul β] (b : β) :
let _inst : has_mul α := e.has_mul in (mul_equiv.symm e.mul_equiv) b = (e.symm) b

def equiv.ring_equiv {α : Type u} {β : Type v} (e : α β) [has_add β] [has_mul β] :
let _inst : has_add α := e.has_add, _inst_3 : has_mul α := 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 : has_add α := e.has_add, _inst_3 : has_mul α := e.has_mul in (ring_equiv.symm e.ring_equiv) b = (e.symm) b

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

Transfer add_semigroup across an equiv

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

Transfer semigroup across an equiv

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

Transfer comm_semigroup across an equiv

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

Transfer add_comm_semigroup across an equiv

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

Transfer add_monoid across an equiv

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

Transfer monoid across an equiv

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

Transfer comm_monoid across an equiv

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

Transfer add_comm_monoid across an equiv

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

Transfer group across an equiv

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

Transfer add_group across an equiv

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

Transfer add_comm_group across an equiv

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

Transfer comm_group across an equiv

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

Transfer semiring across an equiv

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

Transfer comm_semiring across an equiv

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

Transfer ring across an equiv

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

Transfer comm_ring across an equiv

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

Transfer nonzero across an equiv

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

Transfer domain across an equiv

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

Transfer integral_domain across an equiv

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

Transfer division_ring across an equiv

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

Transfer mul_action across an equiv

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

Transfer distrib_mul_action across an equiv

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

Transfer semimodule across an equiv

Equations
def equiv.linear_equiv {α : Type u} {β : Type v} (R : Type u_1) [semiring R] (e : α β) [add_comm_monoid β] [semimodule R β] :
let _inst : add_comm_monoid α := e.add_comm_monoid, _inst_4 : semimodule R α := equiv.semimodule R 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
def equiv.algebra {α : Type u} {β : Type v} (R : Type u_1) [comm_semiring R] (e : α β) [semiring β] :
let _inst : semiring α := e.semiring in Π [_inst_3 : algebra R β], algebra R α

Transfer algebra across an equiv

Equations
def equiv.alg_equiv {α : Type u} {β : Type v} (R : Type u_1) [comm_semiring R] (e : α β) [semiring β] [algebra R β] :
let _inst : semiring α := e.semiring, _inst_4 : algebra R α := equiv.algebra R e 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
theorem ring_equiv.local_ring {A : Type u_1} {B : Type u_2} [comm_ring A] [local_ring A] [comm_ring B] :
A ≃+* Blocal_ring B