# Zulip Chat Archive

## Stream: condensed mathematics

### Topic: homotopies

#### Johan Commelin (Mar 24 2021 at 07:21):

Yesterday I pushed a definition of homotopy between to chain maps. But I realised that I'm not sure what needs to be supported.

- Do people ever consider homotopies between chain maps of complexes of length $n$?
- What are the conditions at the "endpoints"?
- Certainly, we want homotopies for
`chain_complex nat`

. At least for LTE, we want the condition $d_0 \circ h_0 = f_0 - g_0$. Which amounts to the usual condition, if we allow $d_{-1} = 0$ and/or $h_{-1} = 0$. - Do people consider homotopies in the
`nat`

case with "no condition" in degree 0?

#### Johan Commelin (Mar 24 2021 at 07:22):

Currently, the condition is:

```
∀ i j k, coherent_indices cov i j → coherent_indices cov j k → h j i ≫ C₂.d i j + C₁.d j k ≫ h k j = f.f j - g.f j)
```

But `coherent_indices cov i j → coherent_indices cov j k`

means `i + 1 = j`

and `j + 1 = k`

. So we don't have any condition for `j = 0`

at the moment.

#### Scott Morrison (Mar 24 2021 at 07:23):

That doesn't sound right.

#### Johan Commelin (Mar 24 2021 at 07:23):

This can be solved by replacing `coherent_indices i j`

by a special condition, that takes the "end of a complex" into account. But I first want to know whether the "end of a complex" is always treated in the same way.

#### Scott Morrison (Mar 24 2021 at 07:26):

You could do it with the relation we were talking about:

#### Scott Morrison (Mar 24 2021 at 07:27):

`r i j → r j k → h j i ≫ C₂.d i j + C₁.d j k ≫ h k j = f.f j - g.f j`

but then also

`r i j → (∀ k, ¬(r j k)) → h j i ≫ C₂.d i j = f.f j - g.f j`

#### Scott Morrison (Mar 24 2021 at 07:27):

etc

#### Johan Commelin (Mar 24 2021 at 07:28):

I think that with the relation you still have to decide which of the two cases you want

#### Scott Morrison (Mar 24 2021 at 07:28):

so you just have four different axioms, that always hold, but 3 of which aren't relevant except at the ends of chains

#### Johan Commelin (Mar 24 2021 at 07:28):

So my question is first and foremost: do both options occur in practice, or is there always "half a condition at the end of the complex"

#### Scott Morrison (Mar 24 2021 at 07:28):

I'm pretty sure there's always a condition at the end of the complex.

#### Scott Morrison (Mar 24 2021 at 07:29):

complexes with specified support are always really int indexed complexes

#### Johan Commelin (Mar 24 2021 at 07:29):

That would be very helpful, because otherwise we need to support 4 different kinds of homotopies

#### Scott Morrison (Mar 24 2021 at 07:29):

it's only for DTT-hell purposes that we're considering small indexing sets, rather than a support condition, in the first place

#### Julian Külshammer (Mar 24 2021 at 07:44):

To answer your original question: Yes, people consider homotopies of complexes of length n, see e.g. p.8 of https://arxiv.org/abs/1709.06689 There are the half conditions for the end points in place and I also don't recall seeing them not in place.

#### Johan Commelin (Mar 24 2021 at 08:40):

Thanks for all the responses. I've pushed a fix

#### Scott Morrison (Mar 27 2021 at 12:37):

@Johan Commelin, I've just had yet another go at formalizing complexes, this time using a combination of our `gizmo`

attempt, and heavy use of the new `subobject`

API. I'm pretty happy with progress so far: e.g.

```
lemma boundaries_le_cycles (C : homological_complex V c) (i : ι) :
C.boundaries i ≤ C.cycles i :=
begin
dsimp [cycles, boundaries],
split_ifs with h h',
{ exact image_subobject_le_mk _ (C.d _ i) (kernel.lift _ _ (C.d_comp_d _ i _)) (by simp), },
{ exact le_top, },
{ exact bot_le, },
{ exact le_top, },
end
```

It's too late for me tonight, but it would be great to chat about this sometime. It's on branch#homology2 (mathlib) in `src/algebra/homology2`

.

#### Kevin Buzzard (Mar 27 2021 at 12:42):

I would like to develop some of the theory of Tor for R-modules (independent of LTE -- this is for Amelia's project) and was wondering if the definition of a complex was going to change in mathlib at some point?

#### Kevin Buzzard (Mar 27 2021 at 12:44):

Oh I've just seen that the branch is on mathlib! Great!

#### Johan Commelin (Mar 27 2021 at 14:05):

@Scott Morrison looks great! I think I'll have plenty time next week (but maybe not Monday).

#### Kevin Buzzard (Mar 27 2021 at 17:21):

branch#complex_ses contains `src/algebra/homology2/Module.lean`

which is the beginnings of the construction of a long exact sequence of cohomology groups coming from a short exact sequence of complexes a la Scott's branch above.

I'm using `hij : r i j`

as an input (r is the relation saying d i j might not be 0), which I think Johan was reluctant to use in some places, but if I don't use hij I have to input i and j, so I'm sticking with it for now. I'll do a bit more later. Amelia would really like some basic Tor stuff and I'm just thinking about thrashing the whole theory out using Scott's new complexes just to see what happens. I can't do it for abelian categories or whatever because I can't face the diagram chasing without elements -- Markus has some code which needs a lot of clean-up but writes new tactics, and I am not enough of a programmer to be able to go there and pick up where he left off.

#### Kevin Buzzard (Mar 27 2021 at 19:54):

Ha ha I was live streaming on Discord and Kenny popped in. I had defined homology of a complex of R-modules by promoting Ker(d) to a module (from a submodule), explicitly constructing Im(d) as a submodule of that and taking the quotient. Kenny pointed out that instead of my explicit construction I could just use comap. One weird consequence of this is that you now no longer even have to assume d^2=0 :rolling_on_the_floor_laughing: The homology is kernel over (kernel intersect image). I'm seeing how much of the theory I can develop without assuming d^2=0!

#### Johan Commelin (Mar 27 2021 at 19:57):

Well, certainly Euler characteristics will break :rofl:

#### Scott Morrison (Mar 28 2021 at 14:20):

I proved that homotopic maps induce equal maps on homology (modulo a little piece of API about linear combinations factoring through subobjects).

#### Scott Morrison (Mar 28 2021 at 14:21):

It still feels harder than it should have been, but maybe it will polish up more.

Last updated: May 09 2021 at 23:10 UTC