PDBarTensorComparison.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.PDBarQuotient.scalarEquiv line 17
Source documentation
The restricted scalar convention in the detector agrees with the original compatible k action by actual tensor maps in both directions.
```
def scalarEquiv :
    (PDTensor.tensorFunctor k A (RightBase f)).obj (ModuleCat.of A V) ≃ₗ[k]
      BalancedTensor.Tensor k A (RightBase f) V :=
…
```
Mentions: OAI.LittleFinitistic.PDTensor.tensorFunctor, OAI.LittleFinitistic.PDBarQuotient.RightBase, OAI.LittleFinitistic.BalancedTensor.Tensor
def OAI.LittleFinitistic.PDBarQuotient.nativeScalarEquiv line 28
def OAI.LittleFinitistic.PDBarQuotient.objectIso line 38
theorem OAI.LittleFinitistic.PDBarQuotient.objectIso_natural line 45
def OAI.LittleFinitistic.PDBarQuotient.barQuotientIso line 58
Source documentation
The detector's tensor of the actual bar resolution is the bar worker's balanced complex, after restricting only its exterior scalars.
```
def barQuotientIso :
    ((PDTensor.tensorFunctor k A (RightBase f)).mapHomologicalComplex _).obj
      (DerivedBar.projectiveResolution k A N).complex ≅
    ((ModuleCat.restrictScalars (algebraMap k D)).mapHomologicalComplex _).obj
      (DerivedBar.tensorBarComplex k A D N f) :=
…
```
Mentions: OAI.LittleFinitistic.PDTensor.tensorFunctor, OAI.LittleFinitistic.PDBarQuotient.RightBase, OAI.DerivedBar.projectiveResolution, OAI.DerivedBar.tensorBarComplex
def OAI.LittleFinitistic.PDBarQuotient.twoSidedIso line 71
Source documentation
Comparison to the literal two-sided bar complex used in the splitting.
```
def twoSidedIso :
    ((PDTensor.tensorFunctor k A (RightBase f)).mapHomologicalComplex _).obj
      (DerivedBar.projectiveResolution k A N).complex ≅
    ((ModuleCat.restrictScalars (algebraMap k D)).mapHomologicalComplex _).obj
      (DerivedBar.twoSidedComplex k A D N f) :=
…
```
Mentions: OAI.LittleFinitistic.PDTensor.tensorFunctor, OAI.LittleFinitistic.PDBarQuotient.RightBase, OAI.DerivedBar.projectiveResolution, OAI.DerivedBar.twoSidedComplex
def OAI.LittleFinitistic.PDBarQuotient.torIsoTwoSided line 82
Source documentation
Tor computed by the literal two-sided bar, with no assumed quotient comparison.
```
def torIsoTwoSided (n : ℕ) :
    PDTensor.Tor (k := k) (RightBase f) (ModuleCat.of A N) n ≅
…
```
Mentions: OAI.LittleFinitistic.PDTensor.Tor, OAI.LittleFinitistic.PDBarQuotient.RightBase