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.

Instances For

source

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.

Instances For

source

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.

Instances

source

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

source

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

source

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

Instances For

source

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 }

source

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

source

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

source

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₂

source

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

source

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'

source

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

source

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

source

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

source

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

source

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

source

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

source

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 }

source

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

source

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

source

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

source

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

source

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

source

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

source

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

Instances For

source

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

source

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

source

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

source

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

source

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

source

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

source

@[deprecated map_add (since := "2024-06-20")]

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

source

@[deprecated map_zero (since := "2024-06-20")]

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

source

@[deprecated map_mul (since := "2024-06-20")]

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

source

@[deprecated map_one (since := "2024-06-20")]

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

source

@[deprecated map_smul (since := "2024-06-20")]

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

source

@[deprecated map_pow (since := "2024-06-20")]

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

source

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

source

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

source

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

source

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

Instances For

source

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 }

source

@[simp]

theorem AlgEquiv.refl_toAlgHom {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] :

↑AlgEquiv.refl = AlgHom.id R A₁

source

@[simp]

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

⇑AlgEquiv.refl = id

source

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

Instances For

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

Instances For

source

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

source

@[simp]

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

AlgEquiv.refl.symm = AlgEquiv.refl

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

source

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

source

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

source

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

Instances For

source

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

source

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)

source

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

source

@[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₂')

source

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

source

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

Instances For

source

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

source

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

source

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

source

@[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₂₃')

source

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

Instances For

source

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

source

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

source

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

source

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

source

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₁

source

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

Instances For

source

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

source

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

source

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

Instances For

source

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

source

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

source

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

source

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

source

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

source

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

Instances For

source

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

source

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

source

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

source

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

source

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

source

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

source

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

Instances For

source

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

source

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

Instances For

source

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

source

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

source

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

source

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 }

Instances For

source

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

source

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

source

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

source

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 ⋯

source

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

ϕ * ψ = ψ.trans ϕ

source

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

1 = AlgEquiv.refl

source

@[simp]

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

1 x = x

source

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

source

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

Instances For

source

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

source

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

source

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

source

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

source

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

source

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

source

instance AlgEquiv.apply_faithfulSMul {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] :

FaithfulSMul (A₁ ≃ₐ[R] A₁) A₁

source

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₁

source

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₁

source

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

source

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

source

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

source

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

Instances For

source

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

source

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

source

@[simp]

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

AlgEquiv.toLinearMap 1 = 1

source

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.

Instances For

source

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

source

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

source

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

source

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

source

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₂)

Documentation

Mathlib.Algebra.Algebra.Equiv

Isomorphisms of `R`-algebras #

Main definitions #

Notations #

Isomorphisms of R-algebras #

Main definitions #

Notations #

Isomorphisms of `R`-algebras #