OAI/Combinatorics/EuclideanRamsey/IndependentTensor.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.EuclideanRamsey.IndependentTensor.Poly line 15
  2. abbrev OAI.EuclideanRamsey.IndependentTensor.Rat line 16
  3. abbrev OAI.EuclideanRamsey.IndependentTensor.JointPoly line 17
  4. abbrev OAI.EuclideanRamsey.IndependentTensor.JointField line 18
  5. def OAI.EuclideanRamsey.IndependentTensor.polyToRat line 20
  6. def OAI.EuclideanRamsey.IndependentTensor.jointToField line 23
  7. def OAI.EuclideanRamsey.IndependentTensor.leftPolynomialMap line 26
  8. def OAI.EuclideanRamsey.IndependentTensor.rightPolynomialMap line 29
  9. theorem OAI.EuclideanRamsey.IndependentTensor.leftPolynomialMap_injective line 32
  10. theorem OAI.EuclideanRamsey.IndependentTensor.rightPolynomialMap_injective line 37
  11. def OAI.EuclideanRamsey.IndependentTensor.leftMap line 43

    Source documentation

    The first rational-function copy, in the independent left variables.

    def leftMap : Rat ι →ₐ[ℚ] JointField ι :=
…

    Mentions: OAI.EuclideanRamsey.IndependentTensor.Rat, OAI.EuclideanRamsey.IndependentTensor.JointField

  12. def OAI.EuclideanRamsey.IndependentTensor.rightMap line 47

    Source documentation

    The second rational-function copy, in the independent right variables.

    def rightMap : Rat ι →ₐ[ℚ] JointField ι :=
…

    Mentions: OAI.EuclideanRamsey.IndependentTensor.Rat, OAI.EuclideanRamsey.IndependentTensor.JointField

  13. theorem OAI.EuclideanRamsey.IndependentTensor.leftMap_algebraMap line 50
  14. theorem OAI.EuclideanRamsey.IndependentTensor.rightMap_algebraMap line 56
  15. theorem OAI.EuclideanRamsey.IndependentTensor.leftMap_X line 62
  16. theorem OAI.EuclideanRamsey.IndependentTensor.rightMap_X line 67
  17. def OAI.EuclideanRamsey.IndependentTensor.tensorEmbedding line 73

    Source documentation

    The map to the joint rational-function field.

    def tensorEmbedding : Rat ι ⊗[ℚ] Rat ι →ₐ[ℚ] JointField ι :=
…

    Mentions: OAI.EuclideanRamsey.IndependentTensor.Rat, OAI.EuclideanRamsey.IndependentTensor.JointField

  18. theorem OAI.EuclideanRamsey.IndependentTensor.tensorEmbedding_tmul line 76
  19. theorem OAI.EuclideanRamsey.IndependentTensor.tensorEmbedding_X_tmul_one line 80
  20. theorem OAI.EuclideanRamsey.IndependentTensor.tensorEmbedding_one_tmul_X line 86
  21. def OAI.EuclideanRamsey.IndependentTensor.localizeLeft line 92
  22. def OAI.EuclideanRamsey.IndependentTensor.localizeRight line 95
  23. def OAI.EuclideanRamsey.IndependentTensor.halfEmbedding line 98
  24. def OAI.EuclideanRamsey.IndependentTensor.polynomialEmbedding line 101
  25. theorem OAI.EuclideanRamsey.IndependentTensor.polynomialEmbedding_injective line 104
  26. theorem OAI.EuclideanRamsey.IndependentTensor.halfEmbedding_comp_localizeLeft line 111

    Source documentation

    On polynomials the joint map is the standard polynomial tensor equivalence, followed by the injective fraction-ring inclusion.

    theorem halfEmbedding_comp_localizeLeft :
    (halfEmbedding ι).comp (localizeLeft ι) = polynomialEmbedding ι := by
…

    Mentions: OAI.EuclideanRamsey.IndependentTensor.halfEmbedding, OAI.EuclideanRamsey.IndependentTensor.localizeLeft, OAI.EuclideanRamsey.IndependentTensor.polynomialEmbedding

  27. theorem OAI.EuclideanRamsey.IndependentTensor.halfEmbedding_injective line 123

    Source documentation

    First localization: invert all nonzero polynomials in the left factor. The target map detects zero on the polynomial base, hence on its localization.

    theorem halfEmbedding_injective : Function.Injective (halfEmbedding ι) := by
…

    Mentions: OAI.EuclideanRamsey.IndependentTensor.halfEmbedding

  28. theorem OAI.EuclideanRamsey.IndependentTensor.tensorEmbedding_injective line 160

    Source documentation

    The two independent rational-function copies embed faithfully.

    theorem tensorEmbedding_injective : Function.Injective (tensorEmbedding ι) := by
…

    Mentions: OAI.EuclideanRamsey.IndependentTensor.tensorEmbedding