OAI/RepresentationTheory/RestrictedTilting/FrobeniusTensor.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Binary Frobenius multiplication and Steinberg twists of filtrations.

  1. lemma OAI.FiberFunctorProof.expand_homogeneous line 19
  2. def OAI.FiberFunctorProof.binaryFrobeniusMultiply line 25
  3. lemma OAI.FiberFunctorProof.binaryFrobeniusMultiply_tmul line 36
  4. lemma OAI.FiberFunctorProof.binaryFrobeniusMultiply_surjective line 41
  5. lemma OAI.FiberFunctorProof.binaryFrobeniusMultiply_bijective line 67
  6. def OAI.FiberFunctorProof.frobeniusSL2 line 83
  7. lemma OAI.FiberFunctorProof.dualMatrix_frobeniusSL2 line 86
  8. lemma OAI.FiberFunctorProof.linearChange_expand line 93
  9. lemma OAI.FiberFunctorProof.binaryFrobeniusMultiply_intertwines line 102
  10. def OAI.FiberFunctorProof.frobeniusTwist line 128
  11. instance OAI.FiberFunctorProof.(instance at line 131) line 131
  12. lemma OAI.FiberFunctorProof.frobeniusTwist_shortExact line 134
  13. def OAI.FiberFunctorProof.frobeniusCostandardHom line 141
  14. def OAI.FiberFunctorProof.frobeniusCostandardIso line 146
  15. theorem OAI.FiberFunctorProof.HasGoodFiltration.steinberg_frobenius line 156
  16. lemma OAI.FiberFunctorProof.IsRational.frobenius line 173
  17. def OAI.FiberFunctorProof.frobeniusDualIso line 186
  18. theorem OAI.FiberFunctorProof.IsTilting.steinberg_frobenius line 206