RelationBasisAction.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.RelationBasisAction.arrow line 14
Source documentation
The distinguished arrow acts by one, followed by the original generators.
```
def arrow : Fin (d+1) → R := Fin.cases 1 x
```
def OAI.LittleFinitistic.RelationBasisAction.pathValue line 17
Source documentation
Evaluate a length-two path b a in the original algebra.
```
def pathValue : Paths k d →ₗ[k] R :=
…
```
theorem OAI.LittleFinitistic.RelationBasisAction.pathValue_basis line 20
theorem OAI.LittleFinitistic.RelationBasisAction.relationSpace_le_kernel line 32
Source documentation
The entire relation space vanishes, including every chosen independent basis vector.
```
theorem relationSpace_le_kernel : relationSpace P ≤ (pathValue x).ker := by
…
```
Mentions: OAI.LittleFinitistic.RelationBasisAction.pathValue
theorem OAI.LittleFinitistic.RelationBasisAction.basis_action_relation line 43
Source documentation
Exact homogeneous coefficient equations for the fixed-diagram lifting theorem.
```
theorem basis_action_relation (r : RelationIndex P) :
    (∑ a, ∑ b, basisCoefficient P r a b • (arrow x b * arrow x a)) = 0 := by
…
```
Mentions: OAI.LittleFinitistic.RelationBasisAction.arrow
theorem OAI.LittleFinitistic.RelationBasisAction.encoding_basis_action line 51
Source documentation
The concrete selected algebra satisfies all equations of the independent relation basis.
```
theorem encoding_basis_action (E : SelectionEncoding.Encoding k R) (r : RelationIndex E.relations) :
    (∑ a, ∑ b, basisCoefficient E.relations r a b •
      (arrow (SelectionEncoding.generator E) b * arrow (SelectionEncoding.generator E) a)) = 0 :=
…
```
Mentions: OAI.LittleFinitistic.SelectionEncoding.Encoding, OAI.LittleFinitistic.RelationBasisAction.arrow, OAI.LittleFinitistic.SelectionEncoding.generator