BinaryForms.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

Binary homogeneous factorization and prime line equations

theorem OAI.Nagata.W02.natDegree_eval₂_le_totalDegree line 30

Source documentation

Substituting polynomials of degree at most one cannot increase total degree.

theorem natDegree_eval₂_le_totalDegree {σ K : Type*} [CommSemiring K]
    (P : MvPolynomial σ K) (f : σ → Polynomial K)
    (hf : ∀ i, (f i).natDegree ≤ 1) :
    (P.eval₂ Polynomial.C f).natDegree ≤ P.totalDegree := by
…

def OAI.Nagata.W02.DegreeExponent line 63
Source documentation
Ternary exponent vectors with sum k.
```
def DegreeExponent (k : ℕ) := {d : Fin 3 →₀ ℕ // d.degree = k}
```
instance OAI.Nagata.W02.degreeExponentFintype line 65
def OAI.Nagata.W02.homogeneousCoefficientEquiv line 70
Source documentation
Proved identification with the actual supported coefficient submodule.
```
def homogeneousCoefficientEquiv (R : Type*) [CommRing R] (k : ℕ) :
    MvPolynomial.homogeneousSubmodule (Fin 3) R k ≃ₗ[R] (DegreeExponent k →₀ R) :=
…
```
Mentions: OAI.Nagata.W02.DegreeExponent
theorem OAI.Nagata.W02.homogeneousCoefficientEquiv_apply line 76
theorem OAI.Nagata.W02.homogeneousCoefficientEquiv_symm_single line 80
def OAI.Nagata.W02.degreeExponentEquiv line 104
Source documentation
Explicit finite enumeration by the genuine finsupp antidiagonal.
```
def degreeExponentEquiv (k : ℕ) :
    DegreeExponent k ≃ ↥(Finset.finsuppAntidiag (Finset.univ : Finset (Fin 3)) k) where
…
```
Mentions: OAI.Nagata.W02.DegreeExponent
theorem OAI.Nagata.W02.card_degreeExponent line 118
Source documentation
Stars and bars for three variables, with the exact binomial convention required by the manuscript.
```
theorem card_degreeExponent (k : ℕ) :
    Fintype.card (DegreeExponent k) = (k + 2).choose 2 := by
…
```
Mentions: OAI.Nagata.W02.DegreeExponent
def OAI.Nagata.W02.homogeneousBasis line 128
Source documentation
The monomial basis transported through the proved coefficient equivalence.
```
def homogeneousBasis (K : Type*) [Field K] (k : ℕ) :
    Module.Basis (DegreeExponent k) K (MvPolynomial.homogeneousSubmodule (Fin 3) K k) :=
…
```
Mentions: OAI.Nagata.W02.DegreeExponent
theorem OAI.Nagata.W02.homogeneousBasis_coe line 133
Source documentation
Every basis vector is the genuine monomial with its advertised exponent.
```
theorem homogeneousBasis_coe (K : Type*) [Field K] (k : ℕ) (e : DegreeExponent k) :
    ((homogeneousBasis K k e) : MvPolynomial (Fin 3) K) = MvPolynomial.monomial e.val 1 := by
…
```
Mentions: OAI.Nagata.W02.DegreeExponent, OAI.Nagata.W02.homogeneousBasis
instance OAI.Nagata.W02.homogeneousFiniteDimensional line 137

theorem OAI.Nagata.W02.finrank_homogeneousSubmodule line 142

Source documentation

Exact dimension of genuine ternary homogeneous forms.

theorem finrank_homogeneousSubmodule (K : Type*) [Field K] (k : ℕ) :
    Module.finrank K (MvPolynomial.homogeneousSubmodule (Fin 3) K k) =
      (k + 2).choose 2 := by
…

theorem OAI.Nagata.W02.aeval_homogeneousCoefficientEquiv_symm line 161

Source documentation

Decoding a homogeneous coefficient vector and evaluating is exactly its linear combination of evaluated monomials.

theorem aeval_homogeneousCoefficientEquiv_symm (d : ℕ) (s : Fin 3 → A)
    (c : DegreeExponent d →₀ K) :
    MvPolynomial.aeval s
      (((homogeneousCoefficientEquiv K d).symm c) : MvPolynomial (Fin 3) K) =
    Finsupp.linearCombination K
      (fun e : DegreeExponent d => MvPolynomial.aeval s (MvPolynomial.monomial e.val (1 : K))) c := by
…

Mentions: OAI.Nagata.W02.DegreeExponent, OAI.Nagata.W02.homogeneousCoefficientEquiv

abbrev OAI.Nagata.W02.BinaryForm line 187
def OAI.Nagata.W02.binaryLinear line 189
def OAI.Nagata.W02.binaryRootProduct line 191
def OAI.Nagata.W02.binaryAffineHom line 193
theorem OAI.Nagata.W02.binaryAffineHom_apply line 196
theorem OAI.Nagata.W02.binaryLinear_homogeneous line 199
theorem OAI.Nagata.W02.binaryLinear_ne_zero line 202
theorem OAI.Nagata.W02.binaryRootProduct_homogeneous line 207
theorem OAI.Nagata.W02.binaryAffineHom_linear line 214
theorem OAI.Nagata.W02.binaryAffineHom_rootProduct line 219
theorem OAI.Nagata.W02.binary_homogeneous_factorization line 229
Source documentation
Exact projective factorization, including constant forms and all roots at infinity. Every displayed factor is a nonzero homogeneous linear form.
```
theorem binary_homogeneous_factorization {F : BinaryForm} {d : ℕ}
    (hF : F.IsHomogeneous d) (hF0 : F ≠ 0) :
    ∃ (c : ℂ) (e : ℕ) (s : Multiset ℂ), c ≠ 0 ∧ e + s.card = d ∧
      F = C c * ((X 1 : BinaryForm) ^ e * binaryRootProduct s) := by
…
```
Mentions: OAI.Nagata.W02.BinaryForm, OAI.Nagata.W02.binaryRootProduct
theorem OAI.Nagata.W02.lineSubstitution_natDegree_le line 273
Source documentation
The source's explicit line parameterization uses only affine-linear coordinates.
```
theorem lineSubstitution_natDegree_le {K : Type*} [Field K] (i : K) (j : Fin 3) :
    (lineSubstitution i j).natDegree ≤ 1 := by
…
```

theorem OAI.Nagata.W02.lineRestriction_natDegree_le_totalDegree line 285

Source documentation

Actual component restriction degree is bounded by ambient total degree.

theorem lineRestriction_natDegree_le_totalDegree {K : Type*} [Field K]
    (i : K) (P : MvPolynomial (Fin 3) K) :
    (lineRestriction i P).natDegree ≤ P.totalDegree :=
…

theorem OAI.Nagata.W02.binary_homogeneous_notMem line 303

Source documentation

A homogeneous binary relation in a prime ideal forces a linear relation.

theorem binary_homogeneous_notMem {J : Ideal BinaryForm} (hJ : J.IsPrime)
    (hlin : ∀ a b : ℂ, C a * X 0 + C b * X 1 ∈ J → a = 0 ∧ b = 0)
    {F : BinaryForm} {d : ℕ} (hF : F.IsHomogeneous d) (hF0 : F ≠ 0) : F ∉ J := by
…

Mentions: OAI.Nagata.W02.BinaryForm

theorem OAI.Nagata.W02.binary_eq_zero_of_mem line 332

Source documentation

Component closure upgrades the homogeneous conclusion to every binary polynomial.

theorem binary_eq_zero_of_mem {J : Ideal BinaryForm} (hJ : J.IsPrime)
    (hcomp : ∀ F ∈ J, ∀ d, homogeneousComponent d F ∈ J)
    (hlin : ∀ a b : ℂ, C a * X 0 + C b * X 1 ∈ J → a = 0 ∧ b = 0)
    {F : BinaryForm} (hF : F ∈ J) : F = 0 := by
…

Mentions: OAI.Nagata.W02.BinaryForm

theorem OAI.Nagata.W02.homogeneousComponent_rename line 344

Source documentation

Renaming preserves each ordinary homogeneous component, including collisions.

theorem homogeneousComponent_rename {σ ι : Type*} (e : σ → ι)
    (F : MvPolynomial σ ℂ) (d : ℕ) :
    homogeneousComponent d (rename e F) = rename e (homogeneousComponent d F) := by
…

theorem OAI.Nagata.W02.component_mem_of_isHomogeneous line 355

Source documentation

Concrete ordinary component closure extracted from mathlib's graded ideal.

theorem component_mem_of_isHomogeneous {σ : Type*} {I : Ideal (MvPolynomial σ ℂ)}
    (hI : I.IsHomogeneous (homogeneousSubmodule σ ℂ)) {P : MvPolynomial σ ℂ}
    (hP : P ∈ I) (n : ℕ) : homogeneousComponent n P ∈ I := by
…

theorem OAI.Nagata.W02.binary_rename_eq_zero_of_mem line 367

Source documentation

Two variables in a homogeneous prime quotient have no polynomial relation if they have no linear relation. This statement uses genuine renamed polynomials.

theorem binary_rename_eq_zero_of_mem {σ : Type*} (e : Fin 2 → σ)
    {I : Ideal (MvPolynomial σ ℂ)} (hI : I.IsPrime)
    (hhom : I.IsHomogeneous (homogeneousSubmodule σ ℂ))
    (hlin : ∀ a b : ℂ, C a * X (e 0) + C b * X (e 1) ∈ I → a = 0 ∧ b = 0)
    {F : BinaryForm} (hF : rename e F ∈ I) : F = 0 := by
…

Mentions: OAI.Nagata.W02.BinaryForm

theorem OAI.Nagata.W02.algebraicIndependent_quotient_of_no_linear_relation line 383

Source documentation

Algebraic independence of the two actual coordinate classes in the quotient.

theorem algebraicIndependent_quotient_of_no_linear_relation {σ : Type*}
    (e : Fin 2 → σ) {I : Ideal (MvPolynomial σ ℂ)} (hI : I.IsPrime)
    (hhom : I.IsHomogeneous (homogeneousSubmodule σ ℂ))
    (hlin : ∀ a b : ℂ, C a * X (e 0) + C b * X (e 1) ∈ I → a = 0 ∧ b = 0) :
    AlgebraicIndependent ℂ (fun i : Fin 2 => Ideal.Quotient.mk I (X (e i))) := by
…

theorem OAI.Nagata.W02.lineRestriction_natDegree_le line 408