Documentation

TauCeti.Algebra.Category.GradedModuleCat.MinimalResolution

Ext from minimal graded resolutions #

For a minimal graded projective resolution, every differential has image in the positive-degree algebra action. Against a target annihilated by that action, the Hom complex has zero differentials. Its terms therefore compute Ext in every degree, including degree zero.

GradedProjectiveResolution.IsMinimal.extLinearEquiv identifies graded Hom from the nth resolution term with Extⁿ. The vanishing characterization converts diagonal Ext vanishing into vanishing of graded Hom, without assuming the resolution is linear. The equivalence is natural in the target. Neither nonnegative grading nor semisimplicity is needed for this computation; those hypotheses enter when detecting generating degrees or constructing minimal resolutions.

GradedProjectiveResolution.exists_isMinimal_of_forall_cover assembles a minimal resolution from any supply of minimal projective surjections that is stable under passing to kernels.

References #

source
@[simp]
theorem TauCeti.GradedProjectiveResolution.IsMinimal.differential_comp_eq_zero {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} {r : GradedProjectiveResolution 𝒜 M.grading} (hr : r.IsMinimal) (hN : (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤ = ⊥) (n : ℕ) (f : r.termObj n ⟶ N) :
CategoryTheory.CategoryStruct.comp (r.differential n) f = 0

Every differential of a minimal resolution dies after mapping to a target annihilated by positive-degree scalars.

source
@[simp]
theorem TauCeti.GradedProjectiveResolution.IsMinimal.differential_comp_eq_zero_assoc {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} {r : GradedProjectiveResolution 𝒜 M.grading} (hr : r.IsMinimal) (hN : (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤ = ⊥) (n : ℕ) (f : r.termObj n ⟶ N) {Z : GradedModuleCat 𝒜} (h : N ⟶ Z) :
CategoryTheory.CategoryStruct.comp (r.differential n) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp 0 h

Every differential of a minimal resolution dies after mapping to a target annihilated by positive-degree scalars.

source
noncomputable def TauCeti.GradedProjectiveResolution.IsMinimal.augmentationLinearEquiv {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} {r : GradedProjectiveResolution 𝒜 M.grading} (hr : r.IsMinimal) (hN : (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤ = ⊥) :
(M ⟶ N) ≃ₗ[k] r.termObj 0 ⟶ N

Precomposition with the augmentation of a minimal resolution is an equivalence for a positive-action-annihilated target. This also explains the degree-zero Ext computation.

Instances For
    source
    @[simp]
    theorem TauCeti.GradedProjectiveResolution.IsMinimal.augmentationLinearEquiv_apply {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} {r : GradedProjectiveResolution 𝒜 M.grading} (hr : r.IsMinimal) (hN : (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤ = ⊥) (f : M ⟶ N) :
    (hr.augmentationLinearEquiv hN) f = CategoryTheory.CategoryStruct.comp r.augmentation f

    The augmentation equivalence is precomposition with the original augmentation.

    source
    theorem TauCeti.GradedProjectiveResolution.exists_isMinimal_of_forall_cover {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (S T : GradedModuleCat 𝒜 → Prop) (hcover : ∀ (N : GradedModuleCat 𝒜), S N → ∃ (P : GradedModuleCat 𝒜) (π : P ⟶ N), Module.Projective A P.carrier ∧ Function.Surjective ⇑π.hom ∧ (∀ (x : P.carrier), π.hom x = 0 → x ∈ (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤) ∧ T P ∧ S (GradedModuleCat.kernelObj π)) (M : GradedModuleCat 𝒜) (hM : S M) :
    ∃ (r : GradedProjectiveResolution 𝒜 M.grading), r.IsMinimal ∧ ∀ (n : ℕ), T (r.termObj n)

    Iterating minimal projective surjections along successive kernels gives a minimal resolution. Suppose every graded module satisfying S is the target of a projective surjection whose kernel lies in the positive-degree action on the source, whose source satisfies T, and whose kernel again satisfies S. Then every graded module satisfying S has a minimal graded projective resolution all of whose terms satisfy T.

    source
    noncomputable def TauCeti.GradedProjectiveResolution.IsMinimal.extLinearEquiv {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} {r : GradedProjectiveResolution 𝒜 M.grading} [DirectSum.Decomposition 𝒜] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] (hr : r.IsMinimal) (hN : (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤ = ⊥) (n : ℕ) :
    (r.termObj n ⟶ N) ≃ₗ[k] CategoryTheory.Abelian.Ext M N n

    A minimal resolution computes Ext as graded Hom from its terms whenever positive-degree scalars annihilate the target. The statement includes degree zero.

    Instances For
      source
      @[simp]
      theorem TauCeti.GradedProjectiveResolution.IsMinimal.extLinearEquiv_zero_augmentation_comp {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} {r : GradedProjectiveResolution 𝒜 M.grading} [DirectSum.Decomposition 𝒜] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] (hr : r.IsMinimal) (hN : (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤ = ⊥) (f : M ⟶ N) :
      (hr.extLinearEquiv hN 0) (CategoryTheory.CategoryStruct.comp r.augmentation f) = CategoryTheory.Abelian.Ext.mk₀ f

      In degree zero, a map pulled back along the augmentation represents the ordinary Hom class.

      source
      @[simp]
      theorem TauCeti.GradedProjectiveResolution.IsMinimal.augmentation_comp_linearEquiv₀_extLinearEquiv {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} {r : GradedProjectiveResolution 𝒜 M.grading} [DirectSum.Decomposition 𝒜] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] (hr : r.IsMinimal) (hN : (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤ = ⊥) (f : r.termObj 0 ⟶ N) :
      CategoryTheory.CategoryStruct.comp r.augmentation (CategoryTheory.Abelian.Ext.linearEquiv₀ ((hr.extLinearEquiv hN 0) f)) = f

      The degree-zero equivalence descends a map through the augmentation.

      source
      @[simp]
      theorem TauCeti.GradedProjectiveResolution.IsMinimal.augmentation_comp_linearEquiv₀_extLinearEquiv_assoc {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} {r : GradedProjectiveResolution 𝒜 M.grading} [DirectSum.Decomposition 𝒜] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] (hr : r.IsMinimal) (hN : (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤ = ⊥) (f : r.termObj 0 ⟶ N) {Z : GradedModuleCat 𝒜} (h : N ⟶ Z) :
      CategoryTheory.CategoryStruct.comp r.augmentation (CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.Ext.linearEquiv₀ ((hr.extLinearEquiv hN 0) f)) h) = CategoryTheory.CategoryStruct.comp f h

      The degree-zero equivalence descends a map through the augmentation.

      source
      @[simp]
      theorem TauCeti.GradedProjectiveResolution.IsMinimal.extLinearEquiv_succ_apply {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} {r : GradedProjectiveResolution 𝒜 M.grading} [DirectSum.Decomposition 𝒜] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] (hr : r.IsMinimal) (hN : (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤ = ⊥) (n : ℕ) (f : r.termObj (n + 1) ⟶ N) :
      (hr.extLinearEquiv hN (n + 1)) f = r.toProjectiveResolution.extMk (CategoryTheory.CategoryStruct.comp (r.toProjectiveResolutionXIso (n + 1)).hom f) (n + 2) ⋯ ⋯

      In positive degree the equivalence sends a graded map to its projective-resolution class.

      source
      theorem TauCeti.GradedProjectiveResolution.IsMinimal.subsingleton_ext_iff {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} {r : GradedProjectiveResolution 𝒜 M.grading} [DirectSum.Decomposition 𝒜] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] (hr : r.IsMinimal) (hN : (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤ = ⊥) (n : ℕ) :
      Subsingleton (CategoryTheory.Abelian.Ext M N n) ↔ Subsingleton (r.termObj n ⟶ N)

      Ext against an annihilated target vanishes exactly when graded Hom from the corresponding term of the minimal resolution vanishes.

      source
      theorem TauCeti.GradedProjectiveResolution.IsMinimal.extLinearEquiv_comp {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N N' : GradedModuleCat 𝒜} {r : GradedProjectiveResolution 𝒜 M.grading} [DirectSum.Decomposition 𝒜] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] (hr : r.IsMinimal) (hN : (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤ = ⊥) (hN' : (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤ = ⊥) (n : ℕ) (f : r.termObj n ⟶ N) (g : N ⟶ N') :
      (hr.extLinearEquiv hN' n) (CategoryTheory.CategoryStruct.comp f g) = ((hr.extLinearEquiv hN n) f).comp (CategoryTheory.Abelian.Ext.mk₀ g) ⋯

      The minimal-resolution Ext computation is natural under maps between targets annihilated by positive-degree scalars.