SelectedDerivedFunctor.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.SelectedDerivedFunctor.model line 13
Source documentation
One fixed genuine derived tensor functor, chosen before any test module.
```
def model : BimoduleTotal.BoundedProjective ℂ (B P) SelectedRectification.bimodule :=
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.BoundedProjective, OAI.LittleFinitistic.SelectedRectification.bimodule
abbrev OAI.LittleFinitistic.SelectedDerivedFunctor.Phi line 17
def OAI.LittleFinitistic.SelectedDerivedFunctor.comparison line 21
Source documentation
The previously explicit stalk-comparison premise is now discharged for the actual fixed selecting bimodule and its actual derived tensor endofunctor.
```
def comparison (Y : S.{0}) : Phi.obj (derived Y) ≅
    SelectedTensorSplitting.object (representation Y).Evaluation :=
…
```
Mentions: OAI.LittleFinitistic.SelectedTensorSplitting.object

def OAI.LittleFinitistic.SelectedDerivedFunctor.iteration line 26

Source documentation

The actual full B-linear binomial formula for the genuine tensor functor.

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

theorem OAI.LittleFinitistic.SelectedDerivedFunctor.isZero_iff line 32
theorem OAI.LittleFinitistic.SelectedDerivedFunctor.extinction line 37
Source documentation
Exact arbitrarily long finite extinction for one fixed actual tensor functor.
```
theorem extinction (m : ℕ) [NeZero m] :
    (∀ j < m, ¬ IsZero ((Phi.obj^[j]) (derived (test m)))) ∧
      IsZero ((Phi.obj^[m]) (derived (test m))) :=
…
```