Stalks of a pushforward off a closed range #
subsingleton_stalk_pushforward — for f : X ⟶ Y with closed range and y ∉ Set.range f, the
stalk (f _* F) y of the pushforward of a sheaf of abelian groups is a subsingleton.
Where this sits #
Exactness of ι_* along a closed immersion is the last input #572 step 3 needs in order to be
instantiated geometrically (CategoryTheory/Sites/Sheaves/CohomologyPushforward.lean proves the
abstract
statement). The standard proof is stalkwise, and it has two halves:
- on the range,
(f _* F)_{f x} ≅ F_x. This is already in Mathlib, asTopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_isInducing, and it needs onlyIsInducing f— not closedness. That matches the geometry: for any embedding, the opens ofXaroundxare exactly the preimages of opens ofYaroundf x; - off the range, the stalk vanishes. That is this file, and it is where closedness is spent.
The proof, and why closedness is the whole of it #
Set.range f closed makes its complement an open offRange containing every y outside the
range, and every open U ≤ offRange pulls back to ⊥. So (f _* F)(U) = F(⊥), which is terminal
for a sheaf — TopCat.Sheaf.isTerminalOfEmpty — hence a subsingleton in AddCommGrpCat.
exists_le_germ_eq is what makes this an argument about one open rather than a cofinality
computation: it produces, for any element of the stalk, a representing section over an open
inside a neighbourhood of one's choosing. Choose offRange, and every germ is a germ of a
section of a terminal object. Two such germs agree because both equal the germ of 0 over
offRange itself, via germ_res_apply.
Scope #
This says nothing about exactness yet. It is one of the two stalk computations that a stalkwise
exactness proof consumes, and the other one is Mathlib's. Bridging from the topological f _* to
the site-level Functor.sheafPushforwardContinuous that #572 step 3 actually quantifies over is
further work again, and is not begun here.
Main results #
offRangeandpreimage_eq_bot_of_le— the open, and that it pulls back to nothing.subsingleton_of_isTerminal— terminal objects ofAddCommGrpCathave subsingleton carriers.subsingleton_stalk_pushforward— the vanishing.stalkPushforward_naturality— naturality in the presheaf, which Mathlib does not have.surjective_stalk_map_pushforwardandisLocallySurjective_pushforward— the two stalk facts assembled: pushforward along a closed embedding preserves local surjectivity, hence (withisLocallySurjective_iff_epi) epimorphisms.preservesEpimorphisms_pushforward— that, as a statement about the sheaf-level functor, which is the same functor the site-level#572machinery quantifies over.preservesFiniteColimits_pushforward— hence exactness, with limits free from the adjunction.additive_pushforward,opensMap_obj_top— the two small pieces the instantiation also needs.
The complement of a closed range, as an open of the target.
Equations
- DerivedAlgGeo.Topology.offRange f hcl = { carrier := (Set.range ⇑(CategoryTheory.ConcreteCategory.hom f))ᶜ, is_open' := ⋯ }
Instances For
Anything inside the complement of the range pulls back to the empty open.
A terminal object of AddCommGrpCat has a subsingleton carrier.
Stated separately because the route is not the obvious one: there is no IsTerminal.isZero to
hand, so this goes through uniqueUpToIso against the zero object and then
AddCommGrpCat.subsingleton_of_isZero.
Off a closed range, the pushforward of a sheaf has no stalk.
The companion of Mathlib's stalkPushforward_iso_of_isInducing, which handles the range itself and
needs only IsInducing. Closedness is spent here and nowhere else.
Naturality of stalkPushforward #
stalkPushforward is natural in the presheaf.
Mathlib has stalkPushforward.id and stalkPushforward.comp — naturality in the space — but
not this, naturality in the presheaf, which is what a stalkwise argument about a morphism of
sheaves needs.
Both set_options are load-bearing. Without them (pushforward C f).obj F is a
Presheaf C Y, which is not reducibly the functor category (Opens Y)ᵒᵖ ⥤ C, and every rewrite
fails with an application type mismatch rather than a missing-pattern error. The pair is exactly
what Mathlib itself puts on stalkPushforward.id and stalkPushforward.comp two declarations
above the result this one sits beside; it is not a workaround invented here.
They also change how dot-notation resolves: under them F.stalkPushforward in tactic position
looks for Functor.stalkPushforward and fails, so a consumer must write
TopCat.Presheaf.stalkPushforward in full. The statement below still uses dot-notation because
the options apply to elaboration of the proof, not of the signature.
Surjectivity on stalks, and local surjectivity #
Pushforward along an inducing map is surjective on stalks, given the vanishing off the range.
Stated for presheaves, with the vanishing as a hypothesis rather than a sheaf condition: the two
cases want different things, and only the off-range one needs G to be a sheaf. The caller
supplies hvan from subsingleton_stalk_pushforward.
On the range this is stalkPushforward_naturality plus the fact that both stalkPushforwards are
isomorphisms; off it the target stalk is a subsingleton and there is nothing to check.
Pushforward along a closed embedding preserves local surjectivity.
With TopCat.Sheaf.isLocallySurjective_iff_epi this is preservation of epimorphisms, which is the
half of exactness that ι_* does not get for free from being a right adjoint.
Preservation of epimorphisms #
Pushforward along a closed embedding preserves epimorphisms.
Together with ι_* being a right adjoint — hence left exact for free — this is exactness, and it
is the last mathematical input #572 step 3 needs.
The site bridge costs nothing, and that is worth stating #
This is phrased about TopCat.Sheaf.pushforward, while #572 step 3 quantifies over
Functor.sheafPushforwardContinuous. They are the same functor by definition:
TopCat.Sheaf.pushforward C f is defined as (Opens.map f).sheafPushforwardContinuous _ _ _,
and Sheaf.pushforward_map and Sheaf.pushforward_obj_val are both rfl. No comparison
isomorphism is needed anywhere, and none is built.
The instances are all imports, not obligations #
TopCat.Sheaf.isLocallySurjective_iff_epi asks for Balanced on both sheaf categories and
ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization AddCommGrpCat. Every one of them
exists; they arrive with Sites.Abelian, Grp.Abelian, Grp.EpiMono and
ConcreteCategory.EpiMono, and a missing import presents as a bare "failed to synthesize", which
reads exactly like a missing theorem.
Exactness #
The sheaf pushforward is additive.
Sheaf.pushforward_map is rfl, so this is rfl on each pair of morphisms; it is stated because
instance search does not find it and Functor.additive_of_preservesBinaryBiproducts does not
apply without more setup than the fact deserves.
Pushforward along a closed embedding is exact.
Limits it preserves for free, being a right adjoint. For colimits: preserving zero morphisms,
epimorphisms and kernels gives PreservesHomology
(Functor.preservesHomology_of_preservesEpis_and_kernels), and that gives finite colimits. The
epimorphisms are preservesEpimorphisms_pushforward; the kernels come with the right adjoint.
This is the input #572 step 3 needs in order to instantiate the abstract cohomology comparison
of CategoryTheory/Sites/Sheaves/CohomologyPushforward.lean at a closed immersion.
Opens.map sends the whole space to the whole space.
Trivial, and recorded because the instantiation needs IsTerminal ((Opens.map f).obj ⊤) and
IsTerminal.ofUnique does not discharge it -- the Unique instance it wants is not there.