OAI/RepresentationTheory/RestrictedTilting/ThetaTarget.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiberFunctorProof.ThetaTarget.linearChange line 19
  2. lemma OAI.FiberFunctorProof.ThetaTarget.linearChange_X line 23
  3. lemma OAI.FiberFunctorProof.ThetaTarget.linearChange_C line 28
  4. lemma OAI.FiberFunctorProof.ThetaTarget.linearChange_one line 34
  5. lemma OAI.FiberFunctorProof.ThetaTarget.linearChange_mul line 39
  6. lemma OAI.FiberFunctorProof.ThetaTarget.linearChange_homogeneous line 52
  7. def OAI.FiberFunctorProof.ThetaTarget.homogeneousRepresentation line 63
  8. abbrev OAI.FiberFunctorProof.ThetaTarget.SL2 line 83
  9. def OAI.FiberFunctorProof.ThetaTarget.IsRational line 86
  10. def OAI.FiberFunctorProof.ThetaTarget.dualMatrix line 93
  11. instance OAI.FiberFunctorProof.ThetaTarget.homogeneous_finite line 99
  12. def OAI.FiberFunctorProof.ThetaTarget.costandard line 104
  13. inductive OAI.FiberFunctorProof.ThetaTarget.HasGoodFiltration line 108
  14. def OAI.FiberFunctorProof.ThetaTarget.IsTilting line 116
  15. def OAI.FiberFunctorProof.ThetaTarget.steinberg line 120
  16. def OAI.FiberFunctorProof.ThetaTarget.unipotent line 124
  17. lemma OAI.FiberFunctorProof.ThetaTarget.unipotent_zero line 127
  18. lemma OAI.FiberFunctorProof.ThetaTarget.unipotent_add line 132
  19. def OAI.FiberFunctorProof.ThetaTarget.elementaryEmbedding line 140
  20. def OAI.FiberFunctorProof.ThetaTarget.restrictElementary line 146
  21. structure OAI.FiberFunctorProof.ThetaTarget.FiniteSymmetricTensorCategory line 159
  22. abbrev OAI.FiberFunctorProof.ThetaTarget.Tilting line 189
  23. abbrev OAI.FiberFunctorProof.ThetaTarget.tiltingInclusion line 192
  24. class OAI.FiberFunctorProof.ThetaTarget.TiltingTensorStructure line 197
  25. def OAI.FiberFunctorProof.ThetaTarget.steinbergIdeal line 213
  26. structure OAI.FiberFunctorProof.ThetaTarget.TiltingFunctor line 220
  27. structure OAI.FiberFunctorProof.ThetaTarget.ExactTensorFunctor line 230
  28. structure OAI.FiberFunctorProof.ThetaTarget.FiberFunctor line 242
  29. def OAI.FiberFunctorProof.ThetaTarget.MonoidallyIsomorphic line 248
  30. def OAI.FiberFunctorProof.ThetaTarget.HasSteinbergKernel line 254
  31. structure OAI.FiberFunctorProof.ThetaTarget.VerlindePresentation line 260
  32. def OAI.FiberFunctorProof.ThetaTarget.MainTheorem line 274
  33. instance OAI.FiberFunctorProof.ThetaTarget.elementaryRestrictionMonoidal line 287
  34. def OAI.FiberFunctorProof.ThetaTarget.HigherThetaConstruction line 311