A non-vacuous dg category #

DGCategory is a structure with five axioms, and a structure with five axioms is worth nothing until something satisfies them. This file exhibits an instance on an arbitrary object type, so the axiom set is proved consistent before anything is built on top of it.

Const X has X as its objects and, between any two of them, the cochain complex that is ℤ in every degree with zero differential. Composition is multiplication and the identity is 1. Associativity is mul_assoc and the unit laws are one_mul and mul_one, so those three axioms have content. The differential is zero, so the Leibniz rule and the cocycle condition hold for the uninteresting reason — which is the honest thing to say about them. A non-zero differential waits for C^dg in dg-enhancements-e4.

An idiom this file establishes #

AddCommGrpCat.of ℤ's carrier is not transparent to instance search, so a goal stated on ↑((constComplex).X p) cannot use mul_assoc: the Semigroup instance is not found. Two things work. For a term proof, pin the type on the lemma — mul_assoc (G := ℤ) f g h. For a tactic proof, bind the arguments at type ℤ in the field's lambda — fun _ q _ _ _ _ (f : ℤ) (g : ℤ) => ... — after which the goal is about ℤ and ordinary simp works.