OAI/RingTheory/Tachikawa/TwistHom.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Tachikawa.mappedResolution line 13
2. def OAI.Tachikawa.mappedResolutionCochainXIso line 15
3. lemma OAI.Tachikawa.mappedResolutionCochainXIso_nonpos line 25
4. lemma OAI.Tachikawa.mappedResolutionCochainXIso_comm line 35
5. def OAI.Tachikawa.mappedResolutionCochainIso line 54
6. lemma OAI.Tachikawa.mappedResolutionCochainIso_π line 68
7. lemma OAI.Tachikawa.map_toSingle_shifted line 97
8. lemma OAI.Tachikawa.extMk_hom_roof line 127
9. lemma OAI.Tachikawa.mappedResolutionCochain_cocycle line 143
10. lemma OAI.Tachikawa.mapExactFunctor_extMk line 184
11. def OAI.Tachikawa.resolutionTwistHom line 222
12. lemma OAI.Tachikawa.resolutionTwistHom_extMk line 244
13. lemma OAI.Tachikawa.FiniteModule.projectiveResolution_d line 272
14. lemma OAI.Tachikawa.FiniteModule.projectiveResolution_π line 276
15. def OAI.Tachikawa.FiniteModule.positiveTwistLift line 280
16. def OAI.Tachikawa.FiniteModule.negativeTwistLift line 285
17. def OAI.Tachikawa.FiniteModule.completeTwistComponent line 290
18. lemma OAI.Tachikawa.FiniteModule.completeTwistComponent_comm line 295
19. def OAI.Tachikawa.FiniteModule.completeTwistLift line 329
20. lemma OAI.Tachikawa.resolutionTwist_diff_boundary line 351
21. def OAI.Tachikawa.FiniteModule.completeTwistHom line 391
22. lemma OAI.Tachikawa.FiniteModule.completeTwistHom_positive line 396
23. lemma OAI.Tachikawa.FiniteModule.completeTwistHom_negative line 420
24. def OAI.Tachikawa.Enveloping.tensorTwistLift line 457
25. lemma OAI.Tachikawa.Enveloping.tensorTwistLift_aug line 461
26. lemma OAI.Tachikawa.Enveloping.tensorTwistLift_action line 475
27. lemma OAI.Tachikawa.Enveloping.tensor_projected_action line 497