Zulip Chat Archive

Stream: general

Topic: Show the objects for an equality of morphisms


view this post on Zulip Bhavik Mehta (Apr 22 2020 at 16:33):

In the middle of an involved proof, I've got a goal which looks like (pullback.snd ≫ prod.fst) ≫ pullback.snd ≫ prod.snd = pullback.snd ≫ prod.snd ≫ f.hom. Now this is super opaque, though I'm pretty sure the maths proof should be an easy diagram chase. What would be super helpful then is to see the actual objects involved here so it looks a bit more like (pullback.snd ≫ limits.prod.fst) ≫ pullback.snd ≫ (limits.prod.snd : _ ⨯ B ⟶ B) = pullback.snd ≫ (limits.prod.snd : Q f ⨯ f.left ⟶ f.left) ≫ (f.hom : f.left ⟶ B) (ideally some more, but I've just put these in manually. Essentially I'd like something between the default pretty printer and pp.implicit true - is this possible? (of course under an option)

view this post on Zulip Reid Barton (Apr 22 2020 at 16:35):

Hmm, if you made a local notation for with the objects involved explicit, I think the pretty printer would use it over .

view this post on Zulip Bhavik Mehta (Apr 22 2020 at 16:38):

This seems promising - how do I make the objects explicit in a notation though?

view this post on Zulip Reid Barton (Apr 22 2020 at 16:39):

Just get them involved in the notation

view this post on Zulip Bhavik Mehta (Apr 22 2020 at 16:40):

local notation f `% ` A ` %` g := (f : _  A)  (g : A  _)

like this?

view this post on Zulip Bhavik Mehta (Apr 22 2020 at 16:40):

That doesn't seem to work for me... Am I missing some priority thing?

view this post on Zulip Reid Barton (Apr 22 2020 at 16:40):

hmm

view this post on Zulip Reid Barton (Apr 22 2020 at 16:41):

I don't know

view this post on Zulip Bhavik Mehta (Apr 22 2020 at 16:41):

I'll make a MWE, one sec

view this post on Zulip Bhavik Mehta (Apr 22 2020 at 16:45):

import category_theory.category

open category_theory
universes v u

variables {C : Type u} [𝒞 : category.{v} C]
include 𝒞

local notation f `# ` A ` #` g := (f : _  A)  g

example {P Q R S : C} (f : P  Q) (g : Q  R) (h : R  S) : f  g  h = ((f  g)  h) :=
begin

end

view this post on Zulip Kevin Buzzard (Apr 22 2020 at 17:22):

notation B ` & ` f `# ` A ` #` g ` & ` C := (f : B  A)  (g : A  C)

doesn't work either

view this post on Zulip Bhavik Mehta (May 01 2020 at 00:33):

A hack which does the job for now: def tag' (n : ℕ) (A B : C) (f : A ⟶ B) : A ⟶ B := f

view this post on Zulip Bhavik Mehta (May 01 2020 at 00:34):

Then when my goal is pullback m₁ m₂ ⟶ pullback pullback.snd pullback.snd, I can write

view this post on Zulip Bhavik Mehta (May 01 2020 at 00:34):

change pullback m₁ m₂ ⟶ pullback (tag' 0 _ _ pullback.snd) (tag' 1 _ _ pullback.snd),

view this post on Zulip Bhavik Mehta (May 01 2020 at 00:34):

which changes the goal to pullback m₁ m₂ ⟶ pullback (tag' 0 (pullback (mem (⊤_ C)) (prod.map (hat (m₂ ≫ prod.lift (𝟙 E) (terminal.from E))) (𝟙 (⊤_ C)))) (E ⨯ ⊤_ C) pullback.snd) (tag' 1 (pullback (mem (⊤_ C)) (prod.map (hat (m₁ ≫ prod.lift (𝟙 E) (terminal.from E))) (𝟙 (⊤_ C)))) (E ⨯ ⊤_ C) pullback.snd), which is more helpful


Last updated: May 11 2021 at 13:22 UTC