OAI/Algebra/Finitistic/Ordinary/OrdinaryTensorBimoduleComparison.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LittleFinitistic.OrdinarySimulation.VertexTensor line 13
  2. instance OAI.LittleFinitistic.OrdinarySimulation.VertexTensor.(instance at line 20) line 20
  3. instance OAI.LittleFinitistic.OrdinarySimulation.VertexTensor.(instance at line 21) line 21
  4. def OAI.LittleFinitistic.OrdinarySimulation.VertexTensor.action line 23
  5. instance OAI.LittleFinitistic.OrdinarySimulation.VertexTensor.(instance at line 29) line 29
  6. instance OAI.LittleFinitistic.OrdinarySimulation.VertexTensor.(instance at line 30) line 30
  7. def OAI.LittleFinitistic.OrdinarySimulation.VertexTensor.mk line 36
  8. theorem OAI.LittleFinitistic.OrdinarySimulation.VertexTensor.action_tmul_mk line 41
  9. def OAI.LittleFinitistic.OrdinarySimulation.VertexTensor.evaluation line 51

    Source documentation

    Evaluation of the actual BC-balanced tensor.

    def evaluation : VertexTensor P a l i ≃ₗ[k] P.X (a+(i.val:ℤ)) :=
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.VertexTensor

  10. theorem OAI.LittleFinitistic.OrdinarySimulation.VertexTensor.evaluation_mk line 54
  11. theorem OAI.LittleFinitistic.OrdinarySimulation.VertexTensor.enveloping_smul line 60

    Source documentation

    The original enveloping-algebra action is the two original B-actions.

    theorem enveloping_smul (b : B) (r : Bᵐᵒᵖ) (v : BimoduleO P a l) :
    (b ⊗ₜ[k] r : Enveloping k B) • v = b • (r • v) := by
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.BimoduleO, OAI.LittleFinitistic.OrdinarySimulation.Enveloping

  12. theorem OAI.LittleFinitistic.OrdinarySimulation.VertexTensor.evaluation_tmul_smul line 67
  13. theorem OAI.LittleFinitistic.OrdinarySimulation.VertexTensor.evaluation_smul line 87
  14. def OAI.LittleFinitistic.OrdinarySimulation.VertexTensor.bimoduleEquiv line 94

    Source documentation

    Degreewise comparison as a genuine B-bimodule equivalence.

    def bimoduleEquiv : VertexTensor P a l i ≃ₗ[Enveloping k B] P.X (a+(i.val:ℤ)) where
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.VertexTensor, OAI.LittleFinitistic.OrdinarySimulation.Enveloping