1.2 Commutative rings and modules

1.2.1 Reminder: Commutative rings

Definition 1.42

✓

A commutative ring means a set \(K\) equipped with three maps

\begin{align*} \oplus & :K\times K\rightarrow K,\\ \ominus & :K\times K\rightarrow K,\\ \odot & :K\times K\rightarrow K \end{align*}

and two elements \(\mathbf{0}\in K\) and \(\mathbf{1}\in K\) satisfying the following axioms:

Commutativity of addition: We have \(a\oplus b=b\oplus a\) for all \(a,b\in K\).
Associativity of addition: We have \(a\oplus \left( b\oplus c\right) =\left( a\oplus b\right) \oplus c\) for all \(a,b,c\in K\).
Neutrality of zero: We have \(a\oplus \mathbf{0}=\mathbf{0}\oplus a=a\) for all \(a\in K\).
Subtraction undoes addition: Let \(a,b,c\in K\). We have \(a\oplus b=c\) if and only if \(a=c\ominus b\).
Commutativity of multiplication: We have \(a\odot b=b\odot a\) for all \(a,b\in K\).
Associativity of multiplication: We have \(a\odot \left( b\odot c\right) =\left( a\odot b\right) \odot c\) for all \(a,b,c\in K\).
Distributivity: We have

\[ a\odot \left( b\oplus c\right) =\left( a\odot b\right) \oplus \left( a\odot c\right) \ \ \ \ \ \ \ \ \ \ \text{and}\ \ \ \ \ \ \ \ \ \ \left( a\oplus b\right) \odot c=\left( a\odot c\right) \oplus \left( b\odot c\right) \]

for all \(a,b,c\in K\).
Neutrality of one: We have \(a\odot \mathbf{1}=\mathbf{1}\odot a=a\) for all \(a\in K\).
Annihilation: We have \(a\odot \mathbf{0}=\mathbf{0}\odot a=\mathbf{0}\) for all \(a\in K\).

The operations \(\oplus \), \(\ominus \) and \(\odot \) are called the addition, the subtraction and the multiplication of the ring \(K\). When confusion is unlikely, we will denote these three operations \(\oplus \), \(\ominus \) and \(\odot \) by \(+\), \(-\) and \(\cdot \), respectively, and we will abbreviate \(a\odot b=a\cdot b\) by \(ab\).

The elements \(\mathbf{0}\) and \(\mathbf{1}\) are called the zero and the unity (or the one) of the ring \(K\). We will simply call these elements \(0\) and \(1\) when confusion with the corresponding numbers is unlikely.

We will use PEMDAS conventions for the three operations \(\oplus \), \(\ominus \) and \(\odot \). These imply that the operation \(\odot \) has higher precedence than \(\oplus \) and \(\ominus \), while the operations \(\oplus \) and \(\ominus \) are left-associative.

docs source

theorem AlgebraicCombinatorics.FPS.commRing_add_comm {K : Type u_1} [CommRing K] (a b : K) :

a + b = b + a

docs source

theorem AlgebraicCombinatorics.FPS.commRing_add_assoc {K : Type u_1} [CommRing K] (a b c : K) :

a + (b + c) = a + b + c

docs source

theorem AlgebraicCombinatorics.FPS.commRing_add_zero {K : Type u_1} [CommRing K] (a : K) :

a + 0 = a

docs source

theorem AlgebraicCombinatorics.FPS.commRing_sub_iff_add {K : Type u_1} [CommRing K] (a b c : K) :

a + b = c ↔ a = c - b

docs source

theorem AlgebraicCombinatorics.FPS.commRing_mul_comm {K : Type u_1} [CommRing K] (a b : K) :

a * b = b * a

docs source

theorem AlgebraicCombinatorics.FPS.commRing_mul_assoc {K : Type u_1} [CommRing K] (a b c : K) :

a * (b * c) = a * b * c

docs source

theorem AlgebraicCombinatorics.FPS.commRing_left_distrib {K : Type u_1} [CommRing K] (a b c : K) :

a * (b + c) = a * b + a * c

docs source

theorem AlgebraicCombinatorics.FPS.commRing_mul_one {K : Type u_1} [CommRing K] (a : K) :

a * 1 = a

docs source

theorem AlgebraicCombinatorics.FPS.commRing_mul_zero {K : Type u_1} [CommRing K] (a : K) :

a * 0 = 0

1.2.2 Standard rules in commutative rings

Lemma 1.43

✓

Let \(K\) be a commutative ring. For any \(a,b\in K\), we have \(-\left( a+b\right) =\left( -a\right) +\left( -b\right)\).

docs source

theorem AlgebraicCombinatorics.FPS.neg_add_distrib {K : Type u_1} [CommRing K] (a b : K) :

-(a + b) = -a + -b

Proof ▶

Standard ring theory.

Lemma 1.44

✓

Let \(K\) be a commutative ring. For any \(a\in K\), we have \(-\left( -a\right) =a\).

docs source

theorem AlgebraicCombinatorics.FPS.neg_neg_eq {K : Type u_1} [CommRing K] (a : K) :

- -a = a

Proof ▶

Standard ring theory.

Lemma 1.45

✓

Let \(K\) be a commutative ring. For any \(a\in K\) and \(n,m\in \mathbb {Z}\), we have \(\left( n+m\right) a=na+ma\).

docs source

theorem AlgebraicCombinatorics.FPS.add_zsmul_distrib {K : Type u_1} [CommRing K] (a : K) (n m : ℤ) :

(n + m) • a = n • a + m • a

Proof ▶

Standard ring theory.

Lemma 1.46

✓

Let \(K\) be a commutative ring. For any \(a\in K\) and \(n,m\in \mathbb {Z}\), we have \(\left( nm\right) a=n\left( ma\right)\).

docs source

theorem AlgebraicCombinatorics.FPS.mul_zsmul_assoc {K : Type u_1} [CommRing K] (a : K) (n m : ℤ) :

(n * m) • a = n • m • a

Proof ▶

Standard ring theory.

Lemma 1.47

✓

Let \(K\) be a commutative ring. For any \(a,b,c\in K\), we have \(a\left( b-c\right) =\left( ab\right) -\left( ac\right)\).

docs source

theorem AlgebraicCombinatorics.FPS.mul_sub_distrib {K : Type u_1} [CommRing K] (a b c : K) :

a * (b - c) = a * b - a * c

Proof ▶

Standard ring theory.

Lemma 1.48

✓

Let \(K\) be a commutative ring. For any \(a,b\in K\) and \(n\in \mathbb {N}\), we have \(\left( ab\right) ^{n}=a^{n}b^{n}\).

docs source

theorem AlgebraicCombinatorics.FPS.mul_pow_eq {K : Type u_1} [CommRing K] (a b : K) (n : ℕ) :

(a * b) ^ n = a ^ n * b ^ n

Proof ▶

Standard ring theory (induction on \(n\)).

Lemma 1.49

✓

Let \(K\) be a commutative ring. For any \(a\in K\) and \(n,m\in \mathbb {N}\), we have \(a^{n+m}=a^{n}a^{m}\).

docs source

theorem AlgebraicCombinatorics.FPS.pow_add_eq {K : Type u_1} [CommRing K] (a : K) (n m : ℕ) :

a ^ (n + m) = a ^ n * a ^ m

Proof ▶

Standard ring theory (induction on \(m\)).

Lemma 1.50

✓

Let \(K\) be a commutative ring. For any \(a\in K\) and \(n,m\in \mathbb {N}\), we have \(a^{nm}=\left( a^{n}\right) ^{m}\).

docs source

theorem AlgebraicCombinatorics.FPS.pow_mul_eq {K : Type u_1} [CommRing K] (a : K) (n m : ℕ) :

a ^ (n * m) = (a ^ n) ^ m

Proof ▶

Standard ring theory (induction on \(m\)).

Theorem 1.51

(Binomial Theorem.) Let \(K\) be a commutative ring. For any \(a,b\in K\) and \(n\in \mathbb {N}\),

\[ (a+b)^n = \sum _{k=0}^{n} \binom {n}{k} a^k b^{n-k}. \]

docs source

theorem AlgebraicCombinatorics.FPS.binomial_theorem {K : Type u_1} [CommRing K] (a b : K) (n : ℕ) :

(a + b) ^ n = ∑ k ∈ Finset.range (n + 1), a ^ k * b ^ (n - k) * ↑(n.choose k)

Proof ▶

Standard; this is the binomial theorem from Mathlib.

Lemma 1.52

✓

Let \(K\) be a commutative ring. For any \(a,b\in K\) and \(n\in \mathbb {N}\),

\[ (a-b)^n = \sum _{m=0}^{n} (-1)^{m+n} \cdot a^m \cdot b^{n-m} \cdot \binom {n}{m}. \]

docs source

theorem AlgebraicCombinatorics.FPS.binomial_theorem_sub {K : Type u_1} [CommRing K] (a b : K) (n : ℕ) :

(a - b) ^ n = ∑ m ∈ Finset.range (n + 1), (-1) ^ (m + n) * a ^ m * b ^ (n - m) * ↑(n.choose m)

Proof ▶

Write \(a - b = a + (-b)\) and apply Theorem 1.51.

1.2.3 Finite sums and products

Lemma 1.53

✓

Let \(K\) be a commutative ring. Let \(S\) be a finite type, and let \(X, Y\) be disjoint finite subsets of \(S\). For any family \((a_s)_{s \in S}\) of elements of \(K\), we have \(\sum _{s\in X\cup Y}a_{s}=\sum _{s\in X}a_{s}+\sum _{s\in Y}a_{s}\).

docs source

theorem AlgebraicCombinatorics.FPS.sum_disjoint_union {K : Type u_1} [CommRing K] {S : Type u_2} [DecidableEq S] {X Y : Finset S} (hXY : Disjoint X Y) (f : S → K) :

∑ s ∈ X ∪ Y, f s = ∑ s ∈ X, f s + ∑ s ∈ Y, f s

Proof ▶

Standard.

Lemma 1.54

✓

Let \(K\) be a commutative ring. Let \(T\) be a finite set and \((a_s)_{s\in T}\), \((b_s)_{s\in T}\) be two families of elements of \(K\). Then \(\sum _{s\in T}\left( a_{s}+b_{s}\right) =\sum _{s\in T}a_{s}+\sum _{s\in T}b_{s}\).

docs source

theorem AlgebraicCombinatorics.FPS.sum_add_distrib' {K : Type u_1} [CommRing K] {S : Type u_2} {T : Finset S} (f g : S → K) :

∑ s ∈ T, (f s + g s) = ∑ s ∈ T, f s + ∑ s ∈ T, g s

Proof ▶

Standard.

Lemma 1.55

✓

Let \(K\) be a commutative ring. If \(S=\varnothing \), then \(\sum _{s\in S}a_{s}=0\).

docs source

theorem AlgebraicCombinatorics.FPS.sum_empty {K : Type u_1} [CommRing K] {S : Type u_2} (f : S → K) :

∑ _s ∈ ∅, f _s = 0

Proof ▶

By definition.

Lemma 1.56

✓

Let \(K\) be a commutative ring. If \(S=\varnothing \), then \(\prod _{s\in S}a_{s}=1\).

docs source

theorem AlgebraicCombinatorics.FPS.prod_empty {K : Type u_1} [CommRing K] {S : Type u_2} (f : S → K) :

∏ _s ∈ ∅, f _s = 1

Proof ▶

By definition.

1.2.4 \(K\)-modules

Definition 1.57

✓

Let \(K\) be a commutative ring.

A \(K\)-module means a set \(M\) equipped with three maps

\begin{align*} \oplus & :M\times M\rightarrow M,\\ \ominus & :M\times M\rightarrow M,\\ \rightharpoonup & :K\times M\rightarrow M \end{align*}

(notice that the third map has domain \(K\times M\), not \(M\times M\)) and an element \(\overrightarrow {0}\in M\) satisfying the following axioms:

Commutativity of addition: We have \(a\oplus b=b\oplus a\) for all \(a,b\in M\).
Associativity of addition: We have \(a\oplus \left( b\oplus c\right) =\left( a\oplus b\right) \oplus c\) for all \(a,b,c\in M\).
Neutrality of zero: We have \(a\oplus \overrightarrow {0}=\overrightarrow {0}\oplus a=a\) for all \(a\in M\).
Subtraction undoes addition: Let \(a,b,c\in M\). We have \(a\oplus b=c\) if and only if \(a=c\ominus b\).
Associativity of scaling: We have \(u\rightharpoonup \left( v\rightharpoonup a\right) =\left( uv\right) \rightharpoonup a\) for all \(u,v\in K\) and \(a\in M\).
Left distributivity: We have \(u\rightharpoonup \left( a\oplus b\right) =\left( u\rightharpoonup a\right) \oplus \left( u\rightharpoonup b\right) \) for all \(u\in K\) and \(a,b\in M\).
Right distributivity: We have \(\left( u+v\right) \rightharpoonup a=\left( u\rightharpoonup a\right) \oplus \left( v\rightharpoonup a\right) \) for all \(u,v\in K\) and \(a\in M\).
Neutrality of one: We have \(1\rightharpoonup a=a\) for all \(a\in M\).
Left annihilation: We have \(0\rightharpoonup a=\overrightarrow {0}\) for all \(a\in M\).
Right annihilation: We have \(u\rightharpoonup \overrightarrow {0}=\overrightarrow {0}\) for all \(u\in K\).

The operations \(\oplus \), \(\ominus \) and \(\rightharpoonup \) are called the addition, the subtraction and the scaling (or the \(K\)-action) of the \(K\)-module \(M\). When confusion is unlikely, we will denote these three operations \(\oplus \), \(\ominus \) and \(\rightharpoonup \) by \(+\), \(-\) and \(\cdot \), respectively, and we will abbreviate \(a\rightharpoonup b=a\cdot b\) by \(ab\).

The element \(\overrightarrow {0}\) is called the zero (or the zero vector) of the \(K\)-module \(M\). We will usually just call it \(0\).

When \(M\) is a \(K\)-module, the elements of \(M\) are called vectors, while the elements of \(K\) are called scalars.

We will use PEMDAS conventions for the three operations \(\oplus \), \(\ominus \) and \(\rightharpoonup \), with the operation \(\rightharpoonup \) having higher precedence than \(\oplus \) and \(\ominus \).

docs source

theorem AlgebraicCombinatorics.FPS.module_add_comm {M : Type u_2} [AddCommGroup M] (a b : M) :

a + b = b + a

docs source

theorem AlgebraicCombinatorics.FPS.module_add_assoc {M : Type u_2} [AddCommGroup M] (a b c : M) :

a + (b + c) = a + b + c

docs source

theorem AlgebraicCombinatorics.FPS.module_add_zero {M : Type u_2} [AddCommGroup M] (a : M) :

a + 0 = a

docs source

theorem AlgebraicCombinatorics.FPS.module_sub_iff_add {M : Type u_2} [AddCommGroup M] (a b c : M) :

a + b = c ↔ a = c - b

docs source

theorem AlgebraicCombinatorics.FPS.module_smul_assoc {K : Type u_1} [CommRing K] {M : Type u_2} [AddCommGroup M] [Module K M] (u v : K) (a : M) :

u • v • a = (u * v) • a

docs source

theorem AlgebraicCombinatorics.FPS.module_smul_add {K : Type u_1} [CommRing K] {M : Type u_2} [AddCommGroup M] [Module K M] (u : K) (a b : M) :

u • (a + b) = u • a + u • b

docs source

theorem AlgebraicCombinatorics.FPS.module_add_smul {K : Type u_1} [CommRing K] {M : Type u_2} [AddCommGroup M] [Module K M] (u v : K) (a : M) :

(u + v) • a = u • a + v • a

docs source

theorem AlgebraicCombinatorics.FPS.module_one_smul {K : Type u_1} [CommRing K] {M : Type u_2} [AddCommGroup M] [Module K M] (a : M) :

1 • a = a

docs source

theorem AlgebraicCombinatorics.FPS.module_zero_smul {K : Type u_1} [CommRing K] {M : Type u_2} [AddCommGroup M] [Module K M] (a : M) :

0 • a = 0

docs source

theorem AlgebraicCombinatorics.FPS.module_smul_zero {K : Type u_1} [CommRing K] {M : Type u_2} [AddCommGroup M] [Module K M] (u : K) :

u • 0 = 0

1.2.5 Additive inverses in modules

Lemma 1.58

✓

Let \(K\) be a commutative ring and \(M\) a \(K\)-module. For any \(a\in M\), the additive inverse of \(a\) can be constructed as \((-1)\cdot a\), i.e., \(-a = (-1)\cdot a\).

docs source

theorem AlgebraicCombinatorics.FPS.module_neg_eq_neg_one_smul {K : Type u_1} [CommRing K] {M : Type u_2} [AddCommGroup M] [Module K M] (a : M) :

-a = -1 • a

Proof ▶

Standard module theory.

Lemma 1.59

✓

Let \(K\) be a commutative ring and \(M\) a \(K\)-module. For any \(a,b\in M\), we have \(a - b = a + (-b)\).

docs source

theorem AlgebraicCombinatorics.FPS.module_sub_eq_add_neg {M : Type u_2} [AddCommGroup M] (a b : M) :

a - b = a + -b

Proof ▶

Standard module theory.

Lemma 1.60

✓

Let \(K\) be a commutative ring and \(M\) a \(K\)-module. For any \(a,b\in M\), we have \(a - b = a + (-1)\cdot b\).

docs source

theorem AlgebraicCombinatorics.FPS.module_sub_eq_add_neg_one_smul {K : Type u_1} [CommRing K] {M : Type u_2} [AddCommGroup M] [Module K M] (a b : M) :

a - b = a + -1 • b

Proof ▶

Combine the fact that \(-b = (-1)\cdot b\) with \(a - b = a + (-b)\).

Lemma 1.61

✓

Let \(K\) be a commutative ring and \(M\) a \(K\)-module. For any \(a,b\in M\), we have \(-(a+b) = (-a) + (-b)\).

docs source

theorem AlgebraicCombinatorics.FPS.module_neg_add {M : Type u_2} [AddCommGroup M] (a b : M) :

-(a + b) = -a + -b

Proof ▶

Standard module theory.

Lemma 1.62

✓

Let \(K\) be a commutative ring and \(M\) a \(K\)-module. For any \(a\in M\), we have \(-(-a) = a\).

docs source

theorem AlgebraicCombinatorics.FPS.module_neg_neg {M : Type u_2} [AddCommGroup M] (a : M) :

- -a = a

Proof ▶

Standard module theory.

1.2.6 Inverses in commutative rings

Definition 1.63

✓

Let \(L\) be a commutative ring and \(a, b \in L\).

(a) We say that \(b\) is an inverse (or multiplicative inverse) of \(a\) if \(a \cdot b = 1\).

(b) We say that \(a\) is invertible in \(L\) (or a unit of \(L\)) if \(a\) has an inverse.

docs source

def AlgebraicCombinatorics.FPS.IsInverse {L : Type u_1} [CommRing L] (a b : L) :

Prop

AlgebraicCombinatorics.FPS.IsInverse a b = (a * b = 1)

Lemma 1.64

✓

Let \(L\) be a commutative ring. If \(b\) and \(c\) are both inverses of \(a\), then \(b = c\). In other words, the inverse of an element (if it exists) is unique.

docs source

theorem AlgebraicCombinatorics.FPS.isInverse_unique {L : Type u_1} [CommRing L] {a b c : L} (hab : IsInverse a b) (hac : IsInverse a c) :

b = c

Proof ▶

We have \(b = b \cdot 1 = b \cdot (a \cdot c) = (b \cdot a) \cdot c = 1 \cdot c = c\).

Definition 1.65

✓

An element \(a \in L\) is invertible if there exists \(b \in L\) such that \(a \cdot b = 1\).

docs source

def AlgebraicCombinatorics.FPS.IsInvertible {L : Type u_1} [CommRing L] (a : L) :

Prop

AlgebraicCombinatorics.FPS.IsInvertible a = ∃ (b : L), AlgebraicCombinatorics.FPS.IsInverse a b

Lemma 1.66

✓

The definition of invertibility from Definition 1.63 is equivalent to the definition of a unit in Mathlib.

docs source

theorem AlgebraicCombinatorics.FPS.isInvertible_iff_isUnit {L : Type u_1} [CommRing L] (a : L) :

IsInvertible a ↔ IsUnit a

Proof ▶

Both express the existence of a multiplicative inverse; the equivalence is immediate from the definitions.

Lemma 1.67

✓

If \(a\) and \(b\) are invertible in \(L\), then \(a \cdot b\) is invertible.

docs source

theorem AlgebraicCombinatorics.FPS.isInvertible_mul {L : Type u_1} [CommRing L] {a b : L} (ha : IsInvertible a) (hb : IsInvertible b) :

IsInvertible (a * b)

Proof ▶

Convert to the equivalent notion of a unit and use the fact that the product of two units is a unit.

Lemma 1.68

✓

In a field \(F\), an element \(a\) is invertible if and only if \(a \neq 0\).

docs source

theorem AlgebraicCombinatorics.FPS.field_isUnit_iff {F : Type u_2} [Field F] {a : F} :

IsUnit a ↔ a ≠ 0

Proof ▶

Every nonzero element of a field has a multiplicative inverse.

1.2.7 Fractions and integer powers

Definition 1.69

✓

For an invertible element \(a\) and any \(b \in L\), the fraction \(b/a\) is defined as \(b \cdot a^{-1}\).

docs source

def AlgebraicCombinatorics.FPS.fraction {L : Type u_1} [CommRing L] (b : L) (u : Lˣ) :

AlgebraicCombinatorics.FPS.fraction b u = b * ↑u⁻¹

Lemma 1.70

✓

For an invertible element \(a\) and elements \(b, c \in L\), we have \(b / a = c\) if and only if \(b = c \cdot a\).

docs source

theorem AlgebraicCombinatorics.FPS.fraction_eq_iff {L : Type u_1} [CommRing L] (b c : L) (u : Lˣ) :

fraction b u = c ↔ b = c * ↑u

Proof ▶

Multiply both sides by \(a\) (or \(a^{-1}\)) and use \(a \cdot a^{-1} = 1\).

Lemma 1.71

✓

For an invertible element \(a\) and a natural number \(n\), we have \(a^{-n} = (a^{-1})^n\). This defines negative integer powers.

docs source

theorem AlgebraicCombinatorics.FPS.unit_zpow_neg {L : Type u_1} [CommRing L] (u : Lˣ) (n : ℕ) :

u ^ (-↑n) = u⁻¹ ^ n

Proof ▶

By the definition of integer powers on units.

Lemma 1.72

✓

For an invertible element \(a\) and integers \(m, n \in \mathbb {Z}\), we have \(a^{m+n} = a^m \cdot a^n\).

docs source

theorem AlgebraicCombinatorics.FPS.unit_zpow_add {L : Type u_1} [CommRing L] (u : Lˣ) (m n : ℤ) :

u ^ (m + n) = u ^ m * u ^ n

Proof ▶

Standard property of integer powers.