OAI/RepresentationTheory/RestrictedTilting/GlobalLattices.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Fraction charts, global lattices and finite origin quotients.

  1. abbrev OAI.FiberFunctorProof.planeFractionField line 15
  2. instance OAI.FiberFunctorProof.planeCoordinateRing_gcd line 17
  3. lemma OAI.FiberFunctorProof.planeCoordinates_relPrime line 20
  4. lemma OAI.FiberFunctorProof.planeFractionCoordinate_ne_zero line 26
  5. def OAI.FiberFunctorProof.planeChartToFraction line 31
  6. lemma OAI.FiberFunctorProof.planeChartToFraction_algebraMap line 37
  7. lemma OAI.FiberFunctorProof.planeChartToFraction_injective line 43
  8. def OAI.FiberFunctorProof.planeChartToFractionLinear line 58
  9. def OAI.FiberFunctorProof.planeOverlapToFraction line 67
  10. lemma OAI.FiberFunctorProof.planeOverlapToFraction_algebraMap line 76
  11. lemma OAI.FiberFunctorProof.planeChartToFraction_overlap line 84
  12. def OAI.FiberFunctorProof.planeOverlapInverse line 97
  13. lemma OAI.FiberFunctorProof.planeOverlapInverse_evaluation line 100
  14. lemma OAI.FiberFunctorProof.planeOverlapInverse_fraction line 111
  15. lemma OAI.FiberFunctorProof.planeChartVector_mem line 130
  16. lemma OAI.FiberFunctorProof.planeChartPair_fraction_relation line 149
  17. def OAI.FiberFunctorProof.planeGlobalTransition line 181
  18. def OAI.FiberFunctorProof.planeGlobalLattice line 187
  19. lemma OAI.FiberFunctorProof.planeFraction_product_ne_zero line 192
  20. lemma OAI.FiberFunctorProof.planeGlobalTransition_denominator line 198
  21. lemma OAI.FiberFunctorProof.planeGlobalLattice_finite line 204
  22. lemma OAI.FiberFunctorProof.planeChartPair_mem_globalLattice line 209
  23. lemma OAI.FiberFunctorProof.associatedPolynomial_zero line 238
  24. lemma OAI.FiberFunctorProof.associatedPolynomial_add line 246
  25. def OAI.FiberFunctorProof.associatedFractionChart line 252
  26. lemma OAI.FiberFunctorProof.associatedFractionChart_injective line 259
  27. lemma OAI.FiberFunctorProof.associatedFractionChart_mem line 265
  28. theorem OAI.FiberFunctorProof.associatedSections_finite line 277
  29. lemma OAI.FiberFunctorProof.originQuotient_polynomial_smul line 293
  30. theorem OAI.FiberFunctorProof.originQuotient_finite line 311