Algebras over commutative semirings

In this file we define associative unital Algebras over commutative (semi)rings.

• algebra homomorphisms AlgHom are defined in Mathlib.Algebra.Algebra.Hom;

• algebra equivalences AlgEquiv are defined in Mathlib.Algebra.Algebra.Equiv;

• Subalgebras are defined in Mathlib.Algebra.Algebra.Subalgebra;

• The category AlgebraCat R of R-algebras is defined in the file Mathlib.Algebra.Category.Algebra.Basic.

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.

class Algebra (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] extends SMul , RingHom : 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
• toFun : R → A
• map_one' : (↑↑Algebra.toRingHom).toFun 1 = 1
• map_mul' : ∀ (x y : R), (↑↑Algebra.toRingHom).toFun (x * y) = (↑↑Algebra.toRingHom).toFun x * (↑↑Algebra.toRingHom).toFun y
• map_zero' : (↑↑Algebra.toRingHom).toFun 0 = 0
• map_add' : ∀ (x y : R), (↑↑Algebra.toRingHom).toFun (x + y) = (↑↑Algebra.toRingHom).toFun x + (↑↑Algebra.toRingHom).toFun y
• commutes' : ∀ (r : R) (x : A), Algebra.toRingHom r * x = x * Algebra.toRingHom r
• smul_def' : ∀ (r : R) (x : A), r • x = Algebra.toRingHom r * x

theorem Algebra.commutes' {R : Type u} {A : Type v} : ∀ {inst : CommSemiring R} {inst_1 : Semiring A} [self : Algebra R A] (r : R) (x : A), Algebra.toRingHom r * x = x * Algebra.toRingHom r

theorem Algebra.smul_def' {R : Type u} {A : Type v} : ∀ {inst : CommSemiring R} {inst_1 : Semiring A} [self : Algebra R A] (r : R) (x : A), r • x = Algebra.toRingHom r * x

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.toRingHom

@[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)

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 }

theorem algebraMap.coe_zero {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] : ↑0 = 0

theorem algebraMap.coe_one {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] : ↑1 = 1

theorem algebraMap.coe_natCast {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (a : ℕ) : ↑↑a = ↑a

theorem algebraMap.coe_add {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (a : R) (b : R) : ↑(a + b) = ↑a + ↑b

theorem algebraMap.coe_mul {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (a : R) (b : R) : ↑(a * b) = ↑a * ↑b

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

theorem algebraMap.coe_neg {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (x : R) : ↑(-x) = -↑x

theorem algebraMap.coe_sub {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (a : R) (b : R) : ↑(a - b) = ↑a - ↑b

def 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.

Equations

• i.toAlgebra' h = Algebra.mk i h ⋯

def 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.

Equations

• i.toAlgebra = i.toAlgebra' ⋯

theorem RingHom.algebraMap_toAlgebra {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (i : R →+* S) : algebraMap R S = i

@[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

• Algebra.ofModule' h₁ h₂ = Algebra.mk { toFun := fun (r : R) => r • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

@[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' ⋯ ⋯

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

theorem Algebra.algebra_ext {R : Type u_2} [CommSemiring R] {A : Type u_3} [Semiring A] (P : Algebra R A) (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 algebraMaps agree.

@[instance 200]

instance Algebra.toModule {R : Type u_2} {A : Type u_3} : {x : CommSemiring R} → {x_1 : Semiring A} → [inst : Algebra R A] → Module R A

Equations

• Algebra.toModule = Module.mk ⋯ ⋯

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

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

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

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 Algebras when one element is from the base ring.

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

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)

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 Algebras when one element is from the base ring.

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 Algebras when one element is from the base ring.

instance IsScalarTower.right {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] : IsScalarTower R A A

Equations

• ⋯ = ⋯

@[simp]

theorem RingHom.smulOneHom_eq_algebraMap {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] : RingHom.smulOneHom = algebraMap R A

@[simp]

theorem Algebra.mul_smul_comm {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] (s : R) (x : A) (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).

@[simp]

theorem Algebra.smul_mul_assoc {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) (x : A) (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_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

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' := ⋯ }

@[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

theorem Algebra.coe_linearMap (R : Type u) (A : Type w) [CommSemiring R] [Semiring A] [Algebra R A] : ⇑(Algebra.linearMap R A) = ⇑(algebraMap R A)

@[instance 1100]

instance Algebra.id (R : Type u) [CommSemiring R] : Algebra R R

The identity map inducing an Algebra structure.

Equations

• Algebra.id R = Algebra.mk { toFun := fun (x : R) => x, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

@[simp]

theorem Algebra.id.map_eq_id {R : Type u} [CommSemiring R] : algebraMap R R = RingHom.id R

theorem Algebra.id.map_eq_self {R : Type u} [CommSemiring R] (x : R) : (algebraMap R R) x = x

@[simp]

theorem Algebra.id.smul_eq_mul {R : Type u} [CommSemiring R] (x : R) (y : R) : x • y = x * y

theorem algebraMap.coe_smul (A : Type u_1) (B : Type u_2) (C : Type u_3) [SMul A B] [CommSemiring B] [Semiring C] [Algebra B C] [SMul A C] [IsScalarTower A B C] (a : A) (b : B) : ↑(a • b) = a • ↑b