Defining simple categories

Stream: new members

[Vlad Tsyrklevich]

I'm reading Category Theory in Context and I decided to solve a simple exercise using Lean/mathlib just to explore how category theory is implemented in mathlib. The exercise itself was fairly simple, but I spent quite a lot of time defining two categories and a functor between them. In my case, I define one (thin) category with 4 objects and 3 (non-identity) morphisms and then another category with 3 objects and 3 morphisms. I imagine there is probably an easier way to define categories than what I did and I am just not aware of the right tools to do so? Pointers appreciated.

-- Exercise 1.6.iv. Find an example to show that a faithful functor need not preserve epimorphisms.
-- Argue by duality, or by another counterexample, that a faithful functor need not preserve monomorphisms.

/--
  Define a category with the following morphisms:
    a → b → c
        |
        \ → d
-/
inductive t₁ | a | b | c | d
instance Cat_t₁ : SmallCategory t₁ where
  Hom X Y := PLift (X = t₁.a ∨ (X = t₁.b ∧ Y = t₁.c) ∨ (X = t₁.b ∧ Y = t₁.d) ∨ (X = Y))
  id X := by
    simp
    exact { down := trivial }
  comp X Y := by
    refine PLift.pure ?_
    rcases PLift.down X with _ | _ | _ | _ <;> rcases PLift.down Y with _ | _ | _ | _ <;> simp_all

/--
  Define a category with the following morphisms:
    A → B ⇉ C (but there is only one morphism A → C)
-/
inductive t₂ | A | B | C
instance Cat_t₂ : SmallCategory t₂ where
  Hom
  | t₂.A, t₂.A => PUnit
  | t₂.B, t₂.B => PUnit
  | t₂.C, t₂.C => PUnit
  | t₂.A, t₂.B => PUnit
  | t₂.A, t₂.C => PUnit
  | t₂.B, t₂.C => Sum PUnit PUnit     -- inl ⋆ and inr ⋆ are different arrows
  | _, _ => PEmpty
  id X := by
    rcases X <;> simp <;> exact PUnit.unit
  comp {x y z} X Y := by
    rcases x <;> rcases y <;> rcases z <;> simp
    -- kinda ugly but correct
    all_goals first | exact PUnit.unit | exact X | exact Y | exact Sum.inl PUnit.unit
  -- Manually prove these because aesop times out.
  id_comp {X Y} (f) := by rcases X <;> rcases Y <;> simp
  comp_id {X Y} (f) := by rcases X <;> rcases Y <;> simp
  assoc {W X Y Z} (f g h) := by
    simp
    rcases W <;> rcases X <;> rcases Y <;> rcases Z
    all_goals (simp at f g h; aesop)

def t₁_t₂_functor : Functor t₁ t₂ := {
  obj X :=
    match X with
    | t₁.a => t₂.A
    | t₁.b => t₂.B
    | t₁.c => t₂.C
    | t₁.d => t₂.C
  map {x y} X := by
    match x, y with
    | t₁.a, t₁.a => exact PUnit.unit
    | t₁.b, t₁.b => exact PUnit.unit
    | t₁.c, t₁.c => exact PUnit.unit
    | t₁.d, t₁.d => exact PUnit.unit
    | t₁.a, t₁.b => exact PUnit.unit
    | t₁.b, t₁.c => exact Sum.inl PUnit.unit
    | t₁.a, t₁.c => exact PUnit.unit
    | t₁.b, t₁.d => exact Sum.inr PUnit.unit
    | t₁.a, t₁.d => exact PUnit.unit
    | t₁.d, t₁.c => have := PLift.down X; simp_all
    | t₁.d, t₁.b => have := PLift.down X; simp_all
    | t₁.d, t₁.a => have := PLift.down X; simp_all
    | t₁.c, t₁.d => have := PLift.down X; simp_all
    | t₁.c, t₁.b => have := PLift.down X; simp_all
    | t₁.c, t₁.a => have := PLift.down X; simp_all
    | t₁.b, t₁.a => have := PLift.down X; simp_all
  /-
    repeat' split
    all_goals try exact PUnit.unit
    all_goals try (have := PLift.down X; simp_all)
    · exact Sum.inl PUnit.unit
    · exact Sum.inr PUnit.unit
-/
  -- Manually prove because aesop times out.
  map_comp {x y z} X Y := by
    simp
    rcases x <;> rcases y <;> rcases z <;> simp <;> try rfl
    all_goals
    · have := PLift.down X;
      have := PLift.down Y;
      simp_all
}

theorem exercise_1_6_iv_part1 :
    ∃ α β : Type,
    ∃ _ : CategoryTheory.SmallCategory α,
    ∃ _ : CategoryTheory.SmallCategory β,
    ∃ F : CategoryTheory.Functor α β,
    ∃ X Y : α,
    ∃ f : X ⟶ Y,
    F.Faithful ∧ CategoryTheory.Epi f ∧ ¬CategoryTheory.Epi (F.map f) := by
  refine ⟨t₁, t₂, Cat_t₁, Cat_t₂, t₁_t₂_functor, t₁.a, t₁.b, PLift.up (Or.inl rfl), ?_⟩
  refine ⟨?_, ⟨?_, ?_⟩⟩
  · refine { map_injective := fun {X Y} ↦ ?_ }
    simp [t₁_t₂_functor]
    rcases X <;> rcases Y <;> simp [Function.Injective]
    all_goals exact fun ⦃a₁ a₂⦄ => eq_of_comp_right_eq fun {X} => congrFun rfl
  · exact { left_cancellation := fun {z} g h d ↦ eq_of_comp_right_eq fun {X} => congrFun rfl }
  · by_contra h'
    have := h'.left_cancellation (Z := t₂.C) (Sum.inl PUnit.unit : t₂.B ⟶ t₂.C) (Sum.inr PUnit.unit : t₂.B ⟶ t₂.C)
    simp [t₁_t₂_functor, Cat_t₂] at this

theorem exercise_1_6_iv_part2 :
    ∃ α β : Type,
    ∃ _ : CategoryTheory.SmallCategory αᵒᵖ,
    ∃ _ : CategoryTheory.SmallCategory βᵒᵖ,
    ∃ F : CategoryTheory.Functor αᵒᵖ βᵒᵖ,
    ∃ X Y : αᵒᵖ,
    ∃ f : X ⟶ Y,
    F.Faithful ∧ CategoryTheory.Mono f ∧ ¬CategoryTheory.Mono (F.map f) := by
  obtain ⟨s₁, s₂, cat₁, cat₂, functor, x, y, f, ⟨h₁, ⟨h₂, h₃⟩⟩⟩ := exercise_1_6_iv_part1
  refine ⟨s₁, s₂,  cat₁.opposite,  cat₂.opposite,  functor.op,  Opposite.op y, Opposite.op x, f.op, ?_⟩
  refine ⟨Functor.instFaithfulOppositeOp, ⟨op_mono_of_epi f, ?_⟩⟩
  · contrapose! h₃
    simp only [Functor.op_obj, Functor.op_map, Quiver.Hom.unop_op] at h₃
    have := unop_epi_of_mono (functor.map f).op
    simpa using this

[Junyan Xu]

I'm not sure if aesop works better this way, but the homs in such categories are usually defined like this:

open t₂ in
inductive t₂hom : t₂ → t₂ → Type
  | id (x : t₂) : t₂hom x x
  | AB : t₂hom A B
  | AC : t₂hom A C
  | BC₁ : t₂hom B C
  | BC₂ : t₂hom B C

see e.g. CategoryTheory.Limits.WalkingParallelPairHom

[Vlad Tsyrklevich]

Thanks for the pointer. I refactored using your definition, and it is a bit cleaner, thoughaesop still fails to fill in all of the same definitions.

/--
  Define a category with the following morphisms:
    A → B ⇉ C (but there is only one morphism A → C)
-/
inductive t₂ | A | B | C
open t₂ in
inductive t₂hom : t₂ → t₂ → Type
  | id (x : t₂) : t₂hom x x
  | AB : t₂hom A B
  | AC : t₂hom A C
  | BC₁ : t₂hom B C
  | BC₂ : t₂hom B C

instance Cat_t₂ : SmallCategory t₂ where
  Hom := t₂hom
  id X := t₂hom.id X
  comp {x y z} X Y := by
    match X, Y with
    | t₂hom.AB, t₂hom.BC₁ => exact t₂hom.AC
    | t₂hom.AB, t₂hom.BC₂ => exact t₂hom.AC
    | _, t₂hom.id _ => tauto
    | t₂hom.id _, _ => tauto
  -- Manually prove these because aesop times out.
  id_comp {X Y} (f) := by cases f <;> simp
  comp_id {X Y} (f) := by cases f <;> simp
  assoc {W X Y Z} (f g h) := by
    cases f <;> cases g <;> cases h <;> simp_all

def t₁_t₂_functor : Functor t₁ t₂ := {
  obj X :=
    match X with
    | t₁.a => t₂.A
    | t₁.b => t₂.B
    | t₁.c => t₂.C
    | t₁.d => t₂.C
  map {x y} X := by
    match x, y with
    | t₁.a, t₁.a => exact t₂hom.id t₂.A
    | t₁.b, t₁.b => exact t₂hom.id t₂.B
    | t₁.c, t₁.c => exact t₂hom.id t₂.C
    | t₁.d, t₁.d => exact t₂hom.id t₂.C
    | t₁.a, t₁.b => exact t₂hom.AB
    | t₁.b, t₁.c => exact t₂hom.BC₁
    | t₁.a, t₁.c => exact t₂hom.AC
    | t₁.b, t₁.d => exact t₂hom.BC₂
    | t₁.a, t₁.d => exact t₂hom.AC
    | t₁.d, t₁.c => have := PLift.down X; simp_all
    | t₁.d, t₁.b => have := PLift.down X; simp_all
    | t₁.d, t₁.a => have := PLift.down X; simp_all
    | t₁.c, t₁.d => have := PLift.down X; simp_all
    | t₁.c, t₁.b => have := PLift.down X; simp_all
    | t₁.c, t₁.a => have := PLift.down X; simp_all
    | t₁.b, t₁.a => have := PLift.down X; simp_all
  -- Manually prove because aesop times out.
  map_comp {x y z} X Y := by
    simp
    rcases x <;> rcases y <;> rcases z <;> simp <;> try rfl
    all_goals
    · have := PLift.down X;
      have := PLift.down Y;
      simp_all
}

I'm a little surprised there isn't a macro of some sort to specify simple categories/diagrams, though I'm a beginner and have no idea its usefulness.

[Kenny Lau]

Vlad Tsyrklevich said:

there isn't a macro of some sort to specify simple categories/diagrams

it's fin_cases after you provide the corresponding Fintype instances

[Vlad Tsyrklevich]

Not sure I follow, how would one define one of the categories I defined earlier using this?

[Kenny Lau]

Vlad Tsyrklevich said:

Not sure I follow, how would one define one of the categories I defined earlier using this?

you don't change the definitions, but you provide an instance of Fintype t₁

[Kenny Lau]

and also Fintype the homs