Module

Basic.lean

Nyll.AlgebraicCurves.Hilbert.Functor.Basic

4 declarations indexed from sourceView source ↗

Module documentation

Basic

Imports4

Mathlib.Data.Rat.Floor
Mathlib.RingTheory.MvPolynomial.Homogeneous
Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Mathlib.Tactic.Ext

Imported by46

abbrev

piece

L29 ↗

AlgebraicGeometry.HilbertFunctor.piece

Documentation

The degree-d homogeneous piece of the polynomial ring modulo the homogeneous ideal.

Source context 3 commands

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

namespace AlgebraicGeometry.HilbertFunctor
open MvPolynomial
variable {A : Type*} [CommRing A] {n : ℕ}

Lean source · statement

abbrev piece (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (d : ℕ) : Type _

structure

Point

L38 ↗

AlgebraicGeometry.HilbertFunctor.Point

Documentation

A homogeneous ideal with finite projective graded pieces of the prescribed rank at every prime.

Source context 4 commands

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

namespace AlgebraicGeometry.HilbertFunctor
open MvPolynomial
variable {A : Type*} [CommRing A] {n : ℕ}
variable (A n)

Lean source · full declaration

structure Point (h : ℕ → ℕ) where
  /-- The homogeneous ideal defining the family. -/
  I : Ideal (MvPolynomial (Fin (n + 1)) A)
  /-- Each homogeneous component of an element of the ideal remains in the ideal. -/
  homogeneous : ∀ p ∈ I, ∀ d : ℕ, homogeneousComponent d p ∈ I
  /-- Every graded quotient piece is a finite module over the coefficient ring. -/
  finite_piece : ∀ d : ℕ, Module.Finite A (piece I d)
  /-- Every graded quotient piece is projective over the coefficient ring. -/
  projective_piece : ∀ d : ℕ, Module.Projective A (piece I d)
  /-- The local rank of each graded quotient piece is the prescribed Hilbert function. -/
  rankAtStalk_piece : ∀ (d : ℕ) (p : PrimeSpectrum A), Module.rankAtStalk (piece I d) p = h d

theorem

ext

L52 ↗

AlgebraicGeometry.HilbertFunctor.Point.ext

Source context 5 commands

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

namespace AlgebraicGeometry.HilbertFunctor
open MvPolynomial
variable {A : Type*} [CommRing A] {n : ℕ}
variable (A n)
variable {A}

Lean source · statement

theorem Point.ext {h : ℕ → ℕ} {P Q : Point A n h} (e : P.I = Q.I) : P = Q

def

hilbertFunctionOf

L59 ↗

AlgebraicGeometry.HilbertFunctor.hilbertFunctionOf

Documentation

The Hilbert function equal to the ambient polynomial-ring dimension below the cutoff and to the nonnegative integer part of the polynomial value from the cutoff onward.

Source context 5 commands

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

namespace AlgebraicGeometry.HilbertFunctor
open MvPolynomial
variable {A : Type*} [CommRing A] {n : ℕ}
variable (A n)
variable {A}

Lean source · statement

def hilbertFunctionOf (P : Polynomial ℚ) (D₀ : ℕ) : ℕ → ℕ

Module documentation

Basic

Declarations

piece

Point

ext

hilbertFunctionOf