# Zulip Chat Archive

## Stream: condensed mathematics

### Topic: homological headache

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

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

- The above approach hides an automatic tactic call behind
`notation `d``

. Downside: the notation will not be used in the goal view. - Use
`auto_param`

. But this doesn't work with bundled morphisms. - Use
`fact (i + 1 = j)`

. I fear that this might not scale when it comes to chaining equalities together using transitivity.

#### Johan Commelin (Feb 15 2021 at 15:05):

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

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

#### Adam Topaz (Feb 15 2021 at 15:16):

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

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

#### Adam Topaz (Feb 15 2021 at 15:19):

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

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

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

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

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

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

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

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

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

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

#### 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 }
```

#### Kevin Buzzard (Feb 15 2021 at 17:27):

It'll be fun explaining that to the normal people

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

#### Mario Carneiro (Feb 15 2021 at 17:28):

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

#### Kevin Buzzard (Feb 15 2021 at 17:28):

d^2=0

#### Kevin Buzzard (Feb 15 2021 at 17:29):

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

#### Mario Carneiro (Feb 15 2021 at 17:29):

aha, I see now, I like this crazy idea

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

#### Mario Carneiro (Feb 15 2021 at 17:31):

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

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

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

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

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

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

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

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

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

#### 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 :-/

#### Mario Carneiro (Feb 15 2021 at 18:22):

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

#### Mario Carneiro (Feb 15 2021 at 18:23):

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

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

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

#### Kevin Buzzard (Feb 15 2021 at 18:24):

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

#### Mario Carneiro (Feb 15 2021 at 18:28):

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

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

#### Johan Commelin (Feb 15 2021 at 18:33):

So you have `d : C i -> C j`

for all `i`

and `j`

. And

- if
`j = i`

, then`d = id`

- if
`j = i`

, then`d =`

"the*actual*$d$" - otherwise,
`d = 0`

#### Johan Commelin (Feb 15 2021 at 18:35):

~~And so there will be a simp lemma that says that ~~ (This is false, the right hand side could be `d`

composed with `d`

is `d`

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

#### 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)
```

#### Adam Topaz (Feb 15 2021 at 18:37):

In case anyone wants to play with a totalized version

#### Johan Commelin (Feb 15 2021 at 18:39):

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

`mk_graded`

might not fit into your category (e.g. complexes of findim vector spaces)- 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 (Feb 15 2021 at 18:41):

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

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

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

#### Adam Topaz (Feb 15 2021 at 18:44):

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

#### Adam Topaz (Feb 15 2021 at 18:44):

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

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

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

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

#### Mario Carneiro (Feb 15 2021 at 18:52):

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

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

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

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

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

#### Johan Commelin (Feb 15 2021 at 18:57):

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

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

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

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

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

#### Johan Commelin (Feb 15 2021 at 19:15):

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

.

#### 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!

#### Mario Carneiro (Feb 15 2021 at 19:19):

What's problematic? The `rw add_sub_cancel`

lines work now

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

#### Mario Carneiro (Feb 15 2021 at 19:19):

and you can use `i+2`

instead of `i+1+1`

#### Johan Commelin (Feb 15 2021 at 19:20):

aah, so why is `rw`

working and `simp`

failing?

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

#### Adam Topaz (Feb 15 2021 at 19:20):

The `d x = 0`

assumption doesn't match with the `d x = 0`

goal.

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

#### Johan Commelin (Feb 15 2021 at 19:22):

We might need to do that

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

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

#### Mario Carneiro (Feb 15 2021 at 19:23):

that's what causes all the `simp`

sadness though

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

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

#### Johan Commelin (Feb 15 2021 at 19:25):

@Mario Carneiro why can't `angry_simp`

just blast through those annoying badly-typed motives?

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

?

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

#### Adam Topaz (Feb 15 2021 at 19:27):

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

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

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

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

#### Johan Commelin (Feb 15 2021 at 19:31):

I want `yolo_simp`

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

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

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

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

?

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

#### Johan Commelin (Feb 15 2021 at 19:38):

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

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

#### Mario Carneiro (Feb 15 2021 at 19:39):

and then replace `h`

with `rfl`

along with everything else

#### Mario Carneiro (Feb 15 2021 at 19:39):

but doing that in a `rw`

line with no hairy middle steps is a challenge

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

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

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

#### 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"

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

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

#### 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_hom`

s.

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

#### 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)`

.

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

.

- for
`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 (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.

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

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

#### Scott Morrison (Feb 19 2021 at 11:33):

I'd also like to test out the `ℕ ⥤ V`

approach, of course.

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

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

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

#### Johan Commelin (Feb 20 2021 at 18:14):

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

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

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

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