OAI/RepresentationTheory/RestrictedTilting/RegularTorus.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Torus density, regular localization and coprime denominator gluing.

  1. abbrev OAI.FiberFunctorProof.planeTorusPoints line 16
  2. def OAI.FiberFunctorProof.planeTorusEvaluation line 18
  3. lemma OAI.FiberFunctorProof.planeTorusEvaluation_apply line 23
  4. theorem OAI.FiberFunctorProof.planeTorusEvaluation_injective line 33
  5. lemma OAI.FiberFunctorProof.planeTorusEvaluation_X_isUnit line 45
  6. abbrev OAI.FiberFunctorProof.planeCoordinateChart line 52
  7. def OAI.FiberFunctorProof.planeChartEvaluation line 55
  8. lemma OAI.FiberFunctorProof.planeChartEvaluation_algebraMap line 60
  9. theorem OAI.FiberFunctorProof.planeChartEvaluation_injective line 66
  10. lemma OAI.FiberFunctorProof.regularSL2_polynomial_path line 88
  11. def OAI.FiberFunctorProof.regularLowerShear line 105
  12. lemma OAI.FiberFunctorProof.regularLowerShear_zero line 108
  13. lemma OAI.FiberFunctorProof.lowerShear_mul_entry line 113
  14. lemma OAI.FiberFunctorProof.upperShear_mul_entry line 121
  15. theorem OAI.FiberFunctorProof.regularSL2_torus_dense line 131
  16. def OAI.FiberFunctorProof.regularEntry line 186
  17. lemma OAI.FiberFunctorProof.regularEntry_apply line 189
  18. lemma OAI.FiberFunctorProof.regularFirstColumn_eq_entry line 194
  19. abbrev OAI.FiberFunctorProof.regularTorusPoints line 197
  20. def OAI.FiberFunctorProof.regularTorusRestriction line 199
  21. lemma OAI.FiberFunctorProof.regularTorusRestriction_injective line 208
  22. def OAI.FiberFunctorProof.regularPlane line 216
  23. lemma OAI.FiberFunctorProof.regularPlane_evaluation line 220
  24. abbrev OAI.FiberFunctorProof.regularCoordinateLocalization line 233
  25. lemma OAI.FiberFunctorProof.regularTorusRestriction_coordinate_isUnit line 236
  26. def OAI.FiberFunctorProof.regularLocalizationEvaluation line 243
  27. lemma OAI.FiberFunctorProof.regularLocalizationEvaluation_algebraMap line 248
  28. def OAI.FiberFunctorProof.planeChartPullback line 254
  29. lemma OAI.FiberFunctorProof.planeChartPullback_algebraMap line 264
  30. def OAI.FiberFunctorProof.regularToPlaneTorus line 272
  31. lemma OAI.FiberFunctorProof.planeChartPullback_evaluation line 275
  32. def OAI.FiberFunctorProof.regularCoordinateInverse line 298
  33. lemma OAI.FiberFunctorProof.regularCoordinateInverse_evaluation line 301
  34. lemma OAI.FiberFunctorProof.regularLocalization_has_numerator line 315
  35. lemma OAI.FiberFunctorProof.coprime_denominator_glue line 330
  36. lemma OAI.FiberFunctorProof.regularFirstColumns_coprime line 351
  37. theorem OAI.FiberFunctorProof.regularTorus_glue line 365
  38. lemma OAI.FiberFunctorProof.subalgebra_polynomial_mem line 388
  39. lemma OAI.FiberFunctorProof.regularSL2_pullback_mem line 406
  40. def OAI.FiberFunctorProof.regularRightTranslation line 420
  41. lemma OAI.FiberFunctorProof.regularRightTranslation_apply line 432