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_scalar 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
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 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.mul_sub_algebra_map_commutes {R : Type u} {A : Type w} [comm_ring 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_ring 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

If algebra_map R A is injective and A has no zero divisors, R-multiples in A are zero only if one of the factors is zero.

Cannot be an instance because there is no injective (algebra_map R A) typeclass.

@[protected, instance]
@[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.

@[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.ring_hom_class {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R 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) :
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
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
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
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
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
@[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
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 ι) :
φ (∑ (x : ι) in s, f x) = ∑ (x : ι) in s, φ (f x)
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))
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)
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_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
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) :
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 ι) :
φ (∏ (x : ι) in s, f x) = ∏ (x : ι) in s, φ (f x)
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))
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
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_ring 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_ring R] [division_ring A] [division_ring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (x y : A) :
φ (x / y) = φ x / φ y
theorem alg_hom.injective_iff {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_semiring R] [ring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) :
function.injective f ∀ (x : A), f x = 0x = 0
@[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.

@[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
@[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₂)
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
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_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₂] :
@[simp]
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
@[simp]
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
@[simp]
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
@[simp]
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 (∑ (x : ι) in s, f x) = ∑ (x : ι) in s, 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

@[simp]
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
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₂) :
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₂) :
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₂) :
@[protected, instance]
def alg_equiv.has_one {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :
has_one (A₁ ≃ₐ[R] A₁)
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
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
@[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' := _}
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₁
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) :
@[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
@[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_scalar {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :
has_faithful_scalar (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 (∏ (x : ι) in s, f x) = ∏ (x : ι) in s, 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))
@[simp]
theorem alg_equiv.map_neg {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_ring R] [ring A₁] [ring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₁) :
e (-x) = -e x
@[simp]
theorem alg_equiv.map_sub {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_ring 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.

Equations
@[protected, instance]
def algebra_rat {α : Type u_1} [division_ring α] [char_zero α] :
Equations
theorem algebra_rat_subsingleton {α : Type u_1} [semiring α] :
def algebra.of_id (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] :

algebra_map as an alg_hom.

Equations
theorem algebra.of_id_apply {R : Type u} (A : Type v) [comm_semiring R] [semiring A] [algebra R A] (r : R) :
@[protected, instance]
def algebra_int (R : Type u_1) [ring R] :

Ring ⥤ ℤ-Alg

Equations
@[simp]
theorem algebra_map_int_eq (R : Type u_1) [ring R] :

A special case of ring_hom.eq_int_cast' that happens to be true definitionally

@[protected, instance]
def int_algebra_subsingleton {R : Type u_1} [ring R] :

The R-algebra structure on Π i : I, A i when each A i is an R-algebra.

We couldn't set this up back in algebra.pi_instances because this file imports it.

@[protected, instance]
def pi.algebra (I : Type u) {R : Type u_1} (f : I → Type v) {r : comm_semiring R} [s : Π (i : I), semiring (f i)] [Π (i : I), algebra R (f i)] :
algebra R (Π (i : I), f i)
Equations
@[simp]
theorem pi.algebra_map_apply (I : Type u) {R : Type u_1} (f : I → Type v) {r : comm_semiring R} [s : Π (i : I), semiring (f i)] [Π (i : I), algebra R (f i)] (a : R) (i : I) :
(algebra_map R (Π (i : I), f i)) a i = (algebra_map R (f i)) a
@[simp]
theorem pi.eval_alg_hom_apply {I : Type u} (R : Type u_1) (f : I → Type v) {r : comm_semiring R} [Π (i : I), semiring (f i)] [Π (i : I), algebra R (f i)] (i : I) (f_1 : Π (i : I), f i) :
(pi.eval_alg_hom R f i) f_1 = f_1 i
def pi.eval_alg_hom {I : Type u} (R : Type u_1) (f : I → Type v) {r : comm_semiring R} [Π (i : I), semiring (f i)] [Π (i : I), algebra R (f i)] (i : I) :
(Π (i : I), f i) →ₐ[R] f i

function.eval as an alg_hom. The name matches pi.eval_ring_hom, pi.eval_monoid_hom, etc.

Equations
@[simp]
theorem pi.const_alg_hom_apply (R : Type u_1) (A : Type u_2) (B : Type u_3) [comm_semiring R] [semiring B] [algebra R B] (a : B) (ᾰ : A) :
(pi.const_alg_hom R A B) a = function.const A a
def pi.const_alg_hom (R : Type u_1) (A : Type u_2) (B : Type u_3) [comm_semiring R] [semiring B] [algebra R B] :
B →ₐ[R] A → B

function.const as an alg_hom. The name matches pi.const_ring_hom, pi.const_monoid_hom, etc.

Equations
@[simp]
theorem pi.const_ring_hom_eq_algebra_map (R : Type u_1) (A : Type u_2) [comm_semiring R] :

When R is commutative and permits an algebra_map, pi.const_ring_hom is equal to that map.

@[simp]
theorem pi.const_alg_hom_eq_algebra_of_id (R : Type u_1) (A : Type u_2) [comm_semiring R] :
pi.const_alg_hom R A R = algebra.of_id R (A → R)
theorem algebra_compatible_smul {R : Type u_1} [comm_semiring R] (A : Type u_2) [semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] [is_scalar_tower R A M] (r : R) (m : M) :
r m = (algebra_map R A) r m
@[simp]
theorem algebra_map_smul {R : Type u_1} [comm_semiring R] (A : Type u_2) [semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] [is_scalar_tower R A M] (r : R) (m : M) :
(algebra_map R A) r m = r m
@[protected, instance]
def is_scalar_tower.to_smul_comm_class {R : Type u_1} [comm_semiring R] {A : Type u_2} [semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] [is_scalar_tower R A M] :
@[protected, instance]
def is_scalar_tower.to_smul_comm_class' {R : Type u_1} [comm_semiring R] {A : Type u_2} [semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] [is_scalar_tower R A M] :
theorem smul_algebra_smul_comm {R : Type u_1} [comm_semiring R] {A : Type u_2} [semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] [is_scalar_tower R A M] (r : R) (a : A) (m : M) :
a r m = r a m
@[protected, instance]
def linear_map.coe_is_scalar_tower {R : Type u_1} [comm_semiring R] {A : Type u_2} [semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] [is_scalar_tower R A M] {N : Type u_4} [add_comm_monoid N] [module A N] [module R N] [is_scalar_tower R A N] :
has_coe (M →ₗ[A] N) (M →ₗ[R] N)
Equations
@[simp, norm_cast]
theorem linear_map.coe_restrict_scalars_eq_coe (R : Type u_1) [comm_semiring R] {A : Type u_2} [semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] [is_scalar_tower R A M] {N : Type u_4} [add_comm_monoid N] [module A N] [module R N] [is_scalar_tower R A N] (f : M →ₗ[A] N) :
@[simp, norm_cast]
theorem linear_map.coe_coe_is_scalar_tower (R : Type u_1) [comm_semiring R] {A : Type u_2} [semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] [is_scalar_tower R A M] {N : Type u_4} [add_comm_monoid N] [module A N] [module R N] [is_scalar_tower R A N] (f : M →ₗ[A] N) :
def linear_map.lto_fun (R : Type u) (M : Type v) (A : Type w) [comm_semiring R] [add_comm_monoid M] [module R M] [comm_ring A] [algebra R A] :
(M →ₗ[R] A) →ₗ[A] M → A

A-linearly coerce a R-linear map from M to A to a function, given an algebra A over a commutative semiring R and M a module over R.

Equations

TODO: The following lemmas no longer involve algebra at all, and could be moved closer to algebra/module/submodule.lean. Currently this is tricky because ker, range, , and are all defined in linear_algebra/basic.lean.

@[simp]
theorem linear_map.ker_restrict_scalars (R : Type u_1) {S : Type u_2} {M : Type u_3} {N : Type u_4} [semiring R] [semiring S] [has_scalar R S] [add_comm_monoid M] [module R M] [module S M] [is_scalar_tower R S M] [add_comm_monoid N] [module R N] [module S N] [is_scalar_tower R S N] (f : M →ₗ[S] N) :
theorem submodule.span_eq_restrict_scalars (R : Type u_1) (A : Type u_2) (M : Type u_3) [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M] (X : set M) (hsur : function.surjective (algebra_map R A)) :

If A is an R-algebra such that the induced morhpsim R →+* A is surjective, then the R-module generated by a set X equals the A-module generated by X.

@[protected]
def alg_hom.comp_left {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) (I : Type u_1) :
(I → A) →ₐ[R] I → B

R-algebra homomorphism between the function spaces I → A and I → B, induced by an R-algebra homomorphism f between A and B.

Equations
@[simp]
theorem alg_hom.comp_left_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) (I : Type u_1) (h : I → A) (ᾰ : I) :
(f.comp_left I) h = (f h)