QuadraticCharacters.lean

1 import PaperX.QuadraticAlgebra
2 import PaperX.CompletionExamples
3 
4 /-! Quadratic coordinate points are exactly unit-valued characters of the
5 actual cyclic group `Multiplicative (ZMod 2)`. -/
6 set_option autoImplicit false
7 noncomputable section
8 
9 namespace PaperX.QuadraticCharacters
10 open PaperX.QuadraticAlgebra PaperX.CompletionExamples
11 
12 theorem generator_sq : generator ^ 2 = 1 := by decide +kernel
13 
14 theorem generator_ne_one : generator ≠ 1 := by decide +kernel
15 
16 theorem c2_cases (g : C2) : g = 1 ∨ g = generator := by
17   revert g
18   decide +kernel
19 
20 variable {B : Type*} [CommRing B]
21 
22 /-- A quadratic root is a unit, with itself as its inverse. -/
23 def rootUnit (x : Root B) : Bˣ where
24   val := x.val
25   inv := x.val
26   val_inv := by simpa only [pow_two] using x.property
27   inv_val := by simpa only [pow_two] using x.property
28 
29 @[simp] theorem rootUnit_val (x : Root B) : (rootUnit x : B) = x.val := rfl
30 
31 theorem rootUnit_sq (x : Root B) : rootUnit x * rootUnit x = 1 := by
32   apply Units.ext
33   exact (pow_two x.val).symm.trans x.property
34 
35 /-- The character associated with an actual root of `X^2 - 1`. -/
36 def ofRoot (x : Root B) : C2 →* Bˣ where
37   toFun g := if g = 1 then 1 else rootUnit x
38   map_one' := by simp
39   map_mul' g h := by
40     rcases c2_cases g with rfl | rfl <;> rcases c2_cases h with rfl | rfl
41     · simp
42     · simp
43     · simp
44     · have hg : generator * generator = 1 := by simpa only [pow_two] using generator_sq
45       simp [hg, generator_ne_one, rootUnit_sq]
46 
47 @[simp] theorem ofRoot_generator (x : Root B) :
48     (ofRoot x generator : B) = x.val := by
49   simp [ofRoot, generator_ne_one]
50 
51 theorem ofRoot_apply_val (x : Root B) (g : C2) :
52     (ofRoot x g : B) = if g = 1 then 1 else x.val := by
53   split_ifs with h <;> simp [ofRoot, h]
54 
55 /-- Evaluating any C2 character produces a root of the coordinate equation. -/
56 def toRoot (χ : C2 →* Bˣ) : Root B :=
57   ⟨(χ generator : B), by
58     have h : χ generator ^ 2 = 1 := by rw [← map_pow, generator_sq, map_one]
59     simpa only [Units.val_pow_eq_pow_val, Units.val_one] using
60       congrArg (fun u : Bˣ => (u : B)) h⟩
61 
62 /-- Evaluation at the specified generator determines a character. -/
63 theorem character_ext {χ ψ : C2 →* Bˣ}
64     (h : (χ generator : B) = (ψ generator : B)) : χ = ψ := by
65   apply MonoidHom.ext
66   intro g
67   rcases c2_cases g with rfl | rfl
68   · simp
69   · exact Units.ext h
70 
71 /-- No nontriviality, reducedness, or invertibility-of-two assumption is used. -/
72 def characterEquiv : Root B ≃ (C2 →* Bˣ) where
73   toFun := ofRoot
74   invFun := toRoot
75   left_inv x := by
76     apply Subtype.ext
77     exact ofRoot_generator x
78   right_inv χ := by
79     apply character_ext
80     exact ofRoot_generator (toRoot χ)
81 
82 variable {C : Type*} [CommRing C]
83 
84 /-- Reduction of roots agrees with reduction of the associated characters. -/
85 theorem map_ofRoot (f : B →+* C) (x : Root B) :
86     (Units.map f.toMonoidHom).comp (ofRoot x) = ofRoot (mapRoot f x) := by
87   apply character_ext
88   simp
89 
90 variable (R : Type*) [CommRing R] [Algebra R B]
91 
92 /-- The full quotient-ring-point to finite-group-character equivalence. -/
93 def pointCharacterEquiv : (CoordinateRing R →ₐ[R] B) ≃ (C2 →* Bˣ) :=
94   (pointEquiv R).trans characterEquiv
95 
96 end PaperX.QuadraticCharacters

Back to source controls