adamtopaz/UnivAlg

NOTE

This readme is outdated, and refers primarily to the bundled version of our work which preceded the current, unbundled approach.

Experiments with Universal Algebra in Lean

This repository contains some constructions arising from universal algebra, formalized in the lean proof assistant.

We define the following structures:

1. A language defined as a structure in the following way:

structure lang := (op : ℕ → Type*)

Here op n should be thought of as the type of n-ary operations. We introduce a has_coe_to_fun for languages, so that we can just write L n for the type of n-ary operations associated to a language L.

2. Given any language L, we defined a typeclass of interpretations for L. That is, given an n-ary operation of type L n, a type A, and an n-tuple of terms of A, we can "apply" L to produce another term of type A. The approach is as follows.

class has_app (L : lang) (A : Type*) :=
  (app {n} : L n → ftuple A n → A)

3. Given a language L, we defined terms of L by an inductive procedure as follows:

inductive term (L : lang.{v}) : ℕ → Type v 
| of {n} : L n → term n
| get : term 1
| proj {m n} : (fin n → fin m) → term n → term m
| compl {m n} : term m → term (1 + n) → term (m + n)
| compr {m n} : term m → term (n + 1) → term (n + m)

A term of type L.term m n should be thought of as an operations which sends m-tuples to n-tuples. Any type with an interpretation of L obtains an interpretation for any such term by applying structural induction. Note that L.term is a map from ℕ → Type v, and is therefore itself a language. This is captured by the gen construction.

def gen (L : lang.{v}) : lang.{v} := ⟨L.term⟩

4. Given a language L, we defined the type of rules on L, which are relations on the terms of L.
5. Given a language L and rules R, an algebra for the pair (L,R) is a raw algebra which satisfies the axioms outlined by the rules. Our construction for this, denoted ualg extends has_app as follows

class ualg {L : lang} (R : rules L) (A : Type*) extends has_app L A :=
  (cond_eq {n} (t1 t2 : L.gen n) (as : ftuple A n) : R t1 t2 → applyt t1 as = applyt t2 as)

Here L.gen is the (dependent) type of terms generated by the given language L, and applyt is the interpretation of such terms in the given raw algebra.

Morphisms of languages/rules

Given two languages L1 and L2, a morphism L1 -> L2 is simply the data of a function L1 n -> L2 n for every natural n. This is extended to morphisms of pairs (L1,R1) -> (L2,R2) where Ri : rules Li in the obvious way as follows:

structure rules_hom {L1 : lang} (R1 : rules L1) {L2 : lang} (R2 : rules L2) := 
(lhom : lang_hom L1 L2)
(cond_imp {n} {t1 t2 : L1.gen n} : R1 t1 t2 → R2 (lhom.gen t1) (lhom.gen t2))

We use the notation →# to denote morphisms of languages. In the code above, for a morphism f from L1 to L2, the function t.mapt f maps a term in L1 to a term in L2. We also introduce the notation →$ to denote morphisms of pairs consisting of a language and associated rules. If Ri, i = 1,2 are rules on languages Li, then we can simply write R1 →$ R2 for the type of morphisms of pairs (L1,R1) -> (L2,R2).

Left adjoints

Given a morphism of pairs (L1,R1) -> (L2,R2) as above, there is an obvious forgetful functor from (L2,R2)-algebras to (L1,R1)-algebras. The most substantial portion of this work is in the construction of the left adjoint to this forgetful functor. This left adjoint is construted by combining three steps, and the resulting construction can be found in the file src/fron_ualg.lean. It is perhaps important to mention that all of the usual "free" constructions in algebra are special cases of this.