Isomorphisms of R-algebras

This file defines bundled isomorphisms of R-algebras.

Main definitions

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

Notations

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

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

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

  The proposition that the function preserves multiplication

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

  The proposition that the function preserves addition

• commutes' : ∀ (r : R), self.toFun ((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 : 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 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 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 = let __src := ↑f; let __src_1 := ↑f; { toEquiv := __src, 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.instEquivLikeAlgEquiv {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] : EquivLike (A₁ ≃ₐ[R] A₂) A₁ A₂

Equations

• AlgEquiv.instEquivLikeAlgEquiv = { coe := fun (f : A₁ ≃ₐ[R] A₂) => f.toFun, inv := fun (f : A₁ ≃ₐ[R] A₂) => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

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

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

• ⋯ = ⋯

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

@[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.ext {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {f : A₁ ≃ₐ[R] A₂} {g : A₁ ≃ₐ[R] A₂} (h : ∀ (a : A₁), f a = g a) : f = g

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

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

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

theorem AlgEquiv.coe_fun_injective {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] : Function.Injective fun (e : 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_mk {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {toFun : A₁ → A₂} {invFun : A₂ → A₁} {left_inv : Function.LeftInverse invFun toFun} {right_inv : Function.RightInverse invFun toFun} {map_mul : ∀ (x y : A₁), { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv }.toFun (x * y) = { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv }.toFun x * { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv }.toFun y} {map_add : ∀ (x y : A₁), { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv }.toFun (x + y) = { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv }.toFun x + { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv }.toFun y} {commutes : ∀ (r : R), { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv }.toFun ((algebraMap R A₁) r) = (algebraMap R A₂) r} : ⇑{ toEquiv := { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv }, map_mul' := map_mul, map_add' := map_add, commutes' := commutes } = toFun

@[simp]

theorem AlgEquiv.mk_coe {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (e' : A₂ → A₁) (h₁ : Function.LeftInverse e' ⇑e) (h₂ : Function.RightInverse e' ⇑e) (h₃ : ∀ (x y : A₁), { 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) : { toEquiv := { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄, commutes' := h₅ } = e

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

@[simp]

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

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

@[deprecated AlgEquiv.map_sum]

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

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

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

Interpret an algebra equivalence as an algebra homomorphism.

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

Equations

• ↑e = { toRingHom := { toMonoidHom := { toOneHom := { 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

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

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

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

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

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

Algebra equivalences are reflexive.

Equations

• AlgEquiv.refl = let __src := 1; { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

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

Equations

• AlgEquiv.instInhabitedAlgEquiv = { 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

• AlgEquiv.symm e = let __src := RingEquiv.symm (AlgEquiv.toRingEquiv e); { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

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

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 ((AlgEquiv.symm ↑f) x) = x

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

@[simp]

theorem AlgEquiv.symm_mk {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (f : A₁ → A₂) (f' : A₂ → A₁) (h₁ : Function.LeftInverse f' f) (h₂ : Function.RightInverse f' f) (h₃ : ∀ (x y : A₁), { 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) : AlgEquiv.symm { toEquiv := { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄, commutes' := h₅ } = let __src := AlgEquiv.symm { toEquiv := { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄, commutes' := h₅ }; { toEquiv := { toFun := f', invFun := f, left_inv := ⋯, 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.symm AlgEquiv.refl = AlgEquiv.refl

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

@[simp]

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

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

Algebra equivalences are transitive.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

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

Equations

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

This is the AlgEquiv version of AlgEquiv.arrowCongr.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

Equations

• AlgEquiv.ofAlgHom f g h₁ h₂ = { toEquiv := { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯ }, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

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

@[simp]

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

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

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

Promotes a bijective algebra homomorphism to an algebra equivalence.

Equations

• AlgEquiv.ofBijective f hf = let __src := RingEquiv.ofBijective (↑f) hf; { toEquiv := __src.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

@[simp]

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

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

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

Equations

• AlgEquiv.toLinearEquiv e = { toLinearMap := { toAddHom := { toFun := ⇑e, map_add' := ⋯ }, map_smul' := ⋯ }, invFun := ⇑(AlgEquiv.symm e), left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Interpret an algebra equivalence as a linear map.

Equations

• AlgEquiv.toLinearMap e = AlgHom.toLinearMap ↑e

@[simp]

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

def AlgEquiv.ofLinearEquiv {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [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 = { toEquiv := { toFun := ⇑l, invFun := ⇑(LinearEquiv.symm l), left_inv := ⋯, right_inv := ⋯ }, map_mul' := map_mul, map_add' := ⋯, commutes' := ⋯ }

@[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.symm (AlgEquiv.ofLinearEquiv l map_one map_mul) = AlgEquiv.ofLinearEquiv (LinearEquiv.symm l) ⋯ ⋯

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

@[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_symm_apply {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {f : A₁ ≃+* A₂} (hf : ∀ (x : R), f ((algebraMap R A₁) x) = (algebraMap R A₂) x) (a : A₂) : (AlgEquiv.symm (AlgEquiv.ofRingEquiv hf)) a = (RingEquiv.symm f) a

@[simp]

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

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

Promotes a linear ring_equiv to an AlgEquiv.

Equations

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

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

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₁) (ψ : A₁ ≃ₐ[R] A₁) : ϕ * ψ = AlgEquiv.trans ψ ϕ

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

@[simp]

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

@[simp]

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

@[simp]

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

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

An algebra isomorphism induces a group isomorphism between automorphism groups.

This is a more bundled version of AlgEquiv.equivCongr.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

This generalizes Function.End.applyMulAction.

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₁] : SMulCommClass R (A₁ ≃ₐ[R] A₁) A₁

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• AlgEquiv.instMulDistribMulActionAlgEquivUnitsToMonoidToMonoidWithZeroToMonoidToDivInvMonoidAutInstMonoid = 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

@[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 = AlgEquiv.toLinearMap e

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 = { toOneHom := { toFun := AlgEquiv.toLinearMap, map_one' := ⋯ }, map_mul' := ⋯ }

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

@[simp]

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

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

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

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

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.

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Each element of the group defines an algebra equivalence.

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

Equations

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

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)