Isomorphisms of R-algebras

This file defines bundled isomorphisms of R-algebras.

Main definitions

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

Notations

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

structure AlgEquiv (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] extends A ≃ B, A ≃* B, A ≃+ B, A ≃+* B : Type (max v w)

An equivalence of algebras 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 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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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 = { coe := DFunLike.coe, coe_injective' := ⋯ }

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₂

Equations

• ⋯ = ⋯

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

@[deprecated map_add]

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

@[deprecated map_smul]

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

@[deprecated map_pow]

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

theorem AlgEquiv.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₁] : ↑AlgEquiv.refl = AlgHom.id R A₁

@[simp]

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

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

Algebra equivalences are symmetric.

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]

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

@[simp]

theorem AlgEquiv.mk_coe' {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (f : A₂ → A₁) (h₁ : Function.LeftInverse (⇑e) f) (h₂ : Function.RightInverse (⇑e) f) (h₃ : ∀ (x y : A₂), { 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 := 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₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] : AlgEquiv.refl.symm = AlgEquiv.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.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)

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₂] : 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₃'} [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₁'] : 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₂'} [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_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₁) : (AlgEquiv.ofAlgHom f g h₁ h₂) a = f a

@[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₂) : (AlgEquiv.ofAlgHom f g h₁ h₂).symm a = g 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₁) : ↑(AlgEquiv.ofAlgHom f g h₁ h₂) = f

@[simp]

theorem AlgEquiv.ofAlgHom_coe_algHom {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (f : A₁ ≃ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : (↑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₂} [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₁) : (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₂} [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} : ⇑(AlgEquiv.ofBijective f hf) = ⇑f

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

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₁] : AlgEquiv.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.toLinearEquiv.symm = e.symm.toLinearEquiv

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

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

Interpret an algebra equivalence as a linear map.

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₁) : (AlgEquiv.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 AlgEquiv.toLinearMap

@[simp]

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

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

@[simp]

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

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

Stacks Tag 09HR

Equations

• AlgEquiv.aut = Group.mk ⋯

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 = AlgEquiv.refl

@[simp]

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

@[simp]

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

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₁] : AlgEquiv.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 = MulSemiringAction.mk ⋯ ⋯

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

Equations

• ⋯ = ⋯

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₁

Equations

• ⋯ = ⋯

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₁

Equations

• ⋯ = ⋯

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

Equations

• AlgEquiv.instMulDistribMulActionUnits = MulDistribMulAction.mk ⋯ ⋯

@[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 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.toLinearMapHom (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] : (A ≃ₐ[R] A) →* A →ₗ[R] A

AlgEquiv.toLinearMap as a MonoidHom.

Equations

• AlgEquiv.toLinearMapHom R A = { toFun := AlgEquiv.toLinearMap, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem AlgEquiv.toLinearMapHom_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (e : A ≃ₐ[R] A) : (AlgEquiv.toLinearMapHom R A) e = e.toLinearMap

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₁] : AlgEquiv.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) : ((AlgEquiv.algHomUnitsEquiv R S) f).symm a = ↑↑f⁻¹ a

@[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) : ↑((AlgEquiv.algHomUnitsEquiv R S).symm f) = ↑f

@[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) : ((AlgEquiv.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) : ↑((AlgEquiv.algHomUnitsEquiv R S).symm f)⁻¹ = ↑f.symm

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

Equations

• ⋯ = ⋯

@[deprecated map_neg]

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

@[deprecated map_sub]

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

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_apply {G : Type u_2} (R : Type u_3) (A : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [Group G] [MulSemiringAction G A] [SMulCommClass G R A] (g : G) (a✝ : A) : (MulSemiringAction.toAlgEquiv R A g) a✝ = g • a✝

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

@[simp]

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

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

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