small category structure

Stream: new members

[cosindine]

y'all got a better definition for a small category than this?

i have this one stolen from https://www.youtube.com/watch?v=WRjlRq64vws

but i'm not entirely sure how to define sub categories on it

structure Cat where
    Obj: Type u
    Mor: Obj → Obj → Type v
    id: (x: Obj) → Mor x x

    comp: {x y z: Obj} → Mor x y → Mor y z → Mor x z
    id_comp: (x: Obj) → {y: Obj} → (m: Mor x y) → comp (id x) m = m
    comp_id: (x: Obj) → {y: Obj} → (m: Mor y x) → comp m (id x) = m
    assoc: {w x y z: Obj} → (a: Mor w x) → (b: Mor x y) → (c: Mor y z) → comp (comp a b) c = comp a (comp b c)

--my best guess :/
structure SubCat (c: Cat) where
    sc: Cat
    sub_obj: sc.Obj → c.Obj
    sub_mor: sc.Mor x y → c.Mor (sub_obj x) (sub_obj y)
    sub_comp: (a: sc.Mor x y) → (b: sc.Mor y z) → sub_mor (sc.comp a b) = c.comp (sub_mor a) (sub_mor b)

[Kevin Buzzard]

A better definition of a small category would be mathlib's current definition https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Category/Basic.html#CategoryTheory.SmallCategory , which is better because it doesn't involve reinventing the wheel

[cosindine]

Why wouldn't I want to reinvent the wheel while learning a topic?

[Edward van de Meent]

because it means you won't run into the same non-topic-related issues, allowing you to focus on the topic

[cosindine]

As far as I can tell mathlib doesn't even define sub categories...

Also who says I'm reinventing the wheel? The Cat structure is pretty much exactly mathlib's Category just all in one place instead of spread across 3 different files.

[Edward van de Meent]

you're reinventing the wheel because you're creating a new thing instead of using the definition that's in mathlib directly

[Edward van de Meent]

also, i suspect that if you want a subcategory of a category C, the right notion would probably just be CategoryTheory.Subobject C?

[Kevin Buzzard]

If this is a learning exercise then that's definitely a good reason to develop everything yourself! Note though that developing category theory from first principles in Lean's type theory is a hard problem and we already have a solution which looks like it's working.

[cosindine]

so I'm reading Category Theory in Context by Emily Riehl

and i'm trying to do

Exercise 1.1.ii. Let C be a category. Show that the collection of isomorphisms in C defines a subcategory, the maximal groupoid inside C.

I currently have

structure Cat where
    Obj: Type u
    Mor: Obj → Obj → Sort v
    id: (x: Obj) → Mor x x

    comp: {x y z: Obj} → Mor x y → Mor y z → Mor x z
    id_comp: (x: Obj) → {y: Obj} → (m: Mor x y) → comp (id x) m = m
    comp_id: (x: Obj) → {y: Obj} → (m: Mor y x) → comp m (id x) = m
    assoc: {w x y z: Obj} → (a: Mor w x) → (b: Mor x y) → (c: Mor y z) → comp (comp a b) c = comp a (comp b c)

def Mor.dom {c: Cat} {x y: c.Obj} (_: c.Mor x y) := x
def Mor.cod {c: Cat} {x y: c.Obj} (_: c.Mor x y) := y
def Mor.cat {c: Cat} {x y: c.Obj} (_: c.Mor x y) := c

structure Isomorphism {c: Cat} {dom cod: c.Obj} (f: c.Mor dom cod) (g: c.Mor cod dom) : Prop where
    invl: c.comp g f = c.id cod
    invr: c.comp f g = c.id dom

theorem Isomorphism.symm (p: Isomorphism a b) : Isomorphism b a := { invl := p.invr, invr := p.invl }
theorem Isomorphism.trans {c: Cat} {x y z : c.Obj} {f : c.Mor x y} {g : c.Mor y x} {u : c.Mor y z} {v : c.Mor z y}
    (p1: Isomorphism f g) (p2: Isomorphism u v) : Isomorphism (c.comp f u) (c.comp v g) := by
    cases p1
    cases p2
    have h1 : c.comp (c.comp f u) (c.comp v g) = c.id x := by
        have h1 := c.assoc (c.comp f u) v g
        have h2 := c.assoc f u v
        simp_all [c.id_comp, c.comp_id]
    have h2 : c.comp (c.comp v g) (c.comp f u) = c.id z := by
        have h1 := c.assoc (c.comp v g) f u
        have h2 := c.assoc v g f
        simp_all [c.id_comp, c.comp_id]
    exact { invl := h2, invr := h1 }

structure Automorphism {c: Cat} {dom: c.Obj} (f: c.Mor dom dom) (g: c.Mor dom dom): Prop where
    invl: c.comp g f = c.id dom
    invr: c.comp f g = c.id dom

theorem iso_same (iso: Isomorphism (c := c) a a) : Automorphism a a := { invl := iso.invl, invr := iso.invr }

structure Groupoid (c: Cat) where
    inv: (c.Mor x y) → c.Mor y x
    iso: (m: c.Mor x y) → Isomorphism m (inv m)

theorem E1_1_i_i {c: Cat} {x y: c.Obj} (f: c.Mor x y) (g h: c.Mor y x)
    (p1: c.comp g f = c.id y)
    (p2: c.comp f h = c.id x) : g = h := by
    have h1 := c.assoc g f h
    simp_all [c.id_comp, c.comp_id]

theorem E1_1_i_ii {c: Cat} {x y: c.Obj} {f: c.Mor x y} {g h: c.Mor y x}
    (p1: Isomorphism f g)
    (p2: Isomorphism f h) : g = h := by
    cases p1
    cases p2
    have h1 := c.assoc g f h
    simp_all [c.id_comp, c.comp_id]

but I don't know how to define sub categories