OAI/Algebra/Finitistic/Bimodule/BimoduleBarTensorComparison.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LittleFinitistic.BimoduleBarComparison.Actions line 14
  2. instance OAI.LittleFinitistic.BimoduleBarComparison.outsideModule line 17
  3. instance OAI.LittleFinitistic.BimoduleBarComparison.outsideComm line 20
  4. instance OAI.LittleFinitistic.BimoduleBarComparison.outsideTower line 28
  5. abbrev OAI.LittleFinitistic.BimoduleBarComparison.BarTensor line 40
  6. def OAI.LittleFinitistic.BimoduleBarComparison.toBarLinear line 43

    Source documentation

    The field-linear balanced universal map to the bar worker's B-linear quotient.

    def toBarLinear : InputTensor k B M N →ₗ[k] BarTensor k B M N :=
…

    Mentions: OAI.LittleFinitistic.BimoduleBarComparison.BarTensor

  7. def OAI.LittleFinitistic.BimoduleBarComparison.toBar line 50

    Source documentation

    This comparison retains the actual outside B-action.

    def toBar : InputTensor k B M N →ₗ[B] BarTensor k B M N where
…

    Mentions: OAI.LittleFinitistic.BimoduleBarComparison.BarTensor

  8. def OAI.LittleFinitistic.BimoduleBarComparison.fromBarUnbalanced line 63

    Source documentation

    The reverse unbalanced tensor map is B-linear before passing to the quotient.

    def fromBarUnbalanced : Actions k B M ⊗[k] (BalancedTensor.ScalarLeftModule k B N) →ₗ[B]
    InputTensor k B M N where
…

    Mentions: OAI.LittleFinitistic.BimoduleBarComparison.Actions, OAI.LittleFinitistic.BalancedTensor.ScalarLeftModule

  9. def OAI.LittleFinitistic.BimoduleBarComparison.fromBar line 72
  10. def OAI.LittleFinitistic.BimoduleBarComparison.tensorEquiv line 82

    Source documentation

    The two independently defined balanced quotients are naturally B-linearly isomorphic.

    def tensorEquiv : InputTensor k B M N ≃ₗ[B] BarTensor k B M N where
…

    Mentions: OAI.LittleFinitistic.BimoduleBarComparison.BarTensor

  11. def OAI.LittleFinitistic.BimoduleBarComparison.tensorFunctorIso line 106

    Source documentation

    Agreement with the exact ordinary bimodule functor used by DerivedBar.

    def tensorFunctorIso : inputFunctor k B M ≅
    DerivedBar.BimoduleTensor.tensorFunctor k B (Actions k B M) :=
…

    Mentions: OAI.DerivedBar.BimoduleTensor.tensorFunctor, OAI.LittleFinitistic.BimoduleBarComparison.Actions