Bookkeeping for the one-step descent of agreement

Small lemmas used by the proof of agreeOnSubspace_blowUpLift (Hironaka/Resolution/Analytic/MaximalContact/OneStepDescent.lean):

• stalkCast: the transport 𝒪_{M,x} ≃ 𝒪_{M,y} along an equality of points x = y (a ring homomorphism, the identity after subst), with its behaviour on germs of sections, constants, coordinate germs and pulled-back germs — all by subst. It lets the two lifts f' q = g' q be compared without rewriting under dependent types.
• germMap_germMap_germ: functoriality of the stalk maps for a commuting square π ∘ f' = f ∘ π', on germs of sections (no cast: the two membership proofs are separate).
• eval_map_of_isLocalHom: a local stalk homomorphism fixing the constants preserves values.
• stalkIdeal_le_vanishingStalk_of_subset_cosupport: if Z ⊆ cosupp J then every germ of J vanishes on Z — the bridge from Kollár's "Z_i^U ⊆ W_i" [Kol07, Theorem 97, proof] to J ⊆ I_Z (the hypothesis 1 ≤ ν_Z(J) of the marked transform with mark 1).
• Ideal.mem_colon_span_singleton_iff: the colon by a principal ideal (the stalk of the marked transform on the exceptional divisor; off it the colon is by the unit ideal, Ideal.colon_coe_top of Hironaka/Scheme/Snc/TotalTransformOffCentre.lean).
• agreeOnSubspace_of_forall_sub_mem: the pointwise criterion for AgreeOnSubspace f' g' K — at every q with K_q ≠ ⊤, f' q = g' q and f'^* s − g'^* s ∈ K_q for every germ s.

The colon by a principal ideal

theorem Ideal.mem_colon_span_singleton_iff {R : Type u_1} [CommRing R] (I : Ideal R) (e x : R) : x ∈ Submodule.colon I ↑(span {e}) ↔ x * e ∈ I

Values through local homomorphisms; germs of an ideal vanish on its cosupport

theorem Hironaka.Manifold.eval_map_of_isLocalHom {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {N : Type u} [TopologicalSpace N] [ChartedSpace E N] {a : M} {b : N} (G : ↑((Manifold.structureSheaf 𝕜 E M).presheaf.stalk a) →+* ↑((Manifold.structureSheaf 𝕜 E N).presheaf.stalk b)) [IsLocalHom G] (hG : ∀ (c : 𝕜), G ((Manifold.const 𝕜 E M a) c) = (Manifold.const 𝕜 E N b) c) (s : ↑((Manifold.structureSheaf 𝕜 E M).presheaf.stalk a)) : (Manifold.eval 𝕜 E N b) (G s) = (Manifold.eval 𝕜 E M a) s

A local ring homomorphism of stalks fixing the constants preserves the values of germs.

theorem Hironaka.Manifold.stalkIdeal_le_vanishingStalk_of_subset_cosupport {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Z : Set M} (J : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) (hZ : Z ⊆ J.support) (a : M) : J.stalkIdeal a ≤ Manifold.vanishingStalk Z a

Kollár's "Z_i^U ⊆ W_i" [Kol07, Theorem 97, proof] read at the level of ideals: if the closed set Z lies in the cosupport of J, every germ of J vanishes on Z — J_a ⊆ I_{Z,a} for the vanishing ideal of Z (vanishingStalk).

Transport of stalks along an equality of points

noncomputable def Hironaka.Manifold.stalkCast {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {x y : M} (h : x = y) : ↑((Manifold.structureSheaf 𝕜 E M).presheaf.stalk x) →+* ↑((Manifold.structureSheaf 𝕜 E M).presheaf.stalk y)

The transport 𝒪_{M,x} → 𝒪_{M,y} along x = y (the identity after subst).

Equations

• Hironaka.Manifold.stalkCast h = h ▸ RingHom.id ↑((Manifold.structureSheaf 𝕜 E M).presheaf.stalk x)

theorem Hironaka.Manifold.stalkCast_germ {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {x y : M} (h : x = y) {W : TopologicalSpace.Opens M} (hx : x ∈ W) (hy : y ∈ W) (s : ↑((Manifold.structureSheaf 𝕜 E M).presheaf.obj (Opposite.op W))) : (stalkCast h) ((CategoryTheory.ConcreteCategory.hom ((Manifold.structureSheaf 𝕜 E M).presheaf.germ W x hx)) s) = (CategoryTheory.ConcreteCategory.hom ((Manifold.structureSheaf 𝕜 E M).presheaf.germ W y hy)) s

theorem Hironaka.Manifold.stalkCast_const {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {x y : M} (h : x = y) (c : 𝕜) : (stalkCast h) ((Manifold.const 𝕜 E M x) c) = (Manifold.const 𝕜 E M y) c

theorem Hironaka.Manifold.stalkCast_coord {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {x y : M} (h : x = y) {φ : OpenPartialHomeomorph M E} (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (hx : x ∈ φ.source) (hy : y ∈ φ.source) (i : Fin n) : (stalkCast h) (Manifold.coord E ψ φ hφ hx i) = Manifold.coord E ψ φ hφ hy i

instance Hironaka.Manifold.isLocalHom_stalkCast {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {x y : M} (h : x = y) : IsLocalHom (stalkCast h)

Functoriality of the stalk maps on a commuting square; the pointwise criterion

theorem Hironaka.Manifold.stalkCast_germMap_germ {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M M' : AnalyticManifold 𝕜 E} (π : AnalyticMap M' M) {x y : M'.carrier} (h : x = y) {V : TopologicalSpace.Opens M.carrier} (hV : π x ∈ V) (hV' : π y ∈ V) (t : ↑((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.obj (Opposite.op V))) : (stalkCast h) ((Manifold.germMap ⇑π ⋯ x) ((CategoryTheory.ConcreteCategory.hom ((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.germ V (π x) hV)) t)) = (Manifold.germMap ⇑π ⋯ y) ((CategoryTheory.ConcreteCategory.hom ((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.germ V (π y) hV')) t)

The transport commutes with the stalk map of π on germs of sections.

theorem Hironaka.Manifold.germMap_germMap_germ {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U U' M M' : AnalyticManifold 𝕜 E} (f' : AnalyticMap U' M') (π : AnalyticMap M' M) (π' : AnalyticMap U' U) (f : AnalyticMap U M) (hcomm : ∀ (x : U'.carrier), π (f' x) = f (π' x)) (q : U'.carrier) {W : TopologicalSpace.Opens M.carrier} (hW : π (f' q) ∈ W) (hW' : f (π' q) ∈ W) (h : ↑((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.obj (Opposite.op W))) : (Manifold.germMap ⇑f' ⋯ q) ((Manifold.germMap ⇑π ⋯ (f' q)) ((CategoryTheory.ConcreteCategory.hom ((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.germ W (π (f' q)) hW)) h)) = (Manifold.germMap ⇑π' ⋯ q) ((Manifold.germMap ⇑f ⋯ (π' q)) ((CategoryTheory.ConcreteCategory.hom ((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.germ W (f (π' q)) hW')) h))

Functoriality of the stalk maps on a commuting square π ∘ f' = f ∘ π', on the germ of a section h at the common image point (the two membership proofs are separate, so no transport of stalks is needed).

theorem Hironaka.Manifold.agreeOnSubspace_of_forall_sub_mem {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U' M' : AnalyticManifold 𝕜 E} (f' g' : AnalyticMap U' M') (K : U'.IdealSheaf) (h : ∀ (q : U'.carrier), Manifold.IdealSheaf.stalkIdeal K q ≠ ⊤ → ∃ (hpp' : f' q = g' q), ∀ (s : ↑((Manifold.structureSheaf 𝕜 E M'.carrier).presheaf.stalk (f' q))), (Manifold.germMap ⇑f' ⋯ q) s - (Manifold.germMap ⇑g' ⋯ q) ((stalkCast hpp') s) ∈ Manifold.IdealSheaf.stalkIdeal K q) : AgreeOnSubspace f' g' K

The pointwise criterion for AgreeOnSubspace f' g' K: at every point q where K_q ≠ ⊤, the two maps agree, f' q = g' q, and their stalk maps agree modulo K_q on every germ at that point (the second read through the transport along f' q = g' q).