Add (-)^1 = id

[thjread]

An attempt at https://github.com/b-mehta/topos/issues/18

[b-mehta]

@EdAyers It's curious that we need to define unitor outside, and that

hom_equiv := λ X _, ⟨λ a, (prod.left_unitor X).inv ≫ a, λ a, (prod.left_unitor X).hom ≫ a, by tidy, by tidy⟩

doesn't work

[b-mehta]

You could also show your iso is natural in X. This would follow from uniqueness of adjunctions or you could do it directly

On Wed, 26 Feb 2020, 16:40 thjread, notifications@github.com wrote:

@thjread https://github.com/thjread requested your review on: #21 https://github.com/b-mehta/topos/pull/21 Add (-)^1 = id.

— You are receiving this because your review was requested. Reply to this email directly, view it on GitHub https://github.com/b-mehta/topos/pull/21?email_source=notifications&email_token=AHESIOTPRBX2J2VH5HRUVK3RE2LRTA5CNFSM4K4JQ5NKYY3PNVWWK3TUL52HS4DFWZEXG43VMVCXMZLOORHG65DJMZUWGYLUNFXW5KTDN5WW2ZLOORPWSZGOW5AZKGY#event-3074528539, or unsubscribe https://github.com/notifications/unsubscribe-auth/AHESIOUDM7F3LGAQQE5I3O3RE2LRTANCNFSM4K4JQ5NA .

[thjread]

@EdAyers It's curious that we need to define unitor outside, and that

hom_equiv := λ X _, ⟨λ a, (prod.left_unitor X).inv ≫ a, λ a, (prod.left_unitor X).hom ≫ a, by tidy, by tidy⟩

doesn't work

tidy runs intros x, dsimp at *, simp at *. Looks like in the first case dsimp stops at unitor, so simp just has to prove unitor.hom ≫ unitor.inv ≫ x = x. Whereas in the second case, dsimp expands prod.left_unitor and so would have to re-prove that those are inverses from the definitions.

[b-mehta]

In that case I'm surprised/disappointed that simp can't prove the inverses property - thanks for investigating!

[thjread]

lemma exp_terminal_functor_iso : exp.functor ⊤_C ≅ 𝟭 C :=
  nat_iso.of_components (λ X, exp_terminal_iso)
  (λ _ _ f, yoneda.obj_map_id f.op)

That's a solution, but don't ask me how it works... it would be great if someone could figure out how to do this a sane way. Also I think I'm missing something about how to unfold lemmas - I keep spending a long time trying different combinations of dsimp and unfold, and I couldn't get this to work at all without changing exp_terminal_iso from lemma to def.

[thjread]

lemma exp_terminal_functor_iso2 : exp.functor ⊤_C ≅ 𝟭 C :=
  begin
    refine nat_iso.of_components (λ X, exp_terminal_iso) _,
    intros,
    dsimp [exp_terminal_iso, exp.functor, is_left_adjoint.right],
    change (Y⇐⊤_ C) with Y,
    change (X⇐⊤_ C) with X,
    tidy,
  end

That's a more sane approach, though it feels like it shouldn't need to be this long.

[b-mehta]

Also I think I'm missing something about how to unfold lemmas - I keep spending a long time trying different combinations of dsimp and unfold, and I couldn't get this to work at all without changing exp_terminal_iso from lemma to def.

I think definitions can be unfolded, and lemmas shouldn't be - my vague rule of thumb is that Props are for lemmas, and anything else is for def; in particular exp_terminal_iso is the data of an isomorphism, it should be a def. The idea here is that exp_terminal_iso isn't just a proof that they're iso, it's also the actual functions witnessing the iso - the statement is saying: "here's an iso", not just "there is an iso", so def makes sense. Others may have a different view though

[b-mehta]

Heh.

though it feels like it shouldn't need to be this long.

You were right!

By the way, this works because we defined X <= ⊤_C as X, so the rfls sort everything out

[b-mehta]

In hindsight, this might not be a good idea; in particular I'm anxious about making instance terminal_exponentiable an instance rather than a def. The worry is that if in some other context we get that all objects are exponentiable (for instance if we're assuming a cartesian closed category), then none of the rfls would work; and it's not immediately clear if your above proofs would work. I'll investigate a bit

[b-mehta]

I'll investigate a bit

Not clear what would happen. Can someone else chime in? @EdAyers @Vtec234

[b-mehta]

def terminal_exponentiable : exponentiable ⊤_C :=
{ exponentiable := {
  right := 𝟭 C,
  adj := adjunction.mk_of_hom_equiv
  { hom_equiv := λ X _, have unitor : _, from prod.left_unitor X,
      ⟨λ a, unitor.inv ≫ a, λ a, unitor.hom ≫ a, by tidy, by tidy⟩ } } }

def exp_terminal_iso [exponentiable ⊤_C] : (X⇐⊤_C) ≅ X :=
begin
  apply yoneda.ext (X⇐⊤_ C) X _ _ _ _ _,
  intros Y f, exact (prod.left_unitor Y).inv ≫ exp_transpose.inv_fun f,
  intros Y f, apply f ≫ exp_transpose.to_fun (prod.left_unitor X).hom,
  tidy, 
end

Here's a potential alternative - note how exp_terminal_iso doesn't care how the exponential was constructed.

[Vtec234]

Re instances vs defs, this comment seems relevant. If one might want to construct an object of the same type in a different way, then it probably shouldn't be an instance.

[thjread]

Yeah, that's probably sensible! Should we also put in prodinl ⊤_C ≅ 𝟭 C while we're here?

[thjread]

@b-mehta is the tidy metaphorical in your suggestion? Isn't working for me, and seems to take a surprising amount of effort to fix.

[b-mehta]

@b-mehta is the tidy metaphorical in your suggestion? Isn't working for me, and seems to take a surprising amount of effort to fix.

IIRC the suggestion wasn't complete, I don't think the tidy should have finished the final goal, I just thought that might be a good starting point. I could well have been wrong! I'll take a look when I get a chance, but this might be near the start of next week.

I think the important part was that

def exp_terminal_iso [exponentiable ⊤_C] : (X⇐⊤_C) ≅ X 

expresses that we have an iso, regardless of how exponentiable ⊤_C was done.

[thjread]

No problem - just wanted to check I wasn't wasting time filling in something that was happening automatically for you! Here's an initial go, though I'm sure it can be significantly shortened, and there are a few non-terminal simps/tidys.

lemma prod_left_unitor_naturality (f : X ⟶ Y):
  (prod.left_unitor X).inv ≫ (prodinl ⊤_C).map f = f ≫ (prod.left_unitor Y).inv :=
begin
  apply prod.hom_ext,
  tidy,
  exact id_comp C f
end

def terminal_exponentiable : exponentiable ⊤_C :=
{ exponentiable := {
  right := 𝟭 C,
  adj := adjunction.mk_of_hom_equiv
  { hom_equiv := λ X _, have unitor : _, from prod.left_unitor X,
      ⟨λ a, unitor.inv ≫ a, λ a, unitor.hom ≫ a, by tidy, by tidy⟩ } } }

def exp_terminal_iso [exponentiable ⊤_C] : (X⇐⊤_C) ≅ X :=
begin
  apply yoneda.ext (X⇐⊤_ C) X _ _ _ _ _,
  intros Y f, exact (prod.left_unitor Y).inv ≫ exp_transpose.inv_fun f,
  intros Y f, exact exp_transpose.to_fun ((prod.left_unitor Y).hom ≫ f),
  {
    intros Z g,
    change exp_transpose.to_fun ((prod.left_unitor Z).hom ≫
            ((prod.left_unitor Z).inv ≫ exp_transpose.inv_fun g)) =
      g,
    rw ← category.assoc,
    rw iso.hom_inv_id (prod.left_unitor Z),
    simp,
    rw exp_transpose.right_inv,
  },
  {
    intros Z g,
    change (prod.left_unitor Z).inv ≫ exp_transpose.inv_fun
          (exp_transpose.to_fun ((prod.left_unitor Z).hom ≫ g)) =
      g,
    rw exp_transpose.left_inv,
    rw ← category.assoc,
    rw iso.inv_hom_id (prod.left_unitor Z),
    simp,
  },
  intros Z W f g,
  change (prod.left_unitor W).inv ≫ exp_transpose.inv_fun (f ≫ g)  =
    f ≫ (prod.left_unitor Z).inv ≫ exp_transpose.inv_fun g,
  rw exp_transpose_natural_left_symm,
  rw ← category.assoc, rw ← category.assoc,
  refine congr_arg (λ h, h ≫ exp_transpose.inv_fun g) _,
  exact prod_left_unitor_naturality _,
end

I feel like the morally correct way to do this would be to usthe fact that yoneda reflects isomorphisms, and chain together the left unitor natural isomorphism and the hom isomorphism from the adjunction - don't know if that would run into problems.

[b-mehta]

On a brief skim, this looks great; nice job! I think I agree with your morally correct way - I've also found it tempting to chain together isomorphisms between homs... I also can't tell if that would cause more problems than it would solve though

[b-mehta]

Let's add the stuff in @thjread's last message as well!