OAI/Algebra/Finitistic/Bimodule/BimoduleTotalPresentation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.BimoduleTotalPresentation.addHom_smul_zero line 10
2. theorem OAI.LittleFinitistic.BimoduleTotalPresentation.addHom_smul_add line 14
3. def OAI.LittleFinitistic.BimoduleTotalPresentation.termEquiv line 25

   Source documentation

   The canonical balanced quotient comparison retains the outside B action.

   def termEquiv (r q : ℤ) :
       BimoduleComplexTensor.term k B B P Z r q ≃ₗ[B] BimoduleTotal.Term k B P Z r q :=
   …

   Mentions: OAI.LittleFinitistic.BimoduleComplexTensor.term, OAI.LittleFinitistic.BimoduleTotal.Term

4. def OAI.LittleFinitistic.BimoduleTotalPresentation.totalTermEquiv line 42
5. def OAI.LittleFinitistic.BimoduleTotalPresentation.totalIso line 48

   Source documentation

   The two signed totals coincide through their actual tensor-summand equivalences.

   def totalIso : BimoduleComplexTensor.total k B B P Z p hp ≅
       BimoduleTotal.total k B P p hp Z :=
   …

   Mentions: OAI.LittleFinitistic.BimoduleComplexTensor.total, OAI.LittleFinitistic.BimoduleTotal.total

6. theorem OAI.LittleFinitistic.BimoduleTotalPresentation.totalIso_natural line 62
7. def OAI.LittleFinitistic.BimoduleTotalPresentation.totalFunctorIso line 73

   Source documentation

   Natural comparison on all input complexes, with the complete outside action.

   def totalFunctorIso : BimoduleComplexTensor.totalFunctor k B B P p hp ≅
       BimoduleTotal.functor k B P p hp :=
   …

   Mentions: OAI.LittleFinitistic.BimoduleComplexTensor.totalFunctor, OAI.LittleFinitistic.BimoduleTotal.functor