OAI/Combinatorics/EuclideanRamsey/NineField.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.EuclideanRamsey.NineField.ParameterPoly line 14
2. abbrev OAI.EuclideanRamsey.NineField.ParameterField line 15
3. abbrev OAI.EuclideanRamsey.NineField.TargetPoly line 16
4. abbrev OAI.EuclideanRamsey.NineField.TargetField line 17
5. theorem OAI.EuclideanRamsey.NineField.parameterFieldAlgebra_eq_canonical line 29
6. theorem OAI.EuclideanRamsey.NineField.targetFieldAlgebra_eq_canonical line 33
7. def OAI.EuclideanRamsey.NineField.T line 37
8. def OAI.EuclideanRamsey.NineField.U line 40
9. def OAI.EuclideanRamsey.NineField.a0 line 44

   Source documentation

   The three augmented rational parametrization entries.

   def a0 : TargetField := 1

   Mentions: OAI.EuclideanRamsey.NineField.TargetField

10. def OAI.EuclideanRamsey.NineField.a1 line 45
11. def OAI.EuclideanRamsey.NineField.a2 line 46
12. def OAI.EuclideanRamsey.NineField.paramVector line 48
13. def OAI.EuclideanRamsey.NineField.parameter line 56

    Source documentation

    Each parameter is an element of the actual coordinate field, by the proved recovery formula and coordinate-field equality.

    def parameter (i : Fin 9) : Coeff (circleConfig t) :=
    …

    Mentions: OAI.EuclideanRamsey.Coeff

14. theorem OAI.EuclideanRamsey.NineField.parameter_coe line 61
15. theorem OAI.EuclideanRamsey.NineField.coordinate_zero line 63
16. theorem OAI.EuclideanRamsey.NineField.coordinate_one line 69
17. def OAI.EuclideanRamsey.NineField.coefficientEquiv line 81

    Source documentation

    The actual coefficient field is identified with the rational function field using exactly the given algebraic independence of the real parameters.

    def coefficientEquiv : Coeff (circleConfig t) ≃ₐ[ℚ] ParameterField :=
    …

    Mentions: OAI.EuclideanRamsey.Coeff, OAI.EuclideanRamsey.NineField.ParameterField

18. theorem OAI.EuclideanRamsey.NineField.coefficientEquiv_parameter line 85
19. def OAI.EuclideanRamsey.NineField.leftCoeff line 100
20. def OAI.EuclideanRamsey.NineField.rightCoeff line 103
21. theorem OAI.EuclideanRamsey.NineField.leftCoeff_parameter line 106
22. theorem OAI.EuclideanRamsey.NineField.rightCoeff_parameter line 110
23. theorem OAI.EuclideanRamsey.NineField.leftCoeff_coordinate_zero line 114
24. theorem OAI.EuclideanRamsey.NineField.leftCoeff_coordinate_one line 119
25. theorem OAI.EuclideanRamsey.NineField.rightCoeff_coordinate_zero line 124
26. theorem OAI.EuclideanRamsey.NineField.rightCoeff_coordinate_one line 129
27. def OAI.EuclideanRamsey.NineField.coefficientTensorEquiv line 135

    Source documentation

    The tensor equivalence transports both copies of the actual field.

    def coefficientTensorEquiv :
        TensorRing (circleConfig t) ≃ₐ[ℚ] ParameterField ⊗[ℚ] ParameterField :=
    …

    Mentions: OAI.EuclideanRamsey.TensorRing, OAI.EuclideanRamsey.NineField.ParameterField

28. def OAI.EuclideanRamsey.NineField.coordinateTensorEmbedding line 141

    Source documentation

    The coordinate-field tensor square embeds in the rational function field on eighteen variables.

    def coordinateTensorEmbedding : TensorRing (circleConfig t) →ₐ[ℚ] TargetField :=
    …

    Mentions: OAI.EuclideanRamsey.TensorRing, OAI.EuclideanRamsey.NineField.TargetField

29. theorem OAI.EuclideanRamsey.NineField.coordinateTensorEmbedding_injective line 145
30. theorem OAI.EuclideanRamsey.NineField.coordinateTensorEmbedding_tmul line 150
31. theorem OAI.EuclideanRamsey.NineField.coordinateTensorEmbedding_a0_left line 157

    Source documentation

    Exact images of the constant and two spatial augmented coordinates.

    @[simp] theorem coordinateTensorEmbedding_a0_left (i : Fin 9) :
        coordinateTensorEmbedding t ht
          ((augmented (circleConfig t) i none) ⊗ₜ[ℚ] 1) = a0 := by
    …

    Mentions: OAI.EuclideanRamsey.NineField.coordinateTensorEmbedding, OAI.EuclideanRamsey.augmented, OAI.EuclideanRamsey.NineField.a0

32. theorem OAI.EuclideanRamsey.NineField.coordinateTensorEmbedding_a1_left line 162
33. theorem OAI.EuclideanRamsey.NineField.coordinateTensorEmbedding_a2_left line 167
34. theorem OAI.EuclideanRamsey.NineField.coordinateTensorEmbedding_a0_right line 172
35. theorem OAI.EuclideanRamsey.NineField.coordinateTensorEmbedding_a1_right line 177
36. theorem OAI.EuclideanRamsey.NineField.coordinateTensorEmbedding_a2_right line 182
37. theorem OAI.EuclideanRamsey.NineField.leftCoeff_augmented line 187
38. theorem OAI.EuclideanRamsey.NineField.rightCoeff_augmented line 193
39. theorem OAI.EuclideanRamsey.NineField.coordinateTensorEmbedding_augmented_tmul line 200

    Source documentation

    The augmented-coordinate tensors map to entries of the rational evaluation matrix.

    theorem coordinateTensorEmbedding_augmented_tmul (i : Fin 9)
        (α β : Option (Fin 2)) :
        coordinateTensorEmbedding t ht
          ((augmented (circleConfig t) i α) ⊗ₜ[ℚ] (augmented (circleConfig t) i β)) =
          paramVector (T i) α * paramVector (U i) β := by
    …

    Mentions: OAI.EuclideanRamsey.NineField.coordinateTensorEmbedding, OAI.EuclideanRamsey.augmented, OAI.EuclideanRamsey.NineField.paramVector, OAI.EuclideanRamsey.NineField.T, OAI.EuclideanRamsey.NineField.U