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.

Notation

• 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 A ≃ B, A ≃* B, A ≃+ B, A ≃+* B : Type (max v w)

An equivalence of algebras (denoted as A ≃ₐ[R] B) is an equivalence of rings commuting with the actions of scalars.

• toFun : A → B
• invFun : B → A
• 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
• map_add' (x y : A) : self.toFun (x + y) = self.toFun x + self.toFun y
• commutes' (r : R) : self.toFun ((algebraMap R A) r) = (algebraMap R B) r

  An equivalence of algebras commutes with the action of scalars.

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

An equivalence of algebras (denoted as A ≃ₐ[R] B) is an equivalence of rings commuting with the actions of scalars.

Equations

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

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] [EquivLike F A B] extends RingEquivClass F A B : Prop

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 ((algebraMap R A) r) = (algebraMap R B) 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) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [EquivLike F A B] [h : AlgEquivClass F R A B] : AlgHomClass F R A B

@[instance 100]

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] [EquivLike F A 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] [EquivLike F A 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.

Equations

• ↑f = { toEquiv := ↑f, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

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] [EquivLike F A B] [AlgEquivClass F R A B] : CoeTC F (A ≃ₐ[R] B)

Equations

• AlgEquivClass.instCoeTCAlgEquiv F R A B = { coe := AlgEquivClass.toAlgEquiv }

instance AlgEquiv.instEquivLike {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₂

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₂} [CommSemiring R] [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 = EquivLike.toFunLike

instance AlgEquiv.instAlgEquivClass {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₂

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 g : A₁ ≃ₐ[R] A₂} (h : ∀ (a : A₁), f a = g a) : f = g

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 g : A₁ ≃ₐ[R] A₂} : f = g ↔ ∀ (a : A₁), f a = g a

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 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 g : A₁ ≃ₐ[R] A₂} (h : f = g) (x : A₁) : f x = g x

@[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₂] {toEquiv : A₁ ≃ A₂} {map_mul : ∀ (x y : A₁), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y} {map_add : ∀ (x y : A₁), toEquiv.toFun (x + y) = toEquiv.toFun x + toEquiv.toFun y} {commutes : ∀ (r : R), toEquiv.toFun ((algebraMap R A₁) r) = (algebraMap R A₂) r} : ⇑{ toEquiv := toEquiv, map_mul' := map_mul, map_add' := map_add, commutes' := commutes } = ⇑toEquiv

@[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₁), { 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₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : e.toEquiv = ↑e

@[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} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂] (f : F) : ⇑↑f = ⇑f

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 : A₁ ≃ₐ[R] A₂) => ⇑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₂)

Equations

• AlgEquiv.hasCoeToRingEquiv = { coe := AlgEquiv.toRingEquiv }

@[simp]

theorem AlgEquiv.coe_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₂) : ⇑↑e = ⇑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₂) : e.toRingEquiv = ↑e

@[simp]

theorem AlgEquiv.toRingEquiv_toRingHom {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_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₂) : ⇑e.toRingEquiv = ⇑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

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.

Equations

• ↑e = { toFun := e.toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

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

@[simp]

theorem AlgEquiv.toAlgHom_toRingHom {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_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

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

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

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

Algebra equivalences are reflexive.

Equations

• AlgEquiv.refl = { toEquiv := (RingEquiv.refl A₁).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

instance AlgEquiv.instInhabited {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [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₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] : ↑refl = AlgHom.id R A₁

@[simp]

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

@[simp]

theorem AlgEquiv.coe_refl {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] : ⇑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.

Equations

• e.symm = { toEquiv := e.toRingEquiv.symm.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

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 = ⇑e.symm

@[simp]

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} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂] (f : F) (x : A₂) : f ((↑f).symm x) = x

@[simp]

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} [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₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {e : A₁ ≃ₐ[R] A₂} : (↑e).symm = ↑e.symm

simp normal form of invFun_eq_symm

@[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₂) : e.symm.symm = 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 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₂), { 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₂} [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₁), { 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₁

Auxiliary 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

@[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₁), { 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 := 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₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] : refl.symm = refl

theorem AlgEquiv.toRingEquiv_symm {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [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₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : ↑e.symm = (↑e).symm

@[simp]

theorem AlgEquiv.symm_toAddEquiv {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 = (↑e).symm

@[simp]

theorem AlgEquiv.symm_toMulEquiv {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 = (↑e).symm

@[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 (e.symm 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₁) : e.symm (e x) = x

theorem AlgEquiv.symm_apply_eq {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.symm x = y ↔ x = e y

theorem AlgEquiv.eq_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₂} {y : A₁} : y = e.symm x ↔ e y = 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₂) : (↑e).comp ↑e.symm = 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₂) : (↑e.symm).comp ↑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 ⇑e.symm ⇑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 ⇑e.symm ⇑e

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]

Equations

• AlgEquiv.Simps.apply e = ⇑e

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]

Equations

• AlgEquiv.Simps.toEquiv e = ↑e

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]

Equations

• AlgEquiv.Simps.symm_apply e = ⇑e.symm

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.

Equations

• e₁.trans e₂ = { toEquiv := (e₁.toRingEquiv.trans e₂.toRingEquiv).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[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₃) : ⇑(e₁.trans 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₁) : (e₁.trans e₂) x = e₂ (e₁ 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₃) : (e₁.trans e₂).symm x = e₁.symm (e₂.symm x)

@[simp]

theorem AlgEquiv.self_trans_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.trans e.symm = refl

@[simp]

theorem AlgEquiv.symm_trans_self {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.trans e = refl

@[simp]

theorem AlgEquiv.toRingHom_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₃) : ↑(e₁.trans e₂) = (↑e₂).comp ↑e₁

def AlgEquiv.cast {R : Type uR} [CommSemiring R] {ι : Type u_1} {A : ι → Type u_2} [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] {i j : ι} (h : i = j) : A i ≃ₐ[R] A j

Equiv.cast (congrArg _ h) as an algebra equiv.

Note that unlike Equiv.cast, this takes an equality of indices rather than an equality of types, to avoid having to deal with an equality of the algebraic structure itself.

Equations

• AlgEquiv.cast h = { toEquiv := (RingEquiv.cast h).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem AlgEquiv.cast_symm_apply {R : Type uR} [CommSemiring R] {ι : Type u_1} {A : ι → Type u_2} [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] {i j : ι} (h : i = j) (a : A j) : (AlgEquiv.cast h).symm a = cast ⋯ a

@[simp]

theorem AlgEquiv.cast_apply {R : Type uR} [CommSemiring R] {ι : Type u_1} {A : ι → Type u_2} [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] {i j : ι} (h : i = j) (a : A i) : (AlgEquiv.cast h) a = cast ⋯ a

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₂'.

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

@[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₂) : (e₁.arrowCongr e₂) f = ((↑e₂).comp f).comp ↑e₁.symm

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₃) : (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₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] : refl.arrowCongr 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₃') : (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₂'} [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₂') : (e₁.arrowCongr e₂).symm = e₁.symm.arrowCongr e₂.symm

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.

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

@[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₁') : (e.equivCongr e') ψ = e.symm.trans (ψ.trans e')

@[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₁'] : refl.equivCongr 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₂') : (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₃'} [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₃') : (e₁₂.equivCongr e₁₂').trans (e₂₃.equivCongr e₂₃') = (e₁₂.trans e₂₃).equivCongr (e₁₂'.trans 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₁ : 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' := ⋯ }

@[simp]

theorem AlgEquiv.ofAlgHom_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₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : f.comp g = AlgHom.id R A₂) (h₂ : g.comp f = AlgHom.id R A₁) (a : A₂) : (ofAlgHom f g h₁ h₂).symm a = g a

@[simp]

theorem AlgEquiv.ofAlgHom_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₂) (g : A₂ →ₐ[R] A₁) (h₁ : f.comp g = AlgHom.id R A₂) (h₂ : g.comp f = AlgHom.id R A₁) (a : A₁) : (ofAlgHom f g h₁ h₂) a = f a

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₁ : f.comp g = AlgHom.id R A₂) (h₂ : g.comp f = AlgHom.id R A₁) : ↑(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₁ : (↑f).comp g = AlgHom.id R A₂) (h₂ : g.comp ↑f = AlgHom.id R A₁) : 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₁ : f.comp g = AlgHom.id R A₂) (h₂ : g.comp f = AlgHom.id R A₁) : (ofAlgHom f g h₁ h₂).symm = ofAlgHom g f h₂ h₁

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.

Equations

• e.toLinearEquiv = { toFun := ⇑e, map_add' := ⋯, map_smul' := ⋯, invFun := ⇑e.symm, left_inv := ⋯, right_inv := ⋯ }

@[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₁) : e.toLinearEquiv a = e a

@[simp]

theorem AlgEquiv.toLinearEquiv_refl {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] : refl.toLinearEquiv = 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₂) : e.symm.toLinearEquiv = e.toLinearEquiv.symm

@[simp]

theorem AlgEquiv.coe_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₂) : ⇑e.toLinearEquiv = ⇑e

@[simp]

theorem AlgEquiv.coe_symm_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₂) : ⇑e.toLinearEquiv.symm = ⇑e.symm

@[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₃) : (e₁.trans e₂).toLinearEquiv = e₁.toLinearEquiv ≪≫ₗ e₂.toLinearEquiv

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

Equations

• e.toLinearMap = (↑e).toLinearMap

@[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₂) : (↑e).toLinearMap = e.toLinearMap

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₁ : f.comp g = AlgHom.id R A₂) (h₂ : g.comp f = AlgHom.id R A₁) : (ofAlgHom f g h₁ h₂).toLinearMap = f.toLinearMap

@[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₂) : ↑e.toLinearEquiv = e.toLinearMap

@[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₁) : e.toLinearMap 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 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₃) : (f.trans g).toLinearMap = g.toLinearMap ∘ₗ f.toLinearMap

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.

Equations

• AlgEquiv.ofBijective f hf = { toEquiv := (RingEquiv.ofBijective (↑f) hf).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[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) : ⇑(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₁) : (ofBijective f hf) a = f a

@[simp]

theorem AlgEquiv.toLinearMap_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) : (ofBijective f hf).toLinearMap = ↑f

@[simp]

theorem AlgEquiv.toAlgHom_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) : ↑(ofBijective f hf) = f

theorem AlgEquiv.ofBijective_apply_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₁ →ₐ[R] A₂) (hf : Function.Bijective ⇑f) (x : A₂) : f ((ofBijective f hf).symm x) = x

@[simp]

theorem AlgEquiv.ofBijective_symm_apply_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) (x : A₁) : (ofBijective f hf).symm (f x) = x

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

@[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_one : l 1 = 1) (map_mul : ∀ (x y : A₁), l (x * y) = l x * l y) (a : A₁) : (ofLinearEquiv l map_one map_mul) a = l a

def AlgEquiv.ofLinearEquiv_symm.aux {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_one : l 1 = 1) (map_mul : ∀ (x y : A₁), l (x * y) = l x * l y) : A₂ ≃ₐ[R] A₁

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

Equations

• AlgEquiv.ofLinearEquiv_symm.aux l map_one map_mul = (AlgEquiv.ofLinearEquiv l map_one map_mul).symm

@[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_one : l 1 = 1) (map_mul : ∀ (x y : A₁), l (x * y) = l x * l y) : (ofLinearEquiv l map_one map_mul).symm = ofLinearEquiv l.symm ⋯ ⋯

@[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 : e.toLinearEquiv 1 = 1) (map_one : ∀ (x y : A₁), e.toLinearEquiv (x * y) = e.toLinearEquiv x * e.toLinearEquiv y) : ofLinearEquiv e.toLinearEquiv map_mul map_one = 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_one : l 1 = 1) (map_mul : ∀ (x y : A₁), l (x * y) = l x * l y) : (ofLinearEquiv l map_one map_mul).toLinearEquiv = l

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 RingEquiv to an AlgEquiv.

Equations

• AlgEquiv.ofRingEquiv hf = { toFun := ⇑f, invFun := ⇑f.symm, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := hf }

@[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₁) : (ofRingEquiv hf) a = f a

@[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₂) : (ofRingEquiv hf).symm a = f.symm a

@[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) : ↑(ofRingEquiv hf) = { toFun := ⇑f, invFun := ⇑f.symm, left_inv := ⋯, right_inv := ⋯ }

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

Stacks Tag 09HR

Equations

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

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

theorem AlgEquiv.aut_one {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] : 1 = 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₁ e₂ : A₁ ≃ₐ[R] A₁) (x : A₁) : (e₁ * e₂) x = e₁ (e₂ x)

theorem AlgEquiv.aut_inv {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] (ϕ : A₁ ≃ₐ[R] A₁) : ϕ⁻¹ = ϕ.symm

@[simp]

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

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.

Equations

• ϕ.autCongr = { toFun := fun (ψ : A₁ ≃ₐ[R] A₁) => ϕ.symm.trans (ψ.trans ϕ), invFun := fun (ψ : A₂ ≃ₐ[R] A₂) => ϕ.trans (ψ.trans ϕ.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

@[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₁) : ϕ.autCongr ψ = ϕ.symm.trans (ψ.trans ϕ)

@[simp]

theorem AlgEquiv.autCongr_refl {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] : refl.autCongr = 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₂) : ϕ.autCongr.symm = ϕ.symm.autCongr

@[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₃) : ϕ.autCongr.trans ψ.autCongr = (ϕ.trans ψ).autCongr

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.

Equations

• AlgEquiv.applyMulSemiringAction = { smul := fun (x1 : A₁ ≃ₐ[R] A₁) (x2 : A₁) => x1 x2, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, smul_one := ⋯, smul_mul := ⋯ }

@[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₁] {S : Type u_1} [SMul S R] [SMul S A₁] [IsScalarTower S R A₁] : SMulCommClass S (A₁ ≃ₐ[R] A₁) A₁

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

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

Equations

• AlgEquiv.instMulDistribMulActionUnits = { smul := fun (f : A₁ ≃ₐ[R] A₁) => ⇑(Units.map ↑f), one_smul := ⋯, mul_smul := ⋯, smul_mul := ⋯, smul_one := ⋯ }

@[simp]

theorem AlgEquiv.smul_units_def {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] (f : A₁ ≃ₐ[R] A₁) (x : A₁ˣ) : f • x = (Units.map ↑f) x

@[simp]

theorem MulSemiringAction.toRingEquiv_algEquiv {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] (σ : A₁ ≃ₐ[R] A₁) : toRingEquiv (A₁ ≃ₐ[R] A₁) 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

def AlgEquiv.toAlgHomHom (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] : (A ≃ₐ[R] A) →* A →ₐ[R] A

AlgEquiv.toAlgHom as a MonoidHom.

Equations

• AlgEquiv.toAlgHomHom R A = { toFun := AlgEquiv.toAlgHom, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem AlgEquiv.toAlgHomHom_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (e : A ≃ₐ[R] A) : (toAlgHomHom R A) e = ↑e

def AlgEquiv.toLinearMapHom (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] : (A ≃ₐ[R] A) →* Module.End R A

AlgEquiv.toLinearMap as a MonoidHom.

Equations

• AlgEquiv.toLinearMapHom R A = AlgHom.toEnd.comp (AlgEquiv.toAlgHomHom R A)

@[simp]

theorem AlgEquiv.toLinearMapHom_apply_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a✝ : A ≃ₐ[R] A) (a : A) : ((toLinearMapHom R A) a✝) a = a✝ a

theorem AlgEquiv.pow_toLinearMap {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] (σ : A₁ ≃ₐ[R] A₁) (n : ℕ) : (σ ^ n).toLinearMap = σ.toLinearMap ^ n

@[simp]

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

def AlgEquiv.algHomUnitsEquiv (R : Type u_1) (S : Type u_2) [CommSemiring R] [Semiring S] [Algebra R S] : (S →ₐ[R] S)ˣ ≃* S ≃ₐ[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.

@[simp]

theorem AlgEquiv.algHomUnitsEquiv_apply_symm_apply (R : Type u_1) (S : Type u_2) [CommSemiring R] [Semiring S] [Algebra R S] (f : (S →ₐ[R] S)ˣ) (a : S) : ((algHomUnitsEquiv R S) f).symm a = ↑↑f⁻¹ a

@[simp]

theorem AlgEquiv.algHomUnitsEquiv_apply_apply (R : Type u_1) (S : Type u_2) [CommSemiring R] [Semiring S] [Algebra R S] (f : (S →ₐ[R] S)ˣ) (a✝ : S) : ((algHomUnitsEquiv R S) f) a✝ = (↑↑(↑f).toRingHom).toFun a✝

@[simp]

theorem AlgEquiv.val_inv_algHomUnitsEquiv_symm_apply (R : Type u_1) (S : Type u_2) [CommSemiring R] [Semiring S] [Algebra R S] (f : S ≃ₐ[R] S) : ↑((algHomUnitsEquiv R S).symm f)⁻¹ = ↑f.symm

@[simp]

theorem AlgEquiv.val_algHomUnitsEquiv_symm_apply (R : Type u_1) (S : Type u_2) [CommSemiring R] [Semiring S] [Algebra R S] (f : S ≃ₐ[R] S) : ↑((algHomUnitsEquiv R S).symm f) = ↑f

instance Finite.algEquiv {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] [Finite (A₁ →ₐ[R] A₂)] : Finite (A₁ ≃ₐ[R] A₂)

See also Finite.algHom

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.

Equations

• MulSemiringAction.toAlgEquiv R A g = { toEquiv := (MulSemiringAction.toRingEquiv G A g).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[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) : (toAlgEquiv R A g).symm a✝ = g⁻¹ • a✝

@[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) : (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) : ↑(toAlgEquiv R A g) = ↑(toRingEquiv G A g)

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 (toAlgEquiv R A)

def MulSemiringAction.toAlgAut (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 →* A ≃ₐ[R] A

Each element of the group defines an algebra equivalence.

This is a stronger version of MulSemiringAction.toRingAut and DistribMulAction.toModuleEnd.

Equations

• MulSemiringAction.toAlgAut G R A = { toFun := MulSemiringAction.toAlgEquiv R A, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem MulSemiringAction.toAlgAut_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) : (toAlgAut G R A) g = toAlgEquiv R A g

instance instUniqueAlgEquivOfSubsingleton {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommSemiring R] [Semiring S] [Semiring T] [Algebra R S] [Algebra R T] [Subsingleton S] [Subsingleton T] : Unique (S ≃ₐ[R] T)

Equations

• instUniqueAlgEquivOfSubsingleton = { default := AlgEquiv.ofAlgHom default default ⋯ ⋯, uniq := ⋯ }

@[simp]

theorem AlgEquiv.default_apply {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommSemiring R] [Semiring S] [Semiring T] [Algebra R S] [Algebra R T] [Subsingleton S] [Subsingleton T] (x : S) : default x = 0

def ULift.algEquiv {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : ULift.{w, v} A ≃ₐ[R] A

The algebra equivalence between ULift A and A.

Equations

• ULift.algEquiv = { toEquiv := ULift.ringEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

theorem ULift.algEquiv_apply {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (self : ULift.{w, v} A) : algEquiv self = self.down

def LinearEquiv.algEquivOfRing {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (e : R ≃ₗ[R] A) : R ≃ₐ[R] A

If an R-algebra A is isomorphic to R as R-module, then the canonical map R → A is an equivalence of R-algebras.

Note that if e : R ≃ₗ[R] A is the linear equivalence, then this is not the same as the equivalence of algebras provided here unless e 1 = 1.

Equations

• e.algEquivOfRing = { toFun := (↑↑(Algebra.ofId R A).toRingHom).toFun, invFun := fun (x : A) => e.symm (e 1 * x), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem LinearEquiv.algEquivOfRing_symm_apply {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (e : R ≃ₗ[R] A) (x : A) : e.algEquivOfRing.symm x = e.symm (e 1 * x)

@[simp]

theorem LinearEquiv.algEquivOfRing_apply {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (e : R ≃ₗ[R] A) (a✝ : R) : e.algEquivOfRing a✝ = (↑↑(Algebra.ofId R A).toRingHom).toFun a✝