TotalBarDerived.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.DerivedBar.chainQuasiIso line 12
abbrev OAI.DerivedBar.chainDerived line 13
abbrev OAI.DerivedBar.chainQ line 14
def OAI.DerivedBar.ordinaryTensorToDerived line 20
Source documentation
Ordinary balanced tensor on chains followed by the quasi-isomorphism localization.
```
def ordinaryTensorToDerived : ChainComplex (ModuleCat.{u} D) ℕ ⥤ chainDerived D :=
…
```
Mentions: OAI.DerivedBar.chainDerived
theorem OAI.DerivedBar.tensorTotal_inverts line 24
def OAI.DerivedBar.derivedTensor line 32
Source documentation
Left derived balanced tensor on the localization of nonnegative chain complexes.
```
def derivedTensor : chainDerived D ⥤ chainDerived D :=
…
```
Mentions: OAI.DerivedBar.chainDerived
def OAI.DerivedBar.derivedTensorResolutionIso line 36
def OAI.DerivedBar.derivedTensorCounit line 41
instance OAI.DerivedBar.derivedTensor_isLeftDerivedFunctor line 47
Source documentation
The constructed tensor functor satisfies mathlib's genuine left-derived universal property, proved using the projective total bar and its augmentation.
```
instance derivedTensor_isLeftDerivedFunctor :
    (derivedTensor k D X).IsLeftDerivedFunctor (derivedTensorCounit k D X) (chainQuasiIso D) := by
…
```
Mentions: OAI.DerivedBar.derivedTensor, OAI.DerivedBar.derivedTensorCounit, OAI.DerivedBar.chainQuasiIso
def OAI.DerivedBar.derivedTensorExplicitIso line 64
Source documentation
The explicit two-sided total represents the genuine derived tensor of the input.
```
def derivedTensorExplicitIso (Z : ChainComplex (ModuleCat.{u} D) ℕ) :
    (derivedTensor k D X).obj ((chainQ D).obj Z) ≅
      (chainQ D).obj (BimoduleTensor.explicitBarTotal k D X Z) :=
…
```
Mentions: OAI.DerivedBar.derivedTensor, OAI.DerivedBar.chainQ, OAI.DerivedBar.BimoduleTensor.explicitBarTotal

def OAI.DerivedBar.derivedTensorIterate line 71

Source documentation

Genuine derived functor iteration, with the manuscript's right-to-left order.

def derivedTensorIterate : ℕ → (chainDerived D ⥤ chainDerived D)
  | 0 => 𝟭 _
  | r+1 => derivedTensorIterate r ⋙ derivedTensor k D X

/-- Successive resolve-and-tensor complexes represent iteration of the genuine
left derived functor. No derived comparison is included as a hypothesis. -/

Mentions: OAI.DerivedBar.chainDerived, OAI.DerivedBar.derivedTensor

def OAI.DerivedBar.derivedTensorIterateIso line 77

Source documentation

Successive resolve-and-tensor complexes represent iteration of the genuine left derived functor. No derived comparison is included as a hypothesis.

def derivedTensorIterateIso : (r : ℕ) →
    chainQ D ⋙ derivedTensorIterate k D X r ≅ tensorTotalIterate k D X r ⋙ chainQ D
  | 0 => (Functor.rightUnitor _ ) ≪≫ (Functor.leftUnitor _).symm
  | r+1 =>
    (Functor.associator _ _ _).symm ≪≫
      isoWhiskerRight (derivedTensorIterateIso r) (derivedTensor k D X) ≪≫
      Functor.associator _ _ _ ≪≫
      isoWhiskerLeft (tensorTotalIterate k D X r) (derivedTensorResolutionIso k D X) ≪≫
      (Functor.associator _ _ _).symm

/-- The independent recursive multibar. Every new block uses the explicit
endpoint-minus-tail horizontal differential and the standard vertical total sign. -/

Mentions: OAI.DerivedBar.chainQ, OAI.DerivedBar.derivedTensorIterate, OAI.DerivedBar.tensorTotalIterate, OAI.DerivedBar.derivedTensor, OAI.DerivedBar.derivedTensorResolutionIso, OAI.DerivedBar.differential

def OAI.DerivedBar.explicitMultibar line 89
Source documentation
The independent recursive multibar. Every new block uses the explicit endpoint-minus-tail horizontal differential and the standard vertical total sign.
```
def explicitMultibar : ℕ → ChainComplex (ModuleCat.{u} D) ℕ → ChainComplex (ModuleCat.{u} D) ℕ
  | 0, Z => Z
  | r+1, Z => BimoduleTensor.explicitBarTotal k D X (explicitMultibar r Z)
```
Mentions: OAI.DerivedBar.BimoduleTensor.explicitBarTotal
def OAI.DerivedBar.iterateExplicitMultibarIso line 93
def OAI.DerivedBar.derivedIterateMultibarIso line 100
Source documentation
The independent recursive multibar represents genuine finite derived iteration.
```
def derivedIterateMultibarIso (Z : ChainComplex (ModuleCat.{u} D) ℕ) (r : ℕ) :
    (derivedTensorIterate k D X r).obj ((chainQ D).obj Z) ≅
      (chainQ D).obj (explicitMultibar k D X r Z) :=
…
```
Mentions: OAI.DerivedBar.derivedTensorIterate, OAI.DerivedBar.chainQ, OAI.DerivedBar.explicitMultibar
def OAI.DerivedBar.derivedIterateLeadingBarIso line 107
Source documentation
The final leading D-bar resolution leaves the represented derived iterate unchanged.
```
def derivedIterateLeadingBarIso (Z : ChainComplex (ModuleCat.{u} D) ℕ) (r : ℕ) :
    (derivedTensorIterate k D X r).obj ((chainQ D).obj Z) ≅
      (chainQ D).obj (barTotal k D (explicitMultibar k D X r Z)) := by
…
```
Mentions: OAI.DerivedBar.derivedTensorIterate, OAI.DerivedBar.chainQ, OAI.DerivedBar.barTotal, OAI.DerivedBar.explicitMultibar