finite categories

Stream: Is there code for X?

[Reid Barton]

I'm interested in a particular finite category (it has 6 objects and a total of 17 morphisms) and verifying a fact about it, preferably by brute force. Is there a convenient way to write it down in such a way that I get fintype instances for all the Hom-types?

[Adam Topaz]

docs#category_theory.fin_category is the first thing that I can think of

[Adam Topaz]

Well, you would have to provide the fintype instances yourself. I don't know if derive would work in your case.

[Reid Barton]

Right so my first, and perhaps only, question is in something like

import data.fintype.basic
import tactic.derive_fintype

inductive Ob
| A | B | C | D | E | F
open Ob

@[derive fintype]   -- @[derive fintype]: inductive indices are not supported
inductive Hom : Ob → Ob → Type
| f : Hom A B
-- more constructors

is there a way to avoid manually writing an instance for Π (x y : Ob), fintype (Hom x y)?

[Mario Carneiro]

Do you want it to compute?

[Mario Carneiro]

You could have a collection of inductives and use a def to choose between them

[Reid Barton]

Well, what I want in the end is some way to automatically check associativity (and another similar condition which is relevant to my problem)

[Reid Barton]

I guess I don't really care whether it is dec_trivial or a tactic that generates a proof with 100 cases

[Mario Carneiro]

I think that will be okay, although 6^3 is... :grimacing:

[Mario Carneiro]

I feel like this needs some kind of custom automation

[David Wärn]

Is it important that you get Π (x y : Ob), fintype (Hom x y) as opposed to only fintype (Hom A A), fintype (Hom A B) etc ? If not you could define Hom by pattern matching.

[Kyle Miller]

Maybe you could use subtypes to get the fintype instances? I got this to work for a 2-object 4-morphism category.

import category_theory.fin_category
import tactic

open category_theory

@[derive [fintype, decidable_eq]]
inductive objs | a | b

@[derive [fintype, decidable_eq]]
inductive mors | a1 | f | g | b1

def s : mors → objs
| mors.a1 := objs.a
| mors.f := objs.a
| mors.g := objs.a
| mors.b1 := objs.b

def t : mors → objs
| mors.a1 := objs.a
| mors.f := objs.a
| mors.g := objs.b
| mors.b1 := objs.b

abbreviation mors' (x y : objs) : Type := {m : mors // s m = x ∧ t m = y}

example (x y : objs) : fintype (mors' x y) := infer_instance

instance : quiver objs := ⟨mors'⟩

def ids : Π (x : objs), mors' x x
| objs.a  := ⟨mors.a1, by tidy⟩
| objs.b := ⟨mors.b1, by tidy⟩

def comp : mors → mors → option mors
| mors.a1 ψ := if s ψ = objs.a then some ψ else none
| ϕ mors.a1 := if t ϕ = objs.a then some ϕ else none
| mors.b1 ψ := if s ψ = objs.b then some ψ else none
| ϕ mors.b1 := if t ϕ = objs.b then some ϕ else none
| mors.f mors.f := some mors.a1
| mors.f mors.g := some mors.g
| _ _ := none

-- after this point, everything is generic and should work even after changing the above data

def comp' {x y z : objs} : mors' x y → mors' y z → mors' x z :=
begin
  rintro ϕ ψ,
  generalize hc : comp ϕ ψ = ρ,
  cases ρ,
  obtain ⟨ϕ, rfl, rfl⟩ := ϕ,
  obtain ⟨ψ, h, rfl⟩ := ψ,
  exfalso; cases ϕ; cases ψ; simp! at hc h; assumption,
  use ρ,
  obtain ⟨ϕ, rfl, rfl⟩ := ϕ,
  obtain ⟨ψ, h, rfl⟩ := ψ,
  cases ϕ; cases ψ; simp! at h hc; try { exfalso, assumption }; subst_vars; simp!,
end

instance : category objs :=
{ id := λ x, ids x,
  comp := λ x y z ϕ ψ, comp' ϕ ψ,
  id_comp' := λ x y ϕ, begin
    obtain ⟨ϕ, rfl, rfl⟩ := ϕ,
    cases ϕ; refl,
  end,
  comp_id' := λ x y ϕ, begin
    obtain ⟨ϕ, rfl, rfl⟩ := ϕ,
    cases ϕ; refl,
  end,
  assoc' := λ x y z w ϕ ψ ρ, begin
    obtain ⟨ϕ, rfl, rfl⟩ := ϕ,
    obtain ⟨ψ, h, rfl⟩ := ψ,
    obtain ⟨ρ, h', rfl⟩ := ρ,
    cases ϕ; cases ψ; simp! at h; try { exfalso, exact h }; cases ρ; simp! at h'; try { exfalso, exact h' }; refl,
  end }

[Kyle Miller]

But if it would work to case bash for your other condition (rather than needing fintype instances), this works fine for proving it's a category (after needing to alter how composition works to appease the equation compiler) and is significantly faster:

import category_theory.fin_category
import tactic

open category_theory

@[derive [fintype, decidable_eq]]
inductive objs | a | b

@[derive [decidable_eq]]
inductive mors : objs → objs → Type
| a1 : mors objs.a objs.a
| f : mors objs.a objs.a
| g : mors objs.a objs.b
| b1 : mors objs.b objs.b

instance : quiver objs := ⟨mors⟩

def ids : Π (x : objs), mors x x
| objs.a  := mors.a1
| objs.b := mors.b1

def comp : Π {x y z}, mors x y → mors y z → mors x z
| _ _ _ mors.a1 ψ := ψ
| _ _ _ mors.f mors.a1 := mors.f
| _ _ _ mors.b1 ψ := ψ
| _ _ _ mors.g mors.b1 := mors.g
| _ _ _ mors.f mors.f := mors.a1
| _ _ _ mors.f mors.g := mors.g

instance : category objs :=
{ id := λ x, ids x,
  comp := λ x y z ϕ ψ, comp ϕ ψ,
  id_comp' := λ x y ϕ, begin
    cases ϕ; refl,
  end,
  comp_id' := λ x y ϕ, begin
    cases ϕ; refl,
  end,
  assoc' := λ x y z w ϕ ψ ρ, begin
    cases ϕ; cases ψ; cases ρ; refl,
  end }

[Kyle Miller]

I guess creating fintype instances for this in a somewhat generic way isn't too bad, if you need them:

instance (x y : objs) : fintype (mors x y) :=
begin
  let s : finset (mors x y) := ∅,
  cases x; cases y;
  { try { let s := insert mors.a1 s, },
    try { let s := insert mors.f s, },
    try { let s := insert mors.g s, },
    try { let s := insert mors.b1 s, },
    use s,
    intro ϕ,
    cases ϕ;
    simp [finset.not_mem_empty, false_or, or_false, finset.mem_insert], },
end

[Reid Barton]

FWIW while thinking about how to check the other properties of the category I care about, I realized that by adjusting the category slightly I can make them easy to check by hand... so I no longer really need this.