BarFunctor.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.termMap line 18

Source documentation

Functorial map on every augmented bar term.

def termMap (h : V →ₗ[A] W) : (n : ℕ) → term k A V n →ₗ[A] term k A W n
  | 0 => h
  | n+1 => AlgebraTensorModule.lTensor A A ((termMap h n).restrictScalars k)

Mentions: OAI.DerivedBar.term

theorem OAI.DerivedBar.termMap_tmul line 22
theorem OAI.DerivedBar.termMap_comp line 25
theorem OAI.DerivedBar.termMap_id line 37
theorem OAI.DerivedBar.termMap_zero line 47

theorem OAI.DerivedBar.differential_natural line 57

Source documentation

The bar differential is natural for all module maps.

theorem differential_natural (h : V →ₗ[A] W) (n : ℕ) :
    (differential k A W n).comp (termMap k A V W h (n+1)) =
      (termMap k A V W h n).comp (differential k A V n) := by
…

Mentions: OAI.DerivedBar.differential, OAI.DerivedBar.termMap

theorem OAI.DerivedBar.contraction_natural line 81
Source documentation
Unit insertion is natural over k, the key homotopy for the total bar augmentation.
```
theorem contraction_natural (h : V →ₗ[A] W) (n : ℕ) (v : term k A V n) :
    termMap k A V W h (n+1) (contraction k A V n v) =
      contraction k A W n (termMap k A V W h n v) := rfl
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.termMap, OAI.DerivedBar.contraction
def OAI.DerivedBar.complexMap line 86
Source documentation
An actual chain map between unaugmented free bar resolutions.
```
def complexMap (h : V →ₗ[A] W) : complex k A V ⟶ complex k A W where
…
```
Mentions: OAI.DerivedBar.complex
def OAI.DerivedBar.barFunctor line 100
Source documentation
The explicit free bar resolution is functorial, not just an objectwise choice.
```
def barFunctor : ModuleCat.{u} A ⥤ ChainComplex (ModuleCat.{u} A) ℕ where
…
```
instance OAI.DerivedBar.barFunctor_preservesZero line 114
def OAI.DerivedBar.barBicomplex line 124
Source documentation
The bicomplex for the left-module bar resolution of a nonnegative chain complex. Outer degree is the bar length; inner degree is the input complex degree. The two differentials commute by the proved naturality of the absolute bar differential.
```
def barBicomplex (Z : ChainComplex (ModuleCat.{u} A) ℕ) :
    HomologicalComplex₂ (ModuleCat.{u} A) (ComplexShape.down ℕ) (ComplexShape.down ℕ) :=
…
```
instance OAI.DerivedBar.barBicomplex_projective line 129
Source documentation
Each entry in the bar bicomplex is genuinely projective over A.
```
instance barBicomplex_projective (Z : ChainComplex (ModuleCat.{u} A) ℕ) (i q : ℕ) :
    Projective (((barBicomplex k A Z).X i).X q) := by
…
```
Mentions: OAI.DerivedBar.barBicomplex
def OAI.DerivedBar.barTotal line 136
Source documentation
The ordinary direct-sum total bar complex, with standard totalization signs. The total augmentation quasi-isomorphism must still be proved.
```
def barTotal (Z : ChainComplex (ModuleCat.{u} A) ℕ) :
    ChainComplex (ModuleCat.{u} A) ℕ :=
…
```