feat(category_theory/limits): kernels

[semorrison]

Another special shape, as we crawl towards the basics of homological algebra...

[jcommelin]

What a lovely proof.

[semorrison]

There's actually a Lean bug/feature(?) I noticed recently, that prevented me from simplifying quite a few proofs in the limits library to this form. Apparently when you use auto_param in a class field, it can turn implicit arguments back into explicit ones... I'll see if I can pin it down.

[rwbarton]

I actually don't really like this style of proof from a software engineering point of view, at least in this case. It's too much "action at a distance". Suppose you want to know how the zero morphisms in your category are defined. Even once you have tracked them down to this instance : has_zero_morphisms.{v} C, you still need to figure out why there is no definition of has_zero provided and that it comes from an instance 10 lines above.

Much clearer to simply replace everything so far in this section by

/-- A category with a zero object has zero morphisms. -/
instance : has_zero_morphisms.{v} C :=
{ has_zero := λ X Y, ⟨inhabited.default (X ⟶ 0) ≫ inhabited.default (0 ⟶ Y)⟩,
  comp_zero' := λ X Y f Z, by { dunfold has_zero.zero, rw ←category.assoc, congr, },
  zero_comp' := λ X Y Z f, by { dunfold has_zero.zero, rw category.assoc, congr, }, }

[semorrison]

Indeed, that was horrible. Fixed.

[semorrison]

Thanks, @robertylewis, for the reminders about missing docs!

[jcommelin]

Looks good to me. I'm only wondering if we need to support some sort of multiplicative version... we might want to have short exact sequences 1 → µ_n → Gm → Gm → 1 at some point...

[jcommelin]

Looks good to me. @rwbarton Do you have any remarks?

[rwbarton]

How about an example: AddCommGroup? (Or the rest of the monoid/group categories, though we probably only care about AddCommGroup.)

[rwbarton]

I actually don't really like this style of proof from a software engineering point of view, at least in this case. It's too much "action at a distance". Suppose you want to know how the zero morphisms in your category are defined. Even once you have tracked them down to this instance : has_zero_morphisms.{v} C, you still need to figure out why there is no definition of has_zero provided and that it comes from an instance 10 lines above.

Much clearer to simply replace everything so far in this section by

/-- A category with a zero object has zero morphisms. -/
instance : has_zero_morphisms.{v} C :=
{ has_zero := λ X Y, ⟨inhabited.default (X ⟶ 0) ≫ inhabited.default (0 ⟶ Y)⟩,
  comp_zero' := λ X Y f Z, by { dunfold has_zero.zero, rw ←category.assoc, congr, },
  zero_comp' := λ X Y Z f, by { dunfold has_zero.zero, rw category.assoc, congr, }, }

[rwbarton]

Any reason to treat this zero differently than has_zero in has_zero_morphisms? (But see below.)

[rwbarton]

is_initial and is_terminal should exist, and these conditions should be expressed in terms of them.

[rwbarton]

I'm a little reluctant to add more stuff on top of special shapes when they aren't really finished, as discussed in #1444. However, I guess we can always change it later.

This PR adds entirely too many instances of the form instance : some_class C where C is a variable. I think they are probably all bad. For example, take instance : has_zero_morphisms.{v} C, which I'll name zero_morphisms_of_zero_object. Imagine that we also have the following two instances.

variables (D : Type u') [𝒟 : category.{v'} D]
include 𝒟

instance functor.has_zero_morphisms [has_zero_morphisms.{v'} D] :
  has_zero_morphisms.{max u v'} (C ⥤ D) :=
{ has_zero := λ F G, ⟨{ app := λ X, 0 }⟩ }

local attribute [elab_simple] inhabited.default
instance functor.has_zero_object [has_zero_object.{v'} D] : has_zero_object.{max u v'} (C ⥤ D) :=
{ zero := (category_theory.functor.const C).obj 0,
  unique_from := λ F, { default := { app := λ X, inhabited.default (F.obj X ⟶ 0) }, uniq := by tidy },
  unique_to := λ F, { default := { app := λ X, inhabited.default (0 ⟶ F.obj X) }, uniq := by tidy } }

These are sensible instances because they work by "structural recursion" on the type C ⥤ D, and they say two different things. Now, there are two ways to get from has_zero_object.{v'} D to has_zero_morphisms.{max u v'} (C ⥤ D): we could apply zero_morphisms_of_zero_object to D and then functor.has_zero_morphisms, or we could apply functor.has_zero_object and then zero_morphisms_of_zero_object. To my immense disappointment, these two ways resulted in definitionally equal has_zero_morphisms.{max u v'} (C ⥤ D) instances, so this isn't necessarily a disaster. However, it's not clear to me that we can expect this to hold for every similar construction.

I would rather make all the instances in this PR into definitions, which can be used either to define instances for specific categories, or locally made into instances where desired for proving general theorems (although this still has its own dangers, since we may not easily be able to apply those general theorems to specific categories where the expected definitional equalities do not hold).

[rwbarton]

Finally, I worry we are accumulating definitions at too high a rate relative to examples and especially theorems, though I'm not sure off-hand what kind of theorems to suggest proving...

[rwbarton]

Even things like the kernel of a (regular?) monomorphism is initial/terminal/zero (whatever is the correct statement in general here) or that the kernel of the zero map is an isomorphism would be a good start.

[semorrison]

I dealt with some of these comments. I'll get started on "proving some stuff" ... sometime! For now I'll mark as [WIP].

[semorrison]

For (even my own) future reference, we should:

• Construct has_zero_object e.g. for AddCommGroup, possibly others.
• Connect kernel to the concrete version in some examples.
• Prove some basic lemmas, e.g. about the kernel of the zero map being an iso.

[semorrison]

I'm going to close this, to work on later.

[TwoFX]

Hi, I'd be interested in "adopting" this PR and finishing the remaining work that needs to be done. I have been working on zero objects and kernels independently (and only just discovered this PR), and while I used very slightly different definitions, I have proofs that the kernel of a monomorphism is zero and that the kernel of the zero map is an isomorphism and I am certain they can be ported easily. I'd also be happy to create some of the concrete instances and fill in the missing proofs.

@semorrison, would you prefer to work on this yourself or could I give it a try?

[semorrison]

Please adopt!

…

On Tue, Feb 11, 2020, 7:11 AM Markus Himmel ***@***.***> wrote: Hi, I'd be interested in "adopting" this PR and finishing the remaining work that needs to be done. I have been working on zero objects and kernels independently (and only just discovered this PR), and while I used very slightly different definitions, I have proofs that the kernel of a monomorphism is zero and that the kernel of the zero map is an isomorphism and I am certain they can be ported easily. I'd also be happy to create some of the concrete instances and fill in the missing proofs. @semorrison <https://github.com/semorrison>, would you prefer to work on this yourself or could I give it a try? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#1445?email_source=notifications&email_token=AADUWBDTYX7ZGXCLZ6I36WTRCK52PA5CNFSM4IW52U4KYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOELMYZ5I#issuecomment-584682741>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AADUWBGG47LPDU6ANPK3YGTRCK52PANCNFSM4IW52U4A> .