SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2024-10-16 11:37:05 -05:00
Code Issues Projects Releases Packages Wiki Activity

added bullets and the definition of an ideal from mathlib

Browse source
This commit is contained in:
GTBarkley 2023-06-10 15:21:22 -04:00 committed by GitHub
parent d736cf81b3
commit 223660606b
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