Multigraded Betti numbers and Poincaré series

• Multigraded polynomial modules
• Multigraded free modules and graded free resolutions
• Multigraded Betti numbers after residue-field base change
• Degree components of the base-changed multigraded resolution
• Invariance of multigraded Betti numbers across graded free resolutions
• Multigraded Poincaré-series coefficient family
• Multigraded Poincaré polynomial

TheoremFinite homogeneous generating sets#✓fully proved

Let \(K\) be a field, let \(R = K[x_1, \dots, x_n]\), and let \(M\) be a multigraded polynomial module over \(R\), with degree-\(\alpha\) components \(M_\alpha\) for \(\alpha \in \mathbb{Z}^n\), that is finitely generated as an \(R\)-module. Then there is a finite set \(s \subseteq M\) of homogeneous elements, each lying in \(M_\alpha\) for some \(\alpha \in \mathbb{Z}^n\), that generates \(M\) as an \(R\)-module.

public theorem MultigradedPolynomialModule.exists_finset_homogeneous_generators
    (K : Type*) [Field K] (n : ℕ) (M : Type*)
    [AddCommGroup M] [Module (MvPolynomial (Fin n) K) M] [Module K M]
    (targetGraded : MultigradedPolynomialModule K n M)
    [Module.Finite (MvPolynomial (Fin n) K) M] :
    ∃ s : Finset M,
      (∀ m ∈ s, ∃ α : Fin n →₀ Int, m ∈ targetGraded.component α) ∧
      Submodule.span (MvPolynomial (Fin n) K) (s : Set M) = ⊤

Sources

• Braun-Davis, JIS 23 (2020), span 856-877; see https://cs.uwaterloo.ca/journals/JIS/VOL23/Braun/braun4.tex

Uses 1

Statement usesMultigraded modules over a polynomial ring

TheoremFinite bases give finite-dimensional multidegree pieces#✓fully proved

Let \(K\) be a field, let \(R = K[x_1, \dots, x_n]\), let \(M\) be a multigraded polynomial module over \(R\), and let \(F\) be a multigraded free resolution of \(M\) whose term \(F_i\) has the homogeneous basis \((e_j)_{j \in \iota_i}\). Write \(K \otimes_R F\) for the chain complex of \(K\)-vector spaces obtained from \(F\) by extending scalars along the evaluation \(R \to K\) at \(x = 0\). If \(\iota_i\) is finite, then for every \(\alpha \in \mathbb{Z}^n\) the degree-\(\alpha\) piece of \((K \otimes_R F)_i\), the \(K\)-span of the vectors \(1 \otimes e_j\) with \(e_j\) of degree \(\alpha\), is finite-dimensional over \(K\).

theorem MultigradedFreeResolution.baseChangedDegreePiece_finite
    (K : Type u) [Field K] (n : Nat) (M : Type u) [AddCommGroup M]
    [Module (MvPolynomial (Fin n) K) M] [Module K M]
    (targetGraded : MultigradedPolynomialModule K n M)
    (resolution : CategoryTheory.ProjectiveResolution
      (ModuleCat.of (MvPolynomial (Fin n) K) M))
    (ι : Nat → Type u)
    (res : MultigradedFreeResolution K n M targetGraded resolution ι)
    (α : Fin n →₀ Int) (i : Nat) [Finite (ι i)] :
    Module.Finite K ↥(baseChangedDegreePiece (K := K) (n := n) (M := M)
      targetGraded resolution ι res i α)

Sources

• Benjamin Braun and Brian Davis, "Antichain Simplices," Journal of Integer Sequences 23 (2020), lines 862–867, https://cs.uwaterloo.ca/journals/JIS/VOL23/Braun/braun4.tex.

Uses 6 · Used by 1

Statement usesMultigraded free resolution · Multigraded modules over a polynomial ring · Base change of a resolution to the residue field · Degree pieces of the base-changed resolution

Proof usesMultigraded free module · Augmentation of the polynomial ring

Used byExistence of multigraded base-change data

DefinitionMultidegree decomposition of the base-changed resolution#✓fully proved

Let \(K\) be a field, let \(R = K[x_1, \dots, x_n]\), let \(M\) be a multigraded polynomial module over \(R\), and let \(F\) be a multigraded free resolution of \(M\) whose term \(F_i\) has the homogeneous basis \((e_j)_{j \in \iota_i}\). Write \(K \otimes_R F\) for the chain complex of \(K\)-vector spaces obtained from \(F\) by extending scalars along the evaluation \(R \to K\) at \(x = 0\), and for \(\alpha \in \mathbb{Z}^n\) call the \(K\)-span of the vectors \(1 \otimes e_j\) with \(e_j\) of degree \(\alpha\) the degree-\(\alpha\) piece of \((K \otimes_R F)_i\). For every \(i \ge 0\), this is the decomposition of \((K \otimes_R F)_i\) as the internal direct sum of its degree-\(\alpha\) pieces over \(\alpha \in \mathbb{Z}^n\).

MetaMathlibExt.MultigradedFreeResolution.baseChangedDegreeDecomposition · 142 lines

@[instance_reducible]
public noncomputable def MultigradedFreeResolution.baseChangedDegreeDecomposition
    {K : Type u} [Field K] {n : ℕ} {M : Type u} [AddCommGroup M]
    [Module (MvPolynomial (Fin n) K) M] [Module K M]
    (targetGraded : MultigradedPolynomialModule K n M)
    (resolution : CategoryTheory.ProjectiveResolution
      (ModuleCat.of (MvPolynomial (Fin n) K) M))
    (ι : ℕ → Type u) (res : MultigradedFreeResolution K n M targetGraded resolution ι)
    (i : ℕ) :
    DirectSum.Decomposition
      (fun α => baseChangedDegreePiece targetGraded resolution ι res i α) := by
  letI : Module K ↥(resolution.complex.X i) :=
    Module.compHom _ (MvPolynomial.C : K →+* MvPolynomial (Fin n) K)
  letI : Algebra (MvPolynomial (Fin n) K) K := zeroEval.toAlgebra
  let b : Module.Basis (ι i) K ↥((baseChangedComplex resolution).X i) :=
    (res.termFree i).basis.baseChange K
  have fiberEq : ∀ a : (Fin n →₀ Int),
      ({ y | ∃ j : ι i, (res.termFree i).degree j = a ∧ y = b j } :
        Set ↥((baseChangedComplex resolution).X i)) =
      ((⇑b '' ({ k : ι i | (res.termFree i).degree k = a } : Set (ι i))) :
        Set ↥((baseChangedComplex resolution).X i)) := by
    intro a
    apply Set.ext
    intro y
    constructor
    · intro hy
      obtain ⟨j, hjDeg, rfl⟩ := hy
      exact ⟨j, hjDeg, rfl⟩
    · intro hy
      change ∃ j : ι i, j ∈ ({ k : ι i | (res.termFree i).degree k = a } :
        Set (ι i)) ∧ b j = y at hy
      obtain ⟨j, hjMem, rfl⟩ := hy
      exact ⟨j, hjMem, rfl⟩
  have basisInd : LinearIndependent K (⇑b) := b.linearIndependent
  have hiSpan : iSupIndep (fun a : (Fin n →₀ Int) =>
      Submodule.span K
        ({ y | ∃ j : ι i, (res.termFree i).degree j = a ∧ y = b j } :
          Set ↥((baseChangedComplex resolution).X i))) := by
    intro a
    change Disjoint
      (Submodule.span K
        ({ y | ∃ j : ι i, (res.termFree i).degree j = a ∧ y = b j } :
          Set ↥((baseChangedComplex resolution).X i)))
      (⨆ c : (Fin n →₀ Int), ⨆ _ : c ≠ a, Submodule.span K
        ({ y | ∃ j : ι i, (res.termFree i).degree j = c ∧ y = b j } :
          Set ↥((baseChangedComplex resolution).X i)))
    have hDisjIdx : Disjoint
        ({ k : ι i | (res.termFree i).degree k = a } : Set (ι i))
        (⋃ c : (Fin n →₀ Int), ⋃ _ : c ≠ a,
          ({ k : ι i | (res.termFree i).degree k = c } : Set (ι i))) := by
      rw [Set.disjoint_left]
      intro j hjA hjRest
      rw [Set.mem_iUnion] at hjRest
      obtain ⟨c, hcRest⟩ := hjRest
      rw [Set.mem_iUnion] at hcRest
      obtain ⟨hNe, hjC⟩ := hcRest
      have hjA' : (res.termFree i).degree j = a := hjA
      have hjC' : (res.termFree i).degree j = c := hjC
      exact hNe (hjC'.symm.trans hjA')
    have hDisjSpan : Disjoint
        (Submodule.span K
          ((⇑b '' ({ k : ι i | (res.termFree i).degree k = a } : Set (ι i))) :
            Set ↥((baseChangedComplex resolution).X i)))
        (Submodule.span K
          ((⇑b '' (⋃ c : (Fin n →₀ Int), ⋃ _ : c ≠ a,
            ({ k : ι i | (res.termFree i).degree k = c } : Set (ι i)))) :
            Set ↥((baseChangedComplex resolution).X i))) :=
      basisInd.disjoint_span_image hDisjIdx
    have hFA : Submodule.span K
        ({ y | ∃ j : ι i, (res.termFree i).degree j = a ∧ y = b j } :
          Set ↥((baseChangedComplex resolution).X i)) =
        Submodule.span K
          ((⇑b '' ({ k : ι i | (res.termFree i).degree k = a } : Set (ι i))) :
            Set ↥((baseChangedComplex resolution).X i)) := by
      rw [fiberEq a]
    rw [hFA]
    refine Disjoint.mono_right ?_ hDisjSpan
    apply iSup_le
    intro c
    apply iSup_le
    intro hc
    have hNe : c ≠ a := hc
    rw [fiberEq c]
    apply Submodule.span_mono
    apply Set.image_mono
    intro j hj
    rw [Set.mem_iUnion]
    refine ⟨c, ?_⟩
    rw [Set.mem_iUnion]
    exact ⟨hNe, hj⟩
  have hsSpan : (⨆ a : (Fin n →₀ Int), Submodule.span K
      ({ y | ∃ j : ι i, (res.termFree i).degree j = a ∧ y = b j } :
        Set ↥((baseChangedComplex resolution).X i))) = ⊤ := by
    have coverEq : (⋃ a : (Fin n →₀ Int),
        ((⇑b '' ({ k : ι i | (res.termFree i).degree k = a } : Set (ι i))) :
          Set ↥((baseChangedComplex resolution).X i))) =
        Set.range (⇑b) := by
      apply Set.ext
      intro y
      constructor
      · intro hy
        rw [Set.mem_iUnion] at hy
        obtain ⟨a, ha⟩ := hy
        change ∃ j : ι i, j ∈ ({ k : ι i | (res.termFree i).degree k = a } :
          Set (ι i)) ∧ b j = y at ha
        obtain ⟨j, hjMem, hjEq⟩ := ha
        exact Set.mem_range.mpr ⟨j, hjEq⟩
      · intro hy
        obtain ⟨j, hjEq⟩ := Set.mem_range.mp hy
        rw [Set.mem_iUnion]
        exact ⟨(res.termFree i).degree j, j, rfl, hjEq⟩
    calc (⨆ a : (Fin n →₀ Int), Submodule.span K
            ({ y | ∃ j : ι i, (res.termFree i).degree j = a ∧ y = b j } :
              Set ↥((baseChangedComplex resolution).X i)))
        = (⨆ a : (Fin n →₀ Int), Submodule.span K
            ((⇑b '' ({ k : ι i | (res.termFree i).degree k = a } : Set (ι i))) :
              Set ↥((baseChangedComplex resolution).X i))) := by
          simp only [fiberEq]
      _ = Submodule.span K
            (⋃ a : (Fin n →₀ Int),
              ((⇑b '' ({ k : ι i | (res.termFree i).degree k = a } : Set (ι i))) :
                Set ↥((baseChangedComplex resolution).X i))) :=
          (Submodule.span_iUnion _).symm
      _ = Submodule.span K (Set.range (⇑b)) := by
          rw [coverEq]
      _ = ⊤ := b.span_eq
  have hIntSpan : DirectSum.IsInternal (fun a : (Fin n →₀ Int) =>
      Submodule.span K
        ({ y | ∃ j : ι i, (res.termFree i).degree j = a ∧ y = b j } :
          Set ↥((baseChangedComplex resolution).X i))) :=
    DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top hiSpan hsSpan
  have familyEq : (fun α : (Fin n →₀ Int) =>
        baseChangedDegreePiece targetGraded resolution ι res i α) =
      (fun a : (Fin n →₀ Int) => Submodule.span K
        ({ y | ∃ j : ι i, (res.termFree i).degree j = a ∧ y = b j } :
          Set ↥((baseChangedComplex resolution).X i))) :=
    funext (fun α => rfl)
  have hInt : DirectSum.IsInternal (fun α : (Fin n →₀ Int) =>
      baseChangedDegreePiece targetGraded resolution ι res i α) := by
    rw [familyEq]
    exact hIntSpan
  exact DirectSum.IsInternal.chooseDecomposition _ hInt

Sources

• Braun-Davis, JIS 23 (2020), lines 856-867. See https://cs.uwaterloo.ca/journals/JIS/VOL23/Braun/braun4.tex

Uses 6 · Used by 1

Statement usesMultigraded free module · Multigraded free resolution · Multigraded modules over a polynomial ring · Base change of a resolution to the residue field · Degree pieces of the base-changed resolution · Augmentation of the polynomial ring

Used byExistence of multigraded base-change data

TheoremBetti numbers do not depend on the choice of base change data#✓fully proved

Let \(K\) be a field, let \(R = K[x_1, \dots, x_n]\), and let \(M\) be a \(\mathbb{Z}^n\)-graded \(R\)-module with a fixed multigraded free resolution \(P_\bullet \to M\). Any two choices of multigraded base change data for \(P_\bullet\) define the same multigraded Betti numbers, in every multidegree \(\alpha \in \mathbb{Z}^n\) and every homological index \(i \in \mathbb{N}\).

public theorem multigradedBettiNumber_eq_of_baseChange
    {K : Type u} [Field K] {n : ℕ}
    {M : Type u} [AddCommGroup M]
    [Module (MvPolynomial (Fin n) K) M] [Module K M]
    {targetGraded : MultigradedPolynomialModule K n M}
    {resolution : CategoryTheory.ProjectiveResolution
      (ModuleCat.of (MvPolynomial (Fin n) K) M)}
    {ι : ℕ → Type u}
    {res : MultigradedFreeResolution K n M targetGraded resolution ι}
    (data₁ data₂ : MultigradedBaseChange targetGraded resolution ι res)
    (α : Fin n →₀ Int) (i : ℕ) :
    multigradedBettiNumber data₁ α i = multigradedBettiNumber data₂ α i

Sources

• Benjamin Braun and Brian Davis, “Antichain Simplices,” Journal of Integer Sequences 23 (2020), https://cs.uwaterloo.ca/journals/JIS/VOL23/Braun/braun4.tex, exact lines 866--874. This covers only the fixed-resolution coherence step; independence across resolutions, finite support, Poincaré polynomiality, and Hilbert syzygy are deliberately not claimed here.

Uses 6

Statement usesMultigraded base change data · Multigraded free resolution · Multigraded modules over a polynomial ring · Multigraded Betti number

Proof usesBase change of a resolution to the residue field · Degree pieces of the base-changed resolution

TheoremExistence of finite multigraded free resolutions#✓fully proved

Let \(K\) be a field, let \(R = K[x_1, \dots, x_n]\), and let \(M\) be a multigraded \(R\)-module that is finitely generated over \(R\). Then there are a projective resolution \(P_\bullet \to M\) over \(R\), index types \(\iota_i\) for \(i \in \mathbb{N}\), a multigraded free resolution structure on \(P_\bullet\) for the given grading of \(M\) in which \(P_i\) has basis indexed by \(\iota_i\), and a number \(b \in \mathbb{N}\) such that every \(\iota_i\) is finite and \(\iota_i\) is empty for every \(i > b\).

The proof uses stagewise minimal homogeneous free covers, the determinant trick, dimension shifting, and Hilbert's syzygy theorem.

public theorem exists_finite_multigraded_free_resolution
    (K : Type u) (n : ℕ) (M : Type u)
    [Field K] [AddCommGroup M]
    [Module (MvPolynomial (Fin n) K) M] [Module K M]
    (targetGraded : MultigradedPolynomialModule K n M)
    [Module.Finite (MvPolynomial (Fin n) K) M] :
    ∃ (resolution : CategoryTheory.ProjectiveResolution
        (ModuleCat.of (MvPolynomial (Fin n) K) M))
      (ι : ℕ → Type u)
      (res : MultigradedFreeResolution K n M targetGraded resolution ι)
      (bound : ℕ),
      (∀ i, Finite (ι i)) ∧ ∀ i, bound < i → IsEmpty (ι i)

Sources

• Hoffman–Wang, https://export.arxiv.org/e-print/math/0601101v1 lines 592-612 (finite free graded resolution). The Braun–Davis JIS passage https://cs.uwaterloo.ca/journals/JIS/VOL23/Braun/braun4.tex lines 856-876 supplies the motivating Hilbert-syzygy / Poincaré-series context only. No ≤ n bound is claimed here.

Uses 6

Statement usesMultigraded free resolution · Multigraded modules over a polynomial ring

Proof usesHilbert's syzygy theorem · Degree-zero homomorphisms of multigraded modules · Multigraded free module · Exponent vectors as integer vectors

TheoremFinite support of the multigraded Poincaré coefficients#✓fully proved

Let \(K\) be a field, let \(R = K[x_1, \dots, x_n]\), let \(M\) be a multigraded \(R\)-module, and let \(D\) be base-change data for a multigraded free resolution \(F_\bullet\) of \(M\) in which \(F_i\) has a homogeneous basis indexed by \(\iota_i\). Suppose every \(\iota_i\) is finite and, for some \(b \in \mathbb{N}\), \(\iota_i\) is empty for every \(i > b\). Then the multigraded Poincaré coefficient family of \(D\) is nonzero at only finitely many \((i, \alpha) \in \mathbb{N} \times \mathbb{Z}^n\).

public theorem multigradedPoincareCoefficients_hasFiniteSupport_of_finiteResolution
    {K : Type u} [Field K] {n : ℕ}
    {M : Type u} [AddCommGroup M]
    [Module (MvPolynomial (Fin n) K) M] [Module K M]
    {targetGraded : MultigradedPolynomialModule K n M}
    {resolution : CategoryTheory.ProjectiveResolution
      (ModuleCat.of (MvPolynomial (Fin n) K) M)}
    {ι : ℕ → Type u}
    {res : MultigradedFreeResolution K n M targetGraded resolution ι}
    (data : MultigradedBaseChange targetGraded resolution ι res)
    (bound : ℕ)
    (finiteBasis : ∀ i, Finite (ι i))
    (emptyAbove : ∀ i, bound < i → IsEmpty (ι i)) :
    Function.HasFiniteSupport (multigradedPoincareCoefficients data)

Sources

• Benjamin Braun and Brian Davis, “Antichain Simplices,” Journal of Integer Sequences 23 (2020), https://cs.uwaterloo.ca/journals/JIS/VOL23/Braun/braun4.tex, exact line 876. This is the conditional finite-resolution bridge behind that line, not the full Hilbert syzygy existence theorem: it assumes the finite terminating resolution and derives finite coefficient support, without assuming finite support, eventual Betti vanishing, or a polynomial realization, and without constructing the resolution.

Uses 9 · Used by 2

Statement usesMultigraded base change data · Multigraded free resolution · Multigraded modules over a polynomial ring · Multigraded Poincaré coefficients

Proof usesMultigraded free module · Base change of a resolution to the residue field · Degree pieces of the base-changed resolution · Multigraded Betti number · Augmentation of the polynomial ring

Used byMultigraded Poincaré polynomial · Coefficients of the multigraded Poincaré polynomial

TheoremBase change of a homogeneous element along zero evaluation#✓fully proved

Let \(K\) be a field, \(R = K[x_1, \dots, x_n]\), and let \(F\) be a multigraded free \(R\)-module with basis \((b_j)_{j \in \iota}\), where each \(b_j\) is homogeneous of degree \(d_j \in \mathbb{Z}^n\). Make \(K\) an \(R\)-algebra through the zero evaluation \(R \to K\), which sends every variable to \(0\). If \(x \in F\) is homogeneous of degree \(\alpha \in \mathbb{Z}^n\), then \(1 \otimes x \in K \otimes_R F\) lies in the \(K\)-linear span of the vectors \(1 \otimes b_j\) with \(d_j = \alpha\).

theorem MultigradedFreeModule.baseChange_mem_degreeSpan
    {K : Type*} [Field K] {n : ℕ} {F : Type*} [AddCommGroup F]
    [Module (MvPolynomial (Fin n) K) F] [Module K F] {ι : Type*}
    (free : MultigradedFreeModule K n F ι) (α : Fin n →₀ Int) {x : F}
    (hx : x ∈ free.graded.component α) :
    letI : Algebra (MvPolynomial (Fin n) K) K := zeroEval.toAlgebra;
    (1 ⊗ₜ[MvPolynomial (Fin n) K] x : TensorProduct (MvPolynomial (Fin n) K) K F) ∈
      Submodule.span K {y | ∃ j : ι, free.degree j = α ∧ y = free.basis.baseChange K j}

Sources

• Benjamin Braun and Brian Davis, "Antichain Simplices," Journal of Integer Sequences 23 (2020), lines 862–867, https://cs.uwaterloo.ca/journals/JIS/VOL23/Braun/braun4.tex, which split a graded free resolution and take the degree-α component after tensoring with K.

Uses 4 · Used by 1

Statement usesMultigraded free module · Multigraded modules over a polynomial ring · Augmentation of the polynomial ring

Proof usesExponent vectors as integer vectors

Used byThe base-changed differential preserves multidegree

TheoremThe base-changed differential preserves multidegree#✓fully proved

Let \(K\) be a field, let \(R = K[x_1, \dots, x_n]\), let \(M\) be a multigraded polynomial module over \(R\), and let \(F\) be a multigraded free resolution of \(M\) whose term \(F_i\) has the homogeneous basis \((e_j)_{j \in \iota_i}\). Write \(K \otimes_R F\) for the chain complex of \(K\)-vector spaces obtained from \(F\) by extending scalars along the evaluation \(R \to K\) at \(x = 0\), and for \(\alpha \in \mathbb{Z}^n\) call the \(K\)-span of the vectors \(1 \otimes e_j\) with \(e_j\) of degree \(\alpha\) the degree-\(\alpha\) piece of \((K \otimes_R F)_i\). Then for every \(i \ge 0\) and every \(\alpha \in \mathbb{Z}^n\), the differential \((K \otimes_R F)_{i+1} \to (K \otimes_R F)_i\) maps the degree-\(\alpha\) piece of \((K \otimes_R F)_{i+1}\) into the degree-\(\alpha\) piece of \((K \otimes_R F)_i\).

MetaMathlibExt.MultigradedFreeResolution.baseChangedDifferential_preservesDegree · 18 lines

theorem MultigradedFreeResolution.baseChangedDifferential_preservesDegree
    {K : Type u} [Field K] {n : ℕ}
    {M : Type u} [AddCommGroup M] [Module (MvPolynomial (Fin n) K) M]
    [Module K M]
    (targetGraded : MultigradedPolynomialModule K n M)
    (resolution : CategoryTheory.ProjectiveResolution
      (ModuleCat.of (MvPolynomial (Fin n) K) M))
    (ι : ℕ → Type u)
    (res : MultigradedFreeResolution K n M targetGraded resolution ι)
    (i : ℕ) (α : Fin n →₀ Int)
    (x : ↥((baseChangedComplex (K := K) (n := n) (M := M) resolution).X (i + 1)))
    (hx : x ∈ baseChangedDegreePiece (K := K) (n := n) (M := M) targetGraded
      resolution ι res (i + 1) α) :
    (ModuleCat.Hom.hom
      ((baseChangedComplex (K := K) (n := n) (M := M) resolution).d (i + 1)
        i)) x ∈
      baseChangedDegreePiece (K := K) (n := n) (M := M) targetGraded resolution
        ι res i α

Sources

• Benjamin Braun and Brian Davis, "Antichain Simplices," Journal of Integer Sequences 23 (2020), lines 862–867, https://cs.uwaterloo.ca/journals/JIS/VOL23/Braun/braun4.tex.

Uses 8 · Used by 3

Statement usesMultigraded free resolution · Multigraded modules over a polynomial ring · Base change of a resolution to the residue field · Degree pieces of the base-changed resolution

Proof usesDegree-zero homomorphisms of multigraded modules · Multigraded free module · Base change of a homogeneous element along zero evaluation · Augmentation of the polynomial ring

Used byMultidegree component complex of the base-changed resolution · Inclusion of a multidegree component complex · Existence of multigraded base-change data

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.