RecursiveTotalDifferential.lean`

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.RecursiveTotal.sumDesc line 19
Source documentation
Distribution over a finite direct sum, defined by its coproduct property.
```
def sumDesc {Y : ModuleCat.{u} D} (f : ∀ t, G.obj (V t) ⟶ Y) :
    G.obj (ModuleCat.of D (⨁ t, V t)) ⟶ Y :=
…
```
theorem OAI.DerivedBar.RecursiveTotal.lof_sumDesc line 26
theorem OAI.DerivedBar.RecursiveTotal.sum_hom_ext line 31
abbrev OAI.DerivedBar.RecursiveTotal.flat line 43
def OAI.DerivedBar.RecursiveTotal.lof line 46
abbrev OAI.DerivedBar.RecursiveTotal.assemble line 49
theorem OAI.DerivedBar.RecursiveTotal.lof_assemble line 53
def OAI.DerivedBar.RecursiveTotal.horizontal line 63
Source documentation
The horizontal face in a literal outer block; there is no face at length zero.
```
def horizontal (r n i q : ℕ) (h : i+q=n+1) (t : Index r q) :
    (degreeFunctor B r i).obj (summand B Z r q t) ⟶ flat B Z (r+1) n :=
…
```
Mentions: OAI.DerivedBar.RecursiveTotal.Index, OAI.DerivedBar.RecursiveTotal.degreeFunctor, OAI.DerivedBar.RecursiveTotal.summand, OAI.DerivedBar.RecursiveTotal.flat
def OAI.DerivedBar.RecursiveTotal.vertical line 72
Source documentation
The vertical face applies the already defined inner differential, with exactly the totalization sign (-1)^i, then distributes the resulting finite sum.
```
def vertical (r n i q : ℕ) (h : i+q=n+1) (t : Index r q)
    (d : ∀ q, flat B Z r (q+1) ⟶ flat B Z r q) :
    (degreeFunctor B r i).obj (summand B Z r q t) ⟶ flat B Z (r+1) n :=
…
```
Mentions: OAI.DerivedBar.RecursiveTotal.Index, OAI.DerivedBar.RecursiveTotal.flat, OAI.DerivedBar.RecursiveTotal.degreeFunctor, OAI.DerivedBar.RecursiveTotal.summand
def OAI.DerivedBar.RecursiveTotal.differential line 85
Source documentation
Independently recursive differential on the flattened direct sum. Its construction uses only the original functor differentials, finite-sum distribution, and the previously constructed inner differential, never the total differential.
```
def differential : (r n : ℕ) → flat B Z r (n+1) ⟶ flat B Z r n
  | 0, n => ModuleCat.ofHom (DirectSum.toModule D _ _
      (fun _ => (Z.d (n+1) n ≫ lof B Z 0 n ()).hom))
  | r+1, n => ModuleCat.ofHom (DirectSum.toModule D _ _
      (fun t => (horizontal B Z r n t.1.val.1 t.1.val.2 t.1.property t.2 +
        vertical B Z r n t.1.val.1 t.1.val.2 t.1.property t.2
          (differential r)).hom))

@[reassoc (attr := simp)]
```
Mentions: OAI.DerivedBar.RecursiveTotal.flat, OAI.DerivedBar.RecursiveTotal.lof, OAI.DerivedBar.RecursiveTotal.horizontal, OAI.DerivedBar.RecursiveTotal.vertical
theorem OAI.DerivedBar.RecursiveTotal.lof_differential_succ line 94
theorem OAI.DerivedBar.RecursiveTotal.sumDesc_assemble line 106
theorem OAI.DerivedBar.RecursiveTotal.horizontal_assemble line 120
Source documentation
The horizontal face agrees with the actual total on every nested tensor.
```
theorem horizontal_assemble (r n i q : ℕ) (h : i+q=n+1) (t : Index r q) :
    horizontal B Z r n i q h t ≫ assemble B Z (r+1) n =
      (degreeFunctor B r i).map (inclusion B Z r q t) ≫
        (bicomplex B r (iter B Z r)).d₁ c i q n := by
…
```
Mentions: OAI.DerivedBar.RecursiveTotal.Index, OAI.DerivedBar.RecursiveTotal.horizontal, OAI.DerivedBar.RecursiveTotal.assemble, OAI.DerivedBar.RecursiveTotal.degreeFunctor, OAI.DerivedBar.RecursiveTotal.inclusion, OAI.DerivedBar.RecursiveTotal.bicomplex, OAI.DerivedBar.RecursiveTotal.iter
theorem OAI.DerivedBar.RecursiveTotal.vertical_assemble line 142
Source documentation
The signed vertical face agrees with the actual total whenever the inner comparison has been proved; the induction below discharges that premise.
```
theorem vertical_assemble (r n i q : ℕ) (h : i+q=n+1) (t : Index r q)
    (ih : ∀ q, differential B Z r q ≫ assemble B Z r q =
      assemble B Z r (q+1) ≫ (iter B Z r).d (q+1) q) :
    vertical B Z r n i q h t (differential B Z r) ≫ assemble B Z (r+1) n =
      (degreeFunctor B r i).map (inclusion B Z r q t) ≫
        (bicomplex B r (iter B Z r)).d₂ c i q n := by
…
```
Mentions: OAI.DerivedBar.RecursiveTotal.Index, OAI.DerivedBar.RecursiveTotal.differential, OAI.DerivedBar.RecursiveTotal.assemble, OAI.DerivedBar.RecursiveTotal.iter, OAI.DerivedBar.RecursiveTotal.vertical, OAI.DerivedBar.RecursiveTotal.degreeFunctor, OAI.DerivedBar.RecursiveTotal.inclusion, OAI.DerivedBar.RecursiveTotal.bicomplex
theorem OAI.DerivedBar.RecursiveTotal.differential_assemble line 162
theorem OAI.DerivedBar.RecursiveTotal.differential_sq line 194
Source documentation
Square-zero is a consequence of the proved differential comparison.
```
theorem differential_sq (r n : ℕ) :
    differential B Z r (n+1) ≫ differential B Z r n = 0 := by
…
```
Mentions: OAI.DerivedBar.RecursiveTotal.differential
def OAI.DerivedBar.RecursiveTotal.flatComplex line 202
Source documentation
The direct sum with its independently recursive signed differential.
```
def flatComplex (r : ℕ) : ChainComplex (ModuleCat.{u} D) ℕ :=
…
```
def OAI.DerivedBar.RecursiveTotal.flattenChainIso line 207
Source documentation
An actual chain isomorphism flattening every recursive total, with both horizontal and signed vertical differential verified on literal summands.
```
def flattenChainIso (r : ℕ) : flatComplex B Z r ≅ iter B Z r :=
…
```
Mentions: OAI.DerivedBar.RecursiveTotal.flatComplex, OAI.DerivedBar.RecursiveTotal.iter