NYLL
Module

ProjSpaceCech_GradedModule_Presentation_ker_isFG.lean

Nyll.SchemeTheory.Cohomology.Cech.ProjSpaceCech_GradedModule_Presentation_ker_isFG
16 declarations indexed from sourceView source ↗

Module documentation

Finite generation of the kernel of a graded module presentation over a noetherian base.

Imports4
Imported by4

Declarations

instance

F_module

L47 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG.ProjSpaceCech.GradedModule.F_module
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section KerFG
variable {R : Type u} [CommRing R] {n : ℕ} {D : GradedModule R n}
variable (σ : GradedModule.Presentation D)
local notation "S" => MvPolynomial (Fin (n + 1)) R
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
instance GradedModule.F_module : Module S σ.F.M
instance

F_scalarTower

L51 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG.ProjSpaceCech.GradedModule.F_scalarTower
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section KerFG
variable {R : Type u} [CommRing R] {n : ℕ} {D : GradedModule R n}
variable (σ : GradedModule.Presentation D)
local notation "S" => MvPolynomial (Fin (n + 1)) R
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
instance GradedModule.F_scalarTower : IsScalarTower R S σ.F.M
instance

FD_module

L55 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG.ProjSpaceCech.GradedModule.FD_module
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section KerFG
variable {R : Type u} [CommRing R] {n : ℕ} {D : GradedModule R n}
variable (σ : GradedModule.Presentation D)
local notation "S" => MvPolynomial (Fin (n + 1)) R
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
instance GradedModule.FD_module (d : ℤ) : Module S (GradedModule.FD R n d).M
instance

ker_module

L59 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG.ProjSpaceCech.GradedModule.ker_module
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section KerFG
variable {R : Type u} [CommRing R] {n : ℕ} {D : GradedModule R n}
variable (σ : GradedModule.Presentation D)
local notation "S" => MvPolynomial (Fin (n + 1)) R
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
instance GradedModule.ker_module : Module S σ.ker.M
theorem

F_xMul_eq_smul

L63 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG.ProjSpaceCech.GradedModule.F_xMul_eq_smul
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section KerFG
variable {R : Type u} [CommRing R] {n : ℕ} {D : GradedModule R n}
variable (σ : GradedModule.Presentation D)
local notation "S" => MvPolynomial (Fin (n + 1)) R
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.F_xMul_eq_smul (j : Fin (n + 1)) (m : σ.F.M) :
    σ.F.xMul j m = (X j : S) • m
abbrev

Kgr

L69 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG.ProjSpaceCech.GradedModule.Kgr
Documentation

The sum of the homogeneous components of the presentation kernel.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section KerFG
variable {R : Type u} [CommRing R] {n : ℕ} {D : GradedModule R n}
variable (σ : GradedModule.Presentation D)
local notation "S" => MvPolynomial (Fin (n + 1)) R
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
abbrev GradedModule.Kgr : Submodule R σ.F.M
theorem

Kgr_xMul_stable

L73 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG.ProjSpaceCech.GradedModule.Kgr_xMul_stable
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section KerFG
variable {R : Type u} [CommRing R] {n : ℕ} {D : GradedModule R n}
variable (σ : GradedModule.Presentation D)
local notation "S" => MvPolynomial (Fin (n + 1)) R
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.Kgr_xMul_stable (j : Fin (n + 1)) :
    ∀ m ∈ GradedModule.Kgr σ, σ.F.xMul j m ∈ GradedModule.Kgr σ
def

KgrS

L84 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG.ProjSpaceCech.GradedModule.KgrS
Documentation

The homogeneous presentation kernel as a submodule over the polynomial ring.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section KerFG
variable {R : Type u} [CommRing R] {n : ℕ} {D : GradedModule R n}
variable (σ : GradedModule.Presentation D)
local notation "S" => MvPolynomial (Fin (n + 1)) R
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · full declaration
def GradedModule.KgrS : Submodule S σ.F.M where
  carrier := GradedModule.Kgr σ
  add_mem' := Submodule.add_mem _
  zero_mem' := Submodule.zero_mem _
  smul_mem' := fun p m hm => by
    induction p using MvPolynomial.induction_on with
    | C r =>
      have : (C r : S) • m = r • m := by
        funext k; exact MvPolynomial.C_mul'
      rw [this]; exact Submodule.smul_mem _ r hm
    | add p q hp hq =>
      rw [add_smul]; exact Submodule.add_mem _ hp hq
    | mul_X p j hp =>
      rw [mul_comm, mul_smul, ← GradedModule.F_xMul_eq_smul σ j]
      exact GradedModule.Kgr_xMul_stable σ j _ hp
theorem

mem_F_grade

L101 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG.ProjSpaceCech.GradedModule.mem_F_grade
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section KerFG
variable {R : Type u} [CommRing R] {n : ℕ} {D : GradedModule R n}
variable (σ : GradedModule.Presentation D)
local notation "S" => MvPolynomial (Fin (n + 1)) R
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.mem_F_grade (d : ℤ) (m : σ.F.M) :
    m ∈ σ.F.grade d ↔ ∀ k, m k ∈ GradedModule.freeGrade R n (d + σ.d₀ k)
theorem

K_smul_stable

L106 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG.ProjSpaceCech.GradedModule.K_smul_stable
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section KerFG
variable {R : Type u} [CommRing R] {n : ℕ} {D : GradedModule R n}
variable (σ : GradedModule.Presentation D)
local notation "S" => MvPolynomial (Fin (n + 1)) R
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.K_smul_stable (c : S) : ∀ m ∈ σ.K, c • m ∈ σ.K
theorem

freeGrade_smul_mem_grade

L118 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG.ProjSpaceCech.GradedModule.freeGrade_smul_mem_grade
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section KerFG
variable {R : Type u} [CommRing R] {n : ℕ} {D : GradedModule R n}
variable (σ : GradedModule.Presentation D)
local notation "S" => MvPolynomial (Fin (n + 1)) R
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.freeGrade_smul_mem_grade {a e : ℤ} {c : S}
    (hc : c ∈ GradedModule.freeGrade R n a) {m : σ.F.M} (hm : m ∈ σ.F.grade e) :
    c • m ∈ σ.F.grade (e + a)
def

FProj

L144 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG.ProjSpaceCech.GradedModule.FProj
Documentation

The linear projection to the indicated integer grade of the shifted free presentation source.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section KerFG
variable {R : Type u} [CommRing R] {n : ℕ} {D : GradedModule R n}
variable (σ : GradedModule.Presentation D)
local notation "S" => MvPolynomial (Fin (n + 1)) R
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · full declaration
def GradedModule.FProj (d : ℤ) : σ.F.M →ₗ[R] σ.F.M where
  toFun m k := if 0 ≤ d + σ.d₀ k then
    (homogeneousComponent (d + σ.d₀ k).toNat (m k) :
      (GradedModule.FD R n (σ.d₀ k)).M) else 0
  map_add' m₁ m₂ := funext fun k => by
    by_cases h : 0 ≤ d + σ.d₀ k
    · exact (ite_eq_left h).trans ((map_add _ _ _).trans
        (congrArg₂ (· + ·) (ite_eq_left h).symm (ite_eq_left h).symm))
    · exact (ite_eq_right h).trans
        ((zero_add 0).symm.trans (congrArg₂ (· + ·) (ite_eq_right h).symm (ite_eq_right h).symm))
  map_smul' r m := funext fun k => by
    by_cases h : 0 ≤ d + σ.d₀ k
    · exact (ite_eq_left h).trans ((map_smul _ _ _).trans (congrArg (r • ·) (ite_eq_left h).symm))
    · exact (ite_eq_right h).trans ((smul_zero r).symm.trans (congrArg (r • ·) (ite_eq_right
      h).symm))
theorem

FProj_apply

L161 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG.ProjSpaceCech.GradedModule.FProj_apply
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section KerFG
variable {R : Type u} [CommRing R] {n : ℕ} {D : GradedModule R n}
variable (σ : GradedModule.Presentation D)
local notation "S" => MvPolynomial (Fin (n + 1)) R
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · full declaration
theorem GradedModule.FProj_apply (d : ℤ) (m : σ.F.M) (k : σ.J) :
    GradedModule.FProj σ d m k
      = if 0 ≤ d + σ.d₀ k then
          (homogeneousComponent (d + σ.d₀ k).toNat (m k) :
            (GradedModule.FD R n (σ.d₀ k)).M) else 0 := by
  rfl
theorem

FProj_apply_of_mem_grade

L169 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG.ProjSpaceCech.GradedModule.FProj_apply_of_mem_grade
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section KerFG
variable {R : Type u} [CommRing R] {n : ℕ} {D : GradedModule R n}
variable (σ : GradedModule.Presentation D)
local notation "S" => MvPolynomial (Fin (n + 1)) R
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · full declaration
theorem GradedModule.FProj_apply_of_mem_grade (d e : ℤ) {m : σ.F.M}
    (hm : m ∈ σ.F.grade e) :
    GradedModule.FProj σ d m = if d = e then m else 0 := by
  funext k
  rw [GradedModule.FProj_apply]
  have hmk := (GradedModule.mem_F_grade σ e m).mp hm k
  by_cases hd : 0 ≤ d + σ.d₀ k
  · rw [ite_eq_left hd]
    by_cases he : 0 ≤ e + σ.d₀ k
    · rw [GradedModule.freeGrade_of_nonneg R n he] at hmk
      rw [homogeneousComponent_of_mem hmk]
      by_cases hde : d = e
      · erw [ite_eq_left (show (d + σ.d₀ k).toNat = (e + σ.d₀ k).toNat from
        by omega), ite_eq_left hde]
      · erw [ite_eq_right (show (d + σ.d₀ k).toNat ≠ (e + σ.d₀ k).toNat from fun h => hde (
        by omega)),
          ite_eq_right hde]; rfl
    · have hmk0 : m k = 0 := by
        simp only [GradedModule.freeGrade, he, ite_false] at hmk
        exact hmk
      rw [hmk0, ite_eq_right (show d ≠ e from fun h => he (h ▸ hd))]
      exact map_zero _
  · rw [ite_eq_right hd]
    by_cases hde : d = e
    · subst hde
      have hmk0 : m k = 0 := by
        simp only [GradedModule.freeGrade, hd, ite_false] at hmk
        exact hmk
      rw [ite_eq_left rfl]; exact hmk0.symm
    · rw [ite_eq_right hde]; rfl
theorem

ker_isFG'

L207 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG.ProjSpaceCech.GradedModule.Presentation.ker_isFG'
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section KerFG
variable {R : Type u} [CommRing R] {n : ℕ} {D : GradedModule R n}
variable (σ : GradedModule.Presentation D)
local notation "S" => MvPolynomial (Fin (n + 1)) R
open scoped _root_.ProjSpaceCech.GradedModule _root_.ProjSpaceCech.GradedModule.Presentation in
Lean source · statement
theorem GradedModule.Presentation.ker_isFG' [IsNoetherianRing R] : GradedModule.IsFG σ.ker
theorem

ker_isFG

L338 ↗
ProjSpaceCech.GradedModule.Presentation.ker_isFG
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Presentation_ker_isFG
universe u
noncomputable section
open Finset Function MvPolynomial
Lean source · statement
theorem _root_.ProjSpaceCech.GradedModule.Presentation.ker_isFG {R : Type u} [CommRing R]
    [IsNoetherianRing R] {n : ℕ} {D : ProjSpaceCech.GradedModule R n}
    (σ : ProjSpaceCech.GradedModule.Presentation D) : ProjSpaceCech.GradedModule.IsFG σ.ker

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