FiniteGroupAveraging.lean

1 import PaperX.RepresentationClasses
2 import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
3 import Mathlib.RingTheory.LocalRing.ResidueField.Basic
4 
5 /-! Explicit finite-group averaging lifts residual equivariant isomorphisms.
6 The order of the finite source group must be a unit. -/
7 set_option autoImplicit false
8 
9 namespace PaperX.FiniteGroupAveraging
10 open PaperX.RepresentationLimits PaperX.RepresentationClasses
11 open scoped BigOperators
12 
13 variable {R S : Type*} [CommRing R] [CommRing S]
14 variable {Γ : Type*} [Group Γ] [Fintype Γ]
15 variable {ι : Type*} [Fintype ι] [DecidableEq ι]
16 
17 /-- Reynolds averaging on the actual comparison matrix. -/
18 noncomputable def average (ρ τ : MatrixRep R Γ ι)
19     (hΓ : IsUnit (Fintype.card Γ : R)) (A : Matrix ι ι R) : Matrix ι ι R :=
20   (↑(hΓ.unit⁻¹) : R) • ∑ g : Γ, ρ g * A * τ g⁻¹
21 
22 /-- Averaging constructs an intertwiner without requiring the original matrix
23 to intertwine. -/
24 theorem average_intertwines (ρ τ : MatrixRep R Γ ι)
25     (hΓ : IsUnit (Fintype.card Γ : R)) (A : Matrix ι ι R) (h : Γ) :
26     ρ h * average ρ τ hΓ A = average ρ τ hΓ A * τ h := by
27   unfold average
28   rw [Matrix.mul_smul, Matrix.smul_mul, Finset.mul_sum, Finset.sum_mul]
29   congr 1
30   refine Fintype.sum_bijective (h * ·) (Group.mulLeft_bijective h) _ _ fun g => ?_
31   have hcancel : τ h⁻¹ * τ h = 1 := by rw [← map_mul, inv_mul_cancel, map_one]
32   simp only [mul_inv_rev, map_mul, mul_assoc, hcancel, mul_one]
33 
34 /-- If the reduction already intertwines, the average has exactly the same
35 reduction as the original matrix. -/
36 theorem map_average_of_intertwines (f : R →+* S) (ρ τ : MatrixRep R Γ ι)
37     (hΓ : IsUnit (Fintype.card Γ : R)) (A : Matrix ι ι R)
38     (hA : ∀ g, (ρ g).map f * A.map f = A.map f * (τ g).map f) :
39     (average ρ τ hΓ A).map f = A.map f := by
40   have hterm (g : Γ) : (ρ g * A * τ g⁻¹).map f = A.map f := by
41     rw [Matrix.map_mul, Matrix.map_mul, hA, mul_assoc, ← Matrix.map_mul,
42       ← map_mul, mul_inv_cancel, map_one, Matrix.map_one, mul_one] <;> simp
43   have hsum : (∑ g : Γ, ρ g * A * τ g⁻¹).map f =
44       (Fintype.card Γ : S) • A.map f := by
45     change f.mapMatrix (∑ g : Γ, ρ g * A * τ g⁻¹) = _
46     rw [map_sum]
47     simp only [RingHom.mapMatrix_apply, hterm, Finset.sum_const, Finset.card_univ]
48     exact_mod_cast (show Fintype.card Γ • A.map f = Fintype.card Γ • A.map f from rfl)
49   have hsmul (r : R) (M : Matrix ι ι R) :
50       (r • M).map f = f r • M.map f := by
51     ext i j
52     exact map_mul f r (M i j)
53   unfold average
54   rw [hsmul, hsum, smul_smul]
55   have hinv : f (↑(hΓ.unit⁻¹) : R) * (Fintype.card Γ : S) = 1 := by
56     simpa only [map_mul, hΓ.unit_spec, map_natCast, map_one] using
57       congrArg f hΓ.unit.inv_mul
58   rw [hinv, one_smul]
59 
60 omit [Fintype ι] [DecidableEq ι] in
61 /-- Entrywise surjectivity supplies a matrix lift. -/
62 theorem exists_matrix_lift (f : R →+* S) (hf : Function.Surjective f)
63     (B : Matrix ι ι S) : ∃ A : Matrix ι ι R, A.map f = B := by
64   classical
65   choose a ha using fun i j => hf (B i j)
66   exact ⟨a, by ext i j; exact ha i j⟩
67 
68 /-- A local homomorphism reflects matrix units through the determinant. -/
69 theorem matrix_isUnit_of_map (f : R →+* S) [IsLocalHom f]
70     (A : Matrix ι ι R) (hA : IsUnit (A.map f)) : IsUnit A := by
71   apply (Matrix.isUnit_iff_isUnit_det _).mpr
72   apply isUnit_of_map_unit f
73   rw [RingHom.map_det]
74   exact (Matrix.isUnit_iff_isUnit_det _).mp hA
75 
76 /-- An arbitrary residual equivariant matrix lifts to an actual integral
77 intertwiner with the same reduction. -/
78 theorem exists_intertwiner_lift (f : R →+* S) (hf : Function.Surjective f)
79     (ρ τ : MatrixRep R Γ ι) (hΓ : IsUnit (Fintype.card Γ : R))
80     (B : Matrix ι ι S)
81     (hB : ∀ g, (ρ g).map f * B = B * (τ g).map f) :
82     ∃ P : Matrix ι ι R, P.map f = B ∧ ∀ g, ρ g * P = P * τ g := by
83   obtain ⟨A, hA⟩ := exists_matrix_lift f hf B
84   refine ⟨average ρ τ hΓ A, ?_, average_intertwines ρ τ hΓ A⟩
85   rw [map_average_of_intertwines f ρ τ hΓ A (by simpa only [hA] using hB), hA]
86 
87 /-- A residual isomorphism lifts to an integral equivariant isomorphism whenever
88 the surjective coefficient map reflects units and the group order is a unit. -/
89 theorem exists_isomorphism_lift (f : R →+* S) (hf : Function.Surjective f)
90     [IsLocalHom f] (ρ τ : MatrixRep R Γ ι)
91     (hΓ : IsUnit (Fintype.card Γ : R)) (B : (Matrix ι ι S)ˣ)
92     (hB : ∀ g, (ρ g).map f * (B : Matrix ι ι S) =
93       (B : Matrix ι ι S) * (τ g).map f) :
94     ∃ P : (Matrix ι ι R)ˣ, (P : Matrix ι ι R).map f = B ∧
95       ∀ g, ρ g * (P : Matrix ι ι R) = (P : Matrix ι ι R) * τ g := by
96   obtain ⟨P, hP, hρ⟩ := exists_intertwiner_lift f hf ρ τ hΓ B hB
97   have hu : IsUnit P := matrix_isUnit_of_map f P (hP.symm ▸ B.isUnit)
98   obtain ⟨u, hu⟩ := hu
99   exact ⟨u, by simpa only [hu] using hP, by simpa only [hu] using hρ⟩
100 
101 /-- For a finite group of unit order, reduction through a surjective local
102 homomorphism preserves and reflects the integral isomorphism class. -/
103 theorem conjugacy_iff_reduction (f : R →+* S) (hf : Function.Surjective f)
104     [IsLocalHom f] (ρ τ : MatrixRep R Γ ι)
105     (hΓ : IsUnit (Fintype.card Γ : R)) :
106     Conjugate (changeCoefficients f τ) (changeCoefficients f ρ) ↔ Conjugate τ ρ := by
107   constructor
108   · rintro ⟨B, hB⟩
109     have hinter (g : Γ) : (ρ g).map f * (B : Matrix ι ι S) =
110         (B : Matrix ι ι S) * (τ g).map f := by
111       change changeCoefficients f ρ g * (B : Matrix ι ι S) =
112         (B : Matrix ι ι S) * changeCoefficients f τ g
113       rw [← hB]
114       simp only [conjugate_apply, mul_assoc, Units.inv_mul, mul_one]
115     obtain ⟨P, _, hP⟩ := exists_isomorphism_lift f hf ρ τ hΓ B hinter
116     refine ⟨P, MonoidHom.ext fun g => ?_⟩
117     change (P : Matrix ι ι R) * τ g * (↑(P⁻¹) : Matrix ι ι R) = ρ g
118     rw [← hP, mul_assoc]
119     simp
120   · exact changeCoefficients_conjugacy f
121 
122 /-- In particular, residual isomorphism over the actual residue field of a
123 local coefficient ring is equivalent to integral isomorphism. -/
124 theorem conjugacy_iff_residue [IsLocalRing R] (ρ τ : MatrixRep R Γ ι)
125     (hΓ : IsUnit (Fintype.card Γ : R)) :
126     Conjugate (changeCoefficients (IsLocalRing.residue R) τ)
127       (changeCoefficients (IsLocalRing.residue R) ρ) ↔ Conjugate τ ρ :=
128   conjugacy_iff_reduction (IsLocalRing.residue R) IsLocalRing.residue_surjective ρ τ hΓ
129 
130 /-- The lifted comparison retains any prescribed residual isomorphism, rather
131 than merely finding an unrelated change of basis. -/
132 theorem exists_residue_isomorphism_lift [IsLocalRing R]
133     (ρ τ : MatrixRep R Γ ι) (hΓ : IsUnit (Fintype.card Γ : R))
134     (B : (Matrix ι ι (IsLocalRing.ResidueField R))ˣ)
135     (hB : ∀ g, (ρ g).map (IsLocalRing.residue R) * (B : Matrix ι ι _) =
136       (B : Matrix ι ι _) * (τ g).map (IsLocalRing.residue R)) :
137     ∃ P : (Matrix ι ι R)ˣ, (P : Matrix ι ι R).map (IsLocalRing.residue R) = B ∧
138       ∀ g, ρ g * (P : Matrix ι ι R) = (P : Matrix ι ι R) * τ g :=
139   exists_isomorphism_lift (IsLocalRing.residue R) IsLocalRing.residue_surjective ρ τ hΓ B hB
140 
141 end PaperX.FiniteGroupAveraging

Back to source controls