Closed immersions

This module packages the TopCat API for the closed inclusion closedIncl : TopCat.of s ⟶ X and the stalk comparisons needed in the closed-immersion step of Grothendieck vanishing.

Main results:

• closedIncl_isClosedEmbedding and closedIncl_isInducing record the basic topology of the closed inclusion.
• closedIncl_map_eq_bot_of_le_compl shows that opens contained in the complement pull back to ⊥ on the closed subspace.
• pushforward_closedIncl_stalk_eq_zero identifies stalks of a closed-immersion pushforward away from the closed subset with zero.
• closedIncl_pushforward_preservesEpis/Monos and closedIncl_pushforward_shortExact package exactness of pushforward along the closed inclusion for AddCommGrpCat-valued sheaves.
• stalkFunctor_map_iso_toSheafify identifies the stalk of sheafification with an isomorphism.
• closedIncl_counit_isIso identifies the pushforward-pullback counit for presheaves on the closed subspace carrying a sheaf condition.
• stalkPullbackHom_naturality is the stalk-level naturality needed to compare the unit with the counit isomorphism.
• closedIncl_unit_stalk_isIso shows that the adjunction unit is an isomorphism on stalks at points of the closed subset.
• epi_unit_of_closedImmersion upgrades the adjunction unit to an epi of sheaves.
• closedImmersionSES and closedImmersionSES_shortExact package the short exact sequence 0 → ker(η) → F → i_*(i^*F) → 0 associated to a closed immersion.

@[implicit_reducible]

instance sheafAbelianAddCommGrp (X : TopCat) : CategoryTheory.Abelian (TopCat.Sheaf AddCommGrpCat X)

Equations

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

def TopCat.closedIncl {X : TopCat} {s : Set ↑X} (hs : IsClosed s) : of ↑s ⟶ X

Closed inclusion s ↪ X as a morphism in TopCat.

Equations

• TopCat.closedIncl hs = TopCat.ofHom { toFun := Subtype.val, continuous_toFun := ⋯ }

theorem TopCat.set_range_closedIncl {X : TopCat} {s : Set ↑X} (hs : IsClosed s) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (closedIncl hs)) = s

theorem TopCat.closedIncl_isClosedEmbedding {X : TopCat} {s : Set ↑X} (hs : IsClosed s) : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (closedIncl hs))

theorem TopCat.closedIncl_isInducing {X : TopCat} {s : Set ↑X} (hs : IsClosed s) : Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom (closedIncl hs))

theorem TopCat.closedIncl_map_eq_bot_of_le_compl {X : TopCat} {s : Set ↑X} (hs : IsClosed s) {U : TopologicalSpace.Opens ↑X} (hU : U ≤ { carrier := sᶜ, is_open' := ⋯ }) : (TopologicalSpace.Opens.map (closedIncl hs)).obj U = ⊥

instance TopCat.closedIncl_stalkPushforward_isIso {X : TopCat} {s : Set ↑X} {hs : IsClosed s} {C : Type u_1} [CategoryTheory.Category.{u, u_1} C] [CategoryTheory.Limits.HasColimits C] {F : Presheaf C (of ↑s)} {x : ↑(of ↑s)} : CategoryTheory.IsIso (Presheaf.stalkPushforward C (closedIncl hs) F x)

theorem TopCat.opensMap_range_isBasis_of_isInducing {X Y : TopCat} {f : X ⟶ Y} (hf : Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f)) : TopologicalSpace.Opens.IsBasis (Set.range (TopologicalSpace.Opens.map f).obj)

theorem TopCat.opensMap_isCoverDense_of_isInducing {X Y : TopCat} {f : X ⟶ Y} (hf : Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f)) : (TopologicalSpace.Opens.map f).IsCoverDense (Opens.grothendieckTopology ↑X)

instance TopCat.opensMap_isLocallyFull {X Y : TopCat} (f : X ⟶ Y) : (TopologicalSpace.Opens.map f).IsLocallyFull (Opens.grothendieckTopology ↑X)

theorem TopCat.locallyInjective_stalkFunctor_map_injective {C : Type u_1} [CategoryTheory.Category.{u, u_1} C] [CategoryTheory.Limits.HasColimits C] {FC : C → C → Type u_2} {CC : C → Type u} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] {X : TopCat} {F G : Presheaf C X} (T : F ⟶ G) [CategoryTheory.Presheaf.IsLocallyInjective (Opens.grothendieckTopology ↑X) T] (x : ↑X) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((Presheaf.stalkFunctor C x).map T))

theorem TopCat.stalkFunctor_map_iso_toSheafify {C : Type u_1} [CategoryTheory.Category.{u, u_1} C] [CategoryTheory.Limits.HasColimits C] {FC : C → C → Type u_2} {CC : C → Type u} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {X : TopCat} [CategoryTheory.HasWeakSheafify (Opens.grothendieckTopology ↑X) C] [(Opens.grothendieckTopology ↑X).WEqualsLocallyBijective C] (P : Presheaf C X) (x : ↑X) : CategoryTheory.IsIso ((Presheaf.stalkFunctor C x).map (CategoryTheory.toSheafify (Opens.grothendieckTopology ↑X) P))

theorem TopCat.closedIncl_counit_isIso {C : Type u_1} [CategoryTheory.Category.{u, u_1} C] {FC : C → C → Type u_2} {CC : C → Type u} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasColimits C] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {X : TopCat} {s : Set ↑X} (hs : IsClosed s) (F : Sheaf C (of ↑s)) : CategoryTheory.IsIso ((Sheaf.pullbackPushforwardAdjunction C (closedIncl hs)).counit.app F)

theorem pushforward_closedIncl_stalk_eq_zero {X : TopCat} {s : Set ↑X} (hs : IsClosed s) {G : TopCat.Presheaf AddCommGrpCat (TopCat.of ↑s)} (hG : G.IsSheaf) {x : ↑X} (hx : x ∉ s) (a : ↑((TopCat.Presheaf.stalkFunctor AddCommGrpCat x).obj ((TopCat.Presheaf.pushforward AddCommGrpCat (TopCat.closedIncl hs)).obj G))) : a = 0

Stalks of a pushforward along a closed inclusion vanish outside the closed set: if x ∉ s, every element of stalk(i_*(G), x) is zero.

theorem epi_pushforward_map_closedIncl_of_locallySurjective {X : TopCat} {s : Set ↑X} (hs : IsClosed s) {F G : TopCat.Presheaf AddCommGrpCat (TopCat.of ↑s)} (hF : F.IsSheaf) (hG : G.IsSheaf) (f : F ⟶ G) (hf_loc : TopCat.Presheaf.IsLocallySurjective f) : CategoryTheory.Epi ((TopCat.Sheaf.pushforward AddCommGrpCat (TopCat.closedIncl hs)).map (have this := CategoryTheory.ObjectProperty.homMk f; this))

Pushforward along a closed immersion preserves epis: if f : F ⟶ G is epi in presheaves on the closed subspace, then i_*(f) is epi in sheaves on the ambient space whenever f is locally surjective. Proof: stalkwise surjectivity (identity on the closed set, zero outside).

instance closedIncl_pushforward_preservesEpis {X : TopCat} {s : Set ↑X} (hs : IsClosed s) : (TopCat.Sheaf.pushforward AddCommGrpCat (TopCat.closedIncl hs)).PreservesEpimorphisms

instance closedIncl_pushforward_preservesMonos {X : TopCat} {s : Set ↑X} (hs : IsClosed s) : (TopCat.Sheaf.pushforward AddCommGrpCat (TopCat.closedIncl hs)).PreservesMonomorphisms

theorem closedIncl_pushforward_shortExact {X : TopCat} {s : Set ↑X} (hs : IsClosed s) {S : CategoryTheory.ShortComplex (TopCat.Sheaf AddCommGrpCat (TopCat.of ↑s))} (hSE : S.ShortExact) : (S.map (TopCat.Sheaf.pushforward AddCommGrpCat (TopCat.closedIncl hs))).ShortExact

Pushforward along a closed immersion preserves short exact sequences.

theorem TopCat.stalkPullbackHom_naturality {C : Type u_1} [CategoryTheory.Category.{u, u_1} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) {F G : Presheaf C Y} (α : F ⟶ G) (x : ↑X) : CategoryTheory.CategoryStruct.comp ((Presheaf.stalkFunctor C ((CategoryTheory.ConcreteCategory.hom f) x)).map α) (Presheaf.stalkPullbackHom C f G x) = CategoryTheory.CategoryStruct.comp (Presheaf.stalkPullbackHom C f F x) ((Presheaf.stalkFunctor C x).map ((Presheaf.pullback C f).map α))

theorem TopCat.closedIncl_unit_stalk_isIso {C : Type u_1} [CategoryTheory.Category.{u, u_1} C] {FC : C → C → Type u_2} {CC : C → Type u} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasColimits C] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {X : TopCat} {s : Set ↑X} (hs : IsClosed s) (F : Sheaf C X) (x : ↑(of ↑s)) : CategoryTheory.IsIso ((Presheaf.stalkFunctor C ((CategoryTheory.ConcreteCategory.hom (closedIncl hs)) x)).map ((Sheaf.pullbackPushforwardAdjunction C (closedIncl hs)).unit.app F).hom)

theorem epi_unit_of_closedImmersion {X : TopCat} (Z : Set ↑X) (hZ : IsClosed Z) (F : TopCat.Sheaf AddCommGrpCat X) : CategoryTheory.Epi ((TopCat.Sheaf.pullbackPushforwardAdjunction AddCommGrpCat (TopCat.closedIncl hZ)).unit.app F)

noncomputable def closedImmersionSES {X : TopCat} (Z : Set ↑X) (hZ : IsClosed Z) (F : TopCat.Sheaf AddCommGrpCat X) : CategoryTheory.ShortComplex (TopCat.Sheaf AddCommGrpCat X)

The short exact sequence 0 → ker(η) → F → i_*(i^*F) → 0 from a closed immersion, where η is the pullback-pushforward adjunction unit and i : Z ↪ X is the inclusion of a closed subset.

Equations

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

theorem closedImmersionSES_shortExact {X : TopCat} (Z : Set ↑X) (hZ : IsClosed Z) (F : TopCat.Sheaf AddCommGrpCat X) : (closedImmersionSES Z hZ F).ShortExact