Derived categories

Homological algebra, as usually first taught, runs on two moves. To compute $\operatorname{Ext}$ or $\operatorname{Tor}$ you choose a resolution, apply a functor, and take cohomology; then you prove that the answer does not depend on the choice. And at the end you keep only the cohomology groups, throwing the complex away.

Both moves lose information.

• Choices. The resolution $0 \to \Z \xrightarrow{2} \Z \to \Z/2 \to 0$ and the resolution $0 \to \Z^2 \xrightarrow{\left(\begin{smallmatrix} 2 & 0 \\ 0 & 1 \end{smallmatrix}\right)} \Z^2 \to \Z/2 \to 0$ are different complexes. They are homotopy equivalent to each other, but neither is isomorphic to $\Z/2$, not even up to homotopy — yet each "is" $\Z/2$ for every computational purpose. We would like a world in which both are literally isomorphic to $\Z/2$.
• Forgetting. Cohomology groups do not remember how they are glued. Over $\Z/4$ the complex $\Z/4 \xrightarrow{2} \Z/4$ has the same cohomology as $\Z/2[1] \oplus \Z/2$, but we shall prove the two are genuinely different. Composing derived functors, Grothendieck needed spectral sequences precisely because the cohomology of the inner functor is not enough to compute the outer one.

Grothendieck's remedy, worked out by his student Jean-Louis Verdier around 1960–63, was radical: keep the complex, and formally invert every map of complexes that induces an isomorphism on cohomology. The result, the derived category $D(\mathcal{A})$, is where Grothendieck duality, the six operations on sheaves, Fourier–Mukai transforms, tilting theory and much of modern algebraic geometry and representation theory now live.

Start from an abelian category $\mathcal{A}$ (modules over a ring, sheaves of abelian groups on a space, representations of a quiver) and the toolkit of homological algebra. The derived category is reached in three steps.

1. Complexes. Replace objects by cochain complexes $X = (\cdots \to X^{n-1} \xrightarrow{d} X^n \xrightarrow{d} X^{n+1} \to \cdots)$, and objects $M$ of $\mathcal{A}$ by complexes concentrated in degree $0$.
2. Homotopy. Identify chain maps that are chain homotopic. This gives the homotopy category $K(\mathcal{A})$. Homotopic maps induce the same map on cohomology, so nothing cohomological is lost.
3. Inversion. A quasi-isomorphism is a chain map inducing isomorphisms on all cohomology groups. Every resolution $P \to M$ is one. Invert them all.

The picture to keep in mind comes from topology. A space is studied up to weak homotopy equivalence, and every space is weakly equivalent to a CW complex, which is the "good" model you compute with. In the derived category every object is (under mild hypotheses) isomorphic to a complex of projectives or of injectives — the good models — and derived functors are computed by applying ordinary functors to good models.

Throughout, $\mathcal{A}$ is an abelian category and complexes are cochain complexes indexed by $\Z$. A chain map $f : X \to Y$ is a family $f^n : X^n \to Y^n$ with $d f^n = f^{n+1} d$; it induces maps $H^n(f) : H^n(X) \to H^n(Y)$ on cohomology $H^n(X) = \ker d^n / \operatorname{im} d^{n-1}$.

Since homotopic maps become equal in $D(\mathcal{A})$ (proved below), $Q$ factors through $K(\mathcal{A})$, and $D(\mathcal{A})$ is equally the localisation of $K(\mathcal{A})$ at the quasi-isomorphisms. That second description is the useful one, because of the following theorem.

The proof (Verdier's thesis; see Weibel, An Introduction to Homological Algebra, §10.3, or Kashiwara–Schapira, Categories and Sheaves, Ch. 7 and 13) uses the mapping cone and the triangulated structure of $K(\mathcal{A})$, which is the subject of the next lesson, triangulated categories. Without it one runs into a real problem: the localisation of the category of complexes exists formally, but its morphisms are equivalence classes of zigzags of arbitrary length, which is useless for computation, and for some large abelian categories the Hom-"sets" need not even be sets. When $\mathcal{A}$ has enough injectives or enough projectives, Hom-sets in $D^+(\mathcal{A})$ or $D^-(\mathcal{A})$ are sets, as the theorems below show.

The converse of "homotopy equivalence ⟹ quasi-isomorphism" is false: the map $p : P \to \Z/2$ above is a quasi-isomorphism without a homotopy inverse.

Dually, if $\mathcal{A}$ has enough injectives then $D^+(\mathcal{A})$ is equivalent to $K^+(\mathrm{Inj}\,\mathcal{A})$, the homotopy category of bounded-below complexes of injectives; this is how $D^+(\mathcal{A})$ is shown to have Hom-sets, and how $RF$ is constructed. The isomorphism $\operatorname{Ext}^n(M, N) \cong \operatorname{Hom}_D(M, N[n])$ in fact holds in every abelian category, with $\operatorname{Ext}$ defined by Yoneda's classes of $n$-fold extensions (Verdier; see Gelfand–Manin, Ch. III). Under it, the Yoneda product of extensions becomes composition $M \to N[n] \to L[n+m]$ in $D(\mathcal{A})$.

Derived functors compose. If $F$ sends injectives to $G$-acyclic objects, then $R(G \circ F) \cong RG \circ RF$. The Grothendieck spectral sequence $E_2^{p,q} = R^pG(R^qF(M)) \Rightarrow R^{p+q}(GF)(M)$ is the shadow of this single isomorphism on cohomology. This is the reason derived categories became the language of sheaf theory: the six operations $Rf_*, f^{-1}, Rf_!, f^!, \otimes^{L}, R\mathcal{H}om$, the adjunctions $f^{-1} \dashv Rf_*$ and $Rf_! \dashv f^!$, Verdier duality and base change are all statements in derived categories.

Derived equivalences are equivalences $D^b(\mathcal{A}) \simeq D^b(\mathcal{B})$ (of triangulated categories) between abelian categories that need not be equivalent. Established landmarks:

• Beilinson (1978): $D^b(\mathrm{Coh}\,\mathbb{P}^n) \simeq D^b(\text{mod-}\operatorname{End}(\mathcal{O} \oplus \mathcal{O}(1) \oplus \dots \oplus \mathcal{O}(n)))$ — coherent sheaves on projective space are "the same as" representations of a finite quiver with relations.
• Mukai (1981): for an abelian variety $A$ with dual $\hat A$, the Fourier–Mukai transform with the Poincaré bundle as kernel gives $D^b(\mathrm{Coh}\,A) \simeq D^b(\mathrm{Coh}\,\hat A)$, although $A$ and $\hat A$ need not be isomorphic.
• Happel (1987) and Rickard (1989): tilting theory. Rickard's Morita theorem: for rings $A$, $B$, the derived categories of modules are equivalent if and only if $B \cong \operatorname{End}_{D(A)}(T)^{\mathrm{op}}$ for a tilting complex $T$. For example, the path algebras of two quivers with the same underlying tree are derived equivalent (the reflection functors of Bernstein–Gelfand–Ponomarev are derived equivalences); see quiver representations.
• Orlov (1997): every fully faithful exact functor $D^b(\mathrm{Coh}\,X) \to D^b(\mathrm{Coh}\,Y)$ between smooth projective varieties that admits adjoints is a Fourier–Mukai transform. Bondal–Orlov (2001): a smooth projective variety with ample or anti-ample canonical bundle is determined by $D^b(\mathrm{Coh}\,X)$.
• Bridgeland (2002): smooth projective threefolds related by a flop are derived equivalent.

Open problems (as of the references below; check recent surveys before relying on them):

• The DK conjecture of Bondal–Orlov and Kawamata: $K$-equivalent smooth projective varieties are derived equivalent. Known in special cases (e.g. Bridgeland's theorem in dimension three), open in general.
• Broué's abelian defect group conjecture in modular representation theory (a block with abelian defect group is derived equivalent to its Brauer correspondent). Proved for symmetric groups by Chuang–Rouquier (2008) and in many other cases; open in general. See categorical representation theory.
• Kontsevich's homological mirror symmetry (1994), predicting an equivalence between $D^b(\mathrm{Coh}\,X)$ and a derived Fukaya category of a mirror $X^\vee$; proved in important cases (elliptic curves, Polishchuk–Zaslow; the quartic surface, Seidel) and open in general.

What derived categories cannot do. Cones are not functorial (the next lesson), so many constructions — taking limits of diagrams, gluing — cannot be performed inside $D(\mathcal{A})$ alone. The modern response is to remember more: dg-categories (Bondal–Kapranov, Keller) and stable ∞-categories (Lurie), whose homotopy categories are the triangulated derived categories. See stable ∞-categories.

Mathlib contains a serious amount of this theory, largely due to Joël Riou: the homotopy category HomotopyCategory C (ComplexShape.up ℤ), quasi-isomorphisms, the derived category DerivedCategory C constructed as a localisation, with its triangulated structure, the fully faithful embeddings of C in each degree, and Ext groups. Because existence of the localisation with small Hom-types is a real issue, Mathlib asks for an instance [HasDerivedCategory C] — an assumption that a model with morphisms in a chosen universe has been fixed.

First, the two-term shadow of Proposition 1, proved by hand. For complexes $A_1 \xrightarrow{d} A_0$ and $B_1 \xrightarrow{d'} B_0$, a homotopy is a single map $h : A_0 \to B_1$:

/-- Two-term complexes `A₁ --d--> A₀` and `B₁ --d'--> B₀`, chain maps `f = (f₁, f₀)`,
`g = (g₁, g₀)`, and a homotopy `h : A₀ → B₁` with `f₁ - g₁ = h ∘ d` (and `f₀ - g₀ = d' ∘ h`).
Then `f` and `g` agree on the cycles `H₁ = ker d`: if `d x = 0` then
`f₁ x - g₁ x = h (d x) = h 0 = 0`. -/
theorem cycles_map_eq_of_homotopy (d : A₁ →ₗ[R] A₀) (f₁ g₁ : A₁ →ₗ[R] B₁) (h : A₀ →ₗ[R] B₁)
    (hom₁ : f₁ - g₁ = h ∘ₗ d) (x : A₁) (hx : d x = 0) : f₁ x = g₁ x := by
  have key : f₁ x - g₁ x = h (d x) := by
    rw [← LinearMap.sub_apply, hom₁, LinearMap.comp_apply]
  rw [hx, map_zero] at key
  exact sub_eq_zero.mp key

/-- With the same data, on `H₀ = A₀ / im d` the maps `f₀` and `g₀` differ by a boundary:
`f₀ y - g₀ y = d' (h y)` lies in `im d'`, so `f` and `g` induce the same map
`A₀ / im d → B₀ / im d'`. Together with `cycles_map_eq_of_homotopy` this is the two-term case
of "homotopic chain maps induce equal maps on homology". -/
theorem boundary_of_homotopy (d' : B₁ →ₗ[R] B₀) (f₀ g₀ : A₀ →ₗ[R] B₀) (h : A₀ →ₗ[R] B₁)
    (hom₀ : f₀ - g₀ = d' ∘ₗ h) (y : A₀) : f₀ y - g₀ y ∈ LinearMap.range d' := by
  refine ⟨h y, ?_⟩
  rw [← LinearMap.comp_apply, ← hom₀, LinearMap.sub_apply]

/-- The same statement phrased with quotient classes: `f₀` and `g₀` send every `y` to the same
class in `H₀(B) = B₀ / im d'`. -/
theorem homology_class_eq_of_homotopy (d' : B₁ →ₗ[R] B₀) (f₀ g₀ : A₀ →ₗ[R] B₀)
    (h : A₀ →ₗ[R] B₁) (hom₀ : f₀ - g₀ = d' ∘ₗ h) (y : A₀) :
    Submodule.Quotient.mk (p := LinearMap.range d') (f₀ y) =
      Submodule.Quotient.mk (p := LinearMap.range d') (g₀ y) :=
  (Submodule.Quotient.eq _).mpr (boundary_of_homotopy d' f₀ g₀ h hom₀ y)

The general statement, for complexes in any abelian category, and its consequence in the derived category, are in Mathlib:

/-- Homotopic chain maps induce the same map on homology in every degree, for complexes in any
abelian category. This applies Mathlib's `Homotopy.homologyMap_eq`. It is why homology is
well defined on the homotopy category `K(A)`. -/
theorem homologyMap_eq_of_homotopy {K L : CochainComplex C ℤ} {f g : K ⟶ L}
    (ho : Homotopy f g) (i : ℤ) : HomologicalComplex.homologyMap f i =
      HomologicalComplex.homologyMap g i :=
  ho.homologyMap_eq i

/-- Homotopic chain maps become equal in the derived category: the localisation functor
`Q : C(A) → D(A)` factors through `K(A)`. This applies Mathlib's
`DerivedCategory.Q_map_eq_of_homotopy`. -/
theorem Q_map_eq_of_homotopy {K L : CochainComplex C ℤ} {f g : K ⟶ L} (ho : Homotopy f g) :
    DerivedCategory.Q.map f = DerivedCategory.Q.map g :=
  DerivedCategory.Q_map_eq_of_homotopy (h := ho)

/-- A chain map becomes an isomorphism in `D(A)` exactly when it is a quasi-isomorphism: the
derived category inverts the quasi-isomorphisms and nothing else. This applies Mathlib's
`DerivedCategory.isIso_Q_map_iff_quasiIso`. -/
theorem isIso_Q_map_iff_quasiIso {K L : CochainComplex C ℤ} (φ : K ⟶ L) :
    IsIso (DerivedCategory.Q.map φ) ↔ QuasiIso φ :=
  DerivedCategory.isIso_Q_map_iff_quasiIso (φ := φ)

The last statement says that $Q$ inverts exactly the quasi-isomorphisms — slightly more than the universal property asks for. The embedding of Theorem 4 and the degree-zero case of Theorem 3:

/-- The embedding `A → D(A)` (an object placed in degree `0`) is fully faithful:
`Hom_A(X, Y) → Hom_{D(A)}(X, Y)` is a bijection. This applies Mathlib's instances
`(DerivedCategory.singleFunctor C 0).Full` and `.Faithful`, via
`Functor.FullyFaithful.map_bijective`. -/
theorem single_map_bijective (X Y : C) :
    Function.Bijective (fun f : X ⟶ Y => (DerivedCategory.singleFunctor C 0).map f) :=
  (Functor.FullyFaithful.ofFullyFaithful (DerivedCategory.singleFunctor C 0)).map_bijective X Y

/-- Mathlib *defines* `Ext X Y n` as morphisms `X → Y[n]` in the derived category (the lesson's
key formula `Extⁿ(X, Y) ≅ Hom_{D(A)}(X, Y[n])` is built into the definition). In degree `0`
these are just the morphisms of `A`: `Ext.mk₀ : (X ⟶ Y) → Ext X Y 0` is bijective. This applies
Mathlib's `Abelian.Ext.mk₀_bijective`. -/
theorem ext_zero_bijective {C : Type*} [Category C] [Abelian C] [HasExt C] (X Y : C) :
    Function.Bijective (Abelian.Ext.mk₀ (X := X) (Y := Y)) :=
  Abelian.Ext.mk₀_bijective X Y

Note how Mathlib defines $\operatorname{Ext}^n(X, Y)$ as (a small model of) $\operatorname{Hom}_{D(\mathcal{A})}(X, Y[n])$: Theorem 3 is built into the definition, and what must then be proved are the comparison with resolutions and the long exact sequences (Mathlib.Algebra.Homology.DerivedCategory.Ext).

Finally, the facts behind the first worked example, proved by hand: $\Z \xrightarrow{2} \Z \to \Z/2$ is exact, so the resolution is a quasi-isomorphism; but there is no non-zero map $\Z/2 \to \Z$, so it has no inverse chain map.

/-- Multiplication by `2` on `ℤ` is injective, so `0 → ℤ --2--> ℤ` is exact at the left. -/
theorem two_mul_injective : Function.Injective (fun n : ℤ => 2 * n) := by
  intro a b h
  simp only at h
  omega

/-- The kernel of reduction `ℤ → ℤ/2` is exactly the image of multiplication by `2`, so
`ℤ --2--> ℤ → ℤ/2` is exact in the middle. Together with `two_mul_injective` and surjectivity of
reduction, the complex `[ℤ --2--> ℤ]` (in degrees `-1, 0`) is quasi-isomorphic to `ℤ/2`. -/
theorem exact_at_middle (n : ℤ) : (n : ZMod 2) = 0 ↔ ∃ m : ℤ, 2 * m = n := by
  rw [ZMod.intCast_zmod_eq_zero_iff_dvd]
  constructor
  · rintro ⟨m, hm⟩
    exact ⟨m, by simpa using hm.symm⟩
  · rintro ⟨m, rfl⟩
    exact ⟨m, by norm_num⟩

/-- There is no non-zero group homomorphism `ℤ/2 → ℤ`: `2 · φ(x) = φ(2x) = φ(0) = 0`, and `ℤ`
has no elements of order `2`. Consequently the quasi-isomorphism `[ℤ --2--> ℤ] → ℤ/2` has no
inverse chain map `ℤ/2 → [ℤ --2--> ℤ]` (its degree-0 part would be a map `ℤ/2 → ℤ`, hence zero,
and could not induce the identity on `H⁰ = ℤ/2`). In `D(Ab)` it is nevertheless an isomorphism:
inverting it is exactly what localisation does. -/
theorem hom_zmod_two_int_eq_zero (φ : ZMod 2 →+ ℤ) : φ = 0 := by
  ext x
  have h2 : (2 : ℤ) * φ x = 0 := by
    calc (2 : ℤ) * φ x = φ (x + x) := by rw [map_add]; ring
      _ = φ 0 := by
        congr 1
        fin_cases x <;> rfl
      _ = 0 := map_zero φ
  have : φ x = 0 := by omega
  simpa using this

What is not formalised here: the calculus of fractions in detail (Mathlib has it, in Mathlib.Algebra.Homology.DerivedCategory.Fractions), Lemma 2 and Theorem 3 in full, total derived functors (Mathlib has right derived functors of functors between abelian categories with enough injectives), the non-formality of $\Z/4 \xrightarrow{2} \Z/4$, and derived equivalences.

The experiment computes $\operatorname{Ext}^n(M, N) = H^n \operatorname{Hom}(P, N)$ for small cyclic modules by writing down a projective resolution $P$ and counting kernels and images element by element. Over $\Z$ every Ext vanishes beyond degree $1$ (global dimension $1$, so every object of $D^b(\mathrm{Ab})$ splits). Over $\Z/4$ the module $\Z/2$ has non-zero $\operatorname{Ext}^n(\Z/2, \Z/2) = \operatorname{Hom}_D(\Z/2, \Z/2[n])$ in every degree — the same periodicity that made the "same cohomology, different objects" example work — while $\Z/4$ is injective over itself. Finally it counts extensions $0 \to \Z/p \to E \to \Z/p \to 0$ directly as $2$-cocycles modulo coboundaries, and finds $|\operatorname{Ext}^1(\Z/p, \Z/p)| = p$.

"""Ext groups from resolutions, and Ext^1 from extensions, by exact counting.

In the derived category, Ext^n(M, N) = Hom(M, N[n]). To compute it we replace
M by a projective resolution P -> M (a quasi-isomorphism) and take cohomology
of the complex Hom(P, N). Here every module is a finite cyclic group, so
kernels and images can be counted element by element. Over Z every module
has a resolution of length 1 and Ext^n vanishes for n >= 2; over Z/4 the
module Z/2 has an infinite periodic resolution and Ext^n(Z/2, Z/2) = Z/2 for
every n, while Z/4 is injective over itself. Finally we count the extensions
0 -> Z/p -> E -> Z/p -> 0 directly, as symmetric 2-cocycles modulo
coboundaries, and find p classes: |Ext^1(Z/p, Z/p)| = p, with one split
class and p - 1 classes in which E is cyclic. Exact, exhaustive-finite
evidence for the cases shown; the general theorems are proved in the lesson
and its references.
"""

from itertools import product
from math import gcd

def mult_kernel_image(b, c):
    """Sizes of kernel and image of x -> c x on Z/b (by enumeration)."""
    image = {(c * x) % b for x in range(b)}
    kernel = [x for x in range(b) if (c * x) % b == 0]
    return len(kernel), len(image)

def cohomology_orders(b, factors):
    """Orders of H^n of Z/b --c0--> Z/b --c1--> ... --c_{k-1}--> Z/b.

    The complex has len(factors) + 1 terms; H^n = ker d^n / im d^(n-1), with
    d^n = 0 past the last term.
    """
    orders = []
    for n in range(len(factors) + 1):
        ker = mult_kernel_image(b, factors[n])[0] if n < len(factors) else b
        im = mult_kernel_image(b, factors[n - 1])[1] if n > 0 else 1
        orders.append(ker // im)
    return orders

def ext_over_z(a, b, top=3):
    """|Ext^n_Z(Z/a, Z/b)|, n = 0..top, from 0 -> Z --a--> Z -> Z/a."""
    orders = cohomology_orders(b, [a])  # Hom(P0, N) --a--> Hom(P1, N)
    return (orders + [1] * (top + 1))[: top + 1]

def ext_over_zn(big_n, a, b, top=5):
    """|Ext^n_{Z/N}(Z/a, Z/b)| for a, b dividing N, n = 0..top.

    Periodic resolution ... -> Z/N --a--> Z/N --N/a--> Z/N --a--> Z/N -> Z/a.
    Hom(Z/N, Z/b) = Z/b, and the induced maps are the same multiplications.
    """
    if big_n % a or big_n % b:
        raise ValueError("a and b must divide N")
    factors = [a if n % 2 == 0 else big_n // a for n in range(top + 1)]
    return cohomology_orders(b, factors)[: top + 1]

def homs(a, b):
    """Number of group homomorphisms Z/a -> Z/b (brute force)."""
    return sum(1 for x in range(b) if (a * x) % b == 0)

def extension_classes(p):
    """Classes of extensions 0 -> Z/p -> E -> Z/p -> 0 via 2-cocycles.

    Returns (number of classes, number of classes with E cyclic). A symmetric
    normalised cocycle f gives E = Z/p x Z/p with
    (n, a) + (m, b) = (n + m + f(a, b), a + b); cohomologous cocycles give
    equivalent extensions.
    """
    pairs = list(product(range(p), repeat=2))
    cocycles = []
    for values in product(range(p), repeat=len(pairs)):
        f = dict(zip(pairs, values))
        if f[(0, 0)] or any(f[(a, b)] != f[(b, a)] for a, b in pairs):
            continue
        if all((f[(b, c)] - f[((a + b) % p, c)] + f[(a, (b + c) % p)]
                - f[(a, b)]) % p == 0
               for a, b, c in product(range(p), repeat=3)):
            cocycles.append(f)
    boundaries = set()
    for g in product(range(p), repeat=p):
        if g[0] == 0:
            boundaries.add(tuple((g[a] + g[b] - g[(a + b) % p]) % p
                                 for a, b in pairs))
    classes = {}
    for f in cocycles:
        key = min(tuple((f[q] - d[i]) % p for i, q in enumerate(pairs))
                  for d in boundaries)
        classes[key] = f
    cyclic = sum(1 for f in classes.values() if extension_is_cyclic(f, p))
    return len(classes), cyclic

def extension_is_cyclic(f, p):
    """Is the group E built from the cocycle f cyclic (an element of order p^2)?"""
    for n0, a0 in product(range(p), repeat=2):
        n, a, order = n0, a0, 1
        while (n, a) != (0, 0):
            n, a = (n + n0 + f[(a, a0)]) % p, (a + a0) % p
            order += 1
        if order == p * p:
            return True
    return False

def main():
    print("Ext over Z (resolution 0 -> Z --a--> Z -> Z/a):")
    for a, b in [(2, 2), (4, 6), (3, 5)]:
        print(f"  |Ext^n(Z/{a}, Z/{b})|, n = 0..3: {ext_over_z(a, b)}"
              f"   |Hom| = {homs(a, b)} = gcd = {gcd(a, b)}")
    print("Ext over Z/4 (periodic resolution ... --2--> Z/4 --2--> Z/4):")
    print("  |Ext^n(Z/2, Z/2)|, n = 0..5:", ext_over_zn(4, 2, 2))
    print("  |Ext^n(Z/2, Z/4)|, n = 0..5:", ext_over_zn(4, 2, 4))
    print("Ext over Z/9:")
    print("  |Ext^n(Z/3, Z/3)|, n = 0..5:", ext_over_zn(9, 3, 3))
    print()
    print("Extensions 0 -> Z/p -> E -> Z/p -> 0, counted as cocycles:")
    for p in (2, 3):
        total, cyclic = extension_classes(p)
        print(f"  p = {p}: {total} classes = |Ext^1(Z/{p}, Z/{p})|; "
              f"{cyclic} with E = Z/{p * p}, {total - cyclic} split")
    print()
    print("Epistemic status: exact counts, exhaustive over the finite groups")
    print("shown. They illustrate (not prove) Ext^n(M, N) = Hom_D(M, N[n]),")
    print("Z having global dimension 1 while Z/4 and Z/9 have infinite global")
    print("dimension, and Ext^1 as classes of extensions. That Ext does not")
    print("depend on the resolution chosen is a theorem, not checked here.")

if __name__ == "__main__":
    main()

This is exact, exhaustive evidence for finitely many small cases. It illustrates the theorems; the proofs above (and in the references) establish them.