# Algebras over commutative semirings #

In this file we define associative unital `Algebra`s over commutative (semi)rings.

- algebra homomorphisms `AlgHom` are defined in `Mathlib/Algebra/Algebra/Hom.lean`;

- algebra equivalences `AlgEquiv` are defined in `Mathlib/Algebra/Algebra/Equiv.lean`;

- `Subalgebra`s are defined in `Mathlib/Algebra/Algebra/Subalgebra.lean`;

- The category `AlgCat R` of `R`-algebras is defined in the file `Mathlib/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.
- `algebraMap R A : R →+* A`: the canonical map from `R` to `A`, as a `RingHom`. This is the preferred spelling of this map, it is also available as:
  - `Algebra.linearMap R A : R →ₗ[R] A`, a `LinearMap`.
  - `Algebra.ofId R A : R →ₐ[R] A`, an `AlgHom` (defined in a later file).

## 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 `algebraMap 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 `SMul R A` and requiring that this scalar action `r • x` must agree with left multiplication by the image of the structure morphism `algebraMap R A r * x`.

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

1.     variable [CommSemiring R] [Semiring A]
       variable [Algebra R A]

2.     variable [CommSemiring R] [Semiring A]
       variable [Module R A] [SMulCommClass R A A] [IsScalarTower 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*} [CommSemiring R] [Semiring A]
      [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] : Algebra R A :=
    Algebra.ofModule smul_mul_assoc mul_smul_comm

The advantage of the first approach is that `algebraMap R A` is available, and `AlgHom R A B` and `Subalgebra R A` can be used. For concrete `R` and `A`, `algebraMap R A` is often definitionally convenient.

The advantage of the second approach is that `CommSemiring R`, `Semiring A`, and `Module R A` can all be relaxed independently; for instance, this allows us to:

- Replace `Semiring A` with `NonUnitalNonAssocSemiring A` in order to describe non-unital and/or non-associative algebras.
- Replace `CommSemiring R` and `Module R A` with `CommGroup R'` and `DistribMulAction R' A`, which when `R' = Rˣ` lets us talk about the "algebra-like" action of `Rˣ` on an `R`-algebra `A`.

While `AlgHom R A B` cannot be used in the second approach, `NonUnitalAlgHom 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`.

source
class Algebra (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] extends SMul R 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.

- smul : R → A → A
- algebraMap : R →+* A

  Embedding `R →+* A` given by `Algebra` structure. Use `algebraMap` from the root namespace instead.

- commutes' (r : R) (x : A) : Algebra.algebraMap r * x = x * Algebra.algebraMap r
- smul_def' (r : R) (x : A) : r • x = Algebra.algebraMap r * x

Instances

source
def algebraMap (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] :
R →+* A

Embedding `R →+* A` given by `Algebra` structure.

Equations

- algebraMap R A = Algebra.algebraMap

Instances For

source
theorem Algebra.subsingleton (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] [Subsingleton R] :
Subsingleton A
source
@[reducible]
def Algebra.cast {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] :
R → A

Coercion from a commutative semiring to an algebra over this semiring.

Equations

- Algebra.cast = ⇑(algebraMap R A)

Instances For

source
def algebraMap.coeHTCT (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] :
CoeHTCT R A
Equations

- algebraMap.coeHTCT R A = { coe := Algebra.cast }

Instances For

source
theorem algebraMap.coe_zero {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] :
↑0 = 0
source
theorem algebraMap.coe_one {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] :
↑1 = 1
source
theorem algebraMap.coe_natCast {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (a : ℕ) :
↑↑a = ↑a
source
theorem algebraMap.coe_add {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (a b : R) :
↑(a + b) = ↑a + ↑b
source
theorem algebraMap.coe_mul {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (a b : R) :
↑(a * b) = ↑a * ↑b
source
theorem algebraMap.coe_pow {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (a : R) (n : ℕ) :
↑(a ^ n) = ↑a ^ n
source
theorem algebraMap.coe_neg {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (x : R) :
↑(-x) = -↑x
source
theorem algebraMap.coe_sub {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (a b : R) :
↑(a - b) = ↑a - ↑b
source
@[reducible, inline]
abbrev RingHom.toAlgebra' {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] (i : R →+* S) (h : ∀ (c : R) (x : S), i c * x = x * i c) :
Algebra R S

Creating an algebra from a morphism to the center of a semiring. See note [reducible non-instances].

Warning: In general this should not be used if `S` already has a `SMul R S` instance, since this creates another `SMul R S` instance from the supplied `RingHom` and this will likely create a diamond.

Equations

- i.toAlgebra' h = { smul := fun (c : R) (x : S) => i c * x, algebraMap := i, commutes' := h, smul_def' := ⋯ }

Instances For

source
theorem RingHom.smul_toAlgebra' {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] (i : R →+* S) (h : ∀ (c : R) (x : S), i c * x = x * i c) (r : R) (s : S) :
have x := i.toAlgebra' h; r • s = i r * s
source
theorem RingHom.algebraMap_toAlgebra' {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] (i : R →+* S) (h : ∀ (c : R) (x : S), i c * x = x * i c) :
algebraMap R S = i
source
@[reducible, inline]
abbrev RingHom.toAlgebra {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (i : R →+* S) :
Algebra R S

Creating an algebra from a morphism to a commutative semiring. See note [reducible non-instances].

Warning: In general this should not be used if `S` already has a `SMul R S` instance, since this creates another `SMul R S` instance from the supplied `RingHom` and this will likely create a diamond.

Equations

- i.toAlgebra = i.toAlgebra' ⋯

Instances For

source
theorem RingHom.smul_toAlgebra {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (i : R →+* S) (r : R) (s : S) :
have x := i.toAlgebra; r • s = i r * s
source
theorem RingHom.algebraMap_toAlgebra {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (i : R →+* S) :
algebraMap R S = i
source
@[reducible, inline]
abbrev Algebra.ofModule' {R : Type u} {A : Type w} [CommSemiring 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) :
Algebra R A

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

- One or more equations did not get rendered due to their size.

Instances For

source
@[reducible, inline]
abbrev Algebra.ofModule {R : Type u} {A : Type w} [CommSemiring 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)) :
Algebra R A

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

- Algebra.ofModule h₁ h₂ = Algebra.ofModule' ⋯ ⋯

Instances For

source
theorem Algebra.algebra_ext {R : Type u_2} [CommSemiring R] {A : Type u_3} [Semiring A] (P Q : Algebra R A) (h : ∀ (r : R), (algebraMap R A) r = (algebraMap R A) r) :
P = Q

To prove two algebra structures on a fixed `[CommSemiring R] [Semiring A]` agree, it suffices to check the `algebraMap`s agree.

source
theorem Algebra.algebra_ext_iff {R : Type u_2} [CommSemiring R] {A : Type u_3} [Semiring A] {P Q : Algebra R A} :
P = Q ↔ ∀ (r : R), (algebraMap R A) r = (algebraMap R A) r
source
theorem toAlgebra_algebraMap {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] :
(algebraMap R S).toAlgebra = inst✝

An auxiliary lemma used to prove theorems of the form `RingHom.X (algebraMap R S) ↔ Algebra.X R S`.

source
@[instance 200]
instance Algebra.toModule {R : Type u_2} {A : Type u_3} {x✝ : CommSemiring R} {x✝¹ : Semiring A} [Algebra R A] :
Module R A
Equations

- Algebra.toModule = { toSMul := inst✝.toSMul, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

source
theorem Algebra.smul_def {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) (x : A) :
r • x = (algebraMap R A) r * x
source
theorem Algebra.algebraMap_eq_smul_one {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) :
(algebraMap R A) r = r • 1
source
theorem Algebra.algebraMap_eq_smul_one' {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] :
⇑(algebraMap R A) = fun (r : R) => r • 1
source
theorem Algebra.commutes {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) (x : A) :
(algebraMap R A) r * x = x * (algebraMap R A) r

`mul_comm` for `Algebra`s when one element is from the base ring.

source
theorem Algebra.commute_algebraMap_left {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) (x : A) :
Commute ((algebraMap R A) r) x
source
theorem Algebra.commute_algebraMap_right {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) (x : A) :
Commute x ((algebraMap R A) r)
source
theorem Algebra.left_comm {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) (r : R) (y : A) :
x * ((algebraMap R A) r * y) = (algebraMap R A) r * (x * y)

`mul_left_comm` for `Algebra`s when one element is from the base ring.

source
theorem Algebra.right_comm {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) (r : R) (y : A) :
x * (algebraMap R A) r * y = x * y * (algebraMap R A) r

`mul_right_comm` for `Algebra`s when one element is from the base ring.

source
instance IsScalarTower.right {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] :
IsScalarTower R A A
source
@[simp]
theorem RingHom.smulOneHom_eq_algebraMap {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] :
smulOneHom = algebraMap R A
source
@[simp]
theorem Algebra.mul_smul_comm {R : Type u} {A : Type w} [CommSemiring 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).

source
@[simp]
theorem Algebra.smul_mul_assoc {R : Type u} {A : Type w} [CommSemiring 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).

source
@[simp]
theorem smul_algebraMap {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_2} [Monoid α] [MulDistribMulAction α A] [SMulCommClass α R A] (a : α) (r : R) :
a • (algebraMap R A) r = (algebraMap R A) r
source
@[reducible, inline]
abbrev Algebra.compHom {R : Type u} {S : Type v} (A : Type w) [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R A] (f : S →+* R) :
Algebra S A

Compose an `Algebra` with a `RingHom`, with action `f s • m`.

This is the algebra version of `Module.compHom`.

Equations

- Algebra.compHom A f = { smul := fun (s : S) (a : A) => f s • a, algebraMap := (algebraMap R A).comp f, commutes' := ⋯, smul_def' := ⋯ }

Instances For

source
theorem Algebra.compHom_smul_def {R : Type u} {S : Type v} (A : Type w) [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R A] (f : S →+* R) (s : S) (x : A) :
s • x = f s • x
source
theorem Algebra.compHom_algebraMap_eq {R : Type u} {S : Type v} (A : Type w) [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R A] (f : S →+* R) :
algebraMap S A = (algebraMap R A).comp f
source
theorem Algebra.compHom_algebraMap_apply {R : Type u} {S : Type v} (A : Type w) [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R A] (f : S →+* R) (s : S) :
(algebraMap S A) s = (algebraMap R A) (f s)
source
def Algebra.linearMap (R : Type u) (A : Type w) [CommSemiring R] [Semiring A] [Algebra R A] :
R →ₗ[R] A

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

Equations

- Algebra.linearMap R A = { toFun := (↑↑(algebraMap R A)).toFun, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source
def RingTheory.LinearMap.termη :
Lean.ParserDescr

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

Equations

- RingTheory.LinearMap.termη = Lean.ParserDescr.node `RingTheory.LinearMap.termη 1024 (Lean.ParserDescr.symbol "η")

Instances For

source
def RingTheory.LinearMap.«termη[_]» :
Lean.ParserDescr

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Algebra.linearMap_apply (R : Type u) (A : Type w) [CommSemiring R] [Semiring A] [Algebra R A] (r : R) :
(Algebra.linearMap R A) r = (algebraMap R A) r
source
theorem Algebra.coe_linearMap (R : Type u) (A : Type w) [CommSemiring R] [Semiring A] [Algebra R A] :
⇑(Algebra.linearMap R A) = ⇑(algebraMap R A)
source
@[instance 1100]
instance Algebra.id (R : Type u) [CommSemiring R] :
Algebra R R

The identity map inducing an `Algebra` structure.

Equations

- Algebra.id R = { toSMul := instSMulOfMul, algebraMap := Algebra.algebraMap, commutes' := ⋯, smul_def' := ⋯ }

source
@[simp]
theorem Algebra.linearMap_self (R : Type u) [CommSemiring R] :
Algebra.linearMap R R = LinearMap.id
source
@[simp]
theorem Algebra.algebraMap_self {R : Type u} [CommSemiring R] :
algebraMap R R = RingHom.id R
source
theorem Algebra.algebraMap_self_apply {R : Type u} [CommSemiring R] (x : R) :
(algebraMap R R) x = x
source
@[deprecated Algebra.algebraMap_self (since := "2025-07-17")]
theorem Algebra.id.map_eq_id {R : Type u} [CommSemiring R] :
algebraMap R R = RingHom.id R
source
@[deprecated Algebra.algebraMap_self_apply (since := "2025-07-17")]
theorem Algebra.id.map_eq_self {R : Type u} [CommSemiring R] (x : R) :
(algebraMap R R) x = x
source
@[simp]
theorem Algebra.id.smul_eq_mul {R : Type u} [CommSemiring R] (x y : R) :
x • y = x * y
source
theorem algebraMap.coe_smul {A : Type u_1} {B : Type u_2} (a : A) (b : B) (C : Type u_3) [SMul A B] [CommSemiring B] [Semiring C] [Algebra B C] [SMul A C] [IsScalarTower A B C] :
↑(a • b) = a • ↑b
source
theorem algebraMap.coe_smul' {A : Type u_1} {B : Type u_2} (a : A) (b : B) (C : Type u_3) [SMul A B] [CommSemiring B] [Semiring C] [Algebra B C] [Monoid A] [MulDistribMulAction A C] [SMulDistribClass A B C] :
↑(a • b) = a • ↑b