OAI/RepresentationTheory/RestrictedTilting/ExtensionSplitting.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Representation extension splitting, duality and good filtrations.

  1. lemma OAI.FiberFunctorProof.fdrep_hom_ext line 18
  2. lemma OAI.FiberFunctorProof.fdrep_comp_apply line 24
  3. lemma OAI.FiberFunctorProof.fdrep_id_apply line 27
  4. lemma OAI.FiberFunctorProof.fdrep_zero_apply line 30
  5. def OAI.FiberFunctorProof.RepExtensionSplit line 35
  6. lemma OAI.FiberFunctorProof.fdrep_quotient_splice line 40
  7. lemma OAI.FiberFunctorProof.fdrep_kernel_splice line 123
  8. theorem OAI.FiberFunctorProof.RepExtensionSplit.extension_left line 192
  9. lemma OAI.FiberFunctorProof.fgmodule_mate_apply line 224
  10. lemma OAI.FiberFunctorProof.fdrep_dual_repr line 239
  11. def OAI.FiberFunctorProof.fdrepDualMap line 257
  12. lemma OAI.FiberFunctorProof.fdrepDualMap_zero_comp line 267
  13. lemma OAI.FiberFunctorProof.fdrep_dual_shortExact line 280
  14. theorem OAI.FiberFunctorProof.RepExtensionSplit.of_dual line 297
  15. abbrev OAI.FiberFunctorProof.RationalExtensionSplit line 329
  16. lemma OAI.FiberFunctorProof.rationalExtensionSplit_extension_left line 332
  17. lemma OAI.FiberFunctorProof.rationalExtensionSplit_of_dual line 342
  18. lemma OAI.FiberFunctorProof.rationalExtensionSplit_zero line 348
  19. theorem OAI.FiberFunctorProof.costandard_standard_extension_split line 359
  20. theorem OAI.FiberFunctorProof.good_standard_extension_split line 378
  21. theorem OAI.FiberFunctorProof.good_weyl_extension_split line 389
  22. lemma OAI.FiberFunctorProof.HasGoodFiltration.of_iso line 404
  23. lemma OAI.FiberFunctorProof.costandard_hasGoodFiltration line 418
  24. lemma OAI.FiberFunctorProof.fdrepHom_isIso_of_bijective line 429