OAI/Algebra/Finitistic/Selected/SelectedCohomologyAssembly.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LittleFinitistic.SelectedCohomologyAssembly.transfer_square line 12
2. def OAI.LittleFinitistic.SelectedCohomologyAssembly.iso line 34

   Source documentation

   Convert an identified evaluated-representative cohomology diagram into the full cohomology B-module of the one fixed selecting tensor. Only the reference diagram identification is an input; the tensor vertex comparisons are proved.

   def iso
       (h01 : ∀ a,
         homologyMap (((BalancedTensor.tensorFunctor ℂ (B P) N).mapHomologicalComplex (.up ℤ)).map (f a)) n ≫
           (E 1).hom = (E 0).hom ≫
           (LeftVertexHomology.arrow ℂ (B P) (ThreeVertexAlgebra.vertex (composition P) 0)
             (ThreeVertexAlgebra.vertex (composition P) 1) (arrow01 P a)
             (CanonicalArrowCompatibility.arrow01_target P a)).app R)
       (h12 : ∀ b,
         homologyMap (((BalancedTensor.tensorFunctor ℂ (B P) N).mapHomologicalComplex (.up ℤ)).map (g b)) n ≫
           (E 2).hom = (E 1).hom ≫
           (LeftVertexHomology.arrow ℂ (B P) (ThreeVertexAlgebra.vertex (composition P) 1)
             (ThreeVertexAlgebra.vertex (composition P) 2) (arrow12 P b)
   …

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