OAI/RepresentationTheory/RestrictedTilting/FaithfulTarget.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiberFunctorProof.FaithfulTarget.linearChange line 18
  2. lemma OAI.FiberFunctorProof.FaithfulTarget.linearChange_X line 22
  3. lemma OAI.FiberFunctorProof.FaithfulTarget.linearChange_C line 27
  4. lemma OAI.FiberFunctorProof.FaithfulTarget.linearChange_one line 33
  5. lemma OAI.FiberFunctorProof.FaithfulTarget.linearChange_mul line 38
  6. lemma OAI.FiberFunctorProof.FaithfulTarget.linearChange_homogeneous line 51
  7. def OAI.FiberFunctorProof.FaithfulTarget.homogeneousRepresentation line 62
  8. abbrev OAI.FiberFunctorProof.FaithfulTarget.SL2 line 83
  9. def OAI.FiberFunctorProof.FaithfulTarget.IsRational line 86
  10. def OAI.FiberFunctorProof.FaithfulTarget.dualMatrix line 93
  11. instance OAI.FiberFunctorProof.FaithfulTarget.homogeneous_finite line 99
  12. def OAI.FiberFunctorProof.FaithfulTarget.costandard line 104
  13. inductive OAI.FiberFunctorProof.FaithfulTarget.HasGoodFiltration line 108
  14. def OAI.FiberFunctorProof.FaithfulTarget.IsTilting line 116
  15. def OAI.FiberFunctorProof.FaithfulTarget.steinberg line 120
  16. def OAI.FiberFunctorProof.FaithfulTarget.unipotent line 124
  17. lemma OAI.FiberFunctorProof.FaithfulTarget.unipotent_zero line 127
  18. lemma OAI.FiberFunctorProof.FaithfulTarget.unipotent_add line 132
  19. def OAI.FiberFunctorProof.FaithfulTarget.elementaryEmbedding line 140
  20. def OAI.FiberFunctorProof.FaithfulTarget.restrictElementary line 146
  21. structure OAI.FiberFunctorProof.FaithfulTarget.FiniteSymmetricTensorCategory line 160
  22. abbrev OAI.FiberFunctorProof.FaithfulTarget.Tilting line 190
  23. abbrev OAI.FiberFunctorProof.FaithfulTarget.tiltingInclusion line 193
  24. class OAI.FiberFunctorProof.FaithfulTarget.TiltingTensorStructure line 198
  25. def OAI.FiberFunctorProof.FaithfulTarget.steinbergIdeal line 214
  26. structure OAI.FiberFunctorProof.FaithfulTarget.TiltingFunctor line 221
  27. structure OAI.FiberFunctorProof.FaithfulTarget.ExactTensorFunctor line 231
  28. structure OAI.FiberFunctorProof.FaithfulTarget.FiberFunctor line 243
  29. def OAI.FiberFunctorProof.FaithfulTarget.MonoidallyIsomorphic line 249
  30. def OAI.FiberFunctorProof.FaithfulTarget.HasSteinbergKernel line 255
  31. structure OAI.FiberFunctorProof.FaithfulTarget.VerlindePresentation line 261
  32. def OAI.FiberFunctorProof.FaithfulTarget.MainTheorem line 275