OAI/RepresentationTheory/KazhdanLusztig/GradedModules.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

Graded polynomial modules, projective presentations, finite homogeneous generators and uniqueness of minimal covers.

  1. theorem OAI.KLInvariance.Graded.eq_top_of_positive_smul_sup line 20

    Source documentation

    Graded Nakayama in its generation form. The submodule is closed under actual homogeneous components, rather than assumed to be the whole module.

    theorem eq_top_of_positive_smul_sup
    (š“ : ā„¤ ā†’ Submodule k A) (š“œ : ā„¤ ā†’ Submodule k M)
    [DirectSum.Decomposition š“œ] [SetLike.GradedSMul š“ š“œ]
    (dā‚€ : ā„¤) (hbound : āˆ€ j < dā‚€, š“œ j = āŠ„)
    (N : Submodule A M) (hN : āˆ€ n m, m āˆˆ N ā†’ (DirectSum.decompose š“œ m n : M) āˆˆ N)
    (hgen : N āŠ” positiveIdeal š“ ā€¢ (āŠ¤ : Submodule A M) = āŠ¤) : N = āŠ¤ := by
ā€¦

    Mentions: OAI.KLInvariance.Graded.positiveIdeal

  2. theorem OAI.KLInvariance.Graded.component_smul_homogeneous line 99

    Source documentation

    Projection of a scalar multiple of a homogeneous vector.

    theorem component_smul_homogeneous
    (š“ : ā„¤ ā†’ Submodule k A) (š“œ : ā„¤ ā†’ Submodule k M)
    [DirectSum.Decomposition š“] [DirectSum.Decomposition š“œ]
    [SetLike.GradedSMul š“ š“œ] (a : A) (m : M) (d n : ā„¤) (hm : m āˆˆ š“œ d) :
    component š“œ n (a ā€¢ m) = component š“ (n-d) a ā€¢ m := by
ā€¦

    Mentions: OAI.KLInvariance.Graded.component

  3. theorem OAI.KLInvariance.Graded.exists_finite_homogeneous_generators line 129

    Source documentation

    Finite generation can be made homogeneous using the actual finite support decomposition of each generator.

    theorem exists_finite_homogeneous_generators
    (š“œ : ā„¤ ā†’ Submodule k M) [DirectSum.Decomposition š“œ] [Module.Finite A M] :
    āˆƒ t : Finset M, Submodule.span A (t : Set M) = āŠ¤ āˆ§
      āˆ€ m āˆˆ t, āˆƒ d : ā„¤, m āˆˆ š“œ d := by
ā€¦
  4. theorem OAI.KLInvariance.Graded.homogeneous_span_components line 156

    Source documentation

    The span of finitely many homogeneous vectors is closed under each component, as required for graded Nakayama.

    theorem homogeneous_span_components {Ī¹ : Type*} [Fintype Ī¹]
    (š“ : ā„¤ ā†’ Submodule k A) (š“œ : ā„¤ ā†’ Submodule k M)
    [DirectSum.Decomposition š“] [DirectSum.Decomposition š“œ]
    [SetLike.GradedSMul š“ š“œ] (v : Ī¹ ā†’ M) (d : Ī¹ ā†’ ā„¤)
    (hv : āˆ€ i, v i āˆˆ š“œ (d i)) (n : ā„¤) (m : M)
    (hm : m āˆˆ Submodule.span A (Set.range v)) :
    component š“œ n m āˆˆ Submodule.span A (Set.range v) := by
ā€¦

    Mentions: OAI.KLInvariance.Graded.component

  5. theorem OAI.KLInvariance.Graded.quotient_smul_of_scalar_mod line 173

    Source documentation

    Reduction of a scalar modulo the augmentation ideal gives precisely its scalar-field action on the reduced module.

    theorem quotient_smul_of_scalar_mod (I : Ideal A) (a : A) (c : k)
    (hac : a-algebraMap k A c āˆˆ I) (m : M) :
    (I ā€¢ (āŠ¤ : Submodule A M)).mkQ (a ā€¢ m) =
      c ā€¢ (I ā€¢ (āŠ¤ : Submodule A M)).mkQ m := by
ā€¦
  6. theorem OAI.KLInvariance.Graded.linearIndependent_of_projective_cover line 191

    Source documentation

    A finite free cover of a projective module, minimal at any proper augmentation ideal of a noetherian domain, is injective. The determinant form of Nakayama removes the complementary torsion-free kernel.

    theorem linearIndependent_of_projective_cover {Ī¹ : Type*} [Fintype Ī¹]
    [IsDomain A] [IsNoetherianRing A] [Module.Projective A M]
    (I : Ideal A) (hI : I ā‰  āŠ¤)
    (hscalar : āˆ€ a : A, āˆƒ c : k, a-algebraMap k A c āˆˆ I)
    (v : Ī¹ ā†’ M) (hspan : Submodule.span A (Set.range v) = āŠ¤)
    (hind : LinearIndependent k
      (fun i => (I ā€¢ (āŠ¤ : Submodule A M)).mkQ (v i))) :
    LinearIndependent A v := by
ā€¦
  7. theorem OAI.KLInvariance.Graded.quotient_span_of_scalar_mod line 245

    Source documentation

    Images of any finite generating family span the augmentation quotient as a vector space over the degree-zero field.

    theorem quotient_span_of_scalar_mod {Ī¹ : Type*} [Fintype Ī¹]
    (I : Ideal A) (hscalar : āˆ€ a : A, āˆƒ c : k, a-algebraMap k A c āˆˆ I)
    (v : Ī¹ ā†’ M) (hv : Submodule.span A (Set.range v) = āŠ¤) :
    Submodule.span k (Set.range (fun i => (I ā€¢ (āŠ¤ : Submodule A M)).mkQ (v i))) = āŠ¤ := by
ā€¦
  8. theorem OAI.KLInvariance.Graded.exists_homogeneous_basis_of_scalar_mod line 268
  9. def OAI.KLInvariance.Graded.nonnegativeAugmentation line 328

    Source documentation

    The augmentation for a nonnegatively supported integer grading is actual degree-zero projection.

    noncomputable def nonnegativeAugmentation
    (š“ : ā„¤ ā†’ Submodule k A) [DirectSum.Decomposition š“]
    [SetLike.GradedMonoid š“] (hneg : āˆ€ j < 0, š“ j = āŠ„) : A ā†’+* A where
ā€¦
  10. theorem OAI.KLInvariance.Graded.positiveIdeal_eq_augmentation_ker line 376

    Source documentation

    The positive ideal is exactly the augmentation kernel.

    theorem positiveIdeal_eq_augmentation_ker
    (š“ : ā„¤ ā†’ Submodule k A) [DirectSum.Decomposition š“]
    [SetLike.GradedMonoid š“] (hneg : āˆ€ j < 0, š“ j = āŠ„) :
    positiveIdeal š“ = RingHom.ker (nonnegativeAugmentation š“ hneg) := by
ā€¦

    Mentions: OAI.KLInvariance.Graded.positiveIdeal, OAI.KLInvariance.Graded.nonnegativeAugmentation

  11. theorem OAI.KLInvariance.Graded.exists_homogeneous_basis_connected line 400
  12. abbrev OAI.KLInvariance.Graded.polynomialGrading line 426

    Source documentation

    The actual polynomial grading, with each variable in degree one, on integer degrees as used for shifted stalks.

    abbrev polynomialGrading (k : Type*) [Field k] (Ļƒ : Type*) :=
ā€¦
  13. instance OAI.KLInvariance.Graded.polynomialGrading_decomposition line 429
  14. instance OAI.KLInvariance.Graded.polynomialGrading_monoid line 433
  15. theorem OAI.KLInvariance.Graded.polynomialGrading_negative line 437
  16. theorem OAI.KLInvariance.Graded.polynomialGrading_zero line 452
  17. theorem OAI.KLInvariance.Graded.exists_homogeneous_basis_polynomial line 472
  18. def OAI.KLInvariance.ReverseFiltration.scalarQuotientMap line 491
  19. theorem OAI.KLInvariance.ReverseFiltration.scalarQuotientMap_surjective line 498
  20. def OAI.KLInvariance.ReverseFiltration.scalarKernelMap line 507

    Source documentation

    Multiplication by the actual nonzero label identifies the kernel of coordinate reduction with a free module.

    def scalarKernelMap (a : A) (Ī¹ : Type ui) :
    (Ī¹ ā†’ A) ā†’ā‚—[A] LinearMap.ker (scalarQuotientMap a Ī¹) where
ā€¦

    Mentions: OAI.KLInvariance.ReverseFiltration.scalarQuotientMap

  21. theorem OAI.KLInvariance.ReverseFiltration.scalarKernelMap_bijective line 517
  22. theorem OAI.KLInvariance.ReverseFiltration.scalarKernel_projective line 531
  23. theorem OAI.KLInvariance.ReverseFiltration.exists_scalar_presentation line 538

    Source documentation

    Every finite free module over A/(a) has an actual free A-presentation with projective kernel; no projective-dimension hypothesis is inserted.

    theorem exists_scalar_presentation (a : A) (ha : aā‰ 0)
    (P : Type up) [AddCommGroup P] [Module A P]
    [Module (A ā§ø Ideal.span {a}) P] [IsScalarTower A (A ā§ø Ideal.span {a}) P]
    [Module.Free (A ā§ø Ideal.span {a}) P] [Module.Finite (A ā§ø Ideal.span {a}) P] :
    āˆƒ (Ī¹ : Type up), Finite Ī¹ āˆ§ āˆƒ g : (Ī¹ ā†’ A) ā†’ā‚—[A] P,
      Function.Surjective g āˆ§ Module.Projective A (LinearMap.ker g) := by
ā€¦
  24. theorem OAI.KLInvariance.ReverseFiltration.kernel_projective_of_free_scalar_quotient line 561

    Source documentation

    The reverse-filtration kernel is projective when the edge image is actually finite free over the hypersurface quotient.

    theorem kernel_projective_of_free_scalar_quotient
    (a : A) (ha : aā‰ 0) {F : Type*} [AddCommGroup F] [Module A F]
    [Module.Projective A F]
    {P : Type up} [AddCommGroup P] [Module A P]
    [Module (A ā§ø Ideal.span {a}) P] [IsScalarTower A (A ā§ø Ideal.span {a}) P]
    [Module.Free (A ā§ø Ideal.span {a}) P] [Module.Finite (A ā§ø Ideal.span {a}) P]
    (f : F ā†’ā‚—[A] P) (hf : Function.Surjective f) :
    Module.Projective A (LinearMap.ker f) := by
ā€¦
  25. theorem OAI.KLInvariance.Graded.exists_homogeneous_minimal_generators line 587
  26. theorem OAI.KLInvariance.Graded.kernel_minimal_cover line 641
  27. theorem OAI.KLInvariance.Graded.internal_of_components line 681
  28. theorem OAI.KLInvariance.Graded.image_isInternal line 705
  29. def OAI.KLInvariance.Graded.subPiece line 743
  30. theorem OAI.KLInvariance.Graded.sub_isInternal line 746
  31. def OAI.KLInvariance.Graded.quotientPiece line 771
  32. theorem OAI.KLInvariance.Graded.quotient_isInternal line 774
  33. instance OAI.KLInvariance.Graded.sub_gradedSMul line 784
  34. instance OAI.KLInvariance.Graded.quotient_gradedSMul line 793
  35. theorem OAI.KLInvariance.Graded.subPiece_eq_bot line 802
  36. theorem OAI.KLInvariance.Graded.quotientPiece_eq_bot line 809
  37. def OAI.KLInvariance.Graded.shiftedPiece line 813
  38. theorem OAI.KLInvariance.Graded.shifted_isInternal line 820
  39. instance OAI.KLInvariance.Graded.shifted_gradedSMul line 859
  40. theorem OAI.KLInvariance.Graded.shiftedPiece_eq_bot line 867
  41. theorem OAI.KLInvariance.Graded.map_component line 891
  42. theorem OAI.KLInvariance.Graded.kernel_homogeneous line 916
  43. theorem OAI.KLInvariance.Graded.range_homogeneous line 928
  44. theorem OAI.KLInvariance.Graded.component_homogeneous_smul line 938
  45. theorem OAI.KLInvariance.Graded.scalar_range_homogeneous line 948
  46. theorem OAI.KLInvariance.Graded.exists_graded_minimal_free_cover line 958
  47. def OAI.KLInvariance.Graded.piPiece line 987
  48. theorem OAI.KLInvariance.Graded.pi_isInternal line 990
  49. instance OAI.KLInvariance.Graded.pi_gradedSMul line 1020
  50. theorem OAI.KLInvariance.Graded.piPiece_eq_bot line 1027
  51. structure OAI.KLInvariance.Graded.ModuleData line 1051

    Source documentation

    Actual finite nonnegatively graded modules; no character or duality property is folded into this data.

    structure ModuleData (š“ : ā„¤ ā†’ Submodule k A) where
ā€¦
  52. instance OAI.KLInvariance.Graded.(instance at line 1064) line 1064
  53. instance OAI.KLInvariance.Graded.ModuleData.(instance at line 1070) line 1070
  54. instance OAI.KLInvariance.Graded.ModuleData.(instance at line 1071) line 1071
  55. structure OAI.KLInvariance.Graded.ModuleData.Hom line 1073
  56. def OAI.KLInvariance.Graded.ModuleData.sub line 1077
  57. def OAI.KLInvariance.Graded.ModuleData.quotient line 1089
  58. def OAI.KLInvariance.Graded.ModuleData.pi line 1101
  59. def OAI.KLInvariance.Graded.ModuleData.kernel line 1112
  60. def OAI.KLInvariance.Graded.ModuleData.range line 1117
  61. def OAI.KLInvariance.Graded.ModuleData.scalarQuotient line 1122
  62. def OAI.KLInvariance.Graded.ModuleData.projection line 1127
  63. def OAI.KLInvariance.Graded.ModuleData.quotientMap line 1132
  64. def OAI.KLInvariance.Graded.ModuleData.subtype line 1141
  65. def OAI.KLInvariance.Graded.ModuleData.Hom.comp line 1148
  66. def OAI.KLInvariance.Graded.ModuleData.Hom.id line 1153
  67. theorem OAI.KLInvariance.Graded.ModuleData.Hom.component line 1157
  68. def OAI.KLInvariance.Graded.ModuleData.free line 1163
  69. structure OAI.KLInvariance.Graded.ModuleData.MinimalCover line 1175
  70. theorem OAI.KLInvariance.Graded.ModuleData.exists_minimalCover line 1182
  71. theorem OAI.KLInvariance.Graded.shift_isInternal line 1226
  72. def OAI.KLInvariance.Graded.ModuleData.shift line 1244
  73. def OAI.KLInvariance.Graded.ModuleData.Hom.shift line 1260
  74. def OAI.KLInvariance.Graded.ModuleData.prod line 1265
  75. def OAI.KLInvariance.Graded.ModuleData.Hom.prodMap line 1306
  76. theorem OAI.KLInvariance.Graded.ModuleData.Hom.mem_of_map_mem line 1327
  77. theorem OAI.KLInvariance.Graded.ModuleData.Hom.homogeneous_preimage line 1336
  78. theorem OAI.KLInvariance.Graded.ModuleData.exists_hom_lift_of_basis line 1348
  79. theorem OAI.KLInvariance.Graded.ModuleData.exists_hom_lift line 1397
  80. theorem OAI.KLInvariance.Graded.ModuleData.Hom.bijective_of_mod_positive line 1408
  81. theorem OAI.KLInvariance.Graded.ModuleData.MinimalCover.equiv line 1422