Noetherian filtered-colimit infrastructure for sheaf cohomology

Building blocks for the proof that sheaf cohomology commutes with filtered colimits on Noetherian spaces:

• creation of filtered colimits by sheafToPresheaf (createsFilteredColimit);
• flasqueness of filtered colimits of flasque sheaves (isFlasque_filtered_colimit);
• successor-stage dimension shifts and presheaf-boundary comparison maps used in the degree-n+1 colimit comparison.

theorem isSheaf_of_isColimit_of_isSheaf {X : TopCat} [TopologicalSpace.NoetherianSpace ↑X] {J' : Type u} [CategoryTheory.SmallCategory J'] [CategoryTheory.IsFiltered J'] (P : CategoryTheory.Functor J' (CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ AddCommGrpCat)) (hP : ∀ (j : J'), TopCat.Presheaf.IsSheaf (P.obj j)) (c : CategoryTheory.Limits.Cocone P) (hc : CategoryTheory.Limits.IsColimit c) : TopCat.Presheaf.IsSheaf c.pt

On a Noetherian space, a filtered colimit cocone of presheaves is a sheaf if all diagram objects are sheaves. Proof: compactness reduces the sheaf condition to finite covers, then filtered colimit merging passes from per-piece data to glued data.

@[implicit_reducible]

noncomputable def createsFilteredColimit {X : TopCat} [TopologicalSpace.NoetherianSpace ↑X] {J' : Type u} [CategoryTheory.SmallCategory J'] [CategoryTheory.IsFiltered J'] (Y' : CategoryTheory.Functor J' (TopCat.Sheaf AddCommGrpCat X)) : CategoryTheory.CreatesColimit Y' (CategoryTheory.sheafToPresheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat)

On a Noetherian space, sheafToPresheaf creates filtered colimits of sheaves by applying isSheaf_of_isColimit_of_isSheaf to the underlying presheaf diagram.

Equations

• createsFilteredColimit Y' = CategoryTheory.Sheaf.createsColimitOfIsSheaf Y' ⋯

Filtered colimits of flasque sheaves

On Noetherian spaces, sheafToPresheaf creates filtered colimits, so restrictions of filtered colimits are colimits of restrictions. Filtered colimits in AddCommGrpCat preserve surjections, hence stagewise flasque sheaves have flasque colimit.

theorem isFlasque_filtered_colimit {X : TopCat} [TopologicalSpace.NoetherianSpace ↑X] {J : Type u} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (TopCat.Sheaf AddCommGrpCat X)) (hFlasque : ∀ (j : J), IsFlasqueSheaf (F.obj j)) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) : IsFlasqueSheaf c.pt

Filtered colimits of stagewise flasque sheaves on Noetherian spaces are flasque.

Sheaf cohomology and filtered colimits

The formal comparison map sheafHFilteredColimitComparison : colim H^n(F_j) ⟶ H^n(colim F_j) is defined for any small diagram and cocone by colimit.desc.

The genuinely geometric input starts afterwards:

• sheafHPreservesFilteredColimits: the filtered-colimit comparison isomorphism for a sheaf diagram and a colimit cocone.

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

The arrow diagram used in the successor-step dimension-shift construction.

Equations

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

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

Objectwise injective envelopes coming from functorial factorization of 0 : Y_j ⟶ 0.

Equations

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

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

The natural monomorphism from the original diagram into the injective replacement.

Equations

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

theorem sheafH_filtered_colimit_succ_eta_mono {X : TopCat} {J' : Type u} [CategoryTheory.SmallCategory J'] (Y' : CategoryTheory.Functor J' (TopCat.Sheaf AddCommGrpCat X)) [Zero (TopCat.Sheaf AddCommGrpCat X)] (j : J') : CategoryTheory.Mono ((sheafHFilteredColimitSuccEta Y').app j)

noncomputable def sheafHFilteredColimitSuccInjCocone {X : TopCat} {J' : Type u} [CategoryTheory.SmallCategory J'] [CategoryTheory.IsFiltered J'] (Y' : CategoryTheory.Functor J' (TopCat.Sheaf AddCommGrpCat X)) [Zero (TopCat.Sheaf AddCommGrpCat X)] : CategoryTheory.Limits.Cocone (sheafHFilteredColimitSuccInj Y')

The colimit cocone of the injective replacement diagram.

Equations

• sheafHFilteredColimitSuccInjCocone Y' = CategoryTheory.Limits.colimit.cocone (sheafHFilteredColimitSuccInj Y')

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

The cocone obtained by composing the original cocone maps with the injective replacement.

Equations

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

noncomputable def sheafHFilteredColimitSuccIota {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') : c'.pt ⟶ (sheafHFilteredColimitSuccInjCocone Y').pt

The induced map from the colimit of the original diagram to the colimit of its injective replacement.

Equations

• sheafHFilteredColimitSuccIota Y' c' hc' = hc'.desc (sheafHFilteredColimitSuccIotaCocone Y')

theorem sheafH_filtered_colimit_succ_iota_fac {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') (j : J') : CategoryTheory.CategoryStruct.comp (c'.ι.app j) (sheafHFilteredColimitSuccIota Y' c' hc') = CategoryTheory.CategoryStruct.comp ((sheafHFilteredColimitSuccEta Y').app j) ((sheafHFilteredColimitSuccInjCocone Y').ι.app j)

instance sheafH_filtered_colimit_succ_iota_mono {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') : CategoryTheory.Mono (sheafHFilteredColimitSuccIota Y' c' hc')

noncomputable def sheafHFilteredColimitSuccShortComplex {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') : CategoryTheory.ShortComplex (TopCat.Sheaf AddCommGrpCat X)

The short exact sequence on colimit objects obtained from the injective replacement.

Equations

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

theorem sheafH_filtered_colimit_succ_shortExact {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') : (sheafHFilteredColimitSuccShortComplex Y' c' hc').ShortExact

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

The quotient diagram obtained by objectwise cokernels of the injective replacement maps.

Equations

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

noncomputable def sheafHFilteredColimitSuccQuotientCocone {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') : CategoryTheory.Limits.Cocone (sheafHFilteredColimitSuccQuotient Y')

The quotient cocone on the cokernel diagram induced by the colimit short exact sequence.

Equations

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

noncomputable def sheafHFilteredColimitSuccQuotientCoconeIsColimit {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') : CategoryTheory.Limits.IsColimit (sheafHFilteredColimitSuccQuotientCocone Y' c' hc')

The quotient cocone obtained from the stagewise injective replacements is colimiting.

Equations

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

theorem sheafH_filtered_colimit_succ_stage_shortExact {X : TopCat} {J' : Type u} [CategoryTheory.SmallCategory J'] (Y' : CategoryTheory.Functor J' (TopCat.Sheaf AddCommGrpCat X)) [Zero (TopCat.Sheaf AddCommGrpCat X)] (j : J') : { X₁ := Y'.obj j, X₂ := (sheafHFilteredColimitSuccInj Y').obj j, X₃ := CategoryTheory.Limits.cokernel ((sheafHFilteredColimitSuccEta Y').app j), f := (sheafHFilteredColimitSuccEta Y').app j, g := CategoryTheory.Limits.cokernel.π ((sheafHFilteredColimitSuccEta Y').app j), zero := ⋯ }.ShortExact

noncomputable def sheafHFilteredColimitSuccStageMapHom {X : TopCat} {J' : Type u} [CategoryTheory.SmallCategory J'] (Y' : CategoryTheory.Functor J' (TopCat.Sheaf AddCommGrpCat X)) [Zero (TopCat.Sheaf AddCommGrpCat X)] {j j' : J'} (f : j ⟶ j') : { X₁ := Y'.obj j, X₂ := (sheafHFilteredColimitSuccInj Y').obj j, X₃ := CategoryTheory.Limits.cokernel ((sheafHFilteredColimitSuccEta Y').app j), f := (sheafHFilteredColimitSuccEta Y').app j, g := CategoryTheory.Limits.cokernel.π ((sheafHFilteredColimitSuccEta Y').app j), zero := ⋯ } ⟶ { X₁ := Y'.obj j', X₂ := (sheafHFilteredColimitSuccInj Y').obj j', X₃ := CategoryTheory.Limits.cokernel ((sheafHFilteredColimitSuccEta Y').app j'), f := (sheafHFilteredColimitSuccEta Y').app j', g := CategoryTheory.Limits.cokernel.π ((sheafHFilteredColimitSuccEta Y').app j'), zero := ⋯ }

The morphism between stagewise short exact sequences induced by a transition map in the filtered diagram.

Equations

• sheafHFilteredColimitSuccStageMapHom Y' f = CategoryTheory.ShortComplex.homMk (Y'.map f) ((sheafHFilteredColimitSuccInj Y').map f) ((sheafHFilteredColimitSuccQuotient Y').map f) ⋯ ⋯

noncomputable def sheafHFilteredColimitSuccStageHom {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') (j : J') : { X₁ := Y'.obj j, X₂ := (sheafHFilteredColimitSuccInj Y').obj j, X₃ := CategoryTheory.Limits.cokernel ((sheafHFilteredColimitSuccEta Y').app j), f := (sheafHFilteredColimitSuccEta Y').app j, g := CategoryTheory.Limits.cokernel.π ((sheafHFilteredColimitSuccEta Y').app j), zero := ⋯ } ⟶ sheafHFilteredColimitSuccShortComplex Y' c' hc'

The morphism from the stagewise short exact sequence to the colimit short exact sequence.

Equations

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

noncomputable def sheafHFilteredColimitSuccShiftNatIso {X : TopCat} {J' : Type u} [CategoryTheory.SmallCategory J'] (Y' : CategoryTheory.Functor J' (TopCat.Sheaf AddCommGrpCat X)) [Zero (TopCat.Sheaf AddCommGrpCat X)] (n : ℕ) (h_mid_n : ∀ (j : J'), Subsingleton (CategoryTheory.Sheaf.H ((sheafHFilteredColimitSuccInj Y').obj j) n)) (h_mid_succ : ∀ (j : J'), Subsingleton (CategoryTheory.Sheaf.H ((sheafHFilteredColimitSuccInj Y').obj j) (n + 1))) : (sheafHFilteredColimitSuccQuotient Y').comp (sheafCohomologyFunctor X n) ≅ Y'.comp (sheafCohomologyFunctor X (n + 1))

The stagewise dimension-shift natural isomorphism between the quotient diagram in degree n and the original diagram in degree n + 1.

Equations

• sheafHFilteredColimitSuccShiftNatIso Y' n h_mid_n h_mid_succ = CategoryTheory.NatIso.ofComponents (fun (j : J') => sheafHSuccIsoOfSubsingletonMiddle ⋯ n ⋯ ⋯) ⋯

noncomputable def sheafHFilteredColimitSuccShiftDomainIso {X : TopCat} {J' : Type u} [CategoryTheory.SmallCategory J'] (Y' : CategoryTheory.Functor J' (TopCat.Sheaf AddCommGrpCat X)) [Zero (TopCat.Sheaf AddCommGrpCat X)] (n : ℕ) (h_mid_n : ∀ (j : J'), Subsingleton (CategoryTheory.Sheaf.H ((sheafHFilteredColimitSuccInj Y').obj j) n)) (h_mid_succ : ∀ (j : J'), Subsingleton (CategoryTheory.Sheaf.H ((sheafHFilteredColimitSuccInj Y').obj j) (n + 1))) : CategoryTheory.Limits.colimit ((sheafHFilteredColimitSuccQuotient Y').comp (sheafCohomologyFunctor X n)) ≅ CategoryTheory.Limits.colimit (Y'.comp (sheafCohomologyFunctor X (n + 1)))

The induced colimit isomorphism from the successor-step stagewise dimension shift.

Equations

• sheafHFilteredColimitSuccShiftDomainIso Y' n h_mid_n h_mid_succ = CategoryTheory.Limits.HasColimit.isoOfNatIso (sheafHFilteredColimitSuccShiftNatIso Y' n h_mid_n h_mid_succ)

noncomputable def sheafHFilteredColimitSuccShiftCodomainIso {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') (n : ℕ) (h_colim_n : Subsingleton (CategoryTheory.Sheaf.H (sheafHFilteredColimitSuccInjCocone Y').pt n)) (h_colim_succ : Subsingleton (CategoryTheory.Sheaf.H (sheafHFilteredColimitSuccInjCocone Y').pt (n + 1))) : AddCommGrpCat.of (CategoryTheory.Sheaf.H (sheafHFilteredColimitSuccQuotientCocone Y' c' hc').pt n) ≅ AddCommGrpCat.of (CategoryTheory.Sheaf.H c'.pt (n + 1))

The colimit-level dimension-shift isomorphism for the short exact sequence obtained from the injective replacement of the filtered colimit cocone.

Equations

• sheafHFilteredColimitSuccShiftCodomainIso Y' c' hc' n h_colim_n h_colim_succ = sheafHSuccIsoOfSubsingletonMiddle ⋯ n h_colim_n h_colim_succ

theorem sheafH_filtered_colimit_succ_inj_subsingleton {X : TopCat} {J' : Type u} [CategoryTheory.SmallCategory J'] [CategoryTheory.IsFiltered J'] (Y' : CategoryTheory.Functor J' (TopCat.Sheaf AddCommGrpCat X)) [Zero (TopCat.Sheaf AddCommGrpCat X)] [TopologicalSpace.NoetherianSpace ↑X] (n : ℕ) (hInj : ∀ (j : J'), CategoryTheory.Injective ((sheafHFilteredColimitSuccInj Y').obj j)) : Subsingleton (CategoryTheory.Sheaf.H (sheafHFilteredColimitSuccInjCocone Y').pt (n + 1))

The filtered-colimit successor-step vanishing lemma for the injective replacement: the middle term of the induced short exact sequence has trivial cohomology in degree n + 1.

noncomputable def sheafHFilteredColimitComparison {X : TopCat} {J' : Type u} [CategoryTheory.SmallCategory J'] (Y' : CategoryTheory.Functor J' (TopCat.Sheaf AddCommGrpCat X)) (n : ℕ) (c' : CategoryTheory.Limits.Cocone Y') : CategoryTheory.Limits.colimit (Y'.comp (sheafCohomologyFunctor X n)) ⟶ AddCommGrpCat.of (CategoryTheory.Sheaf.H c'.pt n)

The canonical comparison morphism colim H^n(F_j) ⟶ H^n(colim F_j) induced by a cocone.

Equations

• sheafHFilteredColimitComparison Y' n c' = CategoryTheory.Limits.colimit.desc (Y'.comp (sheafCohomologyFunctor X n)) ((sheafCohomologyFunctor X n).mapCocone c')

@[simp]

theorem colimit_ι_sheafH_filtered_colimit_comparison {X : TopCat} {J' : Type u} [CategoryTheory.SmallCategory J'] (Y' : CategoryTheory.Functor J' (TopCat.Sheaf AddCommGrpCat X)) (n : ℕ) (c' : CategoryTheory.Limits.Cocone Y') (j : J') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (Y'.comp (sheafCohomologyFunctor X n)) j) (sheafHFilteredColimitComparison Y' n c') = (sheafCohomologyFunctor X n).map (c'.ι.app j)

theorem sheafH_filtered_colimit_comparison_succ_compatibility {X : TopCat} {J' : Type u} [CategoryTheory.SmallCategory J'] [CategoryTheory.IsFiltered J'] [Zero (TopCat.Sheaf AddCommGrpCat X)] (Ysh : CategoryTheory.Functor J' (TopCat.Sheaf AddCommGrpCat X)) (csh : CategoryTheory.Limits.Cocone Ysh) (hcsh : CategoryTheory.Limits.IsColimit csh) (n : ℕ) (h_mid_n : ∀ (j : J'), Subsingleton (CategoryTheory.Sheaf.H ((sheafHFilteredColimitSuccInj Ysh).obj j) n)) (h_mid_succ : ∀ (j : J'), Subsingleton (CategoryTheory.Sheaf.H ((sheafHFilteredColimitSuccInj Ysh).obj j) (n + 1))) (h_colim_n : Subsingleton (CategoryTheory.Sheaf.H (sheafHFilteredColimitSuccInjCocone Ysh).pt n)) (h_colim_succ : Subsingleton (CategoryTheory.Sheaf.H (sheafHFilteredColimitSuccInjCocone Ysh).pt (n + 1))) : CategoryTheory.CategoryStruct.comp (sheafHFilteredColimitSuccShiftDomainIso Ysh n h_mid_n h_mid_succ).hom (sheafHFilteredColimitComparison Ysh (n + 1) csh) = CategoryTheory.CategoryStruct.comp (sheafHFilteredColimitComparison (sheafHFilteredColimitSuccQuotient Ysh) n (sheafHFilteredColimitSuccQuotientCocone Ysh csh hcsh)) (sheafHFilteredColimitSuccShiftCodomainIso Ysh csh hcsh n h_colim_n h_colim_succ).hom

Successor-step compatibility for the filtered-colimit comparison map: whenever the associated sheaf diagram and its colimit have vanishing injective-replacement cohomology in degrees n and n + 1, the degree-n + 1 comparison is conjugate to the degree-n comparison for the quotient diagram.