OAI/Algebra/Finitistic/Ordinary/OrdinaryFirstDerivedCompatibility.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.LittleFinitistic.BlockModule.firstInflation_preservesFiniteLimits line 12

    Source documentation

    First-block inflation is exact for arbitrary, possibly noncommutative rings.

    instance firstInflation_preservesFiniteLimits :
    PreservesFiniteLimits (ProductModules.firstInflation.{u,u} L R) := by
…
  2. instance OAI.LittleFinitistic.BlockModule.firstInflation_preservesFiniteColimits line 17
  3. instance OAI.LittleFinitistic.BlockModule.derivedFirst_lifting line 25
  4. def OAI.LittleFinitistic.BlockModule.derivedFirstIso line 31

    Source documentation

    The ordinary localization model is naturally the exact derived inflation.

    def derivedFirstIso : derivedFirst L R ≅ (ProductModules.firstInflation L R).mapDerivedCategory :=
…

    Mentions: OAI.LittleFinitistic.BlockModule.derivedFirst, OAI.LittleFinitistic.ProductModules.firstInflation

  5. theorem OAI.LittleFinitistic.BlockModule.derivedFirstIso_hom_app_Q line 40

    Source documentation

    The comparison agrees with both specified localization comparison maps.

    theorem derivedFirstIso_hom_app_Q (Z : CochainComplex (ModuleCat.{u} L) ℤ) :
    (derivedFirstIso L R).hom.app (DerivedCategory.Q.obj Z) ≫
      (ProductModules.firstInflation L R).mapDerivedCategoryFactors.hom.app Z =
    (derivedFirstComparison L R).hom.app Z := by
…

    Mentions: OAI.LittleFinitistic.BlockModule.derivedFirstIso, OAI.LittleFinitistic.ProductModules.firstInflation, OAI.LittleFinitistic.BlockModule.derivedFirstComparison

  6. instance OAI.LittleFinitistic.BlockModule.derivedFirst_commShift line 52

    Source documentation

    Transport the coherent integer shift structure of the exact derived functor.

    instance derivedFirst_commShift : (derivedFirst L R).CommShift ℤ :=
…

    Mentions: OAI.LittleFinitistic.BlockModule.derivedFirst

  7. instance OAI.LittleFinitistic.BlockModule.derivedFirstIso_inv_commShift line 55
  8. instance OAI.LittleFinitistic.BlockModule.derivedFirstIso_hom_commShift line 58
  9. instance OAI.LittleFinitistic.BlockModule.derivedFirst_isTriangulated line 63