BimoduleTensorUnderlying.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.BimoduleBalancedTensor.underlyingEquiv line 14
Source documentation
Forgetting the actual left B action gives exactly the original balanced tensor vector space.
```
def underlyingEquiv (M : ModuleCat.{u} (Enveloping k B)) :
    (ModuleCat.restrictScalars (algebraMap k B)).obj ((functor k B N).obj M) ≃ₗ[k]
      (BalancedTensor.tensorFunctor k B N).obj ((forgetRight k B).obj M) where
…
```
Mentions: OAI.LittleFinitistic.BimoduleBalancedTensor.functor, OAI.LittleFinitistic.BalancedTensor.tensorFunctor
def OAI.LittleFinitistic.BimoduleBalancedTensor.underlyingComparison line 25
Source documentation
The comparison is natural, retaining the actual underlying maps and differentials.
```
def underlyingComparison : functor k B N ⋙ ModuleCat.restrictScalars (algebraMap k B) ≅
    forgetRight k B ⋙ BalancedTensor.tensorFunctor k B N :=
…
```
Mentions: OAI.LittleFinitistic.BimoduleBalancedTensor.functor, OAI.LittleFinitistic.BalancedTensor.tensorFunctor
instance OAI.LittleFinitistic.BimoduleBalancedTensor.finite line 35
Source documentation
Finite input vector spaces give finite balanced tensor spaces.
```
instance finite (M : ModuleCat.{u} (Enveloping k B))
    [FiniteDimensional k (Input k B M)] [FiniteDimensional k N] :
    FiniteDimensional k (Tensor k B M N) := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleBalancedTensor.Input, OAI.LittleFinitistic.BimoduleBalancedTensor.Tensor