DeterminantSpine.lean

1 import PaperX.ClassCompletion
2 import PaperX.ClassInvariants
3 import PaperX.CommonSpine
4 
5 /-! The determinant part of a prescribed common spine is an actual invariant
6 of matrix representation classes. Equality at every coefficient precision
7 recovers its integral value; coefficient change then recovers a separately
8 specified common value in the local coefficient field. No arithmetic
9 interpretation of the other local packet entries is asserted here. -/
10 set_option autoImplicit false
11 namespace PaperX.DeterminantSpine
12 open PaperX.RepresentationLimits PaperX.RepresentationClasses
13 open PaperX.ClassCompletion PaperX.ClassInvariants
14 
15 variable {R : Type*} [CommRing R] {G : Type*} [Group G]
16   {ι : Type*} [Fintype ι] [DecidableEq ι]
17 
18 /-- The actual determinant character, including multiplicativity. -/
19 def determinantCharacter (ρ : MatrixRep R G ι) : G →* R :=
20   Matrix.detMonoidHom.comp ρ
21 
22 @[simp] theorem determinantCharacter_apply (ρ : MatrixRep R G ι) (g : G) :
23     determinantCharacter ρ g = (ρ g).det := rfl
24 
25 theorem determinant_conjugacy {ρ σ : MatrixRep R G ι}
26     (h : Conjugate ρ σ) (g : G) : (ρ g).det = (σ g).det := by
27   obtain ⟨u, hu⟩ := h
28   rw [← hu, det_conjugate]
29 
30 /-- Determinant evaluated on the actual quotient by matrix conjugacy. -/
31 noncomputable def classDet (c : ClassRep R G ι) (g : G) : R :=
32   Quotient.lift (fun ρ : MatrixRep R G ι => (ρ g).det)
33     (fun _ _ h => determinant_conjugacy h g) c
34 
35 @[simp] theorem classDet_classOf (ρ : MatrixRep R G ι) (g : G) :
36     classDet (classOf ρ) g = (ρ g).det := rfl
37 
38 theorem determinant_changeCoefficients {S : Type*} [CommRing S]
39     (f : R →+* S) (ρ : MatrixRep R G ι) (g : G) :
40     (changeCoefficients f ρ g).det = f ((ρ g).det) := by
41   exact (f.map_det (ρ g)).symm
42 
43 theorem classDet_changeCoefficients {S : Type*} [CommRing S]
44     (f : R →+* S) (c : ClassRep R G ι) (g : G) :
45     classDet (changeClassCoefficients f c) g = f (classDet c g) := by
46   obtain ⟨ρ, rfl⟩ := classOf_surjective c
47   exact determinant_changeCoefficients f ρ g
48 
49 /-- Separatedness suffices to recover the entire prescribed determinant. -/
50 theorem determinant_detected (I : Ideal R) [IsHausdorff I R]
51     (ρ : MatrixRep R G ι) (g : G) (d : R)
52     (h : ∀ k, (reduce I ρ k g).det = Ideal.Quotient.mk (I^k) d) :
53     (ρ g).det = d := by
54   apply scalar_ext I
55   intro k
56   exact (determinant_changeCoefficients (Ideal.Quotient.mk (I^k)) ρ g).symm.trans (h k)
57 
58 /-- Prescribing determinant values on every allowed conjugacy class makes
59 those values hold for every integral realization of those classes. -/
60 theorem class_realization_has_determinant {R G ι : Type}
61     [CommRing R] [Group G] [Fintype ι] [DecidableEq ι]
62     (I : Ideal R) [IsHausdorff I R]
63     (C : ClassConditions (G := G) (ι := ι) I)
64     (ρ : MatrixRep R G ι)
65     (hρ : ∀ k, C.allowed k (classOf (reduce I ρ k)))
66     (δ : G → R)
67     (spec : ∀ k c, C.allowed k c → ∀ g,
68       classDet c g = Ideal.Quotient.mk (I^k) (δ g)) :
69     ∀ g, (ρ g).det = δ g := by
70   intro g
71   apply determinant_detected I ρ g (δ g)
72   intro k
73   exact spec k _ (hρ k) g
74 
75 /-- Local integral and common coefficient values are compared only after
76 embedding both into the local coefficient ring. -/
77 theorem determinant_base_change {K E : Type*} [CommRing K] [CommRing E]
78     (inc : R →+* K) (emb : E →+* K) (ρ : MatrixRep R G ι) (g : G)
79     (localδ : R) (commonδ : E)
80     (hlocal : (ρ g).det = localδ) (hcommon : inc localδ = emb commonδ) :
81     (changeCoefficients inc ρ g).det = emb commonδ := by
82   rw [determinant_changeCoefficients, hlocal, hcommon]
83 
84 /-- The determinant entry of a common spine follows from its finite class
85 specification and its integral coefficient comparison. -/
86 theorem class_realization_has_common_determinant {R G ι K E : Type}
87     [CommRing R] [Group G] [Fintype ι] [DecidableEq ι]
88     [CommRing K] [CommRing E]
89     (I : Ideal R) [IsHausdorff I R]
90     (C : ClassConditions (G := G) (ι := ι) I)
91     (ρ : MatrixRep R G ι)
92     (hρ : ∀ k, C.allowed k (classOf (reduce I ρ k)))
93     (inc : R →+* K) (emb : E →+* K)
94     (localδ : G → R) (commonδ : G → E)
95     (integrality : ∀ g, inc (localδ g) = emb (commonδ g))
96     (spec : ∀ k c, C.allowed k c → ∀ g,
97       classDet c g = Ideal.Quotient.mk (I^k) (localδ g)) :
98     ∀ g, (changeCoefficients inc ρ g).det = emb (commonδ g) := by
99   intro g
100   exact determinant_base_change inc emb ρ g (localδ g) (commonδ g)
101     (class_realization_has_determinant I C ρ hρ localδ spec g) (integrality g)
102 
103 end PaperX.DeterminantSpine

Back to source controls