OAI/RepresentationTheory/KazhdanLusztig/HilbertSeries.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Hilbert series of graded modules and boundary sheaves, positivity and strict detection.

  1. theorem OAI.KLInvariance.Hilbert.hasSum_monomials line 14

    Source documentation

    Sum over all monomials in finitely many variables, before grouping by degree.

    theorem hasSum_monomials (σ : Type*) [Fintype σ] {q : ℝ} (hq : 0 ≤ q) (hq1 : q < 1) :
    HasSum (fun d : σ → ℕ => q ^ (∑ i, d i)) ((1-q)⁻¹ ^ Fintype.card σ) := by
…
  2. lemma OAI.KLInvariance.Hilbert.intWeight_eq_natWeight line 38
  3. lemma OAI.KLInvariance.Hilbert.polynomialGrading_nat line 43
  4. instance OAI.KLInvariance.Hilbert.polynomialPiece_finite line 52
  5. lemma OAI.KLInvariance.Hilbert.polynomial_finrank_nat line 62
  6. lemma OAI.KLInvariance.Hilbert.hasSum_finsupp_monomials line 68
  7. theorem OAI.KLInvariance.Hilbert.hasSum_polynomial_nat line 81

    Source documentation

    The actual finite polynomial ring has Hilbert series (1-q)⁻ᴺ.

    theorem hasSum_polynomial_nat (k : Type*) [Field k] (σ : Type*) [Fintype σ]
    {q : ℝ} (hq : 0 ≤ q) (hq1 : q < 1) :
    HasSum (fun n : ℕ => (Module.finrank k (Graded.polynomialGrading k σ n) : ℝ) * q^n)
      ((1-q)⁻¹ ^ Fintype.card σ) := by
…

    Mentions: OAI.KLInvariance.Graded.polynomialGrading

  8. theorem OAI.KLInvariance.Hilbert.hasSum_polynomial line 100

    Source documentation

    Integer-indexed grading, including its zero negative pieces.

    theorem hasSum_polynomial (k : Type*) [Field k] (σ : Type*) [Fintype σ]
    {q : ℝ} (hq : 0 ≤ q) (hq1 : q < 1) :
    HasSum (fun n : ℤ => (Module.finrank k (Graded.polynomialGrading k σ n) : ℝ) * q^n)
      ((1-q)⁻¹ ^ Fintype.card σ) := by
…

    Mentions: OAI.KLInvariance.Graded.polynomialGrading

  9. def OAI.KLInvariance.Hilbert.shiftedPieceEquiv line 127

    Source documentation

    Degree pieces of a shifted finite free module, as a genuine linear equivalence.

    def shiftedPieceEquiv {ι : Type ui} (𝓐 : ℤ → Submodule k A) (d : ι → ℤ) (n : ℤ) :
    Graded.shiftedPiece 𝓐 d n ≃ₗ[k] (∀ i, 𝓐 (n-d i)) where
…

    Mentions: OAI.KLInvariance.Graded.shiftedPiece

  10. instance OAI.KLInvariance.Hilbert.shiftedPiece_finite line 136
  11. lemma OAI.KLInvariance.Hilbert.shiftedPiece_finrank line 142
  12. lemma OAI.KLInvariance.Hilbert.hasSum_shifted_polynomial line 147
  13. theorem OAI.KLInvariance.Hilbert.hasSum_shiftedFree line 160

    Source documentation

    Convergent Hilbert series and its normalization for the actual shifted free module.

    theorem hasSum_shiftedFree (k : Type*) [Field k] (σ : Type*) [Fintype σ]
    {ι : Type*} [Fintype ι] (d : ι → ℤ) {q : ℝ} (hq : 0 < q) (hq1 : q < 1) :
    HasSum (fun n : ℤ =>
      (Module.finrank k (Graded.shiftedPiece (Graded.polynomialGrading k σ) d n) : ℝ) * q^n)
      ((∑ i, q^(d i)) * (1-q)⁻¹ ^ Fintype.card σ) := by
…

    Mentions: OAI.KLInvariance.Graded.shiftedPiece, OAI.KLInvariance.Graded.polynomialGrading

  14. theorem OAI.KLInvariance.Hilbert.exists_finite_graded_cover line 178

    Source documentation

    Any finite graded module admits a finite homogeneous free cover. No projectivity is assumed.

    theorem exists_finite_graded_cover [Module.Finite A M]
    (𝓐 : ℤ → Submodule k A) (𝓜 : ℤ → Submodule k M) [DirectSum.Decomposition 𝓜]
    [SetLike.GradedSMul 𝓐 𝓜] :
    ∃ (ι : Type um), Finite ι ∧ ∃ (d : ι → ℤ) (f : (ι → A) →ₗ[A] M),
      Function.Surjective f ∧ ∀ n v, v ∈ Graded.shiftedPiece 𝓐 d n → f v ∈ 𝓜 n := by
…

    Mentions: OAI.KLInvariance.Graded.shiftedPiece

  15. def OAI.KLInvariance.Hilbert.degreeMap line 196
  16. lemma OAI.KLInvariance.Hilbert.degreeMap_surjective line 202
  17. lemma OAI.KLInvariance.Hilbert.term_top line 217
  18. theorem OAI.KLInvariance.Hilbert.polynomialModule_piece_finite line 232

    Source documentation

    Finiteness of every genuine homogeneous piece, not an extra assumption on the Hilbert series.

    theorem polynomialModule_piece_finite (n : ℤ) : Module.Finite k (𝓜 n) := by
…
  19. theorem OAI.KLInvariance.Hilbert.summable_polynomialModule line 245

    Source documentation

    Every finite graded module over the actual finite polynomial ring has a convergent Hilbert series at every 0<q<1, even when it is not free.

    theorem summable_polynomialModule {q : ℝ} (hq : 0 < q) (hq1 : q < 1) :
    Summable (fun n : ℤ => (Module.finrank k (𝓜 n) : ℝ)*q^n) := by
…
  20. theorem OAI.KLInvariance.Hilbert.summable_term line 262

    Source documentation

    Convergence for every submodule in the fixed finite graded ambient module.

    theorem summable_term (S : Submodule k M) {q : ℝ} (hq : 0 < q) (hq1 : q < 1) :
    Summable (term 𝓜 S q) := by
…

    Mentions: OAI.KLInvariance.Hilbert.term

  21. theorem OAI.KLInvariance.Hilbert.polynomial_eq_of_value_eq line 273

    Source documentation

    Global detection, now with all the manuscript's finite-polynomial-ring hypotheses supplied.

    theorem polynomial_eq_of_value_eq {S T : Submodule k M}
    (h : S ≤ T) (hhom : ∀ n m, m ∈ T → Graded.component 𝓜 n m ∈ T)
    {q : ℝ} (hq : 0 < q) (hq1 : q < 1)
    (hv : value 𝓜 S q = value 𝓜 T q) : S = T := by
…

    Mentions: OAI.KLInvariance.Graded.component, OAI.KLInvariance.Hilbert.value

  22. lemma OAI.KLInvariance.Hilbert.basis_equivFun_symm_graded line 293
  23. lemma OAI.KLInvariance.Hilbert.finrank_homogeneous_basis line 301
  24. theorem OAI.KLInvariance.Hilbert.hasSum_homogeneous_basis line 321

    Source documentation

    The precise Hilbert normalization for a finite homogeneous basis, with the source's convention that a generator in degree d contributes q^d.

    theorem hasSum_homogeneous_basis {q : ℝ} (hq : 0 < q) (hq1 : q < 1) :
    HasSum (fun n : ℤ => (Module.finrank k (𝓜 n) : ℝ)*q^n)
      ((∑ i, q^(d i)) * (1-q)⁻¹ ^ Fintype.card σ) := by
…
  25. def OAI.KLInvariance.Hilbert.degreeKernelEquiv line 346

    Source documentation

    The actual degreewise kernel, not merely an equality of dimensions.

    def degreeKernelEquiv (𝓜 : ℤ → Submodule k M) (𝓝 : ℤ → Submodule k N)
    (f : M →ₗ[A] N) (hf : ∀ n m, m ∈ 𝓜 n → f m ∈ 𝓝 n) (n : ℤ) :
    subPiece 𝓜 (LinearMap.ker f) n ≃ₗ[k] LinearMap.ker (degreeMap 𝓜 𝓝 f hf n) where
…

    Mentions: OAI.KLInvariance.Hilbert.degreeMap

  26. theorem OAI.KLInvariance.Hilbert.finrank_exact line 360
  27. theorem OAI.KLInvariance.Hilbert.value_exact line 374
  28. theorem OAI.KLInvariance.Hilbert.value_exact_of_summable line 392

    Source documentation

    Finite degreewise exactness supplies convergence of both terms; no free-module hypothesis is used.

     theorem value_exact_of_summable
    (𝓜 : ℤ → Submodule k M) (𝓝 : ℤ → Submodule k N)
    [DirectSum.Decomposition 𝓜] [DirectSum.Decomposition 𝓝]
    [∀ n, Module.Finite k (𝓜 n)]
    (f : M →ₗ[A] N) (hf : ∀ n m, m ∈ 𝓜 n → f m ∈ 𝓝 n)
    (hs : Function.Surjective f) {q : ℝ} (hq : 0 < q)
    (hM : Summable (term 𝓜 ⊤ q)) :
    value 𝓜 ⊤ q = value (subPiece 𝓜 (LinearMap.ker f)) ⊤ q + value 𝓝 ⊤ q := by
…

    Mentions: OAI.KLInvariance.Hilbert.term, OAI.KLInvariance.Hilbert.value

  29. def OAI.KLInvariance.Hilbert.subPieceEquiv line 434
  30. theorem OAI.KLInvariance.Hilbert.term_subPiece line 443
  31. theorem OAI.KLInvariance.Hilbert.value_subPiece line 447
  32. def OAI.KLInvariance.Hilbert.imagePieceMap line 451
  33. theorem OAI.KLInvariance.Hilbert.imagePieceMap_surjective line 459
  34. def OAI.KLInvariance.Hilbert.imageKernelEquiv line 476
  35. theorem OAI.KLInvariance.Hilbert.finrank_image_exact line 492
  36. theorem OAI.KLInvariance.Hilbert.value_image_exact line 513

    Source documentation

    Removing a kernel condition adds exactly the Hilbert value of its embedded restriction image. No freeness of the source kernel is used.

     theorem value_image_exact
    (𝓜 : ℤ → Submodule k M) (𝓝 : ℤ → Submodule k N)
    [DirectSum.Decomposition 𝓜] [DirectSum.Decomposition 𝓝]
    [∀ n, Module.Finite k (𝓜 n)]
    (S : Submodule A M) (hS : ∀ n m, m ∈ S → component 𝓜 n m ∈ S)
    (f : M →ₗ[A] N) (hf : ∀ n m, m ∈ 𝓜 n → f m ∈ 𝓝 n)
    {q : ℝ} (hq : 0 < q) (hs : Summable (term 𝓜 (S.restrictScalars k) q)) :
    value 𝓜 (S.restrictScalars k) q =
      value 𝓜 ((S ⊓ LinearMap.ker f).restrictScalars k) q +
      value 𝓝 ((S.map f).restrictScalars k) q := by
…

    Mentions: OAI.KLInvariance.Hilbert.term, OAI.KLInvariance.Hilbert.value