Documentation

TauCeti.Algebra.Category.GradedModuleCat.Free

Graded free modules and projective presentations #

A free graded module with basis degrees d : I β†’ β„€ is the direct sum of copies of the regular module using the internal grading shift -d i, equivalently the categorical shift shiftObj (d i), so basis vector i has degree d i. Its degree-p elements have coordinate i in π’œ (p - d i). Maps out of it are uniquely determined by the images of its homogeneous basis vectors.

Every graded module is a quotient of such a free graded module: use all homogeneous elements as generators. If the underlying module is finitely generated, finitely many homogeneous elements suffice, so the free source can be chosen finitely generated. These presentations provide the projective terms needed to construct graded resolutions; they do not assert minimality. Over a left Noetherian algebra, the kernel is again finitely generated, giving a two-term presentation by finite graded free modules.

No positivity, semisimplicity, or finite-dimensionality assumption on the graded algebra is needed.

References #

The construction uses InternalGrading.directSum and Mathlib's direct-sum universal property. The free object is an abbreviation with a concrete carrier. Its computation lemmas normalize projections with dsimp% only so that they still match after the simplifier reduces that carrier.

source
@[reducible, inline]
noncomputable abbrev TauCeti.GradedModuleCat.free {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (π’œ : β„€ β†’ Submodule k A) [GradedAlgebra π’œ] {I : Type uI} (d : I β†’ β„€) :
GradedModuleCat π’œ

The free graded module with basis indexed by I and basis vector i in degree d i. The abbreviation retains the concrete direct-sum carrier for computations with generators.

Equations
Instances For
    source
    theorem TauCeti.GradedModuleCat.mem_free_piece_iff {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (π’œ : β„€ β†’ Submodule k A) [GradedAlgebra π’œ] {I : Type uI} (d : I β†’ β„€) (p : β„€) (x : (free π’œ d).carrier) :
    x ∈ (InternalGrading.directSum fun (j : I) => (InternalGrading.ofDecomposition π’œ).shift (-d j)).piece p ↔ βˆ€ (i : I), x i ∈ π’œ (p - d i)

    x lies in the degree-p piece exactly when its i-th coordinate lies in π’œ (p - d i). This is not a simp lemma: the direct-sum and shift simp lemmas already simplify its left side.

    source
    noncomputable def TauCeti.GradedModuleCat.freeGenerator {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] {I : Type uI} {d : I β†’ β„€} (i : I) :
    (free π’œ d).carrier

    The homogeneous basis vector indexed by i.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.GradedModuleCat.freeGenerator_apply {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] {I : Type uI} {d : I β†’ β„€} [DecidableEq I] (i j : I) :
      (freeGenerator i) j = if i = j then 1 else 0

      The coordinates of a homogeneous basis vector.

      source
      theorem TauCeti.GradedModuleCat.freeGenerator_eq_lof {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] {I : Type uI} {d : I β†’ β„€} [DecidableEq I] (i : I) :
      freeGenerator i = (DirectSum.lof A I (fun (x : I) => A) i) 1

      The homogeneous basis vector is the canonical inclusion of 1 from its summand.

      source
      theorem TauCeti.GradedModuleCat.freeGenerator_mem_free_piece {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] {I : Type uI} {d : I β†’ β„€} (i : I) :
      freeGenerator i ∈ (free π’œ d).grading.piece (d i)

      The basis vector indexed by i has internal degree d i.

      source
      noncomputable def TauCeti.GradedModuleCat.freeLift {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] {I : Type uI} {d : I β†’ β„€} {M : GradedModuleCat π’œ} (x : (i : I) β†’ β†₯(M.grading.piece (d i))) :
      free π’œ d ⟢ M

      Extend a family of homogeneous elements to a morphism out of the graded free module.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.GradedModuleCat.hom_freeLift {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] {I : Type uI} {d : I β†’ β„€} {M : GradedModuleCat π’œ} (x : (i : I) β†’ β†₯(M.grading.piece (d i))) [hI : DecidableEq I] :
        (freeLift x).hom = DirectSum.toModule A I M.carrier fun (i : I) => LinearMap.toSpanSingleton A M.carrier ↑(x i)

        The underlying linear map of extension is the direct-sum universal map.

        source
        theorem TauCeti.GradedModuleCat.freeLift_lof {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] {I : Type uI} {d : I β†’ β„€} {M : GradedModuleCat π’œ} (x : (i : I) β†’ β†₯(M.grading.piece (d i))) [hI : DecidableEq I] (i : I) (a : A) :
        (freeLift x).hom ((DirectSum.lof A I (fun (x : I) => A) i) a) = a β€’ ↑(x i)

        Extension on a summand is scalar multiplication by its prescribed basis image.

        source
        @[simp]
        theorem TauCeti.GradedModuleCat.freeLift_generator {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] {I : Type uI} {d : I β†’ β„€} {M : GradedModuleCat π’œ} (x : (i : I) β†’ β†₯(M.grading.piece (d i))) (i : I) :
        (freeLift x).hom (freeGenerator i) = ↑(x i)

        The extension evaluates to the prescribed image on each basis vector.

        source
        theorem TauCeti.GradedModuleCat.free_hom_ext {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] {I : Type uI} {d : I β†’ β„€} {M : GradedModuleCat π’œ} {f g : free π’œ d ⟢ M} (h : βˆ€ (i : I), f.hom (freeGenerator i) = g.hom (freeGenerator i)) :
        f = g

        Morphisms out of a free graded module agree if they agree on its homogeneous basis.

        source
        theorem TauCeti.GradedModuleCat.free_hom_ext_iff {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] {I : Type uI} {d : I β†’ β„€} {M : GradedModuleCat π’œ} {f g : free π’œ d ⟢ M} :
        f = g ↔ βˆ€ (i : I), f.hom (freeGenerator i) = g.hom (freeGenerator i)
        source
        @[simp]
        theorem TauCeti.GradedModuleCat.freeLift_comp {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] {I : Type uI} {d : I β†’ β„€} {M N : GradedModuleCat π’œ} (x : (i : I) β†’ β†₯(M.grading.piece (d i))) (g : M ⟢ N) :
        CategoryTheory.CategoryStruct.comp (freeLift x) g = freeLift fun (i : I) => ⟨g.hom ↑(x i), β‹―βŸ©

        Postcomposing extension extends the postcomposed homogeneous basis images.

        source
        noncomputable def TauCeti.GradedModuleCat.freeHomEquiv {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] {I : Type uI} {d : I β†’ β„€} (M : GradedModuleCat π’œ) :
        (free π’œ d ⟢ M) ≃ₗ[k] (i : I) β†’ β†₯(M.grading.piece (d i))

        The linear universal property: maps from a graded free module are families of elements in its specified basis degrees.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem TauCeti.GradedModuleCat.freeHomEquiv_apply_coe {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] {I : Type uI} {d : I β†’ β„€} (M : GradedModuleCat π’œ) (f : free π’œ d ⟢ M) (i : I) :
          ↑(M.freeHomEquiv f i) = f.hom (freeGenerator i)

          The free-module universal property reads off the basis images.

          source
          @[simp]
          theorem TauCeti.GradedModuleCat.freeHomEquiv_symm_apply {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] {I : Type uI} {d : I β†’ β„€} (M : GradedModuleCat π’œ) (x : (i : I) β†’ β†₯(M.grading.piece (d i))) :
          M.freeHomEquiv.symm x = freeLift x

          The inverse universal-property map is extension from the basis images.

          Presentations #

          source
          theorem TauCeti.GradedModuleCat.freeLift_surjective_iff {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] {I : Type uI} {d : I β†’ β„€} {M : GradedModuleCat π’œ} (x : (i : I) β†’ β†₯(M.grading.piece (d i))) :
          Function.Surjective ⇑(freeLift x).hom ↔ Submodule.span A (Set.range fun (i : I) => ↑(x i)) = ⊀

          A graded free map is surjective exactly when its homogeneous basis images generate.

          source
          instance TauCeti.GradedModuleCat.enoughProjectives {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] :
          CategoryTheory.EnoughProjectives (GradedModuleCat π’œ)

          Every graded module admits a projective presentation by a graded free module.

          source
          theorem TauCeti.GradedModuleCat.exists_finite_free_surjection {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] (M : GradedModuleCat π’œ) [Module.Finite A M.carrier] :
          βˆƒ (I : Type (max uA v)) (_ : Finite I) (d : I β†’ β„€) (f : free π’œ d ⟢ M), Function.Surjective ⇑f.hom

          A finitely generated graded module admits a surjection from a finitely generated graded free module. The homogeneous generating set, and hence the free presentation, need not be minimal.

          source
          theorem TauCeti.GradedModuleCat.exists_finite_free_presentation {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] [IsNoetherianRing A] (M : GradedModuleCat π’œ) [Module.Finite A M.carrier] :
          βˆƒ (I : Type (max uA v)) (J : Type (max uA v)) (_ : Finite I) (_ : Finite J) (d : I β†’ β„€) (e : J β†’ β„€) (g : free π’œ e ⟢ free π’œ d) (f : free π’œ d ⟢ M), Function.Exact ⇑g.hom ⇑f.hom ∧ Function.Surjective ⇑f.hom

          Over a left Noetherian algebra, a finitely generated graded module admits a two-term presentation by finite graded free modules. Both maps preserve the internal grading.