simplicial complexes in lean

Stream: maths

[Johan Commelin]

Now we have simplicial complexes!

[Johan Commelin]

And also the singular complex

[Johan Commelin]

With coefficients in arbitrary \Z-modules

[Johan Commelin]

See https://github.com/jcommelin/mathlib/tree/simplicial

[Patrick Massot]

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]

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

[Johan Commelin]

I have no idea what that does...

[Patrick Massot]

Uses congruence exactly once

[Patrick Massot]

congruence is something we wouldn't bother to state

[Johan Commelin]

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

[Patrick Massot]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Massot]

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

[Johan Commelin]

Ok, fair enough

[Patrick Massot]

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

[Johan Commelin]

So, now begins the ugly part...

[Johan Commelin]

cleaning up the proof

[Patrick Massot]

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

[Johan Commelin]

I cleaned up that line

[Johan Commelin]

I also added some user comments to the definitions

[Johan Commelin]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

I stopped when I went below 150 lines

[Patrick Massot]

I hope you can learn stuff from the diff

[Patrick Massot]

But keep in mind these are only local edits

[Johan Commelin]

Thanks! I'm looking at it!

[Patrick Massot]

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

[Patrick Massot]

and using calc would almost certainly make a more readable proof

[Patrick Massot]

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]

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

[Kenny Lau]

don't use it :P

[Patrick Massot]

Reading the doc is a good start

[Johan Commelin]

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

[Patrick Massot]

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

[Kevin Buzzard]

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]

@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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

1) I should look at your code and review it

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Johan Commelin]

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]

1) is not very important. That can wait.

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Kevin Buzzard]

No, I think defining a perfectoid space will be easy

[Kevin Buzzard]

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

[Kevin Buzzard]

I can see no obstruction

[Kevin Buzzard]

and if we find an obstruction

[Kevin Buzzard]

then we learn more about whether Lean is an appropriate place to do interesting mathematics

[Kevin Buzzard]

but if we find an obstruction

[Kevin Buzzard]

I am optimistic the CS guys will fix it

[Kevin Buzzard]

because look at my horrible pre_semi_sheaf question

[Kevin Buzzard]

those goals looked awful

[Kevin Buzzard]

and they fixed it

[Johan Commelin]

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

[Johan Commelin]

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

Yes, that was fantastic.

[Sean Leather]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Sean Leather]

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

[Sean Leather]

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

[Kevin Buzzard]

Oh that's a nice idea

[Kevin Buzzard]

I was just mulling over this sort of thing myself.

[Scott Morrison]

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]

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

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]

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

[Kevin Buzzard]

and perfectoid spaces have sheaves of topological rings...

[Johan Commelin]

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]

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]

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

[Johan Commelin]

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]

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]

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

[Patrick Massot]

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

Did you already gave talks about interactive theorem proving?

[Johan Commelin]

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]

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]

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

[Johan Commelin]

@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]

@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 :=
ext $ λ x, boundary_boundary _ _ _ _

Is there now an easy way to take homology? What is the correct way to do that?

[Reid Barton]

Which machinery did you have in mind?

[Johan Commelin]

Aah, the stuff about cylinders etc

[Reid Barton]

Can we do a version for simplicial modules now?

[Johan Commelin]

I do not have a working functor Top to simplicial_set yet. It is a bit annoying.

[Johan Commelin]

But the other pieces are now becoming quite nice.

[Johan Commelin]

Also, I guess I should call them simplicial types? And the category should be sType?

[Reid Barton]

That is--this argument also works to show that the (unnormalized) chain complex associated to any simplicial module is in fact a chain complex. The original simplicial module doesn't have to be free.

[Reid Barton]

I don't know whether that will make the proof any easier

[Reid Barton]

https://ncatlab.org/nlab/show/Moore+complex#ForSimplicialAbelianGroups

[Johan Commelin]

Aaah, I don't know anything about this.

[Johan Commelin]

Are you planning to PR parts of your project into mathlib in the near future?

[Reid Barton]

Probably not the near future. It's more likely that I will do a "version 2.0" of some parts in the less near future.

[Johan Commelin]

Aha

[Reid Barton]

But, it depends on the part. Some stuff about Top could probably be PRed relatively soon without many changes

[Reid Barton]

Let me see if I can read your proof

[Johan Commelin]

It would be nice to have singular homology

[Reid Barton]

I wrote out a plan for it in a comment on one of your earlier PRs

[Reid Barton]

what's the story with the topological simplices functor?

[Reid Barton]

Delta -> Top

[Reid Barton]

Something broke with it?

[Johan Commelin]

https://github.com/leanprover/mathlib/pull/144#issuecomment-425715546

[Johan Commelin]

Yes, that's broken...

[Johan Commelin]

And I didn't see an obvious fix. The topology on pmf [n] is now no longer a subspace topology of a Pi-topology. But a subspace of some uniform thing.

[Johan Commelin]

And my uniform-fu is nil.

[Reid Barton]

Technically we can do all this right now I think, without even waiting for limits or adjunctions

[Johan Commelin]

Yes, apart from this stupid brokenness, all the other parts are mostly there.

[Johan Commelin]

I didn't abstract complexes yet.

[Johan Commelin]

Did you do complexes somewhere?

[Johan Commelin]

I know that we had some discussion here on zulip a long time ago.

[Reid Barton]

Not yet

[Johan Commelin]

@Patrick Massot Are you interested in exercising your mastery of uniform spaces again?

[Patrick Massot]

I can try

[Patrick Massot]

Did you already precisely described the problem? I didn't read carefully

[Patrick Massot]

Is there something I could clone?

[Johan Commelin]

Nope, there is a broken proof. It used to work, long ago. But then uniform spaces came along, and now it is broken.

[Johan Commelin]

simplicial branch on community mathlib

[Patrick Massot]

did you push everything relevant to that branch?

[Johan Commelin]

https://github.com/leanprover-community/mathlib/blob/simplicial/algebraic_topology/standard_topological_simplex.lean#L31

[Johan Commelin]

That might not be the exact statement that you want to prove...

[Johan Commelin]

You could generalise to any f : X → Y where X and Y are fintypes.

[Johan Commelin]

you get an induced map pmf.map f

[Johan Commelin]

And that should be continuous

[Johan Commelin]

We will then apply this to monotone maps between [n] and [m]

[Patrick Massot]

@Johan Commelin I investigate a bit. There isn't much uniform space here, only metric space. The seemingly missing lemma is:

lemma metric_pi_topology {α : Type*} {π : α → Type*} [fintype α] [∀ a, metric_space (π a)]:
  (@metric_space_pi _ π _ _).to_uniform_space.to_topological_space = @Pi.topological_space _ π _ :=
sorry

[Patrick Massot]

Which says the topology on a finite product of metric spaces is the product topology. It probably used to be rfl but isn't.

[Patrick Massot]

After proving that lemma, typing:

variables {α : Type*} {β : Type*} [fintype α] [fintype β]

def pmf_top : topological_space (pmf α) := subtype.topological_space
local attribute [instance] pmf_top
lemma map.cont  (f : α → β) :
  continuous (pmf.map f) :=
begin
  apply continuous_subtype_mk,
  rw metric_pi_topology,
  apply continuous_pi,
  intro j,
  sorry
end

should put you back on track

[Patrick Massot]

because then theorem map.continuous (f : [m] → [n]) : continuous (map f) := map.cont f

[Patrick Massot]

It may be better to state a continuous_metric_pi with proof containing the rw metric_pi_topology which we'd rather keep hidden

[Patrick Massot]

Clearly the definition metric_space_pi currently lacks proper API. @Sebastien Gouezel and @Johannes Hölzl do you have opinons about that (you don't need to read anything before this monologue)?

[Reid Barton]

@Johan Commelin I pushed an "exercise" for you, in https://github.com/leanprover-community/mathlib/blob/simplicial/algebraic_topology/simplicial_module.lean

[Reid Barton]

It should be a proper subset of your existing boundary_boundary proof, I hope.

[Johan Commelin]

@Patrick Massot Thanks a lot for investigating. I'll connect the pieces together now.

[Johan Commelin]

@Reid Barton Thanks! I'll take a look.

[Patrick Massot]

Johan, are you working on this product topology vs product metric? Or do you need help?

[Johan Commelin]

I just finished some bureaucracy. I'll look at it now

[Patrick Massot]

It probably requires quite a bit of preparation if you want to do it right

[Patrick Massot]

including figuring out what is already in mathlib

[Patrick Massot]

stuff like the base of the product topology in terms of open subsets in the factors, maybe some congr lemma for topologies, balls in the product metric space is products of balls etc.

[Patrick Massot]

maybe also things like projection on factors is an open map

[Johan Commelin]

@Patrick Massot Why do your fintypes have such strange names? Did you give up on X and Y?

[Patrick Massot]

I copied and pasted too much. The idea of using π in {π : α → Type*} [fintype α] [∀ a, metric_space (π a)] is also a nightmare, since there are Pi-type mixed with π map everywhere then

[Johan Commelin]

@Patrick Massot Ok, my proof works again, modulo the lemma. It is a bit scary (in the sense of unmathematical) to do rewrites that don't change the pretty printed goal. But I guess it is fine.

[Patrick Massot]

Which lemma? metric_pi_topology?

[Johan Commelin]

Right, that one.

[Johan Commelin]

I need to dive into mathlib to figure out how to prove that...

[Patrick Massot]

Do you want me to try proving it?

[Patrick Massot]

I'd rather have you work on sheaves or that localization API hole

[Johan Commelin]

Yeah, I should stop again with this project. I needed to do something else than sheaves for a day. But now I should return.

[Johan Commelin]

@Reid Barton How did Lean figure out that your definition of boundary is a linear map?! That's really slick!

[Johan Commelin]

Kudos to @Mario Carneiro

[Johan Commelin]

def simplicial_module := simplicial_object (RMod R)

section

variables {R} (X : simplicial_module R)

local notation ` [`n`] ` := simplex_category.from_nat n

def boundary (n : ℕ) : X.obj [n+1] ⟶ X.obj [n] :=
sum univ $ λ i : [n+1], gsmul ((-1 : ℤ)^i.val) (X.δ i)

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

The only difference from regular math is pretty printing

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

yeah, that's lcomp or llcomp

[Johan Commelin]

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

[Johan Commelin]

Ok, cool.

[Mario Carneiro]

llcomp is linear in all the ways

[Reid Barton]

btw, : ℤ isn't necessary there

[Reid Barton]

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]

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]

@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]

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

[Johan Commelin]

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

[Reid Barton]

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]

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

[Johan Commelin]

It is still maxing out on some typeclass search

[Reid Barton]

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

[Johan Commelin]

Sure, but we don't have enriched categories etc

[Reid Barton]

what about just proving the equality element-wise?

[Reid Barton]

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

[Johan Commelin]

llcomp g f should be an element of linear_map M P

[Reid Barton]

Or, sorry

[Johan Commelin]

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

[Reid Barton]

So how can llcomp help

[Johan Commelin]

llcomp boundary is a linear map

[Reid Barton]

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

[Reid Barton]

This sounds kind of fragile to me

[Johan Commelin]

why?

[Reid Barton]

It just does?

[Reid Barton]

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

[Reid Barton]

and then you're stuck

[Johan Commelin]

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

[Johan Commelin]

Anyway, I'm sidetracking.

[Johan Commelin]

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

[Reid Barton]

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

[Johan Commelin]

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

[Johan Commelin]

That was my plan, at least.

[Reid Barton]

I see

[Reid Barton]

hmm

[Reid Barton]

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]

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]

@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]

@Reid Barton Done.

[Reid Barton]

I just did it too :)

[Johan Commelin]

Ooh, sorry...

[Johan Commelin]

Are our proofs homotopic?

[Johan Commelin]

Oooh, wait... this isn't HoTT

[Reid Barton]

They're pretty similar

[Reid Barton]

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]

Ok, now I should really get back to sheaves

[Johan Commelin]

But I'm a bit stuck there...