NYLL
Module

ProjSpaceCech_GradedModule_subsingleton_cohomology_shift_of_isFG.lean

Nyll.AlgebraicCurves.Cohomology.Cech.ProjSpaceCech_GradedModule_subsingleton_cohomology_shift_of_isFG
9 declarations indexed from sourceView source ↗

Module documentation

Proj Space Cech Graded Module subsingleton cohomology shift of is FG

Imports8
Imported by3

Declarations

theorem

subsingleton_H_pi_FD

L49 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_subsingleton_cohomology_shift_of_isFG.ProjSpaceCech.GradedModule.subsingleton_H_pi_FD
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_GradedModule_subsingleton_cohomology_shift_of_isFG
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section SerreVanishing
variable {R : Type u} [CommRing R] {n : ℕ}
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · full declaration
theorem GradedModule.subsingleton_H_pi_FD {ι : Type} [Fintype ι] (e : ι → ℤ) {i : ℕ} (hi : 1 ≤ i)
    (he : ∀ k, -(n : ℤ) ≤ e k) :
    Subsingleton (GradedModule.H (GradedModule.pi (fun k => GradedModule.FD R n (e k))) i) := by
  obtain ⟨epi⟩ := GradedModule.nonempty_HEquiv_pi (fun k => GradedModule.FD R n (e k)) i
  have : ∀ k, Subsingleton (GradedModule.H (GradedModule.FD R n (e k)) i) := fun k => by
    obtain ⟨eFD⟩ := GradedModule.nonempty_HEquiv_FD R n (e k) i
    have := Twist.subsingleton_cohomology_of_neg_le R n (he k) hi
    exact eFD.symm.toEquiv.subsingleton
  exact epi.toEquiv.subsingleton
def

shiftP

L68 ↗
ProjSpaceCech.GradedModule.Presentation.shiftP
Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_GradedModule_subsingleton_cohomology_shift_of_isFG
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section SerreVanishing
variable {R : Type u} [CommRing R] {n : ℕ}
variable {M : GradedModule R n}
namespace GradedModule.Presentation
open scoped _root_.ProjSpaceCech.GradedModule _root_.ProjSpaceCech.GradedModule.Presentation in
Lean source · full declaration
def _root_.ProjSpaceCech.GradedModule.Presentation.shiftP (σ : GradedModule.Presentation M)
  (d : ℤ) :
    GradedModule.Presentation (GradedModule.shift M d) where
  J := σ.J
  d₀ := fun k => σ.d₀ k + d
  hom :=
    { toLinearMap := σ.hom.toLinearMap
      mem_grade := fun c m hm => by
        change σ.hom.toLinearMap m ∈ M.grade (c + d)
        refine σ.hom.mem_grade (c + d) m ?_
        intro k hk
        have h := hm k hk
        change m k ∈ GradedModule.freeGrade R n (c + (σ.d₀ k + d)) at h
        change m k ∈ GradedModule.freeGrade R n (c + d + σ.d₀ k)
        rwa [show c + d + σ.d₀ k = c + (σ.d₀ k + d) by ring]
      xMul_comm := fun j => LinearMap.ext fun m => LinearMap.congr_fun (σ.hom.xMul_comm j) m }
  surj := fun c m hm => by
    obtain ⟨m', hm', h⟩ := σ.surj (c + d) m hm
    refine ⟨m', fun k hk => ?_, h⟩
    have h' := hm' k hk
    change m' k ∈ GradedModule.freeGrade R n (c + d + σ.d₀ k) at h'
    change m' k ∈ GradedModule.freeGrade R n (c + (σ.d₀ k + d))
    rwa [show c + (σ.d₀ k + d) = c + d + σ.d₀ k by ring]
def

kerToShift

L96 ↗
ProjSpaceCech.GradedModule.Presentation.kerToShift
Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_GradedModule_subsingleton_cohomology_shift_of_isFG
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section SerreVanishing
variable {R : Type u} [CommRing R] {n : ℕ}
variable {M : GradedModule R n}
open _root_.ProjSpaceCech
namespace GradedModule.Presentation
open scoped _root_.ProjSpaceCech.GradedModule _root_.ProjSpaceCech.GradedModule.Presentation in
Lean source · full declaration
def _root_.ProjSpaceCech.GradedModule.Presentation.kerToShift (σ :
  GradedModule.Presentation M) (d : ℤ) :
    GradedModule.Hom (GradedModule.Presentation.ker (σ.shiftP d)) (GradedModule.shift σ.ker d) where
  toLinearMap := LinearMap.id
  mem_grade := fun c m hm => by
    refine ⟨fun k hk => ?_, hm.2⟩
    have h := hm.1 k hk
    change m k ∈ GradedModule.freeGrade R n (c + (σ.d₀ k + d)) at h
    change m k ∈ GradedModule.freeGrade R n (c + d + σ.d₀ k)
    rwa [show c + d + σ.d₀ k = c + (σ.d₀ k + d) by ring]
  xMul_comm := fun _ => rfl
def

shiftToKer

L112 ↗
ProjSpaceCech.GradedModule.Presentation.shiftToKer
Source context 16 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_GradedModule_subsingleton_cohomology_shift_of_isFG
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section SerreVanishing
variable {R : Type u} [CommRing R] {n : ℕ}
variable {M : GradedModule R n}
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
namespace GradedModule.Presentation
open scoped _root_.ProjSpaceCech.GradedModule _root_.ProjSpaceCech.GradedModule.Presentation in
Lean source · full declaration
def _root_.ProjSpaceCech.GradedModule.Presentation.shiftToKer (σ :
  GradedModule.Presentation M) (d : ℤ) :
    GradedModule.Hom (GradedModule.shift σ.ker d) (GradedModule.Presentation.ker (σ.shiftP d)) where
  toLinearMap := LinearMap.id
  mem_grade := fun c m hm => by
    refine ⟨fun k hk => ?_, hm.2⟩
    have h := hm.1 k hk
    change m k ∈ GradedModule.freeGrade R n (c + d + σ.d₀ k) at h
    change m k ∈ GradedModule.freeGrade R n (c + (σ.d₀ k + d))
    rwa [show c + (σ.d₀ k + d) = c + d + σ.d₀ k by ring]
  xMul_comm := fun _ => rfl
theorem

secMap_shiftToKer_kerToShift

L127 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_subsingleton_cohomology_shift_of_isFG.ProjSpaceCech.GradedModule.Presentation.secMap_shiftToKer_kerToShift
Source context 16 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_GradedModule_subsingleton_cohomology_shift_of_isFG
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section SerreVanishing
variable {R : Type u} [CommRing R] {n : ℕ}
variable {M : GradedModule R n}
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
open scoped _root_.ProjSpaceCech.GradedModule _root_.ProjSpaceCech.GradedModule.Presentation in
Lean source · statement
theorem GradedModule.Presentation.secMap_shiftToKer_kerToShift (σ : GradedModule.Presentation M) (d
  : ℤ)
    (I : Finset (Fin (n + 1))) (q : GradedModule.sec (GradedModule.Presentation.ker (σ.shiftP d))
      I) :
    GradedModule.Hom.secMap (σ.shiftToKer d) I (GradedModule.Hom.secMap (σ.kerToShift d) I q) = q
theorem

secMap_kerToShift_shiftToKer

L136 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_subsingleton_cohomology_shift_of_isFG.ProjSpaceCech.GradedModule.Presentation.secMap_kerToShift_shiftToKer
Source context 16 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_GradedModule_subsingleton_cohomology_shift_of_isFG
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section SerreVanishing
variable {R : Type u} [CommRing R] {n : ℕ}
variable {M : GradedModule R n}
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
open scoped _root_.ProjSpaceCech.GradedModule _root_.ProjSpaceCech.GradedModule.Presentation in
Lean source · statement
theorem GradedModule.Presentation.secMap_kerToShift_shiftToKer (σ : GradedModule.Presentation M) (d
  : ℤ)
    (I : Finset (Fin (n + 1))) (q : GradedModule.sec (GradedModule.shift σ.ker d) I) :
    GradedModule.Hom.secMap (σ.kerToShift d) I (GradedModule.Hom.secMap (σ.shiftToKer d) I q) = q
theorem

cochainMap_kerToShift_bijective

L144 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_subsingleton_cohomology_shift_of_isFG.ProjSpaceCech.GradedModule.Presentation.cochainMap_kerToShift_bijective
Source context 16 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_GradedModule_subsingleton_cohomology_shift_of_isFG
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section SerreVanishing
variable {R : Type u} [CommRing R] {n : ℕ}
variable {M : GradedModule R n}
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
open scoped _root_.ProjSpaceCech.GradedModule _root_.ProjSpaceCech.GradedModule.Presentation in
Lean source · statement
theorem GradedModule.Presentation.cochainMap_kerToShift_bijective (σ : GradedModule.Presentation M)
  (d : ℤ)
    (i : ℕ) : Function.Bijective (GradedModule.Hom.cochainMap (σ.kerToShift d) i)
theorem

subsingleton_cohomology_shift_of_isFG'

L155 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_subsingleton_cohomology_shift_of_isFG.ProjSpaceCech.GradedModule.subsingleton_cohomology_shift_of_isFG'
Source context 16 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_GradedModule_subsingleton_cohomology_shift_of_isFG
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section SerreVanishing
variable {R : Type u} [CommRing R] {n : ℕ}
variable {M : GradedModule R n}
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.subsingleton_cohomology_shift_of_isFG' [IsNoetherianRing R]
    (M : GradedModule R n) (hM : GradedModule.IsFG M) :
    ∃ d₀ : ℤ, ∀ d, d₀ ≤ d → ∀ i, 1 ≤ i →
      Subsingleton (GradedModule.H (GradedModule.shift M d) i)
theorem

subsingleton_cohomology_shift_of_isFG

L210 ↗
ProjSpaceCech.GradedModule.subsingleton_cohomology_shift_of_isFG
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_GradedModule_subsingleton_cohomology_shift_of_isFG
universe u
noncomputable section
open Finset Function MvPolynomial
Lean source · statement
theorem _root_.ProjSpaceCech.GradedModule.subsingleton_cohomology_shift_of_isFG {R : Type u}
  [CommRing R] [IsNoetherianRing R] {n : ℕ}
    (M : ProjSpaceCech.GradedModule R n) (hM : ProjSpaceCech.GradedModule.IsFG M) :
    ∃ d₀ : ℤ, ∀ d, d₀ ≤ d → ∀ i, 1 ≤ i → Subsingleton (ProjSpaceCech.GradedModule.H
      (ProjSpaceCech.GradedModule.shift M d) i)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.