Proving the composition law for functoriality of adjoints

[JasonGross]

Continuing from #627, I have the pasting diagram

I guess I want to get rid of the ϵ′ η′ by adjunction laws. But this diagram is reversed from how I read it off from Coq. I should figure out why the pasting diagram I hand-generated is not the one I see in Coq here:*

ε'' (f x) ∘ f'' ₁ (λ' (f x) ∘ λ (f x) ∘ η x) =
   ε' (f x) ∘ f' ₁ (λ (f x) ∘ η x) ∘ (ε'' (f' x) ∘ f'' ₁ (λ' (f' x) ∘ η' x))

(I should also figure out how to get Coq to draw me pasting diagrams automatically, because it usually takes me about an hour to turn a goal into a diagram manually.)

I will probably look at this in the next day or two or three, but if anyone else want's to tell me what I'm missing, I'd be happy to have that, too.

*The goal at that point is:

1 subgoals, subgoal 1 (ID 90)

  H : Funext
  C : PreCategory
  D : PreCategory
  G : Functor D C
  G' : Functor D C
  G'' : Functor D C
  T : NaturalTransformation G G'
  T' : NaturalTransformation G' G''
  M : forall x : C, (x / G)%category
  HM : forall Y : C, IsInitialMorphism (M Y)
  M' : forall x : C, (x / G')%category
  HM' : forall Y : C, IsInitialMorphism (M' Y)
  M'' : forall x : C, (x / G'')%category
  HM'' : forall Y : C, IsInitialMorphism (M'' Y)
  x : C
  ============================
   ((counit (adjunction__of__initial_morphism HM''))
      ((functor__of__initial_morphism HM) x)
    o (functor__of__initial_morphism HM'')
      _1 (T' ((functor__of__initial_morphism HM) x)
          o T ((functor__of__initial_morphism HM) x)
          o (unit (adjunction__of__initial_morphism HM)) x))%morphism =
   ((counit (adjunction__of__initial_morphism HM'))
      ((functor__of__initial_morphism HM) x)
    o (functor__of__initial_morphism HM')
      _1 (T ((functor__of__initial_morphism HM) x)
          o (unit (adjunction__of__initial_morphism HM)) x)
    o ((counit (adjunction__of__initial_morphism HM''))
         ((functor__of__initial_morphism HM') x)
       o (functor__of__initial_morphism HM'')
         _1 (T' ((functor__of__initial_morphism HM') x)
             o (unit (adjunction__of__initial_morphism HM')) x)))%morphism

If I use notation:

        Notation ε := (counit (adjunction__of__initial_morphism HM)).
        Notation ε' := (counit (adjunction__of__initial_morphism HM')).
        Notation ε'' := (counit (adjunction__of__initial_morphism HM'')).
        Notation λ := T.
        Notation λ' := T'.
        Notation η := (unit (adjunction__of__initial_morphism HM)).
        Notation η' := (unit (adjunction__of__initial_morphism HM')).
        Notation η'' := (unit (adjunction__of__initial_morphism HM'')).
        Notation f := (functor__of__initial_morphism HM).
        Notation f' := (functor__of__initial_morphism HM').
        Notation f'' := (functor__of__initial_morphism HM'').
        Require Import categories.Utf8.
        Local Open Scope morphism_scope.

then it becomes

1 subgoals, subgoal 1 (ID 90)

  H : Funext
  C : PreCategory
  D : PreCategory
  G : Functor D C
  G' : Functor D C
  G'' : Functor D C
  T : NaturalTransformation G G'
  T' : NaturalTransformation G' G''
  M : ∀ x : C, (x ↓ G)%category
  HM : ∀ Y : C, IsInitialMorphism (M Y)
  M' : ∀ x : C, (x ↓ G')%category
  HM' : ∀ Y : C, IsInitialMorphism (M' Y)
  M'' : ∀ x : C, (x ↓ G'')%category
  HM'' : ∀ Y : C, IsInitialMorphism (M'' Y)
  x : C
  ============================
   ε'' (f x) ∘ f'' ₁ (λ' (f x) ∘ λ (f x) ∘ η x) =
   ε' (f x) ∘ f' ₁ (λ (f x) ∘ η x) ∘ (ε'' (f' x) ∘ f'' ₁ (λ' (f' x) ∘ η' x))

[mikeshulman]

So the functors labeled x, x', y, and y' in your pasting diagram are identities in your Coq code, with a=a'=a''=C and b=b'=b''=D and u=G, u'=G', u''=G''?

[mikeshulman]

Oh, no, wait, u=G'', u'=G', and u''=G?

[mikeshulman]

I think it's backwards because in your Coq code, you're starting out with natural transformations T, T' between the right adjoints, whereas in your pasting diagram you've drawn λ and λ' as going between the left adjoints.

[JasonGross]

Er, I'm not quite sure if I named f right. Either G is u (or appropriately primed version of it), or u is what I have down as f, and G is really f (or some primed version of it).

[JasonGross]

Ah. That would make sense. Thanks! I'll try drawing the other pasting diagram when I get a chance, and see if I can figure out what to do from that.

[JasonGross]

Updated hand-drawn diagram:

Here's is the collapsed diagram (with 1s filled in):

But Coq says, after notation adjustment*

1 subgoals, subgoal 1 (ID 97)

  H : Funext
  a : PreCategory
  b : PreCategory
  u : Functor b a
  u' : Functor b a
  u'' : Functor b a
  μ : NaturalTransformation u u'
  μ' : NaturalTransformation u' u''
  M : ∀ x : a, (x ↓ u)%category
  HM : ∀ Y : a, IsInitialMorphism (M Y)
  M' : ∀ x : a, (x ↓ u')%category
  HM' : ∀ Y : a, IsInitialMorphism (M' Y)
  M'' : ∀ x : a, (x ↓ u'')%category
  HM'' : ∀ Y : a, IsInitialMorphism (M'' Y)
  x : a
  ============================
   ε'' (f x) ∘ f'' ₁ (μ' (f x) ∘ μ (f x) ∘ η x) =
   ε' (f x) ∘ f' ₁ (μ (f x) ∘ η x) ∘ (ε'' (f' x) ∘ f'' ₁ (μ' (f' x) ∘ η' x))

(I think I got the names right this time.) This still seems backwards. But I suppose this makes sense, because although the diagrams that I drew can be pasted, the 2-cells inside of them only paste when you have identities, and then paste weirdly. (This explains why I couldn't phrase the general case.) So my second (bottom) diagram is actually more like this:

And I don't know what to do with this diagram, or if I've pasted wrongly, to reduce it to the first diagram (with μ′ ∘ μ). Any suggestions/corrections?

*Notation adjustment:

        Notation ε := (counit (adjunction__of__initial_morphism HM)).
        Notation ε' := (counit (adjunction__of__initial_morphism HM')).
        Notation ε'' := (counit (adjunction__of__initial_morphism HM'')).
        Notation η := (unit (adjunction__of__initial_morphism HM)).
        Notation η' := (unit (adjunction__of__initial_morphism HM')).
        Notation η'' := (unit (adjunction__of__initial_morphism HM'')).
        Notation f := (functor__of__initial_morphism HM).
        Notation f' := (functor__of__initial_morphism HM').
        Notation f'' := (functor__of__initial_morphism HM'').
        rename T into μ.
        rename T' into μ'.
        rename G into u.
        rename G' into u'.
        rename G'' into u''.
        rename D into b.
        rename C into a.
        Require Import categories.Utf8.
        Local Open Scope morphism_scope.

[mikeshulman]

Yes, that looks right. I think what you need to do is apply naturality to move all the other things out of the way so you can cancel the ε' and η' in the middle.

[JasonGross]

Which natrual transformation am I first applying naturality of? (Or I need to figure out what using naturality looks like, as opposed to just what commutes states...)

[mikeshulman]

Well, probably the latter will serve you better in the future, (-: but to get you started, I think the first thing you need to do is reassociate and distribute functor application to get

f' ₁ (η x) ∘ ε'' (f' x)

in the middle, and then apply naturality of ε'' to turn that into

ε'' (f' (u (f x))) ∘ f'' ₁ (u'' ₁ (f' ₁ (η x)))

[JasonGross]

Thanks! I've tacticified the proof (essentially, Coq just tries all of the associations and distributions of functor application): #630.

Any ideas about how to state the dependent version (where we have a, a', a'', not just a, and x and x' aren't both 1)?

[mikeshulman]

What's wrong with the sketch in your "Updated hand-drawn diagram" post above?

[JasonGross]

The natural transformations don't all compose. (Picture coming soonish, if that's not enough info.)

[mikeshulman]

If it's easier than drawing a picture, you could say specifically where they fail.

[JasonGross]

Oh, I see. I need to extend the top and bottom boxes with extra identities/whiskering so that it's a full 2x5 instead of the weird shape it is now.