# 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) [] [] [] [Algebra R A] [Algebra R B] extends :
Type (max v w)

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

• toFun : AB
• invFun : BA
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• map_mul' : ∀ (x y : A), self.toFun (x * y) = self.toFun x * self.toFun y

The proposition that the function preserves multiplication

• map_add' : ∀ (x y : A), self.toFun (x + y) = self.toFun x + self.toFun y

The proposition that the function preserves addition

• commutes' : ∀ (r : R), self.toFun (() r) = () r

An equivalence of algebras commutes with the action of scalars.

Instances For
theorem AlgEquiv.commutes' {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (self : A ≃ₐ[R] B) (r : R) :
self.toFun (() r) = () 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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
class AlgEquivClass (F : Type u_1) (R : outParam (Type u_2)) (A : outParam (Type u_3)) (B : outParam (Type u_4)) [] [] [] [Algebra R A] [Algebra R B] [EquivLike F A B] extends :

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.

• 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 (() r) = () r

An equivalence of algebras commutes with the action of scalars.

Instances
theorem AlgEquivClass.commutes {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} [] [] [] [Algebra R A] [Algebra R B] [EquivLike F A B] [self : AlgEquivClass F R A B] (f : F) (r : R) :
f (() r) = () r

An equivalence of algebras commutes with the action of scalars.

@[instance 100]
instance AlgEquivClass.toAlgHomClass (F : Type u_1) (R : Type u_2) (A : Type u_3) (B : Type u_4) [] [] [] [Algebra R A] [Algebra R B] [EquivLike F A B] [h : AlgEquivClass F R A B] :
AlgHomClass F R A B
Equations
• =
@[instance 100]
instance AlgEquivClass.toLinearEquivClass (F : Type u_1) (R : Type u_2) (A : Type u_3) (B : Type u_4) [] [] [] [Algebra R A] [Algebra R B] [EquivLike F A B] [h : AlgEquivClass F R A B] :
Equations
• =
def AlgEquivClass.toAlgEquiv {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] [EquivLike F A B] [AlgEquivClass F R A B] (f : F) :

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.

Equations
• f = let __src := f; let __src_1 := f; { toEquiv := __src, map_mul' := , map_add' := , commutes' := }
Instances For
instance AlgEquivClass.instCoeTCAlgEquiv (F : Type u_1) (R : Type u_2) (A : Type u_3) (B : Type u_4) [] [] [] [Algebra R A] [Algebra R B] [EquivLike F A B] [AlgEquivClass F R A B] :
CoeTC F (A ≃ₐ[R] B)
Equations
• = { coe := AlgEquivClass.toAlgEquiv }
instance AlgEquiv.instEquivLike {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] :
EquivLike (A₁ ≃ₐ[R] A₂) A₁ A₂
Equations
• AlgEquiv.instEquivLike = { coe := fun (f : A₁ ≃ₐ[R] A₂) => f.toFun, inv := fun (f : A₁ ≃ₐ[R] A₂) => f.invFun, left_inv := , right_inv := , coe_injective' := }
instance AlgEquiv.instFunLike {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] :
FunLike (A₁ ≃ₐ[R] A₂) A₁ A₂

Helper instance since the coercion is not always found.

Equations
• AlgEquiv.instFunLike = { coe := DFunLike.coe, coe_injective' := }
instance AlgEquiv.instAlgEquivClass {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] :
AlgEquivClass (A₁ ≃ₐ[R] A₂) R A₁ A₂
Equations
• =
def AlgEquiv.Simps.apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
A₁A₂

See Note [custom simps projection]

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

See Note [custom simps projection]

Equations
Instances For
@[simp]
theorem AlgEquiv.coe_coe {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {F : Type u_1} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂] (f : F) :
f = f
theorem AlgEquiv.ext {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [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₂} [] [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₂} [] [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₂} [] [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₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] :
Function.Injective fun (e : A₁ ≃ₐ[R] A₂) => e
instance AlgEquiv.hasCoeToRingEquiv {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] :
CoeOut (A₁ ≃ₐ[R] A₂) (A₁ ≃+* A₂)
Equations
• AlgEquiv.hasCoeToRingEquiv = { coe := AlgEquiv.toRingEquiv }
@[simp]
theorem AlgEquiv.coe_mk {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [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₁), { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv }.toFun (x * y) = { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv }.toFun x * { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv }.toFun y} {map_add : ∀ (x y : A₁), { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv }.toFun (x + y) = { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv }.toFun x + { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv }.toFun y} {commutes : ∀ (r : R), { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv }.toFun ((algebraMap R A₁) r) = (algebraMap R A₂) r} :
{ 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₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (e' : A₂A₁) (h₁ : ) (h₂ : ) (h₃ : ∀ (x y : A₁), { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y) (h₄ : ∀ (x y : A₁), { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y) (h₅ : ∀ (r : R), { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun ((algebraMap R A₁) r) = (algebraMap R A₂) r) :
{ 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₂} [] [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₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
e.toRingEquiv = e
@[simp]
theorem AlgEquiv.toRingEquiv_toRingHom {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
e = e
@[simp]
theorem AlgEquiv.coe_ringEquiv {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [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₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
e.toRingEquiv = e
theorem AlgEquiv.coe_ringEquiv_injective {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [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₂} [] [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
@[deprecated map_zero]
theorem AlgEquiv.map_zero {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
e 0 = 0
@[deprecated map_mul]
theorem AlgEquiv.map_mul {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [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
@[deprecated map_one]
theorem AlgEquiv.map_one {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [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₂} [] [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
@[deprecated map_smul]
theorem AlgEquiv.map_smul {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (r : R) (x : A₁) :
e (r x) = r e x
@[deprecated map_sum]
theorem AlgEquiv.map_sum {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) {ι : Type u_1} (f : ιA₁) (s : ) :
e (xs, f x) = xs, e (f x)
@[deprecated map_finsupp_sum]
theorem AlgEquiv.map_finsupp_sum {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [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 (f.sum g) = f.sum fun (i : ι) (b : α) => e (g i b)
def AlgEquiv.toAlgHom {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [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.

Equations
• e = { toFun := e.toFun, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
Instances For
@[simp]
theorem AlgEquiv.toAlgHom_eq_coe {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [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₂} [] [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₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] :
Function.Injective AlgHomClass.toAlgHom
@[simp]
theorem AlgEquiv.toAlgHom_toRingHom {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
e = e
theorem AlgEquiv.coe_ringHom_commutes {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [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

@[deprecated map_pow]
theorem AlgEquiv.map_pow {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [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₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
theorem AlgEquiv.surjective {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
theorem AlgEquiv.bijective {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
def AlgEquiv.refl {R : Type uR} {A₁ : Type uA₁} [] [Semiring A₁] [Algebra R A₁] :
A₁ ≃ₐ[R] A₁

Algebra equivalences are reflexive.

Equations
• AlgEquiv.refl = let __src := 1; { toEquiv := __src.toEquiv, map_mul' := , map_add' := , commutes' := }
Instances For
instance AlgEquiv.instInhabited {R : Type uR} {A₁ : Type uA₁} [] [Semiring A₁] [Algebra R A₁] :
Inhabited (A₁ ≃ₐ[R] A₁)
Equations
• AlgEquiv.instInhabited = { default := AlgEquiv.refl }
@[simp]
theorem AlgEquiv.refl_toAlgHom {R : Type uR} {A₁ : Type uA₁} [] [Semiring A₁] [Algebra R A₁] :
AlgEquiv.refl = AlgHom.id R A₁
@[simp]
theorem AlgEquiv.coe_refl {R : Type uR} {A₁ : Type uA₁} [] [Semiring A₁] [Algebra R A₁] :
AlgEquiv.refl = id
def AlgEquiv.symm {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
A₂ ≃ₐ[R] A₁

Algebra equivalences are symmetric.

Equations
• e.symm = let __src := e.toRingEquiv.symm; { toEquiv := __src.toEquiv, map_mul' := , map_add' := , commutes' := }
Instances For
def AlgEquiv.Simps.symm_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
A₂A₁

See Note [custom simps projection]

Equations
• = e.symm
Instances For
theorem AlgEquiv.coe_apply_coe_coe_symm_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {F : Type u_1} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂] (f : F) (x : A₂) :
f ((f).symm x) = x
theorem AlgEquiv.coe_coe_symm_apply_coe_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {F : Type u_1} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂] (f : F) (x : A₁) :
(f).symm (f x) = x
@[simp]
theorem AlgEquiv.symm_toEquiv_eq_symm {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {e : A₁ ≃ₐ[R] A₂} :
(e).symm = e.symm
theorem AlgEquiv.invFun_eq_symm {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {e : A₁ ≃ₐ[R] A₂} :
e.invFun = e.symm
@[simp]
theorem AlgEquiv.symm_symm {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
e.symm.symm = e
theorem AlgEquiv.symm_bijective {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [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₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (f : A₂A₁) (h₁ : Function.LeftInverse (e) f) (h₂ : ) (h₃ : ∀ (x y : A₂), { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }.toFun y) (h₄ : ∀ (x y : A₂), { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }.toFun y) (h₅ : ∀ (r : R), { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }.toFun ((algebraMap R A₂) r) = (algebraMap R A₁) r) :
{ toFun := f, invFun := e, left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, commutes' := h₅ } = e.symm
def AlgEquiv.symm_mk.aux {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (f : A₁A₂) (f' : A₂A₁) (h₁ : ) (h₂ : ) (h₃ : ∀ (x y : A₁), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun y) (h₄ : ∀ (x y : A₁), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun y) (h₅ : ∀ (r : R), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun ((algebraMap R A₁) r) = (algebraMap R A₂) r) :
A₂ ≃ₐ[R] A₁

Auxilliary definition to avoid looping in dsimp with AlgEquiv.symm_mk.

Equations
• AlgEquiv.symm_mk.aux f f' h₁ h₂ h₃ h₄ h₅ = { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, commutes' := h₅ }.symm
Instances For
@[simp]
theorem AlgEquiv.symm_mk {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (f : A₁A₂) (f' : A₂A₁) (h₁ : ) (h₂ : ) (h₃ : ∀ (x y : A₁), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun y) (h₄ : ∀ (x y : A₁), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun y) (h₅ : ∀ (r : R), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun ((algebraMap R A₁) r) = (algebraMap R A₂) r) :
{ toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, commutes' := h₅ }.symm = let __src := AlgEquiv.symm_mk.aux f f' h₁ h₂ h₃ h₄ h₅; { toFun := f', invFun := f, left_inv := , right_inv := , map_mul' := , map_add' := , commutes' := }
@[simp]
theorem AlgEquiv.refl_symm {R : Type uR} {A₁ : Type uA₁} [] [Semiring A₁] [Algebra R A₁] :
AlgEquiv.refl.symm = AlgEquiv.refl
theorem AlgEquiv.toRingEquiv_symm {R : Type uR} {A₁ : Type uA₁} [] [Semiring A₁] [Algebra R A₁] (f : A₁ ≃ₐ[R] A₁) :
(f).symm = f.symm
@[simp]
theorem AlgEquiv.symm_toRingEquiv {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
e.symm = (e).symm
def AlgEquiv.trans {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃} [] [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.

Equations
• e₁.trans e₂ = let __src := e₁.toRingEquiv.trans e₂.toRingEquiv; { toEquiv := __src.toEquiv, map_mul' := , map_add' := , commutes' := }
Instances For
@[simp]
theorem AlgEquiv.apply_symm_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₂) :
e (e.symm x) = x
@[simp]
theorem AlgEquiv.symm_apply_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₁) :
e.symm (e x) = x
@[simp]
theorem AlgEquiv.symm_trans_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃} [] [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₃) :
(e₁.trans e₂).symm x = e₁.symm (e₂.symm x)
@[simp]
theorem AlgEquiv.coe_trans {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃} [] [Semiring A₁] [Semiring A₂] [Semiring A₃] [Algebra R A₁] [Algebra R A₂] [Algebra R A₃] (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) :
(e₁.trans e₂) = e₂ e₁
@[simp]
theorem AlgEquiv.trans_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃} [] [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₁) :
(e₁.trans e₂) x = e₂ (e₁ x)
@[simp]
theorem AlgEquiv.comp_symm {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
(e).comp e.symm = AlgHom.id R A₂
@[simp]
theorem AlgEquiv.symm_comp {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
(e.symm).comp e = AlgHom.id R A₁
theorem AlgEquiv.leftInverse_symm {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
Function.LeftInverse e.symm e
theorem AlgEquiv.rightInverse_symm {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
Function.RightInverse e.symm e
@[simp]
theorem AlgEquiv.arrowCongr_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₁' : Type uA₁'} {A₂' : Type uA₂'} [] [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₂) :
(e₁.arrowCongr e₂) f = ((e₂).comp f).comp e₁.symm
def AlgEquiv.arrowCongr {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₁' : Type uA₁'} {A₂' : Type uA₂'} [] [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₂'.

Equations
• e₁.arrowCongr e₂ = { toFun := fun (f : A₁ →ₐ[R] A₂) => ((e₂).comp f).comp e₁.symm, invFun := fun (f : A₁' →ₐ[R] A₂') => ((e₂.symm).comp f).comp e₁, left_inv := , right_inv := }
Instances For
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₃'} [] [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₃) :
(e₁.arrowCongr e₃) (g.comp f) = ((e₂.arrowCongr e₃) g).comp ((e₁.arrowCongr e₂) f)
@[simp]
theorem AlgEquiv.arrowCongr_refl {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] :
AlgEquiv.refl.arrowCongr 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₃'} [] [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₃') :
(e₁.trans e₂).arrowCongr (e₁'.trans e₂') = (e₁.arrowCongr e₁').trans (e₂.arrowCongr e₂')
@[simp]
theorem AlgEquiv.arrowCongr_symm {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₁' : Type uA₁'} {A₂' : Type uA₂'} [] [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₂') :
(e₁.arrowCongr e₂).symm = e₁.symm.arrowCongr e₂.symm
@[simp]
theorem AlgEquiv.equivCongr_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₁' : Type uA₁'} {A₂' : Type uA₂'} [] [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₁') :
(e.equivCongr e') ψ = e.symm.trans (ψ.trans e')
def AlgEquiv.equivCongr {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₁' : Type uA₁'} {A₂' : Type uA₂'} [] [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.

Equations
• e.equivCongr e' = { toFun := fun (ψ : A₁ ≃ₐ[R] A₁') => e.symm.trans (ψ.trans e'), invFun := fun (ψ : A₂ ≃ₐ[R] A₂') => e.trans (ψ.trans e'.symm), left_inv := , right_inv := }
Instances For
@[simp]
theorem AlgEquiv.equivCongr_refl {R : Type uR} {A₁ : Type uA₁} {A₁' : Type uA₁'} [] [Semiring A₁] [Semiring A₁'] [Algebra R A₁] [Algebra R A₁'] :
AlgEquiv.refl.equivCongr 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₂'} [] [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₂') :
(e.equivCongr e').symm = e.symm.equivCongr e'.symm
@[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₃'} [] [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₃') :
(e₁₂.equivCongr e₁₂').trans (e₂₃.equivCongr e₂₃') = (e₁₂.trans e₂₃).equivCongr (e₁₂'.trans e₂₃')
@[simp]
theorem AlgEquiv.ofAlgHom_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : f.comp g = AlgHom.id R A₂) (h₂ : g.comp f = AlgHom.id R A₁) (a : A₁) :
(AlgEquiv.ofAlgHom f g h₁ h₂) a = f a
@[simp]
theorem AlgEquiv.ofAlgHom_symm_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : f.comp g = AlgHom.id R A₂) (h₂ : g.comp f = AlgHom.id R A₁) (a : A₂) :
(AlgEquiv.ofAlgHom f g h₁ h₂).symm a = g a
def AlgEquiv.ofAlgHom {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : f.comp g = AlgHom.id R A₂) (h₂ : g.comp f = AlgHom.id R A₁) :
A₁ ≃ₐ[R] A₂

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

Equations
• AlgEquiv.ofAlgHom f g h₁ h₂ = { toFun := f, invFun := g, left_inv := , right_inv := , map_mul' := , map_add' := , commutes' := }
Instances For
theorem AlgEquiv.coe_algHom_ofAlgHom {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : f.comp g = AlgHom.id R A₂) (h₂ : g.comp 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₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (f : A₁ ≃ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : (f).comp g = AlgHom.id R A₂) (h₂ : g.comp 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₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : f.comp g = AlgHom.id R A₂) (h₂ : g.comp f = AlgHom.id R A₁) :
(AlgEquiv.ofAlgHom f g h₁ h₂).symm = AlgEquiv.ofAlgHom g f h₂ h₁
noncomputable def AlgEquiv.ofBijective {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (f : A₁ →ₐ[R] A₂) (hf : ) :
A₁ ≃ₐ[R] A₂

Promotes a bijective algebra homomorphism to an algebra equivalence.

Equations
• = let __src := RingEquiv.ofBijective (f) hf; { toEquiv := __src.toEquiv, map_mul' := , map_add' := , commutes' := }
Instances For
@[simp]
theorem AlgEquiv.coe_ofBijective {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {f : A₁ →ₐ[R] A₂} {hf : } :
() = f
theorem AlgEquiv.ofBijective_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {f : A₁ →ₐ[R] A₂} {hf : } (a : A₁) :
() a = f a
@[simp]
theorem AlgEquiv.toLinearEquiv_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (a : A₁) :
e.toLinearEquiv a = e a
def AlgEquiv.toLinearEquiv {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [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.

Equations
• e.toLinearEquiv = { toFun := e, map_add' := , map_smul' := , invFun := e.symm, left_inv := , right_inv := }
Instances For
@[simp]
theorem AlgEquiv.toLinearEquiv_refl {R : Type uR} {A₁ : Type uA₁} [] [Semiring A₁] [Algebra R A₁] :
AlgEquiv.refl.toLinearEquiv =
@[simp]
theorem AlgEquiv.toLinearEquiv_symm {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
e.toLinearEquiv.symm = e.symm.toLinearEquiv
@[simp]
theorem AlgEquiv.toLinearEquiv_trans {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃} [] [Semiring A₁] [Semiring A₂] [Semiring A₃] [Algebra R A₁] [Algebra R A₂] [Algebra R A₃] (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) :
(e₁.trans e₂).toLinearEquiv = e₁.toLinearEquiv ≪≫ₗ e₂.toLinearEquiv
theorem AlgEquiv.toLinearEquiv_injective {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [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₂} [] [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.

Equations
• e.toLinearMap = (e).toLinearMap
Instances For
@[simp]
theorem AlgEquiv.toAlgHom_toLinearMap {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
(e).toLinearMap = e.toLinearMap
theorem AlgEquiv.toLinearMap_ofAlgHom {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : f.comp g = AlgHom.id R A₂) (h₂ : g.comp f = AlgHom.id R A₁) :
(AlgEquiv.ofAlgHom f g h₁ h₂).toLinearMap = f.toLinearMap
@[simp]
theorem AlgEquiv.toLinearEquiv_toLinearMap {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
e.toLinearEquiv = e.toLinearMap
@[simp]
theorem AlgEquiv.toLinearMap_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₁) :
e.toLinearMap x = e x
theorem AlgEquiv.toLinearMap_injective {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [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₃} [] [Semiring A₁] [Semiring A₂] [Semiring A₃] [Algebra R A₁] [Algebra R A₂] [Algebra R A₃] (f : A₁ ≃ₐ[R] A₂) (g : A₂ ≃ₐ[R] A₃) :
(f.trans g).toLinearMap = g.toLinearMap ∘ₗ f.toLinearMap
@[simp]
theorem AlgEquiv.ofLinearEquiv_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (l : A₁ ≃ₗ[R] A₂) (map_one : l 1 = 1) (map_mul : ∀ (x y : A₁), l (x * y) = l x * l y) (a : A₁) :
(AlgEquiv.ofLinearEquiv l map_one map_mul) a = l a
def AlgEquiv.ofLinearEquiv {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (l : A₁ ≃ₗ[R] A₂) (map_one : l 1 = 1) (map_mul : ∀ (x y : A₁), l (x * y) = l x * l y) :
A₁ ≃ₐ[R] A₂

Upgrade a linear equivalence to an algebra equivalence, given that it distributes over multiplication and the identity

Equations
• AlgEquiv.ofLinearEquiv l map_one map_mul = { toFun := l, invFun := l.symm, left_inv := , right_inv := , map_mul' := map_mul, map_add' := , commutes' := }
Instances For
def AlgEquiv.ofLinearEquiv_symm.aux {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (l : A₁ ≃ₗ[R] A₂) (map_one : l 1 = 1) (map_mul : ∀ (x y : A₁), l (x * y) = l x * l y) :
A₂ ≃ₐ[R] A₁

Auxilliary definition to avoid looping in dsimp with AlgEquiv.ofLinearEquiv_symm.

Equations
Instances For
@[simp]
theorem AlgEquiv.ofLinearEquiv_symm {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (l : A₁ ≃ₗ[R] A₂) (map_one : l 1 = 1) (map_mul : ∀ (x y : A₁), l (x * y) = l x * l y) :
(AlgEquiv.ofLinearEquiv l map_one map_mul).symm = AlgEquiv.ofLinearEquiv l.symm
@[simp]
theorem AlgEquiv.ofLinearEquiv_toLinearEquiv {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (map_mul : e.toLinearEquiv 1 = 1) (map_one : ∀ (x y : A₁), e.toLinearEquiv (x * y) = e.toLinearEquiv x * e.toLinearEquiv y) :
AlgEquiv.ofLinearEquiv e.toLinearEquiv map_mul map_one = e
@[simp]
theorem AlgEquiv.toLinearEquiv_ofLinearEquiv {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (l : A₁ ≃ₗ[R] A₂) (map_one : l 1 = 1) (map_mul : ∀ (x y : A₁), l (x * y) = l x * l y) :
(AlgEquiv.ofLinearEquiv l map_one map_mul).toLinearEquiv = l
@[simp]
theorem AlgEquiv.ofRingEquiv_toEquiv {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [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) :
() = { toFun := f, invFun := f.symm, left_inv := , right_inv := }
@[simp]
theorem AlgEquiv.ofRingEquiv_symm_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [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₂) :
().symm a = f.symm a
@[simp]
theorem AlgEquiv.ofRingEquiv_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [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₁) :
() a = f a
def AlgEquiv.ofRingEquiv {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [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 RingEquiv to an AlgEquiv.

Equations
• = { toFun := f, invFun := f.symm, left_inv := , right_inv := , map_mul' := , map_add' := , commutes' := hf }
Instances For
instance AlgEquiv.aut {R : Type uR} {A₁ : Type uA₁} [] [Semiring A₁] [Algebra R A₁] :
Group (A₁ ≃ₐ[R] A₁)
Equations
• AlgEquiv.aut =
theorem AlgEquiv.aut_mul {R : Type uR} {A₁ : Type uA₁} [] [Semiring A₁] [Algebra R A₁] (ϕ : A₁ ≃ₐ[R] A₁) (ψ : A₁ ≃ₐ[R] A₁) :
ϕ * ψ = ψ.trans ϕ
theorem AlgEquiv.aut_one {R : Type uR} {A₁ : Type uA₁} [] [Semiring A₁] [Algebra R A₁] :
1 = AlgEquiv.refl
@[simp]
theorem AlgEquiv.one_apply {R : Type uR} {A₁ : Type uA₁} [] [Semiring A₁] [Algebra R A₁] (x : A₁) :
1 x = x
@[simp]
theorem AlgEquiv.mul_apply {R : Type uR} {A₁ : Type uA₁} [] [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₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (ϕ : A₁ ≃ₐ[R] A₂) (ψ : A₁ ≃ₐ[R] A₁) :
ϕ.autCongr ψ = ϕ.symm.trans (ψ.trans ϕ)
def AlgEquiv.autCongr {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AlgEquiv.autCongr_refl {R : Type uR} {A₁ : Type uA₁} [] [Semiring A₁] [Algebra R A₁] :
AlgEquiv.refl.autCongr = MulEquiv.refl (A₁ ≃ₐ[R] A₁)
@[simp]
theorem AlgEquiv.autCongr_symm {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (ϕ : A₁ ≃ₐ[R] A₂) :
ϕ.autCongr.symm = ϕ.symm.autCongr
@[simp]
theorem AlgEquiv.autCongr_trans {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃} [] [Semiring A₁] [Semiring A₂] [Semiring A₃] [Algebra R A₁] [Algebra R A₂] [Algebra R A₃] (ϕ : A₁ ≃ₐ[R] A₂) (ψ : A₂ ≃ₐ[R] A₃) :
ϕ.autCongr.trans ψ.autCongr = (ϕ.trans ψ).autCongr
instance AlgEquiv.applyMulSemiringAction {R : Type uR} {A₁ : Type uA₁} [] [Semiring A₁] [Algebra R A₁] :
MulSemiringAction (A₁ ≃ₐ[R] A₁) A₁

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

This generalizes Function.End.applyMulAction.

Equations
• AlgEquiv.applyMulSemiringAction =
@[simp]
theorem AlgEquiv.smul_def {R : Type uR} {A₁ : Type uA₁} [] [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₁} [] [Semiring A₁] [Algebra R A₁] :
FaithfulSMul (A₁ ≃ₐ[R] A₁) A₁
Equations
• =
instance AlgEquiv.apply_smulCommClass {R : Type uR} {A₁ : Type uA₁} [] [Semiring A₁] [Algebra R A₁] :
SMulCommClass R (A₁ ≃ₐ[R] A₁) A₁
Equations
• =
instance AlgEquiv.apply_smulCommClass' {R : Type uR} {A₁ : Type uA₁} [] [Semiring A₁] [Algebra R A₁] :
SMulCommClass (A₁ ≃ₐ[R] A₁) R A₁
Equations
• =
instance AlgEquiv.instMulDistribMulActionUnits {R : Type uR} {A₁ : Type uA₁} [] [Semiring A₁] [Algebra R A₁] :
Equations
• AlgEquiv.instMulDistribMulActionUnits =
@[simp]
theorem AlgEquiv.smul_units_def {R : Type uR} {A₁ : Type uA₁} [] [Semiring A₁] [Algebra R A₁] (f : A₁ ≃ₐ[R] A₁) (x : A₁ˣ) :
f x = () x
@[simp]
theorem AlgEquiv.algebraMap_eq_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [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
@[simp]
theorem AlgEquiv.toLinearMapHom_apply (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] (e : A ≃ₐ[R] A) :
() e = e.toLinearMap
def AlgEquiv.toLinearMapHom (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] :
(A ≃ₐ[R] A) →* A →ₗ[R] A

AlgEquiv.toLinearMap as a MonoidHom.

Equations
• = { toFun := AlgEquiv.toLinearMap, map_one' := , map_mul' := }
Instances For
theorem AlgEquiv.pow_toLinearMap {R : Type uR} {A₁ : Type uA₁} [] [Semiring A₁] [Algebra R A₁] (σ : A₁ ≃ₐ[R] A₁) (n : ) :
(σ ^ n).toLinearMap = σ.toLinearMap ^ n
@[simp]
theorem AlgEquiv.one_toLinearMap {R : Type uR} {A₁ : Type uA₁} [] [Semiring A₁] [Algebra R A₁] :
@[simp]
theorem AlgEquiv.algHomUnitsEquiv_apply_symm_apply (R : Type u_1) (S : Type u_2) [] [] [Algebra R S] (f : (S →ₐ[R] S)ˣ) (a : S) :
( f).symm a = f⁻¹ a
@[simp]
theorem AlgEquiv.algHomUnitsEquiv_apply_apply (R : Type u_1) (S : Type u_2) [] [] [Algebra R S] (f : (S →ₐ[R] S)ˣ) :
∀ (a : S), ( f) a = ((f).toRingHom).toFun a
@[simp]
theorem AlgEquiv.val_inv_algHomUnitsEquiv_symm_apply (R : Type u_1) (S : Type u_2) [] [] [Algebra R S] (f : S ≃ₐ[R] S) :
(.symm f)⁻¹ = f.symm
@[simp]
theorem AlgEquiv.val_algHomUnitsEquiv_symm_apply (R : Type u_1) (S : Type u_2) [] [] [Algebra R S] (f : S ≃ₐ[R] S) :
(.symm f) = f
def AlgEquiv.algHomUnitsEquiv (R : Type u_1) (S : Type u_2) [] [] [Algebra R S] :

The units group of S →ₐ[R] S is S ≃ₐ[R] S. See LinearMap.GeneralLinearGroup.generalLinearEquiv for the linear map version.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[deprecated map_prod]
theorem AlgEquiv.map_prod {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [] [] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) {ι : Type u_1} (f : ιA₁) (s : ) :
e (xs, f x) = xs, e (f x)
@[deprecated map_finsupp_prod]
theorem AlgEquiv.map_finsupp_prod {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [] [] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) {α : Type u_1} [Zero α] {ι : Type u_2} (f : ι →₀ α) (g : ιαA₁) :
e (f.prod g) = f.prod fun (i : ι) (a : α) => e (g i a)
@[deprecated map_neg]
theorem AlgEquiv.map_neg {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [Ring A₁] [Ring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₁) :
e (-x) = -e x
@[deprecated map_sub]
theorem AlgEquiv.map_sub {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [] [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_toEquiv {G : Type u_2} (R : Type u_3) (A : Type u_4) [] [] [Algebra R A] [] [] [] (g : G) :
() = ()
@[simp]
theorem MulSemiringAction.toAlgEquiv_symm_apply {G : Type u_2} (R : Type u_3) (A : Type u_4) [] [] [Algebra R A] [] [] [] (g : G) :
∀ (a : A), ().symm a = g⁻¹ a
@[simp]
theorem MulSemiringAction.toAlgEquiv_apply {G : Type u_2} (R : Type u_3) (A : Type u_4) [] [] [Algebra R A] [] [] [] (g : G) :
∀ (a : A), () a = g a
def MulSemiringAction.toAlgEquiv {G : Type u_2} (R : Type u_3) (A : Type u_4) [] [] [Algebra R A] [] [] [] (g : G) :

Each element of the group defines an algebra equivalence.

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem MulSemiringAction.toAlgEquiv_injective {G : Type u_2} (R : Type u_3) (A : Type u_4) [] [] [Algebra R A] [] [] [] [] :