P3Group

$p^3$ 阶群分类的 Lean 4 形式化（其中 $p$ 为素数）， 基于 mathlib4。

论文

概述论文：Classifying the Groups of Order p^3 in Lean， 见 arxiv:2606.26141。

主要结果

每个 $p^3$ 阶有限群（其中 $p$ 为素数）都同构于五个群之一。 在同构意义下，它们分别是：

p 为奇素数

群	结构
循环群	$\mathbb{Z}/p^3\mathbb{Z}$
阿贝尔群	$\mathbb{Z}/p^2\mathbb{Z} \times \mathbb{Z}/p\mathbb{Z}$
初等阿贝尔群	$(\mathbb{Z}/p\mathbb{Z})^3$
Heisenberg 群	$\mathrm{Heis}(\mathbb{Z}/p\mathbb{Z})$ · 指数为 $p$
半直积群	$\mathbb{Z}/p^2\mathbb{Z} \rtimes \mathbb{Z}/p\mathbb{Z}$ · 指数为 $p^2$

p = 2

群	结构
循环群	$\mathbb{Z}/8\mathbb{Z}$
阿贝尔群	$\mathbb{Z}/4\mathbb{Z} \times \mathbb{Z}/2\mathbb{Z}$
初等阿贝尔群	$(\mathbb{Z}/2\mathbb{Z})^3$
二面体群	$D_4$（8 阶）
四元数群	$Q_8$（8 阶）

主定理为 P3Group.classification：

theorem classification (G : Type*) [Group G] [Fintype G]
    (hcard : Nat.card G = p ^ 3) : IsP3Group p G

项目结构

文件	内容
P3Group/Defs.lean	具体群模型：CyclicP3、AbelianP2P、ElementaryP3、Heisenberg、SemidirectP2P
P3Group/Structural.lean	关于 p 群的引理：中心 = $p$、模中心商 ≅ $(\mathbb{Z}/p)^2$、换位子群 = 中心、幂零类 = 2
P3Group/AbelianCase.lean	利用结构定理对 $p^3$ 阶阿贝尔群的分类
P3Group/NonAbelianCase.lean	$p^3$ 阶非阿贝尔群的分类；分为 $p=2$ 与奇素数 $p$，再按指数细分
P3Group/Classification.lean	主定理 + 五种类型两两不同构的证明

构建

lake build

环境要求：Lean 4（leanprover/lean4:v4.31.0 或之后的兼容版本）。

许可

本项目采用 Apache License 2.0 许可。