import Definitions.Def_LanglandsTunnell_CubicInduction_Structure import Mathlib.NumberTheory.NumberField.Completion.FinitePlace set_option autoImplicit false open Matrix IsDedekindDomain NumberField NumberField.AdelicLevel LanglandsTunnell.TateLocal noncomputable section namespace LanglandsTunnell.CubicInduction section PrincipalSeries3 variable (v : HeightOneSpectrum (π“ž β„š)) def diagonal3 (a : Fin 3 β†’ (v.adicCompletion β„š)Λ£) : LocalGL3 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] theorem diagonal3_mul (a b : Fin 3 β†’ (v.adicCompletion β„š)Λ£) : diagonal3 v (a * b) = diagonal3 v a * diagonal3 v b := by ext i j rcases eq_or_ne i j with rfl | hij Β· simp [diagonal3] Β· simp [diagonal3, Matrix.diagonal_apply_ne _ hij] @[simp] theorem diagonal3_coe (a : Fin 3 β†’ (v.adicCompletion β„š)Λ£) : (diagonal3 v a : Matrix (Fin 3) (Fin 3) (v.adicCompletion β„š)) = diagonal fun i => (a i : v.adicCompletion β„š) := rfl def halfModulus3 (a : Fin 3 β†’ (v.adicCompletion β„š)Λ£) : β„‚ := ((β€–(a 0 : v.adicCompletion β„š)β€– / β€–(a 2 : v.adicCompletion β„š)β€– : ℝ) : β„‚) theorem halfModulus3_mul (a b : Fin 3 β†’ (v.adicCompletion β„š)Λ£) : halfModulus3 v (a * b) = halfModulus3 v a * halfModulus3 v b := by simp only [halfModulus3, Pi.mul_apply, Units.val_mul, norm_mul] push_cast ring @[simp] theorem halfModulus3_one : halfModulus3 v 1 = 1 := by simp [halfModulus3] 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 halfModulus3_uniformizerUnit : halfModulus3 v ![uniformizerUnit β„š v, 1, 1] = (((Ideal.absNorm v.asIdeal : β„•) : ℝ)⁻¹ : ℝ) := by simp [halfModulus3, norm_uniformizerUnit] theorem halfModulus3_one_uniformizerUnit_one : halfModulus3 v ![1, uniformizerUnit β„š v, 1] = 1 := by simp [halfModulus3] theorem halfModulus3_one_one_uniformizerUnit : halfModulus3 v ![1, 1, uniformizerUnit β„š v] = (((Ideal.absNorm v.asIdeal : β„•) : ℝ) : ℝ) := by simp [halfModulus3, norm_uniformizerUnit] def torusChar3 (Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) (a : Fin 3 β†’ (v.adicCompletion β„š)Λ£) : β„‚ := ∏ i : Fin 3, ((Ο‡ i (a i) : β„‚Λ£) : β„‚) theorem torusChar3_mul (Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) (a b : Fin 3 β†’ (v.adicCompletion β„š)Λ£) : torusChar3 v Ο‡ (a * b) = torusChar3 v Ο‡ a * torusChar3 v Ο‡ b := by simp only [torusChar3, Pi.mul_apply, map_mul, Units.val_mul, Finset.prod_mul_distrib] @[simp] theorem torusChar3_one (Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) : torusChar3 v Ο‡ 1 = 1 := by simp [torusChar3] def principalSeries3 (Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) : Submodule β„‚ (LocalGL3 v β†’ β„‚) where carrier := {f | IsLocallyConstant f ∧ (βˆ€ (x y z : v.adicCompletion β„š) (g : LocalGL3 v), f (upperUnipotent3 x y z * g) = f g) ∧ βˆ€ (a : Fin 3 β†’ (v.adicCompletion β„š)Λ£) (g : LocalGL3 v), f (diagonal3 v a * g) = torusChar3 v Ο‡ a * halfModulus3 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 y z 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 y z 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_principalSeries3_iff {Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)} {f : LocalGL3 v β†’ β„‚} : f ∈ principalSeries3 v Ο‡ ↔ IsLocallyConstant f ∧ (βˆ€ (x y z : v.adicCompletion β„š) (g : LocalGL3 v), f (upperUnipotent3 x y z * g) = f g) ∧ βˆ€ (a : Fin 3 β†’ (v.adicCompletion β„š)Λ£) (g : LocalGL3 v), f (diagonal3 v a * g) = torusChar3 v Ο‡ a * halfModulus3 v a * f g := Iff.rfl theorem isLocallyConstant_of_mem_principalSeries3 {Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)} {f : LocalGL3 v β†’ β„‚} (hf : f ∈ principalSeries3 v Ο‡) : IsLocallyConstant f := (mem_principalSeries3_iff.mp hf).1 theorem apply_upperUnipotent3_mul_of_mem_principalSeries3 {Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)} {f : LocalGL3 v β†’ β„‚} (hf : f ∈ principalSeries3 v Ο‡) (x y z : v.adicCompletion β„š) (g : LocalGL3 v) : f (upperUnipotent3 x y z * g) = f g := (mem_principalSeries3_iff.mp hf).2.1 x y z g theorem apply_diagonal3_mul_of_mem_principalSeries3 {Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)} {f : LocalGL3 v β†’ β„‚} (hf : f ∈ principalSeries3 v Ο‡) (a : Fin 3 β†’ (v.adicCompletion β„š)Λ£) (g : LocalGL3 v) : f (diagonal3 v a * g) = torusChar3 v Ο‡ a * halfModulus3 v a * f g := (mem_principalSeries3_iff.mp hf).2.2 a g theorem rightTranslate_mem_principalSeries3 {Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)} {f : LocalGL3 v β†’ β„‚} (hf : f ∈ principalSeries3 v Ο‡) (g : LocalGL3 v) : gl3AmbientRightTranslate (R := β„‚) g f ∈ principalSeries3 v Ο‡ := by obtain ⟨hlc, hn, ht⟩ := mem_principalSeries3_iff.mp hf refine mem_principalSeries3_iff.mpr ⟨hlc.comp_continuous (continuous_id.mul continuous_const), fun x y z h => ?_, fun a h => ?_⟩ Β· show f (upperUnipotent3 x y z * h * g) = f (h * g) rw [mul_assoc, hn] Β· show f (diagonal3 v a * h * g) = _ * f (h * g) rw [mul_assoc, ht] def coefficientFn {Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)} (L : β†₯(principalSeries3 v Ο‡) β†’β‚—[β„‚] β„‚) (f : β†₯(principalSeries3 v Ο‡)) : LocalGL3 v β†’ β„‚ := fun g => L ⟨gl3AmbientRightTranslate (R := β„‚) g f, rightTranslate_mem_principalSeries3 f.2 g⟩ def IsWhittakerFunctional3 {Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)} (ψ : AddChar (v.adicCompletion β„š) β„‚) (Ξ› : β†₯(principalSeries3 v Ο‡) β†’β‚—[β„‚] β„‚) : Prop := βˆ€ (x y z : v.adicCompletion β„š) (F : β†₯(principalSeries3 v Ο‡)), Ξ› ⟨gl3AmbientRightTranslate (R := β„‚) (upperUnipotent3 x y z) F, rightTranslate_mem_principalSeries3 F.2 (upperUnipotent3 x y z)⟩ = ψ (x + y) * Ξ› F theorem isWhittakerFunctional3_zero {Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)} (ψ : AddChar (v.adicCompletion β„š) β„‚) : IsWhittakerFunctional3 (Ο‡ := Ο‡) ψ 0 := by intro x y z F simp theorem isGL3PsiWhittakerFn_coefficientFn {Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)} {ψ : AddChar (v.adicCompletion β„š) β„‚} {Ξ› : β†₯(principalSeries3 v Ο‡) β†’β‚—[β„‚] β„‚} (hΞ› : IsWhittakerFunctional3 ψ Ξ›) (f : β†₯(principalSeries3 v Ο‡)) : IsGL3PsiWhittakerFn ψ (coefficientFn Ξ› f) := by intro x y z g have hfun : gl3AmbientRightTranslate (R := β„‚) (upperUnipotent3 x y z * g) (f : LocalGL3 v β†’ β„‚) = gl3AmbientRightTranslate (R := β„‚) (upperUnipotent3 x y z) (gl3AmbientRightTranslate (R := β„‚) g f) := by funext h simp [gl3AmbientRightTranslate, mul_assoc] have hsub : (⟨_, rightTranslate_mem_principalSeries3 f.2 (upperUnipotent3 x y z * g)⟩ : β†₯(principalSeries3 v Ο‡)) = ⟨_, rightTranslate_mem_principalSeries3 (rightTranslate_mem_principalSeries3 f.2 g) (upperUnipotent3 x y z)⟩ := Subtype.ext hfun show Ξ› _ = ψ (x + y) * Ξ› _ rw [hsub] exact hΞ› x y z ⟨_, rightTranslate_mem_principalSeries3 f.2 g⟩ end PrincipalSeries3 section Witness variable (v : HeightOneSpectrum (π“ž β„š)) def gl3Entry (g : LocalGL3 v) (i j : Fin 3) : v.adicCompletion β„š := (g : Matrix (Fin 3) (Fin 3) (v.adicCompletion β„š)) i j def cornerEntry (g : LocalGL3 v) : v.adicCompletion β„š := gl3Entry v g 2 0 def lowerMinor (g : LocalGL3 v) : v.adicCompletion β„š := gl3Entry v g 1 0 * gl3Entry v g 2 1 - gl3Entry v g 1 1 * gl3Entry v g 2 0 def outerMinor (g : LocalGL3 v) : v.adicCompletion β„š := gl3Entry v g 1 0 * gl3Entry v g 2 2 - gl3Entry v g 1 2 * gl3Entry v g 2 0 def gl3Det (g : LocalGL3 v) : v.adicCompletion β„š := (g : Matrix (Fin 3) (Fin 3) (v.adicCompletion β„š)).det theorem gl3Det_ne_zero (g : LocalGL3 v) : gl3Det v g β‰  0 := by have h := (Matrix.GeneralLinearGroup.det g).ne_zero rwa [Matrix.GeneralLinearGroup.val_det_apply] at h theorem gl3Entry_upperUnipotent3_mul_two (x y z : v.adicCompletion β„š) (g : LocalGL3 v) (j : Fin 3) : gl3Entry v (upperUnipotent3 x y z * g) 2 j = gl3Entry v g 2 j := by simp [gl3Entry, Matrix.mul_apply, Fin.sum_univ_three] theorem gl3Entry_upperUnipotent3_mul_one (x y z : v.adicCompletion β„š) (g : LocalGL3 v) (j : Fin 3) : gl3Entry v (upperUnipotent3 x y z * g) 1 j = gl3Entry v g 1 j + y * gl3Entry v g 2 j := by simp [gl3Entry, Matrix.mul_apply, Fin.sum_univ_three] theorem gl3Entry_diagonal3_mul (a : Fin 3 β†’ (v.adicCompletion β„š)Λ£) (g : LocalGL3 v) (i j : Fin 3) : gl3Entry v (diagonal3 v a * g) i j = (a i : v.adicCompletion β„š) * gl3Entry v g i j := by simp [gl3Entry, diagonal3_coe, Matrix.diagonal_mul] theorem cornerEntry_upperUnipotent3_mul (x y z : v.adicCompletion β„š) (g : LocalGL3 v) : cornerEntry v (upperUnipotent3 x y z * g) = cornerEntry v g := gl3Entry_upperUnipotent3_mul_two v x y z g 0 theorem lowerMinor_upperUnipotent3_mul (x y z : v.adicCompletion β„š) (g : LocalGL3 v) : lowerMinor v (upperUnipotent3 x y z * g) = lowerMinor v g := by simp only [lowerMinor, gl3Entry_upperUnipotent3_mul_one, gl3Entry_upperUnipotent3_mul_two] ring theorem outerMinor_upperUnipotent3_mul (x y z : v.adicCompletion β„š) (g : LocalGL3 v) : outerMinor v (upperUnipotent3 x y z * g) = outerMinor v g := by simp only [outerMinor, gl3Entry_upperUnipotent3_mul_one, gl3Entry_upperUnipotent3_mul_two] ring theorem gl3Det_upperUnipotent3_mul (x y z : v.adicCompletion β„š) (g : LocalGL3 v) : gl3Det v (upperUnipotent3 x y z * g) = gl3Det v g := by have h1 : Matrix.det !![(1 : v.adicCompletion β„š), x, z; 0, 1, y; 0, 0, 1] = 1 := by simp [Matrix.det_fin_three] rw [gl3Det, gl3Det, Units.val_mul, Matrix.det_mul, upperUnipotent3_coe, h1, one_mul] theorem cornerEntry_diagonal3_mul (a : Fin 3 β†’ (v.adicCompletion β„š)Λ£) (g : LocalGL3 v) : cornerEntry v (diagonal3 v a * g) = (a 2 : v.adicCompletion β„š) * cornerEntry v g := gl3Entry_diagonal3_mul v a g 2 0 theorem lowerMinor_diagonal3_mul (a : Fin 3 β†’ (v.adicCompletion β„š)Λ£) (g : LocalGL3 v) : lowerMinor v (diagonal3 v a * g) = ((a 1 : v.adicCompletion β„š) * a 2) * lowerMinor v g := by simp only [lowerMinor, gl3Entry_diagonal3_mul] ring theorem outerMinor_diagonal3_mul (a : Fin 3 β†’ (v.adicCompletion β„š)Λ£) (g : LocalGL3 v) : outerMinor v (diagonal3 v a * g) = ((a 1 : v.adicCompletion β„š) * a 2) * outerMinor v g := by simp only [outerMinor, gl3Entry_diagonal3_mul] ring theorem gl3Det_diagonal3_mul (a : Fin 3 β†’ (v.adicCompletion β„š)Λ£) (g : LocalGL3 v) : gl3Det v (diagonal3 v a * g) = ((a 0 : v.adicCompletion β„š) * a 1 * a 2) * gl3Det v g := by rw [gl3Det, gl3Det, Units.val_mul, Matrix.det_mul, diagonal3_coe, Matrix.det_diagonal, Fin.prod_univ_three] def cellRatio (g : LocalGL3 v) : Fin 3 β†’ v.adicCompletion β„š := ![gl3Entry v g 2 1 / cornerEntry v g, gl3Entry v g 2 2 / cornerEntry v g, outerMinor v g / lowerMinor v g] theorem cellRatio_upperUnipotent3_mul (x y z : v.adicCompletion β„š) (g : LocalGL3 v) : cellRatio v (upperUnipotent3 x y z * g) = cellRatio v g := by simp only [cellRatio, gl3Entry_upperUnipotent3_mul_two, cornerEntry_upperUnipotent3_mul, outerMinor_upperUnipotent3_mul, lowerMinor_upperUnipotent3_mul] theorem cellRatio_diagonal3_mul (a : Fin 3 β†’ (v.adicCompletion β„š)Λ£) (g : LocalGL3 v) : cellRatio v (diagonal3 v a * g) = cellRatio v g := by have h2 : (a 2 : v.adicCompletion β„š) β‰  0 := (a 2).ne_zero have h12 : (a 1 : v.adicCompletion β„š) * a 2 β‰  0 := mul_ne_zero (a 1).ne_zero h2 simp only [cellRatio, gl3Entry_diagonal3_mul, cornerEntry_diagonal3_mul, outerMinor_diagonal3_mul, lowerMinor_diagonal3_mul, mul_div_mul_left _ _ h2, mul_div_mul_left _ _ h12] def cellCutoff : Set (LocalGL3 v) := {g | cornerEntry v g β‰  0 ∧ lowerMinor v g β‰  0 ∧ βˆ€ i, Valued.v (cellRatio v g i) ≀ 1} theorem upperUnipotent3_mul_mem_cellCutoff_iff (x y z : v.adicCompletion β„š) (g : LocalGL3 v) : upperUnipotent3 x y z * g ∈ cellCutoff v ↔ g ∈ cellCutoff v := by simp only [cellCutoff, Set.mem_setOf_eq, cornerEntry_upperUnipotent3_mul, lowerMinor_upperUnipotent3_mul, cellRatio_upperUnipotent3_mul] theorem diagonal3_mul_mem_cellCutoff_iff (a : Fin 3 β†’ (v.adicCompletion β„š)Λ£) (g : LocalGL3 v) : diagonal3 v a * g ∈ cellCutoff v ↔ g ∈ cellCutoff v := by simp only [cellCutoff, Set.mem_setOf_eq, cornerEntry_diagonal3_mul, lowerMinor_diagonal3_mul, cellRatio_diagonal3_mul, ne_eq, mul_eq_zero, Units.ne_zero, false_or] def cellValue (Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) (g : LocalGL3 v) : β„‚ := charExt (Ο‡ 0) (gl3Det v g / lowerMinor v g) * charExt (Ο‡ 1) (lowerMinor v g / cornerEntry v g) * charExt (Ο‡ 2) (cornerEntry v g) * ((β€–gl3Det v g / lowerMinor v gβ€– / β€–cornerEntry v gβ€– : ℝ) : β„‚) def cellSection (Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) : LocalGL3 v β†’ β„‚ := (cellCutoff v).indicator (cellValue v Ο‡) theorem charExt_units_mul (Ο‡ : (v.adicCompletion β„š)Λ£ β†’* β„‚Λ£) (u : (v.adicCompletion β„š)Λ£) (x : v.adicCompletion β„š) : charExt Ο‡ ((u : v.adicCompletion β„š) * x) = (Ο‡ u : β„‚) * charExt Ο‡ x := by by_cases hx : x = 0 Β· simp [hx] Β· rw [charExt_of_ne_zero Ο‡ (mul_ne_zero u.ne_zero hx), charExt_of_ne_zero Ο‡ hx, show Units.mk0 ((u : v.adicCompletion β„š) * x) (mul_ne_zero u.ne_zero hx) = u * Units.mk0 x hx from Units.ext (by simp), map_mul, Units.val_mul] theorem cellValue_upperUnipotent3_mul (Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) (x y z : v.adicCompletion β„š) (g : LocalGL3 v) : cellValue v Ο‡ (upperUnipotent3 x y z * g) = cellValue v Ο‡ g := by simp only [cellValue, gl3Det_upperUnipotent3_mul, lowerMinor_upperUnipotent3_mul, cornerEntry_upperUnipotent3_mul] theorem cellValue_diagonal3_mul (Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) (a : Fin 3 β†’ (v.adicCompletion β„š)Λ£) (g : LocalGL3 v) : cellValue v Ο‡ (diagonal3 v a * g) = torusChar3 v Ο‡ a * halfModulus3 v a * cellValue v Ο‡ g := by have h2 : (a 2 : v.adicCompletion β„š) β‰  0 := (a 2).ne_zero have h12 : (a 1 : v.adicCompletion β„š) * a 2 β‰  0 := mul_ne_zero (a 1).ne_zero h2 have hdet : gl3Det v (diagonal3 v a * g) / lowerMinor v (diagonal3 v a * g) = (a 0 : v.adicCompletion β„š) * (gl3Det v g / lowerMinor v g) := by rw [gl3Det_diagonal3_mul, lowerMinor_diagonal3_mul, show (a 0 : v.adicCompletion β„š) * a 1 * a 2 * gl3Det v g = ((a 1 : v.adicCompletion β„š) * a 2) * (a 0 * gl3Det v g) by ring, mul_div_mul_left _ _ h12, mul_div_assoc] have hlow : lowerMinor v (diagonal3 v a * g) / cornerEntry v (diagonal3 v a * g) = (a 1 : v.adicCompletion β„š) * (lowerMinor v g / cornerEntry v g) := by rw [lowerMinor_diagonal3_mul, cornerEntry_diagonal3_mul, show (a 1 : v.adicCompletion β„š) * a 2 * lowerMinor v g = (a 2 : v.adicCompletion β„š) * (a 1 * lowerMinor v g) by ring, mul_div_mul_left _ _ h2, mul_div_assoc] unfold cellValue rw [hdet, hlow, cornerEntry_diagonal3_mul] simp only [charExt_units_mul, norm_mul, halfModulus3, torusChar3, Fin.prod_univ_three] push_cast ring theorem cellSection_upperUnipotent3_mul (Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) (x y z : v.adicCompletion β„š) (g : LocalGL3 v) : cellSection v Ο‡ (upperUnipotent3 x y z * g) = cellSection v Ο‡ g := by by_cases hg : g ∈ cellCutoff v Β· rw [cellSection, Set.indicator_of_mem (by rwa [upperUnipotent3_mul_mem_cellCutoff_iff]), Set.indicator_of_mem hg, cellValue_upperUnipotent3_mul] Β· rw [cellSection, Set.indicator_of_notMem (by rwa [upperUnipotent3_mul_mem_cellCutoff_iff]), Set.indicator_of_notMem hg] theorem cellSection_diagonal3_mul (Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) (a : Fin 3 β†’ (v.adicCompletion β„š)Λ£) (g : LocalGL3 v) : cellSection v Ο‡ (diagonal3 v a * g) = torusChar3 v Ο‡ a * halfModulus3 v a * cellSection v Ο‡ g := by by_cases hg : g ∈ cellCutoff v Β· rw [cellSection, Set.indicator_of_mem (by rwa [diagonal3_mul_mem_cellCutoff_iff]), Set.indicator_of_mem hg, cellValue_diagonal3_mul] Β· rw [cellSection, Set.indicator_of_notMem (by rwa [diagonal3_mul_mem_cellCutoff_iff]), Set.indicator_of_notMem hg, mul_zero] def antidiagonal3 : LocalGL3 v := Matrix.GeneralLinearGroup.mkOfDetNeZero !![(0 : v.adicCompletion β„š), 0, 1; 0, 1, 0; 1, 0, 0] (by simp [Matrix.det_fin_three]) theorem antidiagonal3_coe : (antidiagonal3 v : Matrix (Fin 3) (Fin 3) (v.adicCompletion β„š)) = !![(0 : v.adicCompletion β„š), 0, 1; 0, 1, 0; 1, 0, 0] := rfl theorem cornerEntry_antidiagonal3 : cornerEntry v (antidiagonal3 v) = 1 := by simp [cornerEntry, gl3Entry, antidiagonal3_coe] theorem lowerMinor_antidiagonal3 : lowerMinor v (antidiagonal3 v) = -1 := by simp [lowerMinor, gl3Entry, antidiagonal3_coe] theorem outerMinor_antidiagonal3 : outerMinor v (antidiagonal3 v) = 0 := by simp [outerMinor, gl3Entry, antidiagonal3_coe] theorem gl3Det_antidiagonal3 : gl3Det v (antidiagonal3 v) = -1 := by simp [gl3Det, antidiagonal3_coe, Matrix.det_fin_three] theorem antidiagonal3_mem_cellCutoff : antidiagonal3 v ∈ cellCutoff v := by refine ⟨?_, ?_, ?_⟩ Β· rw [cornerEntry_antidiagonal3] exact one_ne_zero Β· rw [lowerMinor_antidiagonal3] exact neg_ne_zero.mpr one_ne_zero Β· intro i fin_cases i <;> simp [cellRatio, gl3Entry, antidiagonal3_coe, cornerEntry_antidiagonal3, outerMinor_antidiagonal3] theorem cellValue_antidiagonal3 (Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) : cellValue v Ο‡ (antidiagonal3 v) = (Ο‡ 0 1 : β„‚) * (Ο‡ 1 (-1) : β„‚) * (Ο‡ 2 1 : β„‚) := by have h1 : charExt (Ο‡ 1) (-1 : v.adicCompletion β„š) = (Ο‡ 1 (-1) : β„‚) := by simpa using charExt_coe_units (Ο‡ 1) (-1) have h0 : charExt (Ο‡ 0) (1 : v.adicCompletion β„š) = (Ο‡ 0 1 : β„‚) := by simpa using charExt_coe_units (Ο‡ 0) 1 have h2 : charExt (Ο‡ 2) (1 : v.adicCompletion β„š) = (Ο‡ 2 1 : β„‚) := by simpa using charExt_coe_units (Ο‡ 2) 1 simp [cellValue, gl3Det_antidiagonal3, lowerMinor_antidiagonal3, cornerEntry_antidiagonal3, h0, h1, h2] theorem cellSection_antidiagonal3_ne_zero (Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) : cellSection v Ο‡ (antidiagonal3 v) β‰  0 := by rw [cellSection, Set.indicator_of_mem (antidiagonal3_mem_cellCutoff v), cellValue_antidiagonal3] exact mul_ne_zero (mul_ne_zero (Units.ne_zero _) (Units.ne_zero _)) (Units.ne_zero _) theorem cellSection_ne_zero (Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) : cellSection v Ο‡ β‰  0 := fun h => cellSection_antidiagonal3_ne_zero v Ο‡ (by rw [h]; rfl) end Witness section WitnessTopology open Filter Topology variable (v : HeightOneSpectrum (π“ž β„š)) theorem isClopen_valued_le_one : IsClopen {y : v.adicCompletion β„š | Valued.v y ≀ 1} := by exact Valued.isClopen_integer (v.adicCompletion β„š) theorem eventually_valued_eq {x : v.adicCompletion β„š} (hx : x β‰  0) : βˆ€αΆ  y in 𝓝 x, Valued.v y = Valued.v x := by have hvx : Valued.v x β‰  (0 : WithZero (Multiplicative β„€)) := (Valuation.ne_zero_iff _).mpr hx exact Valued.locally_const hvx theorem eventually_valued_lt {c : v.adicCompletion β„š} (hc : c β‰  0) : βˆ€αΆ  y in 𝓝 (0 : v.adicCompletion β„š), Valued.v y < Valued.v c := by have hvc : Valued.v c β‰  0 := (Valuation.ne_zero_iff _).mpr hc rw [Filter.Eventually, Valued.mem_nhds_zero] refine ⟨Units.mk0 (Valued.v.restrict c) ((Valuation.ne_zero_iff _).mpr hc), fun y hy => ?_⟩ exact (Valuation.restrict_lt_iff _).mp hy theorem eventually_norm_eq {x : v.adicCompletion β„š} (hx : x β‰  0) : βˆ€αΆ  y in 𝓝 x, β€–yβ€– = β€–xβ€– := by filter_upwards [eventually_valued_eq v hx] with y hy rw [NumberField.FinitePlace.norm_def, NumberField.FinitePlace.norm_def, hy] theorem eventually_charExt_eq (Ο‡ : (v.adicCompletion β„š)Λ£ β†’* β„‚Λ£) (hΟ‡ : IsLocallyConstant Ο‡) {x : v.adicCompletion β„š} (hx : x β‰  0) : βˆ€αΆ  y in 𝓝 x, charExt Ο‡ y = charExt Ο‡ x := by obtain ⟨U, hU, hUF⟩ := Units.isEmbedding_valβ‚€.toIsInducing.isOpen_iff.mp (hΟ‡.isOpen_fiber (Ο‡ (Units.mk0 x hx))) have hxU : x ∈ U := by have : Units.mk0 x hx ∈ (Units.val ⁻¹' U : Set (v.adicCompletion β„š)Λ£) := by rw [hUF] exact rfl simpa using this filter_upwards [hU.mem_nhds hxU, eventually_ne_nhds hx] with y hyU hy0 have hyF : Units.mk0 y hy0 ∈ (Units.val ⁻¹' U : Set (v.adicCompletion β„š)Λ£) := by simpa using hyU rw [hUF] at hyF rw [charExt_of_ne_zero Ο‡ hy0, charExt_of_ne_zero Ο‡ hx] exact congrArg Units.val hyF theorem eventually_mem_iff_of_isClopen {s : Set (v.adicCompletion β„š)} (hs : IsClopen s) (x : v.adicCompletion β„š) : βˆ€αΆ  y in 𝓝 x, (y ∈ s ↔ x ∈ s) := by by_cases hx : x ∈ s Β· filter_upwards [hs.isOpen.mem_nhds hx] with y hy exact iff_of_true hy hx Β· filter_upwards [hs.isClosed.isOpen_compl.mem_nhds hx] with y hy exact iff_of_false hy hx theorem continuous_gl3Entry (i j : Fin 3) : Continuous fun g : LocalGL3 v => gl3Entry v g i j := Units.continuous_val.matrix_elem i j theorem continuous_cornerEntry : Continuous (cornerEntry v) := continuous_gl3Entry v 2 0 theorem continuous_lowerMinor : Continuous (lowerMinor v) := ((continuous_gl3Entry v 1 0).mul (continuous_gl3Entry v 2 1)).sub ((continuous_gl3Entry v 1 1).mul (continuous_gl3Entry v 2 0)) theorem continuous_outerMinor : Continuous (outerMinor v) := ((continuous_gl3Entry v 1 0).mul (continuous_gl3Entry v 2 2)).sub ((continuous_gl3Entry v 1 2).mul (continuous_gl3Entry v 2 0)) theorem continuous_gl3Det : Continuous (gl3Det v) := Units.continuous_val.matrix_det theorem gl3Det_eq_bottom_expansion (g : LocalGL3 v) : gl3Det v g = gl3Entry v g 2 0 * (gl3Entry v g 0 1 * gl3Entry v g 1 2 - gl3Entry v g 0 2 * gl3Entry v g 1 1) - gl3Entry v g 2 1 * (gl3Entry v g 0 0 * gl3Entry v g 1 2 - gl3Entry v g 0 2 * gl3Entry v g 1 0) + gl3Entry v g 2 2 * (gl3Entry v g 0 0 * gl3Entry v g 1 1 - gl3Entry v g 0 1 * gl3Entry v g 1 0) := by simp only [gl3Det, gl3Entry, Matrix.det_fin_three] ring theorem cornerEntry_mul_gl3Det (g : LocalGL3 v) : cornerEntry v g * gl3Det v g = (gl3Entry v g 0 0 * gl3Entry v g 2 1 - gl3Entry v g 0 1 * cornerEntry v g) * outerMinor v g + (gl3Entry v g 0 2 * cornerEntry v g - gl3Entry v g 0 0 * gl3Entry v g 2 2) * lowerMinor v g := by simp only [gl3Det, gl3Entry, cornerEntry, outerMinor, lowerMinor, Matrix.det_fin_three] ring theorem exists_bottom_entry_ne_zero_of_cornerEntry_eq_zero {g : LocalGL3 v} (hc : cornerEntry v g = 0) : gl3Entry v g 2 1 β‰  0 ∨ gl3Entry v g 2 2 β‰  0 := by by_contra h push Not at h apply gl3Det_ne_zero v g rw [gl3Det_eq_bottom_expansion, h.1, h.2] have hc' : gl3Entry v g 2 0 = 0 := hc rw [hc'] ring theorem outerMinor_ne_zero_of_lowerMinor_eq_zero {g : LocalGL3 v} (hc : cornerEntry v g β‰  0) (hl : lowerMinor v g = 0) : outerMinor v g β‰  0 := by intro ho apply gl3Det_ne_zero v g have h := cornerEntry_mul_gl3Det v g rw [ho, hl, mul_zero, mul_zero, add_zero] at h exact (mul_eq_zero.mp h).resolve_left hc theorem eventually_one_lt_valued_div {n d : LocalGL3 v β†’ v.adicCompletion β„š} {g : LocalGL3 v} (hn : Continuous n) (hd : Continuous d) (hng : n g β‰  0) (hdg : d g = 0) : βˆ€αΆ  h in 𝓝 g, d h β‰  0 β†’ 1 < Valued.v (n h / d h) := by have h1 : βˆ€αΆ  h in 𝓝 g, Valued.v (n h) = Valued.v (n g) := (hn.tendsto g).eventually (eventually_valued_eq v hng) have h2 : βˆ€αΆ  h in 𝓝 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 eventually_cellSection_eq_zero_of_den {Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)} {g : LocalGL3 v} {n d : LocalGL3 v β†’ v.adicCompletion β„š} (i : Fin 3) (hn : Continuous n) (hd : Continuous d) (hng : n g β‰  0) (hdg : d g = 0) (hratio : βˆ€ h, cellRatio v h i = n h / d h) (hden : βˆ€ h, h ∈ cellCutoff v β†’ d h β‰  0) : βˆ€αΆ  h in 𝓝 g, cellSection v Ο‡ h = cellSection v Ο‡ g := by have hg : g βˆ‰ cellCutoff v := fun hmem => hden g hmem hdg filter_upwards [eventually_one_lt_valued_div v hn hd hng hdg] with h hh have hh' : h βˆ‰ cellCutoff v := by intro hmem have hi := hmem.2.2 i rw [hratio] at hi exact absurd hi (not_le.mpr (hh (hden h hmem))) simp only [cellSection, Set.indicator_of_notMem hh', Set.indicator_of_notMem hg] theorem isLocallyConstant_cellSection (Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) (hΟ‡ : βˆ€ i, IsLocallyConstant (Ο‡ i)) : IsLocallyConstant (cellSection v Ο‡) := by rw [IsLocallyConstant.iff_eventually_eq] intro g by_cases hc : cornerEntry v g = 0 Β· rcases exists_bottom_entry_ne_zero_of_cornerEntry_eq_zero v hc with h21 | h22 Β· exact eventually_cellSection_eq_zero_of_den v 0 (continuous_gl3Entry v 2 1) (continuous_cornerEntry v) h21 hc (fun h => rfl) (fun h hh => hh.1) Β· exact eventually_cellSection_eq_zero_of_den v 1 (continuous_gl3Entry v 2 2) (continuous_cornerEntry v) h22 hc (fun h => rfl) (fun h hh => hh.1) by_cases hl : lowerMinor v g = 0 Β· exact eventually_cellSection_eq_zero_of_den v 2 (continuous_outerMinor v) (continuous_lowerMinor v) (outerMinor_ne_zero_of_lowerMinor_eq_zero v hc hl) hl (fun h => rfl) (fun h hh => hh.2.1) have hcA : ContinuousAt (cornerEntry v) g := (continuous_cornerEntry v).continuousAt have hlA : ContinuousAt (lowerMinor v) g := (continuous_lowerMinor v).continuousAt have hdA : ContinuousAt (gl3Det v) g := (continuous_gl3Det v).continuousAt have hr : βˆ€ i, ContinuousAt (fun h => cellRatio v h i) g := by intro i fin_cases i Β· exact ((continuous_gl3Entry v 2 1).continuousAt).div hcA hc Β· exact ((continuous_gl3Entry v 2 2).continuousAt).div hcA hc Β· exact ((continuous_outerMinor v).continuousAt).div hlA hl have hmem : βˆ€αΆ  h in 𝓝 g, (h ∈ cellCutoff v ↔ g ∈ cellCutoff v) := by have hc' : βˆ€αΆ  h in 𝓝 g, cornerEntry v h β‰  0 := hcA.eventually_ne hc have hl' : βˆ€αΆ  h in 𝓝 g, lowerMinor v h β‰  0 := hlA.eventually_ne hl have hr' : βˆ€αΆ  h in 𝓝 g, βˆ€ i, (Valued.v (cellRatio v h i) ≀ 1 ↔ Valued.v (cellRatio v g i) ≀ 1) := eventually_all.mpr fun i => (hr i).eventually (eventually_mem_iff_of_isClopen v (isClopen_valued_le_one v) (cellRatio v g i)) filter_upwards [hc', hl', hr'] with h hch hlh hrh simp only [cellCutoff, Set.mem_setOf_eq, hch, hc, hlh, hl, ne_eq, not_false_eq_true, true_and] exact forall_congr' hrh have hval : βˆ€αΆ  h in 𝓝 g, cellValue v Ο‡ h = cellValue v Ο‡ g := by have hq0 : gl3Det v g / lowerMinor v g β‰  0 := div_ne_zero (gl3Det_ne_zero v g) hl have hq1 : lowerMinor v g / cornerEntry v g β‰  0 := div_ne_zero hl hc have e0 : βˆ€αΆ  h in nhds g, charExt (Ο‡ 0) (gl3Det v h / lowerMinor v h) = charExt (Ο‡ 0) (gl3Det v g / lowerMinor v g) := (hdA.div hlA hl).eventually (eventually_charExt_eq v (Ο‡ 0) (hΟ‡ 0) hq0) have e1 : βˆ€αΆ  h in nhds g, charExt (Ο‡ 1) (lowerMinor v h / cornerEntry v h) = charExt (Ο‡ 1) (lowerMinor v g / cornerEntry v g) := (hlA.div hcA hc).eventually (eventually_charExt_eq v (Ο‡ 1) (hΟ‡ 1) hq1) have e2 : βˆ€αΆ  h in nhds g, charExt (Ο‡ 2) (cornerEntry v h) = charExt (Ο‡ 2) (cornerEntry v g) := hcA.eventually (eventually_charExt_eq v (Ο‡ 2) (hΟ‡ 2) hc) have e3 : βˆ€αΆ  h in nhds g, β€–gl3Det v h / lowerMinor v hβ€– = β€–gl3Det v g / lowerMinor v gβ€– := (hdA.div hlA hl).eventually (eventually_norm_eq v hq0) have e4 : βˆ€αΆ  h in nhds g, β€–cornerEntry v hβ€– = β€–cornerEntry v gβ€– := hcA.eventually (eventually_norm_eq v hc) filter_upwards [e0, e1, e2, e3, e4] with h h0 h1 h2 h3 h4 simp only [cellValue, h0, h1, h2, h3, h4] filter_upwards [hmem, hval] with h h1 h2 by_cases hgS : g ∈ cellCutoff v Β· rw [cellSection, Set.indicator_of_mem (h1.mpr hgS), Set.indicator_of_mem hgS, h2] Β· rw [cellSection, Set.indicator_of_notMem (fun hh => hgS (h1.mp hh)), Set.indicator_of_notMem hgS] theorem cellSection_mem_principalSeries3 (Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) (hΟ‡ : βˆ€ i, IsLocallyConstant (Ο‡ i)) : cellSection v Ο‡ ∈ principalSeries3 v Ο‡ := ⟨isLocallyConstant_cellSection v Ο‡ hΟ‡, cellSection_upperUnipotent3_mul v Ο‡, cellSection_diagonal3_mul v Ο‡βŸ© def cellVector (Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) (hΟ‡ : βˆ€ i, IsLocallyConstant (Ο‡ i)) : β†₯(principalSeries3 v Ο‡) := ⟨cellSection v Ο‡, cellSection_mem_principalSeries3 v Ο‡ hΟ‡βŸ© def evalAntidiagonal3 (Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) : β†₯(principalSeries3 v Ο‡) β†’β‚—[β„‚] β„‚ := (LinearMap.proj (antidiagonal3 v) : (LocalGL3 v β†’ β„‚) β†’β‚—[β„‚] β„‚).comp (principalSeries3 v Ο‡).subtype theorem coefficientFn_evalAntidiagonal3_cellVector_one (Ο‡ : Fin 3 β†’ ((v.adicCompletion β„š)Λ£ β†’* β„‚Λ£)) (hΟ‡ : βˆ€ i, IsLocallyConstant (Ο‡ i)) : coefficientFn (evalAntidiagonal3 v Ο‡) (cellVector v Ο‡ hΟ‡) 1 β‰  0 := by have : coefficientFn (evalAntidiagonal3 v Ο‡) (cellVector v Ο‡ hΟ‡) 1 = cellSection v Ο‡ (antidiagonal3 v) := by simp [coefficientFn, evalAntidiagonal3, cellVector, gl3AmbientRightTranslate] rw [this] exact cellSection_antidiagonal3_ne_zero v Ο‡ end WitnessTopology end LanglandsTunnell.CubicInduction end