OAI/RingTheory/Tachikawa/StableLift.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Tachikawa.ordinary_inAdd_factorization_pf_zero line 13
  2. lemma OAI.Tachikawa.characterBimoduleMap_not_inAdd_factor line 39
  3. theorem OAI.Tachikawa.characterBimoduleMap_not_derived_perfect_factor line 50
  4. def OAI.Tachikawa.Construction.inducedSocleMap line 73
  5. lemma OAI.Tachikawa.Construction.inducedSocleMap_square line 82
  6. theorem OAI.Tachikawa.Construction.inducedSocleMap_not_derived_perfect_factor line 94
  7. def OAI.Tachikawa.Construction.finiteU line 139
  8. lemma OAI.Tachikawa.Construction.inducedSocleMap_high_lift_nonzero line 146
  9. theorem OAI.Tachikawa.Construction.inducedSocleMap_stably_nonzero_lift line 159
  10. lemma OAI.Tachikawa.finiteResolutionLift line 182
  11. lemma OAI.Tachikawa.lift_composite_eq line 192
  12. def OAI.Tachikawa.HomBimodule.underlyingLinearEquiv line 203
  13. instance OAI.Tachikawa.HomBimodule.(instance at line 210) line 210
  14. def OAI.Tachikawa.Construction.xObj line 217
  15. def OAI.Tachikawa.Construction.xUnderlyingLinear line 219
  16. instance OAI.Tachikawa.Construction.(instance at line 229) line 229
  17. def OAI.Tachikawa.Construction.finiteS line 232
  18. def OAI.Tachikawa.Construction.inducedRepresentationMap line 241
  19. lemma OAI.Tachikawa.Construction.inducedRepresentation_socle line 248
  20. theorem OAI.Tachikawa.Construction.separated_stably_nonzero_lifts line 252
  21. lemma OAI.Tachikawa.SymmetrizingForm.syzygyPair_natural line 297
  22. theorem OAI.Tachikawa.SymmetrizingForm.exists_nonzero_postcomposition line 305
  23. lemma OAI.Tachikawa.projectiveFactors_conjugate_iff line 336
  24. theorem OAI.Tachikawa.SymmetrizingForm.exists_syzygy_postcomposition line 355
  25. def OAI.Tachikawa.FiniteModule.syzygyInclusion line 373
  26. lemma OAI.Tachikawa.FiniteModule.syzygyInclusion_injective line 375
  27. lemma OAI.Tachikawa.FiniteModule.syzygyInclusion_exact line 377
  28. def OAI.Tachikawa.FiniteModule.cosyzygyProjection line 381
  29. lemma OAI.Tachikawa.FiniteModule.cosyzygyProjection_surjective line 384
  30. lemma OAI.Tachikawa.FiniteModule.cosyzygyProjection_exact line 386
  31. lemma OAI.Tachikawa.FiniteModule.negative_succ_left line 391
  32. theorem OAI.Tachikawa.FiniteModule.descend_nonzero_composition line 397
  33. theorem OAI.Tachikawa.FiniteModule.descend_nonzero_composition_iterated line 430
  34. def OAI.Tachikawa.Enveloping.inducedFiveCokerEquiv line 453
  35. theorem OAI.Tachikawa.Construction.exists_Y_lift_with_nonzero_composition line 462
  36. lemma OAI.Tachikawa.BalancedTensor.restrictEquiv_mapLeft line 506
  37. lemma OAI.Tachikawa.BalancedTensor.mapLeft_injective_of_right_split line 516
  38. lemma OAI.Tachikawa.BalancedTensor.mapLeft_surjective line 551
  39. lemma OAI.Tachikawa.BalancedTensor.mapLeft_exact_of_right_splitting line 565
  40. instance OAI.Tachikawa.Enveloping.eval_finite line 616
  41. lemma OAI.Tachikawa.Enveloping.evalMap_injective line 620
  42. lemma OAI.Tachikawa.Enveloping.evalMap_surjective line 641
  43. lemma OAI.Tachikawa.Enveloping.evalMap_exact line 645
  44. lemma OAI.Tachikawa.Enveloping.eval_square_factors_iff line 682
  45. lemma OAI.Tachikawa.BimoduleTensorHom.uncurry_factors line 725
  46. lemma OAI.Tachikawa.BimoduleTensorHom.factors_of_uncurry line 742
  47. lemma OAI.Tachikawa.BimoduleTensorHom.factors_iff_uncurry line 773
  48. def OAI.Tachikawa.BimoduleTensorHom.linearEquiv line 778
  49. def OAI.Tachikawa.BimoduleTensorHom.stableEquiv line 783
  50. theorem OAI.Tachikawa.evaluation_nonzero_of_syzygy_composition line 810
  51. theorem OAI.Tachikawa.Construction.exists_evaluated_Y_lift line 882
  52. lemma OAI.Tachikawa.Construction.sigma_fixed_x line 899
  53. def OAI.Tachikawa.Construction.uXIso line 905
  54. theorem OAI.Tachikawa.Construction.exists_nonzero_X_YX line 908