OAI/Algebra/Finitistic/Localization/TensorEvaluationComparison.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.BalancedTensor.fromScalarModule line 13
2. def OAI.LittleFinitistic.BalancedTensor.toScalarModule line 18
3. def OAI.LittleFinitistic.BalancedTensor.tensorFunctorEquiv line 24

   Source documentation

   Compare the functor's canonical scalar restriction with an existing compatible k-action.

   def tensorFunctorEquiv :
       (tensorFunctor k A N).obj (ModuleCat.of Aᵐᵒᵖ M) ≃ₗ[k] Tensor k A M N where
   …

   Mentions: OAI.LittleFinitistic.BalancedTensor.tensorFunctor, OAI.LittleFinitistic.BalancedTensor.Tensor

4. theorem OAI.LittleFinitistic.BalancedTensor.tensorFunctorEquiv_mk line 47