Step 3 of Theorem 103 in the compatible-family form: the finite cover of a compact closure #
Step 3 of the proof of [Kol07, Theorem 103] covers X by open subsets X^{(j)} on each of which
"there is a smooth hypersurface of maximal contact". In the compatible-family
form the value of a functor is read on a relatively compact open U, so only the compact closure
of U has to be covered: finitely many of the neighbourhoods with maximal contact of
[Kol07, Theorem 80 (2)] (exists_isPullbackOf_localMCClass, LocalMaximalContact.lean), embedded
by ιᵢ : Nᵢ → M, suffice, and each is shrunk to an open Wᵢ with compact closure inside the range
of ιᵢ (the manifold is locally compact), so that the pieces ιᵢ^{-1}(Wᵢ ∩ U) are relatively
compact in the charts. The data are bundled as ShrunkMCCover T m U, a shrunk embedding cover
(ShrunkMCCover.toCover : ShrunkEmbeddingCover M U, ShrunkEmbeddingCover.lean) with maximal
contact on the pieces. The coproduct ⊔ᵢ Nᵢ carries the pull-back triple of T, which has a global
hypersurface of maximal contact (localMCClass_pullback_sigmaDescMap, SigmaContact.lean); the
open ⊔ᵢ ιᵢ^{-1}(Wᵢ ∩ U) has compact closure, and the restriction of the coproduct map to it is
Kollár's g : X^* → X over U, surjective onto U and a coproduct of open embeddings (the lemmas
of ShrunkEmbeddingCover, restated on ShrunkMCCover).
AnalyticTriple.exists_finite_shrunk_mcCover— the existence of the cover;ShrunkMCCover,exists_shrunkMCCover— the data and their existence;ShrunkMCCover.sigma,desc,triple,localMCClass_triple— the coproduct, the coproduct map and the pulled-back triple, in the classLocalMCClass m;ShrunkMCCover.opens,isCompact_closure_opens,image_opens_eq— the open⊔ᵢ ιᵢ^{-1}(Wᵢ ∩ U), relatively compact, mapping ontoU;ShrunkMCCover.coverMap,surjective_coverMap,isCoprodOfOpenEmbeddings_coverMap— the cover map⊔ᵢ ιᵢ^{-1}(Wᵢ ∩ U) → U;AnalyticFamilyFunctor.CommutesWithLocalIsos.seqOn_eq_of_image_eq— the commutation of a family functor with a local isomorphism, for a named image open.
The descent of a family functor's value along this cover is in GlobalizeFamDescent.lean.
A compact set of a triple of the class BOClass m is covered by finitely many opens Wᵢ with
compact closures, each inside the range of an open embedding ιᵢ : Nᵢ → M whose pulled-back
triple has a hypersurface of maximal contact (Step 3 of the proof of [Kol07, Theorem 103] with
[Kol07, Theorem 80 (2)], on a compact set). Each point has such a neighbourhood
(exists_isPullbackOf_localMCClass), which contains a compact neighbourhood of the point by local
compactness; finitely many of their interiors cover the compact set.
The data of a finite cover of the closure of a relatively compact open U by open sets Wᵢ
with compact closures, each inside the range of an open embedding ιᵢ : Nᵢ → M whose pulled-back
triple has a hypersurface of maximal contact (Step 3 of the proof of [Kol07, Theorem 103] on the
compact closure of U).
The finite index set (a finite set of points of
M).- N : ↥self.t → AnalyticManifold 𝕜 E
The manifolds of the pieces.
- ι (i : ↥self.t) : AnalyticMap (self.N i) M
The open embeddings of the pieces.
- hι (i : ↥self.t) : IsAnalyticOpenEmbedding (self.ι i)
The maps
ιᵢare analytic open embeddings. - W : ↥self.t → TopologicalSpace.Opens M.carrier
The opens
WᵢofM. - hmc (i : ↥self.t) : HasMaximalContact m (T.pullback (self.ι i) ⋯)
Each pulled-back triple has a global hypersurface of maximal contact.
Each
Wᵢhas compact closure.The closure of
Wᵢlies in the range ofιᵢ.The
Wᵢcover the closure ofU.
Instances For
A finite shrunk cover with maximal contact exists for every triple of the class BOClass m
and every relatively compact open U (exists_finite_shrunk_mcCover for the closure of U).
The cover as a shrunk embedding cover (ShrunkEmbeddingCover), forgetting the maximal
contact. The coproduct, the open ⊔ᵢ ιᵢ^{-1}(Wᵢ ∩ U) and the cover map below are those of this
cover.
Equations
Instances For
The coproduct ⊔ᵢ Nᵢ of the pieces (Kollár's X^*).
Instances For
The coproduct ⊔ᵢ ιᵢ : ⊔ᵢ Nᵢ → M of the embeddings (Kollár's g : X^* → X).
Instances For
The coproduct map is a local analytic isomorphism.
The coproduct map is a coproduct of open embeddings.
The pull-back of T to the coproduct (Kollár's (X^*, g^* I, g^{-1} E)).
Instances For
The pulled-back triple on the coproduct is in the class LocalMCClass m: it has a global
hypersurface of maximal contact, the union of those of the pieces (Step 3 of the proof of
[Kol07, Theorem 103]; localMCClass_pullback_sigmaDescMap).
The open ⊔ᵢ ιᵢ^{-1}(Wᵢ ∩ U) of the coproduct.
Instances For
The closed set ⊔ᵢ ιᵢ^{-1}(closure Wᵢ) of the coproduct, which contains the closure of
opens.
Equations
- C.closedHull = C.toCover.closedHull
Instances For
⊔ᵢ ιᵢ^{-1}(closure Wᵢ) is compact: finitely many pieces, each the preimage under an open
embedding of a compact set inside its range.
The open ⊔ᵢ ιᵢ^{-1}(Wᵢ ∩ U) has compact closure.
The coproduct map sends ⊔ᵢ ιᵢ^{-1}(Wᵢ ∩ U) into U.
The coproduct map sends ⊔ᵢ ιᵢ^{-1}(Wᵢ ∩ U) onto U: the Wᵢ cover the closure of U and
each lies in the range of ιᵢ.
The cover map ⊔ᵢ ιᵢ^{-1}(Wᵢ ∩ U) → U, the restriction of the coproduct map.
Instances For
The cover map is a local analytic isomorphism.
The cover map is surjective onto U.
The cover map is a coproduct of open embeddings.
The commutation of a family functor with a local analytic isomorphism g, with the image open
named: when g(U') = V, the value of the pulled-back triple on U' is the value on V pulled
back along g|_{U'} : U' → V, with its empty blow-ups deleted.