Pullbacks of subobjects

Stream: mathlib4

[Pablo Donato]

Consider the following simp lemma in Mathlib.CategoryTheory.Subobject.MonoOver about pullbacks of monomorphisms :

@[simp]
theorem pullback_obj_left (f : X ⟶ Y) (g : MonoOver Y) :
    ((pullback f).obj g : C) = Limits.pullback g.arrow f :=
  rfl

Now I want to descend this into the category of subobjects. A first naive attempt would lead to the following lemma:

@[simp]
theorem pullback_obj_left (f : X ⟶ Y) (S : Subobject Y) :
    ((pullback f).obj S : C) = Limits.pullback S.arrow f :=
  rfl

However the tactic rfl fails because the two sides are not definitionally equal. I suspect this is because of quotients appearing in the constructions on subobjects, i.e. S.arrow uses Subobject.representative to pick a representative of the equivalence class of monomorphisms of S with the axiom of choice.

Hence I would like to relax this equality into an isomorphism, that can be promoted back to an equality using Subobject.eq_mk_of_comm. However after thinking and contemplating the various definitions involved for a few hours, I still have no clue how to proceed to build such an isomorphism.

The only approach I have in mind is to use the universal property of pullbacks (pullback.lift). But this requires a morphism ((pullback f).obj S : C) ⟶ (S : C) forming a pullback span with ((pullback f).obj S).arrow, and I have no idea how to obtain this data from the Subobject API.

Maybe the designers/implementors of the Subobject module could enlighten me (@Bhavik Mehta @Kim Morrison)? Or anyone familiar working with subobjects really. Btw this is part of my WIP formalizing subobject classifiers, available on a separate repo for now.

[Kim Morrison]

Sorry, don't have time to look at this at present.

[Pablo Donato]

I allow myself to reopen this issue, hopefully with a clearer formulation of the problem.

In essence, what I need is to show that the object S' given by the Subobject.pullback functor by pulling back an object S along a morphism f (i.e. S' := (Subobject.pullback f).obj S) is isomorphic to the usual pullback given by Limits.pullback S.arrow f.

Now I can only see three ways of doing this:

1. Show that the pullback span from S' forms a pullback square (formally IsPullback ?fst S'.arrow S.arrow f where ?fst : S' ⟶ S), and then use the unicity of limits up to isomorphism. But the Subobject API does not expose such a pullback square property, let alone a way to refer to ?fst.
2. Build directly the isomorphism by using the universal property of pullbacks. But then to show that it actually is an iso, I need to exhibit an inverse, which I cannot since again I have no way to show that S' is a pullback.
3. Somehow reduce the definition of Subobject.pullback to that of MonoOver.pullback to reuse the MonoOver.pullback_obj_left theorem, but frankly the tower of definitions makes it very diffcult for me to have a mental model of how I could proceed.

Overall, I find it very difficult to do any kind of reasoning up-to-isomorphism, both because it is impossible to rewrite directly isomorphisms AFAIK, and (more related to this case) because it is extremely difficult to build isos not already in the API without an intricate knowledge of the towers of categorical definitions involved in your objects.

I don't know if this is something inherent to category theory even on paper (and people just make believe that they have a rigorous proof), if this is a limitation of (non-univalent) type theory, or just a lack of experience on my end.

[Pablo Donato]

I should also mention that I don't have much experience working with quotient types, but doing quotient induction did not help in my experiments

[Johan Commelin]

I think (3) is your best option. The definition of Subobject.pullback is exactly in terms of MonoOver.pullback and CategoryTheory.Subobject.lower.

Can you state in Lean what you need to make progress?

[Pablo Donato]

ok here it goes:

import Mathlib.CategoryTheory.Subobject.Basic
import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq
import Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

open CategoryTheory
open Limits
open Subobject

namespace CategoryTheory.Subobject

universe u v

variable {C : Type u} [Category.{v} C] [HasPullbacks C]

def pullback_obj_representative {X Y : C} (f : Y ⟶ X) (x : Subobject X) :
    ((Subobject.pullback f).obj x : C) ≅ ((MonoOver.pullback f).obj (representative.obj x) : C) := by
  sorry

noncomputable def pullback_obj_left {X Y : C} (f : Y ⟶ X) (x : Subobject X) :
    ((Subobject.pullback f).obj x : C) ≅ Limits.pullback x.arrow f := by
  calc
        ((Subobject.pullback f).obj x : C)
    _ ≅ ((MonoOver.pullback f).obj (representative.obj x) : C) := pullback_obj_representative _ _
    _ = Limits.pullback (representative.obj x).arrow f := MonoOver.pullback_obj_left _ _
    _ = Limits.pullback x.arrow f := by rw [representative_arrow]

lemma pullback_obj {X Y : C} (f : Y ⟶ X) (S : Subobject X) :
    (pullback f).obj S = Subobject.mk (pullback.snd S.arrow f) := by
  refine eq_mk_of_comm (pullback.snd S.arrow f) (pullback_obj_left f S) ?_
  sorry

I am interested in pullback_obj which is used elsewhere in my development, and I think the only way to go is to first prove pullback_obj_left, which I do by reducing to an isomorphism pullback_obj_representative that relates Subobject.pullback and MonoOver.pullback. Now it remains to build this isomorphism, and show that it commutes with the arrows

[Johan Commelin]

I'm sorry I don't have more time atm, but here are two things that I would try:

lemma pullback_obj_representative {X Y : C} (f : Y ⟶ X) (x : Subobject X) :
    (Subobject.pullback f).obj x = mk ((MonoOver.pullback f).obj (representative.obj x)).arrow := by
  induction' x using Quotient.inductionOn' with g
  dsimp [pullback, lower]
  sorry

lemma pullback_obj {X Y : C} (f : Y ⟶ X) (S : Subobject X) :
    (pullback f).obj S = Subobject.mk (pullback.snd S.arrow f) := by
  revert S
  apply Subobject.ind
  intro Z g hg
  sorry

[Pablo Donato]

thanks for the help! I have been able to prove pullback_obj_representative :

lemma pullback_obj_representative {X Y : C} (f : Y ⟶ X) (x : Subobject X) :
    (Subobject.pullback f).obj x = Subobject.mk ((MonoOver.pullback f).obj (representative.obj x)).arrow := by
  induction' x using Quotient.inductionOn' with m
  unfold pullback lower
  rw [Quotient.mk''_eq_mk, mk_eq_mk']
  dsimp
  apply Quotient.sound
  constructor
  apply Functor.mapIso (MonoOver.pullback f)
  symm
  exact (representativeIso _)

with the help of an auxiliary trivial lemma mk_eq_mk':

lemma mk_eq_mk' {X : C} (m : MonoOver X) :
    Subobject.mk m.arrow = ⟦m⟧ :=
  rfl

I would be happy to get feedback if you think there is a simpler way to write the proof!

[Pablo Donato]

For now I still find it quite unnatural to reason with quotients and isomorphisms, since I had to navigate between 4 different notions of "equality": =, ≅, ≈, and ≃, which stand respectively for strict equality (the only one that I know how to manipulate naturally with rw), (categorical) isomorphism, equivalence as defined by Lean core's HasEquiv, and equivalence as defined by mathlib's Equiv (which I actually don't need, but I was still confused by the coexistence of two notations/definitions for the same thing). But maybe I should ask for explanations on this in #new members

[Pablo Donato]

ok I've now solved trivially pullback_obj:

lemma pullback_obj {X Y : C} (f : Y ⟶ X) (x : Subobject X) :
    (Subobject.pullback f).obj x = Subobject.mk (pullback.snd x.arrow f) := by
  rw [pullback_obj_representative]
  rfl

topic can be marked as resolved :)