Skip to content

Commit aa6352e

Browse files
kbuzzardkbuzzard
committed
Merge branch 'main' of github.com:ImperialCollegeLondon/FLT
2 parents b208a30 + b4815e2 commit aa6352e

25 files changed

+2101
-272
lines changed

‎.github/workflows/push.yml

+6-6
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ jobs:
2929
name: Build project
3030
steps:
3131
- name: Checkout project
32-
uses: actions/checkout@v2
32+
uses: actions/checkout@v4
3333
with:
3434
fetch-depth: 0
3535

@@ -43,7 +43,7 @@ jobs:
4343
run: ~/.elan/bin/lake build FLT
4444

4545
- name: Cache mathlib docs
46-
uses: actions/cache@v3
46+
uses: actions/cache@v4
4747
with:
4848
path: |
4949
.lake/build/doc/Init
@@ -88,7 +88,7 @@ jobs:
8888
run: |
8989
sudo chown -R runner docs
9090
cp -r .lake/build/doc docs/docs
91-
91+
9292
- name: Bundle dependencies
9393
uses: ruby/setup-ruby@v1
9494
with:
@@ -101,18 +101,18 @@ jobs:
101101
run: JEKYLL_ENV=production bundle exec jekyll build
102102

103103
- name: Upload docs & blueprint artifact
104-
uses: actions/upload-pages-artifact@v1
104+
uses: actions/upload-pages-artifact@v3
105105
with:
106106
path: docs/
107107

108108
- name: Upload docs & blueprint artifact
109-
uses: actions/upload-pages-artifact@v1
109+
uses: actions/upload-pages-artifact@v3
110110
with:
111111
path: docs/_site
112112

113113
- name: Deploy to GitHub Pages
114114
id: deployment
115-
uses: actions/deploy-pages@v1
115+
uses: actions/deploy-pages@v4
116116

117117
- name: Make sure the cache works
118118
run: |

‎.github/workflows/push_pr.yml

+2-2
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ jobs:
77
name: Build project
88
steps:
99
- name: Checkout project
10-
uses: actions/checkout@v2
10+
uses: actions/checkout@v4
1111
with:
1212
fetch-depth: 0
1313

@@ -18,4 +18,4 @@ jobs:
1818
run: ~/.elan/bin/lake exe cache get
1919

2020
- name: Build project
21-
run: ~/.elan/bin/lake build FLT
21+
run: ~/.elan/bin/lake build FLT

‎FLT/AutomorphicForm/QuaternionAlgebra.lean

+210
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,210 @@
1+
/-
2+
Copyright (c) 2024 Kevin Buzzard. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Kevin Buzzard, Ludwig Monnerjahn, Hannah Scholz
5+
-/
6+
import Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
7+
import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
8+
import Mathlib.NumberTheory.NumberField.Basic
9+
import Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
10+
import Mathlib.Algebra.Group.Subgroup.Pointwise
11+
import FLT.HIMExperiments.module_topology
12+
13+
/-
14+
15+
# Definition of automorphic forms on a totally definite quaternion algebra
16+
-/
17+
18+
suppress_compilation
19+
20+
variable (F : Type*) [Field F] [NumberField F]
21+
22+
variable (D : Type*) [Ring D] [Algebra F D] [FiniteDimensional F D]
23+
24+
open DedekindDomain
25+
26+
open scoped NumberField
27+
28+
-- my work (two PRs)
29+
instance : TopologicalSpace (FiniteAdeleRing (𝓞 F) F) := sorry
30+
instance : TopologicalRing (FiniteAdeleRing (𝓞 F) F) := sorry
31+
32+
open scoped TensorProduct
33+
34+
section missing_instances
35+
36+
variable {R D A : Type*} [CommRing R] [Ring D] [CommRing A] [Algebra R D] [Algebra R A]
37+
38+
instance : Algebra A (D ⊗[R] A) :=
39+
Algebra.TensorProduct.includeRight.toRingHom.toAlgebra' (by
40+
simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, Algebra.TensorProduct.includeRight_apply]
41+
intro a b
42+
apply TensorProduct.induction_on (motive := fun b ↦ 1 ⊗ₜ[R] a * b = b * 1 ⊗ₜ[R] a)
43+
. simp only [mul_zero, zero_mul]
44+
. intro d a'
45+
simp only [Algebra.TensorProduct.tmul_mul_tmul, one_mul, mul_one]
46+
rw [NonUnitalCommSemiring.mul_comm]
47+
. intro x y hx hy
48+
rw [left_distrib, hx, hy, right_distrib]
49+
)
50+
51+
instance [Module.Finite R D] : Module.Finite A (D ⊗[R] A) := sorry
52+
instance [Module.Free R D] : Module.Free A (D ⊗[R] A) := sorry
53+
54+
-- #synth Ring (D ⊗[F] FiniteAdeleRing (𝓞 F) F)
55+
56+
end missing_instances
57+
-- your work
58+
instance : TopologicalSpace (D ⊗[F] (FiniteAdeleRing (𝓞 F) F)) := Module.topology (FiniteAdeleRing (𝓞 F) F)
59+
instance : TopologicalRing (D ⊗[F] (FiniteAdeleRing (𝓞 F) F)) := moobar (FiniteAdeleRing (𝓞 F) F) (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))
60+
61+
namespace TotallyDefiniteQuaternionAlgebra
62+
63+
noncomputable example : D →+* (D ⊗[F] FiniteAdeleRing (𝓞 F) F) := by exact
64+
Algebra.TensorProduct.includeLeftRingHom
65+
66+
abbrev Dfx := (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ
67+
noncomputable abbrev incl : Dˣ →* Dfx F D := Units.map Algebra.TensorProduct.includeLeftRingHom.toMonoidHom
68+
69+
structure AutomorphicForm (M : Type*) [AddCommGroup M] where
70+
toFun : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ → M
71+
left_invt : ∀ (d : Dˣ) (x : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ),
72+
toFun (Units.map Algebra.TensorProduct.includeLeftRingHom.toMonoidHom d * x) = toFun x
73+
loc_cst : ∃ U : Subgroup (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ,
74+
IsOpen (U : Set (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ) ∧
75+
∀ (x : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ),
76+
∀ u ∈ U, toFun (x * u) = toFun x
77+
78+
namespace AutomorphicForm
79+
80+
variable {M : Type*} [AddCommGroup M]
81+
82+
variable {F D}
83+
84+
instance : CoeFun (AutomorphicForm F D M) (fun _ ↦ Dfx F D → M) where
85+
coe := toFun
86+
87+
attribute [coe] AutomorphicForm.toFun
88+
89+
@[ext]
90+
lemma ext (φ ψ : AutomorphicForm F D M) (h : ∀ x, φ x = ψ x) : φ = ψ := by
91+
cases φ; cases ψ; simp only [mk.injEq]; ext; apply h
92+
93+
def zero : (AutomorphicForm F D M) where
94+
toFun := 0
95+
left_invt := by simp
96+
loc_cst := by use ⊤; simp
97+
98+
instance : Zero (AutomorphicForm F D M) where
99+
zero := zero
100+
101+
@[simp]
102+
lemma zero_apply (x : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ) :
103+
(0 : AutomorphicForm F D M) x = 0 := rfl
104+
105+
def neg (φ : AutomorphicForm F D M) : AutomorphicForm F D M where
106+
toFun x := - φ x
107+
left_invt := by
108+
intro d x
109+
simp only [RingHom.toMonoidHom_eq_coe, neg_inj]
110+
exact φ.left_invt d x
111+
loc_cst := by
112+
rcases φ.loc_cst with ⟨U, openU, hU⟩
113+
use U
114+
exact ⟨openU, fun x u umem ↦ by rw [neg_inj]; exact hU x u umem⟩
115+
116+
instance : Neg (AutomorphicForm F D M) where
117+
neg := neg
118+
119+
@[simp, norm_cast]
120+
lemma neg_apply (φ : AutomorphicForm F D M) (x : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ) :
121+
(-φ : AutomorphicForm F D M) x = -(φ x) := rfl
122+
123+
instance add (φ ψ : AutomorphicForm F D M) : AutomorphicForm F D M where
124+
toFun x := φ x + ψ x
125+
left_invt := by
126+
intro d x
127+
simp only [← φ.left_invt d x, ← ψ.left_invt d x]
128+
loc_cst := by
129+
rcases φ.loc_cst with ⟨U, openU, hU⟩
130+
rcases ψ.loc_cst with ⟨V, openV, hV⟩
131+
use U ⊓ V
132+
constructor
133+
· unfold Subgroup.instInf Submonoid.instInf
134+
simp only [Subgroup.coe_toSubmonoid, Subgroup.coe_set_mk]
135+
exact IsOpen.inter openU openV
136+
· intro x u ⟨umemU, umemV⟩
137+
simp only
138+
rw [hU x u umemU, hV x u umemV]
139+
140+
instance : Add (AutomorphicForm F D M) where
141+
add := add
142+
143+
@[simp, norm_cast]
144+
lemma add_apply (φ ψ : AutomorphicForm F D M) (x : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ) :
145+
(φ + ψ) x = (φ x) + (ψ x) := rfl
146+
147+
instance addCommGroup : AddCommGroup (AutomorphicForm F D M) where
148+
add := (· + ·)
149+
add_assoc := by intros; ext; simp [add_assoc];
150+
zero := 0
151+
zero_add := by intros; ext; simp
152+
add_zero := by intros; ext; simp
153+
nsmul := nsmulRec
154+
neg := (-·)
155+
zsmul := zsmulRec
156+
add_left_neg := by intros; ext; simp
157+
add_comm := by intros; ext; simp [add_comm]
158+
159+
open ConjAct
160+
open scoped Pointwise
161+
162+
lemma conjAct_mem {G: Type*} [Group G] (U: Subgroup G) (g: G) (x : G):
163+
x ∈ toConjAct g • U ↔ ∃ u ∈ U, g * u * g⁻¹ = x := by rfl
164+
165+
lemma toConjAct_open {G : Type*} [Group G] [TopologicalSpace G] [TopologicalGroup G]
166+
(U : Subgroup G) (hU : IsOpen (U : Set G)) (g : G) : IsOpen (toConjAct g • U : Set G) := by
167+
have this1 := continuous_mul_left g⁻¹
168+
have this2 := continuous_mul_right g
169+
rw [continuous_def] at this1 this2
170+
specialize this2 U hU
171+
specialize this1 _ this2
172+
convert this1 using 1
173+
ext x
174+
convert conjAct_mem _ _ _ using 1
175+
simp only [Set.mem_preimage, SetLike.mem_coe]
176+
refine ⟨?_, ?_⟩ <;> intro h
177+
· use g⁻¹ * x * g -- duh
178+
simp [h]
179+
group
180+
· rcases h with ⟨u, hu, rfl⟩
181+
group
182+
exact hu
183+
184+
instance : SMul (Dfx F D) (AutomorphicForm F D M) where
185+
smul g φ := { -- (g • f) (x) := f(xg) -- x(gf)=(xg)f
186+
toFun := fun x => φ (x * g)
187+
left_invt := by
188+
intros d x
189+
simp only [← φ.left_invt d x, mul_assoc]
190+
exact φ.left_invt d (x * g)
191+
loc_cst := by
192+
rcases φ.loc_cst with ⟨U, openU, hU⟩
193+
use toConjAct g • U
194+
constructor
195+
· apply toConjAct_open _ openU
196+
· intros x u umem
197+
simp only
198+
rw[conjAct_mem] at umem
199+
obtain ⟨ugu, hugu, eq⟩ := umem
200+
rw[←eq, ←mul_assoc, ←mul_assoc, inv_mul_cancel_right, hU (x*g) ugu hugu]
201+
}
202+
203+
@[simp]
204+
lemma sMul_eval (g : Dfx F D) (f : AutomorphicForm F D M) (x : (D ⊗[F] FiniteAdeleRing (𝓞 F) F)ˣ) :
205+
(g • f) x = f (x * g) := rfl
206+
207+
instance : MulAction (Dfx F D) (AutomorphicForm F D M) where
208+
smul := (. • .)
209+
one_smul := by intros; ext; simp only [sMul_eval, mul_one]
210+
mul_smul := by intros; ext; simp only [sMul_eval, mul_assoc]

0 commit comments

Comments
 (0)