category theory rewrite in exactness tactic

Stream: maths

[Kevin Buzzard]

I was just faced with the following goal. Everything is a morphism in some fixed (abelian) category and all morphisms go either from or to some object C.X i of the category, in the centre of the picture.

  /-
  h: exact (C.d (i + 1) i) (C.d i (i - 1))
  ⊢ exact (C.d_to i) (C.d_from i)
  -/

Why can't I solve this with an assumption_mod_cast-like tool? Here C : chain_complex (some_category) (some_shape) and I am lying about dot notation.

The types: C.d_from i : C.X i ⟶ C.X_next i and C.d i (i - 1) : C.X i ⟶ C.X (i - 1) -- these are homs in category theory, not function arrows. But here's a thing. We proved that C.X_next i and C.X (i - 1) were canonically isomorphic in the following sense: the API for C.X_next includes def X_next_iso {i j : ι} (hcan : c.rel i j) : C.X_next i ≅ C.X j := ... and the secret thing which I know about this isomorphism is that it is canonical in that it is rfl modulo a rewrite which introduces an axiom hcan.rec where hcan : A = B is a proof of a possibly non-definitional equality of terms).

So could a "diagram chase lite" tactic be told about this X_next_iso fact, and then if you have a pair of maps like C.d_from i and C.d i j and a proof of c.rel i j, you can register this pair as being "canonically identified" in the system by providing the proof that the triangle with X_next_iso commutes; in this case, this is the lemma @[simp, reassoc] lemma d_from_comp_X_next_iso (r : c.rel i j) : C.d_from i ≫ (C.X_next_iso r).hom = C.d i j already in our API.

If f and g are two maps related in this way, with the same source X_i, then for any a : _ \hom X_i I will know exact a f <-> exact a g, because presumably we know exact a f <-> exact a (f >> (e : iso)). I would like to think of what just happened, changing that f to a g, as some kind of cool rewrite which avoids motive is not type correct errors. Is this anything close to a sensible idea or should I just be doing everything manually?

[Reid Barton]

Is C.d_from i == C.d i (i - 1)?

[Reid Barton]

C.d_from i ≫ (C.X_next_iso r).hom = C.d i j

Is (C.X_next_iso r).hom of the form eq_to_hom of something?

[Reid Barton]

Yeah, it is, so you could use an approach with convert. Or just prove a little lemma like exact f g -> exact (f >> i) (i.inv >> g) (probably got the order wrong).

[Reid Barton]

Or maybe you already think this goal is easy but you just want it to be even easier?

[Adam Topaz]

@Kevin Buzzard we have isomoprhisms between X_next and X_prev and X (i+1) and X (i-1), and the compatibility with d. So you compose with those isomorphisms to deduce exactness.

[Kevin Buzzard]

yeah I know, I'm just trying a more conceptual approach. My hypothesis is now
h : exact (e1.inv >> f) (g >> e2.hom) with goal exact f g. Do we have these "cancel iso" results?

[Adam Topaz]

by simp might work?

[Adam Topaz]

or by simpa using h.

[Kevin Buzzard]

annoyingly simp knows that e1.inv >> f is f' and rewrites to that. I'll remove the lemma.

[Kevin Buzzard]

  simpa [-homological_complex.X_prev_iso_comp_d_to, -homological_complex.d_from_comp_X_next_iso] using h,

does it :-)

[Kevin Buzzard]

simpa only [exact_comp_iso, exact_iso_comp] using h,

[Kevin Buzzard]

I see, so I could have been using the simplifier, I was just unlucky that some other rewrite removing the equiv triggered first.