BimoduleBarComparisonMap.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.LittleFinitistic.BimoduleTotal.barModule line 18
abbrev OAI.LittleFinitistic.BimoduleTotal.actualBarFunctor line 19
def OAI.LittleFinitistic.BimoduleTotal.stalkChainIso line 22
Source documentation
The stalk total on extended chains agrees with the exact tensor functor used by DerivedBar.
```
def stalkChainIso : DerivedBar.integerExtension B ⋙
    functor k B (bimoduleStalk k B X) res.data.degrees
      (intervalDegrees_strictMono res.data.lower res.data.upper) ≅
    (actualBarFunctor (X := X)).mapHomologicalComplex (.down ℕ) ⋙ DerivedBar.integerExtension B :=
…
```
Mentions: OAI.DerivedBar.integerExtension, OAI.LittleFinitistic.BimoduleTotal.functor, OAI.LittleFinitistic.BimoduleTotal.bimoduleStalk, OAI.LittleFinitistic.BimoduleTotal.intervalDegrees_strictMono, OAI.LittleFinitistic.BimoduleTotal.actualBarFunctor
def OAI.LittleFinitistic.BimoduleTotal.resolvedStalkIso line 33
def OAI.LittleFinitistic.BimoduleTotal.actualBarResolutionIso line 45
Source documentation
The native bar functor's defining localization comparisons, with integer extension.
```
def actualBarResolutionIso :
    DerivedBar.chainQ B ⋙
      (DerivedBar.derivedTensor k B (barModule (X := X)) ⋙ DerivedBar.chainToIntegerDerived B) ≅
…
```
Mentions: OAI.DerivedBar.chainQ, OAI.DerivedBar.derivedTensor, OAI.LittleFinitistic.BimoduleTotal.barModule, OAI.DerivedBar.chainToIntegerDerived
def OAI.LittleFinitistic.BimoduleTotal.augmentationComparisonOnChains line 58
Source documentation
Actual comparison induced by the actual bimodule augmentation, before localization descent. Invertibility is a separate finite-total proof obligation.
```
def augmentationComparisonOnChains :
    DerivedBar.chainQ B ⋙ (DerivedBar.chainToIntegerDerived B ⋙ res.data.derived) ⟶
    DerivedBar.chainQ B ⋙
      (DerivedBar.derivedTensor k B (barModule (X := X)) ⋙ DerivedBar.chainToIntegerDerived B) :=
…
```
Mentions: OAI.DerivedBar.chainQ, OAI.DerivedBar.chainToIntegerDerived, OAI.DerivedBar.derivedTensor, OAI.LittleFinitistic.BimoduleTotal.barModule
def OAI.LittleFinitistic.BimoduleTotal.augmentationComparison line 71
Source documentation
The concrete augmentation comparison descends to the genuine chain localization. This constructs a map; it does not assert the still-unproved isomorphism property.
```
def augmentationComparison :
    DerivedBar.chainToIntegerDerived B ⋙ res.data.derived ⟶
      DerivedBar.derivedTensor k B (barModule (X := X)) ⋙ DerivedBar.chainToIntegerDerived B :=
…
```
Mentions: OAI.DerivedBar.chainToIntegerDerived, OAI.DerivedBar.derivedTensor, OAI.LittleFinitistic.BimoduleTotal.barModule
theorem OAI.LittleFinitistic.BimoduleTotal.augmentationComparison_fac line 79
Source documentation
Descent preserves the original comparison, rather than choosing an unrelated map.
```
theorem augmentationComparison_fac :
    whiskerLeft (DerivedBar.chainQ B) (augmentationComparison res i₀ hi₀) =
      augmentationComparisonOnChains res i₀ hi₀ :=
…
```
Mentions: OAI.DerivedBar.chainQ, OAI.LittleFinitistic.BimoduleTotal.augmentationComparison, OAI.LittleFinitistic.BimoduleTotal.augmentationComparisonOnChains