Transfer algebraic structures across Equivs

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

@[reducible, inline]

abbrev Equiv.algebra (R : Type u_1) {α : Type u_2} {β : Type u_3} [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 {R : Type u_1} {α : Type u_2} {β : Type u_3} [CommSemiring R] (e : α ≃ β) [Semiring β] [Algebra R β] (r : R) : (algebraMap R α) r = e.symm ((algebraMap R β) r)

def Equiv.algEquiv (R : Type u_1) {α : Type u_2} {β : Type u_3} [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 {R : Type u_1} {α : Type u_2} {β : Type u_3} [CommSemiring R] (e : α ≃ β) [Semiring β] [Algebra R β] (a : α) : (algEquiv R e) a = e a

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