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, π (see also)
• integrals on measure spaces
• Bochner integrals
• Fréchet derivatives
• Stone-Weierstrauss
• smooth manifolds

Linear algebra

• finite dimensional vector spaces (UROP)
• matrices (work done by Ellen Arlt here)
  • links to linear maps (work done by Blair Shi and Keji Neri here)
  • determinant and trace (work done by Keji Neri here)
  • Cayley--Hamilton
  • Gaussian elimination
• tensor and exterior algebra (note Kenny Lau's work on tensor products)
• classification of quadratic forms by signature
• Ellenberg-Gijswijt (Johannes)

Galois theory

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

Number theory

• Quadratic reciprocity (Chris) (this has been PR'ed!)
• Number fields (waiting for module refactoring)
• Adeles (see former issue)

Commutative algebra

• PIDs (definition is in mathlib, by Chris)
• Smith normal form (do Gaussian elimination first!) and the structure theorem for modules over a PID
• Noetherian rings
  • Noetherian modules over Noetherian rings (community)
  • Hilbert basis theorem

Category theory

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

Algebraic topology

• connectedness (UROP -- see connected_spaces, path_connectedness and local_connectedness files)
• fundamental groups (higher homotopy groups?) (UROP, Reid)
• singular/cellular/... homology (Johan)
• 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