Potential projects

This is a rough list (from the Orsay meeting) of mathematics that we'd like to see in Lean, and that should be not-too-hard from where we are now.

Analysis

• trigonometric functions, π
• integrals on measure spaces
• Bochner integrals
• Fréchet derivatives
• Stone-Weierstrauss
• smooth manifolds

Linear algebra

• finite dimensional vector spaces
• matrices
  • determinant and trace
  • Gaussian elimination
• tensor and exterior algebra
• classification of quadratic forms by signature
• Ellenberg-Gijswijt (Johannes)

Galois theory

• field homomorphisms are injective
• splitting fields
• finite fields
  • e.g. as splitting fields for x^(p^k) - x
• finite extensions

Number theory

• Quadratic reciprocity (Chris)

Commutative algebra

• PIDs
• Smith normal form (do Gaussian elimination first!) and the structure theorem for modules over a PID
• Noetherian rings
  • modules over Noetherian rings

Category theory

• limits/colimits (Scott)
• sheaves
• enriched categories
• 'concrete' categories
• adjunctions

Algebraic topology

• connectedness
• fundamental groups (higher homotopy groups?)
• singular/cellular/... homology
• Brouwer fixed point theorem
• Eilenberg-Steenrod axioms
• suspensions, mapping spaces, loop spaces
• O(n) is homotopy equivalent to GL(n)

Longer term

• some representation theory?
• some Lie theory?
• simplicial sets are a model category
• Bott periodicity