OAI/Algebra/Finitistic/Rectification/CornerPathTransport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.CornerPathTransport.coordinateIso line 15
2. theorem OAI.LittleFinitistic.CornerPathTransport.path_square line 24

   Source documentation

   Coordinate transport preserves each actual path map, before taking any finite sum.

   theorem path_square (v i j : Fin 3) {M N : Type u}
       [AddCommGroup M] [Module k M] [AddCommGroup N] [Module k N]
       (ξ : CornerSpaces.corner μ v j ≃ₗ[k] M)
       (η : CornerSpaces.corner μ v i ≃ₗ[k] N)
       (a : T) (ha : a * ThreeVertexAlgebra.vertex μ i = a)
       (f : M →ₗ[k] N)
       (hc : ∀ x, η (CornerColumnPaths.cornerMap μ v i j a ha x) = f (ξ x)) :
       (coordinateIso μ D v j ξ).hom ≫ (TensorComplex.tensorFunctor (k := k) D).map
   …

   Mentions: OAI.LittleFinitistic.CornerSpaces.corner, OAI.LittleFinitistic.ThreeVertexAlgebra.vertex, OAI.LittleFinitistic.CornerColumnPaths.cornerMap, OAI.LittleFinitistic.CornerPathTransport.coordinateIso, OAI.LittleFinitistic.TensorComplex.tensorFunctor