import Definitions.Def_AutomorphicForm_ArchDerivCasimir set_option autoImplicit false noncomputable section namespace AutomorphicForm open NumberField NumberField.InfinitePlace.Completion Matrix Complex variable (F : Type) [Field F] [NumberField F] section ComplexPlaceTransport variable {F} def archComplexGLAt {w : InfinitePlace F} (hw : w.IsComplex) : GL (Fin 2) β„‚ β†’* AdelicGL2 (π“ž F) F := (adelicArchGLInclAt F w).comp (glEquivOfRingEquiv (ringEquivComplexOfIsComplex hw).symm).toMonoidHom def archComplexLiftAt {w : InfinitePlace F} (hw : w.IsComplex) (e : Fin 2 β†’ Fin 2 β†’ β„‚) : AdelicGL2 (π“ž F) F := if h : (Matrix.of e).det β‰  0 then archComplexGLAt hw (GeneralLinearGroup.mkOfDetNeZero (Matrix.of e) h) else 1 theorem archComplexLiftAt_of_det_ne_zero {w : InfinitePlace F} (hw : w.IsComplex) {e : Fin 2 β†’ Fin 2 β†’ β„‚} (h : (Matrix.of e).det β‰  0) : archComplexLiftAt hw e = archComplexGLAt hw (GeneralLinearGroup.mkOfDetNeZero (Matrix.of e) h) := dif_pos h theorem isOpen_setOf_det_ne_zero_complex : IsOpen {e : Fin 2 β†’ Fin 2 β†’ β„‚ | (Matrix.of e).det β‰  0} := (isClosed_singleton.preimage (continuous_id.matrix_det)).isOpen_compl def IsArchSmoothAtComplex {w : InfinitePlace F} (hw : w.IsComplex) (Ο† : AdelicGL2 (π“ž F) F β†’ β„‚) : Prop := βˆ€ g : AdelicGL2 (π“ž F) F, ContDiffOn ℝ (⊀ : β„•βˆž) (fun e : Fin 2 β†’ Fin 2 β†’ β„‚ => Ο† (g * archComplexLiftAt hw e)) {e | (Matrix.of e).det β‰  0} theorem isArchSmoothAtComplex_const {w : InfinitePlace F} (hw : w.IsComplex) (c : β„‚) : IsArchSmoothAtComplex hw (fun _ => c) := fun _ => contDiffOn_const end ComplexPlaceTransport section ComplexFlows variable {F} inductive ArchDirComplex where | H : ArchDirComplex | E : ArchDirComplex | Fm : ArchDirComplex | iH : ArchDirComplex | iE : ArchDirComplex | iFm : ArchDirComplex def ArchDir.toComplex : ArchDir β†’ ArchDirComplex | .H => .H | .E => .E | .Fm => .Fm def ArchDir.toComplexI : ArchDir β†’ ArchDirComplex | .H => .iH | .E => .iE | .Fm => .iFm def splitTorusGL2Complex (z : β„‚) : GL (Fin 2) β„‚ where val := !![Complex.exp z, 0; 0, Complex.exp (-z)] inv := !![Complex.exp (-z), 0; 0, Complex.exp z] val_inv := by ext i j; fin_cases i <;> fin_cases j <;> simp [Matrix.mul_apply, Fin.sum_univ_two, ← Complex.exp_add] inv_val := by ext i j; fin_cases i <;> fin_cases j <;> simp [Matrix.mul_apply, Fin.sum_univ_two, ← Complex.exp_add] theorem splitTorusGL2Complex_zero : splitTorusGL2Complex 0 = 1 := by ext i j; fin_cases i <;> fin_cases j <;> simp [splitTorusGL2Complex] theorem splitTorusGL2Complex_add (z z' : β„‚) : splitTorusGL2Complex (z + z') = splitTorusGL2Complex z * splitTorusGL2Complex z' := by ext i j; fin_cases i <;> fin_cases j <;> simp [splitTorusGL2Complex, Matrix.mul_apply, Fin.sum_univ_two, Complex.exp_add]; ring_nf def archFlowMatrixComplex : ArchDirComplex β†’ ℝ β†’ GL (Fin 2) β„‚ | .H, t => splitTorusGL2Complex (t : β„‚) | .E, t => unipotentGL2 (t : β„‚) | .Fm, t => lowerUnipotentGL2 (t : β„‚) | .iH, t => splitTorusGL2Complex ((t : β„‚) * I) | .iE, t => unipotentGL2 ((t : β„‚) * I) | .iFm, t => lowerUnipotentGL2 ((t : β„‚) * I) theorem archFlowMatrixComplex_zero (d : ArchDirComplex) : archFlowMatrixComplex d 0 = 1 := by cases d Β· simpa [archFlowMatrixComplex] using splitTorusGL2Complex_zero Β· simp [archFlowMatrixComplex, unipotentGL2_zero] Β· simp [archFlowMatrixComplex, lowerUnipotentGL2_zero] Β· simpa [archFlowMatrixComplex] using splitTorusGL2Complex_zero Β· simp [archFlowMatrixComplex, unipotentGL2_zero] Β· simp [archFlowMatrixComplex, lowerUnipotentGL2_zero] theorem archFlowMatrixComplex_add (d : ArchDirComplex) (s t : ℝ) : archFlowMatrixComplex d (s + t) = archFlowMatrixComplex d s * archFlowMatrixComplex d t := by cases d Β· simp [archFlowMatrixComplex, ← splitTorusGL2Complex_add] Β· simp [archFlowMatrixComplex, ← unipotentGL2_add] Β· simp [archFlowMatrixComplex, ← lowerUnipotentGL2_add] Β· simp [archFlowMatrixComplex, ← splitTorusGL2Complex_add, add_mul] Β· simp [archFlowMatrixComplex, ← unipotentGL2_add, add_mul] Β· simp [archFlowMatrixComplex, ← lowerUnipotentGL2_add, add_mul] def archFlowAtComplex {w : InfinitePlace F} (hw : w.IsComplex) (d : ArchDirComplex) (t : ℝ) : AdelicGL2 (π“ž F) F := archComplexGLAt hw (archFlowMatrixComplex d t) theorem archFlowAtComplex_zero {w : InfinitePlace F} (hw : w.IsComplex) (d : ArchDirComplex) : archFlowAtComplex hw d 0 = 1 := by rw [archFlowAtComplex, archFlowMatrixComplex_zero, map_one] theorem archFlowAtComplex_add {w : InfinitePlace F} (hw : w.IsComplex) (d : ArchDirComplex) (s t : ℝ) : archFlowAtComplex hw d (s + t) = archFlowAtComplex hw d s * archFlowAtComplex hw d t := by rw [archFlowAtComplex, archFlowMatrixComplex_add, map_mul]; rfl def archDerivAtComplex {w : InfinitePlace F} (hw : w.IsComplex) (d : ArchDirComplex) (Ο† : AdelicGL2 (π“ž F) F β†’ β„‚) : AdelicGL2 (π“ž F) F β†’ β„‚ := fun g => deriv (fun t : ℝ => Ο† (g * archFlowAtComplex hw d t)) 0 def archDelAt {w : InfinitePlace F} (hw : w.IsComplex) (d : ArchDir) (Ο† : AdelicGL2 (π“ž F) F β†’ β„‚) : AdelicGL2 (π“ž F) F β†’ β„‚ := (1 / 2 : β„‚) β€’ (archDerivAtComplex hw d.toComplex Ο† - I β€’ archDerivAtComplex hw d.toComplexI Ο†) def archDelBarAt {w : InfinitePlace F} (hw : w.IsComplex) (d : ArchDir) (Ο† : AdelicGL2 (π“ž F) F β†’ β„‚) : AdelicGL2 (π“ž F) F β†’ β„‚ := (1 / 2 : β„‚) β€’ (archDerivAtComplex hw d.toComplex Ο† + I β€’ archDerivAtComplex hw d.toComplexI Ο†) def archCasimirAtComplex {w : InfinitePlace F} (hw : w.IsComplex) (Ο† : AdelicGL2 (π“ž F) F β†’ β„‚) : AdelicGL2 (π“ž F) F β†’ β„‚ := -((1 / 4 : β„‚) β€’ archDelAt hw .H (archDelAt hw .H Ο†) - (1 / 2 : β„‚) β€’ archDelAt hw .H Ο† + archDelAt hw .E (archDelAt hw .Fm Ο†)) def archCasimirBarAtComplex {w : InfinitePlace F} (hw : w.IsComplex) (Ο† : AdelicGL2 (π“ž F) F β†’ β„‚) : AdelicGL2 (π“ž F) F β†’ β„‚ := -((1 / 4 : β„‚) β€’ archDelBarAt hw .H (archDelBarAt hw .H Ο†) - (1 / 2 : β„‚) β€’ archDelBarAt hw .H Ο† + archDelBarAt hw .E (archDelBarAt hw .Fm Ο†)) def archKCasimirAtComplex {w : InfinitePlace F} (hw : w.IsComplex) (Ο† : AdelicGL2 (π“ž F) F β†’ β„‚) : AdelicGL2 (π“ž F) F β†’ β„‚ := archDerivAtComplex hw .iH (archDerivAtComplex hw .iH Ο†) + (archDerivAtComplex hw .E (archDerivAtComplex hw .E Ο† - archDerivAtComplex hw .Fm Ο†) - archDerivAtComplex hw .Fm (archDerivAtComplex hw .E Ο† - archDerivAtComplex hw .Fm Ο†)) + (archDerivAtComplex hw .iE (archDerivAtComplex hw .iE Ο† + archDerivAtComplex hw .iFm Ο†) + archDerivAtComplex hw .iFm (archDerivAtComplex hw .iE Ο† + archDerivAtComplex hw .iFm Ο†)) theorem archDerivAtComplex_const {w : InfinitePlace F} (hw : w.IsComplex) (d : ArchDirComplex) (c : β„‚) : archDerivAtComplex hw d (fun _ => c) = fun _ => 0 := by funext g; simp [archDerivAtComplex] theorem archDelAt_const {w : InfinitePlace F} (hw : w.IsComplex) (d : ArchDir) (c : β„‚) : archDelAt hw d (fun _ => c) = fun _ => 0 := by funext g; simp [archDelAt, archDerivAtComplex_const] theorem archDelBarAt_const {w : InfinitePlace F} (hw : w.IsComplex) (d : ArchDir) (c : β„‚) : archDelBarAt hw d (fun _ => c) = fun _ => 0 := by funext g; simp [archDelBarAt, archDerivAtComplex_const] theorem archCasimirAtComplex_const {w : InfinitePlace F} (hw : w.IsComplex) (c : β„‚) : archCasimirAtComplex hw (fun _ => c) = fun _ => 0 := by funext g simp [archCasimirAtComplex, archDelAt_const] theorem archCasimirBarAtComplex_const {w : InfinitePlace F} (hw : w.IsComplex) (c : β„‚) : archCasimirBarAtComplex hw (fun _ => c) = fun _ => 0 := by funext g simp [archCasimirBarAtComplex, archDelBarAt_const] end ComplexFlows section Circle variable {F} def circleGL2 (ΞΆ : β„‚Λ£) : GL (Fin 2) β„‚ where val := !![(ΞΆ : β„‚), 0; 0, ((΢⁻¹ : β„‚Λ£) : β„‚)] inv := !![((΢⁻¹ : β„‚Λ£) : β„‚), 0; 0, (ΞΆ : β„‚)] 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] def archCircleAt {w : InfinitePlace F} (hw : w.IsComplex) (ΞΆ : β„‚Λ£) : AdelicGL2 (π“ž F) F := archComplexGLAt hw (circleGL2 ΞΆ) def HasCircleWeightAt {w : InfinitePlace F} (hw : w.IsComplex) (m : β„€) (Ο† : AdelicGL2 (π“ž F) F β†’ β„‚) : Prop := βˆ€ (ΞΆ : β„‚Λ£), β€–(ΞΆ : β„‚)β€– = 1 β†’ βˆ€ g : AdelicGL2 (π“ž F) F, Ο† (g * archCircleAt hw ΞΆ) = (ΞΆ : β„‚) ^ m * Ο† g theorem hasCircleWeightAt_zero {w : InfinitePlace F} (hw : w.IsComplex) (m : β„€) : HasCircleWeightAt hw m (fun _ => (0 : β„‚)) := fun _ _ _ => by simp end Circle end AutomorphicForm end