Zulip Chat Archive

Stream: maths

Topic: products of Cauchy filters


view this post on Zulip Patrick Massot (Jul 24 2018 at 19:39):

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.

view this post on Zulip Patrick Massot (Jul 24 2018 at 19:41):

@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...".

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 20:26):

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...

view this post on Zulip Patrick Massot (Jul 24 2018 at 20:29):

We still have one week

view this post on Zulip Patrick Massot (Jul 24 2018 at 20:30):

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

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 20:36):

I need quotient groups.

view this post on Zulip Patrick Massot (Jul 24 2018 at 20:39):

Don't you have quotient groups?

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 20:39):

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.

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 20:39):

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.

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 20:39):

I'll take a look now.

view this post on Zulip Patrick Massot (Jul 24 2018 at 20:40):

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

view this post on Zulip Patrick Massot (Jul 24 2018 at 20:41):

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

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 20:41):

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.

view this post on Zulip Patrick Massot (Jul 24 2018 at 20:42):

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

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 20:45):

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.

view this post on Zulip Kenny Lau (Jul 25 2018 at 01:41):

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).

view this post on Zulip Kenny Lau (Jul 25 2018 at 01:47):

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

view this post on Zulip Kenny Lau (Jul 25 2018 at 01:49):

but here's an alternative proof:

view this post on Zulip Kenny Lau (Jul 25 2018 at 01:49):

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)

view this post on Zulip Kevin Buzzard (Jul 25 2018 at 08:54):

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

view this post on Zulip Kenny Lau (Jul 25 2018 at 08:55):

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

view this post on Zulip Kenny Lau (Jul 25 2018 at 08:55):

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

view this post on Zulip Kevin Buzzard (Jul 25 2018 at 08:55):

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

view this post on Zulip Kenny Lau (Jul 25 2018 at 08:56):

my old tensor product is in the stacks project

view this post on Zulip Kevin Buzzard (Jul 25 2018 at 08:56):

That's still a random repo :-(

view this post on Zulip Kenny Lau (Jul 25 2018 at 08:56):

:-(

view this post on Zulip Kevin Buzzard (Jul 25 2018 at 08:57):

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.

view this post on Zulip Johan Commelin (Jul 25 2018 at 09:02):

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.

view this post on Zulip Patrick Massot (Jul 25 2018 at 09:03):

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.

view this post on Zulip Johan Commelin (Jul 25 2018 at 09:04):

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.

view this post on Zulip Johan Commelin (Jul 25 2018 at 09:05):

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

view this post on Zulip Kevin Buzzard (Jul 25 2018 at 09:05):

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.

view this post on Zulip Johan Commelin (Jul 25 2018 at 09:05):

After 5 years...

view this post on Zulip Johan Commelin (Jul 25 2018 at 09:06):

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).

view this post on Zulip Johan Commelin (Jul 25 2018 at 09:07):

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

view this post on Zulip Kevin Buzzard (Jul 25 2018 at 09:07):

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.

view this post on Zulip Patrick Massot (Jul 25 2018 at 09:08):

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.

view this post on Zulip Johan Commelin (Jul 25 2018 at 09:10):

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.

view this post on Zulip Patrick Massot (Jul 25 2018 at 09:10):

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.

view this post on Zulip Johan Commelin (Jul 25 2018 at 09:11):

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.

view this post on Zulip Kevin Buzzard (Jul 25 2018 at 09:11):

That's September's job.

view this post on Zulip Johan Commelin (Jul 25 2018 at 09:11):

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

view this post on Zulip Patrick Massot (Jul 25 2018 at 09:12):

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.

view this post on Zulip Johan Commelin (Jul 25 2018 at 09:14):

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


Last updated: May 11 2021 at 16:22 UTC