homology design question

Stream: general

[Scott Morrison]

@Markus Himmel, @Johan Commelin, I'm a bit stuck on a design decision regarding homology, and wanted some input.

My current draft uses the subobject API extensively. To understand the key benefit, I need to recall that a Johan-complex is a gadget with a d i j : X i ⟶ X j for all possible i j (but with an axiom that says this is often zero). The reason we do this is essentially to avoid DTT hell in the indices: it's perfectly possible to map from X (i - 1 + 1) to X (i + 1) if that's what you need to do. The cost of this is that we have many "different" differentials out of a given X i (i.e. d i j for every j which equals, possibly up to a theorem, i+1). These different target X j are all isomorphic of course. This is where we get the first payoff from using subobjects: if we define def cycles (i : ι) : subobject (C.X i) := ... we get an invariant object that doesn't depend on which j we used. We then construct an explicit isomorphism (C.cycles i : V) ≅ kernel (C.d i j) for every appropriate j.

However there's a cost, and this cost is feeling increasingly painful to me. Unfortunately it's impossible (right??) to make (kernel_subobject f : C) actually definitionally equal to kernel f; we only get an isomorphism. This means that if we continue down this route, I think we're going to have to rewrite Markus' existing work on exactness, so that it is all written in terms of kernel_subobject rather than kernel, subobject.arrow instead of kernel.ι, and so on. Now this is perfectly doable (indeed I've done about half of it), but it adds to the grunge, and particularly makes it feel like many results need to be stated twice (once for the limits API version, once for the subobjects API version). I'm afraid that if I do this work Markus or others are reasonably going to say that it looks like a regression.

Can anyone see how I can have my cake and eat it too? Or convince me that it's just okay to go one way or the other?

I think the options are:

1. just don't use the subobjects API here
2. use it, and deal with having to write a bulkier API

[Scott Morrison]

I'm sorely tempted to try out 1., and see how it goes, but it's a fair bit of work. :-(

[Markus Himmel]

However there's a cost, and this cost is feeling increasingly painful to me. Unfortunately it's impossible (right??) to make (kernel_subobject f : C) actually definitionally equal to kernel f; we only get an isomorphism.

One way to try to work around this issue is to state every lemma about subobjects twice, once for P : subobject X in terms of P.arrow and once for subobject.mk f in terms of f. Is the situation you're describing one where this approach does not help?

[Johan Commelin]

I think that's option (2) that Scott is describing, right?

[Markus Himmel]

The way I understood it, option (2) would be to more or less literally duplicate the relevant parts of category_theory/limits/shapes/* to category_theory/subobject/limits.lean, while I'm suggesting that it may be sufficient to expand the generic subobject API instead

[Markus Himmel]

But of course, sticking with subobjects will most likely entail a lot of both

[Markus Himmel]

Personally, I'd love to see subobjects used for homology. I'm probably a bit too optimistic here, but I think that a very complete subobject API can make many things in category theory that were previously a bit annoying a lot more easy to work with, and I even think that restating many things about limits in terms of subobjects will be worth the effort down the line because at some point the API will complete enough that things start "just working".

By the way, @Scott Morrison, I'd be very happy to help with the homology2 branch (regardless of which option you choose to explore) if you're interested.

[Scott Morrison]

No, I think you may be right, Markus, that lemmas about subobject.mk may be helpful. I have trouble getting my head around this.

[Scott Morrison]

Yes -- while I was off making dinner here I had much the same thought as what Markus says above. When I look at his code on exactness, and feel bad about polluting it with the subobject API, I realise now that actually what is written about exactness was what was possible before we had subobjects! In fact, many of the next steps in homological algebra will require lots of our subobject machinery (subquotients by sups of subobjects, oh my!).

[Scott Morrison]

So I think we'll just have a go at it, using subobjects, and hopefully we can use subobject.mk lemmas productively in places I'm missing them so far.

[Scott Morrison]

@Markus Himmel -- I'd love to find a time soon to go over the homology2 branch with you. I'd both love help, and I think its substantial enough that the PR review process might best be started away from github.

[Scott Morrison]

@Markus Himmel, I think I'm about to jump in and try this: in particular I'm going to refactor everything from image_to_kernel_map onwards through the two different exact files, to always work in terms of subobjects, rather than directly with the limits API.

[Scott Morrison]

(In particular, I'm changing this stuff, not duplicating it, thereby forcing people who want to interact with */exact.lean to use subobjects.)

[Scott Morrison]

@Markus Himmel, I'm finally returning to this after a week or so away from it, and not very happy. Would you mind having a look at branch#homology2, at the file src/algebra/homology2/exact.lean. Here I've just copied across your file from homology/exact.lean, and changed it to use image_to_kernel which is in terms of subobjects rather then image_to_kernel_map (which was in terms of the limits API).

When faced with the rest of the file, however, I don't really know what I should be doing.

[Scott Morrison]

(Besides that file, the branch compiles and is up-to-date with mathlib.)

[Scott Morrison]

Do we keep the existing statements (in terms of the limits API), and then prove new versions of them (in terms of the subobject API)? Or just discard the old ones?

[Scott Morrison]

I've been avoiding working on this file for several days, and would love someone to get past this hump. :-)

[Markus Himmel]

My first instinct would be to throw everything away and start over with

class exact {A B C : V} (f : A ⟶ B) (g : B ⟶ C) : Prop :=
(image_eq_kernel : image_subobject f = kernel_subobject g)

[Scott Morrison]

Okay,

/--
Two morphisms `f : A ⟶ B`, `g : B ⟶ C` are called exact if
the image of `f` is the same as the kernel of `g`,
as subobjects of `B`.
-/
class exact {A B C : V} (f : A ⟶ B) (g : B ⟶ C) : Prop :=
(image_eq_kernel [] : image_subobject f = kernel_subobject g)

@[simp, reassoc]
lemma exact.w {A B C : V} (f : A ⟶ B) (g : B ⟶ C) [exact f g] : f ≫ g = 0 :=
begin
  rw [←image_subobject_arrow_comp f, category.assoc],
  convert comp_zero,
  rw exact.image_eq_kernel f g,
  simp,
end

instance exact.is_iso {A B C : V} (f : A ⟶ B) (g : B ⟶ C) [exact f g] :
  is_iso (image_to_kernel f g (exact.w f g)) :=
begin
  refine ⟨⟨subobject.of_le _ _ (exact.image_eq_kernel f g).ge, _⟩⟩,
  dsimp [image_to_kernel],
  simp only [subobject.of_le_comp, subobject.of_le_refl],
  simp,
end

lemma exact_of_image_to_kernel_is_iso {A B C : V} (f : A ⟶ B) (g : B ⟶ C) (w : f ≫ g = 0)
  [is_iso (image_to_kernel f g w)] : exact f g :=
{ image_eq_kernel := subobject.eq_of_comm (as_iso (image_to_kernel f g w)) (by simp) }

seems like off to a good start.

[Scott Morrison]

@Markus Himmel, I do find some things that I don't know how to prove now without assuming e.g. abelian. With this definition, is

lemma exact_epi_comp [exact g h] [epi f] : exact (f ≫ g) h :=

still true in general?

[Scott Morrison]

(It's fine if we have to assume abelian earlier, of course.)

[Markus Himmel]

The new definition is definitely more restrictive than the old one

[Scott Morrison]

Ok, in any case I'm stopping on homology2 for the night.

[Markus Himmel]

Regarding your proof of exact.w above: it should probably be a lemma that says image_subobject f ≤ kernel_subobject g ↔ f ≫ g = 0 (cf. docs#linear_map.range_le_ker_iff). Also, there is (as there always should be) an arrow-free proof:

begin
  rw [←image.fac f, category.assoc],
  convert comp_zero,
  exact (limits.mk_le_kernel_subobject_iff g (image.ι f)).1 exact.image_eq_kernel.le
end

provided that we add

lemma mk_le_kernel_subobject_iff (g : Z ⟶ X) [mono g] : mk g ≤ kernel_subobject f ↔ g ≫ f = 0 :=
sorry

in limits.lean.