OAI/RepresentationTheory/RestrictedTilting/PolynomialActions.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Polynomial additive actions and associated polynomial sections.

  1. lemma OAI.FiberFunctorProof.map_aeval_polynomial line 17
  2. def OAI.FiberFunctorProof.polynomialMatrixEval line 29
  3. lemma OAI.FiberFunctorProof.polynomialMatrixEval_map line 34
  4. theorem OAI.FiberFunctorProof.polynomialMatrixEval_add line 44
  5. lemma OAI.FiberFunctorProof.polynomialMatrixEval_zero line 66
  6. def OAI.FiberFunctorProof.polynomialAdditiveRepresentation line 82
  7. lemma OAI.FiberFunctorProof.additive_rep_apply_add line 102
  8. def OAI.FiberFunctorProof.associatedLocalExpression line 109
  9. lemma OAI.FiberFunctorProof.associatedLocalExpression_evaluation line 118
  10. def OAI.FiberFunctorProof.associatedTorusValue line 151
  11. lemma OAI.FiberFunctorProof.associatedChartPair_local_compatible line 157
  12. lemma OAI.FiberFunctorProof.secondColumn_unipotent_mul line 179
  13. def OAI.FiberFunctorProof.regularTorusRightUnipotent line 185
  14. lemma OAI.FiberFunctorProof.associatedTorusValue_unipotent line 190
  15. def OAI.FiberFunctorProof.regularVectorCombination line 208
  16. lemma OAI.FiberFunctorProof.regularVectorCombination_evaluation line 213
  17. theorem OAI.FiberFunctorProof.associatedChartPair_glue line 227
  18. instance OAI.FiberFunctorProof.regularPlaneAlgebra line 310
  19. instance OAI.FiberFunctorProof.regularPlaneScalarTower line 314
  20. lemma OAI.FiberFunctorProof.regularPlane_algebraMap line 318
  21. lemma OAI.FiberFunctorProof.regularVector_plane_smul line 322
  22. lemma OAI.FiberFunctorProof.associatedSections_plane_smul_mem line 334
  23. def OAI.FiberFunctorProof.associatedPolynomialSections line 341
  24. instance OAI.FiberFunctorProof.associatedSectionsAddCommGroup line 348
  25. instance OAI.FiberFunctorProof.(instance at line 352) line 352
  26. instance OAI.FiberFunctorProof.(instance at line 356) line 356
  27. instance OAI.FiberFunctorProof.associatedSectionsScalarTower line 360
  28. def OAI.FiberFunctorProof.associatedXChartPolynomial line 365