CompletionExamples.lean

1 import PaperX.CompletionBoundary
2 import Mathlib.RingTheory.Ideal.Quotient.Index
3 
4 /-! Concrete populated representation forests. The example fixes a cyclic group
5 of order two and a characteristic polynomial, rather than defining an abstract
6 realization map as an assumption. Finite-level matrices may have multiple lifts. -/
7 set_option autoImplicit false
8 namespace PaperX.CompletionExamples
9 open scoped Matrix
10 open PaperX.RepresentationLimits PaperX.RepresentationTopology PaperX.RepresentationForests
11 abbrev C2 := Multiplicative (ZMod 2)
12 instance c2Topology : TopologicalSpace C2 := ⊥
13 instance c2Discrete : DiscreteTopology C2 := ⟨rfl⟩
14 
15 def signValue (g : C2) : ℤ := if g.toAdd = 0 then 1 else -1
16 
17 theorem sign_one : signValue 1 = 1 := by decide +kernel
18 
19 theorem sign_mul : ∀ g h : C2, signValue (g*h) = signValue g * signValue h := by
20   decide +kernel
21 
22 def signRep : MatrixRep ℤ C2 (Fin 2) where
23   toFun g := !![1,0;0,signValue g]
24   map_one' := by
25     ext i j
26     fin_cases i <;> fin_cases j <;> simp [sign_one]
27   map_mul' g h := by
28     ext i j
29     fin_cases i <;> fin_cases j <;>
30       simp [Matrix.mul_apply, Fin.sum_univ_succ, sign_mul]
31 
32 def generator : C2 := Multiplicative.ofAdd 1
33 
34 theorem integer_charpoly : (signRep generator).charpoly = Polynomial.X^2 - 1 := by
35   rw [Matrix.charpoly_fin_two]
36   norm_num [signRep, signValue, generator, Matrix.trace, Fin.sum_univ_succ, Matrix.det_fin_two]
37   ring
38 
39 variable {R : Type} [CommRing R] (I : Ideal R)
40 
41 noncomputable def target : Polynomial R := Polynomial.X^2 - 1
42 
43 /-- All actual C2 representations with the prescribed generator polynomial. -/
44 def involutionConditions : Conditions (G := C2) (ι := Fin 2) I where
45   allowed k ρ := (ρ generator).charpoly = (target (R := R)).map (Ideal.Quotient.mk (I^k))
46   downward := by
47     intro j k hjk ρ hρ
48     change ((ρ generator).map (Ideal.Quotient.factorPow I hjk)).charpoly = _
49     rw [Matrix.charpoly_map, hρ, Polynomial.map_map]
50     simp
51 
52 /-- Every precision is populated by an actual reduced sign representation. -/
53 theorem involution_levels_nonempty (k : ℕ) :
54     ∃ ρ, (involutionConditions I).allowed k ρ := by
55   refine ⟨changeCoefficients (Int.castRingHom (R ⧸ I^k)) signRep, ?_⟩
56   change ((signRep generator).map (Int.castRingHom (R ⧸ I^k))).charpoly =
57     (target (R := R)).map (Ideal.Quotient.mk (I^k))
58   rw [Matrix.charpoly_map, integer_charpoly]
59   simp [target]
60 
61 /-- Unlike arbitrary profinite source groups, this finite source makes the set
62 of all finite-matrix representations finite. -/
63 theorem involution_levels_finite (hI : I.FG) [Finite (R ⧸ I)] (k : ℕ) :
64     Finite {ρ : MatrixRep (R ⧸ I^k) C2 (Fin 2) // (involutionConditions I).allowed k ρ} := by
65   let : Finite (R ⧸ I^k) := Ideal.finite_quotient_pow hI k
66   let : Finite (MatrixRep (R ⧸ I^k) C2 (Fin 2)) :=
67     Finite.of_injective (fun ρ : MatrixRep (R ⧸ I^k) C2 (Fin 2) => (ρ : C2 → _))
68       DFunLike.coe_injective
69   infer_instance
70 
71 /-- This instantiates the representation-forest existence theorem, including
72 continuity and the recovered full characteristic polynomial. -/
73 theorem involution_forest_realized [IsAdicComplete I R] (hI : I.FG) [Finite (R ⧸ I)] :
74     ∃ ρ : MatrixRep R C2 (Fin 2),
75       Realizes I (involutionConditions I) ρ ∧ AdicRepContinuous I ρ ∧
76       (ρ generator).charpoly = target := by
77   obtain ⟨ρ,hρ,hc⟩ := exists_continuous_realization I (involutionConditions I)
78     (involution_levels_finite I hI) (involution_levels_nonempty I)
79     (fun _ τ _ i j g => by simp [nhds_discrete])
80   refine ⟨ρ,hρ,hc,?_⟩
81   exact PaperX.CommonSpine.charpoly_detected I ρ generator target hρ
82 
83 /-- Concrete actual 3-adic realization of the complete-ring hypotheses. -/
84 instance threePrime : Fact (Nat.Prime 3) := ⟨by norm_num⟩
85 instance threeResidueFinite : Finite (ℤ_[3] ⧸ IsLocalRing.maximalIdeal ℤ_[3]) :=
86   Finite.of_equiv (ZMod 3) (PadicInt.residueField (p := 3)).symm.toEquiv
87 
88 theorem actual_three_adic_forest :
89     ∃ ρ : MatrixRep ℤ_[3] C2 (Fin 2),
90       Realizes (IsLocalRing.maximalIdeal ℤ_[3])
91         (involutionConditions (IsLocalRing.maximalIdeal ℤ_[3])) ρ ∧
92       AdicRepContinuous (IsLocalRing.maximalIdeal ℤ_[3]) ρ ∧
93       (ρ generator).charpoly = Polynomial.X^2-1 := by
94   exact involution_forest_realized _ (IsNoetherian.noetherian _)
95 
96 /-- The reconstructed polynomial rules out the identity generator in char. zero. -/
97 theorem nontrivial_generator [CharZero R] (ρ : MatrixRep R C2 (Fin 2))
98     (hρ : (ρ generator).charpoly = Polynomial.X^2-1) : ρ generator ≠ 1 := by
99   intro h
100   have H := congrArg (fun p : Polynomial R => p.coeff 0) hρ
101   rw [h, Matrix.charpoly_fin_two] at H
102   norm_num at H
103 
104 end PaperX.CompletionExamples

Back to source controls