data.equiv.transfer_instance

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

e.mul_equiv = let _inst : has_mul α := e.has_mul in {to_fun := e.to_fun, inv_fun := e.inv_fun, left_inv := _, right_inv := _, map_mul' := _}

source

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.

source

@[simp]

theorem equiv.mul_equiv_apply {α : Type u} {β : Type v} (e : α ≃ β) [has_mul β] (a : α) :

⇑(e.mul_equiv) a = ⇑e a

source

@[simp]

theorem equiv.add_equiv_apply {α : Type u} {β : Type v} (e : α ≃ β) [has_add β] (a : α) :

⇑(e.add_equiv) a = ⇑e a

source

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

source

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

source

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

e.ring_equiv = let _inst : has_add α := e.has_add, _inst_3 : has_mul α := e.has_mul in {to_fun := e.to_fun, inv_fun := e.inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

source

@[simp]

theorem equiv.ring_equiv_apply {α : Type u} {β : Type v} (e : α ≃ β) [has_add β] [has_mul β] (a : α) :

⇑(e.ring_equiv) a = ⇑e a

source

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

source

@[protected]

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

add_semigroup α

Transfer add_semigroup across an equiv

source

@[protected]

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

semigroup α

Transfer semigroup across an equiv

Equations

e.semigroup = let mul : has_mul α := e.has_mul in function.injective.semigroup ⇑e _ _

source

@[protected]

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

semigroup_with_zero α

Transfer semigroup_with_zero across an equiv

Equations

e.semigroup_with_zero = let mul : has_mul α := e.has_mul, zero : has_zero α := e.has_zero in function.injective.semigroup_with_zero ⇑e _ _ _

source

@[protected]

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

comm_semigroup α

Transfer comm_semigroup across an equiv

Equations

e.comm_semigroup = let mul : has_mul α := e.has_mul in function.injective.comm_semigroup ⇑e _ _

source

@[protected]

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

add_comm_semigroup α

Transfer add_comm_semigroup across an equiv

source

@[protected]

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

mul_zero_class α

Transfer mul_zero_class across an equiv

Equations

e.mul_zero_class = let zero : has_zero α := e.has_zero, mul : has_mul α := e.has_mul in function.injective.mul_zero_class ⇑e _ _ _

source

@[protected]

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

mul_one_class α

Transfer mul_one_class across an equiv

Equations

e.mul_one_class = let one : has_one α := e.has_one, mul : has_mul α := e.has_mul in function.injective.mul_one_class ⇑e _ _ _

source

@[protected]

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

add_zero_class α

Transfer add_zero_class across an equiv

source

@[protected]

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

mul_zero_one_class α

Transfer mul_zero_one_class across an equiv

Equations

e.mul_zero_one_class = let zero : has_zero α := e.has_zero, one : has_one α := e.has_one, mul : has_mul α := e.has_mul in function.injective.mul_zero_one_class ⇑e _ _ _ _

source

@[protected]

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

add_monoid α

Transfer add_monoid across an equiv

source

@[protected]

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

monoid α

Transfer monoid across an equiv

Equations

e.monoid = let one : has_one α := e.has_one, mul : has_mul α := e.has_mul in function.injective.monoid ⇑e _ _ _

source

@[protected]

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

comm_monoid α

Transfer comm_monoid across an equiv

Equations

e.comm_monoid = let one : has_one α := e.has_one, mul : has_mul α := e.has_mul in function.injective.comm_monoid ⇑e _ _ _

source

@[protected]

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

add_comm_monoid α

Transfer add_comm_monoid across an equiv

source

@[protected]

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

group α

Transfer group across an equiv

Equations

e.group = let one : has_one α := e.has_one, mul : has_mul α := e.has_mul, inv : has_inv α := e.has_inv, div : has_div α := e.has_div in function.injective.group ⇑e _ _ _ _ _

source

@[protected]

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

add_group α

Transfer add_group across an equiv

source

@[protected]

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

add_comm_group α

Transfer add_comm_group across an equiv

source

@[protected]

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

comm_group α

Transfer comm_group across an equiv

Equations

e.comm_group = let one : has_one α := e.has_one, mul : has_mul α := e.has_mul, inv : has_inv α := e.has_inv, div : has_div α := e.has_div in function.injective.comm_group ⇑e _ _ _ _ _

source

@[protected]

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

semiring α

Transfer semiring across an equiv

Equations

e.semiring = let zero : has_zero α := e.has_zero, add : has_add α := e.has_add, one : has_one α := e.has_one, mul : has_mul α := e.has_mul in function.injective.semiring ⇑e _ _ _ _ _

source

@[protected]

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

comm_semiring α

Transfer comm_semiring across an equiv

Equations

e.comm_semiring = let zero : has_zero α := e.has_zero, add : has_add α := e.has_add, one : has_one α := e.has_one, mul : has_mul α := e.has_mul in function.injective.comm_semiring ⇑e _ _ _ _ _

source

@[protected]

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

ring α

Transfer ring across an equiv

Equations

e.ring = let zero : has_zero α := e.has_zero, add : has_add α := e.has_add, one : has_one α := e.has_one, mul : has_mul α := e.has_mul, neg : has_neg α := e.has_neg, sub : has_sub α := e.has_sub in function.injective.ring ⇑e _ _ _ _ _ _ _

source

@[protected]

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

comm_ring α

Transfer comm_ring across an equiv

Equations

e.comm_ring = let zero : has_zero α := e.has_zero, add : has_add α := e.has_add, one : has_one α := e.has_one, mul : has_mul α := e.has_mul, neg : has_neg α := e.has_neg, sub : has_sub α := e.has_sub in function.injective.comm_ring ⇑e _ _ _ _ _ _ _

source

@[protected]

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

nontrivial α

Transfer nonzero across an equiv

source

@[protected]

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

domain α

Transfer domain across an equiv

Equations

e.domain = let zero : has_zero α := e.has_zero, add : has_add α := e.has_add, one : has_one α := e.has_one, mul : has_mul α := e.has_mul, neg : has_neg α := e.has_neg, sub : has_sub α := e.has_sub in function.injective.domain ⇑e _ _ _ _ _ _ _

source

@[protected]

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

integral_domain α

Transfer integral_domain across an equiv

Equations

e.integral_domain = let zero : has_zero α := e.has_zero, add : has_add α := e.has_add, one : has_one α := e.has_one, mul : has_mul α := e.has_mul, neg : has_neg α := e.has_neg, sub : has_sub α := e.has_sub in function.injective.integral_domain ⇑e _ _ _ _ _ _ _

source

@[protected]

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

division_ring α

Transfer division_ring across an equiv

Equations

e.division_ring = let zero : has_zero α := e.has_zero, add : has_add α := e.has_add, one : has_one α := e.has_one, mul : has_mul α := e.has_mul, neg : has_neg α := e.has_neg, sub : has_sub α := e.has_sub, inv : has_inv α := e.has_inv, div : has_div α := e.has_div in function.injective.division_ring ⇑e _ _ _ _ _ _ _ _ _

source

@[protected]

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

field α

Transfer field across an equiv

Equations

e.field = let zero : has_zero α := e.has_zero, add : has_add α := e.has_add, one : has_one α := e.has_one, mul : has_mul α := e.has_mul, neg : has_neg α := e.has_neg, sub : has_sub α := e.has_sub, inv : has_inv α := e.has_inv, div : has_div α := e.has_div in function.injective.field ⇑e _ _ _ _ _ _ _ _ _

source

@[protected]

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

mul_action R α

Transfer mul_action across an equiv

Equations

equiv.mul_action R e = {to_has_scalar := {smul := has_scalar.smul e.has_scalar}, one_smul := _, mul_smul := _}

source

@[protected]

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

equiv.distrib_mul_action R e = let _inst : add_comm_monoid α := e.add_comm_monoid in λ (_inst_3 : distrib_mul_action R β), let _inst_4 : add_comm_monoid α := e.add_comm_monoid in {to_mul_action := {to_has_scalar := mul_action.to_has_scalar (equiv.mul_action R e), one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}

source

@[protected]

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

equiv.module R e = let _inst : add_comm_monoid α := e.add_comm_monoid in λ (_inst_3 : module R β), {to_distrib_mul_action := {to_mul_action := distrib_mul_action.to_mul_action (equiv.distrib_mul_action R e), smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}

source

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

equiv.linear_equiv R e = let _inst : add_comm_monoid α := e.add_comm_monoid, _inst_4 : module R α := equiv.module R e in {to_fun := e.add_equiv.to_fun, map_add' := _, map_smul' := _, inv_fun := e.add_equiv.inv_fun, left_inv := _, right_inv := _}

source

@[protected]

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

equiv.algebra R e = let _inst : semiring α := e.semiring in λ (_inst_3 : algebra R β), (↑(ring_equiv.symm e.ring_equiv).comp (algebra_map R β)).to_algebra' _

source

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

equiv.alg_equiv R e = let _inst : semiring α := e.semiring, _inst_4 : algebra R α := equiv.algebra R e in {to_fun := e.ring_equiv.to_fun, inv_fun := e.ring_equiv.inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

source

@[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) :

local_ring B

mathlib documentation

Transfer algebraic structures across `equiv`s #

Tags #

Transfer algebraic structures across equivs #

Tags #

Transfer algebraic structures across `equiv`s #