Bar.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.term line 21
Source documentation
The augmented bar terms: term 0 is N; term (n+1) is A ⊗ term n.
```
@[reducible] def term : ℕ → ModuleCat k
  | 0 => ModuleCat.of k N
  | n+1 => ModuleCat.of k (A ⊗[k] term n)
```
instance OAI.DerivedBar.termModule line 25
instance OAI.DerivedBar.termTower line 29
def OAI.DerivedBar.action line 35
Source documentation
Multiplication/action on the first two positions of an augmented bar word.
```
def action (M : Type u) [AddCommGroup M] [Module k M] [Module A M]
    [IsScalarTower k A M] : A ⊗[k] M →ₗ[A] M :=
…
```
theorem OAI.DerivedBar.action_tmul line 44

def OAI.DerivedBar.differential line 49

Source documentation

Recursive alternating face differential. No A-flatness of N is required.

def differential : (n : ℕ) → term k A N (n+1) →ₗ[A] term k A N n
  | 0 => action k A N
  | n+1 => action k A (term k A N (n+1)) -
      AlgebraTensorModule.lTensor A A ((differential n).restrictScalars k)

Mentions: OAI.DerivedBar.term, OAI.DerivedBar.action

theorem OAI.DerivedBar.differential_zero_tmul line 54
theorem OAI.DerivedBar.differential_succ_tmul line 57
theorem OAI.DerivedBar.differential_sq line 62
Source documentation
The actual bar differential squares to zero in every degree.
```
theorem differential_sq (n : ℕ) :
    (differential k A N n).comp (differential k A N (n+1)) = 0 := by
…
```
Mentions: OAI.DerivedBar.differential
def OAI.DerivedBar.contraction line 82
Source documentation
Unit insertion; this is k-linear, generally not A-linear.
```
def contraction (n : ℕ) : term k A N n →ₗ[k] term k A N (n+1) :=
…
```
Mentions: OAI.DerivedBar.term
theorem OAI.DerivedBar.contraction_apply line 86
theorem OAI.DerivedBar.contraction_zero line 90
Source documentation
The augmented degree-zero contraction identity.
```
theorem contraction_zero (z : N) :
    differential k A N 0 (contraction k A N 0 z) = z := by
…
```
Mentions: OAI.DerivedBar.differential, OAI.DerivedBar.contraction
theorem OAI.DerivedBar.contraction_identity line 96
Source documentation
Contracting homotopy in every positive augmented degree.
```
theorem contraction_identity (n : ℕ) (z : term k A N (n+1)) :
    differential k A N (n+1) (contraction k A N (n+1) z) +
      contraction k A N n (differential k A N n z) = z := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.differential, OAI.DerivedBar.contraction
theorem OAI.DerivedBar.differential_exact line 103
Source documentation
Exactness of the augmented absolute bar complex as actual A-linear maps.
```
theorem differential_exact (n : ℕ) :
    LinearMap.range (differential k A N (n+1)) =
      LinearMap.ker (differential k A N n) := by
…
```
Mentions: OAI.DerivedBar.differential
def OAI.DerivedBar.augmentedComplex line 116
Source documentation
The augmented chain complex, including N at homological degree zero.
```
def augmentedComplex : ChainComplex (ModuleCat A) ℕ :=
…
```
def OAI.DerivedBar.complex line 122
Source documentation
The unaugmented absolute bar complex, degree n = A ⊗ A^⊗n ⊗ N.
```
def complex : ChainComplex (ModuleCat A) ℕ :=
…
```
instance OAI.DerivedBar.term_free line 131
Source documentation
Every unaugmented bar term is free as a left A-module, even for noncommutative A.
```
instance term_free (n : ℕ) : Module.Free A (term k A N (n+1)) :=
…
```
Mentions: OAI.DerivedBar.term
instance OAI.DerivedBar.complex_projective line 134
theorem OAI.DerivedBar.augmentation_surjective line 139
Source documentation
Surjectivity of the bar augmentation, witnessed by insertion of 1.
```
theorem augmentation_surjective : Function.Surjective (differential k A N 0) := by
…
```
Mentions: OAI.DerivedBar.differential
def OAI.DerivedBar.augmentation line 144
Source documentation
The bar augmentation as a chain map to N concentrated in degree zero.
```
def augmentation : complex k A N ⟶ (ChainComplex.single₀ (ModuleCat A)).obj (ModuleCat.of A N) :=
…
```
Mentions: OAI.DerivedBar.complex
theorem OAI.DerivedBar.complex_exactAt_succ line 152
Source documentation
All positive-degree homology of the unaugmented bar complex vanishes.
```
theorem complex_exactAt_succ (n : ℕ) : (complex k A N).ExactAt (n+1) := by
…
```
Mentions: OAI.DerivedBar.complex
theorem OAI.DerivedBar.augmentation_exact line 159
Source documentation
Exactness at the augmentation term, stated in the abelian category of A-modules.
```
theorem augmentation_exact :
    (ShortComplex.mk ((complex k A N).d 1 0) (ModuleCat.ofHom (differential k A N 0))
      (ModuleCat.hom_ext (differential_sq k A N 0))).Exact := by
…
```
Mentions: OAI.DerivedBar.complex, OAI.DerivedBar.differential, OAI.DerivedBar.differential_sq
instance OAI.DerivedBar.augmentation_epi line 165
instance OAI.DerivedBar.augmentation_quasiIso line 169
Source documentation
The absolute algebra bar augmentation is a genuine quasi-isomorphism.
```
instance augmentation_quasiIso : QuasiIso (augmentation k A N) := by
…
```
Mentions: OAI.DerivedBar.augmentation
def OAI.DerivedBar.projectiveResolution line 183
Source documentation
Explicit free absolute bar resolution, packaged for derived functor computations.
```
def projectiveResolution : ProjectiveResolution (ModuleCat.of A N) where
…
```