TotalBar.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

instance OAI.DerivedBar.barTotal_projective line 16
Source documentation
Total terms are projective for every nonnegative input, without projectivity or flatness assumptions on the input terms.
```
instance barTotal_projective (Z : ChainComplex (ModuleCat.{u} A) ℕ) (n : ℕ) :
    Projective ((barTotal k A Z).X n) where
…
```
Mentions: OAI.DerivedBar.barTotal
def OAI.DerivedBar.barTotalAugmentationF line 33
Source documentation
The augmentation is the action in bar length zero and zero elsewhere.
```
def barTotalAugmentationF (n : ℕ) : (T).X n ⟶ Z.X n :=
…
```
theorem OAI.DerivedBar.ι_barTotalAugmentationF_zero line 40
theorem OAI.DerivedBar.ι_barTotalAugmentationF_succ line 47

theorem OAI.DerivedBar.barTotal_d₁_succ line 52

Source documentation

Horizontal face formula in positive bar length.

theorem barTotal_d₁_succ (i q n : ℕ) (h : i+q=n) :
    (B).d₁ c (i+1) q n =
      ModuleCat.ofHom (differential k A (Z.X q) (i+1)) ≫ (B).ιTotal c i q n h := by
…

Mentions: OAI.DerivedBar.differential

theorem OAI.DerivedBar.barTotal_d₁_zero line 61
Source documentation
The horizontal differential is absent in bar length zero.
```
@[simp] theorem barTotal_d₁_zero (q n : ℕ) : (B).d₁ c 0 q n = 0 := by
…
```
theorem OAI.DerivedBar.barTotal_d₂_zero line 66
Source documentation
The vertical differential is absent in input degree zero.
```
@[simp] theorem barTotal_d₂_zero (i n : ℕ) : (B).d₂ c i 0 n = 0 := by
…
```

theorem OAI.DerivedBar.barTotal_d₂_succ line 71

Source documentation

Vertical face formula, with the standard totalization sign.

theorem barTotal_d₂_succ (i q n : ℕ) (h : i+q=n) :
    (B).d₂ c i (q+1) n =
      ((-1 : ℤˣ)^i) • (ModuleCat.ofHom
        (termMap k A (Z.X (q+1)) (Z.X q) (Z.d (q+1) q).hom (i+1)) ≫
          (B).ιTotal c i q n h) := by
…

Mentions: OAI.DerivedBar.termMap

theorem OAI.DerivedBar.barTotalAugmentation_comm line 80

Source documentation

The total augmentation is a chain map.

theorem barTotalAugmentation_comm (n : ℕ) :
    (T).d (n+1) n ≫ barTotalAugmentationF k A Z n =
      barTotalAugmentationF k A Z (n+1) ≫ Z.d (n+1) n := by
…

Mentions: OAI.DerivedBar.barTotalAugmentationF

def OAI.DerivedBar.barTotalAugmentation line 124