Degree-one and higher filtered-colimit comparisons #
The degree-1 and higher comparison arguments showing that sheaf cohomology commutes
with filtered colimits on Noetherian spaces, building on the presheaf-boundary and
successor-stage infrastructure in PresheafFilteredColimitCore.
@[simp]
theorem
sheafH_filtered_colimit_comparison_one_iso_hom
{X : TopCat}
[TopologicalSpace.NoetherianSpace ↑X]
{J' : Type u}
[CategoryTheory.SmallCategory J']
[CategoryTheory.IsFiltered J']
(Ysh : CategoryTheory.Functor J' (TopCat.Sheaf AddCommGrpCat X))
(csh : CategoryTheory.Limits.Cocone Ysh)
(hcsh : CategoryTheory.Limits.IsColimit csh)
:
(sheafH_filtered_colimit_comparison_one_iso✝ Ysh csh hcsh).hom = sheafHFilteredColimitComparison Ysh 1 csh
@[simp]
theorem
sheafH_filtered_colimit_comparison_zero_iso_hom
{X : TopCat}
[TopologicalSpace.NoetherianSpace ↑X]
{J' : Type u}
[CategoryTheory.SmallCategory J']
[CategoryTheory.IsFiltered J']
(Ysh : CategoryTheory.Functor J' (TopCat.Sheaf AddCommGrpCat X))
(csh : CategoryTheory.Limits.Cocone Ysh)
(hcsh : CategoryTheory.Limits.IsColimit csh)
:
(sheafH_filtered_colimit_comparison_zero_iso✝ Ysh csh hcsh).hom = sheafHFilteredColimitComparison Ysh 0 csh
noncomputable def
sheafHPreservesFilteredColimits
{X : TopCat}
[TopologicalSpace.NoetherianSpace ↑X]
{J' : Type u}
[CategoryTheory.SmallCategory J']
[CategoryTheory.IsFiltered J']
(Y' : CategoryTheory.Functor J' (TopCat.Sheaf AddCommGrpCat X))
(c' : CategoryTheory.Limits.Cocone Y')
(hc' : CategoryTheory.Limits.IsColimit c')
(n : ℕ)
:
CategoryTheory.Limits.colimit (Y'.comp (sheafCohomologyFunctor X n)) ≅ AddCommGrpCat.of (CategoryTheory.Sheaf.H c'.pt n)
Sheaf cohomology commutes with filtered colimits on Noetherian spaces:
the canonical comparison colim H^n(F_j) ≅ H^n(colim F_j) is an isomorphism.
Equations
- sheafHPreservesFilteredColimits Y' c' hc' n = CategoryTheory.asIso (sheafHFilteredColimitComparison Y' n c')