remove some nonterminal simps?

Stream: general

[Scott Morrison]

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

@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))) :=
begin
  rw [← category.id_comp ((id ℱ).inv.app (op U)), ← nat_iso.app_inv, iso.comp_inv_eq],
  dsimp [id],
  rw colimit.ι_desc_assoc,
  dsimp,
  rw [← ℱ.map_comp, ← ℱ.map_id], refl,
end

[Scott Morrison]

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]

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:

Me:

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) :=
adjunction.nat_iso_of_right_adjoint_nat_iso
  (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.

Andrew:

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