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: #

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
@[instance]
def algebra_map.has_lift_t (R : Type u_1) (A : Type u_2) [comm_semiring R] [semiring A] [algebra R A] :
Equations
@[simp, norm_cast]
theorem algebra_map.coe_zero {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] :
0 = 0
@[simp, norm_cast]
theorem algebra_map.coe_one {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] :
1 = 1
@[norm_cast]
theorem algebra_map.coe_add {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (a b : R) :
(a + b) = a + b
@[norm_cast]
theorem algebra_map.coe_mul {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (a b : R) :
(a * b) = a * b
@[norm_cast]
theorem algebra_map.coe_pow {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (a : R) (n : ) :
(a ^ n) = a ^ n
@[norm_cast]
theorem algebra_map.coe_neg {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [algebra R A] (x : R) :
@[norm_cast]
theorem algebra_map.coe_prod {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_semiring A] [algebra R A] {ι : Type u_3} {s : finset ι} (a : ι R) :
(s.prod (λ (i : ι), a i)) = s.prod (λ (i : ι), (a i))
@[norm_cast]
theorem algebra_map.coe_sum {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_semiring A] [algebra R A] {ι : Type u_3} {s : finset ι} (a : ι R) :
(s.sum (λ (i : ι), a i)) = s.sum (λ (i : ι), (a i))
@[simp, norm_cast]
theorem algebra_map.coe_inj {R : Type u_1} {A : Type u_2} [field R] [comm_semiring A] [nontrivial A] [algebra R A] {a b : R} :
a = b a = b
@[simp, norm_cast]
theorem algebra_map.lift_map_eq_zero_iff {R : Type u_1} {A : Type u_2} [field R] [comm_semiring A] [nontrivial A] [algebra R A] (a : R) :
a = 0 a = 0
def ring_hom.to_algebra' {R : Type u_1} {S : Type u_2} [comm_semiring R] [semiring S] (i : R →+* S) (h : (c : R) (x : S), i c * x = x * i c) :

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

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

Creating an algebra from a morphism to a commutative semiring.

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

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

See note [reducible non-instances].

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

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

See note [reducible non-instances].

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Equations
@[simp]
theorem algebra.linear_map_apply (R : Type u) (A : Type w) [comm_semiring R] [semiring A] [algebra R A] (r : R) :
@[protected, instance]
def algebra.id (R : Type u) [comm_semiring R] :
Equations
@[simp]
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]
Equations
@[simp]
theorem algebra.algebra_map_punit {R : Type u} [comm_semiring R] (r : R) :
(algebra_map R punit) r = punit.star
@[protected, instance]
def ulift.algebra {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] :
Equations
theorem ulift.algebra_map_eq {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] (r : R) :
(algebra_map R (ulift A)) r = {down := (algebra_map R A) r}
@[simp]
theorem ulift.down_algebra_map {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] (r : R) :
@[protected, instance]
def 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_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_semiring R] [ring A] [algebra R A] (x : A) (r : R) :
x * (x - (algebra_map R A) r) = (x - (algebra_map R A) r) * x
theorem algebra.mul_sub_algebra_map_pow_commutes {R : Type u} {A : Type w} [comm_semiring R] [ring A] [algebra R A] (x : A) (r : R) (n : ) :
x * (x - (algebra_map R A) r) ^ n = (x - (algebra_map R A) r) ^ n * x
@[reducible]
def algebra.semiring_to_ring (R : Type u) {A : Type w} [comm_ring R] [semiring A] [algebra R A] :

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

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

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

theorem linear_map.map_mul_algebra_map {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₗ[R] B) (a : A) (r : R) :
f (a * (algebra_map R A) r) = f a * (algebra_map R B) r
@[simp]
theorem rat.smul_one_eq_coe {A : Type u_1} [division_ring A] [algebra A] (m : ) :
m 1 = m
@[protected, instance]
@[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 : ) :
@[protected, instance]
def algebra_rat {α : Type u_1} [division_ring α] [char_zero α] :
Equations
@[protected, instance]
@[simp]

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

@[protected, instance]

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.

theorem ne_zero.of_no_zero_smul_divisors (R : Type u_1) (A : Type u_2) (n : ) [comm_ring R] [ne_zero n] [ring A] [nontrivial A] [algebra R A] [no_zero_smul_divisors R A] :
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
theorem int_cast_smul {k : Type u_1} {V : Type u_2} [comm_ring k] [add_comm_group V] [module k V] (r : ) (x : V) :
r x = r x
@[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
@[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]

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.