向量空间公理蕴含加法交换律#

看到这一道练习题：

Prove that for a vector space $V$ over a field that does not have characteristic $2$ , the hypothesis that $V$ is commutative under addition is redundant.¹

虽然题目说加法交换的条件是多余的，但其实 $\mathrm{char} = 2$ 的条件也是多余的，只要满足模块定义中的四条公理，向量加法群就一定交换（考虑 $2(\mathbf v + \mathbf u)$ , 始终能展开成 $\mathbf v + \mathbf v + \mathbf u + \mathbf u$ 和 $\mathbf v + \mathbf u + \mathbf v + \mathbf u$ , 然后消去就有 $\mathbf v + \mathbf u = \mathbf u + \mathbf v$ ）.

另外，不得不吐槽用 AI 检查时坚信我们的「证明」引用加法交换律，所以认定为循环论证。

1
import Mathlib
2
import Mathlib.Algebra.Group.Defs
3
import Mathlib.Algebra.Field.Defs
4

5
variable (V F : Type) (_: AddGroup V) (_: Field F)
6

7
variable (_ : SMul F V)
8

9
variable (smul_add : ∀ (a : F) (v u : V), a • (v + u) = a • v + a • u)
10

11
variable (add_smul : ∀ (a b : F) (v : V), (a + b) • v = a • v + b • v)
12

13
variable (mul_smul : ∀ (a b : F) (v : V), (a * b) • v = a • (b • v))
14

15
variable (one_smul : ∀ (v : V), (1 : F) • v = v)
16

17
example (v u : V) : v + u = u + v := by
18
  suffices h : v + v + u + u = v + u + v + u by
19
    simpa [add_assoc] using add_right_cancel h
20

21
  have two : (2 : F) = 1 + 1 := by ring
22

23
  have h1: (2 : F) • (v + u) = v + v + u + u := by
24
    simp [two, smul_add, add_smul, one_smul, add_assoc]
25

26
  have h2: (2 : F) • (v + u) = v + u + v + u := by
27
    simp [two, add_smul, smul_add, one_smul, add_assoc]
28

29
  simp [←h1, ←h2]