CyclicInducedDegree.lean

1 import PaperXI.CyclicInducedBasis
2 import PaperXI.TameDegree
3 
4 /-! Source-facing degree-subgroup coordinates for tame cyclic induction. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.CyclicInduced
8 open TameDegree
9 variable {G : Type*} [Group G] (ν : G →* Multiplicative ℤ)
10 variable (φ : G) (hφ : ν φ = Multiplicative.ofAdd (1 : ℤ))
11 variable (n : ℕ) [NeZero n]
12 
13 include hφ in
14 omit [NeZero n] in
15 theorem degreeMod_phi : degreeMod ν n φ = Multiplicative.ofAdd (1 : ZMod n) := by
16   simpa using degreeMod_phi_zpow ν φ hφ n (1 : ℤ)
17 
18 variable (χ : degreeSubgroup ν n →* ℂˣ)
19 /-- The source's induced representation, using the actual degree-divisibility subgroup. -/
20 abbrev degreeInduced := induced (degreeMod ν n) χ
21 abbrev DegreeIndSpace := IndSpace (degreeMod ν n) χ
22 
23 /-- Frobenius coordinates of the actual induced representation. -/
24 def degreeBasis : Module.Basis (ZMod n) ℂ (DegreeIndSpace ν n χ) :=
25   cyclicBasis (degreeMod ν n) φ (degreeMod_phi ν φ hφ n) χ
26 
27 def degreeWeight (g : G) (j : ZMod n) : ℂˣ :=
28   cyclicWeight (degreeMod ν n) φ (degreeMod_phi ν φ hφ n) χ g j
29 
30 /-- Frobenius conjugate of the source character on a basis line. -/
31 def degreeCharacter (j : ZMod n) : degreeSubgroup ν n →* ℂˣ :=
32   cyclicCharacter (degreeMod ν n) φ χ j
33 
34 /-- Translation by degree is the index action on the genuine induced basis. -/
35 theorem degreeBasis_action (g : G) (j : ZMod n) :
36     degreeInduced ν n χ g (degreeBasis ν φ hφ n χ j) =
37       (degreeWeight ν φ hφ n χ g j : ℂ) •
38       degreeBasis ν φ hφ n χ (translationAction ν n g j) :=
39   cyclicBasis_action (degreeMod ν n) φ (degreeMod_phi ν φ hφ n) χ g j
40 
41 /-- Kernel elements act by the explicit conjugated character. -/
42 theorem degreeBasis_action_kernel (h : degreeSubgroup ν n) (j : ZMod n) :
43     degreeInduced ν n χ h (degreeBasis ν φ hφ n χ j) =
44       (degreeCharacter ν φ n χ j h : ℂ) • degreeBasis ν φ hφ n χ j :=
45   cyclicBasis_action_kernel (degreeMod ν n) φ (degreeMod_phi ν φ hφ n) χ h j
46 
47 /-- On the zeroth basis line the character is precisely the inducing character. -/
48 theorem degreeBasis_action_zero (h : degreeSubgroup ν n) :
49     degreeInduced ν n χ h (degreeBasis ν φ hφ n χ 0) =
50       (χ h : ℂ) • degreeBasis ν φ hφ n χ 0 :=
51   cyclicBasis_action_zero (degreeMod ν n) φ (degreeMod_phi ν φ hφ n) χ h
52 
53 /-- Frobenius advances the cyclic basis, including its actual wrap scalar. -/
54 theorem degreeBasis_action_phi (j : ZMod n) :
55     degreeInduced ν n χ φ (degreeBasis ν φ hφ n χ j) =
56       (degreeWeight ν φ hφ n χ φ j : ℂ) • degreeBasis ν φ hφ n χ (j + 1) :=
57   cyclicBasis_action_phi (degreeMod ν n) φ (degreeMod_phi ν φ hφ n) χ j
58 
59 end PaperXI.CyclicInduced

Back to source controls