OAI/RepresentationTheory/RestrictedTilting/RegularActions.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Polynomial coordinate representations and associated sections.

  1. def OAI.FiberFunctorProof.leftCoordinateMatrix line 18
  2. def OAI.FiberFunctorProof.coordinatePolynomialRepresentation line 23
  3. lemma OAI.FiberFunctorProof.coordinatePolynomial_rational line 29
  4. def OAI.FiberFunctorProof.coordinateEvaluation line 40
  5. lemma OAI.FiberFunctorProof.coordinateEvaluation_apply line 44
  6. lemma OAI.FiberFunctorProof.coordinatePolynomial_evaluation line 54
  7. def OAI.FiberFunctorProof.regularSL2Functions line 69
  8. def OAI.FiberFunctorProof.regularSL2Representation line 72
  9. def OAI.FiberFunctorProof.coordinateToRegular line 87
  10. lemma OAI.FiberFunctorProof.coordinateToRegular_surjective line 91
  11. lemma OAI.FiberFunctorProof.regularSL2_rational line 96
  12. def OAI.FiberFunctorProof.regularVectorRepresentation line 107
  13. lemma OAI.FiberFunctorProof.regularVector_rational line 127
  14. def OAI.FiberFunctorProof.regularVectorEvaluation line 148
  15. def OAI.FiberFunctorProof.associatedSectionsSubmodule line 158
  16. def OAI.FiberFunctorProof.associatedSectionsSubrepresentation line 171
  17. def OAI.FiberFunctorProof.associatedSectionsRepresentation line 181
  18. lemma OAI.FiberFunctorProof.associatedSections_rational line 185
  19. def OAI.FiberFunctorProof.regularFirstColumn line 193
  20. lemma OAI.FiberFunctorProof.regularFirstColumn_apply line 196
  21. lemma OAI.FiberFunctorProof.firstColumn_unipotent_mul line 201
  22. def OAI.FiberFunctorProof.regularVectorCoordinateMul line 207
  23. lemma OAI.FiberFunctorProof.regularVectorCoordinateMul_evaluation line 214
  24. lemma OAI.FiberFunctorProof.associatedSections_coordinate_mul_mem line 224
  25. def OAI.FiberFunctorProof.associatedCoordinateMul line 231
  26. lemma OAI.FiberFunctorProof.associatedCoordinateMul_action line 239
  27. def OAI.FiberFunctorProof.associatedOriginRelations line 259
  28. lemma OAI.FiberFunctorProof.associatedOriginRelations_stable line 264
  29. def OAI.FiberFunctorProof.quotientRationalModule line 283
  30. lemma OAI.FiberFunctorProof.quotientRationalModule_rational line 289
  31. def OAI.FiberFunctorProof.associatedOriginRep line 297
  32. lemma OAI.FiberFunctorProof.associatedOrigin_rational line 304