OAI/Algebra/Finitistic/Bimodule/BimoduleTotalFunctor.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LittleFinitistic.BimoduleTotal.TotalTerm line 13
  2. abbrev OAI.LittleFinitistic.BimoduleTotal.vectorTotal line 14
  3. theorem OAI.LittleFinitistic.BimoduleTotal.matrix_smul line 16
  4. theorem OAI.LittleFinitistic.BimoduleTotal.differential_smul line 34
  5. def OAI.LittleFinitistic.BimoduleTotal.total line 61

    Source documentation

    The same signed finite tensor total, retaining the full left B action.

    def total : CochainComplex (ModuleCat.{u} B) ℤ where
…
  6. def OAI.LittleFinitistic.BimoduleTotal.totalMap line 80

    Source documentation

    The original input tensor map is B-linear in every degree.

    def totalMap (f : Z ⟶ Z') : total k B P p hp Z ⟶ total k B P p hp Z' where
…

    Mentions: OAI.LittleFinitistic.BimoduleTotal.total

  7. def OAI.LittleFinitistic.BimoduleTotal.functor line 99

    Source documentation

    Tensoring with the fixed bimodule complex acts on every left-module complex.

    def functor : CochainComplex (ModuleCat.{u} B) ℤ ⥤ CochainComplex (ModuleCat.{u} B) ℤ where
…
  8. instance OAI.LittleFinitistic.BimoduleTotal.additive line 119