VertexModuleAssembly.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.VertexModuleAssembly.assembled line 17
Source documentation
Assemble specified vertex isomorphisms into a vector-space isomorphism.
```
def assembled : M ≃ₗ[k] N :=
…
```
lemma OAI.LittleFinitistic.VertexModuleAssembly.project_assembled line 20
lemma OAI.LittleFinitistic.VertexModuleAssembly.assembled_vertex line 25
theorem OAI.LittleFinitistic.VertexModuleAssembly.vertex_smul line 36
Source documentation
The assembled map commutes with every vertex idempotent.
```
theorem vertex_smul (i : Fin n) (x : M) :
    assembled D E (D.e i • x) = D.e i • assembled D E x := by
…
```
Mentions: OAI.LittleFinitistic.VertexModuleAssembly.assembled
def OAI.LittleFinitistic.VertexModuleAssembly.arrow line 43
Source documentation
A supported arrow acts between its actual source and target subspaces.
```
def arrow {i j : Fin n} (a : A) (ha : D.e j * a = a) :
    Space D M i →ₗ[k] Space D M j where
…
```
theorem OAI.LittleFinitistic.VertexModuleAssembly.arrow_smul line 53
Source documentation
Vertexwise compatibility with an actual arrow gives compatibility of the assembled map on every element of the full module.
```
theorem arrow_smul {i j : Fin n} (a : A) (hl : D.e j * a = a) (hr : a * D.e i = a)
    (hE : ∀ x : Space D M i, E j (arrow D a hl x) = arrow D a hl (E i x))
    (x : M) : assembled D E (a • x) = a • assembled D E x := by
…
```
Mentions: OAI.LittleFinitistic.VertexModuleAssembly.arrow, OAI.LittleFinitistic.VertexModuleAssembly.assembled