Zulip Chat Archive

Stream: general

Topic: remove some nonterminal simps?

Scott Morrison (May 20 2022 at 01:24):

@Andrew Yang, src#Top.presheaf.pullback.id_inv_app (and id above) has a nonterminal simp that is breaking a refactor I'm attempting, and I can't immediately see how to fix it. Would you (or anyone else?) be able to rewrite this proof for me?

Adam Topaz (May 20 2022 at 01:57):

@Scott Morrison I came up with the following proof... I hope this helps!

lemma id_inv_app (U : opens Y) :
  (id ).inv.app (op U) = colimit.ι (Lan.diagram (opens.map (𝟙 Y)).op  (op U))
    (@costructured_arrow.mk _ _ _ _ _ (op U) _ (eq_to_hom (by simp))) :=
  rw [ category.id_comp ((id ).inv.app (op U)),  nat_iso.app_inv, iso.comp_inv_eq],
  dsimp [id],
  rw colimit.ι_desc_assoc,
  rw [ ℱ.map_comp,  ℱ.map_id], refl,

Scott Morrison (May 20 2022 at 01:59):

Great, works even in the refactor branch. src#Top.presheaf.pullback.id also has a non-terminal simp, but ... don't fix what ain't broke? If anyone is keen to do that one I can include it in a PR.

Junyan Xu (May 23 2022 at 08:25):

I've been able to construct pullback.id in another way but never cleaned it up for PR. This isomorphism should be seen as a part of the pushback pseudofunctor, namely docs#category_theory.pseudofunctor.id. The right way to obtain it is by transferring the pushforward (strict) pseudofunctor across the pushforward-pullback adjunction, which I have established in the generality of (op)lax functors, but never cleaned up to fit in the new bicategory framework built by @Yuma Mizuno; I also wanted to change to proofs to use docs#category_theory.adjunction.hom_equiv instead of unit/counit/traingle identities, which I think would make it more conceptual.

When I get back to formalizing Gillam's proof of the completeness of LocallyRingedSpace, I'll eventually PR this part, but I can't say when it'll happen. In the meantime, feel free to clean up my code and PR, or come up with your own better code! It would be more meaningful if you show that the Grothendieck construction associated to the transferred lax functor is opposite to the Grothendieck construction of the original lax functor, with the generalization of Grothendieck construction to lax functors in branch#lax_grothendieck_bicat.

In private (Zulip) communication, @Andrew Yang has granted me permission to change src#Top.presheaf.pullback.id, so you shouldn't worry about changing it:


I see that you took several steps to establish that pullback_obj (𝟙 _) ℱ ≅ ℱ. Is there any particular advantage of your explicit definition? If you just want the isomorphism, you can use uniqueness of adjoint functor up to iso:

def id_iso {X : Top.{v}} : pullback C (𝟙 X)  𝟭 (X.presheaf C) :=
  (pushforward_pullback_adjunction C (𝟙 X))
  adjunction.id $
  eq_to_iso (pushforward_id C)

This more abstract definition seems more natural to me and I imagine would make proving weak functor axioms. Currently I'm trying to prove that both definitions are equal.


Feel free to change that. I thought that it would be useful if there was an explicit form for f1F(U)f^{-1}\mathscr{F}(U) if f(U)f(U) is open. The id thing was just a plus.

Last updated: Aug 03 2023 at 10:10 UTC