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) :
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
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 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) :
@[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
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) :
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) :
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
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 alg_hom.map_int_cast {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) (n : ) :
φ n = n
@[simp]
theorem alg_hom.map_inv {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [division_ring A] [division_ring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (x : A) :
φ x⁻¹ = (φ x)⁻¹
@[simp]
theorem alg_hom.map_div {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [division_ring A] [division_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.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₂) :
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₁] :
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₁] :
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) :
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] [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
@[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
@[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₁
@[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₁
@[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₁
@[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
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))
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))
@[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
@[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
@[simp]
theorem alg_equiv.map_inv {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_ring R] [division_ring A₁] [division_ring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₁) :
@[simp]
theorem alg_equiv.map_div {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_ring R] [division_ring A₁] [division_ring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x y : A₁) :
e (x / y) = e x / e y
def mul_semiring_action.to_alg_hom {M : Type u_1} (R : Type u_3) (A : Type u_4) [comm_semiring R] [semiring A] [algebra R A] [monoid M] [mul_semiring_action M A] [smul_comm_class M R A] (m : M) :

Each element of the monoid defines a algebra homomorphism.

This is a stronger version of mul_semiring_action.to_ring_hom and distrib_mul_action.to_linear_map.

Equations
@[simp]
theorem mul_semiring_action.to_alg_hom_apply {M : Type u_1} (R : Type u_3) (A : Type u_4) [comm_semiring R] [semiring A] [algebra R A] [monoid M] [mul_semiring_action M A] [smul_comm_class M R A] (m : M) (ᾰ : A) :
def mul_semiring_action.to_alg_equiv {G : Type u_2} (R : Type u_3) (A : Type u_4) [comm_semiring R] [semiring A] [algebra R A] [group G] [mul_semiring_action G A] [smul_comm_class G R A] (g : G) :

Each element of the group defines a algebra equivalence.

This is a stronger version of mul_semiring_action.to_ring_equiv and distrib_mul_action.to_linear_equiv.

Equations
@[simp]
theorem mul_semiring_action.to_alg_equiv_symm_apply {G : Type u_2} (R : Type u_3) (A : Type u_4) [comm_semiring R] [semiring A] [algebra R A] [group G] [mul_semiring_action G A] [smul_comm_class G R A] (g : G) (ᾰ : A) :
@[simp]
theorem mul_semiring_action.to_alg_equiv_apply {G : Type u_2} (R : Type u_3) (A : Type u_4) [comm_semiring R] [semiring A] [algebra R A] [group G] [mul_semiring_action G A] [smul_comm_class G R A] (g : G) (ᾰ : A) :
@[protected, instance]
def algebra_nat {R : Type u_1} [semiring R] :

Semiring ⥤ ℕ-Alg

Equations
@[protected, instance]
def nat_algebra_subsingleton {R : Type u_1} [semiring R] :
def ring_hom.to_nat_alg_hom {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (f : R →+* S) :

Reinterpret a ring_hom as an -algebra homomorphism.

Equations
def ring_hom.to_int_alg_hom {R : Type u_1} {S : Type u_2} [ring R] [ring S] [algebra R] [algebra S] (f : R →+* S) :

Reinterpret a ring_hom as a -algebra homomorphism.

Equations
@[simp]
theorem ring_hom.map_rat_algebra_map {R : Type u_1} {S : Type u_2} [ring R] [ring S] [algebra R] [algebra S] (f : R →+* S) (r : ) :
def ring_hom.to_rat_alg_hom {R : Type u_1} {S : Type u_2} [ring R] [ring S] [algebra R] [algebra S] (f : R →+* S) :

Reinterpret a ring_hom as a -algebra homomorphism. This actually yields an equivalence, see ring_hom.equiv_rat_alg_hom.

Equations
@[simp]
theorem ring_hom.to_rat_alg_hom_to_ring_hom {R : Type u_1} {S : Type u_2} [ring R] [ring S] [algebra R] [algebra S] (f : R →+* S) :
@[simp]
theorem alg_hom.to_ring_hom_to_rat_alg_hom {R : Type u_1} {S : Type u_2} [ring R] [ring S] [algebra R] [algebra S] (f : R →ₐ[] S) :
def ring_hom.equiv_rat_alg_hom {R : Type u_1} {S : Type u_2} [ring R] [ring S] [algebra R] [algebra S] :
(R →+* S) (R →ₐ[] S)

The equivalence between ring_hom and -algebra homomorphisms.

Equations
@[simp]
theorem ring_hom.equiv_rat_alg_hom_symm_apply {R : Type u_1} {S : Type u_2} [ring R] [ring S] [algebra R] [algebra S] (self : R →ₐ[] S) :
@[simp]
theorem ring_hom.equiv_rat_alg_hom_apply {R : Type u_1} {S : Type u_2} [ring R] [ring S] [algebra R] [algebra S] (f : R →+* S) :
@[protected, instance]
def algebra_rat {α : Type u_1} [division_ring α] [char_zero α] :
Equations
@[simp]
theorem algebra_map_rat_rat  :