OAI/Algebra/Finitistic/Rectification/AdjacentArrowSum.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.AdjacentArrowSum.vertexComplex line 17
2. def OAI.LittleFinitistic.AdjacentArrowSum.sourceIso line 20
3. def OAI.LittleFinitistic.AdjacentArrowSum.targetIso line 27
4. theorem OAI.LittleFinitistic.AdjacentArrowSum.desc_isIso line 36

   Source documentation

   An actual adjacent path family becomes the full arrow basis under corner coordinates.

   theorem desc_isIso (v i : Fin 3) (d : ℕ)
       (ξ : CornerSpaces.corner μ v i ≃ₗ[k] QuadraticEncoding.Arrows k d)
       (a : Fin (d+1) → ThreeVertexAlgebra μ)
       (ha : ∀ j, a j * ThreeVertexAlgebra.vertex μ i = a j)
       (hc : ∀ j c, ξ (CornerColumnPaths.cornerMap μ v i v (a j) (ha j)
         ((CornerSpaces.diagonalEquiv μ v).symm c)) = c • QuadraticEncoding.basis j) :
       IsIso (biproduct.desc (fun j => (vertexComplex μ v).map
         (ExternalTensor.Section4.path k T (ThreeVertexAlgebra.vertex μ i)
           (ThreeVertexAlgebra.vertex μ v) (a j) (ha j) D))) := by
   …

   Mentions: OAI.LittleFinitistic.CornerSpaces.corner, OAI.LittleFinitistic.QuadraticEncoding.Arrows, OAI.LittleFinitistic.ThreeVertexAlgebra, OAI.LittleFinitistic.ThreeVertexAlgebra.vertex, OAI.LittleFinitistic.CornerColumnPaths.cornerMap, OAI.LittleFinitistic.CornerSpaces.diagonalEquiv, OAI.LittleFinitistic.QuadraticEncoding.basis, OAI.LittleFinitistic.AdjacentArrowSum.vertexComplex, OAI.ExternalTensor.Section4.path