OAI/Algebra/Finitistic/Bimodule/BimoduleTotalCoefficient.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.BimoduleTotal.coefficient line 14
2. theorem OAI.LittleFinitistic.BimoduleTotal.coefficient_at line 18
3. theorem OAI.LittleFinitistic.BimoduleTotal.coefficient_outside line 23
4. theorem OAI.LittleFinitistic.BimoduleTotal.term_left_isZero line 26
5. theorem OAI.LittleFinitistic.BimoduleTotal.coefficient_d_sum line 35

   Source documentation

   The original total differential, read in any integer left degree, including zero degrees outside the chosen finite support.

   theorem coefficient_d_sum (n a : ℤ) (x : TotalTerm k B P p Z n) :
       coefficient k B P Z p (n+1) a (((total k B P p hp Z).d n (n+1)).hom x) =
         (show Term k B P Z a ((n+1) + -a) from
           ((ComplexTensor.column k B (right k B P) Z a).d n (n+1)).hom
             (coefficient k B P Z p n a x)) +
         ∑ i : Fin l, entryBetween k B P Z n (n+1) (p i) a rfl (x i) := by
   …

   Mentions: OAI.LittleFinitistic.BimoduleTotal.TotalTerm, OAI.LittleFinitistic.BimoduleTotal.coefficient, OAI.LittleFinitistic.BimoduleTotal.total, OAI.LittleFinitistic.BimoduleTotal.Term, OAI.LittleFinitistic.ComplexTensor.column, OAI.LittleFinitistic.BimoduleTotal.right, OAI.LittleFinitistic.BimoduleTotal.entryBetween

6. theorem OAI.LittleFinitistic.BimoduleTotal.horizontal_sum_predecessor line 52

   Source documentation

   The horizontal sum has at most its immediately preceding left-degree component.

   theorem horizontal_sum_predecessor (n a : ℤ) (x : TotalTerm k B P p Z n) :
       (∑ i : Fin l, entryBetween k B P Z n (n+1) (p i) a rfl (x i)) =
         horizontalBetween k B P Z n (n+1) (a-1) a rfl (by omega)
           (coefficient k B P Z p n (a-1) x) := by
   …

   Mentions: OAI.LittleFinitistic.BimoduleTotal.TotalTerm, OAI.LittleFinitistic.BimoduleTotal.entryBetween, OAI.LittleFinitistic.BimoduleTotal.horizontalBetween, OAI.LittleFinitistic.BimoduleTotal.coefficient

7. theorem OAI.LittleFinitistic.BimoduleTotal.coefficient_d line 85

   Source documentation

   The complete finite tensor differential consists of its signed vertical term and its immediately preceding horizontal term.

   theorem coefficient_d (n a : ℤ) (x : TotalTerm k B P p Z n) :
       coefficient k B P Z p (n+1) a (((total k B P p hp Z).d n (n+1)).hom x) =
         (show Term k B P Z a ((n+1) + -a) from
           ((ComplexTensor.column k B (right k B P) Z a).d n (n+1)).hom
             (coefficient k B P Z p n a x)) +
         horizontalBetween k B P Z n (n+1) (a-1) a rfl (by omega)
           (coefficient k B P Z p n (a-1) x) := by
   …

   Mentions: OAI.LittleFinitistic.BimoduleTotal.TotalTerm, OAI.LittleFinitistic.BimoduleTotal.coefficient, OAI.LittleFinitistic.BimoduleTotal.total, OAI.LittleFinitistic.BimoduleTotal.Term, OAI.LittleFinitistic.ComplexTensor.column, OAI.LittleFinitistic.BimoduleTotal.right, OAI.LittleFinitistic.BimoduleTotal.horizontalBetween