# Documentation

Mathlib.Logic.Equiv.TransferInstance

# 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.

### 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

def Equiv.zero {α : Type u} {β : Type v} (e : α β) [Zero β] :
Zero α

Transfer Zero across an Equiv

Instances For
@[reducible]
def Equiv.one {α : Type u} {β : Type v} (e : α β) [One β] :
One α

Transfer One across an Equiv

Instances For
theorem Equiv.zero_def {α : Type u} {β : Type v} (e : α β) [Zero β] :
0 = e.symm 0
theorem Equiv.one_def {α : Type u} {β : Type v} (e : α β) [One β] :
1 = e.symm 1
def Equiv.add {α : Type u} {β : Type v} (e : α β) [Add β] :

Transfer Add across an Equiv

Instances For
@[reducible]
def Equiv.mul {α : Type u} {β : Type v} (e : α β) [Mul β] :
Mul α

Transfer Mul across an Equiv

Instances For
theorem Equiv.add_def {α : Type u} {β : Type v} (e : α β) [Add β] (x : α) (y : α) :
x + y = e.symm (e x + e y)
theorem Equiv.mul_def {α : Type u} {β : Type v} (e : α β) [Mul β] (x : α) (y : α) :
x * y = e.symm (e x * e y)
def Equiv.sub {α : Type u} {β : Type v} (e : α β) [Sub β] :
Sub α

Transfer Sub across an Equiv

Instances For
@[reducible]
def Equiv.div {α : Type u} {β : Type v} (e : α β) [Div β] :
Div α

Transfer Div across an Equiv

Instances For
theorem Equiv.sub_def {α : Type u} {β : Type v} (e : α β) [Sub β] (x : α) (y : α) :
x - y = e.symm (e x - e y)
theorem Equiv.div_def {α : Type u} {β : Type v} (e : α β) [Div β] (x : α) (y : α) :
x / y = e.symm (e x / e y)
def Equiv.Neg {α : Type u} {β : Type v} (e : α β) [Neg β] :
Neg α

Transfer Neg across an Equiv

Instances For
@[reducible]
def Equiv.Inv {α : Type u} {β : Type v} (e : α β) [Inv β] :
Inv α

Transfer Inv across an Equiv

Instances For
theorem Equiv.neg_def {α : Type u} {β : Type v} (e : α β) [Neg β] (x : α) :
-x = e.symm (-e x)
theorem Equiv.inv_def {α : Type u} {β : Type v} (e : α β) [Inv β] (x : α) :
x⁻¹ = e.symm (e x)⁻¹
@[reducible]
def Equiv.smul {α : Type u} {β : Type v} (e : α β) (R : Type u_1) [SMul R β] :
SMul R α

Transfer SMul across an Equiv

Instances For
theorem Equiv.smul_def {α : Type u} {β : Type v} (e : α β) {R : Type u_1} [SMul R β] (r : R) (x : α) :
r x = e.symm (r e x)
@[reducible]
def Equiv.pow {α : Type u} {β : Type v} (e : α β) (N : Type u_1) [Pow β N] :
Pow α N

Transfer Pow across an Equiv

Instances For
theorem Equiv.pow_def {α : Type u} {β : Type v} (e : α β) {N : Type u_1} [Pow β N] (n : N) (x : α) :
x ^ n = e.symm (e x ^ n)
theorem Equiv.addEquiv.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [Add β] (x : α) (y : α) :
Equiv.toFun { toFun := e.toFun, invFun := e.invFun, left_inv := (_ : Function.LeftInverse e.invFun e.toFun), right_inv := (_ : Function.RightInverse e.invFun e.toFun) } (x + y) = Equiv.toFun { toFun := e.toFun, invFun := e.invFun, left_inv := (_ : Function.LeftInverse e.invFun e.toFun), right_inv := (_ : Function.RightInverse e.invFun e.toFun) } x + Equiv.toFun { toFun := e.toFun, invFun := e.invFun, left_inv := (_ : Function.LeftInverse e.invFun e.toFun), right_inv := (_ : Function.RightInverse e.invFun e.toFun) } y
def Equiv.addEquiv {α : Type u} {β : Type v} (e : α β) [Add β] :
let mul := ; α ≃+ β

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

Instances For
def Equiv.mulEquiv {α : Type u} {β : Type v} (e : α β) [Mul β] :
let mul := ; α ≃* β

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.

Instances For
@[simp]
theorem Equiv.addEquiv_apply {α : Type u} {β : Type v} (e : α β) [Add β] (a : α) :
↑() a = e a
@[simp]
theorem Equiv.mulEquiv_apply {α : Type u} {β : Type v} (e : α β) [Mul β] (a : α) :
↑() a = e a
theorem Equiv.addEquiv_symm_apply {α : Type u} {β : Type v} (e : α β) [Add β] (b : β) :
↑() b = e.symm b
theorem Equiv.mulEquiv_symm_apply {α : Type u} {β : Type v} (e : α β) [Mul β] (b : β) :
↑() b = e.symm b
def Equiv.ringEquiv {α : Type u} {β : Type v} (e : α β) [Add β] [Mul β] :
let add := ; let mul := ; α ≃+* β

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.

Instances For
@[simp]
theorem Equiv.ringEquiv_apply {α : Type u} {β : Type v} (e : α β) [Add β] [Mul β] (a : α) :
↑() a = e a
theorem Equiv.ringEquiv_symm_apply {α : Type u} {β : Type v} (e : α β) [Add β] [Mul β] (b : β) :
↑() b = e.symm b
def Equiv.addSemigroup {α : Type u} {β : Type v} (e : α β) [] :

Transfer add_semigroup across an Equiv

Instances For
theorem Equiv.addSemigroup.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x y : α), e (e.symm (e x + e y)) = e x + e y
@[reducible]
def Equiv.semigroup {α : Type u} {β : Type v} (e : α β) [] :

Transfer Semigroup across an Equiv

Instances For
@[reducible]
def Equiv.semigroupWithZero {α : Type u} {β : Type v} (e : α β) :

Transfer SemigroupWithZero across an Equiv

Instances For
theorem Equiv.addCommSemigroup.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x y : α), e (e.symm (e x + e y)) = e x + e y
def Equiv.addCommSemigroup {α : Type u} {β : Type v} (e : α β) [] :

Transfer AddCommSemigroup across an Equiv

Instances For
@[reducible]
def Equiv.commSemigroup {α : Type u} {β : Type v} (e : α β) [] :

Transfer CommSemigroup across an Equiv

Instances For
@[reducible]
def Equiv.mulZeroClass {α : Type u} {β : Type v} (e : α β) [] :

Transfer MulZeroClass across an Equiv

Instances For
theorem Equiv.addZeroClass.proof_2 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x y : α), e (e.symm (e x + e y)) = e x + e y
theorem Equiv.addZeroClass.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [] :
e (e.symm 0) = 0
def Equiv.addZeroClass {α : Type u} {β : Type v} (e : α β) [] :

Transfer AddZeroClass across an Equiv

Instances For
@[reducible]
def Equiv.mulOneClass {α : Type u} {β : Type v} (e : α β) [] :

Transfer MulOneClass across an Equiv

Instances For
@[reducible]
def Equiv.mulZeroOneClass {α : Type u} {β : Type v} (e : α β) [] :

Transfer MulZeroOneClass across an Equiv

Instances For
theorem Equiv.addMonoid.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [] :
e (e.symm 0) = 0
theorem Equiv.addMonoid.proof_3 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x : α) (n : ), e (e.symm (n e x)) = n e x
def Equiv.addMonoid {α : Type u} {β : Type v} (e : α β) [] :

Transfer AddMonoid across an Equiv

Instances For
theorem Equiv.addMonoid.proof_2 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x y : α), e (e.symm (e x + e y)) = e x + e y
@[reducible]
def Equiv.monoid {α : Type u} {β : Type v} (e : α β) [] :

Transfer Monoid across an Equiv

Instances For
theorem Equiv.addCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [] :
e (e.symm 0) = 0
theorem Equiv.addCommMonoid.proof_3 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x : α) (n : ), e (e.symm (n e x)) = n e x
def Equiv.addCommMonoid {α : Type u} {β : Type v} (e : α β) [] :

Transfer AddCommMonoid across an Equiv

Instances For
theorem Equiv.addCommMonoid.proof_2 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x y : α), e (e.symm (e x + e y)) = e x + e y
@[reducible]
def Equiv.commMonoid {α : Type u} {β : Type v} (e : α β) [] :

Transfer CommMonoid across an Equiv

Instances For
theorem Equiv.addGroup.proof_3 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x : α), e (e.symm (-e x)) = -e x
theorem Equiv.addGroup.proof_5 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x : α) (n : ), e (e.symm (n e x)) = n e x
theorem Equiv.addGroup.proof_2 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x y : α), e (e.symm (e x + e y)) = e x + e y
theorem Equiv.addGroup.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [] :
e (e.symm 0) = 0
theorem Equiv.addGroup.proof_6 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x : α) (n : ), e (e.symm (n e x)) = n e x
theorem Equiv.addGroup.proof_4 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x y : α), e (e.symm (e x - e y)) = e x - e y
def Equiv.addGroup {α : Type u} {β : Type v} (e : α β) [] :

Transfer AddGroup across an Equiv

Instances For
@[reducible]
def Equiv.group {α : Type u} {β : Type v} (e : α β) [] :

Transfer Group across an Equiv

Instances For
theorem Equiv.addCommGroup.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [] :
e (e.symm 0) = 0
theorem Equiv.addCommGroup.proof_6 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x : α) (n : ), e (e.symm (n e x)) = n e x
theorem Equiv.addCommGroup.proof_2 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x y : α), e (e.symm (e x + e y)) = e x + e y
theorem Equiv.addCommGroup.proof_5 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x : α) (n : ), e (e.symm (n e x)) = n e x
theorem Equiv.addCommGroup.proof_4 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x y : α), e (e.symm (e x - e y)) = e x - e y
def Equiv.addCommGroup {α : Type u} {β : Type v} (e : α β) [] :

Transfer AddCommGroup across an Equiv

Instances For
theorem Equiv.addCommGroup.proof_3 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x : α), e (e.symm (-e x)) = -e x
@[reducible]
def Equiv.commGroup {α : Type u} {β : Type v} (e : α β) [] :

Transfer CommGroup across an Equiv

Instances For
@[reducible]
def Equiv.nonUnitalNonAssocSemiring {α : Type u} {β : Type v} (e : α β) :

Transfer NonUnitalNonAssocSemiring across an Equiv

Instances For
@[reducible]
def Equiv.nonUnitalSemiring {α : Type u} {β : Type v} (e : α β) :

Transfer NonUnitalSemiring across an Equiv

Instances For
@[reducible]
def Equiv.addMonoidWithOne {α : Type u} {β : Type v} (e : α β) [] :

Transfer AddMonoidWithOne across an Equiv

Instances For
@[reducible]
def Equiv.addGroupWithOne {α : Type u} {β : Type v} (e : α β) [] :

Transfer AddGroupWithOne across an Equiv

Instances For
@[reducible]
def Equiv.nonAssocSemiring {α : Type u} {β : Type v} (e : α β) [] :

Transfer NonAssocSemiring across an Equiv

Instances For
@[reducible]
def Equiv.semiring {α : Type u} {β : Type v} (e : α β) [] :

Transfer Semiring across an Equiv

Instances For
@[reducible]
def Equiv.nonUnitalCommSemiring {α : Type u} {β : Type v} (e : α β) :

Transfer NonUnitalCommSemiring across an Equiv

Instances For
@[reducible]
def Equiv.commSemiring {α : Type u} {β : Type v} (e : α β) [] :

Transfer CommSemiring across an Equiv

Instances For
@[reducible]
def Equiv.nonUnitalNonAssocRing {α : Type u} {β : Type v} (e : α β) :

Transfer NonUnitalNonAssocRing across an Equiv

Instances For
@[reducible]
def Equiv.nonUnitalRing {α : Type u} {β : Type v} (e : α β) [] :

Transfer NonUnitalRing across an Equiv

Instances For
@[reducible]
def Equiv.nonAssocRing {α : Type u} {β : Type v} (e : α β) [] :

Transfer NonAssocRing across an Equiv

Instances For
@[reducible]
def Equiv.ring {α : Type u} {β : Type v} (e : α β) [Ring β] :
Ring α

Transfer Ring across an Equiv

Instances For
@[reducible]
def Equiv.nonUnitalCommRing {α : Type u} {β : Type v} (e : α β) :

Transfer NonUnitalCommRing across an Equiv

Instances For
@[reducible]
def Equiv.commRing {α : Type u} {β : Type v} (e : α β) [] :

Transfer CommRing across an Equiv

Instances For
@[reducible]
theorem Equiv.nontrivial {α : Type u} {β : Type v} (e : α β) [] :

Transfer Nontrivial across an Equiv

@[reducible]
theorem Equiv.isDomain {α : Type u} {β : Type v} [Ring α] [Ring β] [] (e : α ≃+* β) :

Transfer IsDomain across an Equiv

@[reducible]
def Equiv.RatCast {α : Type u} {β : Type v} (e : α β) [] :

Transfer RatCast across an Equiv

Instances For
@[reducible]
def Equiv.divisionRing {α : Type u} {β : Type v} (e : α β) [] :

Transfer DivisionRing across an Equiv

Instances For
@[reducible]
def Equiv.field {α : Type u} {β : Type v} (e : α β) [] :

Transfer Field across an Equiv

Instances For
@[reducible]
def Equiv.mulAction {α : Type u} {β : Type v} (R : Type u_1) [] (e : α β) [] :

Transfer MulAction across an Equiv

Instances For
@[reducible]
def Equiv.distribMulAction {α : Type u} {β : Type v} (R : Type u_1) [] (e : α β) [] [] :

Transfer DistribMulAction across an Equiv

Instances For
@[reducible]
def Equiv.module {α : Type u} {β : Type v} (R : Type u_1) [] (e : α β) [] :
let addCommMonoid := ; [inst : Module R β] → Module R α

Transfer Module across an Equiv

Instances For
def Equiv.linearEquiv {α : Type u} {β : Type v} (R : Type u_1) [] (e : α β) [] [Module R β] :
let addCommMonoid := ; let module := ; α ≃ₗ[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.

Instances For
@[reducible]
def Equiv.algebra {α : Type u} {β : Type v} (R : Type u_1) [] (e : α β) [] :
let semiring := ; [inst : Algebra R β] → Algebra R α

Transfer Algebra across an Equiv

Instances For
def Equiv.algEquiv {α : Type u} {β : Type v} (R : Type u_1) [] (e : α β) [] [Algebra R β] :
let semiring := ; let algebra := ; α ≃ₐ[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.

Instances For