OAI/Algebra/Finitistic/Rectification/VertexHomology.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.VertexHomology.preservesHomology line 18

   Source documentation

   Actual vertex projection preserves homology, because it preserves the short exact sequences already proved in VertexFunctor.

   theorem preservesHomology : (VertexFunctor.functor β e hc).PreservesHomology :=
   …

   Mentions: OAI.LittleFinitistic.VertexFunctor.functor

2. def OAI.LittleFinitistic.VertexHomology.iso line 23

   Source documentation

   Homology of the actual vertex complex is the actual vertex of module homology.

   def iso (X : CochainComplex (ModuleCat.{u} A) ℤ) (n : ℤ) :
       (((VertexFunctor.functor β e hc).mapHomologicalComplex (.up ℤ)).obj X).homology n ≅
         (VertexFunctor.functor β e hc).obj (X.homology n) := by
   …

   Mentions: OAI.LittleFinitistic.VertexFunctor.functor

3. theorem OAI.LittleFinitistic.VertexHomology.natural line 31

   Source documentation

   This comparison respects every natural transformation of the vertex functors, so it retains the algebra arrow actions as well as the vertex vector spaces.

   theorem natural (e' : A) (he' : e'*e'=e') (hc' : ∀ b, e'*β b=β b*e')
       (τ : VertexFunctor.functor β e hc ⟶ VertexFunctor.functor β e' hc')
       (X : CochainComplex (ModuleCat.{u} A) ℤ) (n : ℤ) :
       homologyMap ((NatTrans.mapHomologicalComplex τ (.up ℤ)).app X) n ≫
         (iso β e' he' hc' X n).hom =
       (iso β e he hc X n).hom ≫ τ.app (X.homology n) := by
   …

   Mentions: OAI.LittleFinitistic.VertexFunctor.functor, OAI.LittleFinitistic.VertexHomology.iso