OAI/Algebra/Finitistic/Rectification/VertexDecomposition.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.VertexDecomposition.Space line 13
2. def OAI.LittleFinitistic.VertexDecomposition.project line 16

   Source documentation

   Projection onto an actual vertex subspace.

   def project (i : Fin n) : M →ₗ[k] Space D M i where
   …

   Mentions: OAI.LittleFinitistic.VertexDecomposition.Space

3. def OAI.LittleFinitistic.VertexDecomposition.equiv line 25

   Source documentation

   A module decomposes into its actual vertex subspaces. This is a vector-space isomorphism; off-diagonal arrows act between its factors.

   def equiv : M ≃ₗ[k] ((i : Fin n) → Space D M i) where
   …

   Mentions: OAI.LittleFinitistic.VertexDecomposition.Space

4. theorem OAI.LittleFinitistic.VertexDecomposition.equiv_apply line 44
5. theorem OAI.LittleFinitistic.VertexDecomposition.equiv_symm_apply line 47
6. lemma OAI.LittleFinitistic.VertexDecomposition.project_self line 50
7. lemma OAI.LittleFinitistic.VertexDecomposition.project_other line 53