formula for `⊓` in `subobject`

Stream: maths

[Scott Morrison]

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]

(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]

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]

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]

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]

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]

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]

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]

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]

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]

@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]

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

[Bhavik Mehta]

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]

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]

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