OAI/Algebra/Finitistic/Ordinary/OrdinaryTensorTotalFunctor.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.FiniteColumnComplex.diagonal_componentMap line 12
2. def OAI.LittleFinitistic.ComplexTensor.finiteTotalMap line 29

   Source documentation

   Actual tensor total applied to an arbitrary chain map of input complexes.

   def finiteTotalMap (f : Z ⟶ Z') : finiteTotal k A Q Z p hp ⟶ finiteTotal k A Q Z' p hp :=
   …

   Mentions: OAI.LittleFinitistic.ComplexTensor.finiteTotal

3. theorem OAI.LittleFinitistic.ComplexTensor.finiteTotalMap_apply line 41
4. theorem OAI.LittleFinitistic.ComplexTensor.inputMap_id line 48
5. theorem OAI.LittleFinitistic.ComplexTensor.inputMap_comp line 53
6. def OAI.LittleFinitistic.ComplexTensor.finiteTotalFunctor line 60

   Source documentation

   The actual signed finite tensor total is a functor on all input complexes.

   def finiteTotalFunctor : CochainComplex (ModuleCat.{u} A) ℤ ⥤ CochainComplex (ModuleCat.{u} k) ℤ where
   …