OAI/RepresentationTheory/RestrictedTilting/SL2Definitions.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Polynomial actions, rational SL₂ representations and tilting definitions.

  1. def OAI.FiberFunctorProof.linearChange line 19
  2. lemma OAI.FiberFunctorProof.linearChange_X line 23
  3. lemma OAI.FiberFunctorProof.linearChange_C line 28
  4. lemma OAI.FiberFunctorProof.linearChange_one line 34
  5. lemma OAI.FiberFunctorProof.linearChange_mul line 39
  6. lemma OAI.FiberFunctorProof.linearChange_homogeneous line 52
  7. def OAI.FiberFunctorProof.homogeneousRepresentation line 63
  8. abbrev OAI.FiberFunctorProof.SL2 line 84
  9. def OAI.FiberFunctorProof.IsRational line 87
  10. def OAI.FiberFunctorProof.dualMatrix line 94
  11. instance OAI.FiberFunctorProof.homogeneous_finite line 100
  12. def OAI.FiberFunctorProof.costandard line 105
  13. inductive OAI.FiberFunctorProof.HasGoodFiltration line 109
  14. def OAI.FiberFunctorProof.IsTilting line 117
  15. def OAI.FiberFunctorProof.steinberg line 121
  16. def OAI.FiberFunctorProof.unipotent line 125
  17. lemma OAI.FiberFunctorProof.unipotent_zero line 128
  18. lemma OAI.FiberFunctorProof.unipotent_add line 133
  19. def OAI.FiberFunctorProof.elementaryEmbedding line 141
  20. def OAI.FiberFunctorProof.restrictElementary line 147