Completing the Cohomological Extension Package: Section Cocycles and Splitting Criterion for Mathlib
Fuente:
Zenodo
Salvato in:
| Autore principale: | |
|---|---|
| Natura: | Recurso digital |
| Lingua: | inglese |
| Pubblicazione: |
Zenodo
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866901749308063744 |
|---|---|
| author | Spivack, Nova |
| author_facet | Spivack, Nova |
| contents | Mathlib's GroupExtension/Defs.lean documents two explicit TODO items: a bijection between N-conjugacy classes of splittings and H^1, and a bijection between equivalence classes of group extensions and H^2, both for abelian kernel N. Neither is currently formalized. This technical note documents a proposed Mathlib contribution that constitutes Phase 1 of completing these TODOs: the section cocycle associated to a set-theoretic section of a group extension, the splitting criterion (splits_iff_trivial_cocycle), and supporting infrastructure including the section difference function, the conjugation action via sections, and the multiplicative 2-cocycle identity. All theorems are fully verified by the Lean type checker with zero sorry. We describe the proposed API surface, design decisions (nam |
| format | Recurso digital |
| id | zenodo_https___doi_org_10_5281_zenodo_19430566 |
| institution | Zenodo |
| language | eng |
| publishDate | 2026 |
| publisher | Zenodo |
| record_format | zenodo |
| spellingShingle | Completing the Cohomological Extension Package: Section Cocycles and Splitting Criterion for Mathlib Spivack, Nova Lean 4 formal verification infinity compression reflexive systems machine-checked proof NEMS preprint Mathlib's GroupExtension/Defs.lean documents two explicit TODO items: a bijection between N-conjugacy classes of splittings and H^1, and a bijection between equivalence classes of group extensions and H^2, both for abelian kernel N. Neither is currently formalized. This technical note documents a proposed Mathlib contribution that constitutes Phase 1 of completing these TODOs: the section cocycle associated to a set-theoretic section of a group extension, the splitting criterion (splits_iff_trivial_cocycle), and supporting infrastructure including the section difference function, the conjugation action via sections, and the multiplicative 2-cocycle identity. All theorems are fully verified by the Lean type checker with zero sorry. We describe the proposed API surface, design decisions (nam |
| title | Completing the Cohomological Extension Package: Section Cocycles and Splitting Criterion for Mathlib |
| topic | Lean 4 formal verification infinity compression reflexive systems machine-checked proof NEMS preprint |
| url | https://doi.org/10.5281/zenodo.19430566 |