The independence from the hypersurface of maximal contact, in the compatible-family form #
Step 2.3 of the proof of Theorem 103 ([Kol07, 104]): for two hypersurfaces of maximal contact H,
H', Theorem 92 makes (X, I, H + E) and (X, I, H' + E) étale equivalent, hence so are the two
blow-up sequences, and Theorem 97 makes them identical. A family functor has values only on
relatively compact opens, and the pair ψ, ψ' : U ⇉ X of local analytic isomorphisms given by the
analytic form of [Kol07, Theorem 92] lives on a countable disjoint union U, which is not
relatively compact; the argument is therefore run as follows
(AnalyticFamilyFunctor.seqOn_eq_of_maximalContact).
Theorem 92 (maximalContact_locallyIsoEquivalent) is applied to the triple restricted to the
reading open O; MC-invariance and the maximal-contact inequalities restrict along the inclusion.
On every member V_k of an exhaustion of U by relatively compact opens, the family's commutation
with the local analytic isomorphisms incl_O ∘ ψ and incl_O ∘ ψ'
(seqOn_pullback_eq_of_image_subset), applied to the two pulled-back triples, which coincide, shows
that the restrictions to V_k of the pulled-back sequences ψ^* L and ψ'^* L' agree once empty
blow-ups are deleted. The sequences ψ^* L, ψ'^* L' have no empty centres, because every centre
lies over cosupp(𝓘, m) ⊆ ψ(U), and for k large their restrictions to V_k have none either, a
finite sequence of nonempty centres meeting every large member of the exhaustion
(BlowUpSequence.exists_noEmptyCenters_pullback_of_cover); so the deletions are identities and the
sequences agree on an increasing open cover, hence ψ^* L = ψ'^* L'
(BlowUpSequence.eq_of_eraseEmpty_pullback_eq, from eq_of_pullback_openCover; the functoriality
package is local, [Kol07, 34]). This is clause (3) of [Kol07, Definition 96]; the analytic form of
[Kol07, Theorem 97] (BlowUpSequence.eq_of_locallyIsoEquivalentSequences) then gives L = L'.
IdealSheaf.isMCInvariant_comap— MC-invariance ([Kol07, 53]) is kept by pull-back along a local analytic isomorphism, the derivative ideal sheaves pulling back ([Kol07, Lemma 74 (4)]);HypersurfaceFamily.comap_append_preimage,HypersurfaceFamily.comap_comp_map— the inverse image ofE + Hish^{-1}(E) + h^{-1}(H), and inverse images compose;BlowUpSequence.range_liftStep,BlowUpSequence.exists_noEmptyCenters_pullback_of_cover,BlowUpSequence.eq_of_eraseEmpty_pullback_eq— the argument on the exhaustion;CommutesWithLocalIsos.seqOn_pullback_eq_of_image_subset,fam_seqOn_congr_triple,AnalyticTriple.pullback_eq_of_locallyIsoEquivalentMC,CommutesWithLocalIsos.eraseEmpty_pullback_inclusion_eq— the family's values under the pair;AnalyticFamilyFunctor.seqOn_eq_of_maximalContact— Step 2.3 per relatively compact open, for a family functor commuting with local analytic isomorphisms whose values are of order≥ m, on a class closed under pull-back;BO.stepHClass_of_isPullbackOf,BO.maximalContact_persistsFam_tuned,BO.hfStep22FamOn_indep,hfStep2SeqFamOn_indep— the application to Step 2.2 (Step22Fam.lean): the value of Step 2 on an open does not depend on the hypersurface of maximal contact, since Step 2.1 does not mention it and the value of Step 2.2 is that of Lemma 102's family at the greatest member on the tuned triple of Step 2.2, which is MC-invariant of order≤ s, with the transforms ofHandH'as hypersurfaces of maximal contact for it.
The statements about Step 2 are given in the general form hf… over the data HFData ψ₀ s of
Step 2 (HFamData.lean) and as the instance for Lemma 102's data. This independence is what lets
the local functor commute with local analytic isomorphisms (LocalFunctorFam.lean).
MC-invariance restricts along local analytic isomorphisms #
MC-invariance ([Kol07, 53]) is kept by pull-back along a local analytic isomorphism:
h^*(MC(J) · D(J)) = MC(h^* J) · D(h^* J) ≤ h^* J, the derivative ideal sheaves pulling back
([Kol07, Lemma 74 (4)]). Not in the sources; needed because Theorem 92 is applied here to the
triple restricted to an open.
Two equations for hypersurface families #
The inverse image along a composite is the iterated inverse image.
Eventually no empty centres along an increasing cover #
The range of the lift of a map to a blowing-up is the preimage of the range of the map under the blow-down.
A finite sequence of centres with no empty centres, pulled back along an increasing family of
local analytic isomorphisms whose ranges cover the manifold, has no empty centres from some index
on: each of its finitely many nonempty centres meets the range of every large member. By recursion
on the sequence, the family lifted along the first blow-up (range_liftStep). Not in the sources;
the finiteness of a blow-up sequence ([Kol07, Definition 29]) is what is used.
Two sequences with no empty centres whose pull-backs along an increasing cover by analytic open
embeddings agree once empty blow-ups are deleted are equal: from some index on nothing is deleted
(exists_noEmptyCenters_pullback_of_cover), and a sequence is determined by its pull-backs along
an open cover (eq_of_pullback_openCover; the functoriality package is local, [Kol07, 34]).
The family's value under a local isomorphism into a relatively compact open #
The commutation of a family functor with local analytic isomorphisms ([Kol07, 34.1] per open),
for a local analytic isomorphism g carrying a relatively compact open V into a relatively
compact open O: the value of the pulled-back triple on V is the pull-back of the value on O
along g|_V : V → O with the empty blow-ups deleted. The commutation gives it with the image g(V)
in place of O; the compatibility from g(V) to O and the merging of the two deletions
(eraseEmpty_pullback_eraseEmpty) finish.
The value of a family functor on an open depends on the triple only, not on the proof of membership in the class.
Theorems 92 and 97 per relatively compact open #
The pair ψ, ψ' given by the analytic form of [Kol07, Theorem 92] for the restricted triple
pulls the two triples (X, I, E + H) and (X, I, E + H') back to the same triple on U: the
ideal sheaves agree by clause (2′) of the equivalence, the boundaries by clauses (1′) and (3′).
For two triples on X whose pull-backs along incl_O ∘ ψ and incl_O ∘ ψ' coincide, the
restrictions to a relatively compact open V ⊆ U of the pulled-back values ψ^* L and ψ'^* L'
agree once empty blow-ups are deleted: seqOn_pullback_eq_of_image_subset for both, on the equal
triples, with (incl_O ∘ ψ)|_V = ψ ∘ incl_V.
Step 2.3 of the proof of Theorem 103 per relatively compact open ([Kol07, 104], with the
analytic forms of [Kol07, Theorem 92] and [Kol07, Theorem 97]): for a family functor B commuting
with local analytic isomorphisms, whose values are of order ≥ m for the restricted triples, on a
class closed under pull-back along local analytic isomorphisms, two triples TH, TH' with the
same MC-invariant ideal sheaf of order ≤ m and boundaries E + H, E + H' with H, H'
hypersurfaces of maximal contact have the same value on every relatively compact open O.
Theorem 92 for the restricted triple on O gives the pair ψ, ψ' : U ⇉ O; the family commutes with
incl_O ∘ ψ and incl_O ∘ ψ' on every member of an exhaustion of U, the pulled-back triples
being equal; the pulled-back sequences have no empty centres, so eq_of_eraseEmpty_pullback_eq
gives ψ^* L = ψ'^* L', and Theorem 97 (eq_of_locallyIsoEquivalentSequences) gives L = L'.
Stated with the equations hI, hF, hF' between the fields of the two triples.
Step 2.2 on an open does not see the hypersurface #
The class of Step 2.2 (triples of BOClass s whose boundary has a greatest member,
Step22Defs.lean) is closed under pull-back along every local analytic isomorphism: the class
BOClass s is, and the index set is kept.
The transform of a hypersurface of maximal contact along a sequence of order ≥ s is a
hypersurface of maximal contact for the tuned triple of Step 2.2: it is one for the untuned triple
(maximalContact_persistsFam, Step22FamPersist.lean), and MC(W_s(I)) = MC(I)
([Kol07, Proposition 99 (4)]).
Step 2.3 of the proof of Theorem 103 ([Kol07, 104]) for Step 2.2 on an open, in the general form
over the data HFData of Step 2: the value of Step 2.2 does not depend on the hypersurface of
maximal contact. It is the value of the family at the greatest member on the tuned triple of Step
2.2, which is MC-invariant (isMCInvariant_tuned) of order ≤ s (ord_tuned_le), with the
transforms of H and H' as hypersurfaces of maximal contact for it
(maximalContact_persistsFam_tuned), on the class of Step 2.2, closed under pull-back
(stepHClass_of_isPullbackOf); seqOn_eq_of_maximalContact applies.
Step 2.3 of the proof of Theorem 103 ([Kol07, 104]) for Step 2 on an open, in the general form
over the data HFData of Step 2: the value of Step 2 does not depend on the choice of the
hypersurface of maximal contact, since Step 2.1 and the opens do not mention H and the value of
Step 2.2 does not depend on it (hfStep22FamOn_indep).