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

def LibraryNote.instance_transfer_via_equivalence : Batteries.Util.LibraryNote

For many type classes, we have a definition that lets us transfer instances from one type to another using an equivalence, such as Equiv.mul for Mul. Constructing data instances in this way is discouraged because the resulting data is inefficient to unfold. To somewhat mitigate this problem, in these definitions we don't write the projections on Equiv in the usual way using Equiv.symm and DFunLike.coe, and instead use Equiv.toFun and Equiv.invFun directly. As a result, unification has to do less unfolding.

Note also that when constructing data instances in this way, it usually helps to use fast_instance% to get a faster instance.

Equations

• LibraryNote.instance_transfer_via_equivalence = default

@[reducible, inline]

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

Transfer One across an Equiv

Equations

• e.one = { one := e.invFun 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.invFun 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.invFun (e.toFun x * e.toFun 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.invFun (e.toFun x + e.toFun 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.invFun (e.toFun x / e.toFun 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.invFun (e.toFun x - e.toFun 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.invFun (e.toFun 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.invFun (-e.toFun 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.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.invFun (e.toFun x ^ n) }

@[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 (n : M) (x : α) => e.invFun (n • e.toFun 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 (n : M) (x : α) => e.invFun (n +ᵥ e.toFun x) }

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)

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

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

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

@[simp]

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

@[simp]

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.