SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2024-12-26 07:38:36 -06:00
Code Issues Projects Releases Packages Wiki Activity

Merge pull request #7 from GTBarkley/grant

Browse source 
added bullets and the definition of an ideal from mathlib
This commit is contained in:
GTBarkley 2023-06-10 12:22:29 -07:00 committed by GitHub
commit 73a1edf070
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 10 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
README.md
View file

@ -6,19 +6,22 @@ We start the commutative algebra project with a list of important definitions an
Feel free to add, modify, and expand this file. Below are starting points for the project:
Definitions of an ideal, prime ideal, and maximal ideal
- Definitions of an ideal, prime ideal, and maximal ideal:
```lean
def Mathlib.RingTheory.Ideal.Basic.Ideal (R : Type u) [Semiring R] := Submodule R R
```
Definition of a Spec of a ring
- Definition of a Spec of a ring
Definition of a Noetherian and Artinian rings
- Definition of a Noetherian and Artinian rings
Definitions of a local ring and quotient ring
- Definitions of a local ring and quotient ring
Definition of the chain of prime ideals and the length of these chains
- Definition of the chain of prime ideals and the length of these chains
Definition of the Krull dimension (supremum of the lengh of chain of prime ideal)
- Definition of the Krull dimension (supremum of the lengh of chain of prime ideal)
Definition of the height of prime ideal (dimension of A_p)
- Definition of the height of prime ideal (dimension of A_p)
Give Examples of each of the above cases for a particular instances of ring