OAI/RepresentationTheory/RestrictedTilting/SteinbergDuality.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Standard-costandard maps, binomial coefficients and Steinberg self-duality.

  1. def OAI.FiberFunctorProof.costandardHighest line 18
  2. lemma OAI.FiberFunctorProof.costandardHighest_weight line 21
  3. lemma OAI.FiberFunctorProof.costandardHighest_lower_orbit line 28
  4. theorem OAI.FiberFunctorProof.exists_standard_costandard_map line 59
  5. theorem OAI.FiberFunctorProof.costandard_self_dual_of_choose_ne_zero line 88
  6. theorem OAI.FiberFunctorProof.costandard_tilting_of_choose_ne_zero line 117
  7. lemma OAI.FiberFunctorProof.choose_cast_ne_zero_of_lt_char line 130
  8. lemma OAI.FiberFunctorProof.choose_prime_power_cast_eq_zero line 141
  9. theorem OAI.FiberFunctorProof.choose_prime_power_sub_one_cast line 150
  10. lemma OAI.FiberFunctorProof.choose_prime_power_sub_one_ne_zero line 165
  11. theorem OAI.FiberFunctorProof.small_costandard_tilting line 179
  12. theorem OAI.FiberFunctorProof.steinberg_tilting line 185
  13. theorem OAI.FiberFunctorProof.steinberg_self_dual line 189