OAI/Algebra/Finitistic/Ordinary/OrdinaryComplexTensorMaps.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.ComplexTensor.rightTerm line 14
2. abbrev OAI.LittleFinitistic.ComplexTensor.leftTerm line 15
3. abbrev OAI.LittleFinitistic.ComplexTensor.term line 16
4. def OAI.LittleFinitistic.ComplexTensor.map line 19

   Source documentation

   The balanced map for actual maps between terms of the two input complexes.

   def map {p p' q q' : ℤ} (f : Q.X p ⟶ Q.X p') (g : Z.X q ⟶ Z.X q') :
       term k A Q Z p q →ₗ[k] term k A Q Z p' q' :=
   …

   Mentions: OAI.LittleFinitistic.ComplexTensor.term

5. theorem OAI.LittleFinitistic.ComplexTensor.map_comp line 25
6. theorem OAI.LittleFinitistic.ComplexTensor.map_zero_left line 31
7. theorem OAI.LittleFinitistic.ComplexTensor.map_zero_right line 34
8. def OAI.LittleFinitistic.ComplexTensor.column line 38

   Source documentation

   The column at right degree p, including the standard total-complex sign (-1)^p.

   def column (p : ℤ) : CochainComplex (ModuleCat.{u} k) ℤ :=
   …

9. theorem OAI.LittleFinitistic.ComplexTensor.column_d line 41
10. def OAI.LittleFinitistic.ComplexTensor.horizontal line 49

    Source documentation

    Horizontal tensor maps reindex the unchanged left factor along the total degree.

    def horizontal (n p p' : ℤ) (h : p+1=p') :
        term k A Q Z p (n + -p) →ₗ[k] term k A Q Z p' ((n+1) + -p') :=
    …

    Mentions: OAI.LittleFinitistic.ComplexTensor.term

11. theorem OAI.LittleFinitistic.ComplexTensor.horizontal_square line 53