2023-06-09 23:27:40 -05:00
|
|
|
|
# Commutative algebra in Lean
|
2023-06-09 22:51:11 -05:00
|
|
|
|
|
2023-06-09 23:27:40 -05:00
|
|
|
|
Welcome to the repository for adding definitions and theorems related to Krull dimension and Hilbert polynomials to mathlib.
|
2023-06-09 23:05:03 -05:00
|
|
|
|
|
2023-06-09 23:27:40 -05:00
|
|
|
|
We start the commutative algebra project with a list of important definitions and theorems and go from there.
|
|
|
|
|
|
|
|
|
|
Feel free to add, modify, and expand this file. Below are starting points for the project:
|
2023-06-09 22:51:11 -05:00
|
|
|
|
|
2023-06-10 14:21:22 -05:00
|
|
|
|
- Definitions of an ideal, prime ideal, and maximal ideal:
|
|
|
|
|
```lean
|
|
|
|
|
def Mathlib.RingTheory.Ideal.Basic.Ideal (R : Type u) [Semiring R] := Submodule R R
|
|
|
|
|
```
|
2023-06-09 23:05:03 -05:00
|
|
|
|
|
2023-06-10 17:19:33 -05:00
|
|
|
|
- Definition of a Spec of a ring: `Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic.PrimeSpectrum`
|
2023-06-09 23:05:03 -05:00
|
|
|
|
|
2023-06-10 17:19:33 -05:00
|
|
|
|
- Definition of a Noetherian and Artinian rings:
|
|
|
|
|
```lean
|
|
|
|
|
class Mathlib.RingTheory.Noetherian.IsNoetherian (R M) [Semiring R] [AddCommMonoid M] [Module R M] : Prop
|
|
|
|
|
```
|
2023-06-09 22:51:11 -05:00
|
|
|
|
|
2023-06-10 14:21:22 -05:00
|
|
|
|
- Definitions of a local ring and quotient ring
|
2023-06-09 23:05:03 -05:00
|
|
|
|
|
2023-06-10 14:21:22 -05:00
|
|
|
|
- Definition of the chain of prime ideals and the length of these chains
|
2023-06-09 23:05:03 -05:00
|
|
|
|
|
2023-06-10 17:19:33 -05:00
|
|
|
|
- Definition of the Krull dimension (supremum of the lengh of chain of prime ideal): `Mathlib.Order.KrullDimension.krullDim`
|
|
|
|
|
|
|
|
|
|
- Definition of the height of prime ideal (dimension of A_p): `Mathlib.Order.KrullDimension.height`
|
2023-06-09 23:05:03 -05:00
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Give Examples of each of the above cases for a particular instances of ring
|
2023-06-09 22:51:11 -05:00
|
|
|
|
|
2023-06-10 17:19:33 -05:00
|
|
|
|
Theorem 0: Hilbert Basis Theorem:
|
|
|
|
|
```lean
|
|
|
|
|
instance isNoetherianRing [Finite σ] [IsNoetherianRing R] : IsNoetherianRing (MvPolynomial σ R)
|
|
|
|
|
```
|
2023-06-09 23:05:03 -05:00
|
|
|
|
|
2023-06-09 22:51:11 -05:00
|
|
|
|
Theorem 1: If A is a nonzero ring, then dim A[t] >= dim A +1
|
2023-06-09 23:05:03 -05:00
|
|
|
|
|
2023-06-09 22:51:11 -05:00
|
|
|
|
Theorem 2: If A is a nonzero noetherian ring, then dim A[t] = dim A + 1
|
2023-06-09 23:05:03 -05:00
|
|
|
|
|
2023-06-09 22:51:11 -05:00
|
|
|
|
Theorem 3: If A is nonzero ring then dim A_p + dim A/p <= dim A
|
2023-06-10 12:18:47 -05:00
|
|
|
|
|
2023-06-10 12:27:04 -05:00
|
|
|
|
Definition of a graded module
|