Transfer algebraic structures across Equivs

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

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

@[reducible, inline]

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

Transfer SemigroupWithZero across an Equiv

Equations

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

@[reducible, inline]

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

Transfer MulZeroClass across an Equiv

Equations

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

@[reducible, inline]

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

Transfer MulZeroOneClass across an Equiv

Equations

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

@[reducible, inline]

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

Transfer NonUnitalNonAssocSemiring across an Equiv

Equations

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

@[reducible, inline]

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

Transfer NonUnitalSemiring across an Equiv

Equations

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

@[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 := ⋯ }

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

@[reducible, inline]

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

Transfer NonAssocSemiring across an Equiv

Equations

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

@[reducible, inline]

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

Transfer Semiring across an Equiv

Equations

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

@[reducible, inline]

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

Transfer NonUnitalCommSemiring across an Equiv

Equations

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

@[reducible, inline]

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

Transfer CommSemiring across an Equiv

Equations

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

@[reducible, inline]

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

Transfer NonUnitalNonAssocRing across an Equiv

Equations

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

@[reducible, inline]

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

Transfer NonUnitalRing across an Equiv

Equations

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

@[reducible, inline]

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

Transfer NonAssocRing across an Equiv

Equations

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

@[reducible, inline]

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

Transfer Ring across an Equiv

Equations

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

@[reducible, inline]

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

Transfer NonUnitalCommRing across an Equiv

Equations

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

@[reducible, inline]

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

Transfer CommRing across an Equiv

Equations

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

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

Transfer IsDomain across an Equiv

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

@[reducible, inline]

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

Transfer DivisionRing across an Equiv

Equations

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

@[reducible, inline]

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

Transfer Field across an Equiv

Equations

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

@[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 := ⋯ }

@[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 := ⋯ }

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 := ⋯ }

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

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

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