Isomorphisms of R-algebras

This file defines bundled isomorphisms of R-algebras.

Main definitions

• AlgEquiv R A B: the type of R-algebra isomorphisms between A and B.

Notations

• A ≃ₐ[R] B : R-algebra equivalence from A to B.

structure AlgEquiv (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] extends Equiv : Type (max v w)

• toFun : A → B
• invFun : B → A
• left_inv : Function.LeftInverse s.invFun s.toFun
• right_inv : Function.RightInverse s.invFun s.toFun
• map_mul' : ∀ (x y : A), Equiv.toFun s.toEquiv (x * y) = Equiv.toFun s.toEquiv x * Equiv.toFun s.toEquiv y

  The proposition that the function preserves multiplication

• map_add' : ∀ (x y : A), Equiv.toFun s.toEquiv (x + y) = Equiv.toFun s.toEquiv x + Equiv.toFun s.toEquiv y

  The proposition that the function preserves addition

• commutes' : ∀ (r : R), Equiv.toFun s.toEquiv (↑(algebraMap R A) r) = ↑(algebraMap R B) r

  An equivalence of algebras commutes with the action of scalars.

An equivalence of algebras is an equivalence of rings commuting with the actions of scalars.

def «term_≃ₐ[_]_» : Lean.TrailingParserDescr

An equivalence of algebras is an equivalence of rings commuting with the actions of scalars.

class AlgEquivClass (F : Type u_1) (R : outParam (Type u_2)) (A : outParam (Type u_3)) (B : outParam (Type u_4)) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] extends RingEquivClass : Type (max (max u_1 u_3) u_4)

• coe : F → A → B
• inv : F → B → A
• left_inv : ∀ (e : F), Function.LeftInverse (EquivLike.inv e) (EquivLike.coe e)
• right_inv : ∀ (e : F), Function.RightInverse (EquivLike.inv e) (EquivLike.coe e)
• coe_injective' : ∀ (e g : F), EquivLike.coe e = EquivLike.coe g → EquivLike.inv e = EquivLike.inv g → e = g
• map_mul : ∀ (f : F) (a b : A), ↑f (a * b) = ↑f a * ↑f b
• map_add : ∀ (f : F) (a b : A), ↑f (a + b) = ↑f a + ↑f b
• commutes : ∀ (f : F) (r : R), ↑f (↑(algebraMap R A) r) = ↑(algebraMap R B) r

  An equivalence of algebras commutes with the action of scalars.

AlgEquivClass F R A B states that F is a type of algebra structure preserving equivalences. You should extend this class when you extend AlgEquiv.

instance AlgEquivClass.toAlgHomClass (F : Type u_1) (R : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [h : AlgEquivClass F R A B] : AlgHomClass F R A B

instance AlgEquivClass.toLinearEquivClass (F : Type u_1) (R : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [h : AlgEquivClass F R A B] : LinearEquivClass F R A B

def AlgEquivClass.toAlgEquiv {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AlgEquivClass F R A B] (f : F) : A ≃ₐ[R] B

Turn an element of a type F satisfying AlgEquivClass F R A B into an actual AlgEquiv. This is declared as the default coercion from F to A ≃ₐ[R] B.

instance AlgEquivClass.instCoeTCAlgEquiv (F : Type u_1) (R : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AlgEquivClass F R A B] : CoeTC F (A ≃ₐ[R] B)

instance AlgEquiv.instAlgEquivClassAlgEquiv {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] : AlgEquivClass (A₁ ≃ₐ[R] A₂) R A₁ A₂

instance AlgEquiv.instEquivLikeAlgEquiv {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] : EquivLike (A₁ ≃ₐ[R] A₂) A₁ A₂

def AlgEquiv.Simps.apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : A₁ → A₂

See Note [custom simps projection]

def AlgEquiv.Simps.toEquiv {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : A₁ ≃ A₂

See Note [custom simps projection]

@[simp]

theorem AlgEquiv.coe_coe {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {F : Type u_1} [AlgEquivClass F R A₁ A₂] (f : F) : ↑↑f = ↑f

theorem AlgEquiv.ext {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {f : A₁ ≃ₐ[R] A₂} {g : A₁ ≃ₐ[R] A₂} (h : ∀ (a : A₁), ↑f a = ↑g a) : f = g

theorem AlgEquiv.congr_arg {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {f : A₁ ≃ₐ[R] A₂} {x : A₁} {x' : A₁} : x = x' → ↑f x = ↑f x'

theorem AlgEquiv.congr_fun {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {f : A₁ ≃ₐ[R] A₂} {g : A₁ ≃ₐ[R] A₂} (h : f = g) (x : A₁) : ↑f x = ↑g x

theorem AlgEquiv.ext_iff {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {f : A₁ ≃ₐ[R] A₂} {g : A₁ ≃ₐ[R] A₂} : f = g ↔ ∀ (x : A₁), ↑f x = ↑g x

theorem AlgEquiv.coe_fun_injective {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] : Function.Injective fun e => ↑e

instance AlgEquiv.hasCoeToRingEquiv {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] : CoeOut (A₁ ≃ₐ[R] A₂) (A₁ ≃+* A₂)

@[simp]

theorem AlgEquiv.coe_mk {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {toFun : A₁ → A₂} {invFun : A₂ → A₁} {left_inv : Function.LeftInverse invFun toFun} {right_inv : Function.RightInverse invFun toFun} {map_mul : ∀ (x y : A₁), Equiv.toFun { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv } (x * y) = Equiv.toFun { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv } x * Equiv.toFun { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv } y} {map_add : ∀ (x y : A₁), Equiv.toFun { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv } (x + y) = Equiv.toFun { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv } x + Equiv.toFun { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv } y} {commutes : ∀ (r : R), Equiv.toFun { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv } (↑(algebraMap R A₁) r) = ↑(algebraMap R A₂) r} : ↑{ toEquiv := { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv }, map_mul' := map_mul, map_add' := map_add, commutes' := commutes } = toFun

@[simp]

theorem AlgEquiv.mk_coe {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (e' : A₂ → A₁) (h₁ : Function.LeftInverse e' ↑e) (h₂ : Function.RightInverse e' ↑e) (h₃ : ∀ (x y : A₁), Equiv.toFun { toFun := ↑e, invFun := e', left_inv := h₁, right_inv := h₂ } (x * y) = Equiv.toFun { toFun := ↑e, invFun := e', left_inv := h₁, right_inv := h₂ } x * Equiv.toFun { toFun := ↑e, invFun := e', left_inv := h₁, right_inv := h₂ } y) (h₄ : ∀ (x y : A₁), Equiv.toFun { toFun := ↑e, invFun := e', left_inv := h₁, right_inv := h₂ } (x + y) = Equiv.toFun { toFun := ↑e, invFun := e', left_inv := h₁, right_inv := h₂ } x + Equiv.toFun { toFun := ↑e, invFun := e', left_inv := h₁, right_inv := h₂ } y) (h₅ : ∀ (r : R), Equiv.toFun { toFun := ↑e, invFun := e', left_inv := h₁, right_inv := h₂ } (↑(algebraMap R A₁) r) = ↑(algebraMap R A₂) r) : { toEquiv := { toFun := ↑e, invFun := e', left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄, commutes' := h₅ } = e

@[simp]

theorem AlgEquiv.toEquiv_eq_coe {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : e.toEquiv = ↑e

@[simp]

theorem AlgEquiv.toRingEquiv_eq_coe {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : AlgEquiv.toRingEquiv e = ↑e

@[simp]

theorem AlgEquiv.coe_ringEquiv {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : ↑↑e = ↑e

theorem AlgEquiv.coe_ringEquiv' {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : ↑(AlgEquiv.toRingEquiv e) = ↑e

theorem AlgEquiv.coe_ringEquiv_injective {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] : Function.Injective RingEquivClass.toRingEquiv

theorem AlgEquiv.map_add {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₁) (y : A₁) : ↑e (x + y) = ↑e x + ↑e y

theorem AlgEquiv.map_zero {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : ↑e 0 = 0

theorem AlgEquiv.map_mul {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₁) (y : A₁) : ↑e (x * y) = ↑e x * ↑e y

theorem AlgEquiv.map_one {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : ↑e 1 = 1

@[simp]

theorem AlgEquiv.commutes {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (r : R) : ↑e (↑(algebraMap R A₁) r) = ↑(algebraMap R A₂) r

theorem AlgEquiv.map_smul {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (r : R) (x : A₁) : ↑e (r • x) = r • ↑e x

theorem AlgEquiv.map_sum {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) {ι : Type u_1} (f : ι → A₁) (s : Finset ι) : ↑e (Finset.sum s fun x => f x) = Finset.sum s fun x => ↑e (f x)

theorem AlgEquiv.map_finsupp_sum {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) {α : Type u_1} [Zero α] {ι : Type u_2} (f : ι →₀ α) (g : ι → α → A₁) : ↑e (Finsupp.sum f g) = Finsupp.sum f fun i b => ↑e (g i b)

def AlgEquiv.toAlgHom {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : A₁ →ₐ[R] A₂

Interpret an algebra equivalence as an algebra homomorphism.

This definition is included for symmetry with the other to*Hom projections. The simp normal form is to use the coercion of the AlgHomClass.coeTC instance.

@[simp]

theorem AlgEquiv.toAlgHom_eq_coe {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : ↑e = ↑e

@[simp]

theorem AlgEquiv.coe_algHom {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : ↑↑e = ↑e

theorem AlgEquiv.coe_algHom_injective {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] : Function.Injective AlgHomClass.toAlgHom

theorem AlgEquiv.coe_ringHom_commutes {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : ↑↑e = ↑↑e

The two paths coercion can take to a RingHom are equivalent

theorem AlgEquiv.map_pow {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₁) (n : ℕ) : ↑e (x ^ n) = ↑e x ^ n

theorem AlgEquiv.injective {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : Function.Injective ↑e

theorem AlgEquiv.surjective {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : Function.Surjective ↑e

theorem AlgEquiv.bijective {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : Function.Bijective ↑e

def AlgEquiv.refl {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] : A₁ ≃ₐ[R] A₁

Algebra equivalences are reflexive.

instance AlgEquiv.instInhabitedAlgEquiv {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] : Inhabited (A₁ ≃ₐ[R] A₁)

@[simp]

theorem AlgEquiv.refl_toAlgHom {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] : ↑AlgEquiv.refl = AlgHom.id R A₁

@[simp]

theorem AlgEquiv.coe_refl {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] : ↑AlgEquiv.refl = id

def AlgEquiv.symm {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : A₂ ≃ₐ[R] A₁

Algebra equivalences are symmetric.

def AlgEquiv.Simps.symm_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : A₂ → A₁

See Note [custom simps projection]

theorem AlgEquiv.coe_apply_coe_coe_symm_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {F : Type u_1} [AlgEquivClass F R A₁ A₂] (f : F) (x : A₂) : ↑f (↑(AlgEquiv.symm ↑f) x) = x

theorem AlgEquiv.coe_coe_symm_apply_coe_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {F : Type u_1} [AlgEquivClass F R A₁ A₂] (f : F) (x : A₁) : ↑(AlgEquiv.symm ↑f) (↑f x) = x

@[simp]

theorem AlgEquiv.symm_toEquiv_eq_symm {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {e : A₁ ≃ₐ[R] A₂} : (↑e).symm = ↑(AlgEquiv.symm e)

theorem AlgEquiv.invFun_eq_symm {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {e : A₁ ≃ₐ[R] A₂} : e.invFun = ↑(AlgEquiv.symm e)

@[simp]

theorem AlgEquiv.symm_symm {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : AlgEquiv.symm (AlgEquiv.symm e) = e

theorem AlgEquiv.symm_bijective {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] : Function.Bijective AlgEquiv.symm

@[simp]

theorem AlgEquiv.mk_coe' {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (f : A₂ → A₁) (h₁ : Function.LeftInverse (↑e) f) (h₂ : Function.RightInverse (↑e) f) (h₃ : ∀ (x y : A₂), Equiv.toFun { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ } (x * y) = Equiv.toFun { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ } x * Equiv.toFun { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ } y) (h₄ : ∀ (x y : A₂), Equiv.toFun { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ } (x + y) = Equiv.toFun { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ } x + Equiv.toFun { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ } y) (h₅ : ∀ (r : R), Equiv.toFun { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ } (↑(algebraMap R A₂) r) = ↑(algebraMap R A₁) r) : { toEquiv := { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄, commutes' := h₅ } = AlgEquiv.symm e

@[simp]

theorem AlgEquiv.symm_mk {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (f : A₁ → A₂) (f' : A₂ → A₁) (h₁ : Function.LeftInverse f' f) (h₂ : Function.RightInverse f' f) (h₃ : ∀ (x y : A₁), Equiv.toFun { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ } (x * y) = Equiv.toFun { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ } x * Equiv.toFun { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ } y) (h₄ : ∀ (x y : A₁), Equiv.toFun { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ } (x + y) = Equiv.toFun { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ } x + Equiv.toFun { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ } y) (h₅ : ∀ (r : R), Equiv.toFun { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ } (↑(algebraMap R A₁) r) = ↑(algebraMap R A₂) r) : AlgEquiv.symm { toEquiv := { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄, commutes' := h₅ } = let src := AlgEquiv.symm { toEquiv := { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄, commutes' := h₅ }; { toEquiv := { toFun := f', invFun := f, left_inv := (_ : Function.LeftInverse src.invFun src.toFun), right_inv := (_ : Function.RightInverse src.invFun src.toFun) }, map_mul' := (_ : ∀ (x y : A₂), Equiv.toFun src.toEquiv (x * y) = Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y), map_add' := (_ : ∀ (x y : A₂), Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y), commutes' := (_ : ∀ (r : R), Equiv.toFun src.toEquiv (↑(algebraMap R A₂) r) = ↑(algebraMap R A₁) r) }

@[simp]

theorem AlgEquiv.refl_symm {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] : AlgEquiv.symm AlgEquiv.refl = AlgEquiv.refl

theorem AlgEquiv.toRingEquiv_symm {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] (f : A₁ ≃ₐ[R] A₁) : RingEquiv.symm ↑f = ↑(AlgEquiv.symm f)

@[simp]

theorem AlgEquiv.symm_toRingEquiv {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : ↑(AlgEquiv.symm e) = RingEquiv.symm ↑e

def AlgEquiv.trans {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring A₃] [Algebra R A₁] [Algebra R A₂] [Algebra R A₃] (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) : A₁ ≃ₐ[R] A₃

Algebra equivalences are transitive.

@[simp]

theorem AlgEquiv.apply_symm_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₂) : ↑e (↑(AlgEquiv.symm e) x) = x

@[simp]

theorem AlgEquiv.symm_apply_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₁) : ↑(AlgEquiv.symm e) (↑e x) = x

@[simp]

theorem AlgEquiv.symm_trans_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring A₃] [Algebra R A₁] [Algebra R A₂] [Algebra R A₃] (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) (x : A₃) : ↑(AlgEquiv.symm (AlgEquiv.trans e₁ e₂)) x = ↑(AlgEquiv.symm e₁) (↑(AlgEquiv.symm e₂) x)

@[simp]

theorem AlgEquiv.coe_trans {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring A₃] [Algebra R A₁] [Algebra R A₂] [Algebra R A₃] (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) : ↑(AlgEquiv.trans e₁ e₂) = ↑e₂ ∘ ↑e₁

@[simp]

theorem AlgEquiv.trans_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring A₃] [Algebra R A₁] [Algebra R A₂] [Algebra R A₃] (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) (x : A₁) : ↑(AlgEquiv.trans e₁ e₂) x = ↑e₂ (↑e₁ x)

@[simp]

theorem AlgEquiv.comp_symm {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : AlgHom.comp ↑e ↑(AlgEquiv.symm e) = AlgHom.id R A₂

@[simp]

theorem AlgEquiv.symm_comp {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : AlgHom.comp ↑(AlgEquiv.symm e) ↑e = AlgHom.id R A₁

theorem AlgEquiv.leftInverse_symm {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : Function.LeftInverse ↑(AlgEquiv.symm e) ↑e

theorem AlgEquiv.rightInverse_symm {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : Function.RightInverse ↑(AlgEquiv.symm e) ↑e

@[simp]

theorem AlgEquiv.arrowCongr_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₁' : Type uA₁'} {A₂' : Type uA₂'} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring A₁'] [Semiring A₂'] [Algebra R A₁] [Algebra R A₂] [Algebra R A₁'] [Algebra R A₂'] (e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂') (f : A₁ →ₐ[R] A₂) : ↑(AlgEquiv.arrowCongr e₁ e₂) f = AlgHom.comp (AlgHom.comp (↑e₂) f) ↑(AlgEquiv.symm e₁)

def AlgEquiv.arrowCongr {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₁' : Type uA₁'} {A₂' : Type uA₂'} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring A₁'] [Semiring A₂'] [Algebra R A₁] [Algebra R A₂] [Algebra R A₁'] [Algebra R A₂'] (e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂') : (A₁ →ₐ[R] A₂) ≃ (A₁' →ₐ[R] A₂')

If A₁ is equivalent to A₁' and A₂ is equivalent to A₂', then the type of maps A₁ →ₐ[R] A₂ is equivalent to the type of maps A₁' →ₐ[R] A₂'.

theorem AlgEquiv.arrowCongr_comp {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃} {A₁' : Type uA₁'} {A₂' : Type uA₂'} {A₃' : Type uA₃'} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring A₃] [Semiring A₁'] [Semiring A₂'] [Semiring A₃'] [Algebra R A₁] [Algebra R A₂] [Algebra R A₃] [Algebra R A₁'] [Algebra R A₂'] [Algebra R A₃'] (e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂') (e₃ : A₃ ≃ₐ[R] A₃') (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₃) : ↑(AlgEquiv.arrowCongr e₁ e₃) (AlgHom.comp g f) = AlgHom.comp (↑(AlgEquiv.arrowCongr e₂ e₃) g) (↑(AlgEquiv.arrowCongr e₁ e₂) f)

@[simp]

theorem AlgEquiv.arrowCongr_refl {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] : AlgEquiv.arrowCongr AlgEquiv.refl AlgEquiv.refl = Equiv.refl (A₁ →ₐ[R] A₂)

@[simp]

theorem AlgEquiv.arrowCongr_trans {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃} {A₁' : Type uA₁'} {A₂' : Type uA₂'} {A₃' : Type uA₃'} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring A₃] [Semiring A₁'] [Semiring A₂'] [Semiring A₃'] [Algebra R A₁] [Algebra R A₂] [Algebra R A₃] [Algebra R A₁'] [Algebra R A₂'] [Algebra R A₃'] (e₁ : A₁ ≃ₐ[R] A₂) (e₁' : A₁' ≃ₐ[R] A₂') (e₂ : A₂ ≃ₐ[R] A₃) (e₂' : A₂' ≃ₐ[R] A₃') : AlgEquiv.arrowCongr (AlgEquiv.trans e₁ e₂) (AlgEquiv.trans e₁' e₂') = (AlgEquiv.arrowCongr e₁ e₁').trans (AlgEquiv.arrowCongr e₂ e₂')

@[simp]

theorem AlgEquiv.arrowCongr_symm {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₁' : Type uA₁'} {A₂' : Type uA₂'} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring A₁'] [Semiring A₂'] [Algebra R A₁] [Algebra R A₂] [Algebra R A₁'] [Algebra R A₂'] (e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂') : (AlgEquiv.arrowCongr e₁ e₂).symm = AlgEquiv.arrowCongr (AlgEquiv.symm e₁) (AlgEquiv.symm e₂)

@[simp]

theorem AlgEquiv.equivCongr_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₁' : Type uA₁'} {A₂' : Type uA₂'} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring A₁'] [Semiring A₂'] [Algebra R A₁] [Algebra R A₂] [Algebra R A₁'] [Algebra R A₂'] (e : A₁ ≃ₐ[R] A₂) (e' : A₁' ≃ₐ[R] A₂') (ψ : A₁ ≃ₐ[R] A₁') : ↑(AlgEquiv.equivCongr e e') ψ = AlgEquiv.trans (AlgEquiv.symm e) (AlgEquiv.trans ψ e')

def AlgEquiv.equivCongr {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₁' : Type uA₁'} {A₂' : Type uA₂'} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring A₁'] [Semiring A₂'] [Algebra R A₁] [Algebra R A₂] [Algebra R A₁'] [Algebra R A₂'] (e : A₁ ≃ₐ[R] A₂) (e' : A₁' ≃ₐ[R] A₂') : (A₁ ≃ₐ[R] A₁') ≃ A₂ ≃ₐ[R] A₂'

If A₁ is equivalent to A₂ and A₁' is equivalent to A₂', then the type of maps A₁ ≃ₐ[R] A₁' is equivalent to the type of maps A₂ ≃ ₐ[R] A₂'.

This is the AlgEquiv version of AlgEquiv.arrowCongr.

@[simp]

theorem AlgEquiv.equivCongr_refl {R : Type uR} {A₁ : Type uA₁} {A₁' : Type uA₁'} [CommSemiring R] [Semiring A₁] [Semiring A₁'] [Algebra R A₁] [Algebra R A₁'] : AlgEquiv.equivCongr AlgEquiv.refl AlgEquiv.refl = Equiv.refl (A₁ ≃ₐ[R] A₁')

@[simp]

theorem AlgEquiv.equivCongr_symm {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₁' : Type uA₁'} {A₂' : Type uA₂'} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring A₁'] [Semiring A₂'] [Algebra R A₁] [Algebra R A₂] [Algebra R A₁'] [Algebra R A₂'] (e : A₁ ≃ₐ[R] A₂) (e' : A₁' ≃ₐ[R] A₂') : (AlgEquiv.equivCongr e e').symm = AlgEquiv.equivCongr (AlgEquiv.symm e) (AlgEquiv.symm e')

@[simp]

theorem AlgEquiv.equivCongr_trans {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃} {A₁' : Type uA₁'} {A₂' : Type uA₂'} {A₃' : Type uA₃'} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring A₃] [Semiring A₁'] [Semiring A₂'] [Semiring A₃'] [Algebra R A₁] [Algebra R A₂] [Algebra R A₃] [Algebra R A₁'] [Algebra R A₂'] [Algebra R A₃'] (e₁₂ : A₁ ≃ₐ[R] A₂) (e₁₂' : A₁' ≃ₐ[R] A₂') (e₂₃ : A₂ ≃ₐ[R] A₃) (e₂₃' : A₂' ≃ₐ[R] A₃') : (AlgEquiv.equivCongr e₁₂ e₁₂').trans (AlgEquiv.equivCongr e₂₃ e₂₃') = AlgEquiv.equivCongr (AlgEquiv.trans e₁₂ e₂₃) (AlgEquiv.trans e₁₂' e₂₃')

def AlgEquiv.ofAlgHom {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : AlgHom.comp f g = AlgHom.id R A₂) (h₂ : AlgHom.comp g f = AlgHom.id R A₁) : A₁ ≃ₐ[R] A₂

If an algebra morphism has an inverse, it is an algebra isomorphism.

theorem AlgEquiv.coe_algHom_ofAlgHom {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : AlgHom.comp f g = AlgHom.id R A₂) (h₂ : AlgHom.comp g f = AlgHom.id R A₁) : ↑(AlgEquiv.ofAlgHom f g h₁ h₂) = f

@[simp]

theorem AlgEquiv.ofAlgHom_coe_algHom {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (f : A₁ ≃ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : AlgHom.comp (↑f) g = AlgHom.id R A₂) (h₂ : AlgHom.comp g ↑f = AlgHom.id R A₁) : AlgEquiv.ofAlgHom (↑f) g h₁ h₂ = f

theorem AlgEquiv.ofAlgHom_symm {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : AlgHom.comp f g = AlgHom.id R A₂) (h₂ : AlgHom.comp g f = AlgHom.id R A₁) : AlgEquiv.symm (AlgEquiv.ofAlgHom f g h₁ h₂) = AlgEquiv.ofAlgHom g f h₂ h₁

noncomputable def AlgEquiv.ofBijective {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (f : A₁ →ₐ[R] A₂) (hf : Function.Bijective ↑f) : A₁ ≃ₐ[R] A₂

Promotes a bijective algebra homomorphism to an algebra equivalence.

@[simp]

theorem AlgEquiv.coe_ofBijective {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {f : A₁ →ₐ[R] A₂} {hf : Function.Bijective ↑f} : ↑(AlgEquiv.ofBijective f hf) = ↑f

theorem AlgEquiv.ofBijective_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {f : A₁ →ₐ[R] A₂} {hf : Function.Bijective ↑f} (a : A₁) : ↑(AlgEquiv.ofBijective f hf) a = ↑f a

@[simp]

theorem AlgEquiv.toLinearEquiv_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (a : A₁) : ↑(AlgEquiv.toLinearEquiv e) a = ↑e a

def AlgEquiv.toLinearEquiv {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : A₁ ≃ₗ[R] A₂

Forgetting the multiplicative structures, an equivalence of algebras is a linear equivalence.

@[simp]

theorem AlgEquiv.toLinearEquiv_refl {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] : AlgEquiv.toLinearEquiv AlgEquiv.refl = LinearEquiv.refl R A₁

@[simp]

theorem AlgEquiv.toLinearEquiv_symm {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : LinearEquiv.symm (AlgEquiv.toLinearEquiv e) = AlgEquiv.toLinearEquiv (AlgEquiv.symm e)

@[simp]

theorem AlgEquiv.toLinearEquiv_trans {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring A₃] [Algebra R A₁] [Algebra R A₂] [Algebra R A₃] (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) : AlgEquiv.toLinearEquiv (AlgEquiv.trans e₁ e₂) = LinearEquiv.trans (AlgEquiv.toLinearEquiv e₁) (AlgEquiv.toLinearEquiv e₂)

theorem AlgEquiv.toLinearEquiv_injective {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] : Function.Injective AlgEquiv.toLinearEquiv

def AlgEquiv.toLinearMap {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : A₁ →ₗ[R] A₂

Interpret an algebra equivalence as a linear map.

@[simp]

theorem AlgEquiv.toAlgHom_toLinearMap {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : AlgHom.toLinearMap ↑e = AlgEquiv.toLinearMap e

theorem AlgEquiv.toLinearMap_ofAlgHom {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : AlgHom.comp f g = AlgHom.id R A₂) (h₂ : AlgHom.comp g f = AlgHom.id R A₁) : AlgEquiv.toLinearMap (AlgEquiv.ofAlgHom f g h₁ h₂) = AlgHom.toLinearMap f

@[simp]

theorem AlgEquiv.toLinearEquiv_toLinearMap {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : ↑(AlgEquiv.toLinearEquiv e) = AlgEquiv.toLinearMap e

@[simp]

theorem AlgEquiv.toLinearMap_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₁) : ↑(AlgEquiv.toLinearMap e) x = ↑e x

theorem AlgEquiv.toLinearMap_injective {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] : Function.Injective AlgEquiv.toLinearMap

@[simp]

theorem AlgEquiv.trans_toLinearMap {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring A₃] [Algebra R A₁] [Algebra R A₂] [Algebra R A₃] (f : A₁ ≃ₐ[R] A₂) (g : A₂ ≃ₐ[R] A₃) : AlgEquiv.toLinearMap (AlgEquiv.trans f g) = LinearMap.comp (AlgEquiv.toLinearMap g) (AlgEquiv.toLinearMap f)

@[simp]

theorem AlgEquiv.ofLinearEquiv_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (l : A₁ ≃ₗ[R] A₂) (map_mul : ∀ (x y : A₁), ↑l (x * y) = ↑l x * ↑l y) (commutes : ∀ (r : R), ↑l (↑(algebraMap R A₁) r) = ↑(algebraMap R A₂) r) (a : A₁) : ↑(AlgEquiv.ofLinearEquiv l map_mul commutes) a = ↑l a

def AlgEquiv.ofLinearEquiv {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (l : A₁ ≃ₗ[R] A₂) (map_mul : ∀ (x y : A₁), ↑l (x * y) = ↑l x * ↑l y) (commutes : ∀ (r : R), ↑l (↑(algebraMap R A₁) r) = ↑(algebraMap R A₂) r) : A₁ ≃ₐ[R] A₂

Upgrade a linear equivalence to an algebra equivalence, given that it distributes over multiplication and action of scalars.

@[simp]

theorem AlgEquiv.ofLinearEquiv_symm {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (l : A₁ ≃ₗ[R] A₂) (map_mul : ∀ (x y : A₁), ↑l (x * y) = ↑l x * ↑l y) (commutes : ∀ (r : R), ↑l (↑(algebraMap R A₁) r) = ↑(algebraMap R A₂) r) : AlgEquiv.symm (AlgEquiv.ofLinearEquiv l map_mul commutes) = AlgEquiv.ofLinearEquiv (LinearEquiv.symm l) (_ : ∀ (x y : A₂), ↑(AlgEquiv.symm (AlgEquiv.ofLinearEquiv l map_mul commutes)) (x * y) = ↑(AlgEquiv.symm (AlgEquiv.ofLinearEquiv l map_mul commutes)) x * ↑(AlgEquiv.symm (AlgEquiv.ofLinearEquiv l map_mul commutes)) y) (_ : ∀ (r : R), ↑(AlgEquiv.symm (AlgEquiv.ofLinearEquiv l map_mul commutes)) (↑(algebraMap R A₂) r) = ↑(algebraMap R A₁) r)

@[simp]

theorem AlgEquiv.ofLinearEquiv_toLinearEquiv {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (map_mul : ∀ (x y : A₁), ↑(AlgEquiv.toLinearEquiv e) (x * y) = ↑(AlgEquiv.toLinearEquiv e) x * ↑(AlgEquiv.toLinearEquiv e) y) (commutes : ∀ (r : R), ↑(AlgEquiv.toLinearEquiv e) (↑(algebraMap R A₁) r) = ↑(algebraMap R A₂) r) : AlgEquiv.ofLinearEquiv (AlgEquiv.toLinearEquiv e) map_mul commutes = e

@[simp]

theorem AlgEquiv.toLinearEquiv_ofLinearEquiv {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (l : A₁ ≃ₗ[R] A₂) (map_mul : ∀ (x y : A₁), ↑l (x * y) = ↑l x * ↑l y) (commutes : ∀ (r : R), ↑l (↑(algebraMap R A₁) r) = ↑(algebraMap R A₂) r) : AlgEquiv.toLinearEquiv (AlgEquiv.ofLinearEquiv l map_mul commutes) = l

@[simp]

theorem AlgEquiv.ofRingEquiv_toEquiv {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {f : A₁ ≃+* A₂} (hf : ∀ (x : R), ↑f (↑(algebraMap R A₁) x) = ↑(algebraMap R A₂) x) : ↑(AlgEquiv.ofRingEquiv hf) = { toFun := ↑f, invFun := ↑(RingEquiv.symm f), left_inv := (_ : Function.LeftInverse f.invFun f.toFun), right_inv := (_ : Function.RightInverse f.invFun f.toFun) }

@[simp]

theorem AlgEquiv.ofRingEquiv_symm_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {f : A₁ ≃+* A₂} (hf : ∀ (x : R), ↑f (↑(algebraMap R A₁) x) = ↑(algebraMap R A₂) x) (a : A₂) : ↑(AlgEquiv.symm (AlgEquiv.ofRingEquiv hf)) a = ↑(RingEquiv.symm f) a

@[simp]

theorem AlgEquiv.ofRingEquiv_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {f : A₁ ≃+* A₂} (hf : ∀ (x : R), ↑f (↑(algebraMap R A₁) x) = ↑(algebraMap R A₂) x) (a : A₁) : ↑(AlgEquiv.ofRingEquiv hf) a = ↑f a

def AlgEquiv.ofRingEquiv {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {f : A₁ ≃+* A₂} (hf : ∀ (x : R), ↑f (↑(algebraMap R A₁) x) = ↑(algebraMap R A₂) x) : A₁ ≃ₐ[R] A₂

Promotes a linear ring_equiv to an AlgEquiv.

instance AlgEquiv.aut {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] : Group (A₁ ≃ₐ[R] A₁)

theorem AlgEquiv.aut_mul {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] (ϕ : A₁ ≃ₐ[R] A₁) (ψ : A₁ ≃ₐ[R] A₁) : ϕ * ψ = AlgEquiv.trans ψ ϕ

theorem AlgEquiv.aut_one {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] : 1 = AlgEquiv.refl

@[simp]

theorem AlgEquiv.one_apply {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] (x : A₁) : ↑1 x = x

@[simp]

theorem AlgEquiv.mul_apply {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] (e₁ : A₁ ≃ₐ[R] A₁) (e₂ : A₁ ≃ₐ[R] A₁) (x : A₁) : ↑(e₁ * e₂) x = ↑e₁ (↑e₂ x)

@[simp]

theorem AlgEquiv.autCongr_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (ϕ : A₁ ≃ₐ[R] A₂) (ψ : A₁ ≃ₐ[R] A₁) : ↑(AlgEquiv.autCongr ϕ) ψ = AlgEquiv.trans (AlgEquiv.symm ϕ) (AlgEquiv.trans ψ ϕ)

def AlgEquiv.autCongr {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (ϕ : A₁ ≃ₐ[R] A₂) : (A₁ ≃ₐ[R] A₁) ≃* A₂ ≃ₐ[R] A₂

An algebra isomorphism induces a group isomorphism between automorphism groups.

This is a more bundled version of AlgEquiv.equivCongr.

@[simp]

theorem AlgEquiv.autCongr_refl {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] : AlgEquiv.autCongr AlgEquiv.refl = MulEquiv.refl (A₁ ≃ₐ[R] A₁)

@[simp]

theorem AlgEquiv.autCongr_symm {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (ϕ : A₁ ≃ₐ[R] A₂) : MulEquiv.symm (AlgEquiv.autCongr ϕ) = AlgEquiv.autCongr (AlgEquiv.symm ϕ)

@[simp]

theorem AlgEquiv.autCongr_trans {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring A₃] [Algebra R A₁] [Algebra R A₂] [Algebra R A₃] (ϕ : A₁ ≃ₐ[R] A₂) (ψ : A₂ ≃ₐ[R] A₃) : MulEquiv.trans (AlgEquiv.autCongr ϕ) (AlgEquiv.autCongr ψ) = AlgEquiv.autCongr (AlgEquiv.trans ϕ ψ)

instance AlgEquiv.applyMulSemiringAction {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] : MulSemiringAction (A₁ ≃ₐ[R] A₁) A₁

The tautological action by A₁ ≃ₐ[R] A₁ on A₁.

This generalizes Function.End.applyMulAction.

@[simp]

theorem AlgEquiv.smul_def {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] (f : A₁ ≃ₐ[R] A₁) (a : A₁) : f • a = ↑f a

instance AlgEquiv.apply_faithfulSMul {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] : FaithfulSMul (A₁ ≃ₐ[R] A₁) A₁

instance AlgEquiv.apply_smulCommClass {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] : SMulCommClass R (A₁ ≃ₐ[R] A₁) A₁

instance AlgEquiv.apply_smulCommClass' {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] : SMulCommClass (A₁ ≃ₐ[R] A₁) R A₁

@[simp]

theorem AlgEquiv.algebraMap_eq_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) {y : R} {x : A₁} : ↑(algebraMap R A₂) y = ↑e x ↔ ↑(algebraMap R A₁) y = x

theorem AlgEquiv.map_prod {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [CommSemiring A₁] [CommSemiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) {ι : Type u_1} (f : ι → A₁) (s : Finset ι) : ↑e (Finset.prod s fun x => f x) = Finset.prod s fun x => ↑e (f x)

theorem AlgEquiv.map_finsupp_prod {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [CommSemiring A₁] [CommSemiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) {α : Type u_1} [Zero α] {ι : Type u_2} (f : ι →₀ α) (g : ι → α → A₁) : ↑e (Finsupp.prod f g) = Finsupp.prod f fun i a => ↑e (g i a)

theorem AlgEquiv.map_neg {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Ring A₁] [Ring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₁) : ↑e (-x) = -↑e x

theorem AlgEquiv.map_sub {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Ring A₁] [Ring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₁) (y : A₁) : ↑e (x - y) = ↑e x - ↑e y

@[simp]

theorem MulSemiringAction.toAlgEquiv_symm_apply {G : Type u_2} (R : Type u_3) (A : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [Group G] [MulSemiringAction G A] [SMulCommClass G R A] (g : G) : ∀ (a : A), ↑(AlgEquiv.symm (MulSemiringAction.toAlgEquiv R A g)) a = g⁻¹ • a

@[simp]

theorem MulSemiringAction.toAlgEquiv_toEquiv {G : Type u_2} (R : Type u_3) (A : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [Group G] [MulSemiringAction G A] [SMulCommClass G R A] (g : G) : ↑(MulSemiringAction.toAlgEquiv R A g) = ↑(MulSemiringAction.toRingEquiv G A g)

@[simp]

theorem MulSemiringAction.toAlgEquiv_apply {G : Type u_2} (R : Type u_3) (A : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [Group G] [MulSemiringAction G A] [SMulCommClass G R A] (g : G) : ∀ (a : A), ↑(MulSemiringAction.toAlgEquiv R A g) a = g • a

def MulSemiringAction.toAlgEquiv {G : Type u_2} (R : Type u_3) (A : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [Group G] [MulSemiringAction G A] [SMulCommClass G R A] (g : G) : A ≃ₐ[R] A

Each element of the group defines an algebra equivalence.

This is a stronger version of MulSemiringAction.toRingEquiv and DistribMulAction.toLinearEquiv.

theorem MulSemiringAction.toAlgEquiv_injective {G : Type u_2} (R : Type u_3) (A : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [Group G] [MulSemiringAction G A] [SMulCommClass G R A] [FaithfulSMul G A] : Function.Injective (MulSemiringAction.toAlgEquiv R A)