OAI/RepresentationTheory/RestrictedTilting/BinarySequences.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Binary multiplication exact sequences and tensor closure of good filtrations.

  1. abbrev OAI.FiberFunctorProof.BiBinary line 20
  2. abbrev OAI.FiberFunctorProof.BiPolynomial line 21
  3. instance OAI.FiberFunctorProof.biBinaryAddCommGroup line 23
  4. def OAI.FiberFunctorProof.binaryMulX line 26
  5. def OAI.FiberFunctorProof.biBinaryEmbed line 32
  6. lemma OAI.FiberFunctorProof.biBinaryEmbed_injective line 35
  7. def OAI.FiberFunctorProof.determinantMap line 40
  8. def OAI.FiberFunctorProof.biDeterminant line 44
  9. lemma OAI.FiberFunctorProof.embed_determinantMap line 47
  10. lemma OAI.FiberFunctorProof.biDeterminant_ne_zero line 57
  11. lemma OAI.FiberFunctorProof.determinantMap_injective line 66
  12. def OAI.FiberFunctorProof.binaryMultiply line 73
  13. lemma OAI.FiberFunctorProof.binaryMultiply_tmul line 82
  14. lemma OAI.FiberFunctorProof.binaryMultiply_determinantMap line 85
  15. lemma OAI.FiberFunctorProof.binaryMultiply_surjective line 96
  16. lemma OAI.FiberFunctorProof.binaryMultiply_exact line 111
  17. def OAI.FiberFunctorProof.biLinearChange line 133
  18. lemma OAI.FiberFunctorProof.biLinearChange_determinant line 137
  19. def OAI.FiberFunctorProof.biBinaryAction line 147
  20. lemma OAI.FiberFunctorProof.biBinaryEmbed_action line 151
  21. lemma OAI.FiberFunctorProof.determinantMap_equivariant line 158
  22. lemma OAI.FiberFunctorProof.binaryMultiply_equivariant line 166
  23. lemma OAI.FiberFunctorProof.dualMatrix_det line 177
  24. def OAI.FiberFunctorProof.costandardDeterminant line 186
  25. def OAI.FiberFunctorProof.costandardMultiply line 192
  26. lemma OAI.FiberFunctorProof.costandardDeterminant_multiply line 197
  27. def OAI.FiberFunctorProof.costandardTensorSequence line 204
  28. lemma OAI.FiberFunctorProof.costandardTensorSequence_shortExact line 208
  29. lemma OAI.FiberFunctorProof.costandardMultiply_isIso_of_zero line 214
  30. theorem OAI.FiberFunctorProof.costandard_tensor_hasGoodFiltration line 234
  31. lemma OAI.FiberFunctorProof.HasGoodFiltration.tensor_costandard line 253
  32. theorem OAI.FiberFunctorProof.HasGoodFiltration.tensor line 266
  33. def OAI.FiberFunctorProof.fdrepBidual line 277
  34. lemma OAI.FiberFunctorProof.IsRational.of_iso line 282
  35. lemma OAI.FiberFunctorProof.IsTilting.of_iso line 287
  36. theorem OAI.FiberFunctorProof.IsTilting.tensor line 298
  37. theorem OAI.FiberFunctorProof.IsTilting.dual line 304