import Definitions.Def_LanglandsTunnell_CubicInduction_PrincipalSeries3 set_option autoImplicit false open Matrix IsDedekindDomain NumberField NumberField.AdelicLevel LanglandsTunnell.TateLocal noncomputable section namespace LanglandsTunnell.CubicInduction section PrincipalSeries2 variable (v : HeightOneSpectrum (π“ž β„š)) abbrev LocalGL2 : Type := GL (Fin 2) (v.adicCompletion β„š) def rightTranslate2 (g : LocalGL2 v) : Module.End β„‚ (LocalGL2 v β†’ β„‚) where toFun f := fun h => f (h * g) map_add' _ _ := rfl map_smul' _ _ := rfl theorem rightTranslate2_apply (g : LocalGL2 v) (f : LocalGL2 v β†’ β„‚) (h : LocalGL2 v) : rightTranslate2 v g f h = f (h * g) := rfl theorem rightTranslate2_mul (g g' : LocalGL2 v) : rightTranslate2 v (g * g') = rightTranslate2 v g * rightTranslate2 v g' := by ext f h simp [rightTranslate2_apply, mul_assoc] def diagonal2 (a : Fin 2 β†’ (v.adicCompletion β„š)Λ£) : LocalGL2 v where val := diagonal fun i => (a i : v.adicCompletion β„š) inv := diagonal fun i => ((a i)⁻¹ : (v.adicCompletion β„š)Λ£) val_inv := by rw [diagonal_mul_diagonal] simp only [Units.mul_inv, diagonal_one] inv_val := by rw [diagonal_mul_diagonal] simp only [Units.inv_mul, diagonal_one] @[simp] theorem diagonal2_coe (a : Fin 2 β†’ (v.adicCompletion β„š)Λ£) : (diagonal2 v a : Matrix (Fin 2) (Fin 2) (v.adicCompletion β„š)) = diagonal fun i => (a i : v.adicCompletion β„š) := rfl theorem diagonal2_mul (a b : Fin 2 β†’ (v.adicCompletion β„š)Λ£) : diagonal2 v (a * b) = diagonal2 v a * diagonal2 v b := by ext i j rcases eq_or_ne i j with rfl | hij Β· simp [diagonal2] Β· simp [diagonal2, Matrix.diagonal_apply_ne _ hij] def upperUnipotent2 (x : v.adicCompletion β„š) : LocalGL2 v where val := !![1, x; 0, 1] inv := !![1, -x; 0, 1] val_inv := by ext i j fin_cases i <;> fin_cases j <;> simp [Matrix.mul_apply, Fin.sum_univ_two] inv_val := by ext i j fin_cases i <;> fin_cases j <;> simp [Matrix.mul_apply, Fin.sum_univ_two] @[simp] theorem upperUnipotent2_coe (x : v.adicCompletion β„š) : (upperUnipotent2 v x : Matrix (Fin 2) (Fin 2) (v.adicCompletion β„š)) = !![1, x; 0, 1] := rfl def halfModulus2 (a : Fin 2 β†’ (v.adicCompletion β„š)Λ£) : β„‚ := ((Real.sqrt (β€–(a 0 : v.adicCompletion β„š)β€– / β€–(a 1 : v.adicCompletion β„š)β€–) : ℝ) : β„‚) theorem halfModulus2_mul (a b : Fin 2 β†’ (v.adicCompletion β„š)Λ£) : halfModulus2 v (a * b) = halfModulus2 v a * halfModulus2 v b := by simp only [halfModulus2, Pi.mul_apply, Units.val_mul, norm_mul] rw [show β€–(a 0 : v.adicCompletion β„š)β€– * β€–(b 0 : v.adicCompletion β„š)β€– / (β€–(a 1 : v.adicCompletion β„š)β€– * β€–(b 1 : v.adicCompletion β„š)β€–) = β€–(a 0 : v.adicCompletion β„š)β€– / β€–(a 1 : v.adicCompletion β„š)β€– * (β€–(b 0 : v.adicCompletion β„š)β€– / β€–(b 1 : v.adicCompletion β„š)β€–) by ring, Real.sqrt_mul (by positivity)] push_cast ring @[simp] theorem halfModulus2_one : halfModulus2 v 1 = 1 := by simp [halfModulus2] theorem halfModulus2_ne_zero (a : Fin 2 β†’ (v.adicCompletion β„š)Λ£) : halfModulus2 v a β‰  0 := by unfold halfModulus2 exact_mod_cast (Real.sqrt_pos.mpr (div_pos (norm_pos_iff.mpr (a 0).ne_zero) (norm_pos_iff.mpr (a 1).ne_zero))).ne' theorem halfModulus2_eq_pos_real (a : Fin 2 β†’ (v.adicCompletion β„š)Λ£) : βˆƒ r : ℝ, 0 < r ∧ halfModulus2 v a = (r : β„‚) := ⟨_, Real.sqrt_pos.mpr (div_pos (norm_pos_iff.mpr (a 0).ne_zero) (norm_pos_iff.mpr (a 1).ne_zero)), rfl⟩ private theorem toAdd_unzero_exp (n : β„€) (h : (WithZero.exp n : WithZero (Multiplicative β„€)) β‰  0) : Multiplicative.toAdd (WithZero.unzero h) = n := rfl private theorem norm_uniformizerUnit : β€–(uniformizerUnit β„š v : v.adicCompletion β„š)β€– = (((Ideal.absNorm v.asIdeal : β„•) : ℝ))⁻¹ := by rw [NumberField.FinitePlace.norm_def, valued_uniformizerUnit, WithZeroMulInt.toNNReal_neg_apply _ WithZero.exp_ne_zero, toAdd_unzero_exp] simp theorem halfModulus2_sq_uniformizerUnit : halfModulus2 v ![uniformizerUnit β„š v, 1] ^ 2 = ((((Ideal.absNorm v.asIdeal : β„•) : ℝ)⁻¹ : ℝ) : β„‚) := by have h : halfModulus2 v ![uniformizerUnit β„š v, 1] = ((Real.sqrt β€–(uniformizerUnit β„š v : v.adicCompletion β„š)β€– : ℝ) : β„‚) := by simp [halfModulus2] rw [h, ← Complex.ofReal_pow, Real.sq_sqrt (norm_nonneg _), norm_uniformizerUnit] def torusChar2 (Ο‡ : Fin 2 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) (a : Fin 2 β†’ (v.adicCompletion β„š)Λ£) : β„‚ := ∏ i : Fin 2, ((Ο‡ i (a i) : β„‚Λ£) : β„‚) theorem torusChar2_mul (Ο‡ : Fin 2 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) (a b : Fin 2 β†’ (v.adicCompletion β„š)Λ£) : torusChar2 v Ο‡ (a * b) = torusChar2 v Ο‡ a * torusChar2 v Ο‡ b := by simp only [torusChar2, Pi.mul_apply, map_mul, Units.val_mul, Finset.prod_mul_distrib] @[simp] theorem torusChar2_one (Ο‡ : Fin 2 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) : torusChar2 v Ο‡ 1 = 1 := by simp [torusChar2] def principalSeries2 (Ο‡ : Fin 2 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) : Submodule β„‚ (LocalGL2 v β†’ β„‚) where carrier := {f | IsLocallyConstant f ∧ (βˆ€ (x : v.adicCompletion β„š) (g : LocalGL2 v), f (upperUnipotent2 v x * g) = f g) ∧ βˆ€ (a : Fin 2 β†’ (v.adicCompletion β„š)Λ£) (g : LocalGL2 v), f (diagonal2 v a * g) = torusChar2 v Ο‡ a * halfModulus2 v a * f g} zero_mem' := ⟨IsLocallyConstant.const 0, fun _ _ => rfl, fun _ _ => by simp⟩ add_mem' := by intro f₁ fβ‚‚ h₁ hβ‚‚ obtain ⟨h₁lc, h₁n, h₁t⟩ := h₁ obtain ⟨hβ‚‚lc, hβ‚‚n, hβ‚‚t⟩ := hβ‚‚ refine ⟨h₁lc.compβ‚‚ hβ‚‚lc (Β· + Β·), fun x g => ?_, fun a g => ?_⟩ Β· show f₁ _ + fβ‚‚ _ = f₁ g + fβ‚‚ g rw [h₁n, hβ‚‚n] Β· show f₁ _ + fβ‚‚ _ = _ * (f₁ g + fβ‚‚ g) rw [h₁t, hβ‚‚t] ring smul_mem' := by intro c f hf obtain ⟨hlc, hn, ht⟩ := hf refine ⟨hlc.comp (c * Β·), fun x g => ?_, fun a g => ?_⟩ Β· show c * f _ = c * f g rw [hn] Β· show c * f _ = _ * (c * f g) rw [ht] ring variable {v} theorem mem_principalSeries2_iff {Ο‡ : Fin 2 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)} {f : LocalGL2 v β†’ β„‚} : f ∈ principalSeries2 v Ο‡ ↔ IsLocallyConstant f ∧ (βˆ€ (x : v.adicCompletion β„š) (g : LocalGL2 v), f (upperUnipotent2 v x * g) = f g) ∧ βˆ€ (a : Fin 2 β†’ (v.adicCompletion β„š)Λ£) (g : LocalGL2 v), f (diagonal2 v a * g) = torusChar2 v Ο‡ a * halfModulus2 v a * f g := Iff.rfl theorem rightTranslate2_mem_principalSeries2 {Ο‡ : Fin 2 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)} {f : LocalGL2 v β†’ β„‚} (hf : f ∈ principalSeries2 v Ο‡) (g : LocalGL2 v) : rightTranslate2 v g f ∈ principalSeries2 v Ο‡ := by obtain ⟨hlc, hn, ht⟩ := mem_principalSeries2_iff.mp hf refine mem_principalSeries2_iff.mpr ⟨hlc.comp_continuous (continuous_id.mul continuous_const), fun x h => ?_, fun a h => ?_⟩ Β· show f (upperUnipotent2 v x * h * g) = f (h * g) rw [mul_assoc, hn] Β· show f (diagonal2 v a * h * g) = _ * f (h * g) rw [mul_assoc, ht] def principalSeries2Rep (Ο‡ : Fin 2 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) : LocalGL2 v β†’* Module.End β„‚ β†₯(principalSeries2 v Ο‡) where toFun g := (rightTranslate2 v g).restrict fun f hf => rightTranslate2_mem_principalSeries2 hf g map_one' := by ext f h simp [rightTranslate2_apply] map_mul' g g' := by ext f h simp [rightTranslate2_apply, mul_assoc] section Witness2 variable (v) def gl2Entry (g : LocalGL2 v) (i j : Fin 2) : v.adicCompletion β„š := (g : Matrix (Fin 2) (Fin 2) (v.adicCompletion β„š)) i j def gl2Det (g : LocalGL2 v) : v.adicCompletion β„š := (g : Matrix (Fin 2) (Fin 2) (v.adicCompletion β„š)).det theorem gl2Det_ne_zero (g : LocalGL2 v) : gl2Det v g β‰  0 := by have h := (Matrix.GeneralLinearGroup.det g).ne_zero rwa [Matrix.GeneralLinearGroup.val_det_apply] at h theorem gl2Det_eq (g : LocalGL2 v) : gl2Det v g = gl2Entry v g 0 0 * gl2Entry v g 1 1 - gl2Entry v g 0 1 * gl2Entry v g 1 0 := by simp only [gl2Det, gl2Entry, Matrix.det_fin_two] theorem continuous_gl2Entry (i j : Fin 2) : Continuous fun g : LocalGL2 v => gl2Entry v g i j := Units.continuous_val.matrix_elem i j theorem continuous_gl2Det : Continuous (gl2Det v) := Units.continuous_val.matrix_det theorem gl2Entry_upperUnipotent2_mul_one (x : v.adicCompletion β„š) (g : LocalGL2 v) (j : Fin 2) : gl2Entry v (upperUnipotent2 v x * g) 1 j = gl2Entry v g 1 j := by simp [gl2Entry, Matrix.mul_apply, Fin.sum_univ_two] theorem gl2Det_upperUnipotent2_mul (x : v.adicCompletion β„š) (g : LocalGL2 v) : gl2Det v (upperUnipotent2 v x * g) = gl2Det v g := by simp only [gl2Det, Units.val_mul, Matrix.det_mul, upperUnipotent2_coe, Matrix.det_fin_two_of] simp theorem gl2Entry_diagonal2_mul (a : Fin 2 β†’ (v.adicCompletion β„š)Λ£) (g : LocalGL2 v) (i j : Fin 2) : gl2Entry v (diagonal2 v a * g) i j = (a i : v.adicCompletion β„š) * gl2Entry v g i j := by simp [gl2Entry, diagonal2_coe, Matrix.diagonal_mul] theorem gl2Det_diagonal2_mul (a : Fin 2 β†’ (v.adicCompletion β„š)Λ£) (g : LocalGL2 v) : gl2Det v (diagonal2 v a * g) = (a 0 : v.adicCompletion β„š) * a 1 * gl2Det v g := by simp only [gl2Det, Units.val_mul, Matrix.det_mul, diagonal2_coe, Matrix.det_diagonal, Fin.prod_univ_two] def cornerEntry2 (g : LocalGL2 v) : v.adicCompletion β„š := gl2Entry v g 1 0 theorem continuous_cornerEntry2 : Continuous (cornerEntry2 v) := continuous_gl2Entry v 1 0 theorem cornerEntry2_upperUnipotent2_mul (x : v.adicCompletion β„š) (g : LocalGL2 v) : cornerEntry2 v (upperUnipotent2 v x * g) = cornerEntry2 v g := gl2Entry_upperUnipotent2_mul_one v x g 0 theorem cornerEntry2_diagonal2_mul (a : Fin 2 β†’ (v.adicCompletion β„š)Λ£) (g : LocalGL2 v) : cornerEntry2 v (diagonal2 v a * g) = (a 1 : v.adicCompletion β„š) * cornerEntry2 v g := gl2Entry_diagonal2_mul v a g 1 0 theorem gl2Entry_one_one_ne_zero_of_cornerEntry2_eq_zero {g : LocalGL2 v} (hc : cornerEntry2 v g = 0) : gl2Entry v g 1 1 β‰  0 := by intro h apply gl2Det_ne_zero v g have hc' : gl2Entry v g 1 0 = 0 := hc rw [gl2Det_eq, h, hc'] ring def cellCutoff2 : Set (LocalGL2 v) := {g | cornerEntry2 v g β‰  0 ∧ Valued.v (gl2Entry v g 1 1 / cornerEntry2 v g) ≀ 1} theorem upperUnipotent2_mul_mem_cellCutoff2_iff (x : v.adicCompletion β„š) (g : LocalGL2 v) : upperUnipotent2 v x * g ∈ cellCutoff2 v ↔ g ∈ cellCutoff2 v := by simp only [cellCutoff2, Set.mem_setOf_eq, cornerEntry2_upperUnipotent2_mul, gl2Entry_upperUnipotent2_mul_one] theorem diagonal2_mul_mem_cellCutoff2_iff (a : Fin 2 β†’ (v.adicCompletion β„š)Λ£) (g : LocalGL2 v) : diagonal2 v a * g ∈ cellCutoff2 v ↔ g ∈ cellCutoff2 v := by simp only [cellCutoff2, Set.mem_setOf_eq, cornerEntry2_diagonal2_mul, gl2Entry_diagonal2_mul, mul_div_mul_left _ _ (a 1).ne_zero, mul_ne_zero_iff, ne_eq, (a 1).ne_zero, not_false_eq_true, true_and] def cellValue2 (Ο‡ : Fin 2 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) (g : LocalGL2 v) : β„‚ := charExt (Ο‡ 0) (gl2Det v g / cornerEntry2 v g) * charExt (Ο‡ 1) (cornerEntry2 v g) * ((Real.sqrt (β€–gl2Det v g / cornerEntry2 v gβ€– / β€–cornerEntry2 v gβ€–) : ℝ) : β„‚) def cellSection2 (Ο‡ : Fin 2 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) : LocalGL2 v β†’ β„‚ := (cellCutoff2 v).indicator (cellValue2 v Ο‡) theorem cellValue2_upperUnipotent2_mul (Ο‡ : Fin 2 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) (x : v.adicCompletion β„š) (g : LocalGL2 v) : cellValue2 v Ο‡ (upperUnipotent2 v x * g) = cellValue2 v Ο‡ g := by simp only [cellValue2, cornerEntry2_upperUnipotent2_mul, gl2Det_upperUnipotent2_mul] theorem cellSection2_upperUnipotent2_mul (Ο‡ : Fin 2 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) (x : v.adicCompletion β„š) (g : LocalGL2 v) : cellSection2 v Ο‡ (upperUnipotent2 v x * g) = cellSection2 v Ο‡ g := by by_cases hg : g ∈ cellCutoff2 v Β· rw [cellSection2, Set.indicator_of_mem (by rwa [upperUnipotent2_mul_mem_cellCutoff2_iff]), Set.indicator_of_mem hg, cellValue2_upperUnipotent2_mul] Β· rw [cellSection2, Set.indicator_of_notMem (by rwa [upperUnipotent2_mul_mem_cellCutoff2_iff]), Set.indicator_of_notMem hg] theorem cellValue2_diagonal2_mul (Ο‡ : Fin 2 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) (a : Fin 2 β†’ (v.adicCompletion β„š)Λ£) (g : LocalGL2 v) : cellValue2 v Ο‡ (diagonal2 v a * g) = torusChar2 v Ο‡ a * halfModulus2 v a * cellValue2 v Ο‡ g := by have h1 : (a 1 : v.adicCompletion β„š) β‰  0 := (a 1).ne_zero have hdet : gl2Det v (diagonal2 v a * g) / cornerEntry2 v (diagonal2 v a * g) = (a 0 : v.adicCompletion β„š) * (gl2Det v g / cornerEntry2 v g) := by rw [gl2Det_diagonal2_mul, cornerEntry2_diagonal2_mul, show (a 0 : v.adicCompletion β„š) * a 1 * gl2Det v g = (a 1 : v.adicCompletion β„š) * (a 0 * gl2Det v g) by ring, mul_div_mul_left _ _ h1, mul_div_assoc] have hmod : β€–(a 0 : v.adicCompletion β„š) * (gl2Det v g / cornerEntry2 v g)β€– / β€–(a 1 : v.adicCompletion β„š) * cornerEntry2 v gβ€– = β€–(a 0 : v.adicCompletion β„š)β€– / β€–(a 1 : v.adicCompletion β„š)β€– * (β€–gl2Det v g / cornerEntry2 v gβ€– / β€–cornerEntry2 v gβ€–) := by rw [norm_mul, norm_mul] ring rw [cellValue2, cellValue2, hdet, cornerEntry2_diagonal2_mul, hmod, charExt_units_mul, charExt_units_mul, Real.sqrt_mul (div_nonneg (norm_nonneg _) (norm_nonneg _))] simp only [torusChar2, halfModulus2, Fin.prod_univ_two] push_cast ring theorem cellSection2_diagonal2_mul (Ο‡ : Fin 2 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) (a : Fin 2 β†’ (v.adicCompletion β„š)Λ£) (g : LocalGL2 v) : cellSection2 v Ο‡ (diagonal2 v a * g) = torusChar2 v Ο‡ a * halfModulus2 v a * cellSection2 v Ο‡ g := by by_cases hg : g ∈ cellCutoff2 v Β· rw [cellSection2, Set.indicator_of_mem (by rwa [diagonal2_mul_mem_cellCutoff2_iff]), Set.indicator_of_mem hg, cellValue2_diagonal2_mul] Β· rw [cellSection2, Set.indicator_of_notMem (by rwa [diagonal2_mul_mem_cellCutoff2_iff]), Set.indicator_of_notMem hg, mul_zero] theorem eventually_one_lt_valued_div2 {n d : LocalGL2 v β†’ v.adicCompletion β„š} {g : LocalGL2 v} (hn : Continuous n) (hd : Continuous d) (hng : n g β‰  0) (hdg : d g = 0) : βˆ€αΆ  h in nhds g, d h β‰  0 β†’ 1 < Valued.v (n h / d h) := by have h1 : βˆ€αΆ  h in nhds g, Valued.v (n h) = Valued.v (n g) := (hn.tendsto g).eventually (eventually_valued_eq v hng) have h2 : βˆ€αΆ  h in nhds g, Valued.v (d h) < Valued.v (n g) := by have ht : Filter.Tendsto d (nhds g) (nhds 0) := by simpa [hdg] using hd.tendsto g exact ht.eventually (eventually_valued_lt v hng) filter_upwards [h1, h2] with h hn' hd' hd0 have hvd : Valued.v (d h) β‰  0 := (Valuation.ne_zero_iff _).mpr hd0 rw [map_divβ‚€, hn', one_lt_divβ‚€ (lt_of_le_of_ne zero_le' hvd.symm)] exact hd' theorem isLocallyConstant_cellSection2 (Ο‡ : Fin 2 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) (hΟ‡ : βˆ€ i, IsLocallyConstant (Ο‡ i)) : IsLocallyConstant (cellSection2 v Ο‡) := by rw [IsLocallyConstant.iff_eventually_eq] intro g by_cases hc : cornerEntry2 v g = 0 Β· have hg : g βˆ‰ cellCutoff2 v := fun hg => hg.1 hc have hev := eventually_one_lt_valued_div2 v (continuous_gl2Entry v 1 1) (continuous_cornerEntry2 v) (gl2Entry_one_one_ne_zero_of_cornerEntry2_eq_zero v hc) hc filter_upwards [hev] with h hh have hh' : h βˆ‰ cellCutoff2 v := fun hmem => (not_le.mpr (hh hmem.1)) hmem.2 rw [cellSection2, Set.indicator_of_notMem hh', Set.indicator_of_notMem hg] have hcA : ContinuousAt (cornerEntry2 v) g := (continuous_cornerEntry2 v).continuousAt have hc' : βˆ€αΆ  h in nhds g, cornerEntry2 v h β‰  0 := hcA.eventually_ne hc have hr : βˆ€αΆ  h in nhds g, (Valued.v (gl2Entry v h 1 1 / cornerEntry2 v h) ≀ 1 ↔ Valued.v (gl2Entry v g 1 1 / cornerEntry2 v g) ≀ 1) := (((continuous_gl2Entry v 1 1).continuousAt).div hcA hc).eventually (eventually_mem_iff_of_isClopen v (isClopen_valued_le_one v) (gl2Entry v g 1 1 / cornerEntry2 v g)) have hmem : βˆ€αΆ  h in nhds g, (h ∈ cellCutoff2 v ↔ g ∈ cellCutoff2 v) := by filter_upwards [hc', hr] with h hh hrh simp only [cellCutoff2, Set.mem_setOf_eq, hh, hc, ne_eq, not_false_eq_true, true_and] exact hrh have hval : βˆ€αΆ  h in nhds g, cellValue2 v Ο‡ h = cellValue2 v Ο‡ g := by have hdA : ContinuousAt (fun h => gl2Det v h / cornerEntry2 v h) g := ((continuous_gl2Det v).continuousAt).div hcA hc have hd0 : gl2Det v g / cornerEntry2 v g β‰  0 := div_ne_zero (gl2Det_ne_zero v g) hc filter_upwards [hdA.eventually (eventually_charExt_eq v (Ο‡ 0) (hΟ‡ 0) hd0), hcA.eventually (eventually_charExt_eq v (Ο‡ 1) (hΟ‡ 1) hc), hdA.eventually (eventually_norm_eq v hd0), hcA.eventually (eventually_norm_eq v hc)] with h e0 e1 n0 n1 simp only [cellValue2, e0, e1, n0, n1] filter_upwards [hmem, hval] with h hm hv by_cases hg : g ∈ cellCutoff2 v Β· rw [cellSection2, Set.indicator_of_mem (hm.mpr hg), Set.indicator_of_mem hg, hv] Β· rw [cellSection2, Set.indicator_of_notMem (fun hh => hg (hm.mp hh)), Set.indicator_of_notMem hg] theorem cellSection2_mem_principalSeries2 (Ο‡ : Fin 2 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) (hΟ‡ : βˆ€ i, IsLocallyConstant (Ο‡ i)) : cellSection2 v Ο‡ ∈ principalSeries2 v Ο‡ := ⟨isLocallyConstant_cellSection2 v Ο‡ hΟ‡, cellSection2_upperUnipotent2_mul v Ο‡, cellSection2_diagonal2_mul v Ο‡βŸ© def antidiagonal2 : LocalGL2 v := Matrix.GeneralLinearGroup.mkOfDetNeZero !![(0 : v.adicCompletion β„š), 1; 1, 0] (by simp [Matrix.det_fin_two_of]) theorem antidiagonal2_coe : (antidiagonal2 v : Matrix (Fin 2) (Fin 2) (v.adicCompletion β„š)) = !![(0 : v.adicCompletion β„š), 1; 1, 0] := rfl theorem cornerEntry2_antidiagonal2 : cornerEntry2 v (antidiagonal2 v) = 1 := by simp [cornerEntry2, gl2Entry, antidiagonal2_coe] theorem gl2Entry_antidiagonal2_one_one : gl2Entry v (antidiagonal2 v) 1 1 = 0 := by simp [gl2Entry, antidiagonal2_coe] theorem gl2Det_antidiagonal2 : gl2Det v (antidiagonal2 v) = -1 := by simp [gl2Det, antidiagonal2_coe, Matrix.det_fin_two_of] theorem antidiagonal2_mem_cellCutoff2 : antidiagonal2 v ∈ cellCutoff2 v := by refine ⟨?_, ?_⟩ Β· rw [cornerEntry2_antidiagonal2] exact one_ne_zero Β· simp [gl2Entry_antidiagonal2_one_one] theorem cellSection2_antidiagonal2_ne_zero (Ο‡ : Fin 2 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) : cellSection2 v Ο‡ (antidiagonal2 v) β‰  0 := by have h0 : charExt (Ο‡ 0) (-1 : v.adicCompletion β„š) = (Ο‡ 0 (-1) : β„‚) := by simpa using charExt_coe_units (Ο‡ 0) (-1) have h1 : charExt (Ο‡ 1) (1 : v.adicCompletion β„š) = (Ο‡ 1 1 : β„‚) := by simpa using charExt_coe_units (Ο‡ 1) 1 rw [cellSection2, Set.indicator_of_mem (antidiagonal2_mem_cellCutoff2 v)] simp only [cellValue2, gl2Det_antidiagonal2, cornerEntry2_antidiagonal2, div_one, h0, h1, norm_neg, norm_one, Real.sqrt_one, Complex.ofReal_one, mul_one] exact mul_ne_zero (Units.ne_zero _) (Units.ne_zero _) theorem principalSeries2_ne_bot (Ο‡ : Fin 2 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) (hΟ‡ : βˆ€ i, IsLocallyConstant (Ο‡ i)) : principalSeries2 v Ο‡ β‰  βŠ₯ := by intro hbot have hmem := cellSection2_mem_principalSeries2 v Ο‡ hΟ‡ rw [hbot, Submodule.mem_bot] at hmem exact cellSection2_antidiagonal2_ne_zero v Ο‡ (by simp [hmem]) end Witness2 section UnipotentLine variable (v) theorem upperUnipotent2_mul (x y : v.adicCompletion β„š) : upperUnipotent2 v x * upperUnipotent2 v y = upperUnipotent2 v (x + y) := by ext i j fin_cases i <;> fin_cases j <;> simp [Matrix.mul_apply, Fin.sum_univ_two, add_comm] theorem upperUnipotent2_zero : upperUnipotent2 v 0 = 1 := by ext i j fin_cases i <;> fin_cases j <;> simp def unipotentHom2 : Multiplicative (v.adicCompletion β„š) β†’* LocalGL2 v where toFun x := upperUnipotent2 v (Multiplicative.toAdd x) map_one' := upperUnipotent2_zero v map_mul' x y := (upperUnipotent2_mul v (Multiplicative.toAdd x) (Multiplicative.toAdd y)).symm @[simp] theorem unipotentHom2_ofAdd (x : v.adicCompletion β„š) : unipotentHom2 v (Multiplicative.ofAdd x) = upperUnipotent2 v x := rfl def unipotentRep2 (Ο‡ : Fin 2 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) : Representation β„‚ (Multiplicative (v.adicCompletion β„š)) β†₯(principalSeries2 v Ο‡) := (principalSeries2Rep (v := v) Ο‡).comp (unipotentHom2 v) theorem unipotentRep2_ofAdd_apply_coe (Ο‡ : Fin 2 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) (x : v.adicCompletion β„š) (f : β†₯(principalSeries2 v Ο‡)) (g : LocalGL2 v) : (unipotentRep2 v Ο‡ (Multiplicative.ofAdd x) f : LocalGL2 v β†’ β„‚) g = (f : LocalGL2 v β†’ β„‚) (g * upperUnipotent2 v x) := rfl end UnipotentLine end PrincipalSeries2 end LanglandsTunnell.CubicInduction end