NineRationalDeterminant.lean`

27 declarations, 0 contain sorry, 0 declared as axioms

Clearing denominators transfers the polynomial determinant to a faithful rational-function realization. Renaming variables transports the result to any equivalent set of nine row labels.

abbrev OAI.EuclideanRamsey.NineRational.Index line 16
abbrev OAI.EuclideanRamsey.NineRational.Poly line 17
abbrev OAI.EuclideanRamsey.NineRational.K line 18
def OAI.EuclideanRamsey.NineRational.r line 21
Source documentation
Actual rational-coordinate vector, including its constant first entry.
```
def r {F : Type*} [Field F] (z : F) : Fin 3 → F :=
…
```
lemma OAI.EuclideanRamsey.NineRational.polynomial_denominator_ne_zero line 24
lemma OAI.EuclideanRamsey.NineRational.mapped_denominator_ne_zero line 30
lemma OAI.EuclideanRamsey.NineRational.clear_r line 38
def OAI.EuclideanRamsey.NineRational.genericMatrix line 43
Source documentation
The actual rational-coordinate matrix in any faithful polynomial realization.
```
def genericMatrix {F : Type*} [Field F] (f : Poly →+* F) : Matrix Index Index F :=
…
```
Mentions: OAI.EuclideanRamsey.NineRational.Poly, OAI.EuclideanRamsey.NineRational.Index
def OAI.EuclideanRamsey.NineRational.rowDenominator line 46
lemma OAI.EuclideanRamsey.NineRational.cleared_matrix line 50
Source documentation
Multiplying each row by its denominator gives the polynomial matrix.
```
lemma cleared_matrix {F : Type*} [Field F] (f : Poly →+* F)
    (hf : Function.Injective f) :
    f.mapMatrix NineGrid.E = Matrix.diagonal (rowDenominator f) * genericMatrix f := by
…
```
Mentions: OAI.EuclideanRamsey.NineRational.Poly, OAI.EuclideanRamsey.NineGrid.E, OAI.EuclideanRamsey.NineRational.rowDenominator, OAI.EuclideanRamsey.NineRational.genericMatrix
theorem OAI.EuclideanRamsey.NineRational.det_genericMatrix_ne_zero line 64
Source documentation
The rational-coordinate matrix has nonzero determinant in every faithful realization.
```
theorem det_genericMatrix_ne_zero {F : Type*} [Field F]
    (f : Poly →+* F) (hf : Function.Injective f) :
    Matrix.det (genericMatrix f) ≠ 0 := by
…
```
Mentions: OAI.EuclideanRamsey.NineRational.Poly, OAI.EuclideanRamsey.NineRational.genericMatrix
def OAI.EuclideanRamsey.NineRational.polynomialInclusion line 80
Source documentation
The polynomial inclusion into the doubled-variable fraction field.
```
def polynomialInclusion : Poly →+* K := algebraMap Poly K
```
Mentions: OAI.EuclideanRamsey.NineRational.Poly, OAI.EuclideanRamsey.NineRational.K
def OAI.EuclideanRamsey.NineRational.t line 82
def OAI.EuclideanRamsey.NineRational.u line 83
def OAI.EuclideanRamsey.NineRational.M line 85
theorem OAI.EuclideanRamsey.NineRational.det_M_ne_zero line 87
def OAI.EuclideanRamsey.NineRational.tVar line 95
Source documentation
Independent rational-function variables with arbitrary row labels.
```
def tVar (i : ι) : IndependentTensor.JointField ι :=
…
```
Mentions: OAI.EuclideanRamsey.IndependentTensor.JointField
def OAI.EuclideanRamsey.NineRational.uVar line 99
def OAI.EuclideanRamsey.NineRational.transportPoly line 104
Source documentation
Rename the polynomial variables bijectively and include them in the fraction field.
```
def transportPoly (e : ι ≃ Index) : Poly →+* IndependentTensor.JointField ι :=
…
```
Mentions: OAI.EuclideanRamsey.NineRational.Index, OAI.EuclideanRamsey.NineRational.Poly, OAI.EuclideanRamsey.IndependentTensor.JointField
lemma OAI.EuclideanRamsey.NineRational.transportPoly_injective line 108
def OAI.EuclideanRamsey.NineRational.transportedMatrix line 115
Source documentation
Both axes are reindexed by e. Columns encode the two coordinate indices.
```
def transportedMatrix (e : ι ≃ Index) : Matrix ι ι (IndependentTensor.JointField ι) :=
…
```
Mentions: OAI.EuclideanRamsey.NineRational.Index, OAI.EuclideanRamsey.IndependentTensor.JointField
lemma OAI.EuclideanRamsey.NineRational.transportedMatrix_apply line 118
theorem OAI.EuclideanRamsey.NineRational.det_transportedMatrix_ne_zero line 123
def OAI.EuclideanRamsey.NineRational.fin9Equiv line 132
Source documentation
Concrete row/column enumeration of the nine tensor coordinates.
```
def fin9Equiv : Fin 9 ≃ Index := (finProdFinEquiv : Index ≃ Fin (3 * 3)).symm
```
Mentions: OAI.EuclideanRamsey.NineRational.Index
def OAI.EuclideanRamsey.NineRational.fin9Matrix line 134
lemma OAI.EuclideanRamsey.NineRational.fin9Matrix_apply line 137
theorem OAI.EuclideanRamsey.NineRational.det_fin9Matrix_ne_zero line 141