论文标题
半线性图的形式化功能分析
Formalized functional analysis with semilinear maps
论文作者
论文摘要
半线性图是向量空间之间线性图的概括，在该矢量空间之间，我们允许标量作用被环的同态（例如复杂的共轭）扭曲。特别是，这种概括统一了线性和共轭线性图的概念。我们在LEAN的\ textsf {Mathlib}库中实现了这种概括，以及功能分析中的许多重要结果，以前无法正式化正式化。具体而言，我们证明了Fréchet-riesz表示定理和光谱定理，用于在真实和复杂的Hilbert空间上，用于紧凑的自动接合算子。我们还表明，半连接地图通过形式化了Dieudonné定理和Manin定理的一维情况，其应用超出了功能分析，从而在代数封闭的字段上分类了具有积极特征的代数封闭场。
Semilinear maps are a generalization of linear maps between vector spaces where we allow the scalar action to be twisted by a ring homomorphism such as complex conjugation. In particular, this generalization unifies the concepts of linear and conjugate-linear maps. We implement this generalization in Lean's \textsf{mathlib} library, along with a number of important results in functional analysis which previously were impossible to formalize properly. Specifically, we prove the Fréchet--Riesz representation theorem and the spectral theorem for compact self-adjoint operators generically over real and complex Hilbert spaces. We also show that semilinear maps have applications beyond functional analysis by formalizing the one-dimensional case of a theorem of Dieudonné and Manin that classifies the isocrystals over an algebraically closed field with positive characteristic.
