OAI/Algebra/Finitistic/Bimodule/BimoduleTotalInsertion.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.BimoduleTotal.insertion line 14

   Source documentation

   Insert one actual left-degree component into the finite total.

   def insertion (n a : ℤ) : Term k B P Z a (n + -a) →ₗ[B] TotalTerm k B P p Z n := by
   …

   Mentions: OAI.LittleFinitistic.BimoduleTotal.Term, OAI.LittleFinitistic.BimoduleTotal.TotalTerm

2. theorem OAI.LittleFinitistic.BimoduleTotal.insertion_same line 19
3. theorem OAI.LittleFinitistic.BimoduleTotal.insertion_other line 24
4. theorem OAI.LittleFinitistic.BimoduleTotal.coefficient_insertion_other line 30
5. theorem OAI.LittleFinitistic.BimoduleTotal.coefficient_insertion_self line 42
6. theorem OAI.LittleFinitistic.BimoduleTotal.coefficient_d_between line 53
7. theorem OAI.LittleFinitistic.BimoduleTotal.coefficient_d_insertion_above line 65

   Source documentation

   A correction inserted in degree a cannot affect total coordinates above a+1.

   theorem coefficient_d_insertion_above (n m : ℤ) (h : n+1=m) (a b : ℤ) (hab : a+1<b)
       (y : Term k B P Z a (n + -a)) :
       coefficient k B P Z p m b
         (((total k B P p hp Z).d n m).hom (insertion k B P Z p n a y)) = 0 := by
   …

   Mentions: OAI.LittleFinitistic.BimoduleTotal.Term, OAI.LittleFinitistic.BimoduleTotal.coefficient, OAI.LittleFinitistic.BimoduleTotal.total, OAI.LittleFinitistic.BimoduleTotal.insertion

8. theorem OAI.LittleFinitistic.BimoduleTotal.coefficient_d_insertion_next line 77

   Source documentation

   The next coordinate of the inserted correction is exactly its horizontal differential.

   theorem coefficient_d_insertion_next (n m : ℤ) (h : n+1=m) (a b : ℤ) (hab : a+1=b)
       (y : Term k B P Z a (n + -a)) :
       coefficient k B P Z p m b
         (((total k B P p hp Z).d n m).hom (insertion k B P Z p n a y)) =
         horizontalBetween k B P Z n m a b h hab y := by
   …

   Mentions: OAI.LittleFinitistic.BimoduleTotal.Term, OAI.LittleFinitistic.BimoduleTotal.coefficient, OAI.LittleFinitistic.BimoduleTotal.total, OAI.LittleFinitistic.BimoduleTotal.insertion, OAI.LittleFinitistic.BimoduleTotal.horizontalBetween