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.

@[implicit_reducible]

noncomputable def sheafHFilteredColimitH1SectionsFunctor {X : TopCat} : CategoryTheory.Functor (TopCat.Sheaf AddCommGrpCat X) AddCommGrpCat

The global-sections functor used in the degree-1 filtered-colimit boundary construction.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def sheafHFilteredColimitH1GTopNat {X : TopCat} {J' : Type u} [CategoryTheory.SmallCategory J'] (Y' : CategoryTheory.Functor J' (TopCat.Sheaf AddCommGrpCat X)) [Zero (TopCat.Sheaf AddCommGrpCat X)] : (sheafHFilteredColimitSuccInj Y').comp sheafHFilteredColimitH1SectionsFunctor ⟶ (sheafHFilteredColimitSuccQuotient Y').comp sheafHFilteredColimitH1SectionsFunctor

The stagewise top-sections map from the injective replacement to its quotient in the degree-1 filtered-colimit comparison.

Equations

• sheafHFilteredColimitH1GTopNat Y' = { app := fun (j : J') => (CategoryTheory.Limits.cokernel.π ((sheafHFilteredColimitSuccEta Y').app j)).hom.app (Opposite.op ⊤), naturality := ⋯ }

noncomputable def sheafHFilteredColimitH1CokernelFunctor {X : TopCat} {J' : Type u} [CategoryTheory.SmallCategory J'] (Y' : CategoryTheory.Functor J' (TopCat.Sheaf AddCommGrpCat X)) [Zero (TopCat.Sheaf AddCommGrpCat X)] : CategoryTheory.Functor J' AddCommGrpCat

The functor of stagewise cokernels of the top-sections maps used in the degree-1 filtered-colimit boundary construction.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def sheafHFilteredColimitH1CokernelFunctorIso {X : TopCat} {J' : Type u} [CategoryTheory.SmallCategory J'] (Y' : CategoryTheory.Functor J' (TopCat.Sheaf AddCommGrpCat X)) [Zero (TopCat.Sheaf AddCommGrpCat X)] : sheafHFilteredColimitH1CokernelFunctor Y' ≅ CategoryTheory.Limits.cokernel (sheafHFilteredColimitH1GTopNat Y')

Evaluation at each diagram object identifies the stagewise cokernel functor with the cokernel of sheafHFilteredColimitH1GTopNat.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def sheafHFilteredColimitH1StageNatIso {X : TopCat} {J' : Type u} [CategoryTheory.SmallCategory J'] (Y' : CategoryTheory.Functor J' (TopCat.Sheaf AddCommGrpCat X)) [Zero (TopCat.Sheaf AddCommGrpCat X)] (h_mid : ∀ (j : J'), Subsingleton (CategoryTheory.Sheaf.H ((sheafHFilteredColimitSuccInj Y').obj j) 1)) : sheafHFilteredColimitH1CokernelFunctor Y' ≅ Y'.comp (sheafCohomologyFunctor X 1)

The stagewise identification of H¹ with the cokernel of top sections for the injective-replacement short exact sequence used in the filtered-colimit comparison.

Equations

• sheafHFilteredColimitH1StageNatIso Y' h_mid = CategoryTheory.NatIso.ofComponents (fun (j : J') => id (sheafH1CokernelIsoOfSubsingletonMiddle ⋯ ⋯)) ⋯

noncomputable def sheafHFilteredColimitH1GlobalCokernelIso {X : TopCat} {J' : Type u} [CategoryTheory.SmallCategory J'] [CategoryTheory.IsFiltered J'] (Y' : CategoryTheory.Functor J' (TopCat.Sheaf AddCommGrpCat X)) [Zero (TopCat.Sheaf AddCommGrpCat X)] (c' : CategoryTheory.Limits.Cocone Y') (hc' : CategoryTheory.Limits.IsColimit c') (h_colim : Subsingleton (CategoryTheory.Sheaf.H (sheafHFilteredColimitSuccInjCocone Y').pt 1)) : CategoryTheory.Limits.cokernel (sheafHFilteredColimitH1SectionsFunctor.map (CategoryTheory.Limits.cokernel.π (sheafHFilteredColimitSuccIota Y' c' hc'))) ≅ (sheafCohomologyFunctor X 1).obj c'.pt

Identify the global section cokernel with first cohomology of the colimit.

Equations

• sheafHFilteredColimitH1GlobalCokernelIso Y' c' hc' h_colim = id (id (sheafH1CokernelIsoOfSubsingletonMiddle ⋯ h_colim))

noncomputable def sheafHFilteredColimitComparisonOneIso {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) : CategoryTheory.Limits.colimit (Ysh.comp (sheafCohomologyFunctor X 1)) ≅ (sheafCohomologyFunctor X 1).obj csh.pt

The degree-1 filtered-colimit comparison isomorphism, obtained by identifying H¹ with the cokernel of top sections for the injective-replacement short exact sequence.

Equations

• One or more equations did not get rendered due to their size.

@[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) : (sheafHFilteredColimitComparisonOneIso Ysh csh hcsh).hom = sheafHFilteredColimitComparison Ysh 1 csh

noncomputable def sheafHFilteredColimitZeroSectionsIso {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) : CategoryTheory.Limits.colimit (Ysh.comp (sheafCohomologyFunctor X 0)) ≅ sheafHFilteredColimitH1SectionsFunctor.obj csh.pt

The degree-0 comparison up to identifying H⁰ with global sections.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def sheafHFilteredColimitComparisonZeroIso {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) : CategoryTheory.Limits.colimit (Ysh.comp (sheafCohomologyFunctor X 0)) ≅ (sheafCohomologyFunctor X 0).obj csh.pt

The degree-0 filtered-colimit comparison isomorphism, obtained from global sections.

Equations

• sheafHFilteredColimitComparisonZeroIso Ysh csh hcsh = sheafHFilteredColimitZeroSectionsIso Ysh csh hcsh ≪≫ (sheafH0EquivSections csh.pt).toAddCommGrpIso.symm

@[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) : (sheafHFilteredColimitComparisonZeroIso 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)) ≅ (sheafCohomologyFunctor X n).obj c'.pt

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')