RecursiveSuffixDifferential.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DerivedBar.ParityBridge.innerEmbedding_horizontal line 30

Source documentation

The actual horizontal differential followed by the complete suffix embedding.

theorem innerEmbedding_horizontal (r n i q : ℕ) (h : (i+1)+q=n+1)
    (t : RecursiveTotal.Index r q)
    (v : (RecursiveTotal.degreeFunctor B r (i+1)).obj (RecursiveTotal.summand B Z r q t)) :
    innerEmbedding k D X N (r+1) n
      ((RecursiveTotal.horizontal B Z r n (i+1) q h t).hom v) =
    termCast k D X N (show ((r+q)+i)+1=(r+1)+n by omega)
      (barSuffix k D X N (RecursiveTotal.summand B Z r q t) (r+q) i
        ((innerEmbedding k D X N r q).comp
          ((RecursiveTotal.lof B Z r q t).hom.restrictScalars k))
        ((((XB).obj (RecursiveTotal.summand B Z r q t)).d (i+1) i).hom v)) := by
…

Mentions: OAI.DerivedBar.RecursiveTotal.Index, OAI.DerivedBar.RecursiveTotal.degreeFunctor, OAI.DerivedBar.RecursiveTotal.summand, OAI.DerivedBar.ParityBridge.innerEmbedding, OAI.DerivedBar.RecursiveTotal.horizontal, OAI.DerivedBar.ParityBridge.termCast, OAI.DerivedBar.ParityBridge.barSuffix, OAI.DerivedBar.RecursiveTotal.lof

theorem OAI.DerivedBar.ParityBridge.innerEmbedding_vertical line 45

Source documentation

The actual signed vertical face is computed after distribution over the whole inner sum, rather than on an assumed single supported output summand.

theorem innerEmbedding_vertical (r n i q : ℕ) (h : i+(q+1)=n+1)
    (t : RecursiveTotal.Index r (q+1))
    (d : ∀ q, RecursiveTotal.flat B Z r (q+1) ⟶ RecursiveTotal.flat B Z r q)
    (v : (RecursiveTotal.degreeFunctor B r i).obj (RecursiveTotal.summand B Z r (q+1) t)) :
    innerEmbedding k D X N (r+1) n
      ((RecursiveTotal.vertical B Z r n i (q+1) h t d).hom v) =
    (-1:k)^i • termCast k D X N (show ((r+q)+i)+1=(r+1)+n by omega)
      (barSuffix k D X N (RecursiveTotal.summand B Z r (q+1) t) (r+q) i
        ((innerEmbedding k D X N r q).comp
          ((RecursiveTotal.lof B Z r (q+1) t ≫ d q).hom.restrictScalars k)) v) := by
…

Mentions: OAI.DerivedBar.RecursiveTotal.Index, OAI.DerivedBar.RecursiveTotal.flat, OAI.DerivedBar.RecursiveTotal.degreeFunctor, OAI.DerivedBar.RecursiveTotal.summand, OAI.DerivedBar.ParityBridge.innerEmbedding, OAI.DerivedBar.RecursiveTotal.vertical, OAI.DerivedBar.ParityBridge.termCast, OAI.DerivedBar.ParityBridge.barSuffix, OAI.DerivedBar.RecursiveTotal.lof

theorem OAI.DerivedBar.ParityBridge.innerEmbedding_differential_lof line 71

Source documentation

Evaluation of the independently recursive differential on one input summand.

theorem innerEmbedding_differential_lof (r n i q : ℕ) (h : i+q=n+1)
    (t : RecursiveTotal.Index r q)
    (v : RecursiveTotal.summand B Z (r+1) (n+1) ⟨⟨⟨i,q⟩,h⟩,t⟩) :
    innerEmbedding k D X N (r+1) n
      ((RecursiveTotal.differential B Z (r+1) n).hom
        ((RecursiveTotal.lof B Z (r+1) (n+1) ⟨⟨⟨i,q⟩,h⟩,t⟩).hom v)) =
    innerEmbedding k D X N (r+1) n
      ((RecursiveTotal.horizontal B Z r n i q h t).hom v) +
    innerEmbedding k D X N (r+1) n
      ((RecursiveTotal.vertical B Z r n i q h t (RecursiveTotal.differential B Z r)).hom v) := by
…

Mentions: OAI.DerivedBar.RecursiveTotal.Index, OAI.DerivedBar.RecursiveTotal.summand, OAI.DerivedBar.ParityBridge.innerEmbedding, OAI.DerivedBar.RecursiveTotal.differential, OAI.DerivedBar.RecursiveTotal.lof, OAI.DerivedBar.RecursiveTotal.horizontal, OAI.DerivedBar.RecursiveTotal.vertical

theorem OAI.DerivedBar.ParityBridge.termCast_trans line 89
Source documentation
Degree transports compose by equality elimination alone.
```
theorem termCast_trans {a b c : ℕ} (h : a=b) (g : b=c) (v : term k A N a) :
    termCast k D X N g (termCast k D X N h v) = termCast k D X N (h.trans g) v := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.ParityBridge.termCast

theorem OAI.DerivedBar.ParityBridge.innerEmbedding_suffix_induction line 95

Source documentation

Composition of the induction hypothesis with an actual summand inclusion.

theorem innerEmbedding_suffix_induction (r q : ℕ) (t : RecursiveTotal.Index r (q+1))
    (ih : ∀ (v : RecursiveTotal.flat B Z r (q+1)),
      SquareZero.multibarAugmentedDifferential k D X N (r+q)
        (innerEmbedding k D X N r (q+1) v) =
      -innerEmbedding k D X N r q ((RecursiveTotal.differential B Z r q).hom v)) :
    (SquareZero.multibarAugmentedDifferential k D X N (r+q)).comp
      ((innerEmbedding k D X N r (q+1)).comp
        ((RecursiveTotal.lof B Z r (q+1) t).hom.restrictScalars k)) =
    -((innerEmbedding k D X N r q).comp
      ((RecursiveTotal.lof B Z r (q+1) t ≫ RecursiveTotal.differential B Z r q).hom.restrictScalars k)) := by
…

Mentions: OAI.DerivedBar.RecursiveTotal.Index, OAI.DerivedBar.RecursiveTotal.flat, OAI.DerivedBar.SquareZero.multibarAugmentedDifferential, OAI.DerivedBar.ParityBridge.innerEmbedding, OAI.DerivedBar.RecursiveTotal.differential, OAI.DerivedBar.RecursiveTotal.lof