From 852865fe7109a2e315d6e938d7710d9fe90f5016 Mon Sep 17 00:00:00 2001 From: Hannah Scholz Date: Mon, 17 Jun 2024 17:33:15 +0200 Subject: [PATCH 1/5] made some changes in proof of instance : MulAction --- FLT/AutomorphicForm/QuaternionAlgebra.lean | 15 ++++----------- 1 file changed, 4 insertions(+), 11 deletions(-) diff --git a/FLT/AutomorphicForm/QuaternionAlgebra.lean b/FLT/AutomorphicForm/QuaternionAlgebra.lean index 656f560c..ea3fbe3f 100644 --- a/FLT/AutomorphicForm/QuaternionAlgebra.lean +++ b/FLT/AutomorphicForm/QuaternionAlgebra.lean @@ -168,11 +168,10 @@ instance addCommGroup : AddCommGroup (AutomorphicForm F D M) where instance : MulAction (Dfx F D) (AutomorphicForm F D M) where smul g φ := { - toFun := fun x => φ (x*g), + toFun := fun x => φ (x * g) left_invt := by intros d x - simp only [← φ.left_invt d x] - rw [mul_assoc] + simp only [← φ.left_invt d x, mul_assoc] exact φ.left_invt d (x * g) loc_cst := by rcases φ.loc_cst with ⟨U, openU, hU⟩ @@ -183,14 +182,8 @@ instance : MulAction (Dfx F D) (AutomorphicForm F D M) where simp only sorry } -- (g • f) (x) := f(xg) -- x(gf)=(xg)f - one_smul := by - intros φ - have h:{toFun := fun x => φ (x * 1), left_invt := ?_, loc_cst := ?_} = φ := by - simp only [mul_one] - exact h - mul_smul := by - intros g h φ - sorry + one_smul := by intros; simp only [instHSMul, mul_one] + mul_smul := by intros; ext; simp only [instHSMul, mk.injEq, mul_assoc] -- if M is an R-module (e.g. if M = R!), then Automorphic forms are also an R-module -- with the action being 0on the coefficients. From 933bed8afba827117b5581ce56e3b4247feb9e26 Mon Sep 17 00:00:00 2001 From: monnerjahnl0 Date: Tue, 18 Jun 2024 13:15:28 +0200 Subject: [PATCH 2/5] chore: Add conjAct_mem --- FLT/AutomorphicForm/QuaternionAlgebra.lean | 25 +++++++++++++++------- 1 file changed, 17 insertions(+), 8 deletions(-) diff --git a/FLT/AutomorphicForm/QuaternionAlgebra.lean b/FLT/AutomorphicForm/QuaternionAlgebra.lean index ea3fbe3f..a960ac0c 100644 --- a/FLT/AutomorphicForm/QuaternionAlgebra.lean +++ b/FLT/AutomorphicForm/QuaternionAlgebra.lean @@ -7,6 +7,7 @@ import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup import Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra import Mathlib.NumberTheory.NumberField.Basic import Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing +import Mathlib.Algebra.Group.Subgroup.Pointwise import FLT.HIMExperiments.module_topology --import Mathlib @@ -41,7 +42,6 @@ section missing_instances variable {R D A : Type*} [CommRing R] [Ring D] [CommRing A] [Algebra R D] [Algebra R A] ---TODO: instance : Algebra A (D ⊗[R] A) := Algebra.TensorProduct.includeRight.toRingHom.toAlgebra' (by simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, Algebra.TensorProduct.includeRight_apply] @@ -55,8 +55,6 @@ instance : Algebra A (D ⊗[R] A) := rw [left_distrib, hx, hy, right_distrib] ) - - instance [Module.Finite R D] : Module.Finite A (D ⊗[R] A) := sorry instance [Module.Free R D] : Module.Free A (D ⊗[R] A) := sorry @@ -166,8 +164,13 @@ instance addCommGroup : AddCommGroup (AutomorphicForm F D M) where add_left_neg := by intros; ext; simp add_comm := by intros; ext; simp [add_comm] +open scoped Pointwise +lemma conjAct_mem {G: Type*} [Group G] (U: Subgroup G) (g: G) (x : G): + x ∈ ConjAct.toConjAct g • U ↔ ∃ u ∈ U, g * u * g⁻¹ = x := by rfl + + instance : MulAction (Dfx F D) (AutomorphicForm F D M) where - smul g φ := { + smul g φ := { -- (g • f) (x) := f(xg) -- x(gf)=(xg)f toFun := fun x => φ (x * g) left_invt := by intros d x @@ -175,13 +178,19 @@ instance : MulAction (Dfx F D) (AutomorphicForm F D M) where exact φ.left_invt d (x * g) loc_cst := by rcases φ.loc_cst with ⟨U, openU, hU⟩ - use U + use ConjAct.toConjAct g • U constructor - · exact openU + · simp only [Subgroup.coe_pointwise_smul] + suffices @IsOpen (D ⊗[F] FiniteAdeleRing (𝓞 F) F)ˣ _ ↑U by + --exact conjAct_open U g this + sorry + exact openU · intros x u umem simp only - sorry - } -- (g • f) (x) := f(xg) -- x(gf)=(xg)f + rw[conjAct_mem] at umem + obtain ⟨ugu, hugu, eq⟩ := umem + rw[←eq, ←mul_assoc, ←mul_assoc, inv_mul_cancel_right, hU (x*g) ugu hugu] + } one_smul := by intros; simp only [instHSMul, mul_one] mul_smul := by intros; ext; simp only [instHSMul, mk.injEq, mul_assoc] -- if M is an R-module (e.g. if M = R!), then Automorphic forms are also an R-module From e471431a267f08bda953823082efe888fe25af36 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Thu, 20 Jun 2024 16:07:13 +0200 Subject: [PATCH 3/5] fix sorry --- FLT/AutomorphicForm/QuaternionAlgebra.lean | 50 ++++++++++++++++------ 1 file changed, 36 insertions(+), 14 deletions(-) diff --git a/FLT/AutomorphicForm/QuaternionAlgebra.lean b/FLT/AutomorphicForm/QuaternionAlgebra.lean index 8b838c25..3d975dea 100644 --- a/FLT/AutomorphicForm/QuaternionAlgebra.lean +++ b/FLT/AutomorphicForm/QuaternionAlgebra.lean @@ -164,13 +164,32 @@ instance addCommGroup : AddCommGroup (AutomorphicForm F D M) where add_left_neg := by intros; ext; simp add_comm := by intros; ext; simp [add_comm] +open ConjAct + open scoped Pointwise lemma conjAct_mem {G: Type*} [Group G] (U: Subgroup G) (g: G) (x : G): - x ∈ ConjAct.toConjAct g • U ↔ ∃ u ∈ U, g * u * g⁻¹ = x := by rfl - - --- this should be a SMul instance first, and then a simp lemma SMul_eval, and then one_smul etc are easy -instance : MulAction (Dfx F D) (AutomorphicForm F D M) where + x ∈ toConjAct g • U ↔ ∃ u ∈ U, g * u * g⁻¹ = x := by rfl + +lemma toConjAct_open {G : Type*} [Group G] [TopologicalSpace G] [TopologicalGroup G] + (U : Subgroup G) (hU : IsOpen (U : Set G)) (g : G) : IsOpen (toConjAct g • U : Set G) := by + have this1 := continuous_mul_left g⁻¹ + have this2 := continuous_mul_right g + rw [continuous_def] at this1 this2 + specialize this2 U hU + specialize this1 _ this2 + convert this1 using 1 + ext x + convert conjAct_mem _ _ _ using 1 + simp + refine ⟨?_, ?_⟩ <;> intro h + · use g⁻¹ * x * g -- duh + simp [h] + group + · rcases h with ⟨u, hu, rfl⟩ + group + exact hu + +instance : SMul (Dfx F D) (AutomorphicForm F D M) where smul g φ := { -- (g • f) (x) := f(xg) -- x(gf)=(xg)f toFun := fun x => φ (x * g) left_invt := by @@ -179,22 +198,25 @@ instance : MulAction (Dfx F D) (AutomorphicForm F D M) where exact φ.left_invt d (x * g) loc_cst := by rcases φ.loc_cst with ⟨U, openU, hU⟩ - use ConjAct.toConjAct g • U + use toConjAct g • U constructor · simp only [Subgroup.coe_pointwise_smul] - suffices @IsOpen (D ⊗[F] FiniteAdeleRing (𝓞 F) F)ˣ _ ↑U by - --exact conjAct_open U g this - sorry - exact openU + apply toConjAct_open _ openU · intros x u umem simp only rw[conjAct_mem] at umem obtain ⟨ugu, hugu, eq⟩ := umem rw[←eq, ←mul_assoc, ←mul_assoc, inv_mul_cancel_right, hU (x*g) ugu hugu] } - one_smul := by intros; simp only [instHSMul, mul_one] - mul_smul := by intros; ext; simp only [instHSMul, mk.injEq, mul_assoc] --- if M is an R-module (e.g. if M = R!), then Automorphic forms are also an R-module --- with the action being 0on the coefficients. + +@[simp] +lemma sMul_eval (g : Dfx F D) (f : AutomorphicForm F D M) (x : (D ⊗[F] FiniteAdeleRing (𝓞 F) F)ˣ) : + (g • f) x = f (x * g) := rfl + +-- this should be a SMul instance first, and then a simp lemma SMul_eval, and then one_smul etc are easy +instance : MulAction (Dfx F D) (AutomorphicForm F D M) where + smul := (. • .) + one_smul := by intros; ext; simp + mul_smul := by intros; ext; simp [mul_assoc] example(a b c :ℝ ): a * b * c = (a * b) * c := rfl From 4d39d6313c76498b0ac0c64e0185d4f63079f8ad Mon Sep 17 00:00:00 2001 From: monnerjahnl0 Date: Thu, 20 Jun 2024 16:33:48 +0200 Subject: [PATCH 4/5] Clean up --- FLT/AutomorphicForm/QuaternionAlgebra.lean | 21 +++++---------------- 1 file changed, 5 insertions(+), 16 deletions(-) diff --git a/FLT/AutomorphicForm/QuaternionAlgebra.lean b/FLT/AutomorphicForm/QuaternionAlgebra.lean index 3d975dea..e1a71f4e 100644 --- a/FLT/AutomorphicForm/QuaternionAlgebra.lean +++ b/FLT/AutomorphicForm/QuaternionAlgebra.lean @@ -22,22 +22,16 @@ variable (F : Type*) [Field F] [NumberField F] variable (D : Type*) [Ring D] [Algebra F D] [FiniteDimensional F D] -#check DedekindDomain.FiniteAdeleRing - open DedekindDomain open scoped NumberField -#check FiniteAdeleRing (𝓞 F) F - -- my work (two PRs) instance : TopologicalSpace (FiniteAdeleRing (𝓞 F) F) := sorry instance : TopologicalRing (FiniteAdeleRing (𝓞 F) F) := sorry open scoped TensorProduct -#check D ⊗[F] (FiniteAdeleRing (𝓞 F) F) - section missing_instances variable {R D A : Type*} [CommRing R] [Ring D] [CommRing A] [Algebra R D] [Algebra R A] @@ -56,7 +50,6 @@ instance : Algebra A (D ⊗[R] A) := ) instance [Module.Finite R D] : Module.Finite A (D ⊗[R] A) := sorry - instance [Module.Free R D] : Module.Free A (D ⊗[R] A) := sorry -- #synth Ring (D ⊗[F] FiniteAdeleRing (𝓞 F) F) @@ -165,8 +158,8 @@ instance addCommGroup : AddCommGroup (AutomorphicForm F D M) where add_comm := by intros; ext; simp [add_comm] open ConjAct - open scoped Pointwise + lemma conjAct_mem {G: Type*} [Group G] (U: Subgroup G) (g: G) (x : G): x ∈ toConjAct g • U ↔ ∃ u ∈ U, g * u * g⁻¹ = x := by rfl @@ -180,7 +173,7 @@ lemma toConjAct_open {G : Type*} [Group G] [TopologicalSpace G] [TopologicalGrou convert this1 using 1 ext x convert conjAct_mem _ _ _ using 1 - simp + simp only [Set.mem_preimage, SetLike.mem_coe] refine ⟨?_, ?_⟩ <;> intro h · use g⁻¹ * x * g -- duh simp [h] @@ -200,8 +193,7 @@ instance : SMul (Dfx F D) (AutomorphicForm F D M) where rcases φ.loc_cst with ⟨U, openU, hU⟩ use toConjAct g • U constructor - · simp only [Subgroup.coe_pointwise_smul] - apply toConjAct_open _ openU + · apply toConjAct_open _ openU · intros x u umem simp only rw[conjAct_mem] at umem @@ -213,10 +205,7 @@ instance : SMul (Dfx F D) (AutomorphicForm F D M) where lemma sMul_eval (g : Dfx F D) (f : AutomorphicForm F D M) (x : (D ⊗[F] FiniteAdeleRing (𝓞 F) F)ˣ) : (g • f) x = f (x * g) := rfl --- this should be a SMul instance first, and then a simp lemma SMul_eval, and then one_smul etc are easy instance : MulAction (Dfx F D) (AutomorphicForm F D M) where smul := (. • .) - one_smul := by intros; ext; simp - mul_smul := by intros; ext; simp [mul_assoc] - -example(a b c :ℝ ): a * b * c = (a * b) * c := rfl + one_smul := by intros; ext; simp only [sMul_eval, mul_one] + mul_smul := by intros; ext; simp only [sMul_eval, mul_assoc] From 4acc7cfc525b253ab0248d0938c63c3811c37aaf Mon Sep 17 00:00:00 2001 From: monnerjahnl0 Date: Thu, 20 Jun 2024 17:57:10 +0200 Subject: [PATCH 5/5] Add authors --- FLT/AutomorphicForm/QuaternionAlgebra.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FLT/AutomorphicForm/QuaternionAlgebra.lean b/FLT/AutomorphicForm/QuaternionAlgebra.lean index e1a71f4e..db730579 100644 --- a/FLT/AutomorphicForm/QuaternionAlgebra.lean +++ b/FLT/AutomorphicForm/QuaternionAlgebra.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2024 Kevin Buzzard. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Kevin Buzzard +Authors: Kevin Buzzard, Ludwig Monnerjahn, Hannah Scholz -/ import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup import Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra