The one-piece ambient: the inclusion of a smaller open

An open embedding of germs Y_Z ⊂ Y_{Z'} extends to an open embedding U_Z ⊂ U_{Z'} of the ambient opens [Wlo09, §4, (3)⇒(4)]: the ambient of a restricted piece embedding is a smaller open G' ≤ G, and the one-piece ambients Sp(G') → Sp(G) (pieceAmbient) include accordingly. This module builds that inclusion as an analytic map, an open embedding and a local analytic isomorphism (a diffeomorphism onto the coordinate preimage of G'), and the image of an open under it.

• coordPreimage G' G: the points of Sp(G) with coordinates in G';
• pieceAmbientIncl h : AnalyticMap (pieceAmbient 𝕜 G') (pieceAmbient 𝕜 G), with pieceCoord_pieceAmbientIncl (the identity on coordinates), pieceAmbientIncl_injective;
• pieceAmbientInclDiffeo h: the same map as a diffeomorphism onto (pieceAmbient 𝕜 G).restrict (coordPreimage G' G); hence isLocalDiffeomorph_pieceAmbientIncl (a diffeomorphism followed by the inclusion of an open, isLocalDiffeomorph_inclusion);
• pieceAmbientImageOpens h W': the image of an open of Sp(G'), an open of Sp(G) (AnalyticMap.imageOpens of the inclusion), with mem_pieceAmbientImageOpens, pieceAmbientImageOpens_le and isCompact_closure_pieceAmbientImageOpens (relatively compact opens have relatively compact images).

Bookkeeping on the coordinate map pieceCoord (PieceLemma39Model.lean) and on isLocalDiffeomorph_inclusion.

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

The points of the one-piece ambient of G whose coordinates lie in G'.

Equations

• Hironaka.Manifold.coordPreimage G' G = { carrier := Hironaka.Manifold.pieceCoord G ⁻¹' ↑G', is_open' := ⋯ }

theorem Hironaka.Manifold.mem_coordPreimage {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {G' G : TopologicalSpace.Opens (Fin n → 𝕜)} {w : (pieceAmbient 𝕜 G).carrier} : w ∈ coordPreimage G' G ↔ pieceCoord G w ∈ G'

Membership in coordPreimage G' G: the coordinate lies in G'.

def Hironaka.Manifold.pieceAmbientInclFun {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {G' G : TopologicalSpace.Opens (Fin n → 𝕜)} (h : G' ≤ G) : (pieceAmbient 𝕜 G').carrier → (pieceAmbient 𝕜 G).carrier

The inclusion Sp(G') → Sp(G) on points: the same coordinates.

Equations

• Hironaka.Manifold.pieceAmbientInclFun h w = ⟨PUnit.unit, ⟨Hironaka.Manifold.pieceCoord G' w, ⋯⟩⟩

theorem Hironaka.Manifold.pieceCoord_pieceAmbientInclFun {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {G' G : TopologicalSpace.Opens (Fin n → 𝕜)} (h : G' ≤ G) (w : (pieceAmbient 𝕜 G').carrier) : pieceCoord G (pieceAmbientInclFun h w) = pieceCoord G' w

The inclusion of one-piece ambients preserves the coordinate.

theorem Hironaka.Manifold.pieceAmbientInclFun_mem_coordPreimage {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {G' G : TopologicalSpace.Opens (Fin n → 𝕜)} (h : G' ≤ G) (w : (pieceAmbient 𝕜 G').carrier) : pieceAmbientInclFun h w ∈ coordPreimage G' G

The inclusion lands in the preimage open coordPreimage G' G.

theorem Hironaka.Manifold.pieceAmbientInclFun_injective {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {G' G : TopologicalSpace.Opens (Fin n → 𝕜)} (h : G' ≤ G) : Function.Injective (pieceAmbientInclFun h)

The inclusion of one-piece ambients is injective (its coordinate is).

theorem Hironaka.Manifold.contMDiff_pieceAmbientInclFun {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {G' G : TopologicalSpace.Opens (Fin n → 𝕜)} (h : G' ≤ G) : ContMDiff (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ (pieceAmbientInclFun h)

The inclusion is analytic (ContMDiff.sigmaDesc/contMDiff_sigmaMk_comp_iff on the one-point Σ, the coordinate map pieceCoord).

def Hironaka.Manifold.pieceAmbientIncl {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {G' G : TopologicalSpace.Opens (Fin n → 𝕜)} (h : G' ≤ G) : AnalyticMap (pieceAmbient 𝕜 G') (pieceAmbient 𝕜 G)

The inclusion Sp(G') → Sp(G) of one-piece ambients for G' ≤ G (the open embedding U_Z ⊂ U_{Z'} of ambient opens in [Wlo09, §4, (3)⇒(4)]).

Equations

• Hironaka.Manifold.pieceAmbientIncl h = ⟨Hironaka.Manifold.pieceAmbientInclFun h, ⋯⟩

theorem Hironaka.Manifold.pieceAmbientIncl_apply {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {G' G : TopologicalSpace.Opens (Fin n → 𝕜)} (h : G' ≤ G) (w : (pieceAmbient 𝕜 G').carrier) : (pieceAmbientIncl h) w = pieceAmbientInclFun h w

The analytic inclusion Sp(G') → Sp(G) evaluates as pieceAmbientInclFun.

theorem Hironaka.Manifold.pieceCoord_pieceAmbientIncl {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {G' G : TopologicalSpace.Opens (Fin n → 𝕜)} (h : G' ≤ G) (w : (pieceAmbient 𝕜 G').carrier) : pieceCoord G ((pieceAmbientIncl h) w) = pieceCoord G' w

The inclusion Sp(G') → Sp(G) preserves the coordinate.

theorem Hironaka.Manifold.pieceAmbientIncl_injective {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {G' G : TopologicalSpace.Opens (Fin n → 𝕜)} (h : G' ≤ G) : Function.Injective ⇑(pieceAmbientIncl h)

The inclusion Sp(G') → Sp(G) is injective.

def Hironaka.Manifold.pieceAmbientInclInv {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G' G : TopologicalSpace.Opens (Fin n → 𝕜)) : ↥(coordPreimage G' G) → (pieceAmbient 𝕜 G').carrier

The inverse of the inclusion on its image: the same coordinates, read in G'.

Equations

• Hironaka.Manifold.pieceAmbientInclInv G' G v = ⟨PUnit.unit, ⟨Hironaka.Manifold.pieceCoord G ↑v, ⋯⟩⟩

theorem Hironaka.Manifold.contMDiff_pieceAmbientInclInv {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G' G : TopologicalSpace.Opens (Fin n → 𝕜)) : ContMDiff (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ (pieceAmbientInclInv G' G)

The inverse of the inclusion, on coordPreimage G' G, is analytic (a coordinate map).

def Hironaka.Manifold.pieceAmbientInclDiffeo {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {G' G : TopologicalSpace.Opens (Fin n → 𝕜)} (h : G' ≤ G) : Diffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (pieceAmbient 𝕜 G').carrier ((pieceAmbient 𝕜 G).restrict (coordPreimage G' G)).carrier ⊤

The inclusion as a diffeomorphism of Sp(G') onto the coordinate preimage of G' in Sp(G).

Equations

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

theorem Hironaka.Manifold.pieceAmbientInclDiffeo_apply {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {G' G : TopologicalSpace.Opens (Fin n → 𝕜)} (h : G' ≤ G) (w : (pieceAmbient 𝕜 G').carrier) : ↑((pieceAmbientInclDiffeo h) w) = (pieceAmbientIncl h) w

The diffeomorphism onto coordPreimage G' G evaluates as the inclusion.

theorem Hironaka.Manifold.isLocalDiffeomorph_pieceAmbientIncl {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {G' G : TopologicalSpace.Opens (Fin n → 𝕜)} (h : G' ≤ G) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑(pieceAmbientIncl h)

The inclusion is a local analytic isomorphism: the diffeomorphism onto the coordinate preimage followed by the inclusion of that open.

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.pieceAmbientImageOpens {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {G' G : TopologicalSpace.Opens (Fin n → 𝕜)} (h : G' ≤ G) (W' : TopologicalSpace.Opens (pieceAmbient 𝕜 G').carrier) : TopologicalSpace.Opens (pieceAmbient 𝕜 G).carrier

The image of an open of Sp(G') in Sp(G) (AnalyticMap.imageOpens of the inclusion).

Equations

• Hironaka.Manifold.pieceAmbientImageOpens h W' = Hironaka.Manifold.AnalyticMap.imageOpens (Hironaka.Manifold.pieceAmbientIncl h) ⋯ W'

theorem Hironaka.Manifold.mem_pieceAmbientImageOpens {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {G' G : TopologicalSpace.Opens (Fin n → 𝕜)} (h : G' ≤ G) {W' : TopologicalSpace.Opens (pieceAmbient 𝕜 G').carrier} {v : (pieceAmbient 𝕜 G).carrier} : v ∈ pieceAmbientImageOpens h W' ↔ ∃ w ∈ W', (pieceAmbientIncl h) w = v

Membership in the image open: the image of a point of W' under the inclusion.

theorem Hironaka.Manifold.pieceAmbientImageOpens_le {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {G' G : TopologicalSpace.Opens (Fin n → 𝕜)} (h : G' ≤ G) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 G).carrier) (W' : TopologicalSpace.Opens (pieceAmbient 𝕜 G').carrier) (hW' : ∀ w ∈ W', (pieceAmbientIncl h) w ∈ W) : pieceAmbientImageOpens h W' ≤ W

The image of the preimage of W lies in W.

theorem Hironaka.Manifold.isCompact_closure_pieceAmbientImageOpens {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {G' G : TopologicalSpace.Opens (Fin n → 𝕜)} (h : G' ≤ G) (W' : TopologicalSpace.Opens (pieceAmbient 𝕜 G').carrier) (hW' : IsCompact (closure ↑W')) : IsCompact (closure ↑(pieceAmbientImageOpens h W'))

A relatively compact open has a relatively compact image.