LeadingSuffixFaces.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.ParityBridge.outerSuffixEmbed line 20
Source documentation
Retain the exterior D coefficient while inserting an arbitrary suffix.
```
def outerSuffixEmbed (s n : ℕ) (e : M →ₗ[k] term k A N s) :
    D ⊗[k] term k D M n →ₗ[D] D ⊗[k] term k A N (s+n) :=
…
```
Mentions: OAI.DerivedBar.term
theorem OAI.DerivedBar.ParityBridge.outerSuffixEmbed_tmul line 25
theorem OAI.DerivedBar.ParityBridge.coefficient_suffixEmbed line 32
Source documentation
The projected leading face is exactly the original D multiplication.
```
theorem coefficient_suffixEmbed (s n : ℕ) (e : M →ₗ[k] term k A N s)
    (v : term k D M (n+1)) :
    FreeBaseChange.coefficient (fstHom k D X) (term k A N (s+n))
      (suffixEmbed k D X N M s e (n+1) v) = outerSuffixEmbed k D X N M s n e v := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.FreeBaseChange.coefficient, OAI.DerivedBar.ParityBridge.suffixEmbed, OAI.DerivedBar.ParityBridge.outerSuffixEmbed

theorem OAI.DerivedBar.ParityBridge.parity_outerSuffixEmbed line 44

Source documentation

Exterior D comparison with the genuine free-bar differential and all later suffix faces. Negating the suffix differential gives the total sign (-1)^i.

theorem parity_outerSuffixEmbed (s n : ℕ) (e : M →ₗ[k] term k A N (s+1))
    (he : ∀ (d : D) (v : M), e (d • v) = (inl d : A) • e v)
    (v : D ⊗[k] term k D M (n+1)) :
    SquareZero.multibarTwoSidedDifferential k D X N ((s+1)+n)
      (outerSuffixEmbed k D X N M (s+1) (n+1) e v) =
    outerSuffixEmbed k D X N M (s+1) n e (DerivedBar.differential k D M (n+1) v) +
      (-1 : k)^n • AlgebraTensorModule.lTensor D D
        (termCast k D X N (show s+(n+1)=(s+1)+n by omega))
        (outerSuffixEmbed k D X N M s (n+1)
          ((SquareZero.multibarAugmentedDifferential k D X N s).comp e) v) := by
…

Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.multibarTwoSidedDifferential, OAI.DerivedBar.ParityBridge.outerSuffixEmbed, OAI.DerivedBar.differential, OAI.DerivedBar.ParityBridge.termCast, OAI.DerivedBar.SquareZero.multibarAugmentedDifferential

theorem OAI.DerivedBar.ParityBridge.parity_outerSuffixEmbed_zero line 77

Source documentation

At a zero-length leading D block the projected X endpoint is zero.

theorem parity_outerSuffixEmbed_zero (s : ℕ) (e : M →ₗ[k] term k A N (s+1))
    (he : ∀ v, FreeBaseChange.coefficient (fstHom k D X) (term k A N s) (e v) = 0)
    (v : D ⊗[k] M) :
    SquareZero.multibarTwoSidedDifferential k D X N s
      (outerSuffixEmbed k D X N M (s+1) 0 e v) =
    -outerSuffixEmbed k D X N M s 0
      ((SquareZero.multibarAugmentedDifferential k D X N s).comp e) v := by
…

Mentions: OAI.DerivedBar.term, OAI.DerivedBar.FreeBaseChange.coefficient, OAI.DerivedBar.SquareZero.multibarTwoSidedDifferential, OAI.DerivedBar.ParityBridge.outerSuffixEmbed, OAI.DerivedBar.SquareZero.multibarAugmentedDifferential