leancata-1.lean

leancata-1.lean

import Lean
import Lean.Elab.Term
import Mathlib.Data.Finset.Basic
import Mathlib.Logic.ExistsUnique

-- class SmallCategory (ob : Type u) : Type (max u (v+1)) where
class SmallCategory (ob : Type) : Type 1 where
  hom : ob → ob → Type
  id : ∀ x, hom x x
  comp : ∀ {X Y Z}, hom X Y → hom Y Z → hom X Z
  id_comp : ∀ {X Y} (f : hom X Y), comp (id X) f = f
  comp_id : ∀ {X Y} (f : hom X Y), comp f (id Y) = f
  assoc : ∀ {W X Y Z} (f : hom W X) (g : hom X Y) (h : hom Y Z),
    comp (comp f g) h = comp f (comp g h)

infixl:65 " ⟶ " => SmallCategory.hom
notation:65 a:64 " ∘ " b:65 => SmallCategory.comp b a


--------------------------------------------------------------------------------
-- directly showing that Z_2 is a category

inductive AddZ_2 : Type 0
  | add_0
  | add_1

instance CatZ_2 : SmallCategory Star where
  hom _ _ := AddZ_2
  id _ := .add_0
  comp f g :=
    match (f, g) with
    | (.add_0, .add_0) => .add_0
    | (.add_1, .add_0) => .add_1
    | (.add_0, .add_1) => .add_1
    | (.add_1, .add_1) => .add_0
  id_comp := by
     intro X Y f
     cases f <;> rfl

  comp_id := by grind
  assoc := by grind

--------------------------------------------------------------------------------
-- poset category

class Poset (α : Type) where
  le : α → α → Prop
  -- define infix notation with precedence 65
  -- type preceq to get this
  reflex: ∀ x, le x x
  transitive: ∀ x y z, le x y → le y z → le x z
  antisymmetric: ∀ x y, le x y → le y x → x = y

-- define infix notation with precedence 65
infixl:65 " ≤ " => Poset.le

instance PosetCategory P [Poset P] : SmallCategory P where
  hom a b := PLift (a ≤ b)
  id a := PLift.up (Poset.reflex a)
  comp { a b c } f g := ⟨ Poset.transitive a b c f.down g.down ⟩
  id_comp := by grind
  comp_id := by grind
  assoc := by grind

--------------------------------------------------------------------------------
-- endomaps on finite sets

structure Endoset α where
  s : Finset α
  map : s → s

instance EndoCat : SmallCategory (Endoset α) where
  hom a b := { f : a.s -> b.s // f ∘ a.map = b.map ∘ f }
  id a := ⟨ fun x => x, by rfl ⟩
  comp f g :=
    ⟨ g.val ∘ f.val, by
      cases f
      rename_i fv propf
      cases g
      rename_i gv propg
      simp
      -- here I initially wanted to appeal to the associativity of homs.
      -- obviously, this isn't valid, because that would be circular. it's
      -- interesting how, when we are defining the category, we *do* need to
      -- use specific properties of objects (i.e., "look at the objects").
      -- here, we use associativity of functions, from which associativity of homs
      -- is derived
      conv =>
        lhs
        rw [Function.comp_assoc]
        rw [propf]
        rw [<- Function.comp_assoc]
        rw [propg]
      rfl⟩

  -- aesop can handle these which is *awesome*
  id_comp := by aesop
  comp_id := by aesop
  assoc := by aesop