## Stream: maths

### Topic: simplicial complexes in lean

#### Johan Commelin (May 28 2018 at 12:13):

Now we have simplicial complexes!

#### Johan Commelin (May 28 2018 at 12:13):

And also the singular complex

#### Johan Commelin (May 28 2018 at 12:14):

With coefficients in arbitrary \Z-modules

#### Patrick Massot (May 28 2018 at 12:14):

A less magical solution:

lemma simplicial_identity₁ {X : simplicial_set} {n : ℕ} (i j : [n + 1]) (H : i ≤ j) :
(@δ X n) i ∘ δ j.succ = δ j ∘ δ i.raise :=
begin
unfold δ,
rw comp,
rw comp,
congr' 1,
exact simplex_category.simplicial_identity₁ _ _ H
end


#### Johan Commelin (May 28 2018 at 12:14):

Aaah, so congr' is what I was waiting for...

#### Johan Commelin (May 28 2018 at 12:15):

I have no idea what that does...

#### Patrick Massot (May 28 2018 at 12:15):

Uses congruence exactly once

#### Patrick Massot (May 28 2018 at 12:15):

congruence is something we wouldn't bother to state

#### Johan Commelin (May 28 2018 at 12:15):

Alas, we don't have singular homology yet. Because there are no quotient groups... only quotient modules...

#### Patrick Massot (May 28 2018 at 12:15):

x = y implies f(x) = f(y)

#### Johan Commelin (May 28 2018 at 12:16):

And although we take coeffients in \Z-modules, we get a complex of add_comm_groups

#### Johan Commelin (May 28 2018 at 12:16):

Because finsupp gives me add_comm_group, and because is_linear_map drove me crazy...

#### Patrick Massot (May 28 2018 at 12:17):

Small tip: i and j should be implicit arguments because they can be inferred from H

Ok, fair enough

#### Patrick Massot (May 28 2018 at 12:17):

And this is what I did in my simplex_category.simplicial_identity₁ _ _ H

#### Johan Commelin (May 28 2018 at 12:18):

So, now begins the ugly part...

#### Johan Commelin (May 28 2018 at 12:19):

cleaning up the proof

#### Patrick Massot (May 28 2018 at 12:20):

https://github.com/jcommelin/mathlib/blob/06469f0cd7c502ec64b31ba5e6211e937a00b0e1/algebraic_topology/simplicial_set.lean#L49 certainly looks like it could use some cleaning

#### Johan Commelin (May 28 2018 at 13:01):

I cleaned up that line

#### Johan Commelin (May 28 2018 at 13:01):

https://github.com/leanprover/mathlib/pull/144

#### Patrick Massot (May 28 2018 at 14:56):

https://gist.github.com/PatrickMassot/ef4d356b2c42e469a94f392d61cf173b

#### Patrick Massot (May 28 2018 at 14:57):

@Johan Commelin I went through your file, with random local edits

#### Patrick Massot (May 28 2018 at 14:57):

I stopped when I went below 150 lines

#### Patrick Massot (May 28 2018 at 14:57):

I hope you can learn stuff from the diff

#### Patrick Massot (May 28 2018 at 14:57):

But keep in mind these are only local edits

#### Johan Commelin (May 28 2018 at 14:58):

Thanks! I'm looking at it!

#### Patrick Massot (May 28 2018 at 14:58):

You certainly need some global thinking to get useful lemmas replacing parts of this gigantic proof

#### Patrick Massot (May 28 2018 at 14:58):

and using calc would almost certainly make a more readable proof

#### Patrick Massot (May 28 2018 at 15:07):

One last edit spotted because VScode showed me a large area without blue marking: after line 75 of my version simpa using nat.succ_le_succ (mem_filter.mp hp).2 closes the goal

#### Johan Commelin (May 28 2018 at 16:50):

So what is the best way to get some intuition for when to try the finish magic? Or should I just always try it?

don't use it :P

#### Patrick Massot (May 28 2018 at 16:53):

Reading the doc is a good start

#### Johan Commelin (May 28 2018 at 16:57):

Oooh, and thanks a lot for shaving of 80 lines!

#### Patrick Massot (May 28 2018 at 17:00):

Again, you can certainly shave much more, but I hope you can still learn something from this diff

#### Kevin Buzzard (May 28 2018 at 21:39):

Johan I have had my mind on other things today and have only just noticed this -- well done! Want to try perfectoid spaces now? :-)

#### Johan Commelin (May 29 2018 at 06:38):

@Kevin Buzzard Well, I'm not so sure what the best way forward is. (1) I need to do some paper writing on non-formal maths. (2) I would love to formalise something cool (like perfectoid spaces), but I will need a lot of help. (3) There is still a lot of scaffolding missing. module.lean needs some love, I would like to do finitely generated groups/modules/algebras/fields. Then we can do number fields, rings of integers. Define etale morphisms of schemes. Galois theory... the list goes on and on.

#### Johan Commelin (May 29 2018 at 06:38):

So, concerning (3). Your plan is to train an army of students to do this for us.

#### Kevin Buzzard (May 29 2018 at 09:00):

Yes, I also do not know what the best way forward is. Here are some things that need doing.

#### Kevin Buzzard (May 29 2018 at 09:00):

1) I should look at your code and review it

#### Kevin Buzzard (May 29 2018 at 09:00):

2) Someone should look at my schemes code and review it

#### Kevin Buzzard (May 29 2018 at 09:00):

3) A group of people should define a perfectoid space before 1st August

#### Kevin Buzzard (May 29 2018 at 09:00):

I am unclear about how important it is to put those things in an appropriate order

#### Johan Commelin (May 29 2018 at 09:01):

2) Someone should look at my schemes code and review it

I could try to be that someone. But I guess that doesn't help. I can't give much feedback on the Lean... and I'm quite sure that the maths is fine (-; After all, Lean thinks its fine. So I definitely want to review it. But I guess the only one gaining something from that is myself.

#### Johan Commelin (May 29 2018 at 09:02):

1) is not very important. That can wait.

#### Johan Commelin (May 29 2018 at 09:02):

Sounds like Assia wants to look at your scheme code as well.

#### Johan Commelin (May 29 2018 at 09:06):

Ok, Kevin, I've attended a seminar on perfectoid spaces. And I have seen some talks on them (including one by you). Do you think the complexity of the definition is much beyond that of schemes? To me it seems like you need to prove some stuff on power-bounded elements and such, and otherwise you just run the "sheaf of rings on a space" machinery, with a different model of affines.

#### Johan Commelin (May 29 2018 at 09:06):

But of course that is hopelessly naive. Both math-wise and lean-wise, I guess.

#### Kevin Buzzard (May 29 2018 at 09:07):

No, I think defining a perfectoid space will be easy

#### Kevin Buzzard (May 29 2018 at 09:07):

that's why I'm so keen to do it

#### Kevin Buzzard (May 29 2018 at 09:07):

I can see no obstruction

#### Kevin Buzzard (May 29 2018 at 09:08):

and if we find an obstruction

#### Kevin Buzzard (May 29 2018 at 09:08):

but if we find an obstruction

#### Kevin Buzzard (May 29 2018 at 09:08):

I am optimistic the CS guys will fix it

#### Kevin Buzzard (May 29 2018 at 09:08):

because look at my horrible pre_semi_sheaf question

#### Kevin Buzzard (May 29 2018 at 09:08):

those goals looked awful

#### Kevin Buzzard (May 29 2018 at 09:08):

and they fixed it

#### Johan Commelin (May 29 2018 at 09:09):

Ok... do you want to do it in a separate project? Or in a feature branch of mathlib?

#### Johan Commelin (May 29 2018 at 09:13):

because look at my horrible pre_semi_sheaf question
those goals looked awful
and they fixed it

Yes, that was fantastic.

#### Sean Leather (May 29 2018 at 09:13):

Ok... do you want to do it in a separate project? Or in a feature branch of mathlib?

I recommend not starting from a fork of mathlib. Your compile times will generally be faster. You can always add it to mathlib later.

#### Johan Commelin (May 29 2018 at 09:14):

Ok, I developed simplicial sets in a feature branch. And I was quite happy.

#### Johan Commelin (May 29 2018 at 09:15):

The positive side is that it is very easy to make small improvements to mathlib when you need them.

#### Johan Commelin (May 29 2018 at 09:15):

For example, I made small changes to fin and later added nnreal, and I got those merged before my current PR.

#### Sean Leather (May 29 2018 at 09:16):

I've done both, and I was happier not starting from mathlib. :smile:

#### Sean Leather (May 29 2018 at 09:17):

I just add files to the same directory as mathlib that I intend to place them. It's just as easy.

#### Kevin Buzzard (May 29 2018 at 17:50):

Oh that's a nice idea

#### Kevin Buzzard (May 29 2018 at 17:50):

I was just mulling over this sort of thing myself.

#### Scott Morrison (May 29 2018 at 23:07):

I think an advantage of working in a feature branch of mathlib is that it keeps at the front of your mind that it's important that new work is eventually merged into mathlib.

#### Scott Morrison (May 29 2018 at 23:08):

(Otherwise, the work is lost. Of course, indirect consequences of the work, such as inspiring people to think about interactive theorem proving through talks, may survive.)

#### Scott Morrison (May 29 2018 at 23:08):

Not that I am doing this myself. But as soon as I have satisfactory resolution of handling universes in category theory (getting there?), next up should be a PR. :-)

#### Kevin Buzzard (May 29 2018 at 23:19):

Johan Commelin suggests that I wait for you before defining more sheaves of things

#### Kevin Buzzard (May 29 2018 at 23:19):

and perfectoid spaces have sheaves of topological rings...

#### Johan Commelin (May 30 2018 at 03:06):

But Johan Commelin is a layman, who doesn't know anything about proper writing of structures and interfaces. I guess he thinks you just use some abstract category theory imported from Scott's library, and then definitions become 1-liners. But he forgets that you will still need a lot of interface writing. And this interface writing may or may not become more complicated with the overhead of the category lib. Johan has no clue whether this is a good idea or not.

#### Scott Morrison (May 30 2018 at 03:12):

I'm really sorry about being slow. I am feeling lame about not finishing real papers recently, and trying to get some non-Lean work done. Given the perfectoid spaces project is not immediately planning on contributing to mathlib (tsk) perhaps I could give you a relatively stable version of my category theory library to use as a dependency, and once (I mustn't say "if") I get it PR'd into mathlib it should be relatively easy to replumb.

#### Johan Commelin (May 30 2018 at 03:13):

No worries. We all have other obligations as well (-;

#### Johan Commelin (May 30 2018 at 03:14):

The thing is: I really am a layman. I have no clue whether you lib will allow us to write shorter code. Or whether we still need to write lots of plumbing stuff. I just don't have enough experience with formalisations to have good intuition about this.

#### Johan Commelin (May 30 2018 at 03:15):

In maths you would say: "Look, Scott has written a book on category theory! Let's just refer to that, instead of writing a 50 page appendix ourselves. That will save us 50 pages!"

#### Johan Commelin (May 30 2018 at 03:15):

But it seems like it might not work that way in Lean.

#### Patrick Massot (May 30 2018 at 07:05):

Of course, indirect consequences of the work, such as inspiring people to think about interactive theorem proving through talks, may survive.

#### Johan Commelin (Nov 22 2018 at 19:25):

I tried to update my simplicial branch today: https://github.com/leanprover-community/mathlib/blob/simplicial/algebraic_topology/simplicial_set.lean#L188 is the proof that boundary (boundary x) = 0.

#### Johan Commelin (Nov 22 2018 at 19:27):

I do have some issues with pmf.map f where f is a function between two fintypes. This should be continuous for the subspace topology. And I had a working proof. But in the last months, the topology on nnreal has changed, using uniform spaces. Now my proof seems pretty broken.

#### Johan Commelin (Nov 22 2018 at 19:27):

If any of the uniform spaces wizards want to help me out there, that would be cool.

#### Johan Commelin (Nov 22 2018 at 19:42):

@Reid Barton I think that I would like to make use of all the machinery that you have developed in you homotopy repo. So I won't push this much further. At least now the files are somewhat up to date with mathlib again.

#### Johan Commelin (Nov 22 2018 at 20:28):

@Mario Carneiro So now I have a proof that

lemma lboundary_lboundary : (lboundary R M X n).comp (lboundary R M X (n+1)) = 0 :=


#### Mario Carneiro (Nov 23 2018 at 08:30):

I don't know what you are talking about but I'm happy to take credit

#### Johan Commelin (Nov 23 2018 at 08:30):

That's so concise! You'dd almost call it normal math.

#### Johan Commelin (Nov 23 2018 at 08:30):

boundary is a map between to modules. And there you have it.

#### Johan Commelin (Nov 23 2018 at 08:31):

The only difference from regular math is pretty printing

#### Johan Commelin (Nov 23 2018 at 08:33):

It's using the fact that linear_map is a group. It is really nice that this Just Works™

#### Johan Commelin (Nov 23 2018 at 08:37):

@Mario Carneiro Did you also prove that composition of linear maps is bilinear?

#### Mario Carneiro (Nov 23 2018 at 08:37):

yeah, that's lcomp or llcomp

#### Johan Commelin (Nov 23 2018 at 08:37):

Otherwise that would be a natural step in @Reid Bartons challenge.

Ok, cool.

#### Mario Carneiro (Nov 23 2018 at 08:38):

llcomp is linear in all the ways

#### Reid Barton (Nov 23 2018 at 14:23):

btw,  : ℤ isn't necessary there

#### Reid Barton (Nov 23 2018 at 14:24):

And yes, I was pretty happy about how easy it was to write down this statement. Now let's see how the proof turns out :)

#### Johan Commelin (Nov 23 2018 at 14:57):

Yes, I think that we need to change the definition of composition to llcomp g f. After that, there is map_sum for linear_maps. If that works, I think we are good to go. I'll try it when I'm home.

#### Johan Commelin (Nov 23 2018 at 15:51):

@Reid Barton Sadly, this gives a failure

instance RMod_category : category (RMod R) :=
{ hom := λ M N, M →ₗ N,
id := λ M, linear_map.id,
comp := λ M N P f g, linear_map.llcomp M N P g f }


Once again, Lean can not find the ring over which M is a module...

#### Reid Barton (Nov 23 2018 at 15:53):

I'm confused, why are you trying to use llcomp?

#### Johan Commelin (Nov 23 2018 at 15:55):

Because then I can pull sum through the linear map that is composition.

#### Reid Barton (Nov 23 2018 at 15:57):

I see. So in the level of generality that I picked (RMod for a not necessarily commutative ring), the homs are only abelian groups, not modules. Of course, this is still enough but we have to use this additivity somehow

#### Johan Commelin (Nov 23 2018 at 15:57):

Aah, yes, I changed R to comm_ring, but that is not the problem I think.

#### Johan Commelin (Nov 23 2018 at 15:57):

It is still maxing out on some typeclass search

#### Reid Barton (Nov 23 2018 at 15:57):

Well, there is no reason it should not work for ring as well, or any additive category even

#### Johan Commelin (Nov 23 2018 at 15:59):

Sure, but we don't have enriched categories etc

#### Reid Barton (Nov 23 2018 at 15:59):

what about just proving the equality element-wise?

#### Reid Barton (Nov 23 2018 at 15:59):

Well, in any case, comp cannot be llcomp, because it has the wrong type. Right?

#### Johan Commelin (Nov 23 2018 at 15:59):

llcomp g f should be an element of linear_map M P

Or, sorry

#### Johan Commelin (Nov 23 2018 at 16:00):

because llcomp is cast to a function that eats g, etc...

#### Reid Barton (Nov 23 2018 at 16:00):

So how can llcomp help

#### Johan Commelin (Nov 23 2018 at 16:00):

llcomp boundary is a linear map

#### Reid Barton (Nov 23 2018 at 16:01):

is the idea to get an expression containing a coercion of llcomp, so that some lemma can see it's linear?

#### Reid Barton (Nov 23 2018 at 16:02):

This sounds kind of fragile to me

why?

It just does?

#### Reid Barton (Nov 23 2018 at 16:03):

Easy to imagine the simplifier deciding to rewrite llcomp f g to lcomp f g or whatever

#### Reid Barton (Nov 23 2018 at 16:03):

and then you're stuck

#### Johan Commelin (Nov 23 2018 at 16:04):

That would be lcomp g f because of [see above]

#### Johan Commelin (Nov 23 2018 at 16:04):

Anyway, I'm sidetracking.

#### Johan Commelin (Nov 23 2018 at 16:04):

Ok, I'll just change to the llcomp expression inside my proof.

#### Reid Barton (Nov 23 2018 at 16:11):

What lemma are you using to pull the sum through the composition?

#### Johan Commelin (Nov 23 2018 at 16:13):

algebra/module.lean:@[simp] lemma map_sum

#### Johan Commelin (Nov 23 2018 at 16:13):

That was my plan, at least.

I see

hmm

#### Reid Barton (Nov 23 2018 at 16:23):

Maybe it's better to make lemmas like sum_comp/comp_sum phrased in terms of the category composition and then write the proof in terms of those

#### Johan Commelin (Nov 23 2018 at 18:35):

set_option class.instance_max_depth 100


I found this at the top of the tensor_product file. That was why the llcomp stuff wasn't working (@Reid Barton)
Seems a bit fragile indeed...

#### Johan Commelin (Nov 23 2018 at 19:00):

@Reid Barton I just pushed some stuff. I can indeed copy most of my previous proof. I need one more little simp-lemma near the end. But I now need to do some other stuff first...

#### Johan Commelin (Nov 23 2018 at 20:22):

@Reid Barton Done.

#### Reid Barton (Nov 23 2018 at 20:23):

I just did it too :)

Ooh, sorry...

#### Johan Commelin (Nov 23 2018 at 20:23):

Are our proofs homotopic?

#### Johan Commelin (Nov 23 2018 at 20:23):

Oooh, wait... this isn't HoTT

#### Reid Barton (Nov 23 2018 at 20:25):

They're pretty similar

#### Reid Barton (Nov 23 2018 at 20:28):

I added a bunch of lemmas for bilinearity of composition (without proofs)
https://github.com/leanprover-community/mathlib/blob/simplicial2/category_theory/examples/modules.lean#L35

#### Johan Commelin (Nov 23 2018 at 20:31):

Ok, now I should really get back to sheaves

#### Johan Commelin (Nov 23 2018 at 20:31):

But I'm a bit stuck there...

Last updated: May 06 2021 at 19:30 UTC