TotalBarContraction.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.barTotalDH line 20
Source documentation
Horizontal contribution with the declared total object as codomain.
```
def barTotalDH (i q n : ℕ) : (F).obj (((B).X i).X q) ⟶ (F).obj ((T).X n) :=
…
```
def OAI.DerivedBar.barTotalDV line 24
Source documentation
Vertical contribution with the declared total object as codomain.
```
def barTotalDV (i q n : ℕ) : (F).obj (((B).X i).X q) ⟶ (F).obj ((T).X n) :=
…
```
def OAI.DerivedBar.barUnit line 28
Source documentation
Unit insertion on an individual bar term, viewed as an additive map.
```
def barUnit (i q : ℕ) :
    AddCommGrpCat.of (term k A (Z.X q) i) ⟶ AddCommGrpCat.of (term k A (Z.X q) (i+1)) :=
…
```
Mentions: OAI.DerivedBar.term
def OAI.DerivedBar.barRaise line 33
Source documentation
Unit insertion with the exact bicomplex source and target objects.
```
def barRaise (i q : ℕ) :
    (F).obj (((B).X i).X q) ⟶ (F).obj (((B).X (i+1)).X q) :=
…
```
def OAI.DerivedBar.barTotalH line 38
Source documentation
Natural unit insertion in the total bar, increasing bar length by one.
```
def barTotalH (n : ℕ) : (F).obj ((T).X n) ⟶ (F).obj ((T).X (n+1)) :=
…
```
theorem OAI.DerivedBar.ι_barTotalH line 43
def OAI.DerivedBar.barTotalSectionF line 50
Source documentation
Unit insertion in bar length zero gives the additive section.
```
def barTotalSectionF (n : ℕ) : (F).obj (Z.X n) ⟶ (F).obj ((T).X n) :=
…
```
theorem OAI.DerivedBar.barTotalSectionF_augmentation line 54

theorem OAI.DerivedBar.barUnit_natural line 65

Source documentation

Naturality of unit insertion under the input differential.

theorem barUnit_natural (i p q : ℕ) :
    (F).map (ModuleCat.ofHom (termMap k A (Z.X p) (Z.X q) (Z.d p q).hom i)) ≫
      barUnit k A Z i q =
    barUnit k A Z i p ≫
      (F).map (ModuleCat.ofHom (termMap k A (Z.X p) (Z.X q) (Z.d p q).hom (i+1))) := by
…

Mentions: OAI.DerivedBar.termMap, OAI.DerivedBar.barUnit

theorem OAI.DerivedBar.barTotalSectionF_comm line 74

Source documentation

The additive section commutes with the input differential.

theorem barTotalSectionF_comm (n : ℕ) :
    barTotalSectionF k A Z (n+1) ≫ (F).map ((T).d (n+1) n) =
      (F).map (Z.d (n+1) n) ≫ barTotalSectionF k A Z n := by
…

Mentions: OAI.DerivedBar.barTotalSectionF

theorem OAI.DerivedBar.barUnit_identity line 88

Source documentation

The row contraction identity, expressed in additive maps.

theorem barUnit_identity (i q : ℕ) :
    barUnit k A Z (i+1) q ≫ (F).map (ModuleCat.ofHom (differential k A (Z.X q) (i+1))) +
      (F).map (ModuleCat.ofHom (differential k A (Z.X q) i)) ≫ barUnit k A Z i q = 𝟙 _ := by
…

Mentions: OAI.DerivedBar.barUnit, OAI.DerivedBar.differential

theorem OAI.DerivedBar.ι_barTotal_d line 95
theorem OAI.DerivedBar.barTotal_vertical_cancel line 105
Source documentation
The vertical contributions cancel because unit insertion changes bar parity.
```
theorem barTotal_vertical_cancel (i q n : ℕ) (h : i+q=n) :
    barTotalDV k A Z i (q+1) n ≫ barTotalH k A Z n +
      barRaise k A Z i (q+1) ≫ barTotalDV k A Z (i+1) (q+1) (n+1) = 0 := by
…
```
Mentions: OAI.DerivedBar.barTotalDV, OAI.DerivedBar.barTotalH, OAI.DerivedBar.barRaise
theorem OAI.DerivedBar.barTotalH_identity_zero line 119
Source documentation
Total contraction equation in degree zero.
```
theorem barTotalH_identity_zero :
    barTotalH k A Z 0 ≫ (F).map ((T).d 1 0) +
      (F).map ((barTotalAugmentation k A Z).f 0) ≫ barTotalSectionF k A Z 0 = 𝟙 _ := by
…
```
Mentions: OAI.DerivedBar.barTotalH, OAI.DerivedBar.barTotalAugmentation, OAI.DerivedBar.barTotalSectionF
theorem OAI.DerivedBar.barTotal_horizontal_identity line 150
theorem OAI.DerivedBar.add_interleave line 190

theorem OAI.DerivedBar.barTotalH_identity_succ line 195

Source documentation

Total contraction equation in every positive degree.

theorem barTotalH_identity_succ (n : ℕ) :
    (F).map ((T).d (n+1) n) ≫ barTotalH k A Z n +
      barTotalH k A Z (n+1) ≫ (F).map ((T).d (n+2) (n+1)) +
      (F).map ((barTotalAugmentation k A Z).f (n+1)) ≫
        barTotalSectionF k A Z (n+1) = 𝟙 _ := by
…

Mentions: OAI.DerivedBar.barTotalH, OAI.DerivedBar.barTotalAugmentation, OAI.DerivedBar.barTotalSectionF