OAI/Algebra/Finitistic/Ordinary/OrdinaryFirstComponentExact.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.LittleFinitistic.ProductModules.firstFunctor_additive line 11
2. theorem OAI.LittleFinitistic.ProductModules.firstFunctor_mapsExact line 15

   Source documentation

   Exactness on the first central-idempotent component follows by projecting a preimage.

   theorem firstFunctor_mapsExact (K : ShortComplex (ModuleCat.{u} (L × R))) (hK : K.Exact) :
       (K.map (firstFunctor L R)).Exact := by
   …

   Mentions: OAI.LittleFinitistic.ProductModules.firstFunctor

3. instance OAI.LittleFinitistic.ProductModules.firstFunctor_preservesHomology line 29
4. instance OAI.LittleFinitistic.ProductModules.firstFunctor_preservesFiniteLimits line 32
5. instance OAI.LittleFinitistic.ProductModules.firstFunctor_preservesFiniteColimits line 35
6. def OAI.LittleFinitistic.ProductModules.firstInflationComponentEquiv line 39

   Source documentation

   Taking the first component of an inflated module recovers the original module.

   def firstInflationComponentEquiv (M : ModuleCat.{u} L) :
       firstObject L R ((firstInflation L R).obj M) ≃ₗ[L] M where
   …

   Mentions: OAI.LittleFinitistic.ProductModules.firstObject, OAI.LittleFinitistic.ProductModules.firstInflation

7. def OAI.LittleFinitistic.ProductModules.firstInflationComponentIso line 49

   Source documentation

   This recovery is natural in every module and linear map.

   def firstInflationComponentIso : firstInflation.{u,u} L R ⋙ firstFunctor L R ≅ 𝟭 (ModuleCat.{u} L) :=
   …

   Mentions: OAI.LittleFinitistic.ProductModules.firstFunctor