class and def (p-adic reps)

Stream: maths

[Shurui Liu]

We are trying to formalize p-adic representation theory (for GL_n(Q_p) at this moment). At the beginning, we need to define l-group (or td group, i.e. totally disconnected T2 group). Is it a better practice to use Class or Def (I guess should be Class, since Topological Space and IsTopologicalGroup are, although IsTotallyDisconnected is Def)? Also shall I name it TdGroup or IsTdGroup? Thank you very much!

[Junyan Xu]

docs#IsTotallyDisconnected is for sets. docs#TotallyDisconnectedSpace is indeed a class.

[Aaron Liu]

Shurui Liu said:

(or td group, i.e. totally disconnected T2 group)

Is that the same as {G : Type*} [Group G] [TopologicalSpace G] [T2Space G] [TotallyDisconnectedSpace G] [IsTopologicalGroup G]?

[Aaron Liu]

If it is, I would suggest you assume those all separately in your theorems instead of bundling them together into one structure

[Kevin Buzzard]

We do bundle props together sometimes, for example docs#NumberField is just other Prop-valued typeclasses on top of Field. But I agree with Aaron that you should just stick with all the separate assumptions for now. Example of why: if you bundle them all together then you'll prove a bunch of results and then you'll have to assume LocallyCompactSpace (because that comes up pretty early on in representation theory of td groups) and then your bundled assumptions won't be the right ones any more.

You mention $GL_n(\mathbb{Q}_p)$ but I would absolutely recommend that you stay well away from $GL_n$ at the beginning and develop the general theory, and when you do want things related to reductive groups that you don't use $GL_n(\mathbb{Q}_p)$ but you work with $GL_n(K)$ where $K$ is any docs#IsNonarchimedeanLocalField because the results will be no harder to prove. Ideally one should be working with $G(K)$ where $G$ is any affine algebraic group over $K$ but I'm still a bit unclear about how we should be saying that.

[Shurui Liu]

Thank you very much for your answers!

First let me apologize for my poor statement of question; I forgot to mention locally compact condition in my original question. I currently define

def IsTdGroup (G : Type*) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Prop :=
  TotallyDisconnectedSpace G ∧ LocallyCompactSpace G ∧ T2Space G

In literature also known as locally profinite group. Then I define smooth representations, Hecke algebras, etc. for this generality. In this case, Should I bundle them together as a Class?

Second, thank Kevin for the suggestion! Yes I should do general NA local field K. And yes, I am proving/defining things for general td group until I have to use structure theory of reductive groups.

Third, ideally I want to work with G(K) where G is a general split reductive group G. But since reductive group theory has not been formalized yet, maybe it is more doable to stick with GL_n, SL_n for the moment when I need structure theory of reductive groups. Even so, some proofs of general split reductive group G can either be reduced to GL_n (e.g. proving G(K) is td group) or modifying proof of GL_n.

I have a related question then: Say in proof of a later theorem, I need to use Iwasawa decomposition of G. Shall I formalize a lemma "GLn_has_Iwasawa_decomposition", or should I make a definition "Group_with_Iwasawa_decomposition", and show "GL_n" is an instance, so that after reductive group theory is formalized, we could more easily adapt the proof for general G?

Thank you all very much for your time and help! You are really helpful!

[Kevin Buzzard]

Yeah IsTdGroup is a terrible idea because then the typeclass system doesn't know anything. As we're trying to explain, the best thing to do is to write

-- Let `G` be a locally profinite topological group
variable (G : Type*) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G]

at the top of your file, because you will find that some results do not need Hausdorff, some results do not need locally compact etc, and Lean will prove everything in the correct generality, which is what we want in this library.

I would stick to developing the theory in this generality first, and hope that other people decide how to say "split reductive group over a nonarch local field" before you get to that part :-) Right now it's hard for me to imagine what Iwasawa decomposition will look like without having a general theory of split reductive groups, because how can you even say "N is the unipotent radical of a Borel" without developing the theory of reductive groups? But before you get there you have the whole theory of smooth and admissible representations, Hecke algebras etc. Note that we have Haar measure, which will be very helpful.

[Stepan Nesterov]

Kevin Buzzard said:

because how can you even say "N is the unipotent radical of a Borel" without developing the theory of reductive groups?

You can say "$G$ admits a BN-pair, such that $U$ is a complement of $B \cap N$ inside $B$".

[Bryan Wang]

I feel like this may be again a case where what is really wanted (from the user's perspective) is some form of class abbrev, e.g. see lean4#8279?

[Shurui Liu]

Thank Kevin for the suggestion on td groups!

Right now it's hard for me to imagine what Iwasawa decomposition will look like without having a general theory of split reductive groups, because how can you even say "N is the unipotent radical of a Borel" without developing the theory of reductive groups? But before you get there you have the whole theory of smooth and admissible representations, Hecke algebras etc. Note that we have Haar measure, which will be very helpful.

I can bypass this by using dynamic approach to Parabolic/Levi/Unipotent radical, rather than using root systems.

[Shurui Liu]

Kevin Buzzard said:

the best thing to do is to write

-- Let `G` be a locally profinite topological group
variable (G : Type*) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G]

I have a question: if so, when I want to define Hecke algebra (and show it is idempotent, etc.), smooth representations, admissible representations, etc., which depend on the definition of td group, will it be too awkward?

My current understanding is:
(1) I should try to make definition/state theorem/prove theorems for td groups as long as possible.
(2) When I need reductive group theory , I try to choose one of equivalent definitions/statements which can be formalized without dependence on split reductive group theory (e.g. defining parabolic using dynamic approach makes sense for any td group), and I treat theorems (e.g. Iwasawa decomposition, Bruhat decomposition, etc.) as definition (group with certain properties), and show GL_n, SL_n are instances (later on when people set up split reductive group theory, we may be able to prove all G(F) are instances) as long as it is possible to do so.

[Kevin Buzzard]

You just put that code at the top and then press on and everything will be fine. I wouldn't worry about reductive group theory right now; it will take a while to get smooth and admissible representations and Hecke algebras defined, you'll need things like smooth induction and so on, there is a long way to go before needing to worry about reductive groups.