OAI/Algebra/Finitistic/Localization/DerivedTruncationCohomology.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LittleFinitistic.DerivedTruncation.t line 13
  2. abbrev OAI.LittleFinitistic.DerivedTruncation.lower line 14
  3. abbrev OAI.LittleFinitistic.DerivedTruncation.upper line 15
  4. abbrev OAI.LittleFinitistic.DerivedTruncation.inclusion line 16
  5. abbrev OAI.LittleFinitistic.DerivedTruncation.projection line 17
  6. abbrev OAI.LittleFinitistic.DerivedTruncation.triangle line 18
  7. instance OAI.LittleFinitistic.DerivedTruncation.lower_isLE_minus_one line 19
  8. lemma OAI.LittleFinitistic.DerivedTruncation.distinguished line 21
  9. lemma OAI.LittleFinitistic.DerivedTruncation.lower_homology_isIso line 24
  10. lemma OAI.LittleFinitistic.DerivedTruncation.upper_homology_isIso line 35
  11. def OAI.LittleFinitistic.DerivedTruncation.lowerHomologyIso line 46
  12. def OAI.LittleFinitistic.DerivedTruncation.upperHomologyIso line 51
  13. def OAI.LittleFinitistic.DerivedTruncation.TwoDegrees line 57

    Source documentation

    The exact cohomological support hypothesis in Section 4.

    def TwoDegrees (X : DerivedCategory C) : Prop :=
…
  14. lemma OAI.LittleFinitistic.DerivedTruncation.isLE_zero line 60
  15. lemma OAI.LittleFinitistic.DerivedTruncation.isGE_neg_three line 64
  16. lemma OAI.LittleFinitistic.DerivedTruncation.lower_isGE line 68
  17. lemma OAI.LittleFinitistic.DerivedTruncation.lower_isLE line 71
  18. lemma OAI.LittleFinitistic.DerivedTruncation.upper_isLE line 77
  19. def OAI.LittleFinitistic.DerivedTruncation.singleIso line 82

    Source documentation

    An object concentrated in one degree is the stalk of its actual cohomology.

    def singleIso (X : DerivedCategory C) (n : ℤ) [X.IsGE n] [X.IsLE n] :
    X ≅ (singleFunctor C n).obj ((homologyFunctor C n).obj X) := Classical.choice (by
…