algebra.algebra.equiv - mathlib docs

@[nolint]

def alg_equiv.to_add_equiv {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (self : A ≃ₐ[R] B) :

A ≃+ B

source

@[nolint]

def alg_equiv.to_equiv {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (self : A ≃ₐ[R] B) :

A ≃ B

source

@[nolint]

def alg_equiv.to_ring_equiv {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (self : A ≃ₐ[R] B) :

A ≃+* B

source

structure alg_equiv (R : Type u) (A : Type v) (B : Type w) [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :

Type (max v w)

to_fun : A → B
inv_fun : B → A
left_inv : function.left_inverse self.inv_fun self.to_fun
right_inv : function.right_inverse self.inv_fun self.to_fun
map_mul' : ∀ (x y : A), self.to_fun (x * y) = self.to_fun x * self.to_fun y
map_add' : ∀ (x y : A), self.to_fun (x + y) = self.to_fun x + self.to_fun y
commutes' : ∀ (r : R), self.to_fun (⇑(algebra_map R A) r) = ⇑(algebra_map R B) r

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

Instances for alg_equiv

source

@[nolint]

def alg_equiv.to_mul_equiv {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (self : A ≃ₐ[R] B) :

A ≃* B

source

@[class]

structure alg_equiv_class (F : Type u_1) (R : out_param (Type u_2)) (A : out_param (Type u_3)) (B : out_param (Type u_4)) [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :

Type (max u_1 u_3 u_4)

coe : F → A → B
inv : F → B → A
left_inv : ∀ (e : F), function.left_inverse (alg_equiv_class.inv e) (alg_equiv_class.coe e)
right_inv : ∀ (e : F), function.right_inverse (alg_equiv_class.inv e) (alg_equiv_class.coe e)
coe_injective' : ∀ (e g : F), alg_equiv_class.coe e = alg_equiv_class.coe g → alg_equiv_class.inv e = alg_equiv_class.inv g → e = g
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 (⇑(algebra_map R A) r) = ⇑(algebra_map R B) r

alg_equiv_class F R A B states that F is a type of algebra structure preserving equivalences. You should extend this class when you extend alg_equiv.

Instances of this typeclass

alg_equiv.alg_equiv_class

Instances of other typeclasses for alg_equiv_class

alg_equiv_class.has_sizeof_inst

source

@[nolint, instance]

def alg_equiv_class.to_ring_equiv_class (F : Type u_1) (R : out_param (Type u_2)) (A : out_param (Type u_3)) (B : out_param (Type u_4)) [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] [self : alg_equiv_class F R A B] :

ring_equiv_class F A B

source

@[protected, instance]

def alg_equiv_class.to_alg_hom_class (F : Type u_1) (R : Type u_2) (A : Type u_3) (B : Type u_4) [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] [h : alg_equiv_class F R A B] :

alg_hom_class F R A B

Equations

alg_equiv_class.to_alg_hom_class F R A B = {coe := coe_fn fun_like.has_coe_to_fun, coe_injective' := _, map_mul := _, map_one := _, map_add := _, map_zero := _, commutes := _}

source

@[protected, instance]

def alg_equiv_class.to_linear_equiv_class (F : Type u_1) (R : Type u_2) (A : Type u_3) (B : Type u_4) [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] [h : alg_equiv_class F R A B] :

linear_equiv_class F R A B

Equations

alg_equiv_class.to_linear_equiv_class F R A B = {coe := alg_equiv_class.coe h, inv := alg_equiv_class.inv h, left_inv := _, right_inv := _, coe_injective' := _, map_add := _, map_smulₛₗ := _}

source

@[protected, instance]

def alg_equiv_class.alg_equiv.has_coe_t (F : Type u_1) (R : Type u_2) (A : Type u_3) (B : Type u_4) [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] [h : alg_equiv_class F R A B] :

has_coe_t F (A ≃ₐ[R] B)

Equations

alg_equiv_class.alg_equiv.has_coe_t F R A B = {coe := λ (f : F), {to_fun := ⇑f, inv_fun := equiv_like.inv f, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}}

source

@[protected, instance]

def alg_equiv.alg_equiv_class {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] :

alg_equiv_class (A₁ ≃ₐ[R] A₂) R A₁ A₂

Equations

alg_equiv.alg_equiv_class = {coe := alg_equiv.to_fun _inst_6, inv := alg_equiv.inv_fun _inst_6, left_inv := _, right_inv := _, coe_injective' := _, map_mul := _, map_add := _, commutes := _}

source

@[protected, instance]

def alg_equiv.has_coe_to_fun {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] :

has_coe_to_fun (A₁ ≃ₐ[R] A₂) (λ (_x : A₁ ≃ₐ[R] A₂), A₁ → A₂)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations

alg_equiv.has_coe_to_fun = {coe := alg_equiv.to_fun _inst_6}

source

@[protected, simp]

theorem alg_equiv.coe_coe {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] {F : Type u_1} [alg_equiv_class F R A₁ A₂] (f : F) :

⇑↑f = ⇑f

source

@[ext]

theorem alg_equiv.ext {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring 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

@[protected]

theorem alg_equiv.congr_arg {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring 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

@[protected]

theorem alg_equiv.congr_fun {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring 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

@[protected]

theorem alg_equiv.ext_iff {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] {f g : A₁ ≃ₐ[R] A₂} :

f = g ↔ ∀ (x : A₁), ⇑f x = ⇑g x

source

theorem alg_equiv.coe_fun_injective {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] :

function.injective (λ (e : A₁ ≃ₐ[R] A₂), ⇑e)

source

@[protected, instance]

def alg_equiv.has_coe_to_ring_equiv {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] :

has_coe (A₁ ≃ₐ[R] A₂) (A₁ ≃+* A₂)

Equations

alg_equiv.has_coe_to_ring_equiv = {coe := alg_equiv.to_ring_equiv _inst_6}

source

@[simp]

theorem alg_equiv.coe_mk {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] {to_fun : A₁ → A₂} {inv_fun : A₂ → A₁} {left_inv : function.left_inverse inv_fun to_fun} {right_inv : function.right_inverse inv_fun to_fun} {map_mul : ∀ (x y : A₁), to_fun (x * y) = to_fun x * to_fun y} {map_add : ∀ (x y : A₁), to_fun (x + y) = to_fun x + to_fun y} {commutes : ∀ (r : R), to_fun (⇑(algebra_map R A₁) r) = ⇑(algebra_map R A₂) r} :

⇑{to_fun := to_fun, inv_fun := inv_fun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul, map_add' := map_add, commutes' := commutes} = to_fun

source

@[simp]

theorem alg_equiv.mk_coe {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (e' : A₂ → A₁) (h₁ : function.left_inverse e' ⇑e) (h₂ : function.right_inverse e' ⇑e) (h₃ : ∀ (x y : A₁), ⇑e (x * y) = ⇑e x * ⇑e y) (h₄ : ∀ (x y : A₁), ⇑e (x + y) = ⇑e x + ⇑e y) (h₅ : ∀ (r : R), ⇑e (⇑(algebra_map R A₁) r) = ⇑(algebra_map R A₂) r) :

{to_fun := ⇑e, inv_fun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, commutes' := h₅} = e

source

@[simp]

theorem alg_equiv.to_fun_eq_coe {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :

e.to_fun = ⇑e

source

@[simp]

theorem alg_equiv.to_equiv_eq_coe {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :

e.to_equiv = ↑e

source

@[simp]

theorem alg_equiv.to_ring_equiv_eq_coe {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :

e.to_ring_equiv = ↑e

source

@[simp, norm_cast]

theorem alg_equiv.coe_ring_equiv {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :

⇑↑e = ⇑e

source

theorem alg_equiv.coe_ring_equiv' {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :

⇑(e.to_ring_equiv) = ⇑e

source

theorem alg_equiv.coe_ring_equiv_injective {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] :

function.injective coe

source

@[protected]

theorem alg_equiv.map_add {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring 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

@[protected]

theorem alg_equiv.map_zero {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :

⇑e 0 = 0

source

@[protected]

theorem alg_equiv.map_mul {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring 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

@[protected]

theorem alg_equiv.map_one {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :

⇑e 1 = 1

source

@[simp]

theorem alg_equiv.commutes {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (r : R) :

⇑e (⇑(algebra_map R A₁) r) = ⇑(algebra_map R A₂) r

source

@[simp]

theorem alg_equiv.map_smul {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring 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

theorem alg_equiv.map_sum {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) {ι : Type u_1} (f : ι → A₁) (s : finset ι) :

⇑e (s.sum (λ (x : ι), f x)) = s.sum (λ (x : ι), ⇑e (f x))

source

theorem alg_equiv.map_finsupp_sum {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) {α : Type u_1} [has_zero α] {ι : Type u_2} (f : ι →₀ α) (g : ι → α → A₁) :

⇑e (f.sum g) = f.sum (λ (i : ι) (b : α), ⇑e (g i b))

source

def alg_equiv.to_alg_hom {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring 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 alg_hom_class.has_coe_t instance.

Equations

e.to_alg_hom = {to_fun := e.to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

source

@[simp]

theorem alg_equiv.to_alg_hom_eq_coe {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :

e.to_alg_hom = ↑e

source

@[simp, norm_cast]

theorem alg_equiv.coe_alg_hom {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :

⇑↑e = ⇑e

source

theorem alg_equiv.coe_alg_hom_injective {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] :

function.injective coe

source

theorem alg_equiv.coe_ring_hom_commutes {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring 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 ring_hom are equivalent

source

@[protected]

theorem alg_equiv.map_pow {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring 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

@[protected]

theorem alg_equiv.injective {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :

function.injective ⇑e

source

@[protected]

theorem alg_equiv.surjective {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :

function.surjective ⇑e

source

@[protected]

theorem alg_equiv.bijective {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :

function.bijective ⇑e

source

@[refl]

def alg_equiv.refl {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :

A₁ ≃ₐ[R] A₁

Algebra equivalences are reflexive.

Equations

alg_equiv.refl = {to_fun := 1.to_fun, inv_fun := 1.inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

source

@[protected, instance]

def alg_equiv.inhabited {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :

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

Equations

alg_equiv.inhabited = {default := alg_equiv.refl _inst_5}

source

@[simp]

theorem alg_equiv.refl_to_alg_hom {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :

↑alg_equiv.refl = alg_hom.id R A₁

source

@[simp]

theorem alg_equiv.coe_refl {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :

⇑alg_equiv.refl = id

source

@[symm]

def alg_equiv.symm {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring 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 = {to_fun := e.to_ring_equiv.symm.to_fun, inv_fun := e.to_ring_equiv.symm.inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

source

def alg_equiv.simps.symm_apply {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :

A₂ → A₁

See Note [custom simps projection]

Equations

alg_equiv.simps.symm_apply e = ⇑(e.symm)

source

@[simp]

theorem alg_equiv.coe_apply_coe_coe_symm_apply {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] {F : Type u_1} [alg_equiv_class F R A₁ A₂] (f : F) (x : A₂) :

⇑f (⇑(↑f.symm) x) = x

source

@[simp]

theorem alg_equiv.coe_coe_symm_apply_coe_apply {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] {F : Type u_1} [alg_equiv_class F R A₁ A₂] (f : F) (x : A₁) :

⇑(↑f.symm) (⇑f x) = x

source

@[simp]

theorem alg_equiv.inv_fun_eq_symm {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] {e : A₁ ≃ₐ[R] A₂} :

e.inv_fun = ⇑(e.symm)

source

@[simp]

theorem alg_equiv.symm_symm {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :

e.symm.symm = e

source

theorem alg_equiv.symm_bijective {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] :

function.bijective alg_equiv.symm

source

@[simp]

theorem alg_equiv.mk_coe' {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (f : A₂ → A₁) (h₁ : function.left_inverse ⇑e f) (h₂ : function.right_inverse ⇑e f) (h₃ : ∀ (x y : A₂), f (x * y) = f x * f y) (h₄ : ∀ (x y : A₂), f (x + y) = f x + f y) (h₅ : ∀ (r : R), f (⇑(algebra_map R A₂) r) = ⇑(algebra_map R A₁) r) :

{to_fun := f, inv_fun := ⇑e, left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, commutes' := h₅} = e.symm

source

@[simp]

theorem alg_equiv.symm_mk {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (f : A₁ → A₂) (f' : A₂ → A₁) (h₁ : function.left_inverse f' f) (h₂ : function.right_inverse f' f) (h₃ : ∀ (x y : A₁), f (x * y) = f x * f y) (h₄ : ∀ (x y : A₁), f (x + y) = f x + f y) (h₅ : ∀ (r : R), f (⇑(algebra_map R A₁) r) = ⇑(algebra_map R A₂) r) :

{to_fun := f, inv_fun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, commutes' := h₅}.symm = {to_fun := f', inv_fun := f, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

source

@[simp]

theorem alg_equiv.refl_symm {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :

alg_equiv.refl.symm = alg_equiv.refl

source

theorem alg_equiv.to_ring_equiv_symm {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] (f : A₁ ≃ₐ[R] A₁) :

↑f.symm = ↑(f.symm)

source

@[simp]

theorem alg_equiv.symm_to_ring_equiv {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :

↑(e.symm) = ↑e.symm

source

@[trans]

def alg_equiv.trans {R : Type u} {A₁ : Type v} {A₂ : Type w} {A₃ : Type u₁} [comm_semiring 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₂ = {to_fun := (e₁.to_ring_equiv.trans e₂.to_ring_equiv).to_fun, inv_fun := (e₁.to_ring_equiv.trans e₂.to_ring_equiv).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

source

@[simp]

theorem alg_equiv.apply_symm_apply {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring 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 alg_equiv.symm_apply_apply {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₁) :

⇑(e.symm) (⇑e x) = x

source

@[simp]

theorem alg_equiv.symm_trans_apply {R : Type u} {A₁ : Type v} {A₂ : Type w} {A₃ : Type u₁} [comm_semiring 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

@[simp]

theorem alg_equiv.coe_trans {R : Type u} {A₁ : Type v} {A₂ : Type w} {A₃ : Type u₁} [comm_semiring 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 alg_equiv.trans_apply {R : Type u} {A₁ : Type v} {A₂ : Type w} {A₃ : Type u₁} [comm_semiring 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 alg_equiv.comp_symm {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :

↑e.comp ↑(e.symm) = alg_hom.id R A₂

source

@[simp]

theorem alg_equiv.symm_comp {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :

↑(e.symm).comp ↑e = alg_hom.id R A₁

source

theorem alg_equiv.left_inverse_symm {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :

function.left_inverse ⇑(e.symm) ⇑e

source

theorem alg_equiv.right_inverse_symm {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :

function.right_inverse ⇑(e.symm) ⇑e

source

def alg_equiv.arrow_congr {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] {A₁' : Type u_1} {A₂' : Type u_2} [semiring A₁'] [semiring 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₁.arrow_congr e₂ = {to_fun := λ (f : A₁ →ₐ[R] A₂), (e₂.to_alg_hom.comp f).comp e₁.symm.to_alg_hom, inv_fun := λ (f : A₁' →ₐ[R] A₂'), (e₂.symm.to_alg_hom.comp f).comp e₁.to_alg_hom, left_inv := _, right_inv := _}

source

theorem alg_equiv.arrow_congr_comp {R : Type u} {A₁ : Type v} {A₂ : Type w} {A₃ : Type u₁} [comm_semiring R] [semiring A₁] [semiring A₂] [semiring A₃] [algebra R A₁] [algebra R A₂] [algebra R A₃] {A₁' : Type u_1} {A₂' : Type u_2} {A₃' : Type u_3} [semiring A₁'] [semiring A₂'] [semiring 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₁.arrow_congr e₃) (g.comp f) = (⇑(e₂.arrow_congr e₃) g).comp (⇑(e₁.arrow_congr e₂) f)

source

@[simp]

theorem alg_equiv.arrow_congr_refl {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] :

alg_equiv.refl.arrow_congr alg_equiv.refl = equiv.refl (A₁ →ₐ[R] A₂)

source

@[simp]

theorem alg_equiv.arrow_congr_trans {R : Type u} {A₁ : Type v} {A₂ : Type w} {A₃ : Type u₁} [comm_semiring R] [semiring A₁] [semiring A₂] [semiring A₃] [algebra R A₁] [algebra R A₂] [algebra R A₃] {A₁' : Type u_1} {A₂' : Type u_2} {A₃' : Type u_3} [semiring A₁'] [semiring A₂'] [semiring 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₂).arrow_congr (e₁'.trans e₂') = (e₁.arrow_congr e₁').trans (e₂.arrow_congr e₂')

source

@[simp]

theorem alg_equiv.arrow_congr_symm {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] {A₁' : Type u_1} {A₂' : Type u_2} [semiring A₁'] [semiring A₂'] [algebra R A₁'] [algebra R A₂'] (e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂') :

(e₁.arrow_congr e₂).symm = e₁.symm.arrow_congr e₂.symm

source

def alg_equiv.of_alg_hom {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : f.comp g = alg_hom.id R A₂) (h₂ : g.comp f = alg_hom.id R A₁) :

A₁ ≃ₐ[R] A₂

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

Equations

alg_equiv.of_alg_hom f g h₁ h₂ = {to_fun := ⇑f, inv_fun := ⇑g, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

source

theorem alg_equiv.coe_alg_hom_of_alg_hom {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : f.comp g = alg_hom.id R A₂) (h₂ : g.comp f = alg_hom.id R A₁) :

↑(alg_equiv.of_alg_hom f g h₁ h₂) = f

source

@[simp]

theorem alg_equiv.of_alg_hom_coe_alg_hom {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (f : A₁ ≃ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : ↑f.comp g = alg_hom.id R A₂) (h₂ : g.comp ↑f = alg_hom.id R A₁) :

alg_equiv.of_alg_hom ↑f g h₁ h₂ = f

source

theorem alg_equiv.of_alg_hom_symm {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : f.comp g = alg_hom.id R A₂) (h₂ : g.comp f = alg_hom.id R A₁) :

(alg_equiv.of_alg_hom f g h₁ h₂).symm = alg_equiv.of_alg_hom g f h₂ h₁

source

noncomputable def alg_equiv.of_bijective {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring 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

alg_equiv.of_bijective f hf = {to_fun := (ring_equiv.of_bijective ↑f hf).to_fun, inv_fun := (ring_equiv.of_bijective ↑f hf).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

source

@[simp]

theorem alg_equiv.coe_of_bijective {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] {f : A₁ →ₐ[R] A₂} {hf : function.bijective ⇑f} :

⇑(alg_equiv.of_bijective f hf) = ⇑f

source

theorem alg_equiv.of_bijective_apply {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] {f : A₁ →ₐ[R] A₂} {hf : function.bijective ⇑f} (a : A₁) :

⇑(alg_equiv.of_bijective f hf) a = ⇑f a

source

@[simp]

theorem alg_equiv.to_linear_equiv_apply {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (ᾰ : A₁) :

⇑(e.to_linear_equiv) ᾰ = ⇑e ᾰ

source

def alg_equiv.to_linear_equiv {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring 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.to_linear_equiv = {to_fun := ⇑e, map_add' := _, map_smul' := _, inv_fun := ⇑(e.symm), left_inv := _, right_inv := _}

source

@[simp]

theorem alg_equiv.to_linear_equiv_refl {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :

alg_equiv.refl.to_linear_equiv = linear_equiv.refl R A₁

source

@[simp]

theorem alg_equiv.to_linear_equiv_symm {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :

e.to_linear_equiv.symm = e.symm.to_linear_equiv

source

@[simp]

theorem alg_equiv.to_linear_equiv_trans {R : Type u} {A₁ : Type v} {A₂ : Type w} {A₃ : Type u₁} [comm_semiring 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₂).to_linear_equiv = e₁.to_linear_equiv.trans e₂.to_linear_equiv

source

theorem alg_equiv.to_linear_equiv_injective {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] :

function.injective alg_equiv.to_linear_equiv

source

def alg_equiv.to_linear_map {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring 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.to_linear_map = e.to_alg_hom.to_linear_map

source

@[simp]

theorem alg_equiv.to_alg_hom_to_linear_map {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :

↑e.to_linear_map = e.to_linear_map

source

@[simp]

theorem alg_equiv.to_linear_equiv_to_linear_map {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :

e.to_linear_equiv.to_linear_map = e.to_linear_map

source

@[simp]

theorem alg_equiv.to_linear_map_apply {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₁) :

⇑(e.to_linear_map) x = ⇑e x

source

theorem alg_equiv.to_linear_map_injective {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] :

function.injective alg_equiv.to_linear_map

source

@[simp]

theorem alg_equiv.trans_to_linear_map {R : Type u} {A₁ : Type v} {A₂ : Type w} {A₃ : Type u₁} [comm_semiring 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).to_linear_map = g.to_linear_map.comp f.to_linear_map

source

@[simp]

theorem alg_equiv.of_linear_equiv_apply {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (l : A₁ ≃ₗ[R] A₂) (map_mul : ∀ (x y : A₁), ⇑l (x * y) = ⇑l x * ⇑l y) (commutes : ∀ (r : R), ⇑l (⇑(algebra_map R A₁) r) = ⇑(algebra_map R A₂) r) (ᾰ : A₁) :

⇑(alg_equiv.of_linear_equiv l map_mul commutes) ᾰ = ⇑l ᾰ

source

def alg_equiv.of_linear_equiv {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (l : A₁ ≃ₗ[R] A₂) (map_mul : ∀ (x y : A₁), ⇑l (x * y) = ⇑l x * ⇑l y) (commutes : ∀ (r : R), ⇑l (⇑(algebra_map R A₁) r) = ⇑(algebra_map R A₂) r) :

A₁ ≃ₐ[R] A₂

Upgrade a linear equivalence to an algebra equivalence, given that it distributes over multiplication and action of scalars.

Equations

alg_equiv.of_linear_equiv l map_mul commutes = {to_fun := ⇑l, inv_fun := ⇑(l.symm), left_inv := _, right_inv := _, map_mul' := map_mul, map_add' := _, commutes' := commutes}

source

@[simp]

theorem alg_equiv.of_linear_equiv_symm {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (l : A₁ ≃ₗ[R] A₂) (map_mul : ∀ (x y : A₁), ⇑l (x * y) = ⇑l x * ⇑l y) (commutes : ∀ (r : R), ⇑l (⇑(algebra_map R A₁) r) = ⇑(algebra_map R A₂) r) :

(alg_equiv.of_linear_equiv l map_mul commutes).symm = alg_equiv.of_linear_equiv l.symm _ _

source

@[simp]

theorem alg_equiv.of_linear_equiv_to_linear_equiv {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (map_mul : ∀ (x y : A₁), ⇑(e.to_linear_equiv) (x * y) = ⇑(e.to_linear_equiv) x * ⇑(e.to_linear_equiv) y) (commutes : ∀ (r : R), ⇑(e.to_linear_equiv) (⇑(algebra_map R A₁) r) = ⇑(algebra_map R A₂) r) :

alg_equiv.of_linear_equiv e.to_linear_equiv map_mul commutes = e

source

@[simp]

theorem alg_equiv.to_linear_equiv_of_linear_equiv {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (l : A₁ ≃ₗ[R] A₂) (map_mul : ∀ (x y : A₁), ⇑l (x * y) = ⇑l x * ⇑l y) (commutes : ∀ (r : R), ⇑l (⇑(algebra_map R A₁) r) = ⇑(algebra_map R A₂) r) :

(alg_equiv.of_linear_equiv l map_mul commutes).to_linear_equiv = l

source

@[simp]

theorem alg_equiv.of_ring_equiv_symm_apply {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] {f : A₁ ≃+* A₂} (hf : ∀ (x : R), ⇑f (⇑(algebra_map R A₁) x) = ⇑(algebra_map R A₂) x) (ᾰ : A₂) :

⇑((alg_equiv.of_ring_equiv hf).symm) ᾰ = ⇑(f.symm) ᾰ

source

@[simp]

theorem alg_equiv.of_ring_equiv_apply {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] {f : A₁ ≃+* A₂} (hf : ∀ (x : R), ⇑f (⇑(algebra_map R A₁) x) = ⇑(algebra_map R A₂) x) (ᾰ : A₁) :

⇑(alg_equiv.of_ring_equiv hf) ᾰ = ⇑f ᾰ

source

def alg_equiv.of_ring_equiv {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] {f : A₁ ≃+* A₂} (hf : ∀ (x : R), ⇑f (⇑(algebra_map R A₁) x) = ⇑(algebra_map R A₂) x) :

A₁ ≃ₐ[R] A₂

Promotes a linear ring_equiv to an alg_equiv.

Equations

alg_equiv.of_ring_equiv hf = {to_fun := ⇑f, inv_fun := ⇑(f.symm), left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := hf}

source

theorem alg_equiv.aut_one {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :

1 = alg_equiv.refl

source

@[protected, instance]

def alg_equiv.aut {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :

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

Equations

alg_equiv.aut = {mul := λ (ϕ ψ : A₁ ≃ₐ[R] A₁), ψ.trans ϕ, mul_assoc := _, one := alg_equiv.refl _inst_5, one_mul := _, mul_one := _, npow := div_inv_monoid.npow._default alg_equiv.refl (λ (ϕ ψ : A₁ ≃ₐ[R] A₁), ψ.trans ϕ) alg_equiv.aut._proof_4 alg_equiv.aut._proof_5, npow_zero' := _, npow_succ' := _, inv := alg_equiv.symm _inst_5, div := div_inv_monoid.div._default (λ (ϕ ψ : A₁ ≃ₐ[R] A₁), ψ.trans ϕ) alg_equiv.aut._proof_8 alg_equiv.refl alg_equiv.aut._proof_9 alg_equiv.aut._proof_10 (div_inv_monoid.npow._default alg_equiv.refl (λ (ϕ ψ : A₁ ≃ₐ[R] A₁), ψ.trans ϕ) alg_equiv.aut._proof_4 alg_equiv.aut._proof_5) alg_equiv.aut._proof_11 alg_equiv.aut._proof_12 alg_equiv.symm, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default (λ (ϕ ψ : A₁ ≃ₐ[R] A₁), ψ.trans ϕ) alg_equiv.aut._proof_14 alg_equiv.refl alg_equiv.aut._proof_15 alg_equiv.aut._proof_16 (div_inv_monoid.npow._default alg_equiv.refl (λ (ϕ ψ : A₁ ≃ₐ[R] A₁), ψ.trans ϕ) alg_equiv.aut._proof_4 alg_equiv.aut._proof_5) alg_equiv.aut._proof_17 alg_equiv.aut._proof_18 alg_equiv.symm, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}

source

theorem alg_equiv.aut_mul {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] (ϕ ψ : A₁ ≃ₐ[R] A₁) :

ϕ * ψ = ψ.trans ϕ

source

@[simp]

theorem alg_equiv.one_apply {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] (x : A₁) :

⇑1 x = x

source

@[simp]

theorem alg_equiv.mul_apply {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] (e₁ e₂ : A₁ ≃ₐ[R] A₁) (x : A₁) :

⇑(e₁ * e₂) x = ⇑e₁ (⇑e₂ x)

source

def alg_equiv.aut_congr {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring 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

Equations

ϕ.aut_congr = {to_fun := λ (ψ : A₁ ≃ₐ[R] A₁), ϕ.symm.trans (ψ.trans ϕ), inv_fun := λ (ψ : A₂ ≃ₐ[R] A₂), ϕ.trans (ψ.trans ϕ.symm), left_inv := _, right_inv := _, map_mul' := _}

source

@[simp]

theorem alg_equiv.aut_congr_apply {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (ϕ : A₁ ≃ₐ[R] A₂) (ψ : A₁ ≃ₐ[R] A₁) :

⇑(ϕ.aut_congr) ψ = ϕ.symm.trans (ψ.trans ϕ)

source

@[simp]

theorem alg_equiv.aut_congr_refl {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :

alg_equiv.refl.aut_congr = mul_equiv.refl (A₁ ≃ₐ[R] A₁)

source

@[simp]

theorem alg_equiv.aut_congr_symm {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (ϕ : A₁ ≃ₐ[R] A₂) :

ϕ.aut_congr.symm = ϕ.symm.aut_congr

source

@[simp]

theorem alg_equiv.aut_congr_trans {R : Type u} {A₁ : Type v} {A₂ : Type w} {A₃ : Type u₁} [comm_semiring R] [semiring A₁] [semiring A₂] [semiring A₃] [algebra R A₁] [algebra R A₂] [algebra R A₃] (ϕ : A₁ ≃ₐ[R] A₂) (ψ : A₂ ≃ₐ[R] A₃) :

ϕ.aut_congr.trans ψ.aut_congr = (ϕ.trans ψ).aut_congr

source

@[protected, instance]

def alg_equiv.apply_mul_semiring_action {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :

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

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

This generalizes function.End.apply_mul_action.

Equations

alg_equiv.apply_mul_semiring_action = {to_distrib_mul_action := {to_mul_action := {to_has_smul := {smul := λ (_x : A₁ ≃ₐ[R] A₁) (_y : A₁), ⇑_x _y}, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}, smul_one := _, smul_mul := _}

source

@[protected, simp]

theorem alg_equiv.smul_def {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] (f : A₁ ≃ₐ[R] A₁) (a : A₁) :

f • a = ⇑f a

source

@[protected, instance]

def alg_equiv.apply_has_faithful_smul {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :

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

source

@[protected, instance]

def alg_equiv.apply_smul_comm_class {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :

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

source

@[protected, instance]

def alg_equiv.apply_smul_comm_class' {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :

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

source

@[simp]

theorem alg_equiv.algebra_map_eq_apply {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) {y : R} {x : A₁} :

⇑(algebra_map R A₂) y = ⇑e x ↔ ⇑(algebra_map R A₁) y = x

source

theorem alg_equiv.map_prod {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [comm_semiring A₁] [comm_semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) {ι : Type u_1} (f : ι → A₁) (s : finset ι) :

⇑e (s.prod (λ (x : ι), f x)) = s.prod (λ (x : ι), ⇑e (f x))

source

theorem alg_equiv.map_finsupp_prod {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [comm_semiring A₁] [comm_semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) {α : Type u_1} [has_zero α] {ι : Type u_2} (f : ι →₀ α) (g : ι → α → A₁) :

⇑e (f.prod g) = f.prod (λ (i : ι) (a : α), ⇑e (g i a))

source

@[protected]

theorem alg_equiv.map_neg {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [ring A₁] [ring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₁) :

⇑e (-x) = -⇑e x

source

@[protected]

theorem alg_equiv.map_sub {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring 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

source