mathlib documentation

algebra.algebra.basic

Algebras over commutative semirings #

In this file we define associative unital algebras over commutative (semi)rings, algebra homomorphisms alg_hom, and algebra equivalences alg_equiv.

subalgebras are defined in algebra.algebra.subalgebra.

For the category of R-algebras, denoted Algebra R, see the file algebra/category/Algebra/basic.lean.

See the implementation notes for remarks about non-associative and non-unital algebras.

Main definitions: #

Notations #

Implementation notes #

Given a commutative (semi)ring R, there are two ways to define an R-algebra structure on a (possibly noncommutative) (semi)ring A:

We define algebra R A in a way that subsumes both definitions, by extending has_smul R A and requiring that this scalar action r • x must agree with left multiplication by the image of the structure morphism algebra_map R A r * x.

As a result, there are two ways to talk about an R-algebra A when A is a semiring:

  1. variables [comm_semiring R] [semiring A]
    variables [algebra R A]
    
  2. variables [comm_semiring R] [semiring A]
    variables [module R A] [smul_comm_class R A A] [is_scalar_tower R A A]
    

The first approach implies the second via typeclass search; so any lemma stated with the second set of arguments will automatically apply to the first set. Typeclass search does not know that the second approach implies the first, but this can be shown with:

The advantage of the first approach is that algebra_map R A is available, and alg_hom R A B and subalgebra R A can be used. For concrete R and A, algebra_map R A is often definitionally convenient.

The advantage of the second approach is that comm_semiring R, semiring A, and module R A can all be relaxed independently; for instance, this allows us to:

While alg_hom R A B cannot be used in the second approach, non_unital_alg_hom R A B still can.

You should always use the first approach when working with associative unital algebras, and mimic the second approach only when you need to weaken a condition on either R or A.

@[nolint, class]
structure algebra (R : Type u) (A : Type v) [comm_semiring R] [semiring A] :
Type (max u v)

An associative unital R-algebra is a semiring A equipped with a map into its center R → A.

See the implementation notes in this file for discussion of the details of this definition.

Instances of this typeclass
Instances of other typeclasses for algebra
def algebra_map (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] :
R →+* A

Embedding R →+* A given by algebra structure.

Equations
def ring_hom.to_algebra' {R : Type u_1} {S : Type u_2} [comm_semiring R] [semiring S] (i : R →+* S) (h : ∀ (c : R) (x : S), i c * x = x * i c) :

Creating an algebra from a morphism to the center of a semiring.

Equations
def ring_hom.to_algebra {R : Type u_1} {S : Type u_2} [comm_semiring R] [comm_semiring S] (i : R →+* S) :

Creating an algebra from a morphism to a commutative semiring.

Equations
theorem ring_hom.algebra_map_to_algebra {R : Type u_1} {S : Type u_2} [comm_semiring R] [comm_semiring S] (i : R →+* S) :
@[reducible]
def algebra.of_module' {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [module R A] (h₁ : ∀ (r : R) (x : A), r 1 * x = r x) (h₂ : ∀ (r : R) (x : A), x * r 1 = r x) :

Let R be a commutative semiring, let A be a semiring with a module R structure. If (r • 1) * x = x * (r • 1) = r • x for all r : R and x : A, then A is an algebra over R.

See note [reducible non-instances].

Equations
@[reducible]
def algebra.of_module {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [module R A] (h₁ : ∀ (r : R) (x y : A), r x * y = r (x * y)) (h₂ : ∀ (r : R) (x y : A), x * r y = r (x * y)) :

Let R be a commutative semiring, let A be a semiring with a module R structure. If (r • x) * y = x * (r • y) = r • (x * y) for all r : R and x y : A, then A is an algebra over R.

See note [reducible non-instances].

Equations
@[ext]
theorem algebra.algebra_ext {R : Type u_1} [comm_semiring R] {A : Type u_2} [semiring A] (P Q : algebra R A) (w : ∀ (r : R), (algebra_map R A) r = (algebra_map R A) r) :
P = Q

To prove two algebra structures on a fixed [comm_semiring R] [semiring A] agree, it suffices to check the algebra_maps agree.

@[protected, instance]
def algebra.to_module {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] :
module R A
Equations
theorem algebra.smul_def {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] (r : R) (x : A) :
r x = (algebra_map R A) r * x
theorem algebra.algebra_map_eq_smul_one {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] (r : R) :
(algebra_map R A) r = r 1
theorem algebra.algebra_map_eq_smul_one' {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] :
(algebra_map R A) = λ (r : R), r 1
theorem algebra.commutes {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] (r : R) (x : A) :
(algebra_map R A) r * x = x * (algebra_map R A) r

mul_comm for algebras when one element is from the base ring.

theorem algebra.left_comm {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] (x : A) (r : R) (y : A) :
x * ((algebra_map R A) r * y) = (algebra_map R A) r * (x * y)

mul_left_comm for algebras when one element is from the base ring.

theorem algebra.right_comm {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] (x : A) (r : R) (y : A) :
x * (algebra_map R A) r * y = x * y * (algebra_map R A) r

mul_right_comm for algebras when one element is from the base ring.

@[protected, instance]
def is_scalar_tower.right {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] :
@[protected, simp]
theorem algebra.mul_smul_comm {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] (s : R) (x y : A) :
x * s y = s (x * y)

This is just a special case of the global mul_smul_comm lemma that requires less typeclass search (and was here first).

@[protected, simp]
theorem algebra.smul_mul_assoc {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] (r : R) (x y : A) :
r x * y = r (x * y)

This is just a special case of the global smul_mul_assoc lemma that requires less typeclass search (and was here first).

@[simp]
theorem smul_algebra_map {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] {α : Type u_1} [monoid α] [mul_distrib_mul_action α A] [smul_comm_class α R A] (a : α) (r : R) :
@[simp]
theorem algebra.bit0_smul_one {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] {r : R} :
bit0 r 1 = bit0 (r 1)
theorem algebra.bit0_smul_one' {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] {r : R} :
bit0 r 1 = r 2
@[simp]
theorem algebra.bit0_smul_bit0 {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] {r : R} {a : A} :
bit0 r bit0 a = r bit0 (bit0 a)
@[simp]
theorem algebra.bit0_smul_bit1 {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] {r : R} {a : A} :
bit0 r bit1 a = r bit0 (bit1 a)
@[simp]
theorem algebra.bit1_smul_one {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] {r : R} :
bit1 r 1 = bit1 (r 1)
theorem algebra.bit1_smul_one' {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] {r : R} :
bit1 r 1 = r 2 + 1
@[simp]
theorem algebra.bit1_smul_bit0 {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] {r : R} {a : A} :
bit1 r bit0 a = r bit0 (bit0 a) + bit0 a
@[simp]
theorem algebra.bit1_smul_bit1 {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] {r : R} {a : A} :
bit1 r bit1 a = r bit0 (bit1 a) + bit1 a
@[protected]
def algebra.linear_map (R : Type u) (A : Type w) [comm_semiring R] [semiring A] [algebra R A] :

The canonical ring homomorphism algebra_map R A : R →* A for any R-algebra A, packaged as an R-linear map.

Equations
@[simp]
theorem algebra.linear_map_apply (R : Type u) (A : Type w) [comm_semiring R] [semiring A] [algebra R A] (r : R) :
theorem algebra.coe_linear_map (R : Type u) (A : Type w) [comm_semiring R] [semiring A] [algebra R A] :
@[protected, instance]
def algebra.id (R : Type u) [comm_semiring R] :
Equations
@[simp]
theorem algebra.id.map_eq_id {R : Type u} [comm_semiring R] :
theorem algebra.id.map_eq_self {R : Type u} [comm_semiring R] (x : R) :
(algebra_map R R) x = x
@[simp]
theorem algebra.id.smul_eq_mul {R : Type u} [comm_semiring R] (x y : R) :
x y = x * y
@[protected, instance]
def punit.algebra {R : Type u} [comm_semiring R] :
Equations
@[simp]
theorem algebra.algebra_map_punit {R : Type u} [comm_semiring R] (r : R) :
(algebra_map R punit) r = punit.star
@[protected, instance]
def ulift.algebra {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] :
Equations
theorem ulift.algebra_map_eq {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] (r : R) :
(algebra_map R (ulift A)) r = {down := (algebra_map R A) r}
@[simp]
theorem ulift.down_algebra_map {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] (r : R) :
@[protected, instance]
def prod.algebra (R : Type u) (A : Type w) (B : Type u_1) [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] :
algebra R (A × B)
Equations
@[simp]
theorem algebra.algebra_map_prod_apply {R : Type u} {A : Type w} {B : Type u_1} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (r : R) :
(algebra_map R (A × B)) r = ((algebra_map R A) r, (algebra_map R B) r)
@[protected, instance]
def algebra.of_subsemiring {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] (S : subsemiring R) :

Algebra over a subsemiring. This builds upon subsemiring.module.

Equations
@[protected, instance]
def algebra.of_subring {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [algebra R A] (S : subring R) :

Algebra over a subring. This builds upon subring.module.

Equations
theorem algebra.algebra_map_of_subring {R : Type u_1} [comm_ring R] (S : subring R) :
theorem algebra.algebra_map_of_subring_apply {R : Type u_1} [comm_ring R] (S : subring R) (x : S) :
def algebra.algebra_map_submonoid {R : Type u} [comm_semiring R] (S : Type u_1) [semiring S] [algebra R S] (M : submonoid R) :

Explicit characterization of the submonoid map in the case of an algebra. S is made explicit to help with type inference

Equations
theorem algebra.mem_algebra_map_submonoid_of_mem {R : Type u} [comm_semiring R] {S : Type u_1} [semiring S] [algebra R S] {M : submonoid R} (x : M) :
theorem algebra.mul_sub_algebra_map_commutes {R : Type u} {A : Type w} [comm_semiring R] [ring A] [algebra R A] (x : A) (r : R) :
x * (x - (algebra_map R A) r) = (x - (algebra_map R A) r) * x
theorem algebra.mul_sub_algebra_map_pow_commutes {R : Type u} {A : Type w} [comm_semiring R] [ring A] [algebra R A] (x : A) (r : R) (n : ) :
x * (x - (algebra_map R A) r) ^ n = (x - (algebra_map R A) r) ^ n * x
@[reducible]
def algebra.semiring_to_ring (R : Type u) {A : Type w} [comm_ring R] [semiring A] [algebra R A] :

A semiring that is an algebra over a commutative ring carries a natural ring structure. See note [reducible non-instances].

Equations
@[protected, instance]
def mul_opposite.algebra {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] :
Equations
@[simp]
theorem mul_opposite.algebra_map_apply {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (c : R) :
@[protected, instance]
def module.End.algebra (R : Type u) (M : Type v) [comm_semiring R] [add_comm_monoid M] [module R M] :
Equations
theorem module.algebra_map_End_eq_smul_id (R : Type u) (M : Type v) [comm_semiring R] [add_comm_monoid M] [module R M] (a : R) :
@[simp]
theorem module.algebra_map_End_apply (R : Type u) (M : Type v) [comm_semiring R] [add_comm_monoid M] [module R M] (a : R) (m : M) :
((algebra_map R (module.End R M)) a) m = a m
@[simp]
theorem module.ker_algebra_map_End (K : Type u) (V : Type v) [field K] [add_comm_group V] [module K V] (a : K) (ha : a 0) :
theorem module.End_is_unit_apply_inv_apply_of_is_unit {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] {f : module.End R M} (h : is_unit f) (x : M) :
f ((h.unit.inv) x) = x
theorem module.End_is_unit_inv_apply_apply_of_is_unit {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] {f : module.End R M} (h : is_unit f) (x : M) :
(h.unit.inv) (f x) = x
theorem module.End_is_unit_iff {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (f : module.End R M) :
theorem module.End_algebra_map_is_unit_inv_apply_eq_iff {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] {x : R} (h : is_unit ((algebra_map R (module.End R M)) x)) (m m' : M) :
(h.unit)⁻¹ m = m' m = x m'
theorem module.End_algebra_map_is_unit_inv_apply_eq_iff' {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] {x : R} (h : is_unit ((algebra_map R (module.End R M)) x)) (m m' : M) :
m' = (h.unit)⁻¹ m m = x m'
theorem linear_map.map_algebra_map_mul {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₗ[R] B) (a : A) (r : R) :
f ((algebra_map R A) r * a) = (algebra_map R B) r * f a

An alternate statement of linear_map.map_smul for when algebra_map is more convenient to work with than .

theorem linear_map.map_mul_algebra_map {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₗ[R] B) (a : A) (r : R) :
f (a * (algebra_map R A) r) = f a * (algebra_map R B) r
def alg_hom.to_ring_hom {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

Reinterpret an alg_hom as a ring_hom

@[nolint]
structure alg_hom (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)

Defining the homomorphism in the category R-Alg.

Instances for alg_hom
@[nolint, instance]
def alg_hom_class.to_ring_hom_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_hom_class F R A B] :
@[class]
structure alg_hom_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)

alg_hom_class F R A B asserts F is a type of bundled algebra homomorphisms from A to B.

Instances of this typeclass
Instances of other typeclasses for alg_hom_class
  • alg_hom_class.has_sizeof_inst
@[protected, instance]
def alg_hom_class.linear_map_class {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] {F : Type u_4} [alg_hom_class F R A B] :
Equations
@[protected, instance]
def alg_hom.has_coe_to_fun {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
has_coe_to_fun (A →ₐ[R] B) (λ (_x : A →ₐ[R] B), A → B)
Equations
@[simp]
theorem alg_hom.to_fun_eq_coe {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) :
@[protected, instance]
def alg_hom.alg_hom_class {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
alg_hom_class (A →ₐ[R] B) R A B
Equations
@[protected, instance]
def alg_hom.coe_ring_hom {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
has_coe (A →ₐ[R] B) (A →+* B)
Equations
@[protected, instance]
def alg_hom.coe_monoid_hom {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
has_coe (A →ₐ[R] B) (A →* B)
Equations
@[protected, instance]
def alg_hom.coe_add_monoid_hom {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
has_coe (A →ₐ[R] B) (A →+ B)
Equations
@[simp, norm_cast]
theorem alg_hom.coe_mk {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] {f : A → B} (h₁ : f 1 = 1) (h₂ : ∀ (x y : A), f (x * y) = f x * f y) (h₃ : f 0 = 0) (h₄ : ∀ (x y : A), f (x + y) = f x + f y) (h₅ : ∀ (r : R), f ((algebra_map R A) r) = (algebra_map R B) r) :
{to_fun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅} = f
@[simp]
theorem alg_hom.to_ring_hom_eq_coe {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) :
@[simp, norm_cast]
theorem alg_hom.coe_to_ring_hom {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) :
@[simp, norm_cast]
theorem alg_hom.coe_to_monoid_hom {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) :
@[simp, norm_cast]
theorem alg_hom.coe_to_add_monoid_hom {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) :
theorem alg_hom.coe_fn_injective {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
theorem alg_hom.coe_fn_inj {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] {φ₁ φ₂ : A →ₐ[R] B} :
φ₁ = φ₂ φ₁ = φ₂
theorem alg_hom.coe_ring_hom_injective {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
theorem alg_hom.coe_monoid_hom_injective {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
theorem alg_hom.coe_add_monoid_hom_injective {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
@[protected]
theorem alg_hom.congr_fun {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] {φ₁ φ₂ : A →ₐ[R] B} (H : φ₁ = φ₂) (x : A) :
φ₁ x = φ₂ x
@[protected]
theorem alg_hom.congr_arg {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) {x y : A} (h : x = y) :
φ x = φ y
@[ext]
theorem alg_hom.ext {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] {φ₁ φ₂ : A →ₐ[R] B} (H : ∀ (x : A), φ₁ x = φ₂ x) :
φ₁ = φ₂
theorem alg_hom.ext_iff {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] {φ₁ φ₂ : A →ₐ[R] B} :
φ₁ = φ₂ ∀ (x : A), φ₁ x = φ₂ x
@[simp]
theorem alg_hom.mk_coe {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] {f : A →ₐ[R] B} (h₁ : f 1 = 1) (h₂ : ∀ (x y : A), f (x * y) = f x * f y) (h₃ : f 0 = 0) (h₄ : ∀ (x y : A), f (x + y) = f x + f y) (h₅ : ∀ (r : R), f ((algebra_map R A) r) = (algebra_map R B) r) :
{to_fun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅} = f
@[simp]
theorem alg_hom.commutes {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (r : R) :
φ ((algebra_map R A) r) = (algebra_map R B) r
theorem alg_hom.comp_algebra_map {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) :
@[protected]
theorem alg_hom.map_add {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (r s : A) :
φ (r + s) = φ r + φ s
@[protected]
theorem alg_hom.map_zero {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) :
φ 0 = 0
@[protected]
theorem alg_hom.map_mul {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (x y : A) :
φ (x * y) = φ x * φ y
@[protected]
theorem alg_hom.map_one {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) :
φ 1 = 1
@[protected]
theorem alg_hom.map_pow {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (x : A) (n : ) :
φ (x ^ n) = φ x ^ n
@[protected, simp]
theorem alg_hom.map_smul {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (r : R) (x : A) :
φ (r x) = r φ x
@[protected]
theorem alg_hom.map_sum {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) {ι : Type u_1} (f : ι → A) (s : finset ι) :
φ (s.sum (λ (x : ι), f x)) = s.sum (λ (x : ι), φ (f x))
@[protected]
theorem alg_hom.map_finsupp_sum {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) {α : Type u_1} [has_zero α] {ι : Type u_2} (f : ι →₀ α) (g : ι → α → A) :
φ (f.sum g) = f.sum (λ (i : ι) (a : α), φ (g i a))
@[protected]
theorem alg_hom.map_bit0 {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (x : A) :
φ (bit0 x) = bit0 (φ x)
@[protected]
theorem alg_hom.map_bit1 {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (x : A) :
φ (bit1 x) = bit1 (φ x)
def alg_hom.mk' {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →+* B) (h : ∀ (c : R) (x : A), f (c x) = c f x) :

If a ring_hom is R-linear, then it is an alg_hom.

Equations
@[simp]
theorem alg_hom.coe_mk' {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →+* B) (h : ∀ (c : R) (x : A), f (c x) = c f x) :
@[protected]
def alg_hom.id (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] :

Identity map as an alg_hom.

Equations
@[simp]
theorem alg_hom.coe_id (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] :
@[simp]
theorem alg_hom.id_to_ring_hom (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] :
theorem alg_hom.id_apply {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (p : A) :
(alg_hom.id R A) p = p
def alg_hom.comp {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [comm_semiring R] [semiring A] [semiring B] [semiring C] [algebra R A] [algebra R B] [algebra R C] (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) :

Composition of algebra homeomorphisms.

Equations
@[simp]
theorem alg_hom.coe_comp {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [comm_semiring R] [semiring A] [semiring B] [semiring C] [algebra R A] [algebra R B] [algebra R C] (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) :
(φ₁.comp φ₂) = φ₁ φ₂
theorem alg_hom.comp_apply {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [comm_semiring R] [semiring A] [semiring B] [semiring C] [algebra R A] [algebra R B] [algebra R C] (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) (p : A) :
(φ₁.comp φ₂) p = φ₁ (φ₂ p)
theorem alg_hom.comp_to_ring_hom {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [comm_semiring R] [semiring A] [semiring B] [semiring C] [algebra R A] [algebra R B] [algebra R C] (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) :
(φ₁.comp φ₂) = (φ₁.comp φ₂)
@[simp]
theorem alg_hom.comp_id {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) :
φ.comp (alg_hom.id R A) = φ
@[simp]
theorem alg_hom.id_comp {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) :
(alg_hom.id R B).comp φ = φ
theorem alg_hom.comp_assoc {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} {D : Type v₁} [comm_semiring R] [semiring A] [semiring B] [semiring C] [semiring D] [algebra R A] [algebra R B] [algebra R C] [algebra R D] (φ₁ : C →ₐ[R] D) (φ₂ : B →ₐ[R] C) (φ₃ : A →ₐ[R] B) :
(φ₁.comp φ₂).comp φ₃ = φ₁.comp (φ₂.comp φ₃)
def alg_hom.to_linear_map {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) :

R-Alg ⥤ R-Mod

Equations
@[simp]
theorem alg_hom.to_linear_map_apply {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (p : A) :
theorem alg_hom.to_linear_map_injective {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
@[simp]
theorem alg_hom.comp_to_linear_map {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [comm_semiring R] [semiring A] [semiring B] [semiring C] [algebra R A] [algebra R B] [algebra R C] (f : A →ₐ[R] B) (g : B →ₐ[R] C) :
@[simp]
theorem alg_hom.to_linear_map_id {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
def alg_hom.of_linear_map {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₗ[R] B) (map_one : f 1 = 1) (map_mul : ∀ (x y : A), f (x * y) = f x * f y) :

Promote a linear_map to an alg_hom by supplying proofs about the behavior on 1 and *.

Equations
@[simp]
theorem alg_hom.of_linear_map_apply {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₗ[R] B) (map_one : f 1 = 1) (map_mul : ∀ (x y : A), f (x * y) = f x * f y) (ᾰ : A) :
(alg_hom.of_linear_map f map_one map_mul) = f ᾰ
@[simp]
theorem alg_hom.of_linear_map_to_linear_map {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (map_one : (φ.to_linear_map) 1 = 1) (map_mul : ∀ (x y : A), (φ.to_linear_map) (x * y) = (φ.to_linear_map) x * (φ.to_linear_map) y) :
alg_hom.of_linear_map φ.to_linear_map map_one map_mul = φ
@[simp]
theorem alg_hom.to_linear_map_of_linear_map {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₗ[R] B) (map_one : f 1 = 1) (map_mul : ∀ (x y : A), f (x * y) = f x * f y) :
(alg_hom.of_linear_map f map_one map_mul).to_linear_map = f
@[simp]
theorem alg_hom.of_linear_map_id {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (map_one : linear_map.id 1 = 1) (map_mul : ∀ (x y : A), linear_map.id (x * y) = linear_map.id x * linear_map.id y) :
theorem alg_hom.map_smul_of_tower {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) {R' : Type u_1} [has_smul R' A] [has_smul R' B] [linear_map.compatible_smul A B R' R] (r : R') (x : A) :
φ (r x) = r φ x
theorem alg_hom.map_list_prod {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (s : list A) :
theorem alg_hom.End_mul {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (φ₁ φ₂ : A →ₐ[R] A) :
φ₁ * φ₂ = φ₁.comp φ₂
theorem alg_hom.End_one {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
@[protected, instance]
def alg_hom.End {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
Equations
@[simp]
theorem alg_hom.one_apply {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (x : A) :
1 x = x
@[simp]
theorem alg_hom.mul_apply {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (φ ψ : A →ₐ[R] A) (x : A) :
* ψ) x = φ (ψ x)
def alg_hom.fst (R : Type u) (A : Type v) (B : Type w) [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
A × B →ₐ[R] A

First projection as alg_hom.

Equations
def alg_hom.snd (R : Type u) (A : Type v) (B : Type w) [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
A × B →ₐ[R] B

Second projection as alg_hom.

Equations
def alg_hom.prod {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [comm_semiring R] [semiring A] [semiring B] [semiring C] [algebra R A] [algebra R B] [algebra R C] (f : A →ₐ[R] B) (g : A →ₐ[R] C) :
A →ₐ[R] B × C

The pi.prod of two morphisms is a morphism.

Equations
@[simp]
theorem alg_hom.prod_apply {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [comm_semiring R] [semiring A] [semiring B] [semiring C] [algebra R A] [algebra R B] [algebra R C] (f : A →ₐ[R] B) (g : A →ₐ[R] C) (ᾰ : A) :
theorem alg_hom.coe_prod {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [comm_semiring R] [semiring A] [semiring B] [semiring C] [algebra R A] [algebra R B] [algebra R C] (f : A →ₐ[R] B) (g : A →ₐ[R] C) :
@[simp]
theorem alg_hom.fst_prod {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [comm_semiring R] [semiring A] [semiring B] [semiring C] [algebra R A] [algebra R B] [algebra R C] (f : A →ₐ[R] B) (g : A →ₐ[R] C) :
(alg_hom.fst R B C).comp (f.prod g) = f
@[simp]
theorem alg_hom.snd_prod {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [comm_semiring R] [semiring A] [semiring B] [semiring C] [algebra R A] [algebra R B] [algebra R C] (f : A →ₐ[R] B) (g : A →ₐ[R] C) :
(alg_hom.snd R B C).comp (f.prod g) = g
@[simp]
theorem alg_hom.prod_fst_snd {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
(alg_hom.fst R A B).prod (alg_hom.snd R A B) = 1
@[simp]
theorem alg_hom.prod_equiv_apply {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [comm_semiring R] [semiring A] [semiring B] [semiring C] [algebra R A] [algebra R B] [algebra R C] (f : (A →ₐ[R] B) × (A →ₐ[R] C)) :
@[simp]
theorem alg_hom.prod_equiv_symm_apply {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [comm_semiring R] [semiring A] [semiring B] [semiring C] [algebra R A] [algebra R B] [algebra R C] (f : A →ₐ[R] B × C) :
def alg_hom.prod_equiv {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [comm_semiring R] [semiring A] [semiring B] [semiring C] [algebra R A] [algebra R B] [algebra R C] :
(A →ₐ[R] B) × (A →ₐ[R] C) (A →ₐ[R] B × C)

Taking the product of two maps with the same domain is equivalent to taking the product of their codomains.

Equations
theorem alg_hom.algebra_map_eq_apply {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) {y : R} {x : A} (h : (algebra_map R A) y = x) :
(algebra_map R B) y = f x
@[protected]
theorem alg_hom.map_multiset_prod {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [comm_semiring A] [comm_semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (s : multiset A) :
@[protected]
theorem alg_hom.map_prod {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [comm_semiring A] [comm_semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) {ι : Type u_1} (f : ι → A) (s : finset ι) :
φ (s.prod (λ (x : ι), f x)) = s.prod (λ (x : ι), φ (f x))
@[protected]
theorem alg_hom.map_finsupp_prod {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [comm_semiring A] [comm_semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) {α : Type u_1} [has_zero α] {ι : Type u_2} (f : ι →₀ α) (g : ι → α → A) :
φ (f.prod g) = f.prod (λ (i : ι) (a : α), φ (g i a))
@[protected]
theorem alg_hom.map_neg {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [ring A] [ring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (x : A) :
φ (-x) = -φ x
@[protected]
theorem alg_hom.map_sub {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [ring A] [ring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (x y : A) :
φ (x - y) = φ x - φ y
@[simp]
theorem rat.smul_one_eq_coe {A : Type u_1} [division_ring A] [algebra A] (m : ) :
m 1 = m
@[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
@[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
@[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
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)

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

Instances for alg_equiv
@[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
@[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)

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
Instances of other typeclasses for alg_equiv_class
  • alg_equiv_class.has_sizeof_inst
@[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] :
@[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] :
Equations
@[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] :
Equations
@[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
@[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
@[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
@[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'
@[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
@[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
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)
@[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
@[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
@[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
@[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₂) :
@[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₂) :
@[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₂) :
@[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₂) :
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₂) :
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₂] :
@[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
@[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
@[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
@[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
@[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
@[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
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))
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))
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 has_coe_to_alg_hom instance.

Equations
@[protected, instance]
def alg_equiv.has_coe_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₂] :
has_coe (A₁ ≃ₐ[R] A₂) (A₁ →ₐ[R] A₂)
Equations
@[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₂) :
@[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₂) :
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₂] :
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₂) :

The two paths coercion can take to a ring_hom are equivalent

@[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
@[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₂) :
@[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₂) :
@[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₂) :
@[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
@[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
@[simp]
theorem alg_equiv.refl_to_alg_hom {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :
@[simp]
theorem alg_equiv.coe_refl {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :
@[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
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
@[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₂} :
@[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
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₂] :
@[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
@[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' := _}
@[simp]
theorem alg_equiv.refl_symm {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :
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₁) :
@[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₂) :
@[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
@[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
@[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
@[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)
@[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₁
@[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)
@[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₂) :
@[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₂) :
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₂) :
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₂) :
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
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)
@[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₂] :
@[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₂')
@[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
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
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
@[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
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₁
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
@[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} :
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₁) :
@[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 ᾰ
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
@[simp]
theorem alg_equiv.to_linear_equiv_refl {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :
@[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₂) :
@[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₃) :
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₂] :
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
@[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₂) :
@[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₂) :
@[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₁) :
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₂] :
@[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₃) :
@[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 ᾰ
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
@[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) :
@[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) :
@[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) :
@[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₂) :
@[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₁) :
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
theorem alg_equiv.aut_one {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :
@[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
theorem alg_equiv.aut_mul {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] (ϕ ψ : A₁ ≃ₐ[R] A₁) :
ϕ * ψ = ψ.trans ϕ
@[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
@[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)
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
@[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 ϕ)
@[simp]
theorem alg_equiv.aut_congr_refl {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :
@[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₂) :
@[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₃) :
@[protected, instance]
def alg_equiv.apply_mul_semiring_action {R : Type u} {A₁ : Type v} [comm_semiring R] <