General filtered-colimit infrastructure for presheaves

Presheaf-level filtered-colimit helpers that do not require Noetherian hypotheses: finite-cover separation, eventual vanishing, compatible representative extraction, and finite-subcover gluing in cocone points.

theorem transition_preserves_zero {X : TopCat} {J' : Type u} [CategoryTheory.SmallCategory J'] [CategoryTheory.IsFiltered J'] (Y' : CategoryTheory.Functor J' (CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ AddCommGrpCat)) {j₀ j j' : J'} (f : j₀ ⟶ j) (g : j ⟶ j') {U V : TopologicalSpace.Opens ↑X} (φ : U ⟶ V) (b₀ : CategoryTheory.ToType ((Y'.obj j₀).obj (Opposite.op V))) (h : (CategoryTheory.ConcreteCategory.hom ((Y'.obj j).map φ.op)) ((CategoryTheory.ConcreteCategory.hom ((Y'.map f).app (Opposite.op V))) b₀) = 0) : (CategoryTheory.ConcreteCategory.hom ((Y'.obj j').map φ.op)) ((CategoryTheory.ConcreteCategory.hom ((Y'.map (CategoryTheory.CategoryStruct.comp f g)).app (Opposite.op V))) b₀) = 0

Zero is preserved under filtered transitions: if restricting a transition to an open gives 0, then restricting any further transition also gives 0.

theorem transition_preserves_compat {X : TopCat} {J' : Type u} [CategoryTheory.SmallCategory J'] [CategoryTheory.IsFiltered J'] (Y' : CategoryTheory.Functor J' (CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ AddCommGrpCat)) {j₀ j j' : J'} (f : j₀ ⟶ j) (g : j ⟶ j') {U V : TopologicalSpace.Opens ↑X} (a : CategoryTheory.ToType ((Y'.obj j₀).obj (Opposite.op U))) (b : CategoryTheory.ToType ((Y'.obj j₀).obj (Opposite.op V))) (h : (CategoryTheory.ConcreteCategory.hom ((Y'.obj j).map (U.infLELeft V).op)) ((CategoryTheory.ConcreteCategory.hom ((Y'.map f).app (Opposite.op U))) a) = (CategoryTheory.ConcreteCategory.hom ((Y'.obj j).map (U.infLERight V).op)) ((CategoryTheory.ConcreteCategory.hom ((Y'.map f).app (Opposite.op V))) b)) : (CategoryTheory.ConcreteCategory.hom ((Y'.obj j').map (U.infLELeft V).op)) ((CategoryTheory.ConcreteCategory.hom ((Y'.map (CategoryTheory.CategoryStruct.comp f g)).app (Opposite.op U))) a) = (CategoryTheory.ConcreteCategory.hom ((Y'.obj j').map (U.infLERight V).op)) ((CategoryTheory.ConcreteCategory.hom ((Y'.map (CategoryTheory.CategoryStruct.comp f g)).app (Opposite.op V))) b)

Pairwise compatibility is preserved under filtered transitions.

theorem sheaf_section_zero_of_zero_on_cover {X : TopCat} {F : CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ AddCommGrpCat} (hF : TopCat.Presheaf.IsSheaf F) {ι : Type u} {V : TopologicalSpace.Opens ↑X} {W : ι → TopologicalSpace.Opens ↑X} (hW : ∀ (k : ι), W k ≤ V) {t : Finset ι} (hcov : V ≤ ⨆ k ∈ t, W k) (b : CategoryTheory.ToType (F.obj (Opposite.op V))) (hzero : ∀ k ∈ t, (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) b = 0) : b = 0

A section of a sheaf that restricts to 0 on a finite open cover is 0.

theorem filtered_colimit_kills_all_restrictions {J' : Type u} [CategoryTheory.SmallCategory J'] [CategoryTheory.IsFiltered J'] {X : TopCat} (Y' : CategoryTheory.Functor J' (CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ AddCommGrpCat)) {ι : Type u} {V : TopologicalSpace.Opens ↑X} {W : ι → TopologicalSpace.Opens ↑X} (hW : ∀ (k : ι), W k ≤ V) (j₀ : J') (b₀ : CategoryTheory.ToType ((Y'.obj j₀).obj (Opposite.op V))) (t : Finset ι) (h_ev : ∀ k ∈ t, ∃ (jk : J') (fk : j₀ ⟶ jk), (CategoryTheory.ConcreteCategory.hom ((Y'.obj jk).map (CategoryTheory.homOfLE ⋯).op)) ((CategoryTheory.ConcreteCategory.hom ((Y'.map fk).app (Opposite.op V))) b₀) = 0) : ∃ (j₁ : J') (g₀ : j₀ ⟶ j₁), ∀ k ∈ t, (CategoryTheory.ConcreteCategory.hom ((Y'.obj j₁).map (CategoryTheory.homOfLE ⋯).op)) ((CategoryTheory.ConcreteCategory.hom ((Y'.map g₀).app (Opposite.op V))) b₀) = 0

Merge finitely many eventually-zero restrictions into a common index.

theorem filtered_colimit_restriction_eventually_zero_of_zero {X : TopCat} {J' : Type u} [CategoryTheory.SmallCategory J'] [CategoryTheory.IsFiltered J'] (Y' : CategoryTheory.Functor J' (CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ AddCommGrpCat)) {c : CategoryTheory.Limits.Cocone Y'} (hc : CategoryTheory.Limits.IsColimit c) {U V : TopologicalSpace.Opens ↑X} (φ : U ⟶ V) (a : CategoryTheory.ToType (c.pt.obj (Opposite.op V))) {j₀ : J'} (b₀ : CategoryTheory.ToType ((Y'.obj j₀).obj (Opposite.op V))) (hb₀ : (CategoryTheory.ConcreteCategory.hom ((c.ι.app j₀).app (Opposite.op V))) b₀ = a) (ha : (CategoryTheory.ConcreteCategory.hom (c.pt.map φ.op)) a = 0) : ∃ (j' : J') (f : j₀ ⟶ j'), (CategoryTheory.ConcreteCategory.hom ((Y'.obj j').map φ.op)) ((CategoryTheory.ConcreteCategory.hom ((Y'.map f).app (Opposite.op V))) b₀) = 0

If a representative of a colimit section restricts to zero in the cocone point, then after some filtered transition its restriction is already zero.

theorem colimit_section_zero_of_zero_on_cover {X : TopCat} {J' : Type u} [CategoryTheory.SmallCategory J'] [CategoryTheory.IsFiltered J'] (Y' : CategoryTheory.Functor J' (CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ AddCommGrpCat)) (hY : ∀ (j : J'), TopCat.Presheaf.IsSheaf (Y'.obj j)) {c : CategoryTheory.Limits.Cocone Y'} (hc : CategoryTheory.Limits.IsColimit c) {ι : Type u} {V : TopologicalSpace.Opens ↑X} {W : ι → TopologicalSpace.Opens ↑X} (hW : ∀ (k : ι), W k ≤ V) {t : Finset ι} (hcov : V ≤ ⨆ k ∈ t, W k) (a : CategoryTheory.ToType (c.pt.obj (Opposite.op V))) (ha : ∀ k ∈ t, (CategoryTheory.ConcreteCategory.hom (c.pt.map (CategoryTheory.homOfLE ⋯).op)) a = 0) : a = 0

A section of a filtered colimit that restricts to zero on a finite open cover is zero. Combines representative extraction, per-element eventual vanishing, merging to a common index, and sheaf separation.

theorem filtered_colimit_exists_compatible_representatives {X : TopCat} {J' : Type u} [CategoryTheory.SmallCategory J'] [CategoryTheory.IsFiltered J'] (P : CategoryTheory.Functor J' (CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ AddCommGrpCat)) {c : CategoryTheory.Limits.Cocone P} (hc : CategoryTheory.Limits.IsColimit c) {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) (sf : (i : ι) → CategoryTheory.ToType (c.pt.obj (Opposite.op (U i)))) (hcompat : TopCat.Presheaf.IsCompatible c.pt U sf) {t : Finset ι} : ∃ (j₁ : J') (x'' : (k : ↥t) → CategoryTheory.ToType ((P.obj j₁).obj (Opposite.op (U ↑k)))), TopCat.Presheaf.IsCompatible (P.obj j₁) (fun (k : ↥t) => U ↑k) x'' ∧ ∀ (k : ↥t), (CategoryTheory.ConcreteCategory.hom ((c.ι.app j₁).app (Opposite.op (U ↑k)))) (x'' k) = sf ↑k

A finite compatible family in a filtered colimit admits representatives at one filtered stage that are pairwise compatible on the chosen finite subfamily.

theorem colimit_exists_gluing_of_compatible_finite_subcover {X : TopCat} {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} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) (sf : (i : ι) → CategoryTheory.ToType (c.pt.obj (Opposite.op (U i)))) {t : Finset ι} (hsup_le : iSup U ≤ ⨆ k ∈ t, U k) (j₁ : J') (x'' : (k : ↥t) → CategoryTheory.ToType ((P.obj j₁).obj (Opposite.op (U ↑k)))) (hx''_compat : TopCat.Presheaf.IsCompatible (P.obj j₁) (fun (k : ↥t) => U ↑k) x'') (hx'' : ∀ (k : ↥t), (CategoryTheory.ConcreteCategory.hom ((c.ι.app j₁).app (Opposite.op (U ↑k)))) (x'' k) = sf ↑k) : ∃ (s : CategoryTheory.ToType (c.pt.obj (Opposite.op (iSup U)))), ∀ k ∈ t, (CategoryTheory.ConcreteCategory.hom (c.pt.map (TopologicalSpace.Opens.leSupr U k).op)) s = sf k

A compatible family on a finite subcover, represented at a single filtered index, glues to a section of any cocone point with the prescribed finite restrictions.

theorem colimit_restrict_eq_of_eq_on_finite_subcover {X : TopCat} {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) {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) (sf : (i : ι) → CategoryTheory.ToType (c.pt.obj (Opposite.op (U i)))) (hcompat : TopCat.Presheaf.IsCompatible c.pt U sf) {t : Finset ι} (hsup_le : iSup U ≤ ⨆ k ∈ t, U k) (s : CategoryTheory.ToType (c.pt.obj (Opposite.op (iSup U)))) (hs_k : ∀ k ∈ t, (CategoryTheory.ConcreteCategory.hom (c.pt.map (TopologicalSpace.Opens.leSupr U k).op)) s = sf k) (i : ι) : (CategoryTheory.ConcreteCategory.hom (c.pt.map (TopologicalSpace.Opens.leSupr U i).op)) s = sf i

If a section on iSup U agrees with a compatible family on a finite subcover, then it restricts to that family on every U i.

theorem colimit_existsUnique_gluing_of_compatible_finite_subcover {X : TopCat} {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) {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) (sf : (i : ι) → CategoryTheory.ToType (c.pt.obj (Opposite.op (U i)))) (hcompat : TopCat.Presheaf.IsCompatible c.pt U sf) {t : Finset ι} (hsup_le : iSup U ≤ ⨆ k ∈ t, U k) : ∃! s : CategoryTheory.ToType (c.pt.obj (Opposite.op (iSup U))), TopCat.Presheaf.IsGluing c.pt U sf s

A compatible family in a filtered colimit admits a unique gluing once the total open is dominated by a finite subcover.