OAI/Algebra/Finitistic/Rectification/CornerProjection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LittleFinitistic.CornerProjection.videm line 15
  2. theorem OAI.LittleFinitistic.CornerProjection.corner_left_fixed line 18
  3. theorem OAI.LittleFinitistic.CornerProjection.corner_right_fixed line 26
  4. theorem OAI.LittleFinitistic.CornerProjection.ideal_right_fixed line 34
  5. def OAI.LittleFinitistic.CornerProjection.projection line 42

    Source documentation

    Left multiplication by e_i on the actual induced-column first factor B e_j.

    def projection (i j : Fin 3) :
    ExternalTensor.leftIdeal (ThreeVertexAlgebra μ) (vertex μ j) →ₗ[k]
    ExternalTensor.leftIdeal (ThreeVertexAlgebra μ) (vertex μ j) where
…

    Mentions: OAI.ExternalTensor.leftIdeal, OAI.LittleFinitistic.ThreeVertexAlgebra

  6. theorem OAI.LittleFinitistic.CornerProjection.projection_apply line 51
  7. theorem OAI.LittleFinitistic.CornerProjection.projection_idempotent line 54
  8. def OAI.LittleFinitistic.CornerProjection.rangeEquiv line 63

    Source documentation

    The image of the actual column projector is the concrete two-sided path corner.

    def rangeEquiv (i j : Fin 3) : (projection μ i j).range ≃ₗ[k] corner μ i j where
…

    Mentions: OAI.LittleFinitistic.CornerProjection.projection