Proof of comma category characterization of an adjunction

[svenkeidel]

Hi John,

I proved the characterization of an adjunction as comma categories. Cheers.

comma-adjunction.pdf

Regards, Sven

[jwiegley]

Awesome. Can it still be proven when U(φ(A,B,f)) ≅ U(A,B,f) ≅ (A,B), and φ(α,β) ≈ (α,β)?

This problem arises for me because my adjoint functors are functors between quotient categories; I suppose I could try weakening the statement to address only categories, and then I could work with equalities on the objects and morphisms. I think I'll try that next, which should follow directly from your proof, and then see if it can be further generalized. Thanks, Sven!

[jwiegley]

Oh, and I can get a copy of your LaTeX? Your proof is beautiful, and maybe I can use it as a template. :)

[svenkeidel]

https://github.com/svenkeidel/comma-adjunction

[jwiegley]

Thanks!

[svenkeidel]

I renamed the arrow names and category names in the proof.

[svenkeidel]

comma-adjunction.pdf

[svenkeidel]

I added the details about the isomorphism to the proof (comma-adjunction.pdf). Furthermore, I cleaned up the proof by removing the details of the forgetful functor U.

[jwiegley]

@svenkeidel Thanks! What's making this tricky is my inability to apply the π₁ equality. Here's the goal:

  ((a, b); φ' (ψ' x)) ≅ ((a, b); x)
  ============================
  φ' (ψ' x) ≈ x

It seems like this should be obvious, but actually what that context gives me is:

φ' (ψ' x)
       ≈ fmap[G] (snd `1 (from (lawvere_to_from_iso x))) ∘ x
         ∘ fst `1 (to (lawvere_to_from_iso x))

And so far, I haven't been able to show that due to the nature of the isomorphism, these conversions should both be equivalent to id.

[jwiegley]

I feel like I'm just missing a naturality witness here, since φ' on its own is not aware that the morphism is coming from a comma category.

[jwiegley]

@svenkeidel Here are the final two lemmas. Going to give it a rest again, to see if sleep brings more clarity:

Lemma equiv_comma_projF_iso : ∀ {a b} {f : F a ~> b}
  (iso : ((a, b); lawvere_from (lawvere_to f)) ≅[F ↓ Id[C]] ((a, b); f)),
    `1 (to iso) ≈ @id (D ∏ C) _ ∧ `1 (from iso) ≈ @id (D ∏ C) _.
Admitted.

Lemma equiv_comma_projG_iso : ∀ {a b} {g : a ~> G b}
  (iso : ((a, b); lawvere_to (lawvere_from g)) ≅[Id[D] ↓ G] ((a, b); g)),
    `1 (to iso) ≈ @id (D ∏ C) _ ∧ `1 (from iso) ≈ @id (D ∏ C) _.
Admitted.