/commalg

Commutative algebra in Coq/SSReflect

Primary LanguageCoqMIT LicenseMIT

Commutative algebra in Coq/SSReflect

Commutative algebra formalized in Coq using SSReflect/MathComp & packed classes. This repository is part of the Coq/SSReflect algebraic geometry project.

The development currently consists of the following files:

  • classical.v: exports libraries required for classical reasoning, and some additional lemmas. Currently, we assume functional extensionality, Prop extensionality, decidable equality for every type, and the (type-theoretic) Axiom of Choice. The Axiom of Choice, in particular, is required to prove statements such as Krull's theorem;
  • unit.v: unitRing structure for every ring (from classical reasoning);
  • ideal.v: some facts about ideals (e.g., intersection of ideals is an ideal);
  • maximal.v: defines maximal ideals and lemmas about them. Currently, we are working on proving Krull's theorem (every nonzero ring has a maximal ideal);
  • noetherian.v: defines Noetherian rings. Two goal theorems are: (1) a ring is Noetherian iff every ideal is finitely generated, and (2) Hilbert's basis theorem (R[x] is Noetherian if R is Noetherian);
  • local.v: basic facts about local rings;
  • localization.v: the localization of a ring, one of the most important constructions in algebraic geometry;
  • nilpotent.v: facts about nilpotents and the nilradical of a ring.

All rings here are commutative and has 1, as is conventional in commutative algebra. We don't really have a canonical reference here, but we often refer to:

  • David Eisenbud, Commutative Algebra with a View Toward Algebraic Geometry (i.e., GTM 150);
  • M. F. Atiyah & I. G. MacDonald, Introduction to Commutative Algebra;
  • and the Stacks Project.

Usage

Generate the Makefile:

coq_makefile -f _CoqProject -o Makefile

and then run make.

Alternatively, use opam: opam pin . then opam install.

Author

Xuanrui Qi (xuanrui@nagoya-u.jp, me@xuanruiqi.com), with the assistance of:

License

MIT License