SuffixNaturality.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DerivedBar.ParityBridge.suffixEmbed_termMap line 24
Source documentation
Inserting D slots commutes with every actual vertical map of suffix modules.
```
theorem suffixEmbed_termMap (s n : ℕ) (e : W →ₗ[k] term k A N s)
    (f : M →ₗ[D] W) (v : term k D M n) :
    suffixEmbed k D X N W s e n (termMap k D M W f n v) =
    suffixEmbed k D X N M s (e.comp (f.restrictScalars k)) n v := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.ParityBridge.suffixEmbed, OAI.DerivedBar.termMap

theorem OAI.DerivedBar.ParityBridge.idealSuffixEmbed_termMap line 38

Source documentation

X coefficients commute with the same vertical suffix maps.

theorem idealSuffixEmbed_termMap (s n : ℕ) (e : W →ₗ[k] term k A N s)
    (f : M →ₗ[D] W) (v : X ⊗[k] term k D M n) :
    idealSuffixEmbed k D X N W s n e
      (AlgebraTensorModule.lTensor D X ((termMap k D M W f n).restrictScalars k) v) =
    idealSuffixEmbed k D X N M s n (e.comp (f.restrictScalars k)) v := by
…

Mentions: OAI.DerivedBar.term, OAI.DerivedBar.ParityBridge.idealSuffixEmbed, OAI.DerivedBar.termMap

theorem OAI.DerivedBar.ParityBridge.outerSuffixEmbed_termMap line 52

Source documentation

Exterior D coefficients commute with all vertical suffix maps.

theorem outerSuffixEmbed_termMap (s n : ℕ) (e : W →ₗ[k] term k A N s)
    (f : M →ₗ[D] W) (v : D ⊗[k] term k D M n) :
    outerSuffixEmbed k D X N W s n e (termMap k D M W f (n+1) v) =
    outerSuffixEmbed k D X N M s n (e.comp (f.restrictScalars k)) v := by
…

Mentions: OAI.DerivedBar.term, OAI.DerivedBar.ParityBridge.outerSuffixEmbed, OAI.DerivedBar.termMap

theorem OAI.DerivedBar.ParityBridge.suffixEmbed_add_map line 63

Source documentation

The prefix construction is additive in the whole suffix map.

theorem suffixEmbed_add_map (s n : ℕ) (e f : M →ₗ[k] term k A N s)
    (v : term k D M n) :
    suffixEmbed k D X N M s (e+f) n v =
      suffixEmbed k D X N M s e n v + suffixEmbed k D X N M s f n v := by
…

Mentions: OAI.DerivedBar.term, OAI.DerivedBar.ParityBridge.suffixEmbed

theorem OAI.DerivedBar.ParityBridge.suffixEmbed_smul_map line 77
Source documentation
Scalar totalization signs pass through the unchanged tensor prefix.
```
theorem suffixEmbed_smul_map (s n : ℕ) (a : k) (e : M →ₗ[k] term k A N s)
    (v : term k D M n) :
    suffixEmbed k D X N M s (a • e) n v = a • suffixEmbed k D X N M s e n v := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.ParityBridge.suffixEmbed
def OAI.DerivedBar.ParityBridge.suffixEmbedLinear line 90
Source documentation
A genuine linear operation on suffix maps, so finite sums distribute exactly.
```
def suffixEmbedLinear (s n : ℕ) :
    (M →ₗ[k] term k A N s) →ₗ[k] (term k D M n →ₗ[k] term k A N (s+n)) where
…
```
Mentions: OAI.DerivedBar.term

theorem OAI.DerivedBar.ParityBridge.suffixEmbed_sum line 102

Source documentation

The actual finite-sum distribution needed for an arbitrary recursive suffix differential.

theorem suffixEmbed_sum {I : Type*} (S : Finset I) (s n : ℕ)
    (e : I → M →ₗ[k] term k A N s) (v : term k D M n) :
    suffixEmbed k D X N M s (∑ i ∈ S, e i) n v =
      ∑ i ∈ S, suffixEmbed k D X N M s (e i) n v := by
…

Mentions: OAI.DerivedBar.term, OAI.DerivedBar.ParityBridge.suffixEmbed

theorem OAI.DerivedBar.ParityBridge.totalSign_smul line 111
Source documentation
Mathlib's unit-valued totalization sign is exactly the field-valued sign.
```
theorem totalSign_smul (n : ℕ) (v : M) :
    ((-1 : ℤˣ)^n) • v = (-1 : k)^n • v := by
…
```