OAI/RepresentationTheory/RestrictedTilting/StandardLifts.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Highest coefficients, Bruhat intertwiners and standard module lifts.

  1. def OAI.FiberFunctorProof.standardRepresentation line 18
  2. def OAI.FiberFunctorProof.standardBasis line 23
  3. def OAI.FiberFunctorProof.standardHighest line 25
  4. lemma OAI.FiberFunctorProof.eval_linearChange line 27
  5. lemma OAI.FiberFunctorProof.standardHighest_apply line 38
  6. lemma OAI.FiberFunctorProof.unipotent_inv line 61
  7. lemma OAI.FiberFunctorProof.dualMatrix_inv line 66
  8. lemma OAI.FiberFunctorProof.standardHighest_upper_fixed line 71
  9. lemma OAI.FiberFunctorProof.standardHighest_lower_orbit line 87
  10. lemma OAI.FiberFunctorProof.standardBasis_weight line 111
  11. lemma OAI.FiberFunctorProof.standardHighest_weight line 132
  12. lemma OAI.FiberFunctorProof.linearIndependent_powerFunctionsOn line 139
  13. lemma OAI.FiberFunctorProof.upper_lower_bruhat line 158
  14. lemma OAI.FiberFunctorProof.lower_eq_transvection line 172
  15. lemma OAI.FiberFunctorProof.upper_eq_transvection line 179
  16. lemma OAI.FiberFunctorProof.intertwiner_of_root_groups line 187
  17. lemma OAI.FiberFunctorProof.standard_lower_orbit_ext line 207
  18. lemma OAI.FiberFunctorProof.finsupp_sum_fin_of_degree_bound line 226
  19. def OAI.FiberFunctorProof.highestCoefficientMap line 240
  20. lemma OAI.FiberFunctorProof.highestCoefficientMap_lower_orbit line 245
  21. lemma OAI.FiberFunctorProof.highestCoefficientMap_highest line 254
  22. lemma OAI.FiberFunctorProof.highestCoefficientMap_lower_intertwines line 262
  23. lemma OAI.FiberFunctorProof.infinite_bruhat_parameters line 278
  24. lemma OAI.FiberFunctorProof.upper_lower_on_highest line 292
  25. lemma OAI.FiberFunctorProof.highestCoefficientMap_upper_intertwines line 302
  26. theorem OAI.FiberFunctorProof.exists_standard_lift line 325