OAI/Algebra/Finitistic/Ordinary/OrdinaryTensorInputMaps.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.ComplexTensor.inputMap line 15

   Source documentation

   The actual map induced by an input chain map in a single balanced tensor term.

   def inputMap (p q : ℤ) : term k A Q Z p q →ₗ[k] term k A Q Z' p q :=
   …

   Mentions: OAI.LittleFinitistic.ComplexTensor.term

2. def OAI.LittleFinitistic.ComplexTensor.columnMap line 20

   Source documentation

   Input chain maps act on the signed columns by the actual shifted tensor functor.

   def columnMap (p : ℤ) : column k A Q Z p ⟶ column k A Q Z' p :=
   …

   Mentions: OAI.LittleFinitistic.ComplexTensor.column

3. theorem OAI.LittleFinitistic.ComplexTensor.columnMap_f line 24
4. theorem OAI.LittleFinitistic.ComplexTensor.inputMap_transport line 30
5. theorem OAI.LittleFinitistic.ComplexTensor.horizontal_inputMap line 36

   Source documentation

   The horizontal tensor differential is natural in the arbitrary input complex.

   theorem horizontal_inputMap (n p p' : ℤ) (h : p+1=p') :
       (horizontal k A Q Z' n p p' h).comp (inputMap k A Q f p (n + -p)) =
         (inputMap k A Q f p' ((n+1) + -p')).comp (horizontal k A Q Z n p p' h) := by
   …

   Mentions: OAI.LittleFinitistic.ComplexTensor.horizontal, OAI.LittleFinitistic.ComplexTensor.inputMap

6. theorem OAI.LittleFinitistic.ComplexTensor.entry_inputMap line 47
7. theorem OAI.LittleFinitistic.ComplexTensor.matrix_inputMap line 56

   Source documentation

   The full horizontal matrix commutes with the actual input map.

   theorem matrix_inputMap (n : ℤ) :
       (matrix k A Q Z' p n).comp
         (FiniteColumnComplex.componentMap (columns k A Q Z p) (columns k A Q Z' p)
           (fun i => columnMap k A Q f (p i)) n) =
       (FiniteColumnComplex.componentMap (columns k A Q Z p) (columns k A Q Z' p)
         (fun i => columnMap k A Q f (p i)) (n+1)).comp (matrix k A Q Z p n) := by
   …

   Mentions: OAI.LittleFinitistic.ComplexTensor.matrix, OAI.LittleFinitistic.FiniteColumnComplex.componentMap, OAI.LittleFinitistic.ComplexTensor.columns, OAI.LittleFinitistic.ComplexTensor.columnMap