SelectedTensorSplitting.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.LittleFinitistic.SelectedTensorSplitting.object line 13
Source documentation
The actual derived object represented by the full B-valued fixed tensor complex.
```
abbrev object : DerivedCategory (ModuleCat (B P)) := DerivedCategory.Q.obj (SelectedTensor.complex N)
```
Mentions: OAI.LittleFinitistic.SelectedTensor.complex
def OAI.LittleFinitistic.SelectedTensorSplitting.homologyIso line 15
theorem OAI.LittleFinitistic.SelectedTensorSplitting.twoDegrees line 22
Source documentation
Support of the evaluated representative diagram implies actual derived cohomological support of the full tensor object.
```
theorem twoDegrees
    (h : ∀ n : ℤ, n ≠ 0 → n ≠ -3 → ∀ v : Fin 3,
      IsZero ((SelectedTensor.source N v).homology n)) :
    DerivedTruncation.TwoDegrees (object N) := by
…
```
Mentions: OAI.LittleFinitistic.SelectedTensor.source, OAI.LittleFinitistic.DerivedTruncation.TwoDegrees, OAI.LittleFinitistic.SelectedTensorSplitting.object

def OAI.LittleFinitistic.SelectedTensorSplitting.split line 32

Source documentation

Apply the proved B-linear truncation splitting to the actual fixed tensor, using full module cohomology models and source-diagram support.

def split (R : ModuleCat (B P))
    (h0 : (SelectedTensor.complex N).homology 0 ≅ R)
    (h3 : (SelectedTensor.complex N).homology (-3) ≅ R)
    (hz : ∀ n : ℤ, n ≠ 0 → n ≠ -3 → ∀ v : Fin 3,
      IsZero ((SelectedTensor.source N v).homology n)) :
    object N ≅ (DerivedCategory.singleFunctor (ModuleCat (B P)) 0).obj R ⊞
      ((DerivedCategory.singleFunctor (ModuleCat (B P)) 0).obj R)⟦(3 : ℤ)⟧ :=
…

Mentions: OAI.LittleFinitistic.SelectedTensor.complex, OAI.LittleFinitistic.SelectedTensor.source, OAI.LittleFinitistic.SelectedTensorSplitting.object