Outstanding tasks, V10

Stream: FLT

[Kevin Buzzard]

OK so we are hopefully almost over the line with theorem TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.finiteDimensional in FLT/AutomorphicForm/QuaternionAlgebra/FiniteDimensional.lean. Other than #26377 (which is looking in good shape) we were down to 1 sorry which had a simple-looking proof which has turned out to be far more subtle to formalize than I had realised.FLT#828 blows this sorry back up to 9 sorries, of which three are identical and four others are basically in two pairs of "if you do one, then the other is just the same". I'll break them down here. Note that there is no blueprint for any of this.

Update: the remaining tasks below are task 4 (claimed by me but I'm indicating when I'm not working on it) and task 5 (unclaimed).

Update: all tasks done!

[Kevin Buzzard]

First task: the two sorries in FLT/DedekindDomain/FiniteAdeleRing/TensorProduct.lean. Mathematically here's what's going on: if $K$ is a local field and $\mathbb{A}_K^f$ is the finite adeles of $K$ and $v$ is a finite place of $K$, then there's an additive group homomorphism $K_v\to\mathbb{A}_K^f$ called single (sending $x$ to $(0,0,0,\ldots,0,x,0,\ldots)$) and a ring homomorphism $\mathbb{A}_K^f\to K_v$ called eval (sending $(x_w)_w$ to $x_v$). They're both $K$-linear. If you do single then eval you get back to where you started if you do eval and then single then this is $K$-linear (and actually $\mathbb{A}_K^f$-linear) endomorphism of $\mathbb{A}_K^f$ given by multiplication by the local idempotent element $(0,0,0,\ldots,0,1,0,0,\ldots)$ with the $1$ in the $v$ th place.

If now $V$ is a finite-dimensional $K$-vector space then these can be base-extended to functions $K_v\otimes_KV\to\mathbb{A}_K^f\otimes_KV$ and $\mathbb{A}_K^f\otimes_KV\to K_v\otimes_KV$. The theorems evalContinuousAlgebraMap_singleContinuousLinearMap and singleContinuousAlgebraMap_comp_evalContinuousLinearMap (already sorry-free) say that the composites in both directions are still the identity and multiplication by the idempotent.

Now say $\phi:\mathbb{A}_K^f\otimes_KV\to\mathbb{A}_K^f\otimes_KV$ is an $\mathbb{A}_K^f$-linear map (note that $\mathbb{A}_K^f\otimes_KV$ is just a finite free $\mathbb{A}_K^f$-module) and $v$ is a finite place of $K$. The \emph{local component} $\phi_v$ of $\phi$ at $v$ is the composite of eval, $\phi$ and single, so it's a $K$-linear map $K_v\otimes_KV\to K_v\otimes_KV$.

What we need to prove is that if $\phi$ is actually an $\mathbb{A}_K^f$-linear \emph{isomorphism} then $\phi_v$ is too, and that $(\phi^{-1})_v=(\phi_v)^{-1}$. This follows pretty formally from the sorried lemmas TensorProduct.localcomponent_id_apply and TensorProduct.localcomponent_comp_apply. Both of these follow from the definition and the facts about eval and single: localcomponent φ is defined as eval ∘ φ ∘ single, so for id_apply you just need to check eval ∘ single = id and we have this; for comp one needs to check eval ∘ φ ∘ single ∘ eval ∘ ψ ∘ single =
eval ∘ φ ∘ ψ ∘ single and the proof is: cancel the single on the right, then use that the middle single ∘ eval is multiplication by the local idempotent e_v at v (this is singleContinuousAlgebraMap_comp_evalContinuousLinearMap)
and then that φ is 𝔸_K^f-linear, which reduces the question to evalᵥ ∘ (multiply by e_v) = eval which is true and easy by ext.

So perhaps there are two tasks here (edit: both done now)

1) prove localcomponent_id; (done by Bryan Wang)
2) prove localcomponent_comp; (done by Bryan Wang)

Both these are in FLT#833 when I merge it (which will be any minute now; edit: done).

[Kevin Buzzard]

3rd task: IsCompact (v.adicCompletionIntegers K : Set (v.adicCompletion K)). Surely we have this somewhere! It's three(!) sorries in FLT/HaarMeasure/HaarChar/FiniteAdeleRing.lean. Lines 112, 124 and 133 currently.

Status: done by Bryan Wang

[Kevin Buzzard]

4th task: FiniteAdeleRing.Aux.almost_always_integral. This feels subtle and I think I'll take it on. The claim is that if $\phi:\mathbb{A}_K^f\otimes_KV\cong\mathbb{A}_K^f\otimes_KV$ is $\mathbb{A}_K^f$-linear then for almost all local components $\phi_v:K_v^n\to K_v^n$ induce a bijection $\mathcal{O}_v^n\to\mathcal{O}_v^n.$

Status: in progress (Kevin and Bryan)

[Kevin Buzzard]

The 5th task is a diagram chase. It says that if $\phi:\mathbb{A}_K^f\otimes_KV\to\mathbb{A}_K^f\otimes_KV$ then $\phi=\prod_v\phi_v$ where $\phi_v$ is the local component of $\phi$ at $v$. I want this to be ext; rfl but unfortunately it isn't.

Also unfortunately, $\mathbb{A}_K^f\otimes_KV$ isn't definitionally equal to a restricted product (far from it) so it takes a while to even make the statement make sense. We have functions $f$ and $g$ (i.e. FiniteAdeleRing.Aux.f and FiniteAdeleRing.Aux.g) which we use to move from $\mathbb{A}_K^f\otimes_KV$ to $\prod'_v[K_v^n;\mathcal{O}_v^n]$ and a function $e$ which we use to move from $K_v\otimes_KV$ to $K_v^n$ and the claim is that using $f$ and $g$ and $e$ to translate the question to one which does make sense, it's true :-) I am hoping that TensorProduct.localcomponent_apply is the key result.

Status: unclaimed. I'll probably claim it when I've done the previous one, unless someone else wants to have a go.

[Kevin Buzzard]

The 6th and final task is the last two sorries: localcomponent_mulLeft and localcomponent_mulRight in FLT/HaarMeasure/HaarChar/FiniteAdeleRing.lean. This says that if $u\in(\mathbb{A}_K^f\otimes_KB)^\times$ then the local component of left (resp right) multiplication by $u$ is equal to left (resp right) multiplication by $u_v$. Again localcomponent_apply might be helpful.

Status: done by Thomas Browning in FLT#834

[Kevin Buzzard]

The thing which has created all this work is that we need to explicitly make $\mathbb{A}_K^f\otimes_KV$ into a restricted product, which involves (a) picking a $K$-basis for $V$ (a finite-dimensional $$K$-vector space) using Module.Free.chooseBasis (b) getting an isomorphism $\mathbb{A}_K^f\otimes_KV=(\mathbb{A}_K^f)^n$; (c) commuting the $$n$$th power and the restricted product to get $\prod'_v[K_v^n;\mathcal{O}_v^n]$ (d) doing the same locally for $K_v\otimes_KV$ and $K_v^n$; (e) doing something trivial and then having to chase everything back.

[Thomas Browning]

I can do task 6 (at least, I've got the first sorry filled-in now).

[Kevin Buzzard]

Oh nice! I can't imagine that the second one will be any different...

[Bryan Wang]

I'm almost done with the (easy) tasks 1 to 3 and will PR soon!

[Kevin Buzzard]

I'm about to start on the 4th task

[Thomas Browning]

Kevin Buzzard said:

Oh nice! I can't imagine that the second one will be any different...

Yeah, just wanted to clean up the code slightly before duplicating. Here's the PR: FLT#834

[Bryan Wang]

Tasks 1 to 3 in FLT#835

[Kevin Buzzard]

OK I need to go to bed and I am extremely unlikely to be thinking about Task 4 for another 12 hours, so I've PRed my progress in FLT#836 and if someone wants to temporarily claim this off me while I'm sleeping/doing family time tomorrow then they should announce this here. I've pushed what I think is a promising approach but I still need to do the hard work. Hopefully I have reduced the claim to a concrete claim about matrices which are v-adically integral preserving integral structures but now I think I have to unravel everything and draw a diagram to check that everything is now in fact easy.

[Bryan Wang]

I can have a look in a bit

[Bryan Wang]

I reduced task 4 to two sorries about TensorProduct.localcomponent φ in FLT#837; the first (line 281) is that TensorProduct.localcomponent φ is K_v-linear (I hope this is true..) and the second (line 323) is that the matrix rep of TensorProduct.localcomponent φ as K_v-linear map is the local component at v of the matrix rep of φ.

Feel free to use another approach as I'm not sure whether these two sorries are really much easier; I'm heading to a birthday celebration soon so won't be working on it for now, but I can continue later on if necessary.

[Kevin Buzzard]

Thanks. Yes it's definitely K_v-linear and I bet I can prove it. The statement about matrices should also be true, I will let you know when I have time to think about it. I do think that this is progress in the sense that this was how I was going to prove it!

[Kevin Buzzard]

(I'm working on this again now; currently working on K_v-linearity)

[Kevin Buzzard]

The inclusion $K_v\to \mathbb{A}_K^f$ is not a ring homomorphism, but it is a docs#MulHom :D

[Kevin Buzzard]

The other missing piece is

import Mathlib.LinearAlgebra.TensorProduct.Basic
import Mathlib.Algebra.Algebra.Hom

open TensorProduct
/--
The base extension of an R-algebra homomorphism `f : N → P` to an  `f`-semilinear
map `N ⊗[R] M → P ⊗[R] M`.
-/
def AlgHom.rTensor {R : Type*} [CommSemiring R] (M : Type*) {N : Type*}
    {P : Type*} [AddCommMonoid M] [Semiring N] [Semiring P] [Module R M]
    [Algebra R N] [Algebra R P] (f : N →ₐ[R] P) :
  N ⊗[R] M →ₛₗ[f.toRingHom] P ⊗[R] M := {
    __ := LinearMap.rTensor M f
    map_smul' n x := by
      induction x with
      | zero => simp
      | tmul x y =>
        rw [smul_tmul']
        change (LinearMap.rTensor M f.toLinearMap) _ = _
        rw [LinearMap.rTensor_tmul]
        rw [smul_eq_mul]
        change f (n * x) ⊗ₜ[R] y = _
        rw [map_mul]
        rfl
      | add x y _ _ => simp_all

but fortunately I added that a few days ago :-) I was slightly surprised that it wasn't in mathlib, but maybe not too surprised, because we are really hammering rTensor here. Bryan I merged your branch into my branch (this just seemed like the easiest way to proceed) and filled in the proof of K_v-linearity. I'll now start on the matrix calculation.actually I'll maybe review/merge everyone else's stuff! Edit: done; now I'm thinking about the matrix calculation again.

[Kevin Buzzard]

OK I had less time than I thought for the matrix calculation in the 4th task. I've got as far as removing localcomponent and single from the claim, and I suspect that there is now some kind of general fact about matrices/linear maps which can be abstracted out and from which things should follow. I've left a lengthy comment on lines 345-371 of FLT/HaarMeasure/HaarChar/FiniteAdeleRing.lean in FLT#836 (which includes Bryan's commit from FLT#837), explaining where we are. I am now not going to work on this for 12 hours or so.

Vaguely speaking, the missing claim is something of the form: if you have a field $K$, a finite-dimensional $K$-vector space $M$, a linear map $A\otimes_KM\to A\otimes_KM$ with $A$ a $K$-algebra, and a $K$-algebra map $f:A\to B$, then if you choose an $A$-basis of $A\otimes_KM$ you get an induced $B$-basis of $B\otimes_KM$ and if you convert a linear endomorphism of $A\otimes_KM$ into a matrix with coefficients in $A$ and then evaluate all the coordinates on the linear map to get a matrix with coefficients in $B$, and convert that new matrix back into a linear endomorphism of $B\otimes_KM$, then this new linear map evaluated at $(f\otimes 1)(x)$ is equal to $f\otimes 1$ of the old linear map evaluated at $x$.

[Bryan Wang]

I should have some time to think about this in the next 12 hours :)

[Kevin Buzzard]

I don't know if I'm going the right way, but eliminating single (which is not a particularly well-behaved function) seemed like a good idea.

[Bryan Wang]

It's completed in FLT#838; the key was to write φ as (Matrix.toLin b b) (LinearMap.toMatrix b b) φ, then simplify using Matrix.toLin_apply. I think it was surprisingly much less painful than expected, mainly thanks to the well-written Module.Basis API in mathlib :)

[Bryan Wang]

I might have a quick look at task 5 and see how far I get..

[Bryan Wang]

FLT#838 now also finishes task 5, which is also proven using matrix reps. The file is now slightly messy and I can do some cleaning up/refactoring in the coming days, but - it is now sorry-free as far as I can tell :)

[Kevin Buzzard]

Thanks so much!