Zulip Chat Archive

Stream: condensed mathematics

Topic: homotopies


view this post on Zulip 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 nn?
  • What are the conditions at the "endpoints"?
  • Certainly, we want homotopies for chain_complex nat. At least for LTE, we want the condition d0h0=f0g0d_0 \circ h_0 = f_0 - g_0. Which amounts to the usual condition, if we allow d1=0d_{-1} = 0 and/or h1=0h_{-1} = 0.
  • Do people consider homotopies in the nat case with "no condition" in degree 0?

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Mar 24 2021 at 07:23):

That doesn't sound right.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Mar 24 2021 at 07:26):

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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Mar 24 2021 at 07:27):

etc

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Scott Morrison (Mar 24 2021 at 07:28):

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

view this post on Zulip Scott Morrison (Mar 24 2021 at 07:29):

complexes with specified support are always really int indexed complexes

view this post on Zulip Johan Commelin (Mar 24 2021 at 07:29):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 24 2021 at 08:40):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Mar 27 2021 at 12:44):

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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Johan Commelin (Mar 27 2021 at 19:57):

Well, certainly Euler characteristics will break :rofl:

view this post on Zulip 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).

view this post on Zulip 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