The variable Čech diagram of a graded polynomial module

For a tuple of variables, this file forms the product denominator, the corresponding degree-zero localization of an arbitrary graded polynomial module, and the face map obtained by adjoining one variable. The construction is entirely algebraic: it does not mention Proj, basic opens, sheaves, or cohomology.

The natural- and integer-shift terms are definitional specializations of the arbitrary graded-family construction. This file also owns the canonical p / 1 element in a one-variable term. Geometric consumers compare these localizations and elements with sections on intersections of the variable basic-open cover.

Tags

Čech diagram, multivariate polynomial, homogeneous localization, graded module

Denominators

noncomputable def MvPolynomial.polynomialVariableCechDenominator (ι k : Type u) [Field k] {n : ℕ} (x : Fin (n + 1) → ι) : MvPolynomial ι k

The product of the variables indexing one (n + 1)-fold Čech intersection.

Equations

• MvPolynomial.polynomialVariableCechDenominator ι k x = ∏ a : Fin (n + 1), MvPolynomial.X (x a)

theorem MvPolynomial.polynomialVariableCechDenominator_mem (ι k : Type u) [Field k] {n : ℕ} (x : Fin (n + 1) → ι) : polynomialVariableCechDenominator ι k x ∈ polynomialGrading ι k (n + 1)

The Čech denominator for an (n + 1)-fold intersection is homogeneous of degree n + 1.

Natural-shift terms and faces

@[reducible, inline]

noncomputable abbrev MvPolynomial.polynomialVariableCechTerm (ι k : Type u) [Field k] (d n : ℕ) (x : Fin (n + 1) → ι) : Submodule (HomogeneousLocalization (polynomialGrading ι k) (Submonoid.powers (polynomialVariableCechDenominator ι k x))) (LocalizedModule (Submonoid.powers (polynomialVariableCechDenominator ι k x)) (MvPolynomial ι k))

The algebraic degree-d term attached to one variable Čech intersection. It is a degree-zero homogeneous localization, with no geometric or finite-dimensionality assertion.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev MvPolynomial.polynomialVariableCechCochains (ι k : Type u) [Field k] (d n : ℕ) : Type u

Degree-n algebraic Čech cochains for a natural shift.

Equations

• MvPolynomial.polynomialVariableCechCochains ι k d n = ((x : Fin (n + 1) → ι) → ↥(MvPolynomial.polynomialVariableCechTerm ι k d n x))

noncomputable def MvPolynomial.polynomialVariableFraction (ι k : Type u) [Field k] (d : ℕ) (p : ↥(homogeneousSubmodule ι k d)) (i : ι) : ↥(GradedModule.DegreeZeroLocalization (polynomialGrading ι k) (GradedModule.natShift (polynomialGrading ι k) d) (Submonoid.powers (X i)))

The canonical fraction p / 1 in the degree-zero localization at one polynomial variable.

Equations

• MvPolynomial.polynomialVariableFraction ι k d p i = GradedModule.DegreeZeroLocalization.mk { deg := 0, num := ⟨↑p, ⋯⟩, den := ⟨1, ⋯⟩, den_mem := ⋯ }

theorem MvPolynomial.polynomialVariableCechDenominator_succAbove (ι k : Type u) [Field k] {n : ℕ} (x : Fin (n + 2) → ι) (j : Fin (n + 2)) : polynomialVariableCechDenominator ι k (x ∘ j.succAbove) * X (x j) = polynomialVariableCechDenominator ι k x

Dropping the j-th index multiplies the Čech denominator back up by that variable.

theorem MvPolynomial.polynomialVariableCechDenominator_succAbove_mem (ι k : Type u) [Field k] {n : ℕ} (x : Fin (n + 2) → ι) (j : Fin (n + 2)) : polynomialVariableCechDenominator ι k (x ∘ j.succAbove) * X (x j) ∈ Submonoid.powers (polynomialVariableCechDenominator ι k x)

The j-th Čech denominator divides the full one, in the Submonoid.powers form faceMap asks for.

noncomputable def MvPolynomial.polynomialVariableCechFace (ι k : Type u) [Field k] (d : ℕ) {n : ℕ} (x : Fin (n + 2) → ι) (j : Fin (n + 2)) : ↥(polynomialVariableCechTerm ι k d n (x ∘ j.succAbove)) →+ ↥(polynomialVariableCechTerm ι k d (n + 1) x)

The j-th face of the algebraic variable Čech diagram for a natural shift.

Equations

• MvPolynomial.polynomialVariableCechFace ι k d x j = GradedModule.DegreeZeroLocalization.faceMap ⋯ ⋯ ⋯

Integer-shift terms and faces

@[reducible, inline]

noncomputable abbrev MvPolynomial.polynomialVariableIntCechTerm (ι k : Type u) [Field k] (d : ℤ) (n : ℕ) (x : Fin (n + 1) → ι) : Submodule (HomogeneousLocalization (polynomialGrading ι k) (Submonoid.powers (polynomialVariableCechDenominator ι k x))) (LocalizedModule (Submonoid.powers (polynomialVariableCechDenominator ι k x)) (MvPolynomial ι k))

The algebraic term attached to one variable Čech intersection, for an integer shift.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev MvPolynomial.polynomialVariableIntCechCochains (ι k : Type u) [Field k] (d : ℤ) (n : ℕ) : Type u

Degree-n algebraic Čech cochains for an integer shift.

Equations

• MvPolynomial.polynomialVariableIntCechCochains ι k d n = ((x : Fin (n + 1) → ι) → ↥(MvPolynomial.polynomialVariableIntCechTerm ι k d n x))

noncomputable def MvPolynomial.polynomialVariableIntCechFace (ι k : Type u) [Field k] (d : ℤ) {n : ℕ} (x : Fin (n + 2) → ι) (j : Fin (n + 2)) : ↥(polynomialVariableIntCechTerm ι k d n (x ∘ j.succAbove)) →+ ↥(polynomialVariableIntCechTerm ι k d (n + 1) x)

The j-th face of the algebraic variable Čech diagram for an integer shift.

Equations

• MvPolynomial.polynomialVariableIntCechFace ι k d x j = GradedModule.DegreeZeroLocalization.faceMap ⋯ ⋯ ⋯

An arbitrary graded family

@[reducible, inline]

noncomputable abbrev MvPolynomial.cechTerm (ι k : Type u) [Field k] {σM : Type u} [SetLike σM (MvPolynomial ι k)] [AddSubgroupClass σM (MvPolynomial ι k)] (𝓂 : ℕ → σM) [SetLike.GradedSMul (polynomialGrading ι k) 𝓂] {n : ℕ} (x : Fin (n + 1) → ι) : Submodule (HomogeneousLocalization (polynomialGrading ι k) (Submonoid.powers (polynomialVariableCechDenominator ι k x))) (LocalizedModule (Submonoid.powers (polynomialVariableCechDenominator ι k x)) (MvPolynomial ι k))

The algebraic term attached to one variable Čech intersection, for an arbitrary graded family of polynomial modules.

Equations

• MvPolynomial.cechTerm ι k 𝓂 x = GradedModule.DegreeZeroLocalization (MvPolynomial.polynomialGrading ι k) 𝓂 (Submonoid.powers (MvPolynomial.polynomialVariableCechDenominator ι k x))

@[reducible, inline]

abbrev MvPolynomial.cechCochains (ι k : Type u) [Field k] {σM : Type u} [SetLike σM (MvPolynomial ι k)] [AddSubgroupClass σM (MvPolynomial ι k)] (𝓂 : ℕ → σM) [SetLike.GradedSMul (polynomialGrading ι k) 𝓂] (n : ℕ) : Type u

Degree-n algebraic Čech cochains for an arbitrary graded family.

Equations

• MvPolynomial.cechCochains ι k 𝓂 n = ((x : Fin (n + 1) → ι) → ↥(MvPolynomial.cechTerm ι k 𝓂 x))

noncomputable def MvPolynomial.cechFace (ι k : Type u) [Field k] {σM : Type u} [SetLike σM (MvPolynomial ι k)] [AddSubgroupClass σM (MvPolynomial ι k)] (𝓂 : ℕ → σM) [SetLike.GradedSMul (polynomialGrading ι k) 𝓂] {n : ℕ} (x : Fin (n + 2) → ι) (j : Fin (n + 2)) : ↥(cechTerm ι k 𝓂 (x ∘ j.succAbove)) →+ ↥(cechTerm ι k 𝓂 x)

The j-th variable Čech face for an arbitrary graded family.

Equations

• MvPolynomial.cechFace ι k 𝓂 x j = GradedModule.DegreeZeroLocalization.faceMap ⋯ ⋯ ⋯

theorem MvPolynomial.cechFace_natShift (ι k : Type u) [Field k] (d : ℕ) {n : ℕ} (x : Fin (n + 2) → ι) (j : Fin (n + 2)) : cechFace ι k (GradedModule.natShift (polynomialGrading ι k) d) x j = polynomialVariableCechFace ι k d x j

The natural-shift face is the arbitrary-family face at natShift.

theorem MvPolynomial.cechFace_intShift (ι k : Type u) [Field k] (d : ℤ) {n : ℕ} (x : Fin (n + 2) → ι) (j : Fin (n + 2)) : cechFace ι k (GradedModule.intShift (polynomialGrading ι k) d) x j = polynomialVariableIntCechFace ι k d x j

The integer-shift face is the arbitrary-family face at intShift.

Cofactors

noncomputable def MvPolynomial.cechCofactor (ι k : Type u) [Field k] {n : ℕ} (x : Fin (n + 1) → ι) : MvPolynomial ι k

The product of all but the first variable in a Čech index.

Equations

• MvPolynomial.cechCofactor ι k x = ∏ a : Fin n, MvPolynomial.X (x a.succ)

theorem MvPolynomial.X_mul_cechCofactor (ι k : Type u) [Field k] {n : ℕ} (x : Fin (n + 1) → ι) : X (x 0) * cechCofactor ι k x = polynomialVariableCechDenominator ι k x

Splitting the Čech denominator off its first variable.

theorem MvPolynomial.cechCofactor_mem (ι k : Type u) [Field k] {n : ℕ} (x : Fin (n + 1) → ι) : cechCofactor ι k x ∈ polynomialGrading ι k n

The cofactor is homogeneous of degree n.