commutative squares of isomorphisms

Stream: maths

[Chris Henson]

I'm a bit confused by the statement of this lemma from Category Theory in Context:

image.png

and how to quantify a unique $f'$ in Lean. Does "The left-hand diagram defines $f'$" mean we should assume that we have a morphism that makes the left square commute, e.g.

import Mathlib

open CategoryTheory

universe u v

variable {C : Type u} [Category.{v} C] {a b a' b': C}

lemma four_iso (ha : a ≅ a') (hb : b ≅ b') (f : a ⟶  b) (f' : a' ⟶  b') (comm : f' = ha.inv ≫ f ≫ hb.hom)
  : ha.hom ≫ f' = f ≫ hb.hom ∧ ha.inv ≫ f = f' ≫ hb.inv ∧ f = ha.hom ≫ f' ≫ hb.inv
  := sorry

I also always find it awkward to state uniqueness for lemmas like these, what would be the best way to do so here? Bundle this into a structure and prove equal projections of $f'$?

[Aaron Liu]

We have docs#ExistsUnique, but no one uses it

[Aaron Liu]

I would interpret this as needing to prove both existence and uniqueness.

[Aaron Liu]

And the equivalence between any one diagram commuting and all the diagrams commuting

[Kevin Buzzard]

I think that this is mathematically equivalent to the question (uniqueness for one diagram is equivalent to uniqueness for all of them, given that they're equivalent):

import Mathlib

open CategoryTheory

universe u v

variable {C : Type u} [Category.{v} C] {a b a' b': C}

-- uniqueness
lemma four_iso (ha : a ≅ a') (hb : b ≅ b') (f : a ⟶  b) : ∃! (f' : a' ⟶  b'), f' = ha.inv ≫ f ≫ hb.hom := by
  aesop

lemma four_iso' (ha : a ≅ a') (hb : b ≅ b') (f : a ⟶  b) (f' : a' ⟶  b') :
    List.TFAE [f' = ha.inv ≫ f ≫ hb.hom, ha.hom ≫ f' = f ≫ hb.hom, ha.inv ≫ f = f' ≫ hb.inv, f = ha.hom ≫ f' ≫ hb.inv] := by
  sorry

[Chris Henson]

Thanks! That makes sense, though the steps aesop takes are a bit unintuitive to me.

[Kevin Buzzard]

It's obvious that given a y there's a unique x such that x=y. That's why I chose that one for the uniqueness.

[Chris Henson]

Yes, it is obvious once I see docs#forall_eq, docs#exists_eq_left, etc. being called by simp, it just surprised me a bit.

[Ben Eltschig]

Aaron Liu said:

We have docs#ExistsUnique, but no one uses it

It's used in docs#CategoryTheory.Presieve.IsSheafFor, for example. I don't know any other places where it is used though.