Zulip Chat Archive

Stream: condensed mathematics

Topic: homological headache


view this post on Zulip Johan Commelin (Feb 15 2021 at 15:01):

Hmm, I can't replicate the solution that worked in the previous example.
Here are two rather minimal examples that explain the problem.

import algebra.homology.chain_complex
import algebra.category.Group
import tactic.ring

variables (C : cochain_complex AddCommGroup)

open category_theory

section

open tactic

meta def int_magic : tactic unit :=
do (assumption <|> tactic.interactive.ring1 none <|> tactic.interactive.refl) <|>
   target >>= trace

end

/-- Convenience definition:
The identity morphism of an object in the system of complexes
when it is given by different indices that are not
definitionally equal. -/
def congr_hom {i j : } (h : i = j) :
  C.X i  C.X j :=
eq_to_hom $ by { subst h }

/-- `C.d` is the differential `C i ⟶ C (i+1)` for a cochain complex `C`. -/
def differential (i j : ) (hij : i + 1 = j) :
  C.X i  C.X j :=
C.d i  congr_hom C hij

local notation `d` := differential _ _ _ (by int_magic)

lemma differential_rfl (i : ) : differential C i (i+1) rfl = C.d i :=
by { ext, refl }

lemma d_comp_d {i₁ i₂ i₃ : } (h : i₁ + 1 = i₂) (h' : i₂ + 1 = i₃) :
  (d : C.X i₁  C.X i₂)  (d : C.X i₂  C.X i₃) = 0 :=
begin
  subst i₂, subst i₃,
  simp only [differential_rfl],
  exact homological_complex.d_squared _ _
end

lemma d_d {i₁ i₂ i₃ : } (h : i₁ + 1 = i₂) (h' : i₂ + 1 = i₃) (x : C.X i₁) :
  (differential C i₂ _ (by int_magic) (d x : C.X i₂) : C.X i₃) = 0 :=
show ((d : C.X i₁  C.X i₂)  (d : C.X i₂  C.X i₃)) x = 0,
by { rw d_comp_d, refl }

example (h :  i : ,  x : C.X (i+1), d x = 0   y, d y = x)
  (i : ) (x : C.X i) (hx : d x = 0) :
   y : C.X (i-1), d y = x :=
begin
  specialize h (i-1),
  -- rw sub_add_cancel at h,
  simp at h,
end

example (h :  i : ,  x : C.X i, d x = 0   y : C.X (i-1), d y = x)
  (i : ) (x : C.X (i+1)) (hx : d x = 0) :
   y, d y = x :=
begin
  specialize h (i+1),
  -- rw add_sub_cancel at h,
  simp at h,
end

view this post on Zulip Johan Commelin (Feb 15 2021 at 15:04):

I don't care so much about how we invoke automation, as long as it works :stuck_out_tongue_wink:

  1. The above approach hides an automatic tactic call behind notation `d` . Downside: the notation will not be used in the goal view.
  2. Use auto_param. But this doesn't work with bundled morphisms.
  3. Use fact (i + 1 = j). I fear that this might not scale when it comes to chaining equalities together using transitivity.

view this post on Zulip Johan Commelin (Feb 15 2021 at 15:05):

But the problem outlined above is orthogonal to these 3 approaches.

view this post on Zulip Adam Topaz (Feb 15 2021 at 15:16):

@Johan Commelin Have you thought about trying tricks similar to the following?

@[simp] def test {i : } (x : C.X (i-1+1)) : C.X i := congr_hom C (by int_magic) x

example {i : } (cond :  x : C.X (i-1+1), true) :  x : C.X i, true :=
begin
  cases cond,
  simp at cond_w,
  finish,
end

view this post on Zulip Adam Topaz (Feb 15 2021 at 15:16):

I don't know if this would be helpful at all.

view this post on Zulip Johan Commelin (Feb 15 2021 at 15:18):

I would like to hide congr_hom as much as possible behind a basic API. Otherwise we'll end up with many silly proof steps, saying that the norm of congr_hom x is the same as the norm of x, etc... etc...

view this post on Zulip Adam Topaz (Feb 15 2021 at 15:19):

I imagine we can solve these issues with some carefully chosen simp lemmas

view this post on Zulip Johan Commelin (Feb 15 2021 at 15:21):

You can take a look at system_of_complexes.lean on the wip_dtt branch... it didn't look pleasant to me.

view this post on Zulip Johan Commelin (Feb 15 2021 at 15:47):

There was the other proposal to use a massive direct sum, and define d on that. But I don't see how that will play nicely with either categorical language, where you don't have elements (so how do you define a complex in the first place? as something isomorphic to a massive direct sum?) or with elements (how do you move from x : C i to the massive direct sum? will we have canonical inclusion maps before every other element?).
Still, if someone wants to try a test of this, and it works well, then I'll shut up :grinning: :speak_no_evil:

view this post on Zulip Kevin Buzzard (Feb 15 2021 at 16:52):

example (h :  i : ,  x : C.X (i+1), d x = 0   y, d y = x)
  (i : ) (x : C.X i) (hx : d x = 0) :
   y : C.X (i-1), d y = x :=
begin
  suffices :  i j (x : C.X j) (hij : i + 1 = j) (hx : d x = 0),
     y : C.X i, d y = x,
  { exact this _ _ _ _ hx }, clear hx x i,
  rintros i j x rfl hx,
  exact h _ _ hx,
end

view this post on Zulip Kevin Buzzard (Feb 15 2021 at 16:54):

example (h :  i : ,  x : C.X i, d x = 0   y : C.X (i-1), d y = x)
  (i : ) (x : C.X (i+1)) (hx : d x = 0) :
   y, d y = x :=
begin
  suffices :  i j (x : C.X j) (hij : i + 1 = j) (hx : d x = 0),
     y : C.X i, d y = x,
  { exact this _ _ _ _ hx }, clear hx x i,
  rintros i j x hij hx,
  have hij' : i = j - 1 := eq_sub_of_add_eq hij,
  subst hij',
  exact h _ _ hx,
end

view this post on Zulip Kevin Buzzard (Feb 15 2021 at 16:54):

Everything is easy if the hypothesis is stated in the type-theoretically correct way -- there are no fancy tricks here.

view this post on Zulip Kevin Buzzard (Feb 15 2021 at 16:55):

  suffices :  i j (x : C.X j) (hij : i + 1 = j) (hx : d x = 0),
     y : C.X i, d y = x,

This is great because we're quantifying over i and j, and all our dependent types (C.X i and C.X j) can be specialised to the case in hand.

view this post on Zulip Johan Commelin (Feb 15 2021 at 17:21):

On the other hand, it means that we'll always be writing (hij : i + 1 = j) all over the place. It would be great if some tactic could remove that need.

view this post on Zulip Mario Carneiro (Feb 15 2021 at 17:24):

I like this solution, it puts the i+1=j proof into a subgoal where it can be proved by any means necessary

view this post on Zulip Mario Carneiro (Feb 15 2021 at 17:26):

Writing nontrivial terms in rigid positions in a dependent type seems to be a recurring source of problems

view this post on Zulip Adam Topaz (Feb 15 2021 at 17:26):

Crazy idea:

open category_theory
def complex := { C :   AddCommGroup //  (i j : ) (h : i + 2  j), C.map (hom_of_le h) = 0 }

view this post on Zulip Kevin Buzzard (Feb 15 2021 at 17:27):

It'll be fun explaining that to the normal people

view this post on Zulip Kevin Buzzard (Feb 15 2021 at 17:28):

I guess that is of no relevance -- my students don't yet know what the actual definition of is_compact is and yet they can still prove things by finding finite subcovers of open covers

view this post on Zulip Mario Carneiro (Feb 15 2021 at 17:28):

What's it supposed to look like? That seems like a pretty normal definition

view this post on Zulip Kevin Buzzard (Feb 15 2021 at 17:28):

d^2=0

view this post on Zulip Kevin Buzzard (Feb 15 2021 at 17:29):

I mean, like that exact string of characters. It's like a set phrase.

view this post on Zulip Mario Carneiro (Feb 15 2021 at 17:29):

aha, I see now, I like this crazy idea

view this post on Zulip Kevin Buzzard (Feb 15 2021 at 17:31):

I have no idea how to search for d^2=0 on mathoverflow but I am convinced it will be everywhere.

view this post on Zulip Mario Carneiro (Feb 15 2021 at 17:31):

I wonder how common it is to have this whole functor available instead of d

view this post on Zulip Kevin Buzzard (Feb 15 2021 at 17:32):

It's the fact that mathematicians constantly abuse this d notation to mean "all the maps" which makes me open to the idea of the direct sum approach, where one really does have one map d, from the direct sum (or disjoint union, depending on which category you're taking the coproduct in).

view this post on Zulip Alex J. Best (Feb 15 2021 at 17:58):

Kevin Buzzard said:

I have no idea how to search for d^2=0 on mathoverflow but I am convinced it will be everywhere.

Not MO but https://approach0.xyz/search/?q=%24d%5E2%3D0%24&p=1

view this post on Zulip Johan Commelin (Feb 15 2021 at 18:18):

Kevin Buzzard said:

It's the fact that mathematicians constantly abuse this d notation to mean "all the maps" which makes me open to the idea of the direct sum approach, where one really does have one map d, from the direct sum (or disjoint union, depending on which category you're taking the coproduct in).

But I don't see how to write this down in lean, in such a way that you can do complexes of objects in an arbitrary (abelian) category, and at the same time make is useful when trying to apply d to elements of a module in some concrete complex.

view this post on Zulip Johan Commelin (Feb 15 2021 at 18:18):

How do you express that the big complex-object is the direct sum of the constituent objects?

view this post on Zulip Mario Carneiro (Feb 15 2021 at 18:19):

Given any suitable definition of the d function, it's possible to construct a functor like Adam Topaz 's version, and as long as you don't need to reduce it you can just work from that

view this post on Zulip Johan Commelin (Feb 15 2021 at 18:20):

Adam Topaz said:

Crazy idea:

open category_theory
def complex := { C :   AddCommGroup //  (i j : ) (h : i + 2  j), C.map (hom_of_le h) = 0 }

Would this solve the issue that we have in the example from the first post? Of does this just mean that we should never ever talk about d, and always use hom_of_le instead? Doesn't sound like it will be very readable... :sad:

view this post on Zulip Mario Carneiro (Feb 15 2021 at 18:21):

I think you can wrap that behind a definition of type \all i j : int, C i -> C j

view this post on Zulip Kevin Buzzard (Feb 15 2021 at 18:22):

Such a map only exists for i<=j, right? The situation is C i -> C (i + 1) -> C (i + 2) -> ...

view this post on Zulip Adam Topaz (Feb 15 2021 at 18:22):

@Johan Commelin I'm playing with this idea now. And the answer seems to be no, still getting the same issue :-/

view this post on Zulip Mario Carneiro (Feb 15 2021 at 18:22):

ah yeah, it would be \all i j, i <= j -> C i -> C j

view this post on Zulip Mario Carneiro (Feb 15 2021 at 18:23):

and I guess the last arrow is a hom of some kind

view this post on Zulip Kevin Buzzard (Feb 15 2021 at 18:23):

I guess the category of finite abelian groups is a perfectly good abelian category which doesn't have infinite direct sums.

view this post on Zulip Mario Carneiro (Feb 15 2021 at 18:24):

Is it possible / desirable to totalize here? C j is an abelian group so you've got the zero morphism

view this post on Zulip Kevin Buzzard (Feb 15 2021 at 18:24):

yeah, there are zero morphisms in an arbitrary abelian category too

view this post on Zulip Mario Carneiro (Feb 15 2021 at 18:28):

leading to the less well known identity d1=0d^{-1}=0

view this post on Zulip Johan Commelin (Feb 15 2021 at 18:32):

But even if you totalize... does this mean we should just put type ascriptions every where? And give up on the idea that d is a degree 1 map?

view this post on Zulip Johan Commelin (Feb 15 2021 at 18:33):

So you have d : C i -> C j for all i and j. And

  1. if j = i, then d = id
  2. if j = i, then d = "the actual dd"
  3. otherwise, d = 0

view this post on Zulip Johan Commelin (Feb 15 2021 at 18:35):

And so there will be a simp lemma that says that d composed with d is d (This is false, the right hand side could be id while the left hand side is d >> 0). And

lemma d_eq_zero (i j) (h : i + 2 \le j) :
  (d : C i -> C j) = 0 := sorry

view this post on Zulip Johan Commelin (Feb 15 2021 at 18:36):

I was just hoping that lean would be able to infer the type of d x from the type of x... but I guess that's asking for lots of pain, at least in lean3.

view this post on Zulip Adam Topaz (Feb 15 2021 at 18:36):

import algebra.homology.chain_complex
import algebra.category.Group

open category_theory AddCommGroup.colimits

def mk_graded (F :   AddCommGroup) : AddCommGroup := AddCommGroup.colimits.colimit (discrete.functor F)

def ι {i : } {F :   AddCommGroup} : F i  mk_graded F := cocone_morphism (discrete.functor F) i

structure complex :=
(F :   AddCommGroup)
(d : mk_graded F  mk_graded F)
(d_graded :  i : ,  f : F i  F (i+1), ι  d = f  ι)
(d_squared : d  d = 0)

view this post on Zulip Adam Topaz (Feb 15 2021 at 18:37):

In case anyone wants to play with a totalized version

view this post on Zulip Johan Commelin (Feb 15 2021 at 18:39):

But there are two downsides, afaik (sorry for being critical, without having a better solution):

  1. mk_graded might not fit into your category (e.g. complexes of findim vector spaces)
  2. if I have a concrete example of a complex, then I will have some x : F i, and if I want to do a bit of homological algebra, then those ι\iota maps will be all over the place

view this post on Zulip Adam Topaz (Feb 15 2021 at 18:41):

Yeah, I agree. But I still think it's worth some experimentation

view this post on Zulip Mario Carneiro (Feb 15 2021 at 18:42):

those ι\iota maps will be all over the place

I don't think this is a major problem; it's kind of like working with integer expressions involving nats with \u a + \u b - 1 = \u c

view this post on Zulip Mario Carneiro (Feb 15 2021 at 18:43):

Regarding 1, is it possible to take a synthetic colimit here, putting you in a completion of the original category? Like a sigma

view this post on Zulip Adam Topaz (Feb 15 2021 at 18:44):

Yeah, that's what I'm thinking too.

view this post on Zulip Adam Topaz (Feb 15 2021 at 18:44):

Maybe @Bhavik Mehta 's work on ind completions would help here.

view this post on Zulip Bhavik Mehta (Feb 15 2021 at 18:50):

Yeah you can take the synthetic colimit if it's a filtered colimit, but there's already the free cocompletion in mathlib

view this post on Zulip Bhavik Mehta (Feb 15 2021 at 18:50):

But this comes with the caveat that the new category will be (potentially) a lot bigger than the original one - even in non-Lean maths if you take the cocompletion of a small category you end up with a large one

view this post on Zulip Adam Topaz (Feb 15 2021 at 18:51):

Plus the differential in the complex would become some morphism of presheaves, which might confuse even more people :)

view this post on Zulip Mario Carneiro (Feb 15 2021 at 18:52):

In this case you only need the completion wrt colimits of length int

view this post on Zulip Kevin Buzzard (Feb 15 2021 at 18:53):

I still kind of think that d : C_i -> C_j = 0 for i > j is kind of insane. It would then not be true that for all i,j,k, d o d = d, for example. Chains seem to have been implemented as a functor from the integers (so again there are no d's if i > j) and the "d = 0 if i+2<=j" condition does sound like a cool way of setting it up.

view this post on Zulip Mario Carneiro (Feb 15 2021 at 18:54):

It would then not be true that for all i,j,k, d o d = d, for example.

That was never true, because d o d = d doesn't typecheck for a lot of values of i,j,k

view this post on Zulip Johan Commelin (Feb 15 2021 at 18:55):

chain complexes have an "ad hoc" definition. They aren't implemented as functors. Just a collection of int-indexed objects with a d (of degree 1) between them.

view this post on Zulip Mario Carneiro (Feb 15 2021 at 18:55):

the only difference now is that those assumptions are moving from type correctness assumptions to regular assumptions

view this post on Zulip Johan Commelin (Feb 15 2021 at 18:57):

it also means that you get less type inference. so statements will become a lot clunkier

view this post on Zulip Mario Carneiro (Feb 15 2021 at 18:58):

I'm not sure the hypotheses that were being supplied are actually the ones you want though

view this post on Zulip Mario Carneiro (Feb 15 2021 at 18:59):

for example a type correctness hypothesis might be needlessly obtuse like i+1+1 <= j+1 while a regular hypothesis can be stated as i+1 <= j

view this post on Zulip Johan Commelin (Feb 15 2021 at 19:13):

I've adapted the example to a totalized d:

import algebra.category.Group
import tactic

open category_theory

structure cochain_complex extends   AddCommGroup :=
(is_complex :  (i j : ) (h : i + 2  j), map (hom_of_le (show i  j, by linarith)) = 0)

variables {C : cochain_complex} {i j k : }

/-- `C.d` is the differential `C i ⟶ C (i+1)` for a cochain complex `C`. -/
def d : C.obj i  C.obj j :=
if h : i  j then C.map (hom_of_le h) else 0

lemma d_comp_d (h : i + 2  k) :
  (d : C.obj i  C.obj j)  (d : C.obj j  C.obj k) = 0 :=
begin
  delta d,
  by_cases h12 : i  j,
  { by_cases h23 : j  k,
    { rw [dif_pos h12, dif_pos h23,  functor.map_comp],
      exact C.is_complex i k h },
    { rw dif_neg h23, rw limits.comp_zero } },
  { rw dif_neg h12, rw limits.zero_comp }
end

lemma d_d (h : i + 2  k) (x : C.obj i) :
  (d (d x : C.obj j) : C.obj k) = 0 :=
show ((d : C.obj i  C.obj j)  (d : C.obj j  C.obj k)) x = 0,
by { rw d_comp_d h, refl }

example (h :  i : ,  x : C.obj (i+1), (d x : C.obj (i+2)) = 0   y : C.obj i, d y = x)
  (i : ) (x : C.obj i) (hx : (d x : C.obj (i+1)) = 0) :
   y : C.obj (i-1), d y = x :=
begin
  specialize h (i-1),
  -- rw sub_add_cancel at h,
  simp at h,
end

example (h :  i : ,  x : C.obj i, (d x : C.obj (i+1)) = 0   y : C.obj (i-1), d y = x)
  (i : ) (x : C.obj (i+1)) (hx : (d x : C.obj (i+1+1)) = 0) :
   y : C.obj i, d y = x :=
begin
  specialize h (i+1),
  -- rw add_sub_cancel at h,
  simp at h,
end

view this post on Zulip Johan Commelin (Feb 15 2021 at 19:14):

But these statements are still problematic... Should they be written differently now? I don't see how.

view this post on Zulip Johan Commelin (Feb 15 2021 at 19:15):

Unless we use Kevin's approach again... but that also worked with the untotal d.

view this post on Zulip Kevin Buzzard (Feb 15 2021 at 19:17):

Johan Commelin said:

chain complexes have an "ad hoc" definition. They aren't implemented as functors. Just a collection of int-indexed objects with a d (of degree 1) between them.

Oh sorry, I was looking at Adam's definition! I had assumed it was official in some way :-) I think that it definitely has its merits!

view this post on Zulip Mario Carneiro (Feb 15 2021 at 19:19):

What's problematic? The rw add_sub_cancel lines work now

view this post on Zulip Johan Commelin (Feb 15 2021 at 19:19):

Sure, but we would definitely want a constructor that only needs a degree 1 map. E.g., when building a complex from a simplicial module by taking alternating sums of the degeneracy maps... you don't want to worry about arbitrary compositions at that point.

view this post on Zulip Mario Carneiro (Feb 15 2021 at 19:19):

and you can use i+2 instead of i+1+1

view this post on Zulip Johan Commelin (Feb 15 2021 at 19:20):

aah, so why is rw working and simp failing?

view this post on Zulip Adam Topaz (Feb 15 2021 at 19:20):

Yeah:

example (h :  i : ,  x : C.obj (i+1), (d x : C.obj (i+2)) = 0   y : C.obj i, d y = x)
  (i : ) (x : C.obj i) (hx : (d x : C.obj (i+1)) = 0) :
   y : C.obj (i-1), d y = x :=
begin
  specialize h (i-1),
  rw sub_add_cancel i 1 at h,
  apply h,
  assumption, -- fails :(
end

view this post on Zulip Adam Topaz (Feb 15 2021 at 19:20):

The d x = 0 assumption doesn't match with the d x = 0 goal.

view this post on Zulip Mario Carneiro (Feb 15 2021 at 19:21):

I think this would be a lot clearer (and shorter than the type ascriptions) if j was an explicit arg to d

view this post on Zulip Johan Commelin (Feb 15 2021 at 19:22):

We might need to do that

view this post on Zulip Johan Commelin (Feb 15 2021 at 19:22):

Mario Carneiro said:

and you can use i+2 instead of i+1+1

this causes the fail that Adam noticed

view this post on Zulip Kevin Buzzard (Feb 15 2021 at 19:23):

I think d should take a proof that i <= j. That proof which split up into cases -- nobody is going to need the j < i situation ever, right?

view this post on Zulip Mario Carneiro (Feb 15 2021 at 19:23):

that's what causes all the simp sadness though

view this post on Zulip Kevin Buzzard (Feb 15 2021 at 19:23):

Because it's a proof, we don't care if we have a proof of i <= j + 1 - 1 or whatever

view this post on Zulip Mario Carneiro (Feb 15 2021 at 19:24):

but if it's an arg to d then it ends up in statements which is why nothing rewrites properly

view this post on Zulip Johan Commelin (Feb 15 2021 at 19:25):

@Mario Carneiro why can't angry_simp just blast through those annoying badly-typed motives?

view this post on Zulip Johan Commelin (Feb 15 2021 at 19:25):

It will have to fix up those proof arguments... but isn't that just some trans or subst?

view this post on Zulip Adam Topaz (Feb 15 2021 at 19:27):

import algebra.category.Group
import tactic

open category_theory

structure cochain_complex extends   AddCommGroup :=
(is_complex :  (i j : ) (h : i + 2  j), map (hom_of_le (show i  j, by linarith)) = 0)

variables {C : cochain_complex} {i j k : }

/-- `C.d` is the differential `C i ⟶ C (i+1)` for a cochain complex `C`. -/
def d : C.obj i  C.obj j :=
if h : i  j then C.map (hom_of_le h) else 0

def d' (j) : C.obj i  C.obj j := d

lemma d_comp_d (h : i + 2  k) :
  (d : C.obj i  C.obj j)  (d : C.obj j  C.obj k) = 0 :=
begin
  delta d,
  by_cases h12 : i  j,
  { by_cases h23 : j  k,
    { rw [dif_pos h12, dif_pos h23,  functor.map_comp],
      exact C.is_complex i k h },
    { rw dif_neg h23, rw limits.comp_zero } },
  { rw dif_neg h12, rw limits.zero_comp }
end

lemma d_d (h : i + 2  k) (x : C.obj i) :
  (d (d x : C.obj j) : C.obj k) = 0 :=
show ((d : C.obj i  C.obj j)  (d : C.obj j  C.obj k)) x = 0,
by { rw d_comp_d h, refl }

example (h :  i : ,  x : C.obj (i+1), (d' (i+2) x) = 0   y : C.obj i, d y = x)
  (i : ) (x : C.obj i) (hx : (d' (i+1) x) = 0) :
   y : C.obj (i-1), d y = x :=
begin
  specialize h (i-1),
  rw (show i-1+1 = i, by ring) at h,
  rw (show i-1+2 = i+1, by ring) at h,
  exact h _ hx,
end

example (h :  i : ,  x : C.obj i, (d x : C.obj (i+1)) = 0   y : C.obj (i-1), d y = x)
  (i : ) (x : C.obj (i+1)) (hx : (d x : C.obj (i+1+1)) = 0) :
   y : C.obj i, d y = x :=
begin
  specialize h (i+1),
  rw (show i+1-1 = i, by ring) at h,
  apply h _ hx,
end

view this post on Zulip Adam Topaz (Feb 15 2021 at 19:27):

simp's instead of rewrites still don't seem to work

view this post on Zulip Mario Carneiro (Feb 15 2021 at 19:28):

/-- `C.d` is the differential `C i ⟶ C (i+1)` for a cochain complex `C`. -/
def d (j : ) : C.obj i  C.obj j :=
if h : i  j then C.map (hom_of_le h) else 0

lemma d_comp_d (h : i + 2  k) :
  (d j : C.obj i  _)  d k = 0 :=
begin
  delta d,
  by_cases h12 : i  j,
  { by_cases h23 : j  k,
    { rw [dif_pos h12, dif_pos h23,  functor.map_comp],
      exact C.is_complex i k h },
    { rw dif_neg h23, rw limits.comp_zero } },
  { rw dif_neg h12, rw limits.zero_comp }
end

lemma d_d (h : i + 2  k) (x : C.obj i) : d k (d j x) = 0 :=
show (d j  d k) x = 0, by { rw d_comp_d h, refl }

example (h :  i : ,  x : C.obj (i+1), d (i+2) x = 0   y : C.obj i, d _ y = x)
  (i : ) (x : C.obj i) (hx : d (i+1) x = 0) :  y : C.obj (i-1), d _ y = x :=
begin
  specialize h (i-1),
  rw sub_add_cancel at h,
  apply h,
  rwa (by linarith : i - 1 + 2 = i + 1),
end

view this post on Zulip Mario Carneiro (Feb 15 2021 at 19:30):

The statements are indeed a lot shorter, and simp doesn't work because it involves uniformly rewriting in places where simp can't reach because of dependencies (the rwa is actually changing the type of the equality)

view this post on Zulip Mario Carneiro (Feb 15 2021 at 19:31):

rw is too stupid to question whether the rewrite is going to work, it just yolo's and reports motive is not type correct if it turns out not to work

view this post on Zulip Johan Commelin (Feb 15 2021 at 19:31):

I want yolo_simp

view this post on Zulip Johan Commelin (Feb 15 2021 at 19:32):

Are there theoretical obstructions to its existence? Or could a carefully crafted dtt_simp make life easier, without resigning to a bunch of ad hoc hacks?

view this post on Zulip Mario Carneiro (Feb 15 2021 at 19:33):

well the disadvantage of the yolo approach is that you can end up getting tripped up by occurrences of the pattern where it would be best not to touch, like inside proof arguments in the statement

view this post on Zulip Mario Carneiro (Feb 15 2021 at 19:34):

A usable but kind of ugly solution would be to specify exactly which occurrences you want to replace

view this post on Zulip Mario Carneiro (Feb 15 2021 at 19:35):

and that still might not work with situations like the rewrite you sent me

Is the issue that (is_weak_bounded_exact._proof_2 (i + 1)) is only a proof of i + 1 - 1 + 1 = i + 1 and not a proof of i + 1 = i + 1?

view this post on Zulip Mario Carneiro (Feb 15 2021 at 19:37):

As for dtt_simp, things get pretty hairy once you have heterogeneous equality. I think there is a way to do this but it requires pathovers, which we don't have in mathlib

view this post on Zulip Johan Commelin (Feb 15 2021 at 19:38):

But those kind of proofs should be fixable, right? By doing some transitivity of equality.

view this post on Zulip Mario Carneiro (Feb 15 2021 at 19:38):

Yes, the solution is to replace the proof is_weak_bounded_exact._proof_2 (i + 1) with congr_arg (+1) h where h : i + 1 - 1 = 1 is the lemma you are rewriting with

view this post on Zulip Mario Carneiro (Feb 15 2021 at 19:39):

and then replace h with rfl along with everything else

view this post on Zulip Mario Carneiro (Feb 15 2021 at 19:39):

but doing that in a rw line with no hairy middle steps is a challenge

view this post on Zulip Kevin Buzzard (Feb 15 2021 at 19:40):

Here's the "generalize" approach:

example (h :  i : ,  x : C.obj (i+1), (d x : C.obj (i+2)) = 0   y : C.obj i, d y = x)
  (i : ) (x : C.obj i) (hx : (d x : C.obj (i+1)) = 0) :
   y : C.obj (i-1), d y = x :=
begin
  suffices :  i j k : , j = i + 1  k = i + 2   x : C.obj j, (d x : C.obj k) = 0   y : C.obj i, d y = x,
  { apply this _ _ _ _ _ _ hx; ring }, clear hx x i,
  rintros i j k rfl rfl x hx,
  exact h _ _ hx,
end

view this post on Zulip Mario Carneiro (Feb 15 2021 at 19:40):

The generalize_proofs tactic may come in useful here, it will hoist these lemmas into the context where you can replace them in a more targeted way

view this post on Zulip Mario Carneiro (Feb 15 2021 at 19:42):

The suffices line is morally equivalent to the motive that rw is cooking up - the trick is to generalize the right things in the context and it's easy but verbose for a human and hard for a tactic that doesn't know what you are trying to do

view this post on Zulip Mauricio Collares (Feb 15 2021 at 19:51):

Sorry for a (very likely) useless suggestion, but is https://www.cl.cam.ac.uk/~jdy22/papers/frex-indexing-modulo-equations-with-free-extensions.pdf useful for the index computations? I guess it at least provides funny terms such as "slime avoidance" and "fording"

view this post on Zulip Johan Commelin (Feb 15 2021 at 20:08):

It certainly looks relevant... but I don't know enough type theory lingo to see how to apply it in the context at hand

view this post on Zulip Scott Morrison (Feb 16 2021 at 00:53):

Looks like I missed some fun. :-) I've played with this ℤ ⥤ V with C.map (hom_of_le _) = 0 a few times previously. It's a fun definition, and if it actually helped I'm sure we could persuade people that it wasn't insane...

view this post on Zulip Scott Morrison (Feb 16 2021 at 00:55):

But I'm not sure that you get anything from this definition that you don't get just by being careful to insert lots of eq_to_homs.

view this post on Zulip Mario Carneiro (Feb 16 2021 at 01:19):

I think the statements are generally shorter, and you don't have proofs in the statements which causes most of the problem in proofs

view this post on Zulip Scott Morrison (Feb 16 2021 at 02:11):

I guess what I meant was that you still frequently need to move between C.X i and C.X j when you know i = j, you just have an extra way to do this: C.map (hom_of_le (le_of_eq h)), in addition to the general purpose eq_to_hom (congr_arg C.X h).

view this post on Zulip Scott Morrison (Feb 19 2021 at 11:28):

I experimented with yet another definition of a complex, that seems to specialise reasonably to int indexed (co)chain complexes, and to nat indexed chain complexes.

It is:

structure hc {N : Type*} [add_comm_monoid N] (a b : N) :=
(X : N  V)
(d : Π n : N, X (n + a)  X (n + b))
(d_squared' :  (n m : N) (h : n + b = m + a), d n  tra X h  d m = 0 . d_squared_tac)

Here:

  • there are _two_ parameters a b in the definition, which controls where the differential goes.
    • for int indexed chain complexes you want a=0, b=-1.
    • for int indexed cochain complexes you want a=0, b=1.
    • for nat indexed chain complexes you want a=1, b=0.
  • tra X h is just defined as eq_to_hom (congr_arg X h), i.e. it's transport through a type family, as a morphism in the category
  • d_squared_tac is `[{ intros n m h, simp at h, try { subst h }, obviously }].

You can see in https://github.com/leanprover-community/mathlib/blob/hexp/src/algebra/homology/chain_complex_2.lean that at least building the equivalence of categories to cochain complexes, or the equivalence to nat-indexed chain complexes as proposed in #6260, is _relatively_ painless -- d_squared_tac works when you want it to, and tidy manages all the proofs.

Of course, just proving equivalences between definitions is far from enough evidence that this is usable.

view this post on Zulip Scott Morrison (Feb 19 2021 at 11:30):

I was pretty happy in in #6308 that the nat indexed chain complexes of #6260 worked smoothly for defining the Moore complex. So that is some evidence that that definition is usable. I may try redoing the Moore complex using this definition, to see how it goes.

view this post on Zulip Scott Morrison (Feb 19 2021 at 11:32):

The other obvious tests are:

  • adapt the existing algebra/homology/homology.lean
  • write some other equivalences (e.g. coming from an additive automorphism of the indexing monoid N)
  • show that given an inclusion of monoids, the chain complexes on the small monoid are equivalent to chain complexes indexed by the big monoid, supported on the small monoid

view this post on Zulip Scott Morrison (Feb 19 2021 at 11:32):

These aren't the most exciting tests to carry out... So I'm happy to hear feedback or take directions. :-)

view this post on Zulip Scott Morrison (Feb 19 2021 at 11:33):

I'd also like to test out the ℕ ⥤ V approach, of course.

view this post on Zulip Johan Commelin (Feb 19 2021 at 11:36):

Another test is to switch (a branch of) lean-liquid over to your mathlib branch, and rewrite the homological algebra that we've done so far, in terms of this new definition.

view this post on Zulip Kevin Buzzard (Feb 19 2021 at 11:41):

@Floris van Doorn did some homological algebra in Lean 2 using a succ_structure for a base.

view this post on Zulip Floris van Doorn (Feb 20 2021 at 18:02):

Yeah, in Lean 2 I defined chain complexes indexed by a "successor structure" which is just any type equipped with an endofunction, called the successor. It worked nicely, especially when dealing with chain complexes that have some vague periodicity. For example, the long exact sequence of homotopy groups was indexed by nat x fin 3, since every three indices you go up one dimension.

Scott's add_comm_monoid also works for this, and has the advantage that it works well with cochain complexes defined over nat (in my definition this didn't work great, since it would contain one extra map: ... <- X 2 <- X 1 <- X 0 <- X (pred 0))

I also defined graded objects. The linked comment describes two design decisions that are worth considering, though I'm not sure if they would be right for mathlib ((1) looks strange, and (2) might not be a problem if tidy can deal with all the transports.

view this post on Zulip Johan Commelin (Feb 20 2021 at 18:14):

So far, we've been running headfirst into the wall that (2) describes :head_bandage:

view this post on Zulip Johan Commelin (Feb 20 2021 at 18:15):

So I'm inclined to define d as something like

def d {i} (j) : X i -> X j :=
if h : i + 1 = j then (actual def) else 0

view this post on Zulip Johan Commelin (Feb 20 2021 at 18:16):

Note that d >> d = 0 will then hold without proof obligations. For other lemmas/facts we might want to have an auto param that automatically discharges the i + 1 = j-type goals

view this post on Zulip Johan Commelin (Feb 20 2021 at 18:16):

probably a combi of ring and maybe linarith


Last updated: May 09 2021 at 23:10 UTC