Transfer algebraic structures across Equivs

In this file we prove lemmas of the following form: if β has a group structure and α ≃ β then α has a group structure, and similarly for monoids, semigroups and so on.

Implementation details

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

@[reducible, inline]

abbrev Equiv.one {α : Type u_2} {β : Type u_3} (e : α ≃ β) [One β] : One α

Transfer One across an Equiv

Equations

• e.one = { one := e.symm 1 }

@[reducible, inline]

abbrev Equiv.zero {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Zero β] : Zero α

Transfer Zero across an Equiv

Equations

• e.zero = { zero := e.symm 0 }

theorem Equiv.one_def {α : Type u_2} {β : Type u_3} (e : α ≃ β) [One β] : 1 = e.symm 1

theorem Equiv.zero_def {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Zero β] : 0 = e.symm 0

@[reducible, inline]

abbrev Equiv.mul {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Mul β] : Mul α

Transfer Mul across an Equiv

Equations

• e.mul = { mul := fun (x y : α) => e.symm (e x * e y) }

@[reducible, inline]

abbrev Equiv.add {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Add β] : Add α

Transfer Add across an Equiv

Equations

• e.add = { add := fun (x y : α) => e.symm (e x + e y) }

theorem Equiv.mul_def {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Mul β] (x y : α) : x * y = e.symm (e x * e y)

theorem Equiv.add_def {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Add β] (x y : α) : x + y = e.symm (e x + e y)

@[reducible, inline]

abbrev Equiv.div {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Div β] : Div α

Transfer Div across an Equiv

Equations

• e.div = { div := fun (x y : α) => e.symm (e x / e y) }

@[reducible, inline]

abbrev Equiv.sub {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Sub β] : Sub α

Transfer Sub across an Equiv

Equations

• e.sub = { sub := fun (x y : α) => e.symm (e x - e y) }

theorem Equiv.div_def {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Div β] (x y : α) : x / y = e.symm (e x / e y)

theorem Equiv.sub_def {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Sub β] (x y : α) : x - y = e.symm (e x - e y)

@[reducible, inline]

abbrev Equiv.Inv {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Inv β] : Inv α

Transfer Inv across an Equiv

Equations

• e.Inv = { inv := fun (x : α) => e.symm (e x)⁻¹ }

@[reducible, inline]

abbrev Equiv.Neg {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Neg β] : Neg α

Transfer Neg across an Equiv

Equations

• e.Neg = { neg := fun (x : α) => e.symm (-e x) }

theorem Equiv.inv_def {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Inv β] (x : α) : x⁻¹ = e.symm (e x)⁻¹

theorem Equiv.neg_def {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Neg β] (x : α) : -x = e.symm (-e x)

@[reducible, inline]

abbrev Equiv.smul (M : Type u_1) {α : Type u_2} {β : Type u_3} (e : α ≃ β) [SMul M β] : SMul M α

Transfer SMul across an Equiv

Equations

• Equiv.smul M e = { smul := fun (r : M) (x : α) => e.symm (r • e x) }

@[reducible, inline]

abbrev Equiv.vadd (M : Type u_1) {α : Type u_2} {β : Type u_3} (e : α ≃ β) [VAdd M β] : VAdd M α

Transfer VAdd across an Equiv

Equations

• Equiv.vadd M e = { vadd := fun (r : M) (x : α) => e.symm (r +ᵥ e x) }

theorem Equiv.smul_def {M : Type u_1} {α : Type u_2} {β : Type u_3} (e : α ≃ β) [SMul M β] (r : M) (x : α) : r • x = e.symm (r • e x)

theorem Equiv.vadd_def {M : Type u_1} {α : Type u_2} {β : Type u_3} (e : α ≃ β) [VAdd M β] (r : M) (x : α) : r +ᵥ x = e.symm (r +ᵥ e x)

@[reducible, inline]

abbrev Equiv.pow (M : Type u_1) {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Pow β M] : Pow α M

Transfer Pow across an Equiv

Equations

• Equiv.pow M e = { pow := fun (x : α) (n : M) => e.symm (e x ^ n) }

theorem Equiv.pow_def {M : Type u_1} {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Pow β M] (n : M) (x : α) : x ^ n = e.symm (e x ^ n)

def Equiv.mulEquiv {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Mul β] : have x := e.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.

Equations

• e.mulEquiv = { toEquiv := e, map_mul' := ⋯ }

def Equiv.addEquiv {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Add β] : have x := e.add; α ≃+ β

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.

Equations

• e.addEquiv = { toEquiv := e, map_add' := ⋯ }

@[simp]

theorem Equiv.mulEquiv_apply {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Mul β] (a : α) : e.mulEquiv a = e a

@[simp]

theorem Equiv.addEquiv_apply {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Add β] (a : α) : e.addEquiv a = e a

theorem Equiv.mulEquiv_symm_apply {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Mul β] (b : β) : (MulEquiv.symm e.mulEquiv) b = e.symm b

theorem Equiv.addEquiv_symm_apply {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Add β] (b : β) : (AddEquiv.symm e.addEquiv) b = e.symm b

@[reducible, inline]

abbrev Equiv.semigroup {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Semigroup β] : Semigroup α

Transfer Semigroup across an Equiv

Equations

• e.semigroup = Function.Injective.semigroup ⇑e ⋯ ⋯

@[reducible, inline]

abbrev Equiv.addSemigroup {α : Type u_2} {β : Type u_3} (e : α ≃ β) [AddSemigroup β] : AddSemigroup α

Transfer add_semigroup across an Equiv

Equations

• e.addSemigroup = Function.Injective.addSemigroup ⇑e ⋯ ⋯

@[reducible, inline]

abbrev Equiv.commSemigroup {α : Type u_2} {β : Type u_3} (e : α ≃ β) [CommSemigroup β] : CommSemigroup α

Transfer CommSemigroup across an Equiv

Equations

• e.commSemigroup = Function.Injective.commSemigroup ⇑e ⋯ ⋯

@[reducible, inline]

abbrev Equiv.addCommSemigroup {α : Type u_2} {β : Type u_3} (e : α ≃ β) [AddCommSemigroup β] : AddCommSemigroup α

Transfer AddCommSemigroup across an Equiv

Equations

• e.addCommSemigroup = Function.Injective.addCommSemigroup ⇑e ⋯ ⋯

theorem Equiv.isLeftCancelMul {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Mul β] [IsLeftCancelMul β] : IsLeftCancelMul α

Transfer IsLeftCancelMul across an Equiv

theorem Equiv.isLeftCancelAdd {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Add β] [IsLeftCancelAdd β] : IsLeftCancelAdd α

Transfer IsLeftCancelAdd across an Equiv

theorem Equiv.isRightCancelMul {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Mul β] [IsRightCancelMul β] : IsRightCancelMul α

Transfer IsRightCancelMul across an Equiv

theorem Equiv.isRightCancelAdd {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Add β] [IsRightCancelAdd β] : IsRightCancelAdd α

Transfer IsRightCancelAdd across an Equiv

theorem Equiv.isCancelMul {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Mul β] [IsCancelMul β] : IsCancelMul α

Transfer IsCancelMul across an Equiv

theorem Equiv.isCancelAdd {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Add β] [IsCancelAdd β] : IsCancelAdd α

Transfer IsCancelAdd across an Equiv

@[reducible, inline]

abbrev Equiv.mulOneClass {α : Type u_2} {β : Type u_3} (e : α ≃ β) [MulOneClass β] : MulOneClass α

Transfer MulOneClass across an Equiv

Equations

• e.mulOneClass = Function.Injective.mulOneClass ⇑e ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Equiv.addZeroClass {α : Type u_2} {β : Type u_3} (e : α ≃ β) [AddZeroClass β] : AddZeroClass α

Transfer AddZeroClass across an Equiv

Equations

• e.addZeroClass = Function.Injective.addZeroClass ⇑e ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Equiv.monoid {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Monoid β] : Monoid α

Transfer Monoid across an Equiv

Equations

• e.monoid = Function.Injective.monoid ⇑e ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Equiv.addMonoid {α : Type u_2} {β : Type u_3} (e : α ≃ β) [AddMonoid β] : AddMonoid α

Transfer AddMonoid across an Equiv

Equations

• e.addMonoid = Function.Injective.addMonoid ⇑e ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Equiv.commMonoid {α : Type u_2} {β : Type u_3} (e : α ≃ β) [CommMonoid β] : CommMonoid α

Transfer CommMonoid across an Equiv

Equations

• e.commMonoid = Function.Injective.commMonoid ⇑e ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Equiv.addCommMonoid {α : Type u_2} {β : Type u_3} (e : α ≃ β) [AddCommMonoid β] : AddCommMonoid α

Transfer AddCommMonoid across an Equiv

Equations

• e.addCommMonoid = Function.Injective.addCommMonoid ⇑e ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Equiv.group {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Group β] : Group α

Transfer Group across an Equiv

Equations

• e.group = Function.Injective.group ⇑e ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Equiv.addGroup {α : Type u_2} {β : Type u_3} (e : α ≃ β) [AddGroup β] : AddGroup α

Transfer AddGroup across an Equiv

Equations

• e.addGroup = Function.Injective.addGroup ⇑e ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Equiv.commGroup {α : Type u_2} {β : Type u_3} (e : α ≃ β) [CommGroup β] : CommGroup α

Transfer CommGroup across an Equiv

Equations

• e.commGroup = Function.Injective.commGroup ⇑e ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Equiv.addCommGroup {α : Type u_2} {β : Type u_3} (e : α ≃ β) [AddCommGroup β] : AddCommGroup α

Transfer AddCommGroup across an Equiv

Equations

• e.addCommGroup = Function.Injective.addCommGroup ⇑e ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem Finite.exists_type_univ_nonempty_mulEquiv (G : Type u) [Group G] [Finite G] : ∃ (G' : Type v) (x : Group G') (x_1 : Fintype G'), Nonempty (G ≃* G')

Any finite group in universe u is equivalent to some finite group in universe v.

theorem Finite.exists_type_univ_nonempty_addEquiv (G : Type u) [AddGroup G] [Finite G] : ∃ (G' : Type v) (x : AddGroup G') (x_1 : Fintype G'), Nonempty (G ≃+ G')

Any finite group in universe u is equivalent to some finite group in universe v.