products of Cauchy filters

Stream: maths

[Patrick Massot]

I need that a product of Cauchy filters is Cauchy. I couldn't see it in mathlib, so I wrote a couple of lines on paper and decided I should be able to brute force Lean to swallow it. The result on https://gist.github.com/PatrickMassot/aca4545c10aa9d96bf37d9231fb3470c is not pretty (even if you cut in half the two redundant parts). Here brutality is to go all the way down to elements of our uniform spaces. I suspect I missed (or mathlib is missing) some support lemmas which would allow to operate at a higher level. @Mario Carneiro and @Johannes Hölzl, this is probably a good occasion to set a new golfing factor record.

[Patrick Massot]

@Kevin Buzzard if we manage to formalize perfectoid spaces, and someone asks me: "Wow, so you know about perfectoid spaces?" I'll answer "Yeah, it's all about filters...".

[Kevin Buzzard]

Oh we'll definitely formalise perfectoid spaces -- although perhaps not before Scholze gets his fields medal. A lot of it is about completions, for sure...

[Patrick Massot]

We still have one week

[Patrick Massot]

How far are you from perfectoid spaces if you assume topological rings have completions?

[Kevin Buzzard]

I need quotient groups.

[Patrick Massot]

Don't you have quotient groups?

[Kevin Buzzard]

I wrote something, and then Chris wrote something else which probably contradicts it, and he PR'd his to mathlib. There are just so many stupid things which aren't there. I can't define what it means for a valuation to be continuous without quotient rings, fields of fractions etc. It might be possible to do within a week.

[Kevin Buzzard]

But with schemes there was a period of several months when I thought it could all be done in a week and then another hitch appeared.

[Kevin Buzzard]

I'll take a look now.

[Patrick Massot]

I hope I'll be done with completions before the end of this week (but I had the same hope one week ago)

[Patrick Massot]

I had to change my strategy to understand completions of products because I've been too optimistic

[Kevin Buzzard]

Oh I remember now -- I wrote a list of what I needed in the perfectoid thread. I need that a free group is generated by its generators. Some things are only proved for multiplicative groups and some only for additive.

[Patrick Massot]

Maybe @Kenny Lau can help here. He worked a lot on free groups

[Kevin Buzzard]

import group_theory.coset

-- for images
import data.set.basic

-- finsupp for free abelian groups
import data.finsupp

universes u v

variables (G : Type u) [group G] (H : Type v) [group H] (S : set G)

-- maybe use group.in_closure?
theorem closure_image (f : G → H) [is_group_hom f] :
f '' (group.closure (is_group_hom.ker f) ∪ S) = group.closure (f '' S) := sorry

-- don't know why we need decidable equality -- maybe some finsupp reason
example (X : Type u) [decidable_eq X] : add_comm_group (X →₀ ℤ) := by apply_instance

definition group.free_ab_gens (X : Type u) [decidable_eq X] :
X → (X →₀ ℤ) := λ x, finsupp.single x (1 : ℤ)

#check @group.closure

-- do we have to copy out all of the definitions here?
definition group.add_closure {G : Type u} [add_group G] (S : set G) : set G := sorry

-- maybe use finsupp.induction?
theorem closure_free_gens (X : Type u) [decidable_eq X] :
group.add_closure ((group.free_ab_gens X) '' set.univ) = set.univ := sorry

was what I thought I needed after spending several hours proving that if something happened in universe v then it also happened in universe u.

[Kenny Lau]

Oh I remember now -- I wrote a list of what I needed in the perfectoid thread. I need that a free group is generated by its generators. Some things are only proved for multiplicative groups and some only for additive.

I have a similar theorem for free abelian groups (see the other thread).

[Kenny Lau]

but actually there's already enough lemmas in free_group.lean to prove it:

theorem free_group.gen :
  set.univ = group.closure (set.range $ @free_group.of α) :=
calc  set.univ
    = set.range id : set.range_id.symm
... = set.range (free_group.to_group free_group.of) : congr_arg _ $ funext $ λ _, eq.symm $ free_group.to_group.of_eq _
... = group.closure (set.range $ @free_group.of α) : free_group.to_group.range_eq_closure

[Kenny Lau]

but here's an alternative proof:

[Kenny Lau]

import group_theory.free_group

universe u
variable (α : Type u)

@[elab_as_eliminator]
theorem free_group.induction_on {α : Type u}
  {C : free_group α → Prop}
  (z : free_group α)
  (C0 : C 1)
  (C1 : ∀ x, C (free_group.of x))
  (Cn : ∀ x, C (free_group.of x) → C (free_group.of x)⁻¹)
  (Cp : ∀ x y, C x → C y → C (x * y)) : C z :=
quot.induction_on z $ λ L,
list.rec_on L C0 $ λ ⟨x, b⟩ tl ih,
bool.rec_on b (Cp _ _ (Cn _ (C1 x)) ih) (Cp _ _ (C1 x) ih)

theorem free_group.gen :
  set.univ = group.closure (set.range $ @free_group.of α) :=
eq.symm $ set.eq_univ_of_forall $ λ x,
free_group.induction_on x
  (group.in_closure.one _)
  (λ x, group.in_closure.basic ⟨_, rfl⟩)
  (λ x ih, group.in_closure.inv ih)
  (λ _ _, group.in_closure.mul)

[Kevin Buzzard]

Sorry -- I need it for free _abelian_ groups, as defined via the finsupp construction :-/

[Kenny Lau]

1. there is a free abelian group in my new tensor product (the constructive one)

[Kenny Lau]

2. there is a free abelian group in my old tensor product which uses finsupp

[Kevin Buzzard]

I don't want to use random pieces of your random repos :-(

[Kenny Lau]

my old tensor product is in the stacks project

[Kevin Buzzard]

That's still a random repo :-(

[Kenny Lau]

:-(

[Kevin Buzzard]

Although it sounds super-boring I wonder whether after this perfectoid thing I should stop worrying about putting hard maths into Lean and turn my attention to putting easy maths into mathlib. It might teach me a lot about how to write really good Lean code as opposed to just adequate code which runs.

[Johan Commelin]

Hmm, I don't know... I think you should keep the hat of visionary mathematician. There's enough soldiers in your little army to do the "easy math". There are not many people that can think about the big picture.

[Patrick Massot]

At some point we really need to have easy stuff though. Maybe it's because I'm learning so slowly, but I'm a bit pessimistic about Kevin's army learning enough in two summer months to be able to significantly improve the amount of easy maths in mathlib.

[Johan Commelin]

True, but Kevin is writing a book. And I hope that will enable a lot of people to do more stuff. You want some exponential growth to happen. That won't happen if Kevin is busy proving stuff about quotient groups.

[Johan Commelin]

It might happen if every semester 10 UG's from Imperial get interested in Lean and start their own journeys.

[Kevin Buzzard]

I am pessimistic that by 2 months all the students will be writing mathlib-ready code. However I am very optimistic that some of them will be writing good code, and some of them will be writing code which (perhaps inefficiently) fills in holes in mathlb.

[Johan Commelin]

After 5 years...

[Johan Commelin]

I think it is awesome that you guys are now going to teach classes with Lean. I can't pull that off (both because of my Lean-level and career-level).

[Johan Commelin]

But this hasn't happened before, I think. That math students get taught with ITP's

[Kevin Buzzard]

Yes, I am trying to make Lean part of the "culture" here. When I can be bothered to actually go to work I will walk into a room with 10-15 students all doing, and talking about, Lean, and I'll spend the day helping them. I'm hoping it will slowly snowball but I have no idea how realistic this is. I'm pretty sure that in every class of 250 we have I should be able to find 5-10 who are interested and get the hang of it even with no support. The question is how many more I can get in if I make it much easier for them.

[Patrick Massot]

I'm not even talking of mathlib-ready code (I still can't do it myself!). But it could be close enough so that straightening it would be less work than starting from scratch.

[Johan Commelin]

Right, but already you told us that these students are starting to help each other. Which is fantastic. And 2 years from now it will be easy to find TA's for the courses you are giving.

[Patrick Massot]

I won't have 250 students, rather more like 25 (only the students selected for a combined CS/math program). I'm not as brave as Kevin, I'll wait to see what I can do with few good students before trying to use Lean on everybody.

[Johan Commelin]

I do agree that if you teach a course to 250 students, you might want to give them some helper-files that they should import.

[Kevin Buzzard]

That's September's job.

[Johan Commelin]

I just hope that it won't eat up all your time, so that the big picture starts to die...

[Patrick Massot]

I think it is awesome that you guys are now going to teach classes with Lean. I can't pull that off (both because of my Lean-level and career-level).

I hope Lean-level is irrelevant... Career level clearly is, partly because it allows to fool people into trusting you, but mostly because it allows to potentially waste time.

[Johan Commelin]

Well, at my Lean-level, it does become relevant. You are several Lean-levels above me. Your career-level is infinitely beyond mine: tenure vs not