Formalizing Double Groupoids and Cross Modules in the Lean Theorem Prover

DOI10.1007/978-3-319-42432-3_4zbMath1434.68647OpenAlexW2500686156MaRDI QIDQ2819195

Jakob von Raumer

Publication date: 28 September 2016

Published in: Mathematical Software – ICMS 2016 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-42432-3_4

zbMATH Keywords

algebraic topologyformalization of mathematics

Mathematics Subject Classification ID

Nonabelian homological algebra (category-theoretic aspects) (18G50) Groupoids (i.e. small categories in which all morphisms are isomorphisms) (20L05) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) 2-groups, crossed modules, crossed complexes (18G45)

Related Items (1)

Lean

Cites Work

• Nonabelian algebraic topology. Filtered spaces, crossed complexes, cubical homotopy groupoids. With contributions by Christopher D. Wensley and Sergei V. Soloviev
• The Lean Theorem Prover (System Description)

This page was built for publication: Formalizing Double Groupoids and Cross Modules in the Lean Theorem Prover