ProjectiveExample.lean

1 import Mathlib.Data.ZMod.Basic
2 import Mathlib.Tactic.Ring
3 import Mathlib.Tactic.NormNum
4 
5 set_option autoImplicit false
6 
7 /-!
8 # A nontrivial cocycle model
9 
10 For G = (Z/2Z)^2, c(x,y) = x₂ y₁ is an additive Z/2Z-valued 2-cocycle.
11 It cannot be a scalar coboundary: scalar coboundaries on an abelian group are
12 symmetric, while this cocycle is not. This is a finite exact obstruction model,
13 not a theorem identifying any Galois group or proving Langlands descent.
14 -/
15 namespace KomorebiSpace
16 namespace ProjectiveExample
17 abbrev G := (ZMod 2) × (ZMod 2)
18 
19 def phase (x y : G) : ZMod 2 := x.2 * y.1
20 
21 @[simp] theorem phase_zero_left (y : G) : phase 0 y = 0 := by simp [phase]
22 @[simp] theorem phase_zero_right (x : G) : phase x 0 = 0 := by simp [phase]
23 
24 theorem cocycle (x y z : G) :
25     phase x y + phase (x+y) z = phase y z + phase x (y+z) := by
26   simp only [phase, Prod.fst_add, Prod.snd_add]
27   ring
28 
29 def coboundary (a : G → ZMod 2) (x y : G) : ZMod 2 := a x + a y - a (x+y)
30 
31 theorem coboundary_symmetric (a : G → ZMod 2) (x y : G) :
32     coboundary a x y = coboundary a y x := by
33   unfold coboundary
34   rw [add_comm x y, add_comm (a x) (a y)]
35 
36 theorem phase_asymmetric : phase (1,0) (0,1) ≠ phase (0,1) (1,0) := by
37   norm_num [phase]
38 
39 theorem no_scalar_flattening : ¬ ∃ a : G → ZMod 2, ∀ x y, phase x y = coboundary a x y := by
40   rintro ⟨a, ha⟩
41   apply phase_asymmetric
42   rw [ha, ha, coboundary_symmetric]
43 end ProjectiveExample
44 end KomorebiSpace

Back to source controls