OrderPrecision.lean

1 import PaperX.PrecisionAveraging
2 import Mathlib.RingTheory.DiscreteValuationRing.Basic
3 
4 set_option autoImplicit false
5 namespace PaperX.OrderPrecision
6 open PaperX.RepresentationLimits PaperX.RepresentationClasses
7 
8 variable {R Γ : Type*} [CommRing R] [IsDomain R]
9   [IsDiscreteValuationRing R] [Group Γ] [Fintype Γ]
10 
11 omit [Group Γ] in
12 /-- A nonzero group order has a finite uniformizer exponent.  The exponent is
13 chosen from the coefficient ring and group before any representations. -/
14 theorem exists_order_exponent (π : R) (hπ : Irreducible π)
15     (hΓ : (Fintype.card Γ : R) ≠ 0) :
16     ∃ e : ℕ, IsDiscreteValuationRing.addVal R (Fintype.card Γ : R) = e ∧
17       (Fintype.card Γ : R) ∣ π^e := by
18   obtain ⟨e, u, hu⟩ := IsDiscreteValuationRing.eq_unit_mul_pow_irreducible hΓ hπ
19   refine ⟨e, ?_, ?_⟩
20   · rw [hu, IsDiscreteValuationRing.addVal_def' u hπ]
21   · refine ⟨(↑(u⁻¹) : R), ?_⟩
22     rw [hu]
23     rw [mul_right_comm, Units.mul_inv, one_mul]
24 
25 omit [IsDomain R] [IsDiscreteValuationRing R] in
26 /-- Characteristic zero ensures that every finite group has a nonzero order
27 in the coefficient ring. -/
28 theorem order_ne_zero [CharZero R] : (Fintype.card Γ : R) ≠ 0 := by
29   exact_mod_cast Fintype.card_ne_zero (α := Γ)
30 
31 /-- One precision detects integral isomorphism in every rank.  Its value is
32 exactly one more than the valuation of the group order. -/
33 theorem uniform_detection_precision (π : R) (hπ : Irreducible π)
34     (hΓ : (Fintype.card Γ : R) ≠ 0) :
35     ∃ e : ℕ, IsDiscreteValuationRing.addVal R (Fintype.card Γ : R) = e ∧
36       ∀ (n : ℕ) (ρ τ : MatrixRep R Γ (Fin n)),
37         Conjugate (reduce (Ideal.span {π}) τ (e+1))
38           (reduce (Ideal.span {π}) ρ (e+1)) ↔ Conjugate τ ρ := by
39   obtain ⟨e, he, hdiv⟩ := exists_order_exponent π hπ hΓ
40   exact ⟨e, he, fun _ ρ τ => PrecisionAveraging.conjugacy_iff_reduction
41     π e 1 ρ τ hΓ hdiv hπ.not_isUnit (by decide)⟩
42 
43 section Classes
44 variable {ι : Type*} [Fintype ι] [DecidableEq ι]
45 
46 /-- Reduction at the group-order precision is injective on actual integral
47 isomorphism classes.  Surjectivity onto arbitrary quotient representations is
48 not asserted. -/
49 theorem reduceClass_injective (π : R) (hπ : Irreducible π) (e : ℕ)
50     (hΓ : (Fintype.card Γ : R) ≠ 0) (hdiv : (Fintype.card Γ : R) ∣ π^e) :
51     Function.Injective (fun c : ClassRep R Γ ι => reduceClass (Ideal.span {π}) c (e+1)) := by
52   intro x y h
53   obtain ⟨τ, rfl⟩ := classOf_surjective x
54   obtain ⟨ρ, rfl⟩ := classOf_surjective y
55   apply classOf_eq.mpr
56   exact (PrecisionAveraging.conjugacy_iff_reduction π e 1 ρ τ hΓ hdiv
57     hπ.not_isUnit (by decide)).mp (classOf_eq.mp h)
58 
59 omit [IsDomain R] [IsDiscreteValuationRing R] in
60 /-- Finite coefficients and a finite source yield finitely many actual
61 representation classes at that coefficient level. -/
62 theorem finite_classes_of_finite_coefficients [Finite R] : Finite (ClassRep R Γ ι) := by
63   let : Finite (MatrixRep R Γ ι) := Finite.of_injective
64     (fun ρ : MatrixRep R Γ ι => (ρ : Γ → Matrix ι ι R))
65     (fun _ _ h => MonoidHom.ext (congrFun h))
66   exact Finite.of_surjective classOf classOf_surjective
67 
68 /-- For a fixed finite group and rank, finite coefficient quotients imply
69 finitely many integral isomorphism classes.  Completeness is unnecessary. -/
70 theorem finite_integral_classes (π : R) (hπ : Irreducible π)
71     (hΓ : (Fintype.card Γ : R) ≠ 0)
72     (finiteR : ∀ k, Finite (R ⧸ (Ideal.span {π})^k)) :
73     Finite (ClassRep R Γ ι) := by
74   obtain ⟨e, _, hdiv⟩ := exists_order_exponent π hπ hΓ
75   let : Finite (R ⧸ (Ideal.span {π})^(e+1)) := finiteR (e+1)
76   let : Finite (ClassRep (R ⧸ (Ideal.span {π})^(e+1)) Γ ι) :=
77     finite_classes_of_finite_coefficients
78   exact Finite.of_injective _ (reduceClass_injective π hπ e hΓ hdiv)
79 
80 end Classes
81 end PaperX.OrderPrecision

Back to source controls