ClassCompletionExamples.lean

1 import PaperX.ClassCompletion
2 import PaperX.ClassInvariants
3 import PaperX.CompletionExamples
4 
5 /-! Completion from actual conjugacy classes, instantiated over the actual
6 3-adic integers.  The finite source group is C2, not a global Galois group. -/
7 set_option autoImplicit false
8 namespace PaperX.ClassCompletionExamples
9 open PaperX.RepresentationLimits PaperX.RepresentationTopology
10 open PaperX.RepresentationClasses PaperX.ClassInvariants PaperX.ClassCompletion
11 open PaperX.CompletionExamples
12 
13 variable {R : Type} [CommRing R] (I : Ideal R)
14 
15 /-- The allowed nodes are genuine representation classes, constrained by the
16 characteristic polynomial of the actual generator action. -/
17 noncomputable def involutionClasses : ClassConditions (G := C2) (ι := Fin 2) I where
18   allowed k c := classCharpoly c generator =
19     (target (R := R)).map (Ideal.Quotient.mk (I^k))
20   downward := by
21     intro j k hjk c hc
22     change classCharpoly (changeClassCoefficients (Ideal.Quotient.factorPow I hjk) c)
23       generator = _
24     rw [classCharpoly_changeCoefficients, hc, Polynomial.map_map]
25     simp
26 
27 theorem involution_classes_nonempty (k : ℕ) :
28     ∃ c, (involutionClasses I).allowed k c := by
29   obtain ⟨ρ, hρ⟩ := involution_levels_nonempty I k
30   exact ⟨classOf ρ, hρ⟩
31 
32 theorem involution_classes_finite (hI : I.FG) [Finite (R ⧸ I)] (k : ℕ) :
33     Finite {c // (involutionClasses I).allowed k c} := by
34   let : Finite (R ⧸ I^k) := Ideal.finite_quotient_pow hI k
35   let : Finite (MatrixRep (R ⧸ I^k) C2 (Fin 2)) :=
36     Finite.of_injective (fun ρ : MatrixRep (R ⧸ I^k) C2 (Fin 2) => (ρ : C2 → _))
37       DFunLike.coe_injective
38   let : Finite (ClassRep (R ⧸ I^k) C2 (Fin 2)) :=
39     Finite.of_surjective classOf classOf_surjective
40   infer_instance
41 
42 /-- Apply the unframed completion theorem, then detect the polynomial from all
43 reductions. Continuity is actual continuity from the discrete finite group. -/
44 theorem involution_classes_realized [IsAdicComplete I R]
45     (hI : I.FG) [Finite (R ⧸ I)] :
46     ∃ ρ : MatrixRep R C2 (Fin 2),
47       (∀ k, (involutionClasses I).allowed k (classOf (reduce I ρ k))) ∧
48       AdicRepContinuous I ρ ∧ (ρ generator).charpoly = target := by
49   obtain ⟨ρ, hρ⟩ := (class_realization_iff I (involutionClasses I)
50     (finite_coefficients I hI) (fun k _ => involution_classes_finite I hI k)).mpr
51       (fun k _ => involution_classes_nonempty I k)
52   refine ⟨ρ, hρ, ?_, ?_⟩
53   · let : TopologicalSpace R := I.adicTopology
54     exact continuous_of_discreteTopology
55   · exact PaperX.CommonSpine.charpoly_detected I ρ generator target hρ
56 
57 /-- A nontrivial continuous 3-adic representation obtained from finite classes. -/
58 theorem actual_three_adic_class_completion :
59     ∃ ρ : MatrixRep ℤ_[3] C2 (Fin 2),
60       (∀ k, (involutionClasses (IsLocalRing.maximalIdeal ℤ_[3])).allowed k
61         (classOf (reduce (IsLocalRing.maximalIdeal ℤ_[3]) ρ k))) ∧
62       AdicRepContinuous (IsLocalRing.maximalIdeal ℤ_[3]) ρ ∧
63       (ρ generator).charpoly = Polynomial.X^2 - 1 ∧ ρ generator ≠ 1 := by
64   obtain ⟨ρ, hρ, hc, hp⟩ := involution_classes_realized
65     (IsLocalRing.maximalIdeal ℤ_[3]) (IsNoetherian.noetherian _)
66   exact ⟨ρ, hρ, hc, hp, nontrivial_generator ρ hp⟩
67 
68 end PaperX.ClassCompletionExamples

Back to source controls