Mathlib.Algebra.Algebra.Defs

Module docstring

{"# 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. lean variable [CommSemiring R] [Semiring A] variable [Algebra R A] 2. lean 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: lean 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.

Algebra structure

(R : Type u) (A : Type v) [CommSemiring R] [Semiring A] extends SMul R A

Full source

/-- 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.
-/
class Algebra (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] extends SMul R A where
  /-- Embedding `R →+* A` given by `Algebra` structure.
  Use `algebraMap` from the root namespace instead. -/
  protected algebraMap : R →+* A
  commutes' : ∀ r x, algebraMap r * x = x * algebraMap r
  smul_def' : ∀ r x, r • x = algebraMap r * x

Associative Unital Algebra over a Commutative Semiring

Informal description

An associative unital $R$-algebra is a semiring $A$ equipped with a scalar multiplication operation $R \times A \to A$ and a ring homomorphism $\text{algebraMap} \colon R \to A$ whose image lies in the center of $A$. The scalar multiplication must agree with left multiplication by the image of $\text{algebraMap}$, i.e., $r \cdot x = \text{algebraMap}(r) * x$ for all $r \in R$ and $x \in A$. This structure generalizes both the notion of an algebra defined via a ring homomorphism and the notion of an algebra defined via a compatible module structure.

algebraMap definition

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

Full source

/-- Embedding `R →+* A` given by `Algebra` structure. -/
def algebraMap (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] : R →+* A :=
  Algebra.algebraMap

Canonical algebra homomorphism

Informal description

The canonical ring homomorphism $\text{algebraMap} \colon R \to A$ associated with an $R$-algebra structure on $A$, where $R$ is a commutative semiring and $A$ is a semiring. This map embeds $R$ into the center of $A$ and satisfies $r \cdot x = \text{algebraMap}(r) * x$ for all $r \in R$ and $x \in A$.

Algebra.cast definition

{R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] : R → A

Full source

/-- Coercion from a commutative semiring to an algebra over this semiring. -/
@[coe, reducible]
def Algebra.cast {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] : R → A :=
  algebraMap R A

Canonical embedding of a commutative semiring into an algebra

Informal description

The canonical embedding of a commutative semiring $R$ into an $R$-algebra $A$, given by the ring homomorphism $\text{algebraMap} \colon R \to A$. This map satisfies $r \cdot x = \text{algebraMap}(r) * x$ for all $r \in R$ and $x \in A$, and its image lies in the center of $A$.

algebraMap.coeHTCT instance

(R A : Type*) [CommSemiring R] [Semiring A] [Algebra R A] : CoeHTCT R A

Full source

scoped instance coeHTCT (R A : Type*) [CommSemiring R] [Semiring A] [Algebra R A] :
    CoeHTCT R A :=
  ⟨Algebra.cast⟩

Canonical Embedding of Commutative Semiring into Algebra

Informal description

For any commutative semiring $R$ and semiring $A$ with an $R$-algebra structure, there is a canonical embedding of $R$ into $A$ via the ring homomorphism $\text{algebraMap} \colon R \to A$.

algebraMap.coe_zero theorem

: (↑(0 : R) : A) = 0

Full source

@[norm_cast]
theorem coe_zero : (↑(0 : R) : A) = 0 :=
  map_zero (algebraMap R A)

Image of zero under algebra homomorphism

Informal description

For any commutative semiring $R$ and any $R$-algebra $A$, the image of $0 \in R$ under the canonical algebra homomorphism $\text{algebraMap} \colon R \to A$ is equal to $0 \in A$, i.e., $\text{algebraMap}(0) = 0$.

algebraMap.coe_one theorem

: (↑(1 : R) : A) = 1

Full source

@[norm_cast]
theorem coe_one : (↑(1 : R) : A) = 1 :=
  map_one (algebraMap R A)

Preservation of Multiplicative Identity under Algebra Map

Informal description

For any commutative semiring $R$ and semiring $A$ with an $R$-algebra structure, the canonical embedding $\text{algebraMap} \colon R \to A$ maps the multiplicative identity $1 \in R$ to the multiplicative identity $1 \in A$, i.e., $\text{algebraMap}(1) = 1$.

algebraMap.coe_natCast theorem

(a : ℕ) : (↑(a : R) : A) = a

Full source

@[norm_cast]
theorem coe_natCast (a : ℕ) : (↑(a : R) : A) = a :=
  map_natCast (algebraMap R A) a

Natural Number Preservation under Algebra Homomorphism

Informal description

For any natural number $a$, the image of $a$ under the canonical algebra homomorphism from a commutative semiring $R$ to an $R$-algebra $A$ is equal to $a$ itself, i.e., $\text{algebraMap}(a) = a$.

algebraMap.coe_add theorem

(a b : R) : (↑(a + b : R) : A) = ↑a + ↑b

Full source

@[norm_cast]
theorem coe_add (a b : R) : (↑(a + b : R) : A) = ↑a + ↑b :=
  map_add (algebraMap R A) a b

Additivity of the canonical algebra homomorphism

Informal description

For any elements $a, b$ in a commutative semiring $R$ and any $R$-algebra $A$, the canonical algebra homomorphism $\text{algebraMap} \colon R \to A$ preserves addition, i.e., $\text{algebraMap}(a + b) = \text{algebraMap}(a) + \text{algebraMap}(b)$.

algebraMap.coe_mul theorem

(a b : R) : (↑(a * b : R) : A) = ↑a * ↑b

Full source

@[norm_cast]
theorem coe_mul (a b : R) : (↑(a * b : R) : A) = ↑a * ↑b :=
  map_mul (algebraMap R A) a b

Multiplicativity of the Algebra Homomorphism: $\text{algebraMap}(a * b) = \text{algebraMap}(a) * \text{algebraMap}(b)$

Informal description

For any elements $a, b$ in a commutative semiring $R$, the image of their product under the canonical algebra homomorphism $\text{algebraMap} \colon R \to A$ equals the product of their images, i.e., $\text{algebraMap}(a * b) = \text{algebraMap}(a) * \text{algebraMap}(b)$.

algebraMap.coe_pow theorem

(a : R) (n : ℕ) : (↑(a ^ n : R) : A) = (a : A) ^ n

Full source

@[norm_cast]
theorem coe_pow (a : R) (n : ℕ) : (↑(a ^ n : R) : A) = (a : A) ^ n :=
  map_pow (algebraMap R A) _ _

Power Preservation under Algebra Homomorphism: $\text{algebraMap}(a^n) = (\text{algebraMap}(a))^n$

Informal description

For any commutative semiring $R$ and $R$-algebra $A$, the canonical algebra homomorphism $\text{algebraMap} \colon R \to A$ preserves powers. Specifically, for any element $a \in R$ and natural number $n$, the image of $a^n$ under $\text{algebraMap}$ equals the $n$-th power of $\text{algebraMap}(a)$ in $A$, i.e., $\text{algebraMap}(a^n) = (\text{algebraMap}(a))^n$.

algebraMap.coe_neg theorem

(x : R) : (↑(-x : R) : A) = -↑x

Full source

@[norm_cast]
theorem coe_neg (x : R) : (↑(-x : R) : A) = -↑x :=
  map_neg (algebraMap R A) x

Negation Preservation in Algebra Homomorphism: $\text{algebraMap}(-x) = -\text{algebraMap}(x)$

Informal description

For any element $x$ in a commutative ring $R$ and an $R$-algebra $A$, the image of $-x$ under the canonical algebra homomorphism $\text{algebraMap} \colon R \to A$ equals the negation of the image of $x$, i.e., $\text{algebraMap}(-x) = -\text{algebraMap}(x)$.

algebraMap.coe_sub theorem

(a b : R) : (↑(a - b : R) : A) = ↑a - ↑b

Full source

@[norm_cast]
theorem coe_sub (a b : R) :
    (↑(a - b : R) : A) = ↑a - ↑b :=
  map_sub (algebraMap R A) a b

Algebra Homomorphism Preserves Subtraction: $\text{algebraMap}(a - b) = \text{algebraMap}(a) - \text{algebraMap}(b)$

Informal description

For any elements $a$ and $b$ in a commutative semiring $R$, the image of their difference $a - b$ under the canonical algebra homomorphism $\text{algebraMap} \colon R \to A$ equals the difference of their images in the $R$-algebra $A$, i.e., $\text{algebraMap}(a - b) = \text{algebraMap}(a) - \text{algebraMap}(b)$.

RingHom.toAlgebra' abbrev

{R S} [CommSemiring R] [Semiring S] (i : R →+* S) (h : ∀ c x, i c * x = x * i c) : Algebra R S

Full source

/-- Creating an algebra from a morphism to the center of a semiring.
See note [reducible non-instances]. -/
abbrev RingHom.toAlgebra' {R S} [CommSemiring R] [Semiring S] (i : R →+* S)
    (h : ∀ c x, i c * x = x * i c) : Algebra R S where
  smul c x := i c * x
  commutes' := h
  smul_def' _ _ := rfl
  algebraMap := i

Induced Algebra Structure via Central Ring Homomorphism

Informal description

Given a commutative semiring $R$ and a semiring $S$, any ring homomorphism $i \colon R \to S$ whose image lies in the center of $S$ (i.e., $i(c) * x = x * i(c)$ for all $c \in R$ and $x \in S$) induces an $R$-algebra structure on $S$.

RingHom.smul_toAlgebra' theorem

 {R S} [CommSemiring R] [Semiring S] (i : R →+* S) (h : ∀ c x, i c * x = x * i c) (r : R) (s : S) :
  let _ := RingHom.toAlgebra' i h
  r • s = i r * s

Full source

theorem RingHom.smul_toAlgebra' {R S} [CommSemiring R] [Semiring S] (i : R →+* S)
    (h : ∀ c x, i c * x = x * i c) (r : R) (s : S) :
    let _ := RingHom.toAlgebra' i h
    r • s = i r * s := rfl

Scalar multiplication in induced algebra equals ring homomorphism action: $r \cdot s = i(r) * s$

Informal description

Let $R$ be a commutative semiring and $S$ a semiring. Given a ring homomorphism $i \colon R \to S$ such that $i(c) * x = x * i(c)$ for all $c \in R$ and $x \in S$, the scalar multiplication $r \cdot s$ in the induced $R$-algebra structure on $S$ satisfies $r \cdot s = i(r) * s$ for all $r \in R$ and $s \in S$.

RingHom.algebraMap_toAlgebra' theorem

 {R S} [CommSemiring R] [Semiring S] (i : R →+* S) (h : ∀ c x, i c * x = x * i c) :
  @algebraMap R S _ _ (i.toAlgebra' h) = i

Full source

theorem RingHom.algebraMap_toAlgebra' {R S} [CommSemiring R] [Semiring S] (i : R →+* S)
    (h : ∀ c x, i c * x = x * i c) :
    @algebraMap R S _ _ (i.toAlgebra' h) = i :=
  rfl

Canonical Algebra Map Equals Inducing Homomorphism for Central Extensions

Informal description

Let $R$ be a commutative semiring and $S$ a semiring. Given a ring homomorphism $i \colon R \to S$ whose image lies in the center of $S$ (i.e., $i(c) * x = x * i(c)$ for all $c \in R$ and $x \in S$), the canonical algebra homomorphism $\text{algebraMap} \colon R \to S$ associated with the induced $R$-algebra structure on $S$ equals $i$.

RingHom.toAlgebra abbrev

{R S} [CommSemiring R] [CommSemiring S] (i : R →+* S) : Algebra R S

Full source

/-- Creating an algebra from a morphism to a commutative semiring.
See note [reducible non-instances]. -/
abbrev RingHom.toAlgebra {R S} [CommSemiring R] [CommSemiring S] (i : R →+* S) : Algebra R S :=
  i.toAlgebra' fun _ => mul_comm _

Induced Algebra Structure via Ring Homomorphism between Commutative Semirings

Informal description

Given a commutative semiring $R$ and a commutative semiring $S$, any ring homomorphism $i \colon R \to S$ induces an $R$-algebra structure on $S$.

RingHom.smul_toAlgebra theorem

 {R S} [CommSemiring R] [CommSemiring S] (i : R →+* S) (r : R) (s : S) :
  let _ := RingHom.toAlgebra i
  r • s = i r * s

Full source

theorem RingHom.smul_toAlgebra {R S} [CommSemiring R] [CommSemiring S] (i : R →+* S)
    (r : R) (s : S) :
    let _ := RingHom.toAlgebra i
    r • s = i r * s := rfl

Scalar multiplication equals image multiplication in induced algebra structure

Informal description

Let $R$ and $S$ be commutative semirings, and let $i \colon R \to S$ be a ring homomorphism. Under the $R$-algebra structure on $S$ induced by $i$, the scalar multiplication $r \bullet s$ of $r \in R$ and $s \in S$ is equal to the product $i(r) \cdot s$ in $S$.

RingHom.algebraMap_toAlgebra theorem

{R S} [CommSemiring R] [CommSemiring S] (i : R →+* S) : @algebraMap R S _ _ i.toAlgebra = i

Full source

theorem RingHom.algebraMap_toAlgebra {R S} [CommSemiring R] [CommSemiring S] (i : R →+* S) :
    @algebraMap R S _ _ i.toAlgebra = i :=
  rfl

Canonical Algebra Homomorphism Induced by Ring Homomorphism Equals Original Homomorphism

Informal description

Given a commutative semiring $R$ and a commutative semiring $S$, for any ring homomorphism $i \colon R \to S$, the canonical algebra homomorphism $\text{algebraMap} \colon R \to S$ induced by the $R$-algebra structure on $S$ via $i$ is equal to $i$ itself.

Algebra.ofModule' abbrev

 [CommSemiring R] [Semiring A] [Module R A] (h₁ : ∀ (r : R) (x : A), r • (1 : A) * x = r • x)
  (h₂ : ∀ (r : R) (x : A), x * r • (1 : A) = r • x) : Algebra R A

Full source

/-- 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]. -/
abbrev ofModule' [CommSemiring R] [Semiring A] [Module R A]
    (h₁ : ∀ (r : R) (x : A), r • (1 : A) * x = r • x)
    (h₂ : ∀ (r : R) (x : A), x * r • (1 : A) = r • x) : Algebra R A where
  algebraMap :=
  { toFun r := r • (1 : A)
    map_one' := one_smul _ _
    map_mul' r₁ r₂ := by simp only [h₁, mul_smul]
    map_zero' := zero_smul _ _
    map_add' r₁ r₂ := add_smul r₁ r₂ 1 }
  commutes' r x := by simp [h₁, h₂]
  smul_def' r x := by simp [h₁]

Construction of Algebra Structure via Module Compatibility with Unit Multiplication

Informal description

Let $R$ be a commutative semiring and $A$ be a semiring equipped with a module structure over $R$. If for all $r \in R$ and $x \in A$, the following conditions hold: 1. $(r \bullet 1_A) * x = r \bullet x$ 2. $x * (r \bullet 1_A) = r \bullet x$ then $A$ can be endowed with the structure of an $R$-algebra.

Algebra.ofModule abbrev

 [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

Full source

/-- 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]. -/
abbrev ofModule [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 :=
  ofModule' (fun r x => by rw [h₁, one_mul]) fun r x => by rw [h₂, mul_one]

Module Compatibility Conditions Induce Algebra Structure

Informal description

Let $R$ be a commutative semiring and $A$ be a semiring equipped with a module structure over $R$. If for all $r \in R$ and $x, y \in A$, the following compatibility conditions hold: 1. $(r \bullet x) * y = r \bullet (x * y)$ 2. $x * (r \bullet y) = r \bullet (x * y)$ then $A$ can be endowed with the structure of an $R$-algebra.

Algebra.algebra_ext theorem

 {R : Type*} [CommSemiring R] {A : Type*} [Semiring A] (P Q : Algebra R A)
  (h :
    ∀ r : R,
      (haveI := P;
        algebraMap R A r) =
        haveI := Q;
        algebraMap R A r) :
  P = Q

Full source

/-- To prove two algebra structures on a fixed `[CommSemiring R] [Semiring A]` agree,
it suffices to check the `algebraMap`s agree.
-/
@[ext]
theorem algebra_ext {R : Type*} [CommSemiring R] {A : Type*} [Semiring A] (P Q : Algebra R A)
    (h : ∀ r : R, (haveI := P; algebraMap R A r) = haveI := Q; algebraMap R A r) :
    P = Q := by
  replace h : P.algebraMap = Q.algebraMap := DFunLike.ext _ _ h
  have h' : (haveI := P; (· • ·) : R → A → A) = (haveI := Q; (· • ·) : R → A → A) := by
    funext r a
    rw [P.smul_def', Q.smul_def', h]
  rcases P with @⟨⟨P⟩⟩
  rcases Q with @⟨⟨Q⟩⟩
  congr

Equality of Algebra Structures via Equal Algebra Maps

Informal description

Let $R$ be a commutative semiring and $A$ a semiring. For any two $R$-algebra structures $P$ and $Q$ on $A$, if their associated algebra homomorphisms $\text{algebraMap}_P, \text{algebraMap}_Q \colon R \to A$ satisfy $\text{algebraMap}_P(r) = \text{algebraMap}_Q(r)$ for all $r \in R$, then $P = Q$.

Algebra.toModule instance

{R A} {_ : CommSemiring R} {_ : Semiring A} [Algebra R A] : Module R A

Full source

instance (priority := 200) toModule {R A} {_ : CommSemiring R} {_ : Semiring A} [Algebra R A] :
    Module R A where
  one_smul _ := by simp [smul_def']
  mul_smul := by simp [smul_def', mul_assoc]
  smul_add := by simp [smul_def', mul_add]
  smul_zero := by simp [smul_def']
  add_smul := by simp [smul_def', add_mul]
  zero_smul := by simp [smul_def']

$R$-Algebra Induces $R$-Module Structure

Informal description

For any commutative semiring $R$ and semiring $A$ equipped with an $R$-algebra structure, $A$ is also an $R$-module where the scalar multiplication is given by $r \cdot x = \text{algebraMap}(r) * x$.

Algebra.smul_def theorem

(r : R) (x : A) : r • x = algebraMap R A r * x

Full source

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

Scalar Multiplication Equals Algebra Map Multiplication in Algebras

Informal description

For any element $r$ in a commutative semiring $R$ and any element $x$ in an $R$-algebra $A$, the scalar multiplication $r \cdot x$ is equal to the product of the algebra homomorphism $\text{algebraMap}(r)$ and $x$, i.e., $r \cdot x = \text{algebraMap}(r) * x$.

Algebra.algebraMap_eq_smul_one theorem

(r : R) : algebraMap R A r = r • (1 : A)

Full source

theorem algebraMap_eq_smul_one (r : R) : algebraMap R A r = r • (1 : A) :=
  calc
    algebraMap R A r = algebraMap R A r * 1 := (mul_one _).symm
    _ = r • (1 : A) := (Algebra.smul_def r 1).symm

Algebra Homomorphism as Scalar Multiplication of Identity

Informal description

For any element $r$ in a commutative semiring $R$ and any $R$-algebra $A$, the image of $r$ under the algebra homomorphism $\text{algebraMap} \colon R \to A$ is equal to the scalar multiplication of $r$ with the multiplicative identity $1 \in A$, i.e., \[ \text{algebraMap}(r) = r \cdot 1. \]

Algebra.algebraMap_eq_smul_one' theorem

: ⇑(algebraMap R A) = fun r => r • (1 : A)

Full source

theorem algebraMap_eq_smul_one' : ⇑(algebraMap R A) = fun r => r • (1 : A) :=
  funext algebraMap_eq_smul_one

Algebra Homomorphism as Scalar Multiplication of Identity (Function Form)

Informal description

The algebra homomorphism $\text{algebraMap} \colon R \to A$ is equal to the function that maps each element $r \in R$ to the scalar multiplication $r \cdot 1_A$, where $1_A$ is the multiplicative identity in $A$.

Algebra.commutes theorem

(r : R) (x : A) : algebraMap R A r * x = x * algebraMap R A r

Full source

/-- `mul_comm` for `Algebra`s when one element is from the base ring. -/
theorem commutes (r : R) (x : A) : algebraMap R A r * x = x * algebraMap R A r :=
  Algebra.commutes' r x

Commutativity of algebra map elements in an $R$-algebra

Informal description

Let $R$ be a commutative semiring and $A$ be an $R$-algebra. For any element $r \in R$ and any $x \in A$, the image of $r$ under the algebra map $\text{algebraMap} \colon R \to A$ commutes with $x$, i.e., \[ \text{algebraMap}(r) * x = x * \text{algebraMap}(r). \]

Algebra.commute_algebraMap_left theorem

(r : R) (x : A) : Commute (algebraMap R A r) x

Full source

lemma commute_algebraMap_left (r : R) (x : A) : Commute (algebraMap R A r) x :=
  Algebra.commutes r x

Commutativity of algebra map elements with algebra elements

Informal description

For any element $r$ in a commutative semiring $R$ and any element $x$ in an $R$-algebra $A$, the image of $r$ under the algebra homomorphism $\text{algebraMap} \colon R \to A$ commutes with $x$, i.e., $\text{algebraMap}(r) * x = x * \text{algebraMap}(r)$.

Algebra.commute_algebraMap_right theorem

(r : R) (x : A) : Commute x (algebraMap R A r)

Full source

lemma commute_algebraMap_right (r : R) (x : A) : Commute x (algebraMap R A r) :=
  (Algebra.commutes r x).symm

Right Commutativity of Algebra Map Elements in an $R$-Algebra

Informal description

For any element $r$ in a commutative semiring $R$ and any element $x$ in an $R$-algebra $A$, the element $x$ commutes with the image of $r$ under the algebra homomorphism $\text{algebraMap} \colon R \to A$, i.e., \[ x * \text{algebraMap}(r) = \text{algebraMap}(r) * x. \]

Algebra.left_comm theorem

(x : A) (r : R) (y : A) : x * (algebraMap R A r * y) = algebraMap R A r * (x * y)

Full source

/-- `mul_left_comm` for `Algebra`s when one element is from the base ring. -/
theorem left_comm (x : A) (r : R) (y : A) :
    x * (algebraMap R A r * y) = algebraMap R A r * (x * y) := by
  rw [← mul_assoc, ← commutes, mul_assoc]

Left Commutativity of Algebra Multiplication with Scalar Action

Informal description

Let $R$ be a commutative semiring and $A$ be an $R$-algebra. For any elements $x, y \in A$ and $r \in R$, the following identity holds: \[ x \cdot (\text{algebraMap}(r) \cdot y) = \text{algebraMap}(r) \cdot (x \cdot y), \] where $\text{algebraMap} \colon R \to A$ is the canonical algebra homomorphism.

Algebra.right_comm theorem

(x : A) (r : R) (y : A) : x * algebraMap R A r * y = x * y * algebraMap R A r

Full source

/-- `mul_right_comm` for `Algebra`s when one element is from the base ring. -/
theorem right_comm (x : A) (r : R) (y : A) :
    x * algebraMap R A r * y = x * y * algebraMap R A r := by
  rw [mul_assoc, commutes, ← mul_assoc]

Right commutativity of algebra map elements in an $R$-algebra

Informal description

Let $R$ be a commutative semiring and $A$ be an $R$-algebra. For any elements $x, y \in A$ and any $r \in R$, the following equality holds: \[ x \cdot \text{algebraMap}(r) \cdot y = x \cdot y \cdot \text{algebraMap}(r), \] where $\text{algebraMap} \colon R \to A$ is the canonical algebra homomorphism.

IsScalarTower.right instance

: IsScalarTower R A A

Full source

instance _root_.IsScalarTower.right : IsScalarTower R A A :=
  ⟨fun x y z => by rw [smul_eq_mul, smul_eq_mul, smul_def, smul_def, mul_assoc]⟩

Scalar Multiplication Tower Property for Algebras

Informal description

For any commutative semiring $R$ and semiring $A$ equipped with an $R$-algebra structure, the scalar multiplication action of $R$ on $A$ satisfies the tower property with respect to $A$ acting on itself. That is, for any $r \in R$ and $x, y \in A$, we have $(r \cdot x) \cdot y = r \cdot (x \cdot y)$.

RingHom.smulOneHom_eq_algebraMap theorem

: RingHom.smulOneHom = algebraMap R A

Full source

@[simp]
theorem _root_.RingHom.smulOneHom_eq_algebraMap : RingHom.smulOneHom = algebraMap R A :=
  RingHom.ext fun r => (algebraMap_eq_smul_one r).symm

Equality of scalar multiplication homomorphism and algebra map: $\text{smulOneHom} = \text{algebraMap}$

Informal description

The ring homomorphism defined by scalar multiplication with the multiplicative identity, $x \mapsto x \cdot 1_A$, is equal to the canonical algebra homomorphism $\text{algebraMap} \colon R \to A$ for any commutative semiring $R$ and $R$-algebra $A$.

Algebra.mul_smul_comm theorem

(s : R) (x y : A) : x * s • y = s • (x * y)

Full source

/-- This is just a special case of the global `mul_smul_comm` lemma that requires less typeclass
search (and was here first). -/
@[simp]
protected theorem mul_smul_comm (s : R) (x y : A) : x * s • y = s • (x * y) := by
  rw [smul_def, smul_def, left_comm]

Commutativity of scalar multiplication with algebra multiplication: $x \cdot (s \cdot y) = s \cdot (x \cdot y)$

Informal description

Let $R$ be a commutative semiring and $A$ be an $R$-algebra. For any elements $x, y \in A$ and scalar $s \in R$, the following identity holds: \[ x \cdot (s \cdot y) = s \cdot (x \cdot y). \]

Algebra.smul_mul_assoc theorem

(r : R) (x y : A) : r • x * y = r • (x * y)

Full source

/-- This is just a special case of the global `smul_mul_assoc` lemma that requires less typeclass
search (and was here first). -/
@[simp]
protected theorem smul_mul_assoc (r : R) (x y : A) : r • x * y = r • (x * y) :=
  smul_mul_assoc r x y

Scalar Multiplication Associativity in Algebras: $r \cdot (x * y) = (r \cdot x) * y$

Informal description

Let $R$ be a commutative semiring and $A$ be a semiring with an $R$-algebra structure. For any $r \in R$ and $x, y \in A$, the scalar multiplication satisfies: $$ r \cdot (x * y) = (r \cdot x) * y. $$

smul_algebraMap theorem

 {α : Type*} [Monoid α] [MulDistribMulAction α A] [SMulCommClass α R A] (a : α) (r : R) :
  a • algebraMap R A r = algebraMap R A r

Full source

@[simp]
theorem _root_.smul_algebraMap {α : Type*} [Monoid α] [MulDistribMulAction α A]
    [SMulCommClass α R A] (a : α) (r : R) : a • algebraMap R A r = algebraMap R A r := by
  rw [algebraMap_eq_smul_one, smul_comm a r (1 : A), smul_one]

Invariance of algebra homomorphism under compatible scalar multiplication

Informal description

Let $A$ be an $R$-algebra over a commutative semiring $R$, and let $\alpha$ be a monoid acting distributively on $A$ via multiplication such that the actions of $\alpha$ and $R$ on $A$ commute. Then for any $a \in \alpha$ and $r \in R$, the scalar multiplication of $a$ with the algebra homomorphism $\text{algebraMap}(r)$ satisfies: \[ a \cdot \text{algebraMap}(r) = \text{algebraMap}(r). \]

Algebra.compHom abbrev

: Algebra S A

Full source

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

This is the algebra version of `Module.compHom`.
-/
abbrev compHom : Algebra S A where
  smul s a := f s • a
  algebraMap := (algebraMap R A).comp f
  commutes' _ _ := Algebra.commutes _ _
  smul_def' _ _ := Algebra.smul_def _ _

Induced Algebra Structure via Ring Homomorphism Composition

Informal description

Given a commutative semiring $R$ and a semiring $A$ with an $R$-algebra structure, and given a ring homomorphism $f \colon S \to R$ where $S$ is another commutative semiring, the composition $\text{algebraMap} \circ f \colon S \to A$ induces an $S$-algebra structure on $A$. More precisely, the scalar multiplication in this induced $S$-algebra structure is defined by $s \cdot x = f(s) \cdot x$ for all $s \in S$ and $x \in A$, where the right-hand side uses the original $R$-algebra structure on $A$.

Algebra.compHom_smul_def theorem

 (s : S) (x : A) :
  letI := compHom A f
  s • x = f s • x

Full source

theorem compHom_smul_def (s : S) (x : A) :
    letI := compHom A f
    s • x = f s • x := rfl

Scalar Multiplication in Induced Algebra via Ring Homomorphism

Informal description

Let $R$ be a commutative semiring, $A$ a semiring with an $R$-algebra structure, and $f \colon S \to R$ a ring homomorphism where $S$ is another commutative semiring. Then, under the induced $S$-algebra structure on $A$ via $f$, the scalar multiplication satisfies $s \cdot x = f(s) \cdot x$ for all $s \in S$ and $x \in A$, where the right-hand side uses the original $R$-algebra structure on $A$.

Algebra.compHom_algebraMap_eq theorem

 :
  letI := compHom A f
  algebraMap S A = (algebraMap R A).comp f

Full source

theorem compHom_algebraMap_eq :
    letI := compHom A f
    algebraMap S A = (algebraMap R A).comp f := rfl

Equality of Induced Algebra Map with Composition

Informal description

Let $R$ and $S$ be commutative semirings, $A$ a semiring with an $R$-algebra structure, and $f \colon S \to R$ a ring homomorphism. When $A$ is given the induced $S$-algebra structure via composition with $f$, the algebra map $\text{algebraMap}_{S \to A}$ equals the composition $\text{algebraMap}_{R \to A} \circ f$.

Algebra.compHom_algebraMap_apply theorem

 (s : S) :
  letI := compHom A f
  algebraMap S A s = (algebraMap R A) (f s)

Full source

theorem compHom_algebraMap_apply (s : S) :
    letI := compHom A f
    algebraMap S A s = (algebraMap R A) (f s) := rfl

Algebra Map Composition via Ring Homomorphism

Informal description

Let $R$ and $S$ be commutative semirings, $A$ be a semiring with an $R$-algebra structure, and $f \colon S \to R$ be a ring homomorphism. Then, under the induced $S$-algebra structure on $A$ via $f$, the algebra map $\text{algebraMap}_{S \to A}$ satisfies $\text{algebraMap}_{S \to A}(s) = \text{algebraMap}_{R \to A}(f(s))$ for all $s \in S$.

Algebra.linearMap definition

: R →ₗ[R] A

Full source

/-- The canonical ring homomorphism `algebraMap R A : R →+* A` for any `R`-algebra `A`,
packaged as an `R`-linear map.
-/
protected def linearMap : R →ₗ[R] A :=
  { algebraMap R A with map_smul' := fun x y => by simp [Algebra.smul_def] }

Canonical algebra linear map

Informal description

The canonical $R$-linear map $\text{Algebra.linearMap} \colon R \to A$ associated with an $R$-algebra structure on $A$, where $R$ is a commutative semiring and $A$ is a semiring. This map is defined as the ring homomorphism $\text{algebraMap} \colon R \to A$ equipped with the additional property that it is $R$-linear, i.e., it satisfies $\text{Algebra.linearMap}(r \cdot s) = r \cdot \text{Algebra.linearMap}(s)$ for all $r, s \in R$.

Algebra.linearMap_apply theorem

(r : R) : Algebra.linearMap R A r = algebraMap R A r

Full source

@[simp]
theorem linearMap_apply (r : R) : Algebra.linearMap R A r = algebraMap R A r :=
  rfl

Equality of Canonical Algebra Maps: $\text{Algebra.linearMap}(r) = \text{algebraMap}(r)$

Informal description

For any element $r$ in a commutative semiring $R$, the canonical $R$-linear map $\text{Algebra.linearMap} \colon R \to A$ evaluated at $r$ equals the canonical algebra homomorphism $\text{algebraMap} \colon R \to A$ evaluated at $r$, i.e., $\text{Algebra.linearMap}(r) = \text{algebraMap}(r)$.

Algebra.coe_linearMap theorem

: ⇑(Algebra.linearMap R A) = algebraMap R A

Full source

theorem coe_linearMap : ⇑(Algebra.linearMap R A) = algebraMap R A :=
  rfl

Equality of Underlying Functions: $\text{Algebra.linearMap} = \text{algebraMap}$

Informal description

The underlying function of the canonical $R$-linear map $\text{Algebra.linearMap} \colon R \to A$ is equal to the algebra homomorphism $\text{algebraMap} \colon R \to A$.

Algebra.id instance

: Algebra R R

Full source

/-- The identity map inducing an `Algebra` structure. -/
instance (priority := 1100) id : Algebra R R where
  -- We override `toFun` and `toSMul` because `RingHom.id` is not reducible and cannot
  -- be made so without a significant performance hit.
  -- see library note [reducible non-instances].
  toSMul := Mul.toSMul _
  __ := ({RingHom.id R with toFun x := x}).toAlgebra

Canonical Algebra Structure on a Commutative Semiring

Informal description

For any commutative semiring $R$, there is a canonical $R$-algebra structure on $R$ itself, where the algebra map $\text{algebraMap} \colon R \to R$ is the identity ring homomorphism.

Algebra.id.map_eq_id theorem

: algebraMap R R = RingHom.id _

Full source

@[simp]
theorem map_eq_id : algebraMap R R = RingHom.id _ :=
  rfl

Identity of the Canonical Algebra Homomorphism: $\text{algebraMap} = \text{id}$

Informal description

For any commutative semiring $R$, the canonical algebra homomorphism $\text{algebraMap} \colon R \to R$ is equal to the identity ring homomorphism on $R$.

Algebra.id.map_eq_self theorem

(x : R) : algebraMap R R x = x

Full source

theorem map_eq_self (x : R) : algebraMap R R x = x :=
  rfl

Canonical Algebra Homomorphism Acts as Identity on $R$

Informal description

For any element $x$ in a commutative semiring $R$, the canonical algebra homomorphism $\text{algebraMap} \colon R \to R$ satisfies $\text{algebraMap}(x) = x$.

Algebra.id.smul_eq_mul theorem

(x y : R) : x • y = x * y

Full source

@[simp]
theorem smul_eq_mul (x y : R) : x • y = x * y :=
  rfl

Scalar Multiplication Equals Ring Multiplication in Canonical Algebra Structure

Informal description

For any elements $x$ and $y$ in a commutative semiring $R$, the scalar multiplication $x \cdot y$ (denoted $x \• y$) is equal to the ring multiplication $x * y$.

algebraMap.coe_smul theorem

 (A B C : Type*) [SMul A B] [CommSemiring B] [Semiring C] [Algebra B C] [SMul A C] [IsScalarTower A B C] (a : A)
  (b : B) : (a • b : B) = a • (b : C)

Full source

@[norm_cast]
theorem algebraMap.coe_smul (A B C : Type*) [SMul A B] [CommSemiring B] [Semiring C] [Algebra B C]
    [SMul A C] [IsScalarTower A B C] (a : A) (b : B) : (a • b : B) = a • (b : C) := calc
  ((a • b : B) : C) = (a • b) • 1 := Algebra.algebraMap_eq_smul_one _
  _ = a • (b • 1) := smul_assoc ..
  _ = a • (b : C) := congrArg _ (Algebra.algebraMap_eq_smul_one b).symm

Compatibility of Scalar Multiplication via Algebra Map

Informal description

Let $A$, $B$, and $C$ be types with the following structures: - $A$ has a scalar multiplication operation on $B$ (denoted $A \times B \to B$). - $B$ is a commutative semiring. - $C$ is a semiring equipped with an $B$-algebra structure. - $A$ also has a scalar multiplication operation on $C$ (denoted $A \times C \to C$). - The scalar multiplications satisfy the tower property: $A$ acts on $C$ via its action on $B$. Then for any $a \in A$ and $b \in B$, the scalar multiplication $a \cdot b$ in $B$ is equal to the scalar multiplication $a \cdot b$ in $C$ (where $b$ is viewed as an element of $C$ via the algebra map $B \to C$). In symbols: \[ (a \cdot b : B) = a \cdot (b : C) \]