0 \ne 0

Stream: condensed mathematics

[Johan Commelin]

I just got bitten by

@abelian.has_zero_object.{u u+1} Ab.{u} AddCommGroup.large_category.{u} AddCommGroup.category_theory.abelian.{u}
 =
AddCommGroup.has_zero_object.{u}

[Johan Commelin]

cc @Scott Morrison
This showed up in a version of homology = homology

[Johan Commelin]

Should has_zero_object be a Prop?

[Scott Morrison]

Yes. :-)

[Scott Morrison]

I guess it was missed in the big Prop-ification of the limits API.

[Scott Morrison]

I had a quick go at this. I run into trouble because this helpful @[simp] lemma is no longer true:

@[simp] lemma functor.zero_obj {B : Type*} [category B] [has_zero_morphisms C] (X : B) :
  (0 : B ⥤ C).obj X = 0 := rfl

[Scott Morrison]

Because 0 is now produced using choice, there is no reason to expect (0 : B ⥤ C).obj X should be the previously chosen 0: it should be any other (isomorphic) zero object.

[Scott Morrison]

I think resolving this cleanly will requiring installing the is_zero_object predicate in mathlib. If no one has tackled this in a week I will try to get to it then.

[Johan Commelin]

Thanks for diving into this. Note that there is already a lot of API for is_zero(_object) in LTE.

[Scott Morrison]

Pity it's not in mathlib. :-)

[Johan Commelin]

Here's a first PR: https://github.com/leanprover-community/mathlib/pull/13511

[Johan Commelin]

I'm working on turning has_zero_object into a Prop. There are way too many instances of this class in mathlib :see_no_evil: :grinning:

[Johan Commelin]

Here's the next PR:

refactor(category_theory): make has_zero_object a Prop #13517