OAI/Algebra/Finitistic/Localization/SingleDegreeNaturality.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LittleFinitistic.DerivedTruncation.single_homology_injective line 12
2. lemma OAI.LittleFinitistic.DerivedTruncation.homology_injective line 26
3. def OAI.LittleFinitistic.DerivedTruncation.cohomologyAutomorphism line 36
4. def OAI.LittleFinitistic.DerivedTruncation.canonicalIso line 41

   Source documentation

   Normalize a single-degree identification to induce the identity on its actual cohomology.

   def canonicalIso : X ≅ (singleFunctor C n).obj ((homologyFunctor C n).obj X) :=
   …

5. lemma OAI.LittleFinitistic.DerivedTruncation.canonicalIso_homology line 44
6. theorem OAI.LittleFinitistic.DerivedTruncation.canonicalIso_naturality line 61

   Source documentation

   The normalized single-degree identification commutes with every derived morphism.

   theorem canonicalIso_naturality (f : X ⟶ Y) :
       f ≫ (canonicalIso n Y).hom =
         (canonicalIso n X).hom ≫ (singleFunctor C n).map ((homologyFunctor C n).map f) := by
   …

   Mentions: OAI.LittleFinitistic.DerivedTruncation.canonicalIso