CubicRelations.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Finite-dimensional cubic relations among section products

theorem OAI.Nagata.W02.exists_nonzero_linearRelation line 18

Source documentation

More vectors than the dimension yield an actual nonzero finitely supported coefficient vector annihilated by their linear-combination map.

theorem exists_nonzero_linearRelation {K V I : Type*} [Field K]
    [AddCommGroup V] [Module K V] [Module.Finite K V] [Fintype I]
    (v : I → V) (hdim : Module.finrank K V < Fintype.card I) :
    ∃ c : I →₀ K, c ≠ 0 ∧ Finsupp.linearCombination K v c = 0 := by
…

theorem OAI.Nagata.W02.ten_vectors_relation line 30

Source documentation

Ten actual vectors in any space of dimension at most nine satisfy a nontrivial coefficient relation. Repeated vectors and the zero vector are allowed.

theorem ten_vectors_relation {K V : Type*} [Field K] [AddCommGroup V]
    [Module K V] [Module.Finite K V] (v : Fin 10 → V)
    (hdim : Module.finrank K V ≤ 9) :
    ∃ c : Fin 10 →₀ K, c ≠ 0 ∧ Finsupp.linearCombination K v c = 0 := by
…

theorem OAI.Nagata.W02.cubicExponent_sum line 47
theorem OAI.Nagata.W02.aeval_cubicMonomial_function line 50
theorem OAI.Nagata.W02.card_cubicExponent line 75
Source documentation
The actual homogeneous degree-three exponent space has ten monomials.
```
theorem card_cubicExponent : Fintype.card (DegreeExponent 3) = 10 := by
…
```
Mentions: OAI.Nagata.W02.DegreeExponent

theorem OAI.Nagata.W02.exists_nonzero_homogeneousCubic_relation line 82

Source documentation

Ten actual cubic monomials in a subspace of dimension at most nine give a nonzero genuine homogeneous cubic vanishing on the three algebra elements. This theorem does not assert smoothness, irreducibility, or image equality.

theorem exists_nonzero_homogeneousCubic_relation (s : Fin 3 → A)
    (W : Submodule K A) [Module.Finite K W]
    (hdim : Module.finrank K W ≤ 9)
    (hmon : ∀ e : DegreeExponent 3,
      MvPolynomial.aeval s (MvPolynomial.monomial e.val (1 : K)) ∈ W) :
    ∃ P : MvPolynomial (Fin 3) K,
      P ≠ 0 ∧ P.IsHomogeneous 3 ∧ MvPolynomial.aeval s P = 0 := by
…

Mentions: OAI.Nagata.W02.DegreeExponent