Mathlib4中CompleteBooleanAlgebra类的简化与Galois连接应用

引言

在Lean4的数学库Mathlib4中，CompleteBooleanAlgebra类结合了完全格和布尔代数的特性。近期社区发现该类中的两个假设条件inf_sSup_le_iSup_inf和iInf_sup_le_sup_sInf实际上是冗余的，可以通过更基础的代数性质推导得出。

CompleteBooleanAlgebra的原始定义

CompleteBooleanAlgebra类原本继承了CompleteLattice和BooleanAlgebra，并额外添加了两个假设条件：

1. inf_sSup_le_iSup_inf：对于任意元素a和集合s，a与s的上确界的交小于等于a与s中各元素交的并
2. iInf_sup_le_sup_sInf：对于任意元素a和集合s，a与s中各元素并的交小于等于a与s下确界的并

冗余条件的证明

通过深入分析，我们发现这两个条件实际上是布尔代数中更基础性质的推论，不需要作为独立的假设存在。

使用Galois连接的证明

数学库中已经存在关于Galois连接的工具，可以简洁地证明这些性质：

lemma inf_sSup_le_iSup_inf (a : α) (s : Set α) : a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b :=
  gc_inf_himp.l_sSup.le

这个证明利用了布尔代数中交运算(⊓)与蕴含运算(→)形成的Galois连接。类似地，对偶性质也可以通过Galois连接证明：

lemma iInf_sup_le_sup_sInf (a : α) (s : Set α) : ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s :=
  gc_sdiff_sup.u_sInf.ge

初等证明方法

对于不熟悉Galois连接的用户，也可以通过初等方法证明这些性质。以inf_sSup_le_iSup_inf为例：

1. 首先将sSup表示为iSup
2. 利用布尔代数中的分解性质：b = (b ⊓ a) ⊔ (b ⊓ aᶜ)
3. 通过不等式放缩和重排完成证明

这种证明虽然更长，但更直观地展示了布尔代数性质如何导致这些不等式成立。

理论背景与推广

这些结果实际上反映了更一般的数学原理：

1. 在布尔代数中，交运算(⊓)作为左伴随函子保持上确界
2. 并运算(⊔)作为右伴随函子保留下确界
3. 这种性质不仅限于布尔代数，在更一般的Heyting代数和co-Heyting代数中也存在类似结果

对Mathlib4的影响

这一发现将带来以下改进：

1. 简化CompleteBooleanAlgebra类的定义，移除冗余假设
2. 减少证明实例时需要验证的条件
3. 更清晰地展示布尔代数与格论之间的内在联系
4. 为未来可能的推广奠定更坚实的理论基础

结语

这一工作展示了数学形式化过程中理论简化的价值，也体现了Galois连接这一抽象工具的强大威力。通过深入理解数学结构的内在联系，我们可以构建更简洁、更通用的数学库，为后续的数学形式化工作提供更好的基础。