OAI/Algebra/Finitistic/Ordinary/OrdinaryFixedTensorFunctor.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.BalancedTensor.ScalarLeftModule line 14
2. instance OAI.LittleFinitistic.BalancedTensor.scalarLeftTower line 17
3. def OAI.LittleFinitistic.BalancedTensor.fixedTensorFunctor line 25

   Source documentation

   Tensor by a fixed actual right module on every left module.

   def fixedTensorFunctor : ModuleCat.{u} A ⥤ ModuleCat.{u} k where
   …

4. instance OAI.LittleFinitistic.BalancedTensor.fixedTensorFunctor_additive line 40
5. theorem OAI.LittleFinitistic.BalancedTensor.idempotentTensor_mapsExact line 50
6. theorem OAI.LittleFinitistic.BalancedTensor.idempotentTensor_preservesHomology line 71

   Source documentation

   Derived input complexes remain arbitrary: this functor preserves homology.

   theorem idempotentTensor_preservesHomology :
       (fixedTensorFunctor k A (IdempotentTensor.rightIdeal e)).PreservesHomology :=
   …

   Mentions: OAI.LittleFinitistic.BalancedTensor.fixedTensorFunctor, OAI.LittleFinitistic.IdempotentTensor.rightIdeal

7. theorem OAI.LittleFinitistic.BalancedTensor.idempotentTensor_quasiIso line 77

   Source documentation

   No boundedness, dimension, projectivity, or flatness hypothesis on either input complex.

   theorem idempotentTensor_quasiIso
       {Z Z' : CochainComplex (ModuleCat.{u} A) ℤ} (f : Z ⟶ Z') [QuasiIso f] :
       QuasiIso (((fixedTensorFunctor k A (IdempotentTensor.rightIdeal e)).mapHomologicalComplex (.up ℤ)).map f) := by
   …

   Mentions: OAI.LittleFinitistic.BalancedTensor.fixedTensorFunctor, OAI.LittleFinitistic.IdempotentTensor.rightIdeal