OAI/Algebra/Finitistic/Selected/SelectedFiniteTensorEvaluation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.LittleFinitistic.BalancedTensor.tensorFinite line 13
2. theorem OAI.LittleFinitistic.BalancedTensor.tensorFunctor_finite line 18
3. theorem OAI.LittleFinitistic.BalancedTensor.complex_zero line 26

   Source documentation

   The termwise evaluation preserves every actual zero term, hence bounded support.

   theorem complex_zero (K : CochainComplex (ModuleCat.{w} Aᵐᵒᵖ) ℤ) (i : ℤ)
       (h : IsZero (K.X i)) :
       IsZero (((tensorFunctor k A N).mapHomologicalComplex (ComplexShape.up ℤ)).obj K |>.X i) :=
   …

   Mentions: OAI.LittleFinitistic.BalancedTensor.tensorFunctor

4. theorem OAI.LittleFinitistic.BalancedTensor.bounded_support line 32

   Source documentation

   A bounded input has a bounded output with the same interval of possible nonzero terms.

   theorem bounded_support (K : CochainComplex (ModuleCat.{w} Aᵐᵒᵖ) ℤ) (a b : ℤ)
       (h : ∀ i, i < a ∨ b < i → IsZero (K.X i)) :
       ∀ i, i < a ∨ b < i →
         IsZero (((tensorFunctor k A N).mapHomologicalComplex (ComplexShape.up ℤ)).obj K |>.X i) :=
   …

   Mentions: OAI.LittleFinitistic.BalancedTensor.tensorFunctor