RecursiveSuffixCoefficient.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DerivedBar.ParityBridge.coefficient_termCast line 26
theorem OAI.DerivedBar.ParityBridge.barSuffix_coefficient_zero line 35
Source documentation
The first X factor is killed by the exterior projection A -> D.
```
theorem barSuffix_coefficient_zero (V : ModuleCat.{u} D) (s i : ℕ)
    (e : V →ₗ[k] term k A N s) (v : ((XB).obj V).X i) :
    FreeBaseChange.coefficient (fstHom k D X) (term k A N (s+i))
      (barSuffix k D X N V s i e v) = 0 := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.FreeBaseChange.coefficient, OAI.DerivedBar.ParityBridge.barSuffix
theorem OAI.DerivedBar.ParityBridge.innerEmbedding_coefficient_of_pos line 50
Source documentation
The exterior endpoint vanishes at every positive suffix degree, including zero input summands when no X has yet been inserted.
```
theorem innerEmbedding_coefficient_of_pos (r n s : ℕ) (hs : r+n=s+1)
    (v : RecursiveTotal.flat B Z r n) :
    FreeBaseChange.coefficient (fstHom k D X) (term k A N s)
      (termCast k D X N hs (innerEmbedding k D X N r n v)) = 0 := by
…
```
Mentions: OAI.DerivedBar.RecursiveTotal.flat, OAI.DerivedBar.FreeBaseChange.coefficient, OAI.DerivedBar.term, OAI.DerivedBar.ParityBridge.termCast, OAI.DerivedBar.ParityBridge.innerEmbedding
theorem OAI.DerivedBar.ParityBridge.innerTotalEmbedding_coefficient_of_pos line 76
theorem OAI.DerivedBar.ParityBridge.innerEmbedding_coefficient_zero line 82
theorem OAI.DerivedBar.ParityBridge.innerTotalEmbedding_coefficient_zero line 89