Zulip Chat Archive

Stream: condensed mathematics

Topic: salamander/ab cat stuff

Kevin Buzzard (Apr 12 2022 at 15:12):

I'm taking a break from marking and so I pulled LTE. The most noticeable thing was a new 1000 line file from Johan called for_mathlib/salamander which does a lot of diagram-chasology but is not quite sorry-free. I drew the diagram for the first sorry and it seems to me that the missing ingredient is that if A B C : \C^op and f: A-> B and g:B->C with gf=0 then you can make a commuting square from this picture with ker(g) being the fourth vertex, the map from A to ker(g) is called something like kernel.lift and the map from ker(g) to C is 0. Now you can take the unop of this entire diagram and get a commuting square in the original abelian category C but you can also make it by hand using coker(g^unop) and cokernel.desc. What we need is that "these diagrams are the same". How is one expected to prove this? I'm reminded of what we did in version 1 of schemes where we had to prove a ton of diagrams commuted and we just bashed it all out. But is there some sort of more sophisticated approach? I'm assuming (ker g)^unop isn't equal to coker(g^unop) in general. In schemes we introduced an "is_localisation" predicate. Do we have an "is_cokernel" predicate here because that would be one way to proceed. Or do people have completely different ideas about how to go about this?

Johan Commelin (Apr 12 2022 at 15:14):

Yeah, there are 5 annoying sorries left in that file. But once we have those filled in, we'll have a very nice atomic building block for diagram chases in double complexes.

As you can see, Bhavik wasn't a fan.

Reid Barton (Apr 12 2022 at 15:32):

nonono

Adam Topaz (Apr 12 2022 at 15:33):

I guess Reid is not a fan either ;)

Kevin Buzzard (Apr 12 2022 at 17:47):

The argument against is that it carries data but surely you can somehow bundle everything together and have a prop-valued predicate. Oh I guess the point is then that it can't be a class

Adam Topaz (Apr 12 2022 at 17:51):

I don't think it's a problem for it to contain data. Yes, if we start throwing a bunch of instances of such classes in mathlib, that would be bad, but if we are conservative about what instances are declared as such, I don't think it would be a problem.

This is_zero that I suggested in the link above is a special case that was added to LTE and it works very nicely.
We could add is_cokernel and is_kernel as well, and I would guess they would be just as nice to work with in practice.

Kevin Buzzard (Apr 12 2022 at 17:52):

But as Bhavik pointed out, is_zero doesn't have any data. Somehow you have to remember the map as well as the object with is_cokernel

Adam Topaz (Apr 12 2022 at 17:53):

Yeah, but that map is unique given the properties it satisfies.

Adam Topaz (Apr 12 2022 at 18:18):

Here's some code for the special case of cokernels.

import category_theory.abelian.basic

namespace category_theory

variables {C : Type*} [category C] [abelian C]

class is_cokernel {X Y : C} (f : out_param (X ⟶ Y)) (Z : C) :=
(π' : Y ⟶ Z)
(h1 : f ≫ π' = 0)
(h2 : nonempty (limits.is_colimit (limits.cokernel_cofork.of_π _ h1)))

variables {X Y : C} (f : X ⟶ Y) (Z : C) [is_cokernel f Z]

def is_cokernel.π {X Y : C} (f : X ⟶ Y) (Z : C) [is_cokernel f Z] : Y ⟶ Z :=
is_cokernel.π' X

@[simp, reassoc]
lemma is_cokernel.condition : f ≫ is_cokernel.π f Z = 0 :=
is_cokernel.h1

def is_cokernel.cofork : limits.cokernel_cofork f :=
limits.cokernel_cofork.of_π (is_cokernel.π f Z) (is_cokernel.condition f Z)

noncomputable
def is_cokernel.is_colimit : limits.is_colimit (is_cokernel.cofork f Z) :=
is_cokernel.h2.some

noncomputable
def is_cokernel.desc {W : C} (g : Y ⟶ W) (w : f ≫ g = 0) : Z ⟶ W :=
(is_cokernel.is_colimit f Z).desc $ limits.cokernel_cofork.of_π g w

@[simp, reassoc]
lemma is_cokernel.fac {W : C} (g : Y ⟶ W) (w : f ≫ g = 0) :
  is_cokernel.π f Z ≫ is_cokernel.desc f Z g w = g :=
(is_cokernel.is_colimit f Z).fac (limits.cokernel_cofork.of_π g w) (limits.walking_parallel_pair.one)

lemma is_cokernel.uniq {W : C} (g : Y ⟶ W) (w : f ≫ g = 0) (m : Z ⟶ W)
  (hm : is_cokernel.π f Z ≫ m = g) : m = is_cokernel.desc f Z g w :=
begin
  apply (is_cokernel.is_colimit f Z).uniq (limits.cokernel_cofork.of_π g w) m,
  rintros (_|_), { simp }, { exact hm }
end

@[ext]
lemma is_cokernel.hom_ext {W : C} (m₁ m₂ : Z ⟶ W) (h : is_cokernel.π f Z ≫ m₁ = is_cokernel.π f Z ≫ m₂) :
  m₁ = m₂ :=
begin
  apply (is_cokernel.is_colimit f Z).hom_ext,
  rintros (_|_), { simp }, { exact h },
end

noncomputable
def is_cokernel.iso (Z' : C) [is_cokernel f Z'] : Z ≅ Z' :=
(is_cokernel.is_colimit f Z).cocone_point_unique_up_to_iso (is_cokernel.is_colimit f Z')

@[simp]
lemma is_cokernel.iso_hom (Z' : C) [is_cokernel f Z'] :
  (is_cokernel.iso f Z Z').hom = is_cokernel.desc f Z (is_cokernel.π f Z') (is_cokernel.condition f Z') := rfl

@[simp]
lemma is_cokernel.iso_inv (Z' : C) [is_cokernel f Z'] :
  (is_cokernel.iso f Z Z').inv = is_cokernel.desc f Z' (is_cokernel.π f Z) (is_cokernel.condition f Z) := rfl

end category_theory

Adam Topaz (Apr 12 2022 at 18:28):

Oh, and of course we can't forget

noncomputable
instance cokernel_is_cokernel : is_cokernel f (limits.cokernel f) :=
{ π' := limits.cokernel.π _,
  h1 := by simp,
  h2 := nonempty.intro $
  { desc := λ (S : limits.cokernel_cofork _), limits.cokernel.desc _ S.π $ by simp,
    fac' := by { rintro (S : limits.cokernel_cofork _) (_|_), { simp }, { simp } },
    uniq' := begin
      rintro (S : limits.cokernel_cofork _) m h,
      apply limits.coequalizer.hom_ext,
      simpa using h limits.walking_parallel_pair.one,
    end }
}

Kevin Buzzard (Apr 12 2022 at 22:12):

Does this make the sorry easier? Does it really need to be a class rather than just a structure?

Kevin Buzzard (Apr 12 2022 at 22:13):

docs#is_localization

Kevin Buzzard (Apr 12 2022 at 22:14):

That's a class but also a Prop. Can you make pi' be an input rather than a field? Could it be a predicate on the morphism rather than the object?

Adam Topaz (Apr 12 2022 at 22:22):

It doesn't need to be a class. If you're happy with a structure, then you can carry around a term of type limits.is_colimit (limits.cokernel_cofork.of_π _ _) (that what we currently have).

Adam Topaz (Apr 12 2022 at 22:30):

From a purely philosophical point of view, what do you think of when you think of a limit? Say just a product $X \times Y$ .
From my perspective, it's an object, say $P$ , which is endowed with the data of two projections $P \to X$ and $P \to Y$ which satisfy some axioms. Yes, the two projections $P \to X$ and $P \to Y$ are additional data, and the additional axioms are propositions.

I think it would be nice to be able to write [is_product X Y P] and get pi_1 : P \to X and pi_2 : P \to Y (as well as the axioms) as part of the class..

Reid Barton (Apr 12 2022 at 23:51):

For me the salient example is a square being a pullback (or pushout), which has a pasting/cancellation property that seems more or less impossible to express in this language.

Reid Barton (Apr 12 2022 at 23:53):

But the same kind of issue arises even for products, e.g. a model of a Lawvere theory is a functor that preserves products and this also seems not to fit well with the [is_product X Y P] class

Johan Commelin (May 09 2022 at 21:27):

We can probably avoid using the salamander lemma file. So there's no hurry to work on the remaining sorrys in salamander.lean.

Last updated: Dec 20 2023 at 11:08 UTC