Step 3 of Theorem 103 in the compatible-family form: the descended family functor #
Step 3 of the proof of [Kol07, Theorem 103]: the functor defined on the triples with a global
hypersurface of maximal contact descends "as in (37)" to the whole class, and Theorem 103 (2) holds
for the descended functor. In the compatible-family form the value of the descended functor on a
triple T of the class BOClass m is, on every relatively compact open U, the sequence
descended from the family's value on the coproduct of a finite cover of the closure of U by
pieces with maximal contact (GlobalizeFamCover.lean, GlobalizeFamDescent.lean), the cover
being chosen for each U (chosenCover, globalizeSeqOn). Every property of the descended
functor is an instance of the comparison lemma of GlobalizeFamDescent.lean:
ShrunkMCCover.descent_eq_globalizeSeqOn— the descent along any finite cover of the closure ofUby pieces with maximal contact is the chosen one (the uniqueness in [Kol07, Proposition 37]);globalizeSeqOn_compat— the values are compatible under restriction: onU ≤ Vthe value onUis the pull-back of the value onValong the open inclusion with empty blow-ups deleted ([Wlo09, Theorem 2.0.3 (4)] with [Wlo09, Definition 3.2.6]);globalizeSeqOn_eq_seqOn,globalizeFam_fam_eq— on a triple with a global hypersurface of maximal contact the descended functor agrees with the family;globalizeSeqOn_commutes,globalizeFam_commutesWithLocalIsos— the descended functor commutes with local analytic isomorphisms (Theorem 103 (2); both clauses of [Kol07, 34.1] per open).
AnalyticFamilyFunctor.globalizeFam B hB is the descended family functor on BOClass m; the
existence statement BO_globalizeFam and the descent of the remaining clauses of Theorem 103 are in
GlobalizeFamClauses.lean; globalizeFam_seqOn_eq_pullback restates the cover-independence for
the pull-back along a local isomorphism (a form no other declaration depends on), and the descended
functor of the local functor of Steps 1 and 2 is localFunctorFam there.
The class LocalMCClass m of triples with a global hypersurface of maximal contact is closed
under pull-back along local analytic isomorphisms, stated for the pull-back triple
T'.pullback g hg itself, the form the comparison lemma takes; it restates
localMCClass_of_isPullbackOf (GlobalizeCover.lean), which is stated for any triple carrying the
pull-back data and carries the finite-dimensionality binder, supplied here by
finiteDimensional_of_chartIso.
A finite cover of the closure of U by pieces with maximal contact, chosen once for each
triple and each relatively compact open U (exists_shrunkMCCover).
Equations
Instances For
Kollár's B̄(X) on the relatively compact open U: the sequence descended from the family's
value on the coproduct of the chosen cover (ShrunkMCCover.descent).
Equations
- B.globalizeSeqOn hB hT U hU = (Hironaka.Manifold.AnalyticFamilyFunctor.chosenCover hT U hU).descent B hT ⋯
Instances For
The descended value on U has no empty centres.
The descent along any finite cover of the closure of U by pieces with maximal contact is the
chosen one (the uniqueness in [Kol07, Proposition 37]): by the comparison lemma the value on the
given cover is the pull-back of the chosen descent along the given cover map, with empty blow-ups
deleted; the cover map is surjective, so nothing is deleted, and the descent along the given cover
is unique.
The descended values are compatible under restriction ([Wlo09, Theorem 2.0.3 (4)] with
[Wlo09, Definition 3.2.6]): on U ≤ V the value on U is the pull-back of the value on V along
the open inclusion with empty blow-ups deleted. This is the comparison lemma for the chosen cover
of U against the chosen cover of V, and the uniqueness of the descent along the cover of U.
On a triple with a global hypersurface of maximal contact the descended value is the family's
own value: the family commutes with the coproduct map of the chosen cover, which is surjective onto
U, and the descent is unique.
The value of the descended functor on a triple T of the class BOClass m: the compatible
family of the descended sequences over the relatively compact opens.
Equations
- B.globalizeFamily hB hT = { seqOn := fun (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) => B.globalizeSeqOn ⋯ hT U hU, noEmptyCenters := ⋯, compat := ⋯ }
Instances For
Step 3 of the proof of [Kol07, Theorem 103] in the compatible-family form: the extension to
the class BOClass m of a family functor B on the class LocalMCClass m of triples with a global
hypersurface of maximal contact, B commuting with local analytic isomorphisms. On every relatively
compact open U the value is descended from the value of B on the coproduct of a finite cover of
the closure of U by pieces with maximal contact ("we argue as in (37)").
Equations
- B.globalizeFam hB = { fam := fun {M : AnalyticManifold 𝕜 E} (x : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass m x) => B.globalizeFamily ⋯ hT }
Instances For
The descended functor agrees with B on the class LocalMCClass m (the descent along the
cover of Step 3 of the proof of [Kol07, Theorem 103] restricts to the identity on the pieces).
Theorem 103 (2) for the descended values, both clauses of [Kol07, 34.1] per open: along a
local analytic isomorphism g the value on U' is the pull-back of the value on g(U') with empty
blow-ups deleted. This is the comparison lemma for the chosen cover of U', composed with g,
against the chosen cover of g(U'), and the uniqueness of the descent.
The descended functor commutes with local analytic isomorphisms ([Kol07, Theorem 103 (2)]).
Cover-independence for the pull-back along a local isomorphism (a form no other declaration
of the library depends on): along a local analytic isomorphism g : N → M with T₁ the pull-back
of a triple T of the class and T₁ with
a global hypersurface of maximal contact, the value of B on a relatively compact U₁ ⊆ N with
g(U₁) = U is the pull-back of the descended value on U along g|_{U₁}; no empty blow-up is
deleted, since g|_{U₁} is onto U.