CornerArrowCoordinates.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.CornerArrowCoordinates.arrow01_coordinate line 13
Source documentation
On the adjacent 1,0 corner, the original a-arrow inserts its actual basis vector.
```
theorem arrow01_coordinate (a : Fin (d+1)) (c : k) :
    CornerSpaces.corner10Equiv (composition P)
      (cornerMap (composition P) 1 0 1 (arrow01 P a)
        ((ConcreteQuadraticDiagram.quadratic P).ha a)
        ((CornerSpaces.diagonalEquiv (composition P) 1).symm c)) = c • basis a := by
…
```
Mentions: OAI.LittleFinitistic.CornerSpaces.corner10Equiv, OAI.LittleFinitistic.ConcreteQuadraticDiagram.quadratic, OAI.LittleFinitistic.CornerSpaces.diagonalEquiv
theorem OAI.LittleFinitistic.CornerArrowCoordinates.arrow12_coordinate line 22
Source documentation
On the adjacent 2,1 corner, the original b-arrow inserts its actual basis vector.
```
theorem arrow12_coordinate (b : Fin (d+1)) (c : k) :
    CornerSpaces.corner21Equiv (composition P)
      (cornerMap (composition P) 2 1 2 (arrow12 P b)
        ((ConcreteQuadraticDiagram.quadratic P).hb b)
        ((CornerSpaces.diagonalEquiv (composition P) 2).symm c)) = c • basis b := by
…
```
Mentions: OAI.LittleFinitistic.CornerSpaces.corner21Equiv, OAI.LittleFinitistic.ConcreteQuadraticDiagram.quadratic, OAI.LittleFinitistic.CornerSpaces.diagonalEquiv

theorem OAI.LittleFinitistic.CornerArrowCoordinates.lengthTwo_coordinate line 31

Source documentation

Length-two multiplication is exactly the quotient of the original tensor path.

theorem lengthTwo_coordinate (a : Fin (d+1)) (w : Arrows k d) :
    CornerSpaces.corner20Equiv (composition P)
      (cornerMap (composition P) 2 0 1 (arrow01 P a)
        ((ConcreteQuadraticDiagram.quadratic P).ha a)
        ((CornerSpaces.corner21Equiv (composition P)).symm w)) =
      (relationSpace P).mkQ (w ⊗ₜ[k] basis a) := by
…

Mentions: OAI.LittleFinitistic.CornerSpaces.corner20Equiv, OAI.LittleFinitistic.ConcreteQuadraticDiagram.quadratic, OAI.LittleFinitistic.CornerSpaces.corner21Equiv