OAI/RepresentationTheory/RestrictedTilting/AssociatedWeights.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Character transfer, numerator weights and associated-origin tilting.

  1. def OAI.FiberFunctorProof.characterFiniteSubmodule line 19
  2. lemma OAI.FiberFunctorProof.characterFinite_eigen line 29
  3. lemma OAI.FiberFunctorProof.characterFinite_map line 35
  4. lemma OAI.FiberFunctorProof.HasCharacterExpansions.of_surjective line 46
  5. lemma OAI.FiberFunctorProof.HasCharacterExpansions.of_injective line 54
  6. def OAI.FiberFunctorProof.diagonalPolynomialScale line 77
  7. lemma OAI.FiberFunctorProof.diagonalPolynomialScale_monomial line 81
  8. lemma OAI.FiberFunctorProof.diagonalPolynomialScale_coeff line 96
  9. def OAI.FiberFunctorProof.planeTorusPolynomial line 111
  10. lemma OAI.FiberFunctorProof.planeTorusPolynomial_coeff line 115
  11. lemma OAI.FiberFunctorProof.positive_plane_weight_dvd line 124
  12. def OAI.FiberFunctorProof.coordinateCharacter line 152
  13. lemma OAI.FiberFunctorProof.linearChange_diagonal line 155
  14. lemma OAI.FiberFunctorProof.leftCoordinateMatrix_diagonal line 160
  15. lemma OAI.FiberFunctorProof.coordinatePolynomial_torus_scale line 171
  16. lemma OAI.FiberFunctorProof.coordinatePolynomial_characters line 177
  17. lemma OAI.FiberFunctorProof.regularSL2_characters line 192
  18. lemma OAI.FiberFunctorProof.regularVector_characters line 204
  19. lemma OAI.FiberFunctorProof.associatedSections_characters line 225
  20. def OAI.FiberFunctorProof.planeTorusScale line 239
  21. lemma OAI.FiberFunctorProof.planeTorusScale_coordinate line 247
  22. lemma OAI.FiberFunctorProof.diagonalPolynomialScale_eval line 252
  23. lemma OAI.FiberFunctorProof.planeTorusPolynomial_eval line 265
  24. lemma OAI.FiberFunctorProof.planeXSection_torus line 277
  25. lemma OAI.FiberFunctorProof.associatedXChart_torus_evaluation line 292
  26. lemma OAI.FiberFunctorProof.associatedNumerator_weight line 302
  27. lemma OAI.FiberFunctorProof.gluedLattice_div_y line 333
  28. lemma OAI.FiberFunctorProof.associated_y_divisible line 358
  29. lemma OAI.FiberFunctorProof.associatedOrigin_weight_upper line 401
  30. theorem OAI.FiberFunctorProof.associatedOrigin_weights line 435
  31. def OAI.FiberFunctorProof.associatedOriginFD line 453
  32. theorem OAI.FiberFunctorProof.associatedOrigin_tilting line 459