Stream: maths

Topic: products of Cauchy filters

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.

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

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

Patrick Massot (Jul 24 2018 at 20:29):

We still have one week

Patrick Massot (Jul 24 2018 at 20:30):

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

Kevin Buzzard (Jul 24 2018 at 20:36):

I need quotient groups.

Patrick Massot (Jul 24 2018 at 20:39):

Don't you have quotient groups?

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.

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.

Kevin Buzzard (Jul 24 2018 at 20:39):

I'll take a look now.

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)

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

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.

Patrick Massot (Jul 24 2018 at 20:42):

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

Kevin Buzzard (Jul 24 2018 at 20:45):

import group_theory.coset

-- for images
import data.set.basic

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

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  Kenny Lau (Jul 25 2018 at 01:49): but here's an alternative proof: 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)


Kevin Buzzard (Jul 25 2018 at 08:54):

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

Kenny Lau (Jul 25 2018 at 08:55):

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

Kenny Lau (Jul 25 2018 at 08:55):

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

Kevin Buzzard (Jul 25 2018 at 08:55):

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

Kenny Lau (Jul 25 2018 at 08:56):

my old tensor product is in the stacks project

Kevin Buzzard (Jul 25 2018 at 08:56):

That's still a random repo :-(

:-(

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.

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.

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.

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.

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.

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.

After 5 years...

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

Johan Commelin (Jul 25 2018 at 09:07):

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

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.

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.

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.

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.

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.

Kevin Buzzard (Jul 25 2018 at 09:11):

That's September's job.

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

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.

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