The summand-wise coordinate map Θ₀ : ⊔ᵢ Gᵢ' → ⊔ᵢ Sp(Gᵢ)

Kollár presents the local model as the disjoint union X' = ⊔ᵢ Uᵢ of the charts [Kol07, Proposition 37, proof]. The library spells that disjoint union twice: the ambient manifold of the local model of exists_functorial_resolution is a sigmaOpens G' (Σ i, ↥(G' i), the Σ-type of opens G' i ⊆ 𝕜ⁿ), while the order-reduction functor is applied on sigmaManifold (fun i => pieceAmbient 𝕜 (G i)) (Σ i, Σ _ : PUnit, ↥(G i), the disjoint union of the one-piece ambients Sp(Gᵢ)). Given relatively compact opens Wᵢ ⊆ Sp(Gᵢ) on which the functor was applied, this module identifies the sigmaOpens of the coordinate images Gᵢ' := pieceCoord '' Wᵢ with the open U_Σ = ⋃ᵢ sigmaMk i '' Wᵢ of the functor's ambient:

• coordImageOpens G W: the coordinate image pieceCoord G '' W ⊆ 𝕜ⁿ of an open W ⊆ Sp(G), an open of 𝕜ⁿ (pieceCoord is an open map — isOpenMap_pieceCoord, PieceRestrict.lean), with mem_coordImageOpens and coordImageOpens_le;
• sigmaCoordMap G W: Θ₀, the analytic map ⊔ᵢ Gᵢ' → ⊔ᵢ Sp(Gᵢ), ⟨i, z⟩ ↦ ⟨i, ⟨(), z⟩⟩ (sigmaCoordMap_apply); the summand square sigmaCoordMap_mk_of_mem (the point of Gᵢ' with the coordinates of w ∈ Wᵢ goes to w);
• isAnalyticOpenEmbedding_sigmaCoordMap: Θ₀ is an analytic open embedding (a local analytic isomorphism, injective), by IsLocalDiffeomorph.sigmaDesc of the summand maps;
• sigmaCoordImage G W: its image U_Σ (Mathlib's IsLocalDiffeomorph.image), with coe_sigmaCoordImage (= ⋃ᵢ sigmaMk i '' Wᵢ) and isCompact_closure_sigmaCoordImage (a finite union of relatively compact opens).

Internal helpers: pieceAmbientMkDiffeo G, the diffeomorphism ↥G ≃ Sp(G), z ↦ ⟨(), z⟩ (with pieceAmbientMkDiffeo_apply); the summand map sigmaCoordSummand G W i with sigmaCoordSummand_apply, contMDiff_sigmaCoordSummand and isLocalDiffeomorph_sigmaCoordSummand; sigmaCoordMap_injective.

Not in the sources; bookkeeping: Θ₀ is Kollár's identification X' = ⊔ Uᵢ read against the two spellings of the disjoint union (compare [Kol07, Warning 38]). Θ₀ is used in AmbientEmb.lean; its image U_Σ (sigmaCoordImage) also in CoproductSumData.lean, CoproductPadIdentity.lean, CoproductPadIdentityPiece.lean, DoubledDatumLabels.lean and Hironaka/Resolution/Analytic/Kol07Thm45/SigmaSubmanifold.lean.

def Hironaka.Manifold.pieceAmbientMkDiffeo {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) : Diffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (↥G) (pieceAmbient 𝕜 G).carrier ⊤

The one-piece ambient Sp(G) = ⊔_{PUnit} G is the open G ⊆ 𝕜ⁿ itself — the diffeomorphism ↥G ≃ Sp(G), z ↦ ⟨(), z⟩, with inverse the second projection. Internal helper.

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Manifold.pieceAmbientMkDiffeo_apply {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) (z : ↥G) : (pieceAmbientMkDiffeo G) z = ⟨PUnit.unit, z⟩

The diffeomorphism ↥G ≃ Sp(G) on points.

def Hironaka.Manifold.coordImageOpens {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 G).carrier) : TopologicalSpace.Opens (Fin n → 𝕜)

The coordinate image pieceCoord G '' W ⊆ 𝕜ⁿ of an open W of the one-piece ambient Sp(G) = ⊔_{PUnit} G, as an open of 𝕜ⁿ (one of the opens Uᵢ ⊆ 𝕜ⁿ of the disjoint-union presentation, [Kol07, Proposition 37, proof]): the summand Gᵢ' := pieceCoord '' Wᵢ over which the functor's value on Wᵢ is read.

Equations

• Hironaka.Manifold.coordImageOpens G W = { carrier := Hironaka.Manifold.pieceCoord G '' ↑W, is_open' := ⋯ }

theorem Hironaka.Manifold.mem_coordImageOpens {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 G).carrier) (z : Fin n → 𝕜) : z ∈ coordImageOpens G W ↔ ∃ w ∈ W, pieceCoord G w = z

Membership in the coordinate image — a point of W with these coordinates.

theorem Hironaka.Manifold.coordImageOpens_le {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 G).carrier) : coordImageOpens G W ≤ G

The coordinate image lies in G — the coordinates of a point of Sp(G) lie in G (pieceCoord_mem).

noncomputable def Hironaka.Manifold.sigmaCoordSummand {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {ι : Type u} [Finite ι] (G : ι → TopologicalSpace.Opens (Fin n → 𝕜)) (W : (i : ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (G i)).carrier) (i : ι) (z : ↥(coordImageOpens (G i) (W i))) : (Manifold.sigmaManifold fun (i : ι) => pieceAmbient 𝕜 (G i)).carrier

The i-th summand map of Θ₀, Gᵢ' → ⊔ⱼ Sp(Gⱼ), z ↦ ⟨i, ⟨(), z⟩⟩ — the diffeomorphism ↥Gᵢ' ≃ Sp(Gᵢ'), the inclusion Sp(Gᵢ') → Sp(Gᵢ) of one-piece ambients (pieceAmbientIncl, Gᵢ' ≤ Gᵢ), then the summand inclusion sigmaMk i. Internal helper.

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Manifold.sigmaCoordSummand_apply {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {ι : Type u} [Finite ι] (G : ι → TopologicalSpace.Opens (Fin n → 𝕜)) (W : (i : ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (G i)).carrier) (i : ι) (z : ↥(coordImageOpens (G i) (W i))) : sigmaCoordSummand G W i z = (Manifold.sigmaMk (fun (i : ι) => pieceAmbient 𝕜 (G i)) i) ⟨PUnit.unit, ⟨↑z, ⋯⟩⟩

The summand map on points.

theorem Hironaka.Manifold.contMDiff_sigmaCoordSummand {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {ι : Type u} [Finite ι] (G : ι → TopologicalSpace.Opens (Fin n → 𝕜)) (W : (i : ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (G i)).carrier) (i : ι) : ContMDiff (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ (sigmaCoordSummand G W i)

The summand map is analytic — a composite of analytic maps.

theorem Hironaka.Manifold.isLocalDiffeomorph_sigmaCoordSummand {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {ι : Type u} [Finite ι] (G : ι → TopologicalSpace.Opens (Fin n → 𝕜)) (W : (i : ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (G i)).carrier) (i : ι) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ (sigmaCoordSummand G W i)

The summand map is a local analytic isomorphism — a diffeomorphism, then the inclusion of one-piece ambients (isLocalDiffeomorph_pieceAmbientIncl), then the summand inclusion (isLocalDiffeomorph_sigmaMk), composed pointwise (IsLocalDiffeomorphAt.comp).

noncomputable def Hironaka.Manifold.sigmaCoordMap {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {ι : Type u} [Finite ι] (G : ι → TopologicalSpace.Opens (Fin n → 𝕜)) (W : (i : ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (G i)).carrier) : AnalyticMap (AnalyticManifold.sigmaOpens fun (i : ι) => coordImageOpens (G i) (W i)) (Manifold.sigmaManifold fun (i : ι) => pieceAmbient 𝕜 (G i))

Θ₀, the summand-wise coordinate map ⊔ᵢ Gᵢ' → ⊔ᵢ Sp(Gᵢ), ⟨i, z⟩ ↦ ⟨i, ⟨(), z⟩⟩ — from the sigmaOpens of the coordinate images Gᵢ' = pieceCoord '' Wᵢ into the disjoint union of the one-piece ambients: Kollár's identification X' = ⊔ Uᵢ [Kol07, Proposition 37, proof] read against the two spellings of the disjoint union. Analytic by ContMDiff.sigmaDesc of the summand maps.

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Manifold.sigmaCoordMap_apply {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {ι : Type u} [Finite ι] (G : ι → TopologicalSpace.Opens (Fin n → 𝕜)) (W : (i : ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (G i)).carrier) (i : ι) (z : ↥(coordImageOpens (G i) (W i))) : (sigmaCoordMap G W) ⟨i, z⟩ = (Manifold.sigmaMk (fun (i : ι) => pieceAmbient 𝕜 (G i)) i) ⟨PUnit.unit, ⟨↑z, ⋯⟩⟩

Θ₀ on points, ⟨i, z⟩ ↦ ⟨i, ⟨(), z⟩⟩ (the coordinates of z read in Gᵢ, coordImageOpens_le).

theorem Hironaka.Manifold.sigmaCoordMap_mk_of_mem {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {ι : Type u} [Finite ι] (G : ι → TopologicalSpace.Opens (Fin n → 𝕜)) (W : (i : ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (G i)).carrier) (i : ι) (w : (pieceAmbient 𝕜 (G i)).carrier) (hw : w ∈ W i) : (sigmaCoordMap G W) ⟨i, ⟨pieceCoord (G i) w, ⋯⟩⟩ = (Manifold.sigmaMk (fun (i : ι) => pieceAmbient 𝕜 (G i)) i) w

The summand square: the point of Gᵢ' with the coordinates of w ∈ Wᵢ goes to w — a point of Sp(Gᵢ) is determined by its coordinates (Sigma.ext, Subtype.ext).

theorem Hironaka.Manifold.sigmaCoordMap_injective {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {ι : Type u} [Finite ι] (G : ι → TopologicalSpace.Opens (Fin n → 𝕜)) (W : (i : ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (G i)).carrier) : Function.Injective ⇑(sigmaCoordMap G W)

Θ₀ is injective — equal images have the same summand (congrArg Sigma.fst) and, in that summand (sigma_mk_injective), the same coordinates (pieceCoord). Internal helper.

theorem Hironaka.Manifold.isAnalyticOpenEmbedding_sigmaCoordMap {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {ι : Type u} [Finite ι] (G : ι → TopologicalSpace.Opens (Fin n → 𝕜)) (W : (i : ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (G i)).carrier) : Manifold.IsAnalyticOpenEmbedding (sigmaCoordMap G W)

Θ₀ is an analytic open embedding (a local analytic isomorphism, injective): the coproduct of the local analytic isomorphisms of the summands (IsLocalDiffeomorph.sigmaDesc) and sigmaCoordMap_injective.

noncomputable def Hironaka.Manifold.sigmaCoordImage {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {ι : Type u} [Finite ι] (G : ι → TopologicalSpace.Opens (Fin n → 𝕜)) (W : (i : ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (G i)).carrier) : TopologicalSpace.Opens (Manifold.sigmaManifold fun (i : ι) => pieceAmbient 𝕜 (G i)).carrier

U_Σ, the image of Θ₀ (Mathlib's IsLocalDiffeomorph.image, ⟨range Θ₀, _⟩) — the open of ⊔ᵢ Sp(Gᵢ) on which the data of the local model live.

Equations

• Hironaka.Manifold.sigmaCoordImage G W = ⋯.image

theorem Hironaka.Manifold.coe_sigmaCoordImage {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {ι : Type u} [Finite ι] (G : ι → TopologicalSpace.Opens (Fin n → 𝕜)) (W : (i : ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (G i)).carrier) : ↑(sigmaCoordImage G W) = ⋃ (i : ι), ⇑(Manifold.sigmaMk (fun (i : ι) => pieceAmbient 𝕜 (G i)) i) '' ↑(W i)

U_Σ = ⋃ᵢ sigmaMk i '' Wᵢ — a point of the range of Θ₀ is sigmaMk i w for the w ∈ Wᵢ with its coordinates (mem_coordImageOpens), and conversely by the summand square sigmaCoordMap_mk_of_mem.

theorem Hironaka.Manifold.isCompact_closure_sigmaCoordImage {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {ι : Type u} [Finite ι] (G : ι → TopologicalSpace.Opens (Fin n → 𝕜)) (W : (i : ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (G i)).carrier) (hW : ∀ (i : ι), IsCompact (closure ↑(W i))) : IsCompact (closure ↑(sigmaCoordImage G W))

U_Σ is relatively compact when the Wᵢ are — a FINITE union (closure_iUnion_of_finite, isCompact_iUnion) of the images of relatively compact opens under the analytic maps sigmaMk i (AnalyticMap.isCompact_closure_image).