QuadraticAlgebra.lean

1 import Mathlib.RingTheory.AdjoinRoot
2 
3 /-! The actual quadratic coordinate ring and its points, over arbitrary
4 commutative rings, including characteristic two and the zero ring. -/
5 set_option autoImplicit false
6 noncomputable section
7 
8 namespace PaperX.QuadraticAlgebra
9 
10 variable (B : Type*) [CommRing B]
11 
12 /-- Solutions of the defining quadratic equation. -/
13 abbrev Root := {x : B // x ^ 2 = 1}
14 
15 variable {B} {C : Type*} [CommRing C] {D : Type*} [CommRing D]
16 
17 /-- Coefficient change on actual roots. -/
18 def mapRoot (f : B →+* C) (x : Root B) : Root C :=
19   ⟨f x.val, by simpa only [map_pow, map_one] using congrArg f x.property⟩
20 
21 @[simp] theorem mapRoot_val (f : B →+* C) (x : Root B) :
22     (mapRoot f x).val = f x.val := rfl
23 
24 @[simp] theorem mapRoot_id (x : Root B) : mapRoot (RingHom.id B) x = x := rfl
25 
26 @[simp] theorem mapRoot_comp (f : B →+* C) (g : C →+* D) (x : Root B) :
27     mapRoot (g.comp f) x = mapRoot g (mapRoot f x) := rfl
28 
29 variable (R : Type*) [CommRing R]
30 
31 def equation : Polynomial R := Polynomial.X ^ 2 - 1
32 
33 /-- This is literally the polynomial quotient by the ideal generated by
34 `X^2 - 1`, using Mathlib's `AdjoinRoot` construction. -/
35 abbrev CoordinateRing := AdjoinRoot (equation R)
36 
37 def coordinate : CoordinateRing R := AdjoinRoot.root (equation R)
38 
39 theorem coordinate_sq : coordinate R ^ 2 = 1 := by
40   have h := AdjoinRoot.eval₂_root (equation R)
41   change (Polynomial.X ^ 2 - (1 : Polynomial R)).eval₂ _ (coordinate R) = 0 at h
42   rw [Polynomial.eval₂_sub, Polynomial.eval₂_pow, Polynomial.eval₂_X,
43     Polynomial.eval₂_one] at h
44   exact sub_eq_zero.mp h
45 
46 variable [Algebra R B]
47 
48 /-- A genuine algebra point gives a solution by evaluating the coordinate. -/
49 def pointRoot (f : CoordinateRing R →ₐ[R] B) : Root B :=
50   ⟨f (coordinate R), by simpa only [map_pow, map_one] using congrArg f (coordinate_sq R)⟩
51 
52 /-- The quotient universal property realizes each quadratic root as a point. -/
53 def rootPoint (x : Root B) : CoordinateRing R →ₐ[R] B :=
54   AdjoinRoot.liftAlgHom (equation R) (Algebra.ofId R B) x.val (by
55     simp [equation, x.property])
56 
57 @[simp] theorem rootPoint_coordinate (x : Root B) :
58     rootPoint R x (coordinate R) = x.val := by
59   simp [rootPoint, coordinate]
60 
61 /-- The complete functor-of-points statement, without a separability assumption. -/
62 def pointEquiv : (CoordinateRing R →ₐ[R] B) ≃ Root B where
63   toFun := pointRoot R
64   invFun := rootPoint R
65   left_inv f := by
66     apply AdjoinRoot.algHom_ext
67     exact rootPoint_coordinate R (pointRoot R f)
68   right_inv x := by
69     apply Subtype.ext
70     exact rootPoint_coordinate R x
71 
72 @[simp] theorem pointEquiv_val (f : CoordinateRing R →ₐ[R] B) :
73     (pointEquiv R f).val = f (coordinate R) := rfl
74 
75 variable [Algebra R C]
76 
77 /-- Specializing a point and specializing its root commute exactly. -/
78 theorem pointEquiv_natural (f : B →ₐ[R] C) (p : CoordinateRing R →ₐ[R] B) :
79     pointEquiv R (f.comp p) = mapRoot f.toRingHom (pointEquiv R p) := rfl
80 
81 theorem rootPoint_natural (f : B →ₐ[R] C) (x : Root B) :
82     f.comp (rootPoint R x) = rootPoint R (mapRoot f.toRingHom x) := by
83   apply AdjoinRoot.algHom_ext
84   simp [rootPoint]
85 
86 end PaperX.QuadraticAlgebra

Back to source controls