OAI/RepresentationTheory/RestrictedTilting/SimpleModules.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Costandard socles and the digit factorization of simple SL₂ modules.

  1. lemma OAI.FiberFunctorProof.independent_sum_mem line 18
  2. lemma OAI.FiberFunctorProof.costandard_weight_component_mem line 31
  3. lemma OAI.FiberFunctorProof.costandard_basis_upper_orbit line 62
  4. lemma OAI.FiberFunctorProof.costandardHighest_mem_of_basis_mem line 92
  5. lemma OAI.FiberFunctorProof.costandardHighest_mem_of_ne_bot line 111
  6. def OAI.FiberFunctorProof.standardCostandardMap line 128
  7. lemma OAI.FiberFunctorProof.standardCostandardMap_basis line 134
  8. lemma OAI.FiberFunctorProof.standardCostandardMap_highest line 139
  9. def OAI.FiberFunctorProof.costandardSocle line 148
  10. lemma OAI.FiberFunctorProof.costandardHighest_mem_socle line 152
  11. lemma OAI.FiberFunctorProof.costandardSocle_le_of_highest_mem line 156
  12. lemma OAI.FiberFunctorProof.costandardSocle_le_of_ne_bot line 182
  13. lemma OAI.FiberFunctorProof.costandardSocle_ne_bot line 187
  14. lemma OAI.FiberFunctorProof.binaryBasis_mem_costandardSocle line 193
  15. lemma OAI.FiberFunctorProof.costandardSocle_eq_top line 207
  16. def OAI.FiberFunctorProof.simpleSL2 line 217
  17. lemma OAI.FiberFunctorProof.simpleSL2_rational line 220
  18. def OAI.FiberFunctorProof.simpleCostandardι line 225
  19. lemma OAI.FiberFunctorProof.simpleSL2_eq_costandard_of_choose line 228
  20. lemma OAI.FiberFunctorProof.simpleSL2_irreducible line 240
  21. def OAI.FiberFunctorProof.binaryDigitMultiply line 283
  22. lemma OAI.FiberFunctorProof.binaryDigitMultiply_basis line 294
  23. lemma OAI.FiberFunctorProof.digitIndex_injective line 310
  24. lemma OAI.FiberFunctorProof.binaryDigitMultiply_injective line 322
  25. lemma OAI.FiberFunctorProof.choose_digit_cast line 340
  26. lemma OAI.FiberFunctorProof.binaryDigitMultiply_intertwines line 350
  27. lemma OAI.FiberFunctorProof.binaryDigitMultiply_mem_socle line 376
  28. def OAI.FiberFunctorProof.binarySocleDigitMultiply line 402
  29. lemma OAI.FiberFunctorProof.binarySocleDigitMultiply_injective line 408
  30. lemma OAI.FiberFunctorProof.binarySocleDigitMultiply_mem line 414
  31. lemma OAI.FiberFunctorProof.binarySocleDigitMultiply_intertwines line 423
  32. lemma OAI.FiberFunctorProof.binarySocleDigitMultiply_range line 435
  33. def OAI.FiberFunctorProof.simpleDigitIso line 454