OAI/Algebra/Finitistic/Localization/NativeProjectiveModel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.BimoduleTotal.nativeProjectiveModel line 12

   Source documentation

   Direct adapter for the boundedness and right-projectivity fields of the native fixed rectification.

   def nativeProjectiveModel (P : BiComplex k B) (lo hi : ℤ)
       (bounded : ∀ n, n < lo ∨ hi < n → IsZero (P.X n))
       (projective : ∀ n, CategoryTheory.Projective ((right k B P).X n)) :
       BoundedProjective k B P where
   …

   Mentions: OAI.LittleFinitistic.BimoduleTotal.right, OAI.LittleFinitistic.BimoduleTotal.BoundedProjective