OAI/RepresentationTheory/RestrictedTilting/RepresentationMaps.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Kernels, ranges, quotients and factorization of finite-dimensional representations.

  1. def OAI.FiberFunctorProof.fdrepHom line 17
  2. def OAI.FiberFunctorProof.fdrepForget line 24
  3. instance OAI.FiberFunctorProof.(instance at line 27) line 27
  4. instance OAI.FiberFunctorProof.(instance at line 31) line 31
  5. instance OAI.FiberFunctorProof.(instance at line 35) line 35
  6. instance OAI.FiberFunctorProof.(instance at line 39) line 39
  7. lemma OAI.FiberFunctorProof.fdrep_shortExact line 42
  8. abbrev OAI.FiberFunctorProof.fdrepLinear line 63
  9. lemma OAI.FiberFunctorProof.fdrepLinear_comm line 65
  10. lemma OAI.FiberFunctorProof.fdrep_injective line 69
  11. lemma OAI.FiberFunctorProof.fdrep_surjective line 73
  12. lemma OAI.FiberFunctorProof.fdrep_exact line 77
  13. def OAI.FiberFunctorProof.fdrepKernelSub line 82
  14. def OAI.FiberFunctorProof.fdrepKernel line 88
  15. def OAI.FiberFunctorProof.fdrepKernelι line 91
  16. def OAI.FiberFunctorProof.fdrepKernelLift line 94
  17. lemma OAI.FiberFunctorProof.fdrepKernelLift_ι line 104
  18. def OAI.FiberFunctorProof.linearFactor line 108
  19. lemma OAI.FiberFunctorProof.linearFactor_comp line 114
  20. def OAI.FiberFunctorProof.fdrepFactor line 122
  21. lemma OAI.FiberFunctorProof.fdrepFactor_comp line 130
  22. lemma OAI.FiberFunctorProof.fdrep_splice line 139
  23. lemma OAI.FiberFunctorProof.fdrepDesc_range line 219
  24. def OAI.FiberFunctorProof.fdrepDesc line 232
  25. lemma OAI.FiberFunctorProof.fdrepDesc_comp line 248
  26. def OAI.FiberFunctorProof.fdrepRangeSub line 265
  27. def OAI.FiberFunctorProof.fdrepQuotient line 271
  28. def OAI.FiberFunctorProof.fdrepQuotientπ line 275
  29. lemma OAI.FiberFunctorProof.fdrepQuotientπ_surjective line 280
  30. lemma OAI.FiberFunctorProof.fdrepQuotientπ_eq_zero line 284