OAI/Algebra/Finitistic/Ordinary/OrdinaryVertexCompression.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LittleFinitistic.OrdinarySimulation.Compression.insert line 13

    Source documentation

    Coordinate insertion is linear over the full coefficient algebra A.

    def insert (i : Fin (l+1)) : P.X (a+(i.val:ℤ)) →ₗ[A] Compression P a l :=
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.Compression

  2. def OAI.LittleFinitistic.OrdinarySimulation.Compression.project line 16
  3. theorem OAI.LittleFinitistic.OrdinarySimulation.Compression.vertex_action line 18
  4. def OAI.LittleFinitistic.OrdinarySimulation.Compression.vertexSpace line 24

    Source documentation

    The vertex part is a submodule over A, hence retains both B-actions when A=B tensor B-op.

    def vertexSpace (i : Fin (l+1)) : Submodule A (Compression P a l) where
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.Compression

  5. def OAI.LittleFinitistic.OrdinarySimulation.Compression.vertexInsert line 35
  6. def OAI.LittleFinitistic.OrdinarySimulation.Compression.vertexEquiv line 44

    Source documentation

    Actual A-linear identification of the compressed vertex with its original term.

    def vertexEquiv (i : Fin (l+1)) : vertexSpace (k := k) P a l i ≃ₗ[A] P.X (a+(i.val:ℤ)) where
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.Compression.vertexSpace

  7. def OAI.LittleFinitistic.OrdinarySimulation.Compression.vertexSpaceScalarEquiv line 55

    Source documentation

    Change only the scalar description of the same actual vertex subspace.

    def vertexSpaceScalarEquiv (i : Fin (l+1)) :
    IdempotentTensor.leftSpace (k := k) (ChainAlgebra.vertex k l i) (Compression P a l) ≃ₗ[k]
…

    Mentions: OAI.LittleFinitistic.IdempotentTensor.leftSpace, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.vertex, OAI.LittleFinitistic.OrdinarySimulation.Compression

  8. def OAI.LittleFinitistic.OrdinarySimulation.Compression.vertexTensorEquiv line 66

    Source documentation

    The genuine balanced tensor on a vertex projective evaluates to the original term.

    def vertexTensorEquiv (i : Fin (l+1)) :
    BalancedTensor.Tensor k (ChainAlgebra k l)
      (IdempotentTensor.rightIdeal (ChainAlgebra.vertex k l i)) (Compression P a l) ≃ₗ[k]
      (underlyingComplex (k := k) P).X (a+(i.val:ℤ)) := by
…

    Mentions: OAI.LittleFinitistic.BalancedTensor.Tensor, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.IdempotentTensor.rightIdeal, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.vertex, OAI.LittleFinitistic.OrdinarySimulation.Compression, OAI.LittleFinitistic.OrdinarySimulation.underlyingComplex