MonomialInduction.lean

1 import PaperXI.LineCharacter
2 import Mathlib.RepresentationTheory.Induced
3 
4 /-! Actual induction from the stabilizer of a nonzero monomial basis line. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.MonomialInduction
8 open Representation Module
9 variable {G V : Type*} [Group G] [AddCommGroup V] [Module ℂ V]
10 
11 /-- The one dimensional representation belonging to a scalar character. -/
12 def scalarRepresentation {H : Type*} [Group H] (χ : H →* ℂˣ) : Representation ℂ H ℂ where
13   toFun h := (χ h : ℂ) • LinearMap.id
14   map_one' := by ext; simp
15   map_mul' h k := by ext; simp [smul_smul, mul_comm]
16 
17 @[simp] theorem scalarRepresentation_apply {H : Type*} [Group H] (χ : H →* ℂˣ)
18     (h : H) (a : ℂ) : scalarRepresentation χ h a = (χ h : ℂ) * a := rfl
19 
20 variable (ρ : Representation ℂ G V) (v : V) (hv : v ≠ 0)
21 
22 abbrev stabilizer := LineCharacter.lineStabilizer ρ v
23 abbrev character := LineCharacter.character ρ v hv
24 abbrev lineRepresentation := scalarRepresentation (character ρ v hv)
25 abbrev induced := Representation.ind (stabilizer ρ v).subtype (lineRepresentation ρ v hv)
26 abbrev InducedSpace := Representation.IndV (stabilizer ρ v).subtype (lineRepresentation ρ v hv)
27 
28 /-- Inclusion of the character line into the restricted representation. -/
29 def lineMap : Representation.IntertwiningMap (lineRepresentation ρ v hv)
30     (ρ.comp (stabilizer ρ v).subtype) :=
31   ⟨LinearMap.toSpanSingleton ℂ V v, by
32     intro h
33     apply LinearMap.ext
34     intro a
35     change ((character ρ v hv h : ℂ) * a) • v = ρ (h : G) (a • v)
36     rw [map_smul, LineCharacter.character_action ρ v hv h]
37     simp [smul_smul, mul_comm]⟩
38 
39 /-- The universal induced map is evaluated in the original representation. -/
40 def evaluation : Representation.IntertwiningMap (induced ρ v hv) ρ :=
41   ⟨Representation.Coinvariants.lift _
42     (TensorProduct.lift <| (Finsupp.lift _ _ _ fun h : G =>
43       ρ h⁻¹ ∘ₗ (lineMap ρ v hv).toLinearMap) ∘ₗ
44       (MonoidAlgebra.coeffLinearEquiv ℂ).toLinearMap)
45     (fun g => by
46       ext h
47       simp only [LinearMap.coe_comp, Function.comp_apply, MonoidAlgebra.lsingle_apply]
48       simp [Representation.ofMulAction_single, mul_inv_rev,
49         -scalarRepresentation_apply, (lineMap ρ v hv).isIntertwining]),
50     fun g => by ext; simp⟩
51 
52 @[simp] theorem evaluation_mk (g : G) (a : ℂ) :
53     evaluation ρ v hv (IndV.mk (stabilizer ρ v).subtype (lineRepresentation ρ v hv) g a) =
54       a • ρ g⁻¹ v := by
55   simp [evaluation, lineMap, map_smul]
56 
57 /-- The actual quotient relation for a stabilizer scalar. -/
58 theorem mk_stabilizer (h : stabilizer ρ v) (g : G) (a : ℂ) :
59     IndV.mk (stabilizer ρ v).subtype (lineRepresentation ρ v hv)
60       ((h : G)⁻¹ * g) a =
61     IndV.mk (stabilizer ρ v).subtype (lineRepresentation ρ v hv)
62       g ((character ρ v hv h : ℂ) * a) := by
63   have hh := Coinvariants.mk_inv_tmul
64     ((Representation.leftRegular ℂ G).comp (stabilizer ρ v).subtype)
65     (lineRepresentation ρ v hv) (MonoidAlgebra.single g 1) a h
66   simpa using hh
67 
68 variable {X : Type*} (b : Basis X ℂ V) (r : X → G) (a : X → ℂˣ)
69 
70 /-- An explicit inverse, using the given basis and actual orbit representatives. -/
71 def reconstruction : V →ₗ[ℂ] InducedSpace ρ v hv :=
72   b.constr ℂ fun i => (a i : ℂ)⁻¹ •
73     IndV.mk (stabilizer ρ v).subtype (lineRepresentation ρ v hv) (r i)⁻¹ 1
74 
75 @[simp] theorem reconstruction_basis (i : X) :
76     reconstruction ρ v hv b r a (b i) = (a i : ℂ)⁻¹ •
77       IndV.mk (stabilizer ρ v).subtype (lineRepresentation ρ v hv) (r i)⁻¹ 1 :=
78   b.constr_basis ℂ _ i
79 
80 variable (hr : ∀ i, ρ (r i) v = (a i : ℂ) • b i)
81 
82 include hr in
83 theorem evaluation_reconstruction :
84     (evaluation ρ v hv).toLinearMap ∘ₗ reconstruction ρ v hv b r a = LinearMap.id := by
85   apply b.ext
86   intro i
87   change evaluation ρ v hv (reconstruction ρ v hv b r a (b i)) = b i
88   rw [reconstruction_basis, map_smul, evaluation_mk]
89   simp [hr, smul_smul]
90 
91 include hr in
92 theorem representative_inverse (i : X) : ρ (r i)⁻¹ (b i) = (a i : ℂ)⁻¹ • v := by
93   apply (ρ.apply_bijective (r i)).injective
94   simp [hr, smul_smul]
95 
96 /- Any group translate of the distinguished vector remains in one basis line. -/
97 variable (hmono : ∀ g : G, ∃ i : X, ∃ d : ℂˣ, ρ g v = (d : ℂ) • b i)
98 
99 include hr hmono in
100 theorem reconstruction_evaluation :
101     reconstruction ρ v hv b r a ∘ₗ (evaluation ρ v hv).toLinearMap = LinearMap.id := by
102   apply IndV.hom_ext
103   intro g
104   apply LinearMap.ext_ring
105   obtain ⟨i, d, hd⟩ := hmono g⁻¹
106   have hk : (r i)⁻¹ * g⁻¹ ∈ stabilizer ρ v := by
107     refine ⟨(d : ℂ) * (a i : ℂ)⁻¹, ?_⟩
108     simp [map_mul, Module.End.mul_apply, hd,
109       representative_inverse ρ v b r a hr i, smul_smul]
110   let k : stabilizer ρ v := ⟨(r i)⁻¹ * g⁻¹, hk⟩
111   have hc : (character ρ v hv k : ℂ) = (d : ℂ) * (a i : ℂ)⁻¹ := by
112     apply LineCharacter.scalar_unique hv
113     rw [← LineCharacter.character_action]
114     change ρ ((r i)⁻¹ * g⁻¹) v = _
115     simp [map_mul, Module.End.mul_apply, hd,
116       representative_inverse ρ v b r a hr i, smul_smul]
117   have hm := mk_stabilizer ρ v hv k (r i)⁻¹ 1
118   have hm' : IndV.mk (stabilizer ρ v).subtype (lineRepresentation ρ v hv) g 1 =
119       ((d : ℂ) * (a i : ℂ)⁻¹) •
120         IndV.mk (stabilizer ρ v).subtype (lineRepresentation ρ v hv) (r i)⁻¹ 1 := by
121     have hh : ((k : G)⁻¹ * (r i)⁻¹) = g := by simp [k, mul_assoc]
122     rw [hh, hc, mul_one] at hm
123     calc
124       _ = IndV.mk (stabilizer ρ v).subtype (lineRepresentation ρ v hv)
125         (r i)⁻¹ ((d : ℂ) * (a i : ℂ)⁻¹) := hm
126       _ = _ := by rw [← map_smul]; simp only [smul_eq_mul, mul_one]
127   change reconstruction ρ v hv b r a
128       (evaluation ρ v hv (IndV.mk (stabilizer ρ v).subtype (lineRepresentation ρ v hv) g 1)) = _
129   rw [evaluation_mk, one_smul, hd, map_smul, reconstruction_basis, smul_smul]
130   exact hm'.symm
131 
132 include hr hmono in
133 theorem evaluation_bijective : Function.Bijective (evaluation ρ v hv) := by
134   constructor
135   · exact Function.HasLeftInverse.injective
136       ⟨reconstruction ρ v hv b r a, fun x =>
137         LinearMap.congr_fun (reconstruction_evaluation ρ v hv b r a hr hmono) x⟩
138   · exact Function.HasRightInverse.surjective
139       ⟨reconstruction ρ v hv b r a, fun x =>
140         LinearMap.congr_fun (evaluation_reconstruction ρ v hv b r a hr) x⟩
141 
142 /-- A transitive monomial basis identifies the original representation with the
143 actual Mathlib induction of the scalar character on its line stabilizer. -/
144 def equivalence : Representation.Equiv (induced ρ v hv) ρ :=
145   (evaluation ρ v hv).ofBijective (evaluation_bijective ρ v hv b r a hr hmono)
146 
147 @[simp] theorem equivalence_mk (g : G) (z : ℂ) :
148     equivalence ρ v hv b r a hr hmono
149       (IndV.mk (stabilizer ρ v).subtype (lineRepresentation ρ v hv) g z) =
150       z • ρ g⁻¹ v := evaluation_mk ρ v hv g z
151 
152 end PaperXI.MonomialInduction

Back to source controls