mathlib docs: data.equiv.transfer

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

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

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

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

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

add_semigroup α

Transfer add_semigroup across an equiv

source

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

semigroup α

Transfer semigroup across an equiv

Equations

e.semigroup = {mul := has_mul.mul e.has_mul, mul_assoc := _}

source

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

comm_semigroup α

Transfer comm_semigroup across an equiv

Equations

e.comm_semigroup = {mul := semigroup.mul e.semigroup, mul_assoc := _, mul_comm := _}

source

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

add_comm_semigroup α

Transfer add_comm_semigroup across an equiv

source

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

monoid α

Transfer monoid across an equiv

Equations

e.monoid = {mul := semigroup.mul e.semigroup, mul_assoc := _, one := 1, one_mul := _, mul_one := _}

source

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

add_monoid α

Transfer add_monoid across an equiv

source

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

add_comm_monoid α

Transfer add_comm_monoid across an equiv

source

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

comm_monoid α

Transfer comm_monoid across an equiv

Equations

e.comm_monoid = {mul := comm_semigroup.mul e.comm_semigroup, mul_assoc := _, one := monoid.one e.monoid, one_mul := _, mul_one := _, mul_comm := _}

source

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

group α

Transfer group across an equiv

Equations

e.group = {mul := monoid.mul e.monoid, mul_assoc := _, one := monoid.one e.monoid, one_mul := _, mul_one := _, inv := has_inv.inv e.has_inv, mul_left_inv := _}

source

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

add_group α

Transfer add_group across an equiv

source

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

comm_group α

Transfer comm_group across an equiv

Equations

e.comm_group = {mul := group.mul e.group, mul_assoc := _, one := group.one e.group, one_mul := _, mul_one := _, inv := group.inv e.group, mul_left_inv := _, mul_comm := _}

source

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

add_comm_group α

Transfer add_comm_group across an equiv

source

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

semiring α

Transfer semiring across an equiv

Equations

e.semiring = {add := has_add.add e.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, add_comm := _, mul := has_mul.mul e.has_mul, mul_assoc := _, one := monoid.one e.monoid, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}

source

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

comm_semiring α

Transfer comm_semiring across an equiv

Equations

e.comm_semiring = {add := semiring.add e.semiring, add_assoc := _, zero := semiring.zero e.semiring, zero_add := _, add_zero := _, add_comm := _, mul := semiring.mul e.semiring, mul_assoc := _, one := semiring.one e.semiring, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, mul_comm := _}

source

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

ring α

Transfer ring across an equiv

Equations

e.ring = {add := semiring.add e.semiring, add_assoc := _, zero := semiring.zero e.semiring, zero_add := _, add_zero := _, neg := add_comm_group.neg e.add_comm_group, add_left_neg := _, add_comm := _, mul := semiring.mul e.semiring, mul_assoc := _, one := semiring.one e.semiring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _}

source

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

comm_ring α

Transfer comm_ring across an equiv

Equations

e.comm_ring = {add := ring.add e.ring, add_assoc := _, zero := ring.zero e.ring, zero_add := _, add_zero := _, neg := ring.neg e.ring, add_left_neg := _, add_comm := _, mul := comm_monoid.mul e.comm_monoid, mul_assoc := _, one := comm_monoid.one e.comm_monoid, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}

source

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

nontrivial α

Transfer nonzero across an equiv

source

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

domain α

Transfer domain across an equiv

Equations

e.domain = {add := ring.add e.ring, add_assoc := _, zero := ring.zero e.ring, zero_add := _, add_zero := _, neg := ring.neg e.ring, add_left_neg := _, add_comm := _, mul := ring.mul e.ring, mul_assoc := _, one := ring.one e.ring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}

source

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

integral_domain α

Transfer integral_domain across an equiv

Equations

e.integral_domain = {add := domain.add e.domain, add_assoc := _, zero := domain.zero e.domain, zero_add := _, add_zero := _, neg := domain.neg e.domain, add_left_neg := _, add_comm := _, mul := domain.mul e.domain, mul_assoc := _, one := domain.one e.domain, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}

source

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

division_ring α

Transfer division_ring across an equiv

Equations

e.division_ring = {add := domain.add e.domain, add_assoc := _, zero := 0, zero_add := _, add_zero := _, neg := domain.neg e.domain, add_left_neg := _, add_comm := _, mul := domain.mul e.domain, mul_assoc := _, one := 1, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, inv := has_inv.inv e.has_inv, exists_pair_ne := _, mul_inv_cancel := _, inv_mul_cancel := _, inv_zero := _}

source

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

field α

Transfer field across an equiv

Equations

e.field = {add := integral_domain.add e.integral_domain, add_assoc := _, zero := integral_domain.zero e.integral_domain, zero_add := _, add_zero := _, neg := integral_domain.neg e.integral_domain, add_left_neg := _, add_comm := _, mul := integral_domain.mul e.integral_domain, mul_assoc := _, one := integral_domain.one e.integral_domain, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := division_ring.inv e.division_ring, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}

source

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

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

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

equiv.semimodule R e = let _inst : add_comm_monoid α := e.add_comm_monoid in λ (_inst_3 : semimodule 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 β] [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

equiv.linear_equiv R e = let _inst : add_comm_monoid α := e.add_comm_monoid, _inst_4 : semimodule R α := equiv.semimodule 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

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' := _}

mathlib documentation

data.equiv.transfer_instance

Transfer algebraic structures across `equiv`s

Tags

General documentation

Additional documentation

Library

mathlib documentation

data.​equiv.​transfer_instance

Transfer algebraic structures across equivs

Tags

General documentation

Additional documentation

Library

data.equiv.transfer_instance

Transfer algebraic structures across `equiv`s