Algebras over commutative semirings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

• algebra R A: the algebra typeclass.
• algebra_map R A : R →+* A: the canonical map from R to A, as a ring_hom. This is the preferred spelling of this map, it is also available as:
  • algebra.linear_map R A : R →ₗ[R] A, a linear_map.
  • algebra.of_id R A : R →ₐ[R] A, an alg_hom (defined in a later file).
• Instances of algebra in this file:
  • algebra.id
  • algebra_nat
  • algebra_int
  • algebra_rat
  • mul_opposite.algebra
  • module.End.algebra

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:

• By endowing A with a morphism of rings R →+* A denoted algebra_map R A which lands in the center of A.
• By requiring A be an R-module such that the action associates and commutes with multiplication as r • (a₁ * a₂) = (r • a₁) * a₂ = a₁ * (r • 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:

example {R A : Type*} [comm_semiring R] [semiring A]
  [module R A] [smul_comm_class R A A] [is_scalar_tower R A A] : algebra R A :=
algebra.of_module smul_mul_assoc mul_smul_comm

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:

• Replace semiring A with non_unital_non_assoc_semiring A in order to describe non-unital and/or non-associative algebras.
• Replace comm_semiring R and module R A with comm_group R' and distrib_mul_action R' A, which when R' = Rˣ lets us talk about the "algebra-like" action of Rˣ on an R-algebra A.

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.

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.