OAI/Algebra/Finitistic/Ordinary/OrdinaryTensorFiniteMatrix.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.ComplexTensor.columns line 14
2. def OAI.LittleFinitistic.ComplexTensor.entry line 17

   Source documentation

   The actual horizontal matrix entry, zero unless the right degrees are consecutive.

   def entry (n : ℤ) (i j : Fin l) :
       term k A Q Z (p i) (n + -(p i)) →ₗ[k] term k A Q Z (p j) ((n+1) + -(p j)) :=
   …

   Mentions: OAI.LittleFinitistic.ComplexTensor.term

3. theorem OAI.LittleFinitistic.ComplexTensor.entry_square line 21
4. theorem OAI.LittleFinitistic.ComplexTensor.entry_mixed line 30
5. def OAI.LittleFinitistic.ComplexTensor.matrix line 39

   Source documentation

   The actual finite horizontal tensor differential, on the sum of all selected columns.

   def matrix (n : ℤ) : FiniteColumnComplex.term (columns k A Q Z p) n →ₗ[k]
       FiniteColumnComplex.term (columns k A Q Z p) (n+1) :=
   …

   Mentions: OAI.LittleFinitistic.FiniteColumnComplex.term, OAI.LittleFinitistic.ComplexTensor.columns

6. theorem OAI.LittleFinitistic.ComplexTensor.matrix_apply line 43
7. theorem OAI.LittleFinitistic.ComplexTensor.matrix_square line 51
8. theorem OAI.LittleFinitistic.ComplexTensor.matrix_mixed line 64
9. theorem OAI.LittleFinitistic.ComplexTensor.matrix_upper line 81
10. def OAI.LittleFinitistic.ComplexTensor.tensorHorizontal line 95

    Source documentation

    Actual tensor horizontal maps satisfy every requirement of the finite total construction.

    def tensorHorizontal (hp : StrictMono p) : FiniteColumnComplex.Horizontal (columns k A Q Z p) where
    …

    Mentions: OAI.LittleFinitistic.FiniteColumnComplex.Horizontal, OAI.LittleFinitistic.ComplexTensor.columns

11. def OAI.LittleFinitistic.ComplexTensor.finiteTotal line 102

    Source documentation

    The signed total tensor complex on a finite interval of the right complex.

    def finiteTotal (hp : StrictMono p) : CochainComplex (ModuleCat.{u} k) ℤ :=
    …