TotalBarTensor.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

instance OAI.DerivedBar.barTotalFunctor_map_quasiIso line 13
Source documentation
Resolving a quasi-isomorphism gives a quasi-isomorphism between projective complexes.
```
instance barTotalFunctor_map_quasiIso {Z W : ChainComplex (ModuleCat.{u} D) ℕ}
    (f : Z ⟶ W) [QuasiIso f] : QuasiIso ((barTotalFunctor k D).map f) := by
…
```
Mentions: OAI.DerivedBar.barTotalFunctor

theorem OAI.DerivedBar.additive_map_quasiIso_of_projective line 22

Source documentation

Additive functors preserve quasi-isomorphisms between nonnegative projective complexes. This uses the proved homotopy-equivalence criterion, not a flatness hypothesis.

theorem additive_map_quasiIso_of_projective (G : ModuleCat.{u} D ⥤ ModuleCat.{u} D)
    [G.Additive] {P Q : ChainComplex (ModuleCat.{u} D) ℕ}
    [∀ n, Projective (P.X n)] [∀ n, Projective (Q.X n)]
    (f : P ⟶ Q) [QuasiIso f] :
    QuasiIso ((G.mapHomologicalComplex (ComplexShape.down ℕ)).map f) := by
…

def OAI.DerivedBar.tensorTotalFunctor line 35
Source documentation
Resolve the entire input complex before applying the actual balanced tensor functor.
```
def tensorTotalFunctor : ChainComplex (ModuleCat.{u} D) ℕ ⥤ ChainComplex (ModuleCat.{u} D) ℕ :=
…
```
instance OAI.DerivedBar.tensorTotalFunctor_map_quasiIso line 40
Source documentation
The resolved tensor construction preserves all quasi-isomorphisms.
```
instance tensorTotalFunctor_map_quasiIso {Z W : ChainComplex (ModuleCat.{u} D) ℕ}
    (f : Z ⟶ W) [QuasiIso f] : QuasiIso ((tensorTotalFunctor k D X).map f) := by
…
```
Mentions: OAI.DerivedBar.tensorTotalFunctor
instance OAI.DerivedBar.tensorTotalAugmentation_quasiIso line 49
Source documentation
On a projective chain input, tensoring the augmentation is a quasi-isomorphism, even when X is not flat. This identifies the construction with tensor of that projective model.
```
instance tensorTotalAugmentation_quasiIso (P : ChainComplex (ModuleCat.{u} D) ℕ)
    [∀ n, Projective (P.X n)] :
    QuasiIso (((BimoduleTensor.tensorFunctor k D X).mapHomologicalComplex (ComplexShape.down ℕ)).map
      (barTotalAugmentation k D P)) := by
…
```
Mentions: OAI.DerivedBar.BimoduleTensor.tensorFunctor, OAI.DerivedBar.barTotalAugmentation
def OAI.DerivedBar.tensorTotalIterate line 59
Source documentation
Repeated resolution and balanced tensor, proceeding from the right as in Section 6. The identification with the independently signed literal multibar is a separate obligation.
```
def tensorTotalIterate : ℕ → (ChainComplex (ModuleCat.{u} D) ℕ ⥤ ChainComplex (ModuleCat.{u} D) ℕ)
  | 0 => 𝟭 _
  | r+1 => tensorTotalIterate r ⋙ tensorTotalFunctor k D X
```
Mentions: OAI.DerivedBar.tensorTotalFunctor
instance OAI.DerivedBar.tensorTotalIterate_map_quasiIso line 63