OAI/Algebra/Finitistic/Selected/SelectedIteration.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.SelectedIteration.split line 19
2. def OAI.LittleFinitistic.SelectedIteration.iteration line 23

   Source documentation

   The exact binomial formula, instantiated with the actual finite module family.

   def iteration (j : ℕ) (Y : S) :
       (Phi.obj^[j]) (derived Y) ≅
         ⨁ fun q : Fin (j+1) => ⨁ fun _ : Fin (Nat.choose j q.val) =>
           (derived ((H^[j]) Y))⟦(3 : ℤ)*(q.val : ℤ)⟧ :=
   …

3. def OAI.LittleFinitistic.SelectedIteration.shiftedSplit line 29
4. theorem OAI.LittleFinitistic.SelectedIteration.isZero_iff line 33
5. theorem OAI.LittleFinitistic.SelectedIteration.extinction line 40

   Source documentation

   Actual Section 2 tests give arbitrarily long finite extinction for this tensor functor, once its stated stalk comparison is instantiated.

   theorem extinction (m : ℕ) [NeZero m] :
       (∀ j < m, ¬ IsZero ((Phi.obj^[j]) (derived (test m)))) ∧
         IsZero ((Phi.obj^[m]) (derived (test m))) := by
   …