RecursivePrefixInclusions.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DerivedBar.ParityBridge.hom_square_of_heq line 12
theorem OAI.DerivedBar.ParityBridge.hom_heq_of_square line 19
theorem OAI.DerivedBar.ParityBridge.barInclusionStep_heq line 24
theorem OAI.DerivedBar.ParityBridge.barInclusionStep_target line 38
theorem OAI.DerivedBar.ParityBridge.leadingIter_prefix line 61
theorem OAI.DerivedBar.ParityBridge.leadingInclusion_prefix_heq line 66
Source documentation
Literal recursive inclusions depend only on the functors in their prefix.
```
theorem leadingInclusion_prefix_heq (r m n : ℕ) (h : m≤r) (t : Index m n) :
    HEq (inclusion (leadingBarSequence k D X r) Z m n t) (inclusion B Z m n t) := by
…
```
Mentions: OAI.DerivedBar.leadingBarSequence
theorem OAI.DerivedBar.ParityBridge.leadingInclusion_prefix line 81
theorem OAI.DerivedBar.ParityBridge.leadingIter_total line 88
Source documentation
The final total agrees with the actual exterior bar on the constant-X prefix.
```
theorem leadingIter_total (r : ℕ) :
    iter (leadingBarSequence k D X r) Z (r+1) = barTotal k D (iter B Z r) :=
…
```
Mentions: OAI.DerivedBar.leadingBarSequence, OAI.DerivedBar.barTotal
theorem OAI.DerivedBar.ParityBridge.leadingSummand_last line 93

theorem OAI.DerivedBar.ParityBridge.leadingInclusion_total line 100

Source documentation

The exterior inclusion is exactly the free-bar map of the original inner inclusion.

theorem leadingInclusion_total (r n i q : ℕ) (h : i+q=n) (t : Index r q) :
    inclusion (leadingBarSequence k D X r) Z (r+1) n ⟨⟨⟨i,q⟩,h⟩,t⟩ ≫
      eqToHom (congrArg (fun W => W.X n) (leadingIter_total k D X N r)) =
    eqToHom (leadingSummand_last k D X N r n i q h t) ≫
    (barFunctor k D ⋙ HomologicalComplex.eval _ c i).map
      (eqToHom (leadingSummand_prefix k D X Z r r q le_rfl t) ≫ inclusion B Z r q t) ≫
        (barBicomplex k D (iter B Z r)).ιTotal c i q n h := by
…

Mentions: OAI.DerivedBar.leadingBarSequence, OAI.DerivedBar.ParityBridge.leadingIter_total, OAI.DerivedBar.ParityBridge.leadingSummand_last, OAI.DerivedBar.barFunctor, OAI.DerivedBar.barBicomplex