diff options
| -rw-r--r-- | Nominal/Category.lean | 43 |
1 files changed, 43 insertions, 0 deletions
diff --git a/Nominal/Category.lean b/Nominal/Category.lean new file mode 100644 index 0000000..fc7e161 --- /dev/null +++ b/Nominal/Category.lean @@ -0,0 +1,43 @@ +import Mathlib +import Nominal.Support +import Nominal.Equivariance + +/-! +# Nominal Set Category + +Nominal sets form a category, where the morphisms are exactly equivariant functions between them. +This file contains formalizations for this category-theoretical view. +-/ + +variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] + +/-! +## Category Definition + +Definition of the Nom category instance. +-/ +section Definition + +/-- An object in the category of nominal sets; i.e., a nominal set. -/ +structure Nom where + /-- The underlying set. -/ + carrier : Type + /-- Nominal set instance. -/ + [nom : NominalSet 𝔸 carrier] + +attribute [instance] Nom.nom + +/-- A morphism in the category of nominal sets; i.e., an equivariant function. -/ +structure Nom.Hom (X Y : Nom 𝔸) where + /-- The underlying function. -/ + toFun : X.carrier → Y.carrier + /-- Equivariance of the function. -/ + equivariant : Equivariant 𝔸 toFun + +/-- Nominal sets form a category with equivariant functions as morphisms. -/ +instance : CategoryTheory.Category (Nom 𝔸) where + Hom := Nom.Hom 𝔸 + id X := ⟨id, id_equivariant 𝔸⟩ + comp f g := ⟨g.toFun ∘ f.toFun, comp_equivariant 𝔸 f.equivariant g.equivariant⟩ + +end Definition |