LeftVertexHomology.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.LittleFinitistic.LeftVertexHomology.scalar_commute line 11
abbrev OAI.LittleFinitistic.LeftVertexHomology.vertex line 15
Source documentation
The actual left vertex functor from B-modules to k-vector spaces.
```
abbrev vertex (e : B) : ModuleCat.{u} B ⥤ ModuleCat.{u} k :=
…
```
def OAI.LittleFinitistic.LeftVertexHomology.arrow line 19
Source documentation
Arrow action is a natural transformation between the actual vertex functors.
```
def arrow (ei ej a : B) (ha : ej*a=a) : vertex k B ei ⟶ vertex k B ej where
…
```
Mentions: OAI.LittleFinitistic.LeftVertexHomology.vertex
instance OAI.LittleFinitistic.LeftVertexHomology.scalarTower line 37
def OAI.LittleFinitistic.LeftVertexHomology.spaceEquiv line 42
Source documentation
Identify the vertex functor with the actual fixed subspace of scalar restriction.
```
def spaceEquiv (e : B) (M : ModuleCat.{u} B) :
    (vertex k B e).obj M ≃ₗ[k]
      IdempotentTensor.leftSpace (k := k) e ((ModuleCat.restrictScalars (algebraMap k B)).obj M) where
…
```
Mentions: OAI.LittleFinitistic.LeftVertexHomology.vertex, OAI.LittleFinitistic.IdempotentTensor.leftSpace
def OAI.LittleFinitistic.LeftVertexHomology.homologyEquiv line 53
Source documentation
Actual vertex homology, identified with the actual subspace of module homology.
```
def homologyEquiv (e : B) (he : e*e=e)
    (X : CochainComplex (ModuleCat.{u} B) ℤ) (n : ℤ) :
    (((vertex k B e).mapHomologicalComplex (.up ℤ)).obj X).homology n ≃ₗ[k]
      IdempotentTensor.leftSpace (k := k) e
…
```
Mentions: OAI.LittleFinitistic.LeftVertexHomology.vertex, OAI.LittleFinitistic.IdempotentTensor.leftSpace

theorem OAI.LittleFinitistic.LeftVertexHomology.arrow_homology line 62

Source documentation

Cohomology comparison retains the original arrow action, not only dimensions.

theorem arrow_homology (ei ej a : B) (hi : ei*ei=ei) (hj : ej*ej=ej) (ha : ej*a=a)
    (X : CochainComplex (ModuleCat.{u} B) ℤ) (n : ℤ) :
    homologyMap ((NatTrans.mapHomologicalComplex (arrow k B ei ej a ha) (.up ℤ)).app X) n ≫
      (VertexHomology.iso (algebraMap k B) ej hj (scalar_commute k B ej) X n).hom =
    (VertexHomology.iso (algebraMap k B) ei hi (scalar_commute k B ei) X n).hom ≫
      (arrow k B ei ej a ha).app (X.homology n) :=
…

Mentions: OAI.LittleFinitistic.LeftVertexHomology.arrow, OAI.LittleFinitistic.VertexHomology.iso, OAI.LittleFinitistic.LeftVertexHomology.scalar_commute