NineLinearObstruction.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Nonsingular tensor evaluation matrices obstruct the Euclidean Ramsey property.

theorem OAI.EuclideanRamsey.NineLinearObstruction.vector_eq_zero_of_det_ne_zero line 13
abbrev OAI.EuclideanRamsey.NineLinearObstruction.Column line 20
def OAI.EuclideanRamsey.NineLinearObstruction.evaluationMatrix line 24
Source documentation
Rows are reindexed by an actual equivalence; entries are the exact images of the two augmented-coordinate tensor factors in FieldCriterion.
```
def evaluationMatrix {s d : ℕ} (a : Fin s → Space d)
    {K : Type*} [Field K] [Algebra ℚ K]
    (f : TensorRing a →ₐ[ℚ] K) (e : Column d ≃ Fin s) :
    Matrix (Column d) (Column d) K := fun i q =>
…
```
Mentions: OAI.EuclideanRamsey.Space, OAI.EuclideanRamsey.TensorRing, OAI.EuclideanRamsey.NineLinearObstruction.Column
theorem OAI.EuclideanRamsey.NineLinearObstruction.not_fieldCriterion_of_det_ne_zero line 31
theorem OAI.EuclideanRamsey.NineLinearObstruction.not_ramsey_of_det_ne_zero line 63
Source documentation
Ramsey configurations cannot have a nonsingular tensor evaluation matrix.
```
theorem not_ramsey_of_det_ne_zero {s d : ℕ} (a : Fin s → Space d)
    (hs : 0 < s) (hd : 0 < d)
    (hspan : affineSpan ℝ (Set.range a) = ⊤)
    {K : Type*} [Field K] [Algebra ℚ K]
    (f : TensorRing a →ₐ[ℚ] K) (hf : Function.Injective f)
    (e : Column d ≃ Fin s) (hdet : (evaluationMatrix a f e).det ≠ 0) :
    ¬ Ramsey a := by
…
```
Mentions: OAI.EuclideanRamsey.Space, OAI.EuclideanRamsey.TensorRing, OAI.EuclideanRamsey.NineLinearObstruction.Column, OAI.EuclideanRamsey.NineLinearObstruction.evaluationMatrix, OAI.EuclideanRamsey.Ramsey