cokernels in normed_group/NormedGroup

Stream: condensed mathematics

[Scott Morrison]

It seems in normed_group/NormedGroup.lean that kernels are constructed using the limits API, and then cokernels are constructed "ad hoc", with most of the limits API for cokernels repeated by hand. Is there a good reason for this? If not, I can try to refactor.

Also, I noticed there coker.map and coker.map_lift_comm, which work in any category with cokernels and are not at all specific to normed groups. Again, unless I'm missing something I can replace these.

[Johan Commelin]

The problem is "bounded limits"

[Johan Commelin]

same for equalizers, we also do them by hand

[Johan Commelin]

The problems is, if D : J => NormedGroup is some diagram, and X is the limit of D, then I can pick any norm-increasing isom f : Y \to X and then Y is also a limit, but typically in an unhelpful way.

[Johan Commelin]

In particular, the natural map \iota : equalizer f g -> V_1 cannot be shown to be norm-nonincreasing, if we stick to the usual limits API

[Johan Commelin]

Similar issues with quotients.

[Johan Commelin]

Adam started working on a "bounded limits" API, but I don't know what the status is.

[Scott Morrison]

So should things like instance : limits.has_kernels.{u (u+1)} NormedGroup just be deleted?

[Scott Morrison]

And in any case, the ad hoc development of coker doesn't seem to account for what you say in any way.

[Scott Morrison]

It just repeats the standard setup for cokernel.

[Scott Morrison]

Is it also junk?

[Johan Commelin]

The kernels definitely aren't used.

[Johan Commelin]

Are you talking about

/-- The cokernel of a morphism of normed groups. -/
@[simp]
noncomputable
def coker (f : A ⟶ B) : NormedGroup := NormedGroup.of $
  quotient_add_group.quotient f.range

[Scott Morrison]

Oh, maybe I see: if you just picked any arbitrary categorical cokernel, you wouldn't be able to prove

lemma coker.π_norm_noninc {f : A ⟶ B} :
  (coker.π : B ⟶ coker f).norm_noninc :=

[Johan Commelin]

That one is certainly used.

[Johan Commelin]

Exactly, that silly lemma is crucial!

[Scott Morrison]

So are there (conventional) cokernels in the category of normed groups with non-increasing maps as morphisms?

[Johan Commelin]

Yes, because we use semi-normed groups

[Scott Morrison]

Okay, so my questions above become: can/should someone (e.g. me) refactor the ad hoc development of cokernels, replacing it with the standard limits API version of cokernels in that category?

[Johan Commelin]

I think the concensus was that instead of changing the category, we should extend the limits API

[Johan Commelin]

Because sometimes we want to take limits of maps whose norms are all bounded by C, and get a universal property for maps bounded by C', etc...

[Johan Commelin]

It's not clear to me that we can always assume C = 1 in the proof of 8.19

[Johan Commelin]

Also, to construct the system of complexes that we are interested in, we need to work with norm-increasing maps in intermediary steps.

[Scott Morrison]

Sure. Of course it has to be convenient to step outside the non-increasing morphism subcategory.

[Scott Morrison]

But I'd be happier if I knew a concrete problem that required something more general than (co)limits in the non-increasing map category.

[Johan Commelin]

So, I'm not saying we shouldn't add NormedGroupNormNoninc. But I just want to warn that we can't simply move the entire project over to that category.

[Scott Morrison]

Definitely.

[Johan Commelin]

The proof of 8.19 needs that more general thing.

[Johan Commelin]

But Adam understands the details a lot better than I do