Category Theory

Stream: general

[Success Moses]

image.png

I am trying to formalise the lemma above in lean, but there is a sorry and I think I misformalised:

open CategoryTheory Category Opposite Function

abbrev fstar {C : Type} [Category C] {x y : C} (f : x ⟶ y) (c : C) : (c ⟶ x) → (c ⟶ y) :=
  fun g => g ≫ f

-- TODO: use bijection instead
def HasInverse {α β : Type} (f : α → β) := HasLeftInverse f ∧ HasRightInverse f

variable {C : Type} [Category C] {x y : C} (f : x ⟶ y)

theorem t1 : IsIso f ↔ ∀ c : C, HasInverse (fstar f _ : (c ⟶ x) → (c ⟶ y)) := by
  constructor
  · intro ⟨g, h₁, h₂⟩ c; refine ⟨?_, ?_⟩
    · use (fun g' => g' ≫ g)
      intro f'; dsimp
      unfold fstar
      rw [assoc, h₁, Category.comp_id]
    · use (fun g' => g' ≫ g)
      intro f'; dsimp
      unfold fstar
      rw [assoc, h₂, Category.comp_id]
  · intro h
    obtain h₁ := HasRightInverse.surjective (h y).right
    obtain h₂ := HasLeftInverse.injective (h x).left
    obtain ⟨g, cat⟩ := h₁ (𝟙 _)
    refine ⟨⟨g, h₂ ?_, cat⟩⟩
    unfold fstar at *
    rw [assoc, cat, Category.comp_id, Category.id_comp]

section

abbrev fstar' {C : Type} [Category C] {x y : C} (f : x ⟶ y) (c : C) : (y ⟶ c) → (x ⟶ c) :=
  fun g => f ≫ g

variable {C : Type} [Category C] {x y : C} (f : x ⟶ y)

example : IsIso f ↔ ∀ c : C, HasInverse (fstar' f c) := by
  have h := t1 f.op
  sorry

[Success Moses]

t1 f.op is supposed to close the second goal. I tried simpa using (t1 f.op) but it did not work. Maybe I need a show that fstar f.op = fstar' f, but it is not true because they are not the same type. Maybe I misformalised.

[Success Moses]

This lemma is Lemma 1.2.3 from "Category Theory in Context" by Emily Riehl.

[Robin Arnez]

You are searching for docs#CategoryTheory.isIso_iff_yoneda_map_bijective and docs#CategoryTheory.isIso_iff_coyoneda_map_bijective​?