homotopies

Stream: condensed mathematics

[Johan Commelin]

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]

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]

That doesn't sound right.

[Johan Commelin]

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]

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

[Scott Morrison]

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]

etc

[Johan Commelin]

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

[Scott Morrison]

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]

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]

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

[Scott Morrison]

complexes with specified support are always really int indexed complexes

[Johan Commelin]

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

[Scott Morrison]

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]

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]

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

[Scott Morrison]

@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]

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]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

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]

Well, certainly Euler characteristics will break :rofl:

[Scott Morrison]

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

[Scott Morrison]

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