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 use abbrev. See note [reducible non-instances].

Tags

equiv, group, ring, field, module, algebra

@[reducible, inline]

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

Transfer One across an Equiv

Equations

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

@[reducible, inline]

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

Transfer Zero across an Equiv

Equations

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

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

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

noncomputable instance Equiv.instOneShrink {α : Type u} [Small.{v, u} α] [One α] : One (Shrink.{v, u} α)

Equations

• Equiv.instOneShrink = (equivShrink α).symm.one

noncomputable instance Equiv.instZeroShrink {α : Type u} [Small.{v, u} α] [Zero α] : Zero (Shrink.{v, u} α)

Equations

• Equiv.instZeroShrink = (equivShrink α).symm.zero

@[reducible, inline]

abbrev Equiv.mul {α : Type u} {β : Type v} (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} {β : Type v} (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} {β : Type v} (e : α ≃ β) [Mul β] (x y : α) : x * y = e.symm (e x * e y)

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

noncomputable instance Equiv.instMulShrink {α : Type u} [Small.{v, u} α] [Mul α] : Mul (Shrink.{v, u} α)

Equations

• Equiv.instMulShrink = (equivShrink α).symm.mul

noncomputable instance Equiv.instAddShrink {α : Type u} [Small.{v, u} α] [Add α] : Add (Shrink.{v, u} α)

Equations

• Equiv.instAddShrink = (equivShrink α).symm.add

@[reducible, inline]

abbrev Equiv.div {α : Type u} {β : Type v} (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} {β : Type v} (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} {β : Type v} (e : α ≃ β) [Div β] (x y : α) : x / y = e.symm (e x / e y)

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

noncomputable instance Equiv.instDivShrink {α : Type u} [Small.{v, u} α] [Div α] : Div (Shrink.{v, u} α)

Equations

• Equiv.instDivShrink = (equivShrink α).symm.div

noncomputable instance Equiv.instSubShrink {α : Type u} [Small.{v, u} α] [Sub α] : Sub (Shrink.{v, u} α)

Equations

• Equiv.instSubShrink = (equivShrink α).symm.sub

@[reducible, inline]

abbrev Equiv.Inv {α : Type u} {β : Type v} (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} {β : Type v} (e : α ≃ β) [Neg β] : Neg α

Transfer Neg across an Equiv

Equations

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

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

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

noncomputable instance Equiv.instInvShrink {α : Type u} [Small.{v, u} α] [Inv α] : Inv (Shrink.{v, u} α)

Equations

• Equiv.instInvShrink = (equivShrink α).symm.Inv

noncomputable instance Equiv.instNegShrink {α : Type u} [Small.{v, u} α] [Neg α] : Neg (Shrink.{v, u} α)

Equations

• Equiv.instNegShrink = (equivShrink α).symm.Neg

@[reducible, inline]

abbrev Equiv.smul {α : Type u} {β : Type v} (e : α ≃ β) (R : Type u_1) [SMul R β] : SMul R α

Transfer SMul across an Equiv

Equations

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

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)

noncomputable instance Equiv.instSMulShrink {α : Type u} [Small.{v, u} α] (R : Type u_1) [SMul R α] : SMul R (Shrink.{v, u} α)

Equations

• Equiv.instSMulShrink R = (equivShrink α).symm.smul R

@[reducible]

def Equiv.pow {α : Type u} {β : Type v} (e : α ≃ β) (N : Type u_1) [Pow β N] : Pow α N

Transfer Pow across an Equiv

Equations

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

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)

noncomputable instance Equiv.instPowShrink {α : Type u} [Small.{v, u} α] (N : Type u_1) [Pow α N] : Pow (Shrink.{v, u} α) N

Equations

• Equiv.instPowShrink N = (equivShrink α).symm.pow N

def Equiv.mulEquiv {α : Type u} {β : Type v} (e : α ≃ β) [Mul β] : let 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} {β : Type v} (e : α ≃ β) [Add β] : let 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} {β : Type v} (e : α ≃ β) [Mul β] (a : α) : e.mulEquiv a = e a

@[simp]

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

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

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

noncomputable def Shrink.mulEquiv {α : Type u} [Small.{v, u} α] [Mul α] : Shrink.{v, u} α ≃* α

Shrink α to a smaller universe preserves multiplication.

Equations

• Shrink.mulEquiv = (equivShrink α).symm.mulEquiv

noncomputable def Shrink.addEquiv {α : Type u} [Small.{v, u} α] [Add α] : Shrink.{v, u} α ≃+ α

Shrink α to a smaller universe preserves addition.

Equations

• Shrink.addEquiv = (equivShrink α).symm.addEquiv

def Equiv.ringEquiv {α : Type u} {β : Type v} (e : α ≃ β) [Add β] [Mul β] : let add := e.add; let mul := e.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.

Equations

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

@[simp]

theorem Equiv.ringEquiv_apply {α : Type u} {β : Type v} (e : α ≃ β) [Add β] [Mul β] (a : α) : e.ringEquiv a = e a

theorem Equiv.ringEquiv_symm_apply {α : Type u} {β : Type v} (e : α ≃ β) [Add β] [Mul β] (b : β) : (RingEquiv.symm e.ringEquiv) b = e.symm b

noncomputable def Shrink.ringEquiv (α : Type u) [Small.{v, u} α] [Add α] [Mul α] : Shrink.{v, u} α ≃+* α

Shrink α to a smaller universe preserves ring structure.

Equations

• Shrink.ringEquiv α = (equivShrink α).symm.ringEquiv

@[reducible, inline]

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

Transfer Semigroup across an Equiv

Equations

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

@[reducible, inline]

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

Transfer add_semigroup across an Equiv

Equations

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

noncomputable instance Equiv.instSemigroupShrink {α : Type u} [Small.{v, u} α] [Semigroup α] : Semigroup (Shrink.{v, u} α)

Equations

• Equiv.instSemigroupShrink = (equivShrink α).symm.semigroup

noncomputable instance Equiv.instAddSemigroupShrink {α : Type u} [Small.{v, u} α] [AddSemigroup α] : AddSemigroup (Shrink.{v, u} α)

Equations

• Equiv.instAddSemigroupShrink = (equivShrink α).symm.addSemigroup

@[reducible, inline]

abbrev Equiv.semigroupWithZero {α : Type u} {β : Type v} (e : α ≃ β) [SemigroupWithZero β] : SemigroupWithZero α

Transfer SemigroupWithZero across an Equiv

Equations

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

noncomputable instance Equiv.instSemigroupWithZeroShrink {α : Type u} [Small.{v, u} α] [SemigroupWithZero α] : SemigroupWithZero (Shrink.{v, u} α)

Equations

• Equiv.instSemigroupWithZeroShrink = (equivShrink α).symm.semigroupWithZero

@[reducible, inline]

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

Transfer CommSemigroup across an Equiv

Equations

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

@[reducible, inline]

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

Transfer AddCommSemigroup across an Equiv

Equations

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

noncomputable instance Equiv.instCommSemigroupShrink {α : Type u} [Small.{v, u} α] [CommSemigroup α] : CommSemigroup (Shrink.{v, u} α)

Equations

• Equiv.instCommSemigroupShrink = (equivShrink α).symm.commSemigroup

noncomputable instance Equiv.instAddCommSemigroupShrink {α : Type u} [Small.{v, u} α] [AddCommSemigroup α] : AddCommSemigroup (Shrink.{v, u} α)

Equations

• Equiv.instAddCommSemigroupShrink = (equivShrink α).symm.addCommSemigroup

@[reducible, inline]

abbrev Equiv.mulZeroClass {α : Type u} {β : Type v} (e : α ≃ β) [MulZeroClass β] : MulZeroClass α

Transfer MulZeroClass across an Equiv

Equations

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

noncomputable instance Equiv.instMulZeroClassShrink {α : Type u} [Small.{v, u} α] [MulZeroClass α] : MulZeroClass (Shrink.{v, u} α)

Equations

• Equiv.instMulZeroClassShrink = (equivShrink α).symm.mulZeroClass

@[reducible, inline]

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

Transfer MulOneClass across an Equiv

Equations

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

@[reducible, inline]

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

Transfer AddZeroClass across an Equiv

Equations

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

noncomputable instance Equiv.instMulOneClassShrink {α : Type u} [Small.{v, u} α] [MulOneClass α] : MulOneClass (Shrink.{v, u} α)

Equations

• Equiv.instMulOneClassShrink = (equivShrink α).symm.mulOneClass

noncomputable instance Equiv.instAddZeroClassShrink {α : Type u} [Small.{v, u} α] [AddZeroClass α] : AddZeroClass (Shrink.{v, u} α)

Equations

• Equiv.instAddZeroClassShrink = (equivShrink α).symm.addZeroClass

@[reducible, inline]

abbrev Equiv.mulZeroOneClass {α : Type u} {β : Type v} (e : α ≃ β) [MulZeroOneClass β] : MulZeroOneClass α

Transfer MulZeroOneClass across an Equiv

Equations

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

noncomputable instance Equiv.instMulZeroOneClassShrink {α : Type u} [Small.{v, u} α] [MulZeroOneClass α] : MulZeroOneClass (Shrink.{v, u} α)

Equations

• Equiv.instMulZeroOneClassShrink = (equivShrink α).symm.mulZeroOneClass

@[reducible, inline]

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

Transfer Monoid across an Equiv

Equations

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

@[reducible, inline]

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

Transfer AddMonoid across an Equiv

Equations

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

noncomputable instance Equiv.instMonoidShrink {α : Type u} [Small.{v, u} α] [Monoid α] : Monoid (Shrink.{v, u} α)

Equations

• Equiv.instMonoidShrink = (equivShrink α).symm.monoid

noncomputable instance Equiv.instAddMonoidShrink {α : Type u} [Small.{v, u} α] [AddMonoid α] : AddMonoid (Shrink.{v, u} α)

Equations

• Equiv.instAddMonoidShrink = (equivShrink α).symm.addMonoid

@[reducible, inline]

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

Transfer CommMonoid across an Equiv

Equations

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

@[reducible, inline]

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

Transfer AddCommMonoid across an Equiv

Equations

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

noncomputable instance Equiv.instCommMonoidShrink {α : Type u} [Small.{v, u} α] [CommMonoid α] : CommMonoid (Shrink.{v, u} α)

Equations

• Equiv.instCommMonoidShrink = (equivShrink α).symm.commMonoid

noncomputable instance Equiv.instAddCommMonoidShrink {α : Type u} [Small.{v, u} α] [AddCommMonoid α] : AddCommMonoid (Shrink.{v, u} α)

Equations

• Equiv.instAddCommMonoidShrink = (equivShrink α).symm.addCommMonoid

@[reducible, inline]

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

Transfer Group across an Equiv

Equations

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

@[reducible, inline]

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

Transfer AddGroup across an Equiv

Equations

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

noncomputable instance Equiv.instGroupShrink {α : Type u} [Small.{v, u} α] [Group α] : Group (Shrink.{v, u} α)

Equations

• Equiv.instGroupShrink = (equivShrink α).symm.group

noncomputable instance Equiv.instAddGroupShrink {α : Type u} [Small.{v, u} α] [AddGroup α] : AddGroup (Shrink.{v, u} α)

Equations

• Equiv.instAddGroupShrink = (equivShrink α).symm.addGroup

@[reducible, inline]

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

Transfer CommGroup across an Equiv

Equations

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

@[reducible, inline]

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

Transfer AddCommGroup across an Equiv

Equations

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

noncomputable instance Equiv.instCommGroupShrink {α : Type u} [Small.{v, u} α] [CommGroup α] : CommGroup (Shrink.{v, u} α)

Equations

• Equiv.instCommGroupShrink = (equivShrink α).symm.commGroup

noncomputable instance Equiv.instAddCommGroupShrink {α : Type u} [Small.{v, u} α] [AddCommGroup α] : AddCommGroup (Shrink.{v, u} α)

Equations

• Equiv.instAddCommGroupShrink = (equivShrink α).symm.addCommGroup

@[reducible, inline]

abbrev Equiv.nonUnitalNonAssocSemiring {α : Type u} {β : Type v} (e : α ≃ β) [NonUnitalNonAssocSemiring β] : NonUnitalNonAssocSemiring α

Transfer NonUnitalNonAssocSemiring across an Equiv

Equations

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

noncomputable instance Equiv.instNonUnitalNonAssocSemiringShrink {α : Type u} [Small.{v, u} α] [NonUnitalNonAssocSemiring α] : NonUnitalNonAssocSemiring (Shrink.{v, u} α)

Equations

• Equiv.instNonUnitalNonAssocSemiringShrink = (equivShrink α).symm.nonUnitalNonAssocSemiring

@[reducible, inline]

abbrev Equiv.nonUnitalSemiring {α : Type u} {β : Type v} (e : α ≃ β) [NonUnitalSemiring β] : NonUnitalSemiring α

Transfer NonUnitalSemiring across an Equiv

Equations

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

noncomputable instance Equiv.instNonUnitalSemiringShrink {α : Type u} [Small.{v, u} α] [NonUnitalSemiring α] : NonUnitalSemiring (Shrink.{v, u} α)

Equations

• Equiv.instNonUnitalSemiringShrink = (equivShrink α).symm.nonUnitalSemiring

@[reducible, inline]

abbrev Equiv.addMonoidWithOne {α : Type u} {β : Type v} (e : α ≃ β) [AddMonoidWithOne β] : AddMonoidWithOne α

Transfer AddMonoidWithOne across an Equiv

Equations

• e.addMonoidWithOne = AddMonoidWithOne.mk ⋯ ⋯

noncomputable instance Equiv.instAddMonoidWithOneShrink {α : Type u} [Small.{v, u} α] [AddMonoidWithOne α] : AddMonoidWithOne (Shrink.{v, u} α)

Equations

• Equiv.instAddMonoidWithOneShrink = (equivShrink α).symm.addMonoidWithOne

@[reducible, inline]

abbrev Equiv.addGroupWithOne {α : Type u} {β : Type v} (e : α ≃ β) [AddGroupWithOne β] : AddGroupWithOne α

Transfer AddGroupWithOne across an Equiv

Equations

• e.addGroupWithOne = AddGroupWithOne.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable instance Equiv.instAddGroupWithOneShrink {α : Type u} [Small.{v, u} α] [AddGroupWithOne α] : AddGroupWithOne (Shrink.{v, u} α)

Equations

• Equiv.instAddGroupWithOneShrink = (equivShrink α).symm.addGroupWithOne

@[reducible, inline]

abbrev Equiv.nonAssocSemiring {α : Type u} {β : Type v} (e : α ≃ β) [NonAssocSemiring β] : NonAssocSemiring α

Transfer NonAssocSemiring across an Equiv

Equations

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

noncomputable instance Equiv.instNonAssocSemiringShrink {α : Type u} [Small.{v, u} α] [NonAssocSemiring α] : NonAssocSemiring (Shrink.{v, u} α)

Equations

• Equiv.instNonAssocSemiringShrink = (equivShrink α).symm.nonAssocSemiring

@[reducible, inline]

abbrev Equiv.semiring {α : Type u} {β : Type v} (e : α ≃ β) [Semiring β] : Semiring α

Transfer Semiring across an Equiv

Equations

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

noncomputable instance Equiv.instSemiringShrink {α : Type u} [Small.{v, u} α] [Semiring α] : Semiring (Shrink.{v, u} α)

Equations

• Equiv.instSemiringShrink = (equivShrink α).symm.semiring

@[reducible, inline]

abbrev Equiv.nonUnitalCommSemiring {α : Type u} {β : Type v} (e : α ≃ β) [NonUnitalCommSemiring β] : NonUnitalCommSemiring α

Transfer NonUnitalCommSemiring across an Equiv

Equations

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

noncomputable instance Equiv.instNonUnitalCommSemiringShrink {α : Type u} [Small.{v, u} α] [NonUnitalCommSemiring α] : NonUnitalCommSemiring (Shrink.{v, u} α)

Equations

• Equiv.instNonUnitalCommSemiringShrink = (equivShrink α).symm.nonUnitalCommSemiring

@[reducible, inline]

abbrev Equiv.commSemiring {α : Type u} {β : Type v} (e : α ≃ β) [CommSemiring β] : CommSemiring α

Transfer CommSemiring across an Equiv

Equations

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

noncomputable instance Equiv.instCommSemiringShrink {α : Type u} [Small.{v, u} α] [CommSemiring α] : CommSemiring (Shrink.{v, u} α)

Equations

• Equiv.instCommSemiringShrink = (equivShrink α).symm.commSemiring

@[reducible, inline]

abbrev Equiv.nonUnitalNonAssocRing {α : Type u} {β : Type v} (e : α ≃ β) [NonUnitalNonAssocRing β] : NonUnitalNonAssocRing α

Transfer NonUnitalNonAssocRing across an Equiv

Equations

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

noncomputable instance Equiv.instNonUnitalNonAssocRingShrink {α : Type u} [Small.{v, u} α] [NonUnitalNonAssocRing α] : NonUnitalNonAssocRing (Shrink.{v, u} α)

Equations

• Equiv.instNonUnitalNonAssocRingShrink = (equivShrink α).symm.nonUnitalNonAssocRing

@[reducible, inline]

abbrev Equiv.nonUnitalRing {α : Type u} {β : Type v} (e : α ≃ β) [NonUnitalRing β] : NonUnitalRing α

Transfer NonUnitalRing across an Equiv

Equations

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

noncomputable instance Equiv.instNonUnitalRingShrink {α : Type u} [Small.{v, u} α] [NonUnitalRing α] : NonUnitalRing (Shrink.{v, u} α)

Equations

• Equiv.instNonUnitalRingShrink = (equivShrink α).symm.nonUnitalRing

@[reducible, inline]

abbrev Equiv.nonAssocRing {α : Type u} {β : Type v} (e : α ≃ β) [NonAssocRing β] : NonAssocRing α

Transfer NonAssocRing across an Equiv

Equations

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

noncomputable instance Equiv.instNonAssocRingShrink {α : Type u} [Small.{v, u} α] [NonAssocRing α] : NonAssocRing (Shrink.{v, u} α)

Equations

• Equiv.instNonAssocRingShrink = (equivShrink α).symm.nonAssocRing

@[reducible, inline]

abbrev Equiv.ring {α : Type u} {β : Type v} (e : α ≃ β) [Ring β] : Ring α

Transfer Ring across an Equiv

Equations

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

noncomputable instance Equiv.instRingShrink {α : Type u} [Small.{v, u} α] [Ring α] : Ring (Shrink.{v, u} α)

Equations

• Equiv.instRingShrink = (equivShrink α).symm.ring

@[reducible, inline]

abbrev Equiv.nonUnitalCommRing {α : Type u} {β : Type v} (e : α ≃ β) [NonUnitalCommRing β] : NonUnitalCommRing α

Transfer NonUnitalCommRing across an Equiv

Equations

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

noncomputable instance Equiv.instNonUnitalCommRingShrink {α : Type u} [Small.{v, u} α] [NonUnitalCommRing α] : NonUnitalCommRing (Shrink.{v, u} α)

Equations

• Equiv.instNonUnitalCommRingShrink = (equivShrink α).symm.nonUnitalCommRing

@[reducible, inline]

abbrev Equiv.commRing {α : Type u} {β : Type v} (e : α ≃ β) [CommRing β] : CommRing α

Transfer CommRing across an Equiv

Equations

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

noncomputable instance Equiv.instCommRingShrink {α : Type u} [Small.{v, u} α] [CommRing α] : CommRing (Shrink.{v, u} α)

Equations

• Equiv.instCommRingShrink = (equivShrink α).symm.commRing

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

Transfer Nontrivial across an Equiv

instance Equiv.instNontrivialShrink {α : Type u} [Small.{v, u} α] [Nontrivial α] : Nontrivial (Shrink.{v, u} α)

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

Transfer IsDomain across an Equiv

instance Equiv.instIsDomainShrink {α : Type u} [Small.{v, u} α] [Semiring α] [IsDomain α] : IsDomain (Shrink.{v, u} α)

@[reducible, inline]

abbrev Equiv.nnratCast {α : Type u} {β : Type v} (e : α ≃ β) [NNRatCast β] : NNRatCast α

Transfer NNRatCast across an Equiv

Equations

• e.nnratCast = { nnratCast := fun (q : ℚ≥0) => e.symm ↑q }

@[reducible, inline]

abbrev Equiv.ratCast {α : Type u} {β : Type v} (e : α ≃ β) [RatCast β] : RatCast α

Transfer RatCast across an Equiv

Equations

• e.ratCast = { ratCast := fun (n : ℚ) => e.symm ↑n }

noncomputable instance Shrink.instNNRatCast {α : Type u} [Small.{v, u} α] [NNRatCast α] : NNRatCast (Shrink.{v, u} α)

Equations

• Shrink.instNNRatCast = (equivShrink α).symm.nnratCast

noncomputable instance Shrink.instRatCast {α : Type u} [Small.{v, u} α] [RatCast α] : RatCast (Shrink.{v, u} α)

Equations

• Shrink.instRatCast = (equivShrink α).symm.ratCast

@[reducible, inline]

abbrev Equiv.divisionRing {α : Type u} {β : Type v} (e : α ≃ β) [DivisionRing β] : DivisionRing α

Transfer DivisionRing across an Equiv

Equations

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

noncomputable instance Equiv.instDivisionRingShrink {α : Type u} [Small.{v, u} α] [DivisionRing α] : DivisionRing (Shrink.{v, u} α)

Equations

• Equiv.instDivisionRingShrink = (equivShrink α).symm.divisionRing

@[reducible, inline]

abbrev Equiv.field {α : Type u} {β : Type v} (e : α ≃ β) [Field β] : Field α

Transfer Field across an Equiv

Equations

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

noncomputable instance Equiv.instFieldShrink {α : Type u} [Small.{v, u} α] [Field α] : Field (Shrink.{v, u} α)

Equations

• Equiv.instFieldShrink = (equivShrink α).symm.field

@[reducible, inline]

abbrev Equiv.mulAction {α : Type u} {β : Type v} (R : Type u_1) [Monoid R] (e : α ≃ β) [MulAction R β] : MulAction R α

Transfer MulAction across an Equiv

Equations

• Equiv.mulAction R e = MulAction.mk ⋯ ⋯

noncomputable instance Equiv.instMulActionShrink {α : Type u} (R : Type u_1) [Monoid R] [Small.{v, u} α] [MulAction R α] : MulAction R (Shrink.{v, u} α)

Equations

• Equiv.instMulActionShrink R = Equiv.mulAction R (equivShrink α).symm

@[reducible, inline]

abbrev Equiv.distribMulAction {α : Type u} {β : Type v} (R : Type u_1) [Monoid R] (e : α ≃ β) [AddCommMonoid β] [DistribMulAction R β] : DistribMulAction R α

Transfer DistribMulAction across an Equiv

Equations

• Equiv.distribMulAction R e = DistribMulAction.mk ⋯ ⋯

noncomputable instance Equiv.instDistribMulActionShrink {α : Type u} (R : Type u_1) [Monoid R] [Small.{v, u} α] [AddCommMonoid α] [DistribMulAction R α] : DistribMulAction R (Shrink.{v, u} α)

Equations

• Equiv.instDistribMulActionShrink R = Equiv.distribMulAction R (equivShrink α).symm

@[reducible, inline]

abbrev Equiv.module {α : Type u} {β : Type v} (R : Type u_1) [Semiring R] (e : α ≃ β) [AddCommMonoid β] : let x := e.addCommMonoid; [inst : Module R β] → Module R α

Transfer Module across an Equiv

Equations

• @Equiv.module α β R inst✝¹ e inst✝ = fun [Module R β] => let __src := Equiv.distribMulAction R e; Module.mk ⋯ ⋯

noncomputable instance Equiv.instModuleShrink {α : Type u} (R : Type u_1) [Semiring R] [Small.{v, u} α] [AddCommMonoid α] [Module R α] : Module R (Shrink.{v, u} α)

Equations

• Equiv.instModuleShrink R = Equiv.module R (equivShrink α).symm

def Equiv.linearEquiv {α : Type u} {β : Type v} (R : Type u_1) [Semiring R] (e : α ≃ β) [AddCommMonoid β] [Module R β] : let addCommMonoid := e.addCommMonoid; let module := Equiv.module R e; α ≃ₗ[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.linearEquiv R e = { toFun := e.addEquiv.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := e.addEquiv.invFun, left_inv := ⋯, right_inv := ⋯ }

noncomputable def Shrink.linearEquiv (α : Type u) (R : Type u_1) [Semiring R] [Small.{v, u} α] [AddCommMonoid α] [Module R α] : Shrink.{v, u} α ≃ₗ[R] α

Shrink α to a smaller universe preserves module structure.

Equations

• Shrink.linearEquiv α R = Equiv.linearEquiv R (equivShrink α).symm

@[simp]

theorem Shrink.linearEquiv_apply (α : Type u) (R : Type u_1) [Semiring R] [Small.{v, u} α] [AddCommMonoid α] [Module R α] (a✝ : Shrink.{v, u} α) : (linearEquiv α R) a✝ = (equivShrink α).symm a✝

@[simp]

theorem Shrink.linearEquiv_symm_apply (α : Type u) (R : Type u_1) [Semiring R] [Small.{v, u} α] [AddCommMonoid α] [Module R α] (a✝ : α) : (linearEquiv α R).symm a✝ = (AddEquiv.symm (equivShrink α).symm.addEquiv) a✝

@[reducible, inline]

abbrev Equiv.algebra {α : Type u} {β : Type v} (R : Type u_1) [CommSemiring R] (e : α ≃ β) [Semiring β] : let x := e.semiring; [inst : Algebra R β] → Algebra R α

Transfer Algebra across an Equiv

Equations

• @Equiv.algebra α β R inst✝¹ e inst✝ = fun [Algebra R β] => Algebra.ofModule ⋯ ⋯

theorem Equiv.algebraMap_def {α : Type u} {β : Type v} (R : Type u_1) [CommSemiring R] (e : α ≃ β) [Semiring β] [Algebra R β] (r : R) : (algebraMap R α) r = e.symm ((algebraMap R β) r)

noncomputable instance Equiv.instAlgebraShrink {α : Type u} (R : Type u_1) [CommSemiring R] [Small.{v, u} α] [Semiring α] [Algebra R α] : Algebra R (Shrink.{v, u} α)

Equations

• Equiv.instAlgebraShrink R = Equiv.algebra R (equivShrink α).symm

def Equiv.algEquiv {α : Type u} {β : Type v} (R : Type u_1) [CommSemiring R] (e : α ≃ β) [Semiring β] [Algebra R β] : let semiring := e.semiring; let algebra := Equiv.algebra R e; α ≃ₐ[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.algEquiv R e = { toEquiv := e.ringEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem Equiv.algEquiv_apply {α : Type u} {β : Type v} (R : Type u_1) [CommSemiring R] (e : α ≃ β) [Semiring β] [Algebra R β] (a : α) : (algEquiv R e) a = e a

theorem Equiv.algEquiv_symm_apply {α : Type u} {β : Type v} (R : Type u_1) [CommSemiring R] (e : α ≃ β) [Semiring β] [Algebra R β] (b : β) : (AlgEquiv.symm (algEquiv R e)) b = e.symm b

noncomputable def Shrink.algEquiv (α : Type u) (R : Type u_1) [CommSemiring R] [Small.{v, u} α] [Semiring α] [Algebra R α] : Shrink.{v, u} α ≃ₐ[R] α

Shrink α to a smaller universe preserves algebra structure.

Equations

• Shrink.algEquiv α R = Equiv.algEquiv R (equivShrink α).symm

@[simp]

theorem Shrink.algEquiv_symm_apply (α : Type u) (R : Type u_1) [CommSemiring R] [Small.{v, u} α] [Semiring α] [Algebra R α] (a✝ : α) : (algEquiv α R).symm a✝ = (equivShrink α) a✝

@[simp]

theorem Shrink.algEquiv_apply (α : Type u) (R : Type u_1) [CommSemiring R] [Small.{v, u} α] [Semiring α] [Algebra R α] (a✝ : Shrink.{v, u} α) : (algEquiv α R) a✝ = (equivShrink α).symm a✝

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.

@[reducible, inline]

abbrev AddEquiv.module {α : Type u} {β : Type v} (A : Type u_2) [Semiring A] [AddCommMonoid α] [AddCommMonoid β] [Module A β] (e : α ≃+ β) : Module A α

Transport a module instance via an isomorphism of the underlying abelian groups. This has better definitional properties than Equiv.module since here the abelian group structure remains unmodified.

Equations

• AddEquiv.module A e = Module.mk ⋯ ⋯

theorem LinearEquiv.isScalarTower {α : Type u} {β : Type v} {R : Type u_1} [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] [AddCommMonoid α] [AddCommMonoid β] [Module A β] [Module R α] [Module R β] [IsScalarTower R A β] (e : α ≃ₗ[R] β) : IsScalarTower R A α

The module instance from AddEquiv.module is compatible with the R-module structures, if the AddEquiv is induced by an R-module isomorphism.