Transfer algebraic structures across Equivs

This continues the pattern set in Mathlib/Algebra/Group/TransferInstance.lean.

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

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

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

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

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

Equations

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

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

Equations

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

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 β] : have add := e.add; have 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

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

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

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

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

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

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

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 = { natCast := fun (n : ℕ) => e.symm ↑n, toAddMonoid := e.addMonoid, toOne := e.one, natCast_zero := ⋯, natCast_succ := ⋯ }

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

• One or more equations did not get rendered due to their size.

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

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

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 = { toMulAction := Equiv.mulAction R e, smul_zero := ⋯, smul_add := ⋯ }

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 β] : have x := e.addCommMonoid; [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; { toDistribMulAction := __src, add_smul := ⋯, zero_smul := ⋯ }

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; have 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 β] : have x := e.semiring; [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; have 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✝

@[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 = { toSMul := Equiv.smul A e.toEquiv, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

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.