mathlib3 documentation

logic.equiv.transfer_instance

Transfer algebraic structures across equivs #

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

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.

Implementation details #

When adding new definitions that transfer type-classes across an equivalence, please mark them @[reducible]. See note [reducible non-instances].

Tags #

equiv, group, ring, field, module, algebra

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

Transfer has_one across an equiv

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

Transfer has_zero across an equiv

Equations
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, reducible]
def equiv.has_add {α : Type u} {β : Type v} (e : α β) [has_add β] :

Transfer has_add across an equiv

Equations
@[protected, reducible]
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, reducible]
def equiv.has_sub {α : Type u} {β : Type v} (e : α β) [has_sub β] :

Transfer has_sub across an equiv

Equations
@[protected, reducible]
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, reducible]
def equiv.has_neg {α : Type u} {β : Type v} (e : α β) [has_neg β] :

Transfer has_neg across an equiv

Equations
@[protected, reducible]
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, reducible]
def equiv.has_smul {α : Type u} {β : Type v} (e : α β) (R : Type u_1) [has_smul R β] :

Transfer has_smul across an equiv

Equations
theorem equiv.smul_def {α : Type u} {β : Type v} (e : α β) {R : Type u_1} [has_smul R β] (r : R) (x : α) :
r x = (e.symm) (r e x)
@[protected, reducible]
def equiv.has_pow {α : Type u} {β : Type v} (e : α β) (N : Type u_1) [has_pow β N] :
has_pow α N

Transfer has_pow across an equiv

Equations
theorem equiv.pow_def {α : Type u} {β : Type v} (e : α β) {N : Type u_1} [has_pow β N] (n : N) (x : α) :
x ^ n = (e.symm) (e x ^ n)
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.

Equations
@[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
@[protected, reducible]
def equiv.add_semigroup {α : Type u} {β : Type v} (e : α β) [add_semigroup β] :

Transfer add_semigroup across an equiv

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

Transfer semigroup across an equiv

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

Transfer semigroup_with_zero across an equiv

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

Transfer comm_semigroup across an equiv

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

Transfer add_comm_semigroup across an equiv

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

Transfer mul_zero_class across an equiv

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

Transfer mul_one_class across an equiv

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

Transfer add_zero_class across an equiv

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

Transfer mul_zero_one_class across an equiv

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

Transfer add_monoid across an equiv

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

Transfer monoid across an equiv

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

Transfer comm_monoid across an equiv

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

Transfer add_comm_monoid across an equiv

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

Transfer group across an equiv

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

Transfer add_group across an equiv

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

Transfer add_comm_group across an equiv

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

Transfer comm_group across an equiv

Equations
@[protected, reducible]

Transfer non_unital_non_assoc_semiring across an equiv

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

Transfer non_unital_semiring across an equiv

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

Transfer add_monoid_with_one across an equiv

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

Transfer non_assoc_semiring across an equiv

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

Transfer semiring across an equiv

Equations
@[protected, reducible]

Transfer non_unital_comm_semiring across an equiv

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

Transfer comm_semiring across an equiv

Equations
@[protected, reducible]

Transfer non_unital_non_assoc_ring across an equiv

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

Transfer non_unital_ring across an equiv

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

Transfer non_assoc_ring across an equiv

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

Transfer ring across an equiv

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

Transfer non_unital_comm_ring across an equiv

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

Transfer comm_ring across an equiv

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

Transfer nontrivial across an equiv

@[protected, reducible]
theorem equiv.is_domain {α : Type u} {β : Type v} [ring α] [ring β] [is_domain β] (e : α ≃+* β) :

Transfer is_domain across an equiv

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

Transfer has_rat_cast across an equiv

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

Transfer division_ring across an equiv

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

Transfer field across an equiv

Equations
@[protected, reducible]
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
@[protected, reducible]
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
@[protected, reducible]
def equiv.module {α : 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 : module R β], module R α

Transfer module across an equiv

Equations
def equiv.linear_equiv {α : Type u} {β : Type v} (R : Type u_1) [semiring R] (e : α β) [add_comm_monoid β] [module R β] :
let _inst : add_comm_monoid α := e.add_comm_monoid, _inst_4 : module R α := equiv.module 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
@[protected, reducible]
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