OAI/Algebra/Finitistic/Bimodule/BimoduleSingleTerms.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.BimoduleTotal.singleInput line 14
2. abbrev OAI.LittleFinitistic.BimoduleTotal.moduleEvaluation line 17

   Source documentation

   The native degree-zero-module evaluation, retaining its original B action and differential.

   abbrev moduleEvaluation :=
   …

3. def OAI.LittleFinitistic.BimoduleTotal.singleTermIso line 21
4. theorem OAI.LittleFinitistic.BimoduleTotal.singleTerm_isZero line 27
5. def OAI.LittleFinitistic.BimoduleTotal.piSingleEquiv line 34

   Source documentation

   A finite product with only one possibly nonzero factor is that actual factor.

   def piSingleEquiv {l : ℕ} (V : Fin l → Type u) [∀ i, AddCommGroup (V i)] [∀ i, Module B (V i)]
       (i : Fin l) (hz : ∀ j, j ≠ i → Subsingleton (V j)) : (∀ j, V j) ≃ₗ[B] V i where
   …

6. def OAI.LittleFinitistic.BimoduleTotal.evaluationAtIndex line 50
7. theorem OAI.LittleFinitistic.BimoduleTotal.totalSingle_isZero line 58
8. def OAI.LittleFinitistic.BimoduleTotal.evaluationTermIso line 64

   Source documentation

   The finite total and the native module evaluation agree in every degree, provided every nonzero P-degree is included.

   def evaluationTermIso
       (hP : ∀ n, (∀ i, p i ≠ n) → IsZero (P.X n)) (n : ℤ) :
       ModuleCat.of B (TotalTerm k B P p (singleInput B N) n) ≅ (moduleEvaluation k B P N).X n := by
   …

   Mentions: OAI.LittleFinitistic.BimoduleTotal.TotalTerm, OAI.LittleFinitistic.BimoduleTotal.singleInput, OAI.LittleFinitistic.BimoduleTotal.moduleEvaluation