-
Notifications
You must be signed in to change notification settings - Fork 52
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Issue #259: A_K/K is compact if A_Q/Q is compact #310
Conversation
I've bumped main in the FLT project because we had been stuck on 4.15 for technical reasons; this created conflicts and errors in this PR but I've fixed them all in this commit. PS oh dear the diff is nasty, basically all I did was replace |
simp only [_root_.TensorProduct.piScalarRight_symm_apply, LinearMap.lsum_apply, | ||
LinearMap.coeFn_sum, LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.coe_proj, | ||
Finset.sum_apply, Function.comp_apply, Function.eval, Algebra.algebraMap_eq_smul_one, | ||
TensorProduct.smul_tmul, ← TensorProduct.tmul_sum, ← Pi.single_smul, smul_eq_mul, mul_one] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
simp only [_root_.TensorProduct.piScalarRight_symm_apply, LinearMap.lsum_apply, | |
LinearMap.coeFn_sum, LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.coe_proj, | |
Finset.sum_apply, Function.comp_apply, Function.eval, Algebra.algebraMap_eq_smul_one, | |
TensorProduct.smul_tmul, ← TensorProduct.tmul_sum, ← Pi.single_smul, smul_eq_mul, mul_one] | |
simp [LinearEquiv.symm_apply_eq, algebraMap_eq_smul_one] |
@@ -0,0 +1,10 @@ | |||
import Mathlib.LinearAlgebra.TensorProduct.Pi | |||
|
|||
theorem TensorProduct.piScalarRight_symm_apply (R S N ι : Type*) [CommSemiring R] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't think we need this theorem. See my suggestion below for avoiding it the only time you use it.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice, this has been removed in #315
FLT/NumberField/AdeleRing.lean
Outdated
noncomputable instance : Algebra K (NumberField.AdeleRing L) := | ||
RingHom.toAlgebra <| (algebraMap L (NumberField.AdeleRing L)).comp <| algebraMap K L |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
noncomputable instance : Algebra K (NumberField.AdeleRing L) := | |
RingHom.toAlgebra <| (algebraMap L (NumberField.AdeleRing L)).comp <| algebraMap K L | |
noncomputable instance : Algebra K (NumberField.AdeleRing (𝓞 L) L) := | |
Algebra.compHom _ (algebraMap K L) |
I think this is better because if K=L then you might get a diamond with your approach. Indeed this suggestion breaks a proof in a good way later on (it finishes early)
FLT/NumberField/AdeleRing.lean
Outdated
https://math.mit.edu/classes/18.785/2017fa/LectureNotes25.pdf (just above Prop 25.10) | ||
for an informal source where the tensor product is given the product topology. Maybe they | ||
coincide! | ||
-/ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, the module topology on a finite free R-module coincides with the product topology for any choice of basis (and in particular the topology on a finite free thing is independent of choice of basis). IsModuleTopology.instPi
(in mathlib) proves this. What I initially don't like about your instance is that it might depend on a choice of basis. But in fact you can just prove it's the module topology using instPi
so it doesn't really matter. The point about the module topology is that you don't have to choose a basis.
FLT/NumberField/AdeleRing.lean
Outdated
to using `AdeleRing K ⊗[K] L` is that it automatically gets | ||
a `K` algebra instance via the instance `Algebra.TensorProduct.leftAlgebra` | ||
(while `rightAlgebra` is a def), but maybe there are other reasons to | ||
prefer the `rightAlgebra` set up. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah :-/ Of course the benefit of using the other order is that you automatically get an L
-algebra instance. I am still really unclear about the best way to proceed here. When doing automorphic forms it's really normal to have G(Q) \ G(A) and so I've been putting number fields on the left in general but that was my only logic.
FLT/NumberField/AdeleRing.lean
Outdated
(while `rightAlgebra` is a def), but maybe there are other reasons to | ||
prefer the `rightAlgebra` set up. | ||
-/ | ||
def baseChange : (AdeleRing K ⊗[K] L) ≃A[K] AdeleRing L := sorry |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is there a way we can write down the data and only sorry the proofs here?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think you should write L ⊗ AdeleRing K
and make it an L
-algebra homomorphism.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I imagine this result will follow from some results that combine the two base changes for the infinite and finite adele ring. I can work on that in this PR as well.
FLT/NumberField/AdeleRing.lean
Outdated
variable {L} | ||
|
||
theorem baseChange_tsum_apply_right (l : L) : | ||
baseChange K L (1 ⊗ₜ[K] l) = algebraMap L (AdeleRing L) l := sorry |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
because then this theorem would be provable.
Sorry, I somehow managed to close this PR without meaning to! The new one is open here #315 It includes some fixes to comments here, but some still remain so it's WIP atm. |
Closes #259