The chaining of the closed-embedding commutation, II: the flag cover

[Kol07, 108] reduces the commutation with closed embeddings to the hypersurface case along a chain of smooth subvarieties Y = Y₀ ⊂ Y₁ ⊂ ⋯ ⊂ Y_c = X, each a hypersurface in the next, the identity being a local question on X. On analytic manifolds the per-open identity of the predicate CommutesWithClosedEmbeddingsOfEmptyDivisorFam is read on a relatively compact open U, so only the compact closure U has to be covered (compare [BM97, Theorem 1.6] and the remark following it on relatively compact opens), and a closed submanifold S of codimension s + 1 is, on the source of each of its adapted charts, the bottom of a flag S ∩ W ⊂ Y ⊂ W with Y the zero set of the first s normal coordinates (IsAdaptedChart.exists_flag). This module builds the cover:

• FlagPiece hS W: an open W with a closed submanifold Y of the open submanifold W of codimension s containing the trace of S, of which the trace is a hypersurface; exists_flagPiece_of_adaptedChart (the source of an adapted chart, through the chart transported to the open submanifold, where its source is the whole manifold) and FlagPiece.compl (the complement M ∖ S with Y = ∅);
• FlagCover hS U: finitely many pieces Wᵢ with shrunk opens Vᵢ ⋐ Wᵢ (compact closures inside the pieces) covering closure U; exists_flagCover by compactness, as exists_finite_shrunk_mcCover (Hironaka.Resolution.Analytic.OrderReduction.GlobalizeFamCover);
• the coproduct FlagCover.sigma = ⨆ᵢ Wᵢ of the pieces with the cover map desc, the open opens = ⨆ᵢ (Vᵢ ∩ U) with compact closure and image U, and the restricted cover map coverMap : sigma.restrict opens → M.restrict U, a surjective local analytic isomorphism — all read off the shrunk embedding cover FlagCover.toCover (ShrunkEmbeddingCover, shared with ShrunkMCCover);
• the flag on the coproduct: flag = ⋃ᵢ sigmaMk i '' Yᵢ is a closed submanifold of codimension s (IsClosedSubmanifold.iUnion_image) containing the preimage of S, of which that preimage is a hypersurface (preimage_val_of_subset at codimension s + 1 - s = 1).

The chaining lemma (Hironaka.Resolution.Analytic.Functor.ChainClosedEmbeddingChain) pulls the two sides of the identity on U back along the cover map, where the flag exists, and descends by the injectivity of the pull-back along a surjective local isomorphism (BlowUpSequence.pullback_injective_of_surjective).

Flag pieces

structure Hironaka.Manifold.FlagPiece {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S (s + 1)) (W : TopologicalSpace.Opens M.carrier) : Type u

A flag piece for S (codimension s + 1) on the open W — a closed submanifold Y of the open submanifold W of codimension s containing the trace of S, of which the trace is a hypersurface.

• Y : Set (M.restrict W).carrier

  The middle member of the flag on the piece.

• hY : Manifold.IsClosedSubmanifold ψ self.Y s

  Y is a closed submanifold of codimension s.

• subset : ⇑(M.inclusion W) ⁻¹' S ⊆ self.Y

  The trace of S lies in Y.

• hSY : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⇑⋯.inclusionMap ⁻¹' ⇑(M.inclusion W) ⁻¹' S) 1

  The trace of S is a hypersurface of the bundled Y.

theorem Hironaka.Manifold.FlagPiece.isClosedSubmanifold_trace {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S (s + 1)) (W : TopologicalSpace.Opens M.carrier) : Manifold.IsClosedSubmanifold ψ (⇑(M.inclusion W) ⁻¹' S) (s + 1)

The trace of S on a piece is a closed submanifold of codimension s + 1 (restrictOpen).

theorem Hironaka.Manifold.exists_flagPiece_of_adaptedChart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S (s + 1)) {φ : OpenPartialHomeomorph M.carrier E} {σ : Fin (s + 1) ↪ Fin n} (hφ : Manifold.IsAdaptedChart ψ S φ σ) {a : M.carrier} (ha : a ∈ φ.source) : Nonempty (FlagPiece hS { carrier := φ.source, is_open' := ⋯ })

The flag piece on the source of an adapted chart of S: the chart transported to the open submanifold φ.source (transportChart along the inverse of the inclusion, as IsClosedSubmanifoldOn.restrict) is an adapted chart of the trace whose source is the whole manifold, and IsAdaptedChart.exists_flag gives the flag.

def Hironaka.Manifold.FlagPiece.compl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S (s + 1)) : FlagPiece hS { carrier := Sᶜ, is_open' := ⋯ }

The flag piece on the complement of S — the empty middle member (isClosedSubmanifold_empty').

Equations

• Hironaka.Manifold.FlagPiece.compl hS = { Y := ∅, hY := ⋯, subset := ⋯, hSY := ⋯ }

The finite shrunk flag cover of a relatively compact open

structure Hironaka.Manifold.FlagCover {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S (s + 1)) (U : TopologicalSpace.Opens M.carrier) : Type (u + 1)

A flag cover of the relatively compact open U — finitely many flag pieces Wᵢ with shrunk opens Vᵢ (compact closures inside the Wᵢ) covering closure U.

• ι : Type u

  The (finite) index type of the pieces.

• finite : Finite self.ι
• W : self.ι → TopologicalSpace.Opens M.carrier

  The pieces.

• piece (i : self.ι) : FlagPiece hS (self.W i)

  The flag on each piece.

• V : self.ι → TopologicalSpace.Opens M.carrier

  The shrunk opens.

• hVc (i : self.ι) : IsCompact (closure ↑(self.V i))

  The shrunk opens have compact closures.

• hVW (i : self.ι) : closure ↑(self.V i) ⊆ ↑(self.W i)

  The closures of the shrunk opens lie in the pieces.

• hcov : closure ↑U ⊆ ⋃ (i : self.ι), ↑(self.V i)

  The shrunk opens cover closure U.

theorem Hironaka.Manifold.exists_flagCover {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S (s + 1)) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : Nonempty (FlagCover hS U)

Every relatively compact open has a flag cover — at a point of S the source of an adapted chart (exists_flagPiece_of_adaptedChart), off S the complement (FlagPiece.compl); a compact neighbourhood inside the piece (exists_compact_subset, the manifold being locally compact); finitely many by the compactness of closure U.

The coproduct of the pieces and its cover map

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.FlagCover.N {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) (i : C.ι) : AnalyticManifold 𝕜 E

The pieces as open submanifolds.

Equations

• C.N i = M.restrict (C.W i)

@[reducible, inline]

abbrev Hironaka.Manifold.FlagCover.incl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) (i : C.ι) : AnalyticMap (C.N i) M

The inclusions of the pieces.

Equations

• C.incl i = M.inclusion (C.W i)

theorem Hironaka.Manifold.FlagCover.isAnalyticOpenEmbedding_incl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) (i : C.ι) : Manifold.IsAnalyticOpenEmbedding (C.incl i)

theorem Hironaka.Manifold.FlagCover.range_incl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) (i : C.ι) : Set.range ⇑(C.incl i) = ↑(C.W i)

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.FlagCover.toCover {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) : ShrunkEmbeddingCover M U

The flag cover as a shrunk embedding cover (ShrunkEmbeddingCover): the pieces embedded by their inclusions, the shrunk opens inside their ranges. The coproduct, the open ⨆ᵢ (Vᵢ ∩ U) and the cover map below are those of this cover.

Equations

• C.toCover = { ι := C.ι, finite := ⋯, N := C.N, incl := C.incl, isAnalyticOpenEmbedding_incl := ⋯, V := C.V, hVc := ⋯, hVr := ⋯, hcov := ⋯ }

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.FlagCover.sigma {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) : AnalyticManifold 𝕜 E

The coproduct ⨆ᵢ Wᵢ of the pieces.

Equations

• C.sigma = C.toCover.sigma

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.FlagCover.desc {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) : AnalyticMap C.sigma M

The cover map ⨆ᵢ Wᵢ → M.

Equations

• C.desc = C.toCover.desc

theorem Hironaka.Manifold.FlagCover.isLocalDiffeomorph_desc {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑C.desc

theorem Hironaka.Manifold.FlagCover.desc_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) (p : C.sigma.carrier) : C.desc p = ↑p.snd

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.FlagCover.opens {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) : TopologicalSpace.Opens C.sigma.carrier

The open ⨆ᵢ (Vᵢ ∩ U) of the coproduct.

Equations

• C.opens = C.toCover.opens

theorem Hironaka.Manifold.FlagCover.mem_opens {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) (p : C.sigma.carrier) : p ∈ ↑C.opens ↔ (C.incl p.fst) p.snd ∈ ↑(C.V p.fst) ∩ ↑U

@[reducible, inline]

abbrev Hironaka.Manifold.FlagCover.closedHull {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) : Set C.sigma.carrier

The closed set ⨆ᵢ ιᵢ⁻¹(closure Vᵢ) containing the closure of opens.

Equations

• C.closedHull = C.toCover.closedHull

theorem Hironaka.Manifold.FlagCover.isClosed_closedHull {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) : IsClosed C.closedHull

theorem Hironaka.Manifold.FlagCover.closedHull_eq_iUnion {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) : C.closedHull = ⋃ (i : C.ι), ⇑(Manifold.sigmaMk C.N i) '' ⇑(C.incl i) ⁻¹' closure ↑(C.V i)

theorem Hironaka.Manifold.FlagCover.isCompact_closedHull {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) : IsCompact C.closedHull

theorem Hironaka.Manifold.FlagCover.closure_opens_subset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) : closure ↑C.opens ⊆ C.closedHull

theorem Hironaka.Manifold.FlagCover.isCompact_closure_opens {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) : IsCompact (closure ↑C.opens)

The open ⨆ᵢ (Vᵢ ∩ U) has compact closure.

theorem Hironaka.Manifold.FlagCover.image_opens_subset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) : ⇑C.desc '' ↑C.opens ⊆ ↑U

theorem Hironaka.Manifold.FlagCover.image_opens_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) : ⇑C.desc '' ↑C.opens = ↑U

The cover map sends ⨆ᵢ (Vᵢ ∩ U) onto U (the Vᵢ cover closure U ⊇ U).

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.FlagCover.coverMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) : AnalyticMap (C.sigma.restrict C.opens) (M.restrict U)

The cover map ⨆ᵢ (Vᵢ ∩ U) → U (Kollár's g : X^* → X over U).

Equations

• C.coverMap = C.toCover.coverMap

theorem Hironaka.Manifold.FlagCover.isLocalDiffeomorph_coverMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑C.coverMap

theorem Hironaka.Manifold.FlagCover.surjective_coverMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) : Function.Surjective ⇑C.coverMap

The flag on the coproduct

theorem Hironaka.Manifold.FlagCover.pairwise_disjoint_range_sigmaMk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) : Pairwise fun (i j : C.ι) => Disjoint (Set.range ⇑(Manifold.sigmaMk C.N i)) (Set.range ⇑(Manifold.sigmaMk C.N j))

theorem Hironaka.Manifold.FlagCover.iUnion_range_sigmaMk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) : ⋃ (i : C.ι), Set.range ⇑(Manifold.sigmaMk C.N i) = Set.univ

theorem Hironaka.Manifold.FlagCover.isClosedSubmanifold_preimage {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) : Manifold.IsClosedSubmanifold ψ (⇑C.desc ⁻¹' S) (s + 1)

The preimage of S in the coproduct, a closed submanifold of codimension s + 1 (preimage_of_isLocalDiffeomorph).

def Hironaka.Manifold.FlagCover.flag {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) : Set C.sigma.carrier

The flag ⋃ᵢ sigmaMk i '' Yᵢ on the coproduct (Y_N).

Equations

• C.flag = ⋃ (i : C.ι), ⇑(Manifold.sigmaMk C.N i) '' (C.piece i).Y

theorem Hironaka.Manifold.FlagCover.isClosedSubmanifold_flag {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) : Manifold.IsClosedSubmanifold ψ C.flag s

The flag is a closed submanifold of codimension s (IsClosedSubmanifold.iUnion_image).

theorem Hironaka.Manifold.FlagCover.preimage_subset_flag {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) : ⇑C.desc ⁻¹' S ⊆ C.flag

theorem Hironaka.Manifold.FlagCover.isClosedSubmanifold_preimage_flag {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} {hS : Manifold.IsClosedSubmanifold ψ S (s + 1)} {U : TopologicalSpace.Opens M.carrier} (C : FlagCover hS U) : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⇑⋯.inclusionMap ⁻¹' ⇑C.desc ⁻¹' S) 1

The preimage of S is a hypersurface of the bundled flag (preimage_val_of_subset at codimension s + 1 - s = 1).