Zulip Chat Archive

Stream: maths

Topic: formula for `⊓` in `subobject`


Scott Morrison (May 25 2022 at 08:05):

I'd like to have the following formula for inf in subobject A:

import category_theory.subobject.lattice

open category_theory
open category_theory.limits

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

lemma inf_eq_mk_fst_arrow {A : C} {X Y : subobject A} :
  X  Y = subobject.mk ((pullback.fst : limits.pullback X.arrow Y.arrow  X)  X.arrow) :=
sorry

lemma inf_eq_mk_snd_arrow {A : C} {X Y : subobject A} :
  X  Y = subobject.mk ((pullback.snd : limits.pullback X.arrow Y.arrow  Y)  Y.arrow) :=
sorry

Can anyone fill this in? I don't see how to get it from the existing API for . @Bhavik Mehta?

(If one needs to actually unfold the definition of , perhaps the second lemma is easier because docs#category_theory.over.pullback is defined in terms of pullback.snd.)

Scott Morrison (May 25 2022 at 10:00):

(I've found another solution to my problems that don't need these lemmas, but I'm still curious how they should be proved.)

Bhavik Mehta (May 25 2022 at 11:31):

I'm pretty sure I had these lemmas in the topos project a while back, I will take a closer look later today if I can!

Scott Morrison (May 25 2022 at 11:37):

I did manage to prove X ⊔ Y = subobject.mk (image.ι (coprod.desc X.arrow Y.arrow)) (although needed to assume [has_equalizers C]...).

Bhavik Mehta (May 25 2022 at 15:27):

Scott Morrison said:

I'd like to have the following formula for inf in subobject A:

import category_theory.subobject.lattice

open category_theory
open category_theory.limits

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

lemma inf_eq_mk_fst_arrow {A : C} {X Y : subobject A} :
  X  Y = subobject.mk ((pullback.fst : limits.pullback X.arrow Y.arrow  X)  X.arrow) :=
sorry

lemma inf_eq_mk_snd_arrow {A : C} {X Y : subobject A} :
  X  Y = subobject.mk ((pullback.snd : limits.pullback X.arrow Y.arrow  Y)  Y.arrow) :=
sorry

Can anyone fill this in? I don't see how to get it from the existing API for . Bhavik Mehta?

(If one needs to actually unfold the definition of , perhaps the second lemma is easier because docs#category_theory.over.pullback is defined in terms of pullback.snd.)

If it comes to it, I think using antisymm should give this

Bhavik Mehta (May 25 2022 at 15:28):

I've always been very hesitant about subobject.arrow, I expect the easiest way to prove this would be to show it for mono_over using antisymm, and then taking this special case

Scott Morrison (May 25 2022 at 23:42):

If you think it's a good idea I can try to do a refactor of the subobject/ directory, moving as much as possible about arrow into a new arrow.lean.

Scott Morrison (May 25 2022 at 23:42):

I admit I do like to use the arrow API, but maybe it makes sense to make it clearer in the sources that it is an optional extra.

Scott Morrison (May 25 2022 at 23:45):

I'm curious what your preferred formulation of something like

example [...hypotheses on C...] (X : subobject A) : ( Y, is_compl X Y)  ( (Y : C) (i : (X : C)  Y  A), X.arrow = biprod.inl  i.hom) := ...

(stating that "complemented in the lattice sense" and "complemented in the biproduct sense" agree, with whatever hypotheses are required to make it true) would be.

Bhavik Mehta (May 26 2022 at 00:15):

Scott Morrison said:

If you think it's a good idea I can try to do a refactor of the subobject/ directory, moving as much as possible about arrow into a new arrow.lean.

I think it might be nice but I don't have particularly strong feelings on it - I personally prefer to state things without using arrow but I agree there are times when it's needed.

Scott Morrison (May 26 2022 at 06:20):

@Bhavik Mehta (or anyone else!!), any ideas on how to prove

example [has_pullbacks C] [has_initial C] [initial_mono_class C] [has_binary_coproducts C]
  [...more hypotheses on C?...]
  {A : C} {X Y : subobject A} (h : X  Y = ) : mono (coprod.desc X.arrow Y.arrow) :=

either on paper or in Lean? I hope it's true fairly generally, but don't see why yet. Perhaps replacing the coproduct with biproduct could make it easier?

Bhavik Mehta (May 26 2022 at 16:02):

I expect you need https://ncatlab.org/nlab/show/disjoint+coproduct for this to be true

Bhavik Mehta (May 26 2022 at 16:03):

oops wrong way round - I don't think this is true nope I'm not sure again, let me think about this harder

Bhavik Mehta (May 27 2022 at 12:59):

I have a rough idea of a proof which additionally requires that your category has images, and is extensive - namely condition 3 here https://ncatlab.org/nlab/show/extensive+category#extensive_categories; I think I have a formalisation of the equivalence between 1,2,3 in a branch but I expect it's rotted quite a bit now

Scott Morrison (Jun 02 2022 at 05:08):

Hmm... it would be nice to have a proof that works for Vect, which is not extensive.


Last updated: Dec 20 2023 at 11:08 UTC