Homology and the forgetful functor from FGModuleCat #
This file records the comparison between taking homology in FGModuleCat and taking homology
after forgetting to ModuleCat. It lets invariants of homology objects, such as finrank, be
transported between the two categories for Euler-characteristic computations.
noncomputable def
HomologicalComplex.homologyForgetIso
{k : Type u}
[DivisionRing k]
(K : CochainComplex (FGModuleCat k) ℤ)
(n : ℤ)
:
(((CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k)).mapHomologicalComplex (ComplexShape.up ℤ)).obj K).homology n ≅ (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k)).obj (homology K n)
The comparison between homology after forgetting an FGModuleCat cochain complex and the
underlying module of its homology.
Equations
- One or more equations did not get rendered due to their size.