Imports
/-
Copyright (c) 2026 Terence Rokop. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Terence Rokop
-/
module
public import Geb.Mathlib.Data.UnionFind.OfEdges
public import Geb.Mathlib.CategoryTheory.FinSetSkel.Basic
public import Geb.Mathlib.Data.List.NodupEquivFin
public import Geb.Mathlib.Data.Vector.OfFn
The coequalizer of a parallel pair in FinSetSkel
The coequalizer of f g : X ⟶ Y in the category of finite sets is
the quotient of Y by the equivalence relation generated by
f i ∼ g i. Here that quotient is computed: the pairs
(f.toVec.get i, g.toVec.get i) are folded through
Batteries.UnionFind.Sized.ofEdges, the resulting roots are
renumbered onto an initial segment by Fin.compressEquiv, and the
carrier's length is the number of roots.
Everything is stated over the application-normal form
f.toVec.get i rather than over bare index functions, so the wrapper
that packages this as a ColimitCocone is a transcription rather than
a translation. The module is Classical.choice-free; the wrapper is
not, and is separate for that reason.
The fold runs once per coequalizer. Nothing expensive sits above a
lambda anywhere in this module: the union-find is a parameter that no
definition below rebuilds, and the per-class renumbering data is a
Vector rather than a function.
Main definitions
FinSetSkel.Quotient.edges, FinSetSkel.Quotient.unionFind — the
pairs a parallel pair generates, and the fold over them.
FinSetSkel.Quotient.obj, FinSetSkel.Quotient.rep,
FinSetSkel.Quotient.π, FinSetSkel.Quotient.desc — the carrier,
its chosen representatives, the projection, and the factorisation.
Main statements
FinSetSkel.Quotient.comp_π — the projection coequalizes the pair.
FinSetSkel.Quotient.π_desc,
FinSetSkel.Quotient.desc_uniq — the universal property.
Implementation notes
Fin (obj Y v).len, Fin (len v) and
Fin ((List.finRange Y.len).filter (isRoot v)).length are three
forms of the carrier's index type. Every statement uses the first,
which the morphism types force, and each of π, rep and desc
therefore carries an unfolding lemma stated by hand rather than
inherited from Vector.get_ofFnC.
rep_π and π_rep both carry @[simp]: each is a round trip whose
right-hand side is strictly smaller than its left-hand side, which is
the criterion for marking an equation in the stated orientation.
References
[nLabCoequalizer] — the coequalizer, and the quotient-set
construction of it in Set.
Tags
category, finite set, coequalizer, quotient, union-find, choice-free
@[expose] public sectionuniverse uopen CategoryTheory Batteriesnamespace FinSetSkel.Quotientsectionvariable {X Y : FinSetSkel.{u}}The pairs a parallel pair generates: one per domain index.
def edges (f g : X ⟶ Y) : List (Fin Y.len × Fin Y.len) :=
(List.finRange X.len).map fun i ↦ (f.toVec.get i, g.toVec.get i)The union-find merging exactly the pairs a parallel pair generates. This is where the fold runs, once per coequalizer.
def unionFind (f g : X ⟶ Y) : UnionFind.Sized Y.len :=
UnionFind.Sized.ofEdges _ (edges f g)
Whether an index is its own root. The decidability instance is
named rather than left to search: two routes inhabit
DecidableEq (Fin n), and which of them is choice-free depends on
the import set, so a bump could otherwise change this term's axioms
silently.
def isRoot (v : UnionFind.Sized n) : Fin n → Bool :=
fun j ↦ @decide (v.root j = j) (instDecidableEqFin _ _ _)The number of classes: the number of indices that are their own root.
def len (v : UnionFind.Sized n) : ℕ :=
((List.finRange n).filter (isRoot v)).lengthA root is its own root.
theorem isRoot_root (v : UnionFind.Sized n) (j : Fin n) :
isRoot v (v.root j) := n:ℕv:UnionFind.Sized nj:Fin n⊢ isRoot v (v.root j) = true
All goals completed! 🐙The coequalizer's carrier: one index per class.
def obj (Y : FinSetSkel.{u}) (v : UnionFind.Sized Y.len) :
FinSetSkel.{u} := ⟨len v⟩
A chosen representative of each class, as a vector so that its
consumers index it rather than rebuilding Fin.compressEquiv per
class.
def rep (Y : FinSetSkel.{u}) (v : UnionFind.Sized Y.len) :
Vector (Fin Y.len) (obj Y v).len :=
let e := Fin.compressEquiv (isRoot v)
Vector.ofFnC fun c ↦ (e c).1The projection onto the carrier: an index goes to the compressed index of its root.
def π (Y : FinSetSkel.{u}) (v : UnionFind.Sized Y.len) : Y ⟶ obj Y v :=
let e := Fin.compressEquiv (isRoot v)
Hom.ofVec (Vector.ofFnC fun j ↦ e.symm ⟨v.root j, isRoot_root v j⟩)
The factorisation of a morphism through the carrier. It carries no
compatibility hypothesis, so it computes for any h; only π_desc
constrains h.
def desc (Y : FinSetSkel.{u}) (v : UnionFind.Sized Y.len)
(h : Y ⟶ Z) : obj Y v ⟶ Z :=
let r := rep Y v
Hom.ofVec (Vector.ofFnC fun c ↦ h.toVec.get (r.get c))The projection at an index.
theorem π_get (Y : FinSetSkel.{u}) (v : UnionFind.Sized Y.len)
(j : Fin Y.len) :
(π Y v).toVec.get j
= (Fin.compressEquiv (isRoot v)).symm ⟨v.root j, isRoot_root v j⟩ := Y:FinSetSkelv:UnionFind.Sized Y.lenj:Fin Y.len⊢ (Hom.toVec (π Y v)).get j = (Fin.compressEquiv (isRoot v)).symm ⟨v.root j, ⋯⟩
Y:FinSetSkelv:UnionFind.Sized Y.lenj:Fin Y.len⊢ (Hom.ofVec (Vector.ofFnC fun j ↦ (Fin.compressEquiv (isRoot v)).symm ⟨v.root j, ⋯⟩)).toVec.get j =
(Fin.compressEquiv (isRoot v)).symm ⟨v.root j, ⋯⟩
Y:FinSetSkelv:UnionFind.Sized Y.lenj:Fin Y.len⊢ (Vector.ofFnC fun j ↦ (Fin.compressEquiv (isRoot v)).symm ⟨v.root j, ⋯⟩).get j =
(Fin.compressEquiv (isRoot v)).symm ⟨v.root j, ⋯⟩
All goals completed! 🐙The representative of a class.
theorem rep_get (Y : FinSetSkel.{u}) (v : UnionFind.Sized Y.len)
(c : Fin (obj Y v).len) :
(rep Y v).get c = (Fin.compressEquiv (isRoot v) c).1 :=
Vector.get_ofFnC _ _The factorisation at a class.
theorem desc_get (Y : FinSetSkel.{u}) (v : UnionFind.Sized Y.len)
(h : Y ⟶ Z) (c : Fin (obj Y v).len) :
(desc Y v h).toVec.get c = h.toVec.get ((rep Y v).get c) := Z:FinSetSkelY:FinSetSkelv:UnionFind.Sized Y.lenh:Y ⟶ Zc:Fin (obj Y v).len⊢ (Hom.toVec (desc Y v h)).get c = (Hom.toVec h).get ((rep Y v).get c)
Z:FinSetSkelY:FinSetSkelv:UnionFind.Sized Y.lenh:Y ⟶ Zc:Fin (obj Y v).len⊢ (Hom.ofVec (Vector.ofFnC fun c ↦ (Hom.toVec h).get ((rep Y v).get c))).toVec.get c = (Hom.toVec h).get ((rep Y v).get c)
Z:FinSetSkelY:FinSetSkelv:UnionFind.Sized Y.lenh:Y ⟶ Zc:Fin (obj Y v).len⊢ (Vector.ofFnC fun c ↦ (Hom.toVec h).get ((rep Y v).get c)).get c = (Hom.toVec h).get ((rep Y v).get c)
All goals completed! 🐙The representative of an index's class is its root.
@[simp] theorem rep_π (Y : FinSetSkel.{u}) (v : UnionFind.Sized Y.len)
(j : Fin Y.len) :
(rep Y v).get ((π Y v).toVec.get j) = v.root j :=
(congrArg _ (π_get Y v j)).trans
((rep_get Y v _).trans
(congrArg Subtype.val (Equiv.apply_symm_apply _ _)))The class of a representative is that class.
@[simp] theorem π_rep (Y : FinSetSkel.{u}) (v : UnionFind.Sized Y.len)
(c : Fin (obj Y v).len) :
(π Y v).toVec.get ((rep Y v).get c) = c := Y:FinSetSkelv:UnionFind.Sized Y.lenc:Fin (obj Y v).len⊢ (Hom.toVec (π Y v)).get ((rep Y v).get c) = c
Y:FinSetSkelv:UnionFind.Sized Y.lenc:Fin (obj Y v).lenh:v.root ((rep Y v).get c) = (rep Y v).get c⊢ (Hom.toVec (π Y v)).get ((rep Y v).get c) = c
Y:FinSetSkelv:UnionFind.Sized Y.lenc:Fin (obj Y v).lenh:v.root ((rep Y v).get c) = (rep Y v).get c⊢ (Fin.compressEquiv (isRoot v)).symm ⟨v.root ((rep Y v).get c), ⋯⟩ = c
Y:FinSetSkelv:UnionFind.Sized Y.lenc:Fin (obj Y v).lenh:v.root ((rep Y v).get c) = (rep Y v).get c⊢ (Fin.compressEquiv (isRoot v)).symm ⟨(rep Y v).get c, ⋯⟩ = c
All goals completed! 🐙The projection coequalizes the pair.
theorem comp_π (f g : X ⟶ Y) :
f ≫ π Y (unionFind f g) = g ≫ π Y (unionFind f g) :=
hom_ext fun i ↦ X:FinSetSkelY:FinSetSkelf:X ⟶ Yg:X ⟶ Yi:Fin X.len⊢ (Hom.toVec (f ≫ π Y (unionFind f g))).get i = (Hom.toVec (g ≫ π Y (unionFind f g))).get i
X:FinSetSkelY:FinSetSkelf:X ⟶ Yg:X ⟶ Yi:Fin X.len⊢ (Fin.compressEquiv (isRoot (unionFind f g))).symm ⟨(unionFind f g).root ((Hom.toVec f).get i), ⋯⟩ =
(Fin.compressEquiv (isRoot (unionFind f g))).symm ⟨(unionFind f g).root ((Hom.toVec g).get i), ⋯⟩
All goals completed! 🐙A morphism coequalizing the pair factors through the projection.
theorem π_desc (f g : X ⟶ Y) (h : Y ⟶ Z) (w : f ≫ h = g ≫ h) :
π Y (unionFind f g) ≫ desc Y (unionFind f g) h = h :=
hom_ext fun j ↦ X:FinSetSkelY:FinSetSkelZ:FinSetSkelf:X ⟶ Yg:X ⟶ Yh:Y ⟶ Zw:f ≫ h = g ≫ hj:Fin Y.len⊢ (Hom.toVec (π Y (unionFind f g) ≫ desc Y (unionFind f g) h)).get j = (Hom.toVec h).get j
X:FinSetSkelY:FinSetSkelZ:FinSetSkelf:X ⟶ Yg:X ⟶ Yh:Y ⟶ Zw:f ≫ h = g ≫ hj:Fin Y.len⊢ (Hom.toVec h).get ((unionFind f g).root j) = (Hom.toVec h).get j
X:FinSetSkelY:FinSetSkelZ:FinSetSkelf:X ⟶ Yg:X ⟶ Yh:Y ⟶ Zw:f ≫ h = g ≫ hj:Fin Y.lenp:Fin Y.len × Fin Y.lenhp:p ∈ edges f g⊢ (Hom.toVec h).get p.fst = (Hom.toVec h).get p.snd
X:FinSetSkelY:FinSetSkelZ:FinSetSkelf:X ⟶ Yg:X ⟶ Yh:Y ⟶ Zw:f ≫ h = g ≫ hj:Fin Y.leni:Fin X.lenhp:((Hom.toVec f).get i, (Hom.toVec g).get i) ∈ edges f g⊢ (Hom.toVec h).get ((Hom.toVec f).get i, (Hom.toVec g).get i).fst =
(Hom.toVec h).get ((Hom.toVec f).get i, (Hom.toVec g).get i).snd
All goals completed! 🐙The factorisation is unique.
theorem desc_uniq (f g : X ⟶ Y) (h : Y ⟶ Z)
(m : obj Y (unionFind f g) ⟶ Z)
(hm : π Y (unionFind f g) ≫ m = h) : m = desc Y (unionFind f g) h :=
hom_ext fun c ↦ X:FinSetSkelY:FinSetSkelZ:FinSetSkelf:X ⟶ Yg:X ⟶ Yh:Y ⟶ Zm:obj Y (unionFind f g) ⟶ Zhm:π Y (unionFind f g) ≫ m = hc:Fin (obj Y (unionFind f g)).len⊢ (Hom.toVec m).get c = (Hom.toVec (desc Y (unionFind f g) h)).get c All goals completed! 🐙endend FinSetSkel.Quotient