Stacks definition of abelian cats

Stream: Is there code for X?

[Adam Topaz]

Do we have a constructor for docs#category_theory.abelian which directly follows the definition on the stacks project https://stacks.math.columbia.edu/tag/0109 ?

[Johan Commelin]

I think we have only two constructors. The definition, and the one that avoids preadditive

[Johan Commelin]

In src/category_theory/abelian/non_preadditive.lean

[Adam Topaz]

Yeah, those were the only two I found as well. And I'm fairly sure the answer is no, since docs#category_theory.abelian.coimages.coimage requires [abelian A] for some reason...

[Johan Commelin]

In both cases you need to provide

(normal_mono : Π {X Y : C} (f : X ⟶ Y) [mono f], normal_mono f)
(normal_epi : Π {X Y : C} (f : X ⟶ Y) [epi f], normal_epi f)

which is what you are trying to avoid, I guess

[Adam Topaz]

yeah exactly.

[Adam Topaz]

As you can probably guess, I'm starting to think about how to formalize the fact that abelian sheaves form an abelian category. I want to do this with an arbitrary abelian category A as opposed to just Ab, since we could then apply it to R-mod as well. In any case, I'm finding working with normal_mono and normal_epi to be a big pain, and I think working directly with kernels/cokernels should be easier.

[Johan Commelin]

I've never used normal mono/epi maps before. How hard is it to build the new stacks-like constructor?

[Adam Topaz]

I'm trying now...

[Adam Topaz]

Well, I didn't get very far, and I need to go to sleep. In case you want to give it a go, here's a skeleton:

import category_theory.abelian.basic
import category_theory.additive.basic

namespace category_theory
open category_theory.limits

variables {C : Type*} [category C] [additive_category C] [has_kernels C] [has_cokernels C]

noncomputable theory

abbreviation coim {X Y : C} (f : X ⟶ Y) := cokernel (kernel.ι f)
abbreviation im {X Y : C} (f : X ⟶ Y) := kernel (cokernel.π f)

def coim_to_im {X Y : C} (f : X ⟶ Y) : coim f ⟶ im f :=
cokernel.desc _ (kernel.lift _ f (cokernel.condition _)) $
  by { ext, simp only [zero_comp, kernel.condition, category.assoc, kernel.lift_ι] }

def abelian_of_coim_to_im (h : ∀ {X Y : C} (f : X ⟶ Y), is_iso (coim_to_im f)) : abelian C :=
{ normal_mono := λ X Y f hf,
  { Z := cokernel f,
    g := cokernel.π _,
    w := cokernel.condition _,
    is_limit := is_limit_aux _
    (λ S, _) _ _ },
  normal_epi := _, }

end category_theory

[Johan Commelin]

I'm looking at it

[Johan Commelin]

Is the empty category abelian?

[Johan Commelin]

According to the stacks project: yes

[Kevin Buzzard]

I'm surprised -- aren't they supposed to have a zero object? You don't mean the "zero category"?

[Johan Commelin]

According to mathlib, it has at least a zero object.

import category_theory.abelian.basic
import category_theory.additive.basic
import algebra.homology.exact

namespace category_theory
open category_theory.limits

noncomputable
example (A : Type*) [category A] [abelian A] : has_zero_object A := by apply_instance -- works

[Johan Commelin]

https://stacks.math.columbia.edu/tag/0109 ?

I don't think that :this: gives you any objects.

[Kevin Buzzard]

It's the first axiom on Wikipedia

[Johan Commelin]

Who is correcter, wiki or stacks?

[Johan Commelin]

Maybe some random dude wrote that wiki page. It's his word against Johan de Jong :rofl:

[Filippo A. E. Nuccio]

It seems reasonable for it to be abelian, though, no?

[Kevin Buzzard]

not for me, really. That's like saying it's reasonable for the empty set to be a group

[Filippo A. E. Nuccio]

Well, but I see the zero object being only defined by a universal property, which is satisfied for the empty category. I don't see the identity of a group as the same thing.

[Johan Commelin]

@Filippo A. E. Nuccio Does the empty category have all finite products?

[Johan Commelin]

Answer: nope, it lacks the empty product

[Johan Commelin]

Which is bad, I think

[Kevin Buzzard]

it's not true that the universal property is satisfied for the empty category. Any universal property you write down for the zero object will say that there is some zero object surely.

[Filippo A. E. Nuccio]

Oh, nice! I see my mistake (and there are two, actually).

[Kevin Buzzard]

Johan (de Jong) is just wrong, he's written something, he's forgotten a bit, he's made mistakes before, it's a one man show, he relies on people fixing his stuff, just make a comment.

[Filippo A. E. Nuccio]

Thanks: OK, I give up my battle :white_flag:

[Kevin Buzzard]

When we were formalising schemes I noticed his definition of presheaf on a basis was wrong. Of course there are mistakes, nobody refereed this stuff.

[Johan Commelin]

I'll make a comment

[Johan Commelin]

In fact, I'll create a PR (-;

[Johan Commelin]

https://github.com/stacks/stacks-project/pull/120

[Kevin Buzzard]

Oh but he demands finite products in https://stacks.math.columbia.edu/tag/0104 so he's OK

[Johan Commelin]

Ooh, good point.

[Johan Commelin]

I think

instance (D : Type*) [category D] [has_zero_morphisms D] [has_finite_biproducts D] : nonempty D :=
let Z : D := biproduct (λ i : ulift (fin 0), i.down.elim) in ⟨Z⟩

was missing.

[Johan Commelin]

@Adam Topaz Sorry free:

def abelian_of_coim_to_im (h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), is_iso (coim_to_im f)) :
  abelian C :=
{ normal_mono := λ X Y f hf, by exactI normal_mono_of_mono f h,
  normal_epi := λ X Y f hf, by exactI normal_epi_of_epi f h, }

[Johan Commelin]

I pushed it to LTE:

commit 8c17a5d4821fa382eda233afbebf8dba1ccec540 (HEAD -> master, origin/master, origin/HEAD)
Author: Johan Commelin <johan@commelin.net>
Date:   Tue Nov 16 10:17:38 2021 +0000

    abelian cats constructor a la Stacks

 src/for_mathlib/abelian_of_isom_thm.lean | 160 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 160 insertions(+)

[Patrick Massot]

Did you mean "à la Stacks"?

[Johan Commelin]

Sorry for my brutal asciification

[Scott Morrison]

I hadn't noticed this thread, and was planning to work on exactly this constructor. Fortunately, while googling around to for an informal proof, I found the public archive of this thread. :-) I've done half the tidying-up work to move this to mathlib now, and just need to migrate some more lemmas into earlier files and write more doc-strings.

[Johan Commelin]

search engines are noticing our efforts... I like it

[Scott Morrison]

#12972