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

@[reducible, inline]

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

Transfer Zero across an Equiv

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

@[reducible, inline]

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

Transfer Add across an Equiv

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

@[reducible, inline]

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

Transfer Sub across an Equiv

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

@[reducible, inline]

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

Transfer Neg across an Equiv

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

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

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

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.

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.

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

@[reducible, inline]

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

Transfer add_semigroup across an Equiv

@[reducible, inline]

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

Transfer CommSemigroup across an Equiv

@[reducible, inline]

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

Transfer AddCommSemigroup across an Equiv

@[reducible, inline]

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

Transfer MulOneClass across an Equiv

@[reducible, inline]

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

Transfer AddZeroClass across an Equiv

@[reducible, inline]

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

Transfer Monoid across an Equiv

@[reducible, inline]

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

Transfer AddMonoid across an Equiv

@[reducible, inline]

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

Transfer CommMonoid across an Equiv

@[reducible, inline]

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

Transfer AddCommMonoid across an Equiv

@[reducible, inline]

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

Transfer Group across an Equiv

@[reducible, inline]

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

Transfer AddGroup across an Equiv

@[reducible, inline]

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

Transfer CommGroup across an Equiv

@[reducible, inline]

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

Transfer AddCommGroup across an Equiv

@[reducible, inline]

abbrev Equiv.mulAction (M : Type u_1) {α : Type u_2} {β : Type u_3} [Monoid M] (e : α ≃ β) [MulAction M β] : MulAction M α

Transfer MulAction across an Equiv

@[reducible, inline]

abbrev Equiv.addAction (M : Type u_1) {α : Type u_2} {β : Type u_3} [AddMonoid M] (e : α ≃ β) [AddAction M β] : AddAction M α

Transfer AddAction across an Equiv

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.