Moduli of perfect complexes

Declarations in this subtree use the geometry-owned AlgebraicGeometry namespace; neutral moduli objects do not belong to a stability namespace. Comparison.lean records the proved arrows between two-term presentation data, the absolute coherent-derived perfect locus, and its Dqc image; it does not identify those notions with relative perfection over a base.