NYLL
Module

IntegralRelation.lean

Nyll.SchemeTheory.NoetherNormalization.IntegralRelation
2 declarations indexed from sourceView source ↗

Module documentation

Integral elements from linearized polynomial relations

This file turns the unit-leading-coefficient relation produced by the triangular change of variables into an actual monic relation over the algebra generated by the remaining coordinates.

Imports3
Imported by3

Declarations

theorem

exists_linearCoordinatesFirst_isIntegral

L35 ↗
FieldArithmetic.Chapter06.exists_linearCoordinatesFirst_isIntegral
Documentation

If a nonzero polynomial relation holds on a tuple, then after a triangular linear change the first coordinate is integral over the algebra generated by the remaining changed coordinates.

This is the monic-relation step in Fried--Jarden, Lemma 22.5.1.

Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open MvPolynomial
variable {K : Type*} [Field K] [Infinite K]
Lean source · statement
theorem exists_linearCoordinatesFirst_isIntegral
    {A : Type*} [CommRing A] [Algebra K A] {n : ℕ}
    (x : Fin (n + 1) → A) {F : MvPolynomial (Fin (n + 1)) K}
    (hF : F ≠ 0) (hrel : aeval x F = 0) :
    ∃ c : Fin n → K,
      IsIntegral
        (Algebra.adjoin K (Set.range (linearTailCoordinatesFirst c x))) (x 0)
theorem

exists_linearCoordinates_all_isIntegral

L100 ↗
FieldArithmetic.Chapter06.exists_linearCoordinates_all_isIntegral
Documentation

The same triangular change makes every original coordinate integral over the algebra generated by the changed tail coordinates.

Indeed, each changed tail coordinate already belongs to the base algebra and the inverse change has the form xᵢ = (xᵢ - cᵢ x₀) + cᵢ x₀.

Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open MvPolynomial
variable {K : Type*} [Field K] [Infinite K]
Lean source · statement
theorem exists_linearCoordinates_all_isIntegral
    {A : Type*} [CommRing A] [Algebra K A] {n : ℕ}
    (x : Fin (n + 1) → A) {F : MvPolynomial (Fin (n + 1)) K}
    (hF : F ≠ 0) (hrel : aeval x F = 0) :
    ∃ c : Fin n → K, ∀ i : Fin (n + 1),
      IsIntegral
        (Algebra.adjoin K (Set.range (linearTailCoordinatesFirst c x))) (x i)

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