SelectedBarComparison.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.SelectedBarComparison.resolution line 15
Source documentation
The actual fixed resolution supplies every generic native/bar premise.
```
def resolution := BimoduleTotal.ofNonpositiveResolution
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.ofNonpositiveResolution
abbrev OAI.LittleFinitistic.SelectedBarComparison.native line 22
Source documentation
The native finite-interval presentation of tensor by the actual Q_X. Its comparison to the ordinary total presentation is proved separately.
```
abbrev native := resolution.data.derived
```
def OAI.LittleFinitistic.SelectedBarComparison.naturalIso line 26
Source documentation
The native tensor of the actual Q_X agrees naturally with bar-derived tensor by the ORIGINAL X, with no remaining augmentation or action premise.
```
def naturalIso : DerivedBar.chainToIntegerDerived D ⋙ native ≅
    DerivedBar.derivedTensor ℂ D X ⋙ DerivedBar.chainToIntegerDerived D :=
…
```
Mentions: OAI.DerivedBar.chainToIntegerDerived, OAI.LittleFinitistic.SelectedBarComparison.native, OAI.DerivedBar.derivedTensor
def OAI.LittleFinitistic.SelectedBarComparison.powerIso line 36
Source documentation
Every actual native iterate on a stalk is the original-X bar-derived iterate.
```
def powerIso (N : ModuleCat.{0} D) (r : ℕ) :
    (native.obj^[r]) (DerivedCategory.Q.obj (BimoduleTotal.singleInput D N)) ≅
      DerivedBar.IterateSupport.object ℂ D X N r :=
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.singleInput, OAI.DerivedBar.IterateSupport.object