RecursiveSuffixFaces.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DerivedBar.ParityBridge.parity_termCast line 26
Source documentation
The original augmented parity operator commutes with degree transport.
```
theorem parity_termCast {a b : ℕ} (h : a=b) (h' : a+1=b+1)
    (v : term k A N (a+1)) :
    SquareZero.multibarAugmentedDifferential k D X N b (termCast k D X N h' v) =
      termCast k D X N h (SquareZero.multibarAugmentedDifferential k D X N a v) := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.multibarAugmentedDifferential, OAI.DerivedBar.ParityBridge.termCast

theorem OAI.DerivedBar.ParityBridge.parity_barSuffix line 34

Source documentation

Positive-block face comparison for the actual categorical bar functor.

theorem parity_barSuffix (V : ModuleCat.{u} D) (s i : ℕ)
    (e : V →ₗ[k] term k A N (s+1))
    (he : ∀ (d : D) (v : V), e (d • v) = (inl d : A) • e v)
    (v : ((XB).obj V).X (i+1)) :
    SquareZero.multibarAugmentedDifferential k D X N (((s+1)+i)+1)
      (barSuffix k D X N V (s+1) (i+1) e v) =
    -barSuffix k D X N V (s+1) i e ((((XB).obj V).d (i+1) i).hom v) +
      (-1:k)^(i+1) • termCast k D X N (show (s+(i+1))+1=((s+1)+i)+1 by omega)
        (barSuffix k D X N V s (i+1)
          ((SquareZero.multibarAugmentedDifferential k D X N s).comp e) v) := by
…

Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.multibarAugmentedDifferential, OAI.DerivedBar.ParityBridge.barSuffix, OAI.DerivedBar.ParityBridge.termCast

theorem OAI.DerivedBar.ParityBridge.parity_barSuffix_zero line 52

Source documentation

Empty blocks retain the suffix face with no extra sign.

theorem parity_barSuffix_zero (V : ModuleCat.{u} D) (s : ℕ)
    (e : V →ₗ[k] term k A N (s+1))
    (he : ∀ (x : X) (v : V), (inr x : A) • e v = 0)
    (v : ((XB).obj V).X 0) :
    SquareZero.multibarAugmentedDifferential k D X N (s+1)
      (barSuffix k D X N V (s+1) 0 e v) =
    barSuffix k D X N V s 0
      ((SquareZero.multibarAugmentedDifferential k D X N s).comp e) v :=
…

Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.multibarAugmentedDifferential, OAI.DerivedBar.ParityBridge.barSuffix

theorem OAI.DerivedBar.ParityBridge.parity_barSuffix_endpoint line 63
Source documentation
A terminal empty block has zero face by the actual inflation of N.
```
theorem parity_barSuffix_endpoint (V : ModuleCat.{u} D)
    (e : V →ₗ[k] term k A N 0) (v : ((XB).obj V).X 0) :
    SquareZero.multibarAugmentedDifferential k D X N 0
      (barSuffix k D X N V 0 0 e v) = 0 := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.multibarAugmentedDifferential, OAI.DerivedBar.ParityBridge.barSuffix
theorem OAI.DerivedBar.ParityBridge.barSuffix_neg line 77
Source documentation
Prefix insertion is linear in the complete suffix map.
```
theorem barSuffix_neg (V : ModuleCat.{u} D) (s i : ℕ)
    (e : V →ₗ[k] term k A N s) :
    barSuffix k D X N V s i (-e) = -barSuffix k D X N V s i e := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.ParityBridge.barSuffix
theorem OAI.DerivedBar.ParityBridge.barSuffix_zero line 91

theorem OAI.DerivedBar.ParityBridge.barSuffix_termCast line 106

Source documentation

Prefix insertion commutes with exact degree casts on a suffix.

theorem barSuffix_termCast (V : ModuleCat.{u} D) {a b : ℕ} (h : a=b) (i : ℕ)
    (e : V →ₗ[k] term k A N a) (v : ((XB).obj V).X i) :
    barSuffix k D X N V b i ((termCast k D X N h).comp e) v =
      termCast k D X N (show (a+i)+1=(b+i)+1 by omega)
        (barSuffix k D X N V a i e v) := by
…

Mentions: OAI.DerivedBar.term, OAI.DerivedBar.ParityBridge.barSuffix, OAI.DerivedBar.ParityBridge.termCast

theorem OAI.DerivedBar.ParityBridge.suffixEmbed_id line 114
theorem OAI.DerivedBar.ParityBridge.idealSuffixEmbed_id line 127
theorem OAI.DerivedBar.ParityBridge.innerEmbedding_zero_lof line 137
Source documentation
The degree-zero input embedding is the identity on its sole summand.
```
theorem innerEmbedding_zero_lof (t : RecursiveTotal.Index 0 0) :
    (innerEmbedding k D X N 0 0).comp
      ((RecursiveTotal.lof B Z 0 0 t).hom.restrictScalars k) = LinearMap.id := by
…
```
Mentions: OAI.DerivedBar.RecursiveTotal.Index, OAI.DerivedBar.ParityBridge.innerEmbedding, OAI.DerivedBar.RecursiveTotal.lof

theorem OAI.DerivedBar.ParityBridge.parity_barSuffix_terminal line 146

Source documentation

The terminal positive X bar has exactly minus its original bar differential.

theorem parity_barSuffix_terminal (i : ℕ) (v : ((XB).obj N).X (i+1)) :
    SquareZero.multibarAugmentedDifferential k D X N ((0+i)+1)
      (barSuffix k D X N N 0 (i+1) LinearMap.id v) =
    -barSuffix k D X N N 0 i LinearMap.id
      ((((XB).obj N).d (i+1) i).hom v) := by
…

Mentions: OAI.DerivedBar.SquareZero.multibarAugmentedDifferential, OAI.DerivedBar.ParityBridge.barSuffix

theorem OAI.DerivedBar.ParityBridge.innerEmbedding_bottom line 162
Source documentation
The augmented bottom face vanishes at every recursive depth.
```
theorem innerEmbedding_bottom (r : ℕ) (v : RecursiveTotal.flat B Z (r+1) 0) :
    SquareZero.multibarAugmentedDifferential k D X N r
      (termCast k D X N (show (r+1)+0=r+1 by omega)
        (innerEmbedding k D X N (r+1) 0 v)) = 0 := by
…
```
Mentions: OAI.DerivedBar.RecursiveTotal.flat, OAI.DerivedBar.SquareZero.multibarAugmentedDifferential, OAI.DerivedBar.ParityBridge.termCast, OAI.DerivedBar.ParityBridge.innerEmbedding