OAI/Algebra/Finitistic/Rectification/VertexCategoricalAssembly.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.VertexCategoricalAssembly.scalar line 16
2. def OAI.LittleFinitistic.VertexCategoricalAssembly.vertexEquiv line 18
3. def OAI.LittleFinitistic.VertexCategoricalAssembly.iso line 27

   Source documentation

   Compatible categorical vertex isomorphisms determine a full B-module isomorphism. The hypotheses are exactly the two finite arrow squares; length-two actions follow.

   def iso
       (h01 : ∀ a,
         (LeftVertexHomology.arrow k (B P) (ThreeVertexAlgebra.vertex (composition P) 0)
           (ThreeVertexAlgebra.vertex (composition P) 1) (arrow01 P a)
           (CanonicalArrowCompatibility.arrow01_target P a)).app M ≫ (E 1).hom =
         (E 0).hom ≫ (LeftVertexHomology.arrow k (B P) (ThreeVertexAlgebra.vertex (composition P) 0)
           (ThreeVertexAlgebra.vertex (composition P) 1) (arrow01 P a)
           (CanonicalArrowCompatibility.arrow01_target P a)).app N)
       (h12 : ∀ b,
         (LeftVertexHomology.arrow k (B P) (ThreeVertexAlgebra.vertex (composition P) 1)
           (ThreeVertexAlgebra.vertex (composition P) 2) (arrow12 P b)
           (CanonicalArrowCompatibility.arrow12_target P b)).app M ≫ (E 2).hom =
   …

   Mentions: OAI.LittleFinitistic.LeftVertexHomology.arrow, OAI.LittleFinitistic.ThreeVertexAlgebra.vertex, OAI.LittleFinitistic.CanonicalArrowCompatibility.arrow01_target, OAI.LittleFinitistic.CanonicalArrowCompatibility.arrow12_target