CyclicInducedCharacter.lean

1 import PaperXI.CyclicInducedDegree
2 
3 /-! Exact subgroup character values of the monomial coefficients of actual induction. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace PaperXI.CyclicInduced
7 open TameDegree
8 variable {G : Type*} [Group G] (ν : G →* Multiplicative ℤ)
9 variable (φ : G) (hφ : ν φ = Multiplicative.ofAdd (1 : ℤ))
10 variable (n : ℕ) [NeZero n] (χ : degreeSubgroup ν n →* ℂˣ)
11 
12 /-- Exact unit-valued coefficient on the inducing subgroup. -/
13 theorem degreeWeight_kernel (h : degreeSubgroup ν n) (j : ZMod n) :
14     degreeWeight ν φ hφ n χ h j = degreeCharacter ν φ n χ j h :=
15   weight_kernel (degreeMod ν n) (cyclicRep φ) (cyclicRep_degree (degreeMod ν n) φ
16     (degreeMod_phi ν φ hφ n)) χ h (Multiplicative.ofAdd j)
17 
18 /-- The subgroup coefficient is literally the expected Frobenius conjugate character. -/
19 theorem degreeCharacter_apply (h : degreeSubgroup ν n) (j : ZMod n) :
20     degreeCharacter ν φ n χ j h =
21       χ ⟨φ ^ (-(j.val : ℤ)) * (h : G) * φ ^ (j.val : ℤ), by
22         change degreeMod ν n (φ ^ (-(j.val : ℤ)) * (h : G) * φ ^ (j.val : ℤ)) = 1
23         have hh : degreeMod ν n h = 1 := h.property
24         simp only [map_mul, map_inv, map_zpow, zpow_neg, hh, mul_one, inv_mul_cancel]⟩ :=
25   cyclicCharacter_apply (degreeMod ν n) φ χ j h
26 
27 /-- On residue zero, the conjugated character is the original character. -/
28 theorem degreeCharacter_zero (h : degreeSubgroup ν n) :
29     degreeCharacter ν φ n χ 0 h = χ h := by
30   rw [degreeCharacter_apply]
31   apply congrArg χ
32   apply Subtype.ext
33   simp
34 
35 /-- Exact origin coefficient, as an equality of units. -/
36 theorem degreeWeight_zero (h : degreeSubgroup ν n) :
37     degreeWeight ν φ hφ n χ h 0 = χ h := by
38   rw [degreeWeight_kernel, degreeCharacter_zero]
39 
40 variable {l : ℕ} (hdiv : n ∣ l)
41 
42 /-- Restricting to a smaller degree subgroup gives the explicitly conjugated character. -/
43 theorem degreeWeight_restrict (h : degreeSubgroup ν l) (j : ZMod n) :
44     degreeWeight ν φ hφ n χ h j =
45       χ (conjugationInto ν n l hdiv (φ ^ (-(j.val : ℤ))) h) := by
46   let h' : degreeSubgroup ν n := ⟨h, degreeSubgroup_le ν n l hdiv h.property⟩
47   change degreeWeight ν φ hφ n χ (h' : G) j = _
48   rw [degreeWeight_kernel, degreeCharacter_apply]
49   apply congrArg χ
50   apply Subtype.ext
51   simp [h', conjugationInto_apply, zpow_neg]
52 
53 /-- The zeroth tensor factor restricts without conjugation. -/
54 theorem degreeWeight_restrict_zero (h : degreeSubgroup ν l) :
55     degreeWeight ν φ hφ n χ h 0 =
56       χ ⟨h, degreeSubgroup_le ν n l hdiv h.property⟩ := by
57   let h' : degreeSubgroup ν n := ⟨h, degreeSubgroup_le ν n l hdiv h.property⟩
58   exact degreeWeight_zero ν φ hφ n χ h'
59 
60 end PaperXI.CyclicInduced

Back to source controls