NativeBoundedDerived.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.BimoduleTotal.inducedBoundedProjective line 13
Source documentation
Build the complete derived-tensor model from the actual native rectification, with no tensor-comparison assumption.
```
def inducedBoundedProjective
    {A J R : Type} [Fintype A] [Fintype J] [Fintype R]
    (s : Quadratic k B (A := A) (J := J) (R := R))
…
```
def OAI.LittleFinitistic.BimoduleTotal.BoundedProjective.nativeEvaluation line 36
Source documentation
The exact native module-valued degree-zero evaluation, using the module's original compatible k action.
```
def nativeEvaluation (N : Type u) [AddCommGroup N] [Module k N] [Module B N] [IsScalarTower k B N] :
    data.derived.obj (DerivedCategory.Q.obj (singleInput B (ModuleCat.of B N))) ≅
      DerivedCategory.Q.obj (((BimoduleBalancedTensor.functor k B N).mapHomologicalComplex (.up ℤ)).obj P) :=
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.singleInput, OAI.LittleFinitistic.BimoduleBalancedTensor.functor