Document Open Access Logo

Group Cohomology in the Lean Community Library

Author Amelia Livingston

PDF
Thumbnail PDF

File

LIPIcs.ITP.2023.22.pdf
  • Filesize: 0.7 MB
  • 17 pages

Document Identifiers

Author Details

Amelia Livingston
  • King’s College London, UK

Funding

This work was supported by the Engineering and Physical Sciences Research Council [EP/S021590/1]. The EPSRC Centre for Doctoral Training in Geometry and Number Theory (The London School of Geometry and Number Theory), University College London

Acknowledgements

I am very grateful to Kevin Buzzard for his ongoing mathematical and Lean-related support and guidance. I am also indebted to Joël Riou for his explanation of the simplicial interpretation of group cohomology and his thorough reviewing of and advice regarding my work, and for his formalisation of some of the results I used. I also depended heavily on Scott Morrison’s development of Lean’s representation theory library and the category theory library more generally. Finally, thanks to anyone who answered my questions on the Xena Project Discord server and the Lean Zulip.

Cite AsGet BibTex

Amelia Livingston. Group Cohomology in the Lean Community Library. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITP.2023.22

Abstract

Group cohomology is a tool which has become indispensable in a wide range of modern mathematics, like algebraic geometry and algebraic number theory, as well as group theory itself. For example, it allows us to reformulate classical class field theory in cohomological terms; this formulation is essential to landmarks of modern number theory, like Wiles’s proof of Fermat’s Last Theorem. We explore the challenges of formalising group cohomology in the Lean theorem prover in a generality suitable for inclusion in the community library mathlib.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Type theory
Keywords
  • formal math
  • Lean
  • mathlib
  • group cohomology
  • homological algebra

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Anne Baanen. Use and Abuse of Instance Parameters in the Lean Mathematical Library. In June Andronick and Leonardo de Moura, editors, 13th International Conference on Interactive Theorem Proving (ITP 2022), volume 237 of Leibniz International Proceedings in Informatics (LIPIcs), pages 4:1-4:20, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2022.4.
  2. John W. S. Cassels and Albrecht Fröhlich. Algebraic Number Theory. London Mathematical Society, London, 2010. Google Scholar
  3. María Inés de Frutos-Fernández. Formalizing the Ring of Adèles of a Global Field. In 13th International Conference on Interactive Theorem Proving (ITP 2022), volume 237, pages 14:1-14:18, 2022. URL: https://drops.dagstuhl.de/opus/volltexte/2022/16723/pdf/LIPIcs-ITP-2022-14.pdf.
  4. César Domínguez and Julio Rubio. Computing in coq with infinite algebraic data structures. In Proceedings of the 10th ASIC and 9th MKM International Conference, and 17th Calculemus Conference on Intelligent Computer Mathematics, volume 6167, April 2010. URL: https://doi.org/10.1007/978-3-642-14128-7_18.
  5. Paul G. Goerss and John F. Jardine. Simplicial Homotopy Theory. Springer Science & Business Media, 2009. URL: https://doi.org/10.1007/978-3-0346-0189-4.
  6. Gerhard Hochschild and Jean-Pierre Serre. Cohomology of group extensions. Transactions of the American Mathematical Society, 74(1):110-134, 1953. URL: https://doi.org/10.1090/S0002-9947-1953-0052438-8.
  7. Shin-ichi Katayama. Diophantine Equations and Hilbert’s Theorem 90. Journal of mathematics, the University of Tokushima, 48:35-40, 2014. URL: https://cir.nii.ac.jp/crid/1574231877578024320.
  8. Ernst E. Kummer. Über eine besondere Art, aus complexen Einheiten gebildeter Ausdrücke. Journal für die reine und angewandte Mathematik, 1855(50):212-232, 1855. URL: https://doi.org/10.1515/crll.1855.50.212.
  9. Serge Lang. Algebra, volume 211. Springer Science & Business Media, 2012. URL: https://doi.org/10.1007/978-1-4613-0041-0.
  10. The mathlib Community. The Lean Mathematical Library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 367-381, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3372885.3373824.
  11. nLab authors. Moore complex. https://ncatlab.org/nlab/show/Moore+complex, February 2023. URL: https://ncatlab.org/nlab/revision/Moore+complex/59.
  12. The Stacks project authors. The stacks project. https://stacks.math.columbia.edu, 2023.
  13. Charles A. Weibel. An Introduction to Homological Algebra. Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1994. URL: https://doi.org/10.1017/CBO9781139644136.
  14. Charles A. Weibel. History of Homological Algebra. In Ioan M. James, editor, History of Topology, chapter 28, pages 797-836. North Holland, 1999. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact