OAI/Algebra/Finitistic/Bimodule/BimoduleVertex.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.BimoduleVertex.restriction line 15
2. abbrev OAI.LittleFinitistic.BimoduleVertex.vertex line 17
3. theorem OAI.LittleFinitistic.BimoduleVertex.vertex_idempotent line 19
4. theorem OAI.LittleFinitistic.BimoduleVertex.vertex_commute line 23
5. abbrev OAI.LittleFinitistic.BimoduleVertex.functor line 28

   Source documentation

   The original left vertex action, with the right B-module structure retained.

   abbrev functor (e : B) : ModuleCat.{u} (B ⊗[k] Bᵐᵒᵖ) ⥤ ModuleCat.{u} Bᵐᵒᵖ :=
   …

6. theorem OAI.LittleFinitistic.BimoduleVertex.map_shortExact line 31
7. abbrev OAI.LittleFinitistic.BimoduleVertex.columnObj line 47
8. abbrev OAI.LittleFinitistic.BimoduleVertex.columnFixed line 49
9. def OAI.LittleFinitistic.BimoduleVertex.columnFixedEquiv line 54

   Source documentation

   Identifies the original enveloping vertex action with its corner projector.

   def columnFixedEquiv (i j : Fin 3) :
       columnFixed μ N i j ≃ₗ[Tᵐᵒᵖ]
       TensorProjection.fixed (B := T) (N := N) (CornerProjection.projection μ i j) := by
   …

   Mentions: OAI.LittleFinitistic.BimoduleVertex.columnFixed, OAI.LittleFinitistic.TensorProjection.fixed, OAI.LittleFinitistic.CornerProjection.projection

10. def OAI.LittleFinitistic.BimoduleVertex.diagonalEquiv line 80

    Source documentation

    A column's own vertex is its original right module, with no replacement action.

    def diagonalEquiv (i : Fin 3) :
        (functor k T (ThreeVertexAlgebra.vertex μ i)).obj
          ((ExternalTensor.Section4.columnFunctor k T
            (ThreeVertexAlgebra.vertex μ i)).obj N) ≃ₗ[Tᵐᵒᵖ] N :=
    …

    Mentions: OAI.LittleFinitistic.BimoduleVertex.functor, OAI.LittleFinitistic.ThreeVertexAlgebra.vertex, OAI.ExternalTensor.Section4.columnFunctor