homological headache

Stream: condensed mathematics

[Johan Commelin]

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

[Johan Commelin]

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.

[Johan Commelin]

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

[Adam Topaz]

@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

[Adam Topaz]

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

[Johan Commelin]

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

[Adam Topaz]

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

[Johan Commelin]

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

[Johan Commelin]

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:

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

  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.

[Johan Commelin]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Adam Topaz]

Crazy idea:

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

[Kevin Buzzard]

It'll be fun explaining that to the normal people

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

d^2=0

[Kevin Buzzard]

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

[Mario Carneiro]

aha, I see now, I like this crazy idea

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Alex J. Best]

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

[Johan Commelin]

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.

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

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:

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Adam Topaz]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Johan Commelin]

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?

[Johan Commelin]

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 $d$"
3. otherwise, d = 0

[Johan Commelin]

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

[Johan Commelin]

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.

[Adam Topaz]

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)

[Adam Topaz]

In case anyone wants to play with a totalized version

[Johan Commelin]

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

[Adam Topaz]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Adam Topaz]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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.

[Mario Carneiro]

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

[Johan Commelin]

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.

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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!

[Mario Carneiro]

What's problematic? The rw add_sub_cancel lines work now

[Johan Commelin]

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.

[Mario Carneiro]

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

[Johan Commelin]

aah, so why is rw working and simp failing?

[Adam Topaz]

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

[Adam Topaz]

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

[Mario Carneiro]

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

[Johan Commelin]

We might need to do that

[Johan Commelin]

Mario Carneiro said:

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

this causes the fail that Adam noticed

[Kevin Buzzard]

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?

[Mario Carneiro]

that's what causes all the simp sadness though

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Mario Carneiro]

/-- `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

[Mario Carneiro]

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)

[Mario Carneiro]

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

[Johan Commelin]

I want yolo_simp

[Johan Commelin]

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?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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?

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

and then replace h with rfl along with everything else

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mauricio Collares]

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"

[Johan Commelin]

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

[Scott Morrison]

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

[Scott Morrison]

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.

[Mario Carneiro]

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

[Scott Morrison]

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

[Scott Morrison]

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.

[Scott Morrison]

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.

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Johan Commelin]

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.

[Kevin Buzzard]

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

[Floris van Doorn]

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.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

probably a combi of ring and maybe linarith