Zulip Chat Archive

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

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

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

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

Johan Commelin (May 28 2018 at 12:17):

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

I also added some user comments to the definitions

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?

Kenny Lau (May 28 2018 at 16:51):

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

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

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.

Did you already gave talks about interactive theorem proving?

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

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

Reid Barton (Nov 22 2018 at 20:28):

Which machinery did you have in mind?

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

Aah, the stuff about cylinders etc

Reid Barton (Nov 22 2018 at 20:28):

Can we do a version for simplicial modules now?

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.

Johan Commelin (Nov 22 2018 at 20:29):

But the other pieces are now becoming quite nice.

Johan Commelin (Nov 22 2018 at 20:30):

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

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.

Reid Barton (Nov 22 2018 at 20:30):

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

Reid Barton (Nov 22 2018 at 20:31):

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

Johan Commelin (Nov 22 2018 at 20:31):

Aaah, I don't know anything about this.

Johan Commelin (Nov 22 2018 at 20:32):

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

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.

Johan Commelin (Nov 22 2018 at 20:33):

Aha

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

Reid Barton (Nov 22 2018 at 20:33):

Let me see if I can read your proof

Johan Commelin (Nov 22 2018 at 20:33):

It would be nice to have singular homology

Reid Barton (Nov 22 2018 at 20:34):

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

Reid Barton (Nov 22 2018 at 20:35):

what's the story with the topological simplices functor?

Reid Barton (Nov 22 2018 at 20:35):

Delta -> Top

Reid Barton (Nov 22 2018 at 20:35):

Something broke with it?

Johan Commelin (Nov 22 2018 at 20:35):

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

Johan Commelin (Nov 22 2018 at 20:36):

Yes, that's broken...

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.

Johan Commelin (Nov 22 2018 at 20:37):

And my uniform-fu is nil.

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

Johan Commelin (Nov 22 2018 at 20:38):

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

Johan Commelin (Nov 22 2018 at 20:38):

I didn't abstract complexes yet.

Johan Commelin (Nov 22 2018 at 20:43):

Did you do complexes somewhere?

Johan Commelin (Nov 22 2018 at 20:43):

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

Reid Barton (Nov 22 2018 at 20:43):

Not yet

Johan Commelin (Nov 22 2018 at 20:45):

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

Patrick Massot (Nov 22 2018 at 20:47):

I can try

Patrick Massot (Nov 22 2018 at 20:47):

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

Patrick Massot (Nov 22 2018 at 20:48):

Is there something I could clone?

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.

Johan Commelin (Nov 22 2018 at 20:48):

simplicial branch on community mathlib

Patrick Massot (Nov 22 2018 at 20:48):

did you push everything relevant to that branch?

Johan Commelin (Nov 22 2018 at 20:49):

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

Johan Commelin (Nov 22 2018 at 20:49):

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

Johan Commelin (Nov 22 2018 at 20:49):

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

Johan Commelin (Nov 22 2018 at 20:50):

you get an induced map pmf.map f

Johan Commelin (Nov 22 2018 at 20:50):

And that should be continuous

Johan Commelin (Nov 22 2018 at 20:50):

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

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

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.

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

Patrick Massot (Nov 22 2018 at 21:42):

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

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

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

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

Reid Barton (Nov 23 2018 at 01:06):

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

Johan Commelin (Nov 23 2018 at 05:10):

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

Johan Commelin (Nov 23 2018 at 05:10):

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

Patrick Massot (Nov 23 2018 at 07:53):

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

Johan Commelin (Nov 23 2018 at 07:53):

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

Patrick Massot (Nov 23 2018 at 07:53):

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

Patrick Massot (Nov 23 2018 at 07:54):

including figuring out what is already in mathlib

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.

Patrick Massot (Nov 23 2018 at 07:55):

maybe also things like projection on factors is an open map

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?

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

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.

Patrick Massot (Nov 23 2018 at 08:23):

Which lemma? metric_pi_topology?

Johan Commelin (Nov 23 2018 at 08:25):

Right, that one.

Johan Commelin (Nov 23 2018 at 08:26):

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

Patrick Massot (Nov 23 2018 at 08:26):

Do you want me to try proving it?

Patrick Massot (Nov 23 2018 at 08:26):

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

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.

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!

Johan Commelin (Nov 23 2018 at 08:29):

Kudos to @Mario Carneiro

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)

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.

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

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

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

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

Johan Commelin (Nov 23 2018 at 16:02):

why?

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

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.

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

I see

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

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

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

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: Dec 20 2023 at 11:08 UTC