OAI/RepresentationTheory/RestrictedTilting/TiltingBounds.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Highest weights, irreducible representations and bounded-weight tilting.

  1. def OAI.FiberFunctorProof.steinbergStepIso line 19
  2. def OAI.FiberFunctorProof.frobeniusTensorIso line 32
  3. theorem OAI.FiberFunctorProof.steinberg_tensor_simple_tilting line 38
  4. def OAI.FiberFunctorProof.weylReflection line 80
  5. lemma OAI.FiberFunctorProof.diagonalTorus_weylReflection line 83
  6. lemma OAI.FiberFunctorProof.reflected_weight line 91
  7. lemma OAI.FiberFunctorProof.weights_between_of_upper line 102
  8. lemma OAI.FiberFunctorProof.integer_coefficient_eigen line 119
  9. lemma OAI.FiberFunctorProof.exists_highest_in_bound line 137
  10. lemma OAI.FiberFunctorProof.exists_costandard_dual_embedding line 184
  11. lemma OAI.FiberFunctorProof.exists_socle_dual_embedding line 208
  12. lemma OAI.FiberFunctorProof.dual_eval_surjective line 245
  13. lemma OAI.FiberFunctorProof.exists_simple_dual_surjection line 251
  14. lemma OAI.FiberFunctorProof.irreducible_iso_simple_dual line 270
  15. theorem OAI.FiberFunctorProof.irreducible_eq_simple_dual line 304
  16. lemma OAI.FiberFunctorProof.hasWeightsBetween_of_injective line 328
  17. lemma OAI.FiberFunctorProof.hasWeightsBetween_of_surjective line 341
  18. lemma OAI.FiberFunctorProof.fdrep_isZero_of_subsingleton line 352
  19. lemma OAI.FiberFunctorProof.IsTilting.of_subsingleton line 359
  20. lemma OAI.FiberFunctorProof.IsTilting.extension line 367
  21. lemma OAI.FiberFunctorProof.exists_proper_subrepresentation line 382
  22. lemma OAI.FiberFunctorProof.fdrep_proper_shortExact line 398
  23. theorem OAI.FiberFunctorProof.fdrep_induction line 426
  24. lemma OAI.FiberFunctorProof.steinberg_tensor_simple_dual_tilting line 451
  25. lemma OAI.FiberFunctorProof.steinberg_tensor_irreducible_tilting line 459
  26. theorem OAI.FiberFunctorProof.bounded_weights_tilting line 469