Outstanding tasks, V8 : Hecke algebras

Stream: FLT

[Kevin Buzzard]

The FLT project dashboard containing the current list of tasks is here . Instructions on how to claim and work on a task are here.

I've just created 13 new tasks (i.e. sorried theorems) around restricted products and group theory, needed to construct the key Hecke algebras used in the R=T theorem. I've also just merged an entire new miniproject on Hecke algebras to the blueprint. My motivation is that I want to say "We have a definition of the Hecke algebra which sorries no data" in my Big Proof talk a week tomorrow. Here's a desciption of the new tasks.

• FLT#563 is a straightforward lemma in topological group theory.
• FLT#568 is the claim that restricted products wrt open subsets commute with binary products (what happens if the subsets are not open I don't know, and I haven't found anyone who knows, but we don't need it). Detailed proof in blueprint.
• FLT#569 is me not being very good at filter_upwardsa.k.a. finite intersection of things in a filter are in a filter.
• FLT#570 is the claim that restricted products commute with finite products so on paper it's "induction, given the binary case above".
• FLT#571 is the claim that restricted products commute with "take m x n matrices" but because matrices are m -> n -> X not m x n -> X it will no doubt be fiddly to deduce this from FLT#570.
• FLT#581 is a fun topology lemma: units of an arbitrary product of topological monoids is homeomorphic to a product of units. Detailed proof in the blueprint.
• FLT#582 is the same statement but for restricted products; paper proof in blueprint is "a morphism of topological groups is continuous iff it's continuous at 1, which reduces us to FLT#581". Again this might be fiddly in Lean, not sure.
• FLT#583 probably needs some more LaTeX and some more sublemmas. It's the proof that a certain adelic subgroup is compact and open. In the blueprint I actually work with a more general class of subgroups which is probably what we should be working with. Anyone who wants to work on this should probably contact me directly for more info rather than diving in; this could probably be split up into several smaller tasks.
• FLT#584 is the statement that two Hecke operators at a bad prime commute; it is some slightly delicate group theory using some machinery (of being an internal direct product) which I've only just written and isn't really battle-tested so again if someone is interested in this task then they should probably talk to me rather than diving in.
• FLT#585 is the proof that the Hecke algebra is commutative. This should be straightforward if my machine to prove that Hecke operators commute actually works.
• In contrast to the last three perhaps large projects, FLT#586 is a straightforward bit of API: fixed points of a G-action on an R-module are an R-submodule.
• FLT#587 is a straightforward piece of topological algebra: units of an open submonoid of a topological monoid are an open subgroup of the units of the monoid. Proof in the blueprint.
• Finally #588 is an equally straightforward piece of topological algebra: units of a compact submonoid of a Hausdorff topological monoid are a compact subgroup of the units. Is this true without Hausdorff? I don't have a counterexample but my proof doesn't work (and I only need it in the Hausdorff case).