OAI/RepresentationTheory/RestrictedTilting/OriginCoordinates.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Plane-origin coordinate rings, stalk lattices and overlap evaluation.

  1. abbrev OAI.FiberFunctorProof.planeCoordinateRing line 17
  2. def OAI.FiberFunctorProof.planeOriginIdeal line 19
  3. instance OAI.FiberFunctorProof.planeOriginIdeal_isMaximal line 22
  4. lemma OAI.FiberFunctorProof.planeOriginIdeal_eq_span line 26
  5. abbrev OAI.FiberFunctorProof.planeOriginRing line 44
  6. abbrev OAI.FiberFunctorProof.planeOriginCoordinate line 46
  7. lemma OAI.FiberFunctorProof.planeOriginCoordinate_ne_zero line 49
  8. lemma OAI.FiberFunctorProof.planeOrigin_maximalIdeal line 54
  9. lemma OAI.FiberFunctorProof.planeOriginCoordinate_prime line 66
  10. lemma OAI.FiberFunctorProof.planeOriginCoordinates_relPrime line 74
  11. instance OAI.FiberFunctorProof.planeOriginRing_gcd line 88
  12. example OAI.FiberFunctorProof.(example at line 91) line 91
  13. example OAI.FiberFunctorProof.(example at line 92) line 92
  14. lemma OAI.FiberFunctorProof.linearEquiv_map_base_smul line 99
  15. lemma OAI.FiberFunctorProof.powerLocalization_idem line 103
  16. lemma OAI.FiberFunctorProof.powerLocalization_equiv_map line 110
  17. theorem OAI.FiberFunctorProof.gluedLattice_xChart line 132
  18. theorem OAI.FiberFunctorProof.gluedLattice_yChart line 155
  19. abbrev OAI.FiberFunctorProof.planeOriginFractionField line 188
  20. instance OAI.FiberFunctorProof.planeOriginFraction_tower line 190
  21. instance OAI.FiberFunctorProof.planeOriginFraction_isFractionRing line 195
  22. def OAI.FiberFunctorProof.planeStalkTransition line 201
  23. def OAI.FiberFunctorProof.planeAssociatedLattice line 210
  24. lemma OAI.FiberFunctorProof.planeOrigin_product_ne_zero line 216
  25. lemma OAI.FiberFunctorProof.planeStalkTransition_denominator line 224
  26. lemma OAI.FiberFunctorProof.planeStalkTransition_symm_denominator line 230
  27. theorem OAI.FiberFunctorProof.planeAssociatedLattice_finite_free line 241
  28. theorem OAI.FiberFunctorProof.planeAssociatedLattice_xChart line 251
  29. theorem OAI.FiberFunctorProof.planeAssociatedLattice_yChart line 256
  30. abbrev OAI.FiberFunctorProof.planeOverlapRing line 266
  31. lemma OAI.FiberFunctorProof.planeTorusEvaluation_product_isUnit line 270
  32. def OAI.FiberFunctorProof.planeOverlapEvaluation line 276
  33. lemma OAI.FiberFunctorProof.planeOverlapEvaluation_algebraMap line 281
  34. theorem OAI.FiberFunctorProof.planeOverlapEvaluation_injective line 286
  35. lemma OAI.FiberFunctorProof.planeOverlapCoordinate_isUnit line 303
  36. def OAI.FiberFunctorProof.planeChartToOverlap line 311
  37. lemma OAI.FiberFunctorProof.planeChartToOverlap_algebraMap line 318
  38. lemma OAI.FiberFunctorProof.planeChartToOverlap_evaluation line 325
  39. lemma OAI.FiberFunctorProof.planeChartToOverlap_injective line 338