Zulip Chat Archive

Stream: maths

Topic: simplicial complexes in lean


view this post on Zulip Johan Commelin (May 28 2018 at 12:13):

Now we have simplicial complexes!

view this post on Zulip Johan Commelin (May 28 2018 at 12:13):

And also the singular complex

view this post on Zulip Johan Commelin (May 28 2018 at 12:14):

With coefficients in arbitrary \Z-modules

view this post on Zulip Johan Commelin (May 28 2018 at 12:14):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 28 2018 at 12:14):

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

view this post on Zulip Johan Commelin (May 28 2018 at 12:15):

I have no idea what that does...

view this post on Zulip Patrick Massot (May 28 2018 at 12:15):

Uses congruence exactly once

view this post on Zulip Patrick Massot (May 28 2018 at 12:15):

congruence is something we wouldn't bother to state

view this post on Zulip 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...

view this post on Zulip Patrick Massot (May 28 2018 at 12:15):

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

view this post on Zulip Johan Commelin (May 28 2018 at 12:16):

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

view this post on Zulip Johan Commelin (May 28 2018 at 12:16):

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

view this post on Zulip Patrick Massot (May 28 2018 at 12:17):

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

view this post on Zulip Johan Commelin (May 28 2018 at 12:17):

Ok, fair enough

view this post on Zulip Patrick Massot (May 28 2018 at 12:17):

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

view this post on Zulip Johan Commelin (May 28 2018 at 12:18):

So, now begins the ugly part...

view this post on Zulip Johan Commelin (May 28 2018 at 12:19):

cleaning up the proof

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 28 2018 at 13:01):

I cleaned up that line

view this post on Zulip Johan Commelin (May 28 2018 at 13:01):

I also added some user comments to the definitions

view this post on Zulip Johan Commelin (May 28 2018 at 13:01):

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

view this post on Zulip Patrick Massot (May 28 2018 at 14:56):

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

view this post on Zulip Patrick Massot (May 28 2018 at 14:57):

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

view this post on Zulip Patrick Massot (May 28 2018 at 14:57):

I stopped when I went below 150 lines

view this post on Zulip Patrick Massot (May 28 2018 at 14:57):

I hope you can learn stuff from the diff

view this post on Zulip Patrick Massot (May 28 2018 at 14:57):

But keep in mind these are only local edits

view this post on Zulip Johan Commelin (May 28 2018 at 14:58):

Thanks! I'm looking at it!

view this post on Zulip Patrick Massot (May 28 2018 at 14:58):

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

view this post on Zulip Patrick Massot (May 28 2018 at 14:58):

and using calc would almost certainly make a more readable proof

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kenny Lau (May 28 2018 at 16:51):

don't use it :P

view this post on Zulip Patrick Massot (May 28 2018 at 16:53):

Reading the doc is a good start

view this post on Zulip Johan Commelin (May 28 2018 at 16:57):

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

view this post on Zulip 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

view this post on Zulip 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? :-)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 29 2018 at 09:00):

1) I should look at your code and review it

view this post on Zulip Kevin Buzzard (May 29 2018 at 09:00):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 09:00):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 09:00):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 29 2018 at 09:02):

1) is not very important. That can wait.

view this post on Zulip Johan Commelin (May 29 2018 at 09:02):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 29 2018 at 09:06):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 09:07):

No, I think defining a perfectoid space will be easy

view this post on Zulip Kevin Buzzard (May 29 2018 at 09:07):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 09:07):

I can see no obstruction

view this post on Zulip Kevin Buzzard (May 29 2018 at 09:08):

and if we find an obstruction

view this post on Zulip Kevin Buzzard (May 29 2018 at 09:08):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 09:08):

but if we find an obstruction

view this post on Zulip Kevin Buzzard (May 29 2018 at 09:08):

I am optimistic the CS guys will fix it

view this post on Zulip Kevin Buzzard (May 29 2018 at 09:08):

because look at my horrible pre_semi_sheaf question

view this post on Zulip Kevin Buzzard (May 29 2018 at 09:08):

those goals looked awful

view this post on Zulip Kevin Buzzard (May 29 2018 at 09:08):

and they fixed it

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 29 2018 at 09:14):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Sean Leather (May 29 2018 at 09:16):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 29 2018 at 17:50):

Oh that's a nice idea

view this post on Zulip Kevin Buzzard (May 29 2018 at 17:50):

I was just mulling over this sort of thing myself.

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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. :-)

view this post on Zulip Kevin Buzzard (May 29 2018 at 23:19):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 23:19):

and perfectoid spaces have sheaves of topological rings...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 30 2018 at 03:13):

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

view this post on Zulip 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.

view this post on Zulip 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!"

view this post on Zulip Johan Commelin (May 30 2018 at 03:15):

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

view this post on Zulip 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.

Did you already gave talks about interactive theorem proving?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 :=
ext $ λ x, boundary_boundary _ _ _ _

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

view this post on Zulip Reid Barton (Nov 22 2018 at 20:28):

Which machinery did you have in mind?

view this post on Zulip Johan Commelin (Nov 22 2018 at 20:28):

Aah, the stuff about cylinders etc

view this post on Zulip Reid Barton (Nov 22 2018 at 20:28):

Can we do a version for simplicial modules now?

view this post on Zulip Johan Commelin (Nov 22 2018 at 20:29):

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

view this post on Zulip Johan Commelin (Nov 22 2018 at 20:29):

But the other pieces are now becoming quite nice.

view this post on Zulip Johan Commelin (Nov 22 2018 at 20:30):

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

view this post on Zulip Reid Barton (Nov 22 2018 at 20:30):

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.

view this post on Zulip Reid Barton (Nov 22 2018 at 20:30):

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

view this post on Zulip Reid Barton (Nov 22 2018 at 20:31):

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

view this post on Zulip Johan Commelin (Nov 22 2018 at 20:31):

Aaah, I don't know anything about this.

view this post on Zulip Johan Commelin (Nov 22 2018 at 20:32):

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

view this post on Zulip Reid Barton (Nov 22 2018 at 20:33):

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.

view this post on Zulip Johan Commelin (Nov 22 2018 at 20:33):

Aha

view this post on Zulip Reid Barton (Nov 22 2018 at 20:33):

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

view this post on Zulip Reid Barton (Nov 22 2018 at 20:33):

Let me see if I can read your proof

view this post on Zulip Johan Commelin (Nov 22 2018 at 20:33):

It would be nice to have singular homology

view this post on Zulip Reid Barton (Nov 22 2018 at 20:34):

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

view this post on Zulip Reid Barton (Nov 22 2018 at 20:35):

what's the story with the topological simplices functor?

view this post on Zulip Reid Barton (Nov 22 2018 at 20:35):

Delta -> Top

view this post on Zulip Reid Barton (Nov 22 2018 at 20:35):

Something broke with it?

view this post on Zulip Johan Commelin (Nov 22 2018 at 20:35):

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

view this post on Zulip Johan Commelin (Nov 22 2018 at 20:36):

Yes, that's broken...

view this post on Zulip Johan Commelin (Nov 22 2018 at 20:36):

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.

view this post on Zulip Johan Commelin (Nov 22 2018 at 20:37):

And my uniform-fu is nil.

view this post on Zulip Reid Barton (Nov 22 2018 at 20:37):

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

view this post on Zulip Johan Commelin (Nov 22 2018 at 20:38):

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

view this post on Zulip Johan Commelin (Nov 22 2018 at 20:38):

I didn't abstract complexes yet.

view this post on Zulip Johan Commelin (Nov 22 2018 at 20:43):

Did you do complexes somewhere?

view this post on Zulip Johan Commelin (Nov 22 2018 at 20:43):

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

view this post on Zulip Reid Barton (Nov 22 2018 at 20:43):

Not yet

view this post on Zulip Johan Commelin (Nov 22 2018 at 20:45):

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

view this post on Zulip Patrick Massot (Nov 22 2018 at 20:47):

I can try

view this post on Zulip Patrick Massot (Nov 22 2018 at 20:47):

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

view this post on Zulip Patrick Massot (Nov 22 2018 at 20:48):

Is there something I could clone?

view this post on Zulip Johan Commelin (Nov 22 2018 at 20:48):

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

view this post on Zulip Johan Commelin (Nov 22 2018 at 20:48):

simplicial branch on community mathlib

view this post on Zulip Patrick Massot (Nov 22 2018 at 20:48):

did you push everything relevant to that branch?

view this post on Zulip Johan Commelin (Nov 22 2018 at 20:49):

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

view this post on Zulip Johan Commelin (Nov 22 2018 at 20:49):

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

view this post on Zulip Johan Commelin (Nov 22 2018 at 20:49):

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

view this post on Zulip Johan Commelin (Nov 22 2018 at 20:50):

you get an induced map pmf.map f

view this post on Zulip Johan Commelin (Nov 22 2018 at 20:50):

And that should be continuous

view this post on Zulip Johan Commelin (Nov 22 2018 at 20:50):

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

view this post on Zulip Patrick Massot (Nov 22 2018 at 21:40):

@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

view this post on Zulip Patrick Massot (Nov 22 2018 at 21:40):

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

view this post on Zulip Patrick Massot (Nov 22 2018 at 21:41):

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

view this post on Zulip Patrick Massot (Nov 22 2018 at 21:42):

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

view this post on Zulip Patrick Massot (Nov 22 2018 at 21:44):

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

view this post on Zulip Patrick Massot (Nov 22 2018 at 21:45):

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

view this post on Zulip Reid Barton (Nov 23 2018 at 01:06):

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

view this post on Zulip Reid Barton (Nov 23 2018 at 01:06):

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

view this post on Zulip Johan Commelin (Nov 23 2018 at 05:10):

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

view this post on Zulip Johan Commelin (Nov 23 2018 at 05:10):

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

view this post on Zulip Patrick Massot (Nov 23 2018 at 07:53):

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

view this post on Zulip Johan Commelin (Nov 23 2018 at 07:53):

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

view this post on Zulip Patrick Massot (Nov 23 2018 at 07:53):

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

view this post on Zulip Patrick Massot (Nov 23 2018 at 07:54):

including figuring out what is already in mathlib

view this post on Zulip Patrick Massot (Nov 23 2018 at 07:55):

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.

view this post on Zulip Patrick Massot (Nov 23 2018 at 07:55):

maybe also things like projection on factors is an open map

view this post on Zulip Johan Commelin (Nov 23 2018 at 07:57):

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

view this post on Zulip Patrick Massot (Nov 23 2018 at 07:59):

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

view this post on Zulip Johan Commelin (Nov 23 2018 at 08:22):

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

view this post on Zulip Patrick Massot (Nov 23 2018 at 08:23):

Which lemma? metric_pi_topology?

view this post on Zulip Johan Commelin (Nov 23 2018 at 08:25):

Right, that one.

view this post on Zulip Johan Commelin (Nov 23 2018 at 08:26):

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

view this post on Zulip Patrick Massot (Nov 23 2018 at 08:26):

Do you want me to try proving it?

view this post on Zulip Patrick Massot (Nov 23 2018 at 08:26):

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

view this post on Zulip Johan Commelin (Nov 23 2018 at 08:29):

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

view this post on Zulip Johan Commelin (Nov 23 2018 at 08:29):

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

view this post on Zulip Johan Commelin (Nov 23 2018 at 08:29):

Kudos to @Mario Carneiro

view this post on Zulip Johan Commelin (Nov 23 2018 at 08:30):

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)

view this post on Zulip Mario Carneiro (Nov 23 2018 at 08:30):

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

view this post on Zulip Johan Commelin (Nov 23 2018 at 08:30):

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

view this post on Zulip Johan Commelin (Nov 23 2018 at 08:30):

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

view this post on Zulip Johan Commelin (Nov 23 2018 at 08:31):

The only difference from regular math is pretty printing

view this post on Zulip 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™

view this post on Zulip Johan Commelin (Nov 23 2018 at 08:37):

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

view this post on Zulip Mario Carneiro (Nov 23 2018 at 08:37):

yeah, that's lcomp or llcomp

view this post on Zulip Johan Commelin (Nov 23 2018 at 08:37):

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

view this post on Zulip Johan Commelin (Nov 23 2018 at 08:37):

Ok, cool.

view this post on Zulip Mario Carneiro (Nov 23 2018 at 08:38):

llcomp is linear in all the ways

view this post on Zulip Reid Barton (Nov 23 2018 at 14:23):

btw, : ℤ isn't necessary there

view this post on Zulip 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 :)

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Reid Barton (Nov 23 2018 at 15:53):

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

view this post on Zulip Johan Commelin (Nov 23 2018 at 15:55):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 23 2018 at 15:57):

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

view this post on Zulip Johan Commelin (Nov 23 2018 at 15:57):

It is still maxing out on some typeclass search

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 23 2018 at 15:59):

Sure, but we don't have enriched categories etc

view this post on Zulip Reid Barton (Nov 23 2018 at 15:59):

what about just proving the equality element-wise?

view this post on Zulip Reid Barton (Nov 23 2018 at 15:59):

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

view this post on Zulip Johan Commelin (Nov 23 2018 at 15:59):

llcomp g f should be an element of linear_map M P

view this post on Zulip Reid Barton (Nov 23 2018 at 16:00):

Or, sorry

view this post on Zulip Johan Commelin (Nov 23 2018 at 16:00):

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

view this post on Zulip Reid Barton (Nov 23 2018 at 16:00):

So how can llcomp help

view this post on Zulip Johan Commelin (Nov 23 2018 at 16:00):

llcomp boundary is a linear map

view this post on Zulip 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?

view this post on Zulip Reid Barton (Nov 23 2018 at 16:02):

This sounds kind of fragile to me

view this post on Zulip Johan Commelin (Nov 23 2018 at 16:02):

why?

view this post on Zulip Reid Barton (Nov 23 2018 at 16:03):

It just does?

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 23 2018 at 16:03):

and then you're stuck

view this post on Zulip Johan Commelin (Nov 23 2018 at 16:04):

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

view this post on Zulip Johan Commelin (Nov 23 2018 at 16:04):

Anyway, I'm sidetracking.

view this post on Zulip Johan Commelin (Nov 23 2018 at 16:04):

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

view this post on Zulip Reid Barton (Nov 23 2018 at 16:11):

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

view this post on Zulip Johan Commelin (Nov 23 2018 at 16:13):

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

view this post on Zulip Johan Commelin (Nov 23 2018 at 16:13):

That was my plan, at least.

view this post on Zulip Reid Barton (Nov 23 2018 at 16:14):

I see

view this post on Zulip Reid Barton (Nov 23 2018 at 16:14):

hmm

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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...

view this post on Zulip Johan Commelin (Nov 23 2018 at 20:22):

@Reid Barton Done.

view this post on Zulip Reid Barton (Nov 23 2018 at 20:23):

I just did it too :)

view this post on Zulip Johan Commelin (Nov 23 2018 at 20:23):

Ooh, sorry...

view this post on Zulip Johan Commelin (Nov 23 2018 at 20:23):

Are our proofs homotopic?

view this post on Zulip Johan Commelin (Nov 23 2018 at 20:23):

Oooh, wait... this isn't HoTT

view this post on Zulip Reid Barton (Nov 23 2018 at 20:25):

They're pretty similar

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 23 2018 at 20:31):

Ok, now I should really get back to sheaves

view this post on Zulip Johan Commelin (Nov 23 2018 at 20:31):

But I'm a bit stuck there...


Last updated: May 06 2021 at 19:30 UTC