Fibre products of local covers: the closed embedding (p₁, p₂), restriction to opens

The proof of [Kol07, Proposition 37] compares the two pull-backs of a blow-up sequence to X'' := ∐_{i ≤ j} Uᵢ ∩ Uⱼ, the fibre product of the cover with itself (IsFibreProduct). For the family functors the values live on relatively compact opens, so the comparison must be run on a relatively compact open of the fibre product: for a fibre product (P, p₁, p₂) of g₁ : N₁ → M with a coproduct of open embeddings g₂ : N₂ → M, the joint map (p₁, p₂) : P → N₁ × N₂ is a closed embedding onto the set-theoretic fibre product (IsFibreProduct.isClosedEmbedding_prodMk), so the open p₁⁻¹(O₁) ∩ p₂⁻¹(O₂) over relatively compact opens O₁, O₂ has compact closure (isCompact_closure_restrictOpens), and the restricted projections form a fibre product of the restricted maps g₁|_{O₁}, g₂|_{O₂} : Oᵢ → V (isFibreProduct_restrict; AnalyticMap.restrictMap). These are the tools of the globalization of family functors.

theorem Manifold.IsFibreProduct.injective_prodMk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N₁ N₂ P : AnalyticManifold 𝕜 E} {g₁ : AnalyticMap N₁ M} {g₂ : AnalyticMap N₂ M} {p₁ : AnalyticMap P N₁} {p₂ : AnalyticMap P N₂} (hp : IsFibreProduct g₁ g₂ p₁ p₂) : Function.Injective fun (z : P.carrier) => (p₁ z, p₂ z)

The joint map (p₁, p₂) is injective (the uniqueness clause of the fibre product).

theorem Manifold.IsFibreProduct.range_prodMk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N₁ N₂ P : AnalyticManifold 𝕜 E} {g₁ : AnalyticMap N₁ M} {g₂ : AnalyticMap N₂ M} {p₁ : AnalyticMap P N₁} {p₂ : AnalyticMap P N₂} (hp : IsFibreProduct g₁ g₂ p₁ p₂) : (Set.range fun (z : P.carrier) => (p₁ z, p₂ z)) = {xy : N₁.carrier × N₂.carrier | g₁ xy.1 = g₂ xy.2}

The range of (p₁, p₂) is the set-theoretic fibre product.

theorem Manifold.IsFibreProduct.isClosed_range_prodMk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N₁ N₂ P : AnalyticManifold 𝕜 E} {g₁ : AnalyticMap N₁ M} {g₂ : AnalyticMap N₂ M} {p₁ : AnalyticMap P N₁} {p₂ : AnalyticMap P N₂} (hp : IsFibreProduct g₁ g₂ p₁ p₂) : IsClosed (Set.range fun (z : P.carrier) => (p₁ z, p₂ z))

theorem Manifold.IsFibreProduct.continuous_prodMk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N₁ N₂ P : AnalyticManifold 𝕜 E} {p₁ : AnalyticMap P N₁} {p₂ : AnalyticMap P N₂} : Continuous fun (z : P.carrier) => (p₁ z, p₂ z)

theorem Manifold.IsFibreProduct.isInducing_prodMk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N₁ N₂ P : AnalyticManifold 𝕜 E} {g₁ : AnalyticMap N₁ M} {g₂ : AnalyticMap N₂ M} {p₁ : AnalyticMap P N₁} {p₂ : AnalyticMap P N₂} (hp : IsFibreProduct g₁ g₂ p₁ p₂) (hg₂ : IsCoprodOfOpenEmbeddings g₂) : Topology.IsInducing fun (z : P.carrier) => (p₁ z, p₂ z)

(p₁, p₂) is inducing when g₂ is a coproduct of open embeddings: near z, a point w with p₁ w in a small image p₁(Z₀) and p₂ w in the clopen piece of p₂ z equals the point of Z₀ over p₁ w, by the injectivity of p₁ on p₂⁻¹ of a piece (injOn_fst).

theorem Manifold.IsFibreProduct.isClosedEmbedding_prodMk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N₁ N₂ P : AnalyticManifold 𝕜 E} {g₁ : AnalyticMap N₁ M} {g₂ : AnalyticMap N₂ M} {p₁ : AnalyticMap P N₁} {p₂ : AnalyticMap P N₂} (hp : IsFibreProduct g₁ g₂ p₁ p₂) (hg₂ : IsCoprodOfOpenEmbeddings g₂) : Topology.IsClosedEmbedding fun (z : P.carrier) => (p₁ z, p₂ z)

[Kol07, Proposition 37] at the family level, the topological core: (p₁, p₂) is a closed embedding when g₂ is a coproduct of open embeddings.

def Manifold.IsFibreProduct.restrictOpens {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N₁ N₂ P : AnalyticManifold 𝕜 E} (p₁ : AnalyticMap P N₁) (p₂ : AnalyticMap P N₂) (O₁ : TopologicalSpace.Opens N₁.carrier) (O₂ : TopologicalSpace.Opens N₂.carrier) : TopologicalSpace.Opens P.carrier

The open p₁⁻¹(O₁) ∩ p₂⁻¹(O₂) of the fibre product over opens O₁ ⊆ N₁, O₂ ⊆ N₂.

Equations

• Manifold.IsFibreProduct.restrictOpens p₁ p₂ O₁ O₂ = { carrier := ⇑p₁ ⁻¹' ↑O₁ ∩ ⇑p₂ ⁻¹' ↑O₂, is_open' := ⋯ }

theorem Manifold.IsFibreProduct.mem_restrictOpens {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N₁ N₂ P : AnalyticManifold 𝕜 E} {p₁ : AnalyticMap P N₁} {p₂ : AnalyticMap P N₂} {O₁ : TopologicalSpace.Opens N₁.carrier} {O₂ : TopologicalSpace.Opens N₂.carrier} {z : P.carrier} : z ∈ ↑(restrictOpens p₁ p₂ O₁ O₂) ↔ p₁ z ∈ ↑O₁ ∧ p₂ z ∈ ↑O₂

theorem Manifold.IsFibreProduct.image_fst_restrictOpens {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N₁ N₂ P : AnalyticManifold 𝕜 E} {p₁ : AnalyticMap P N₁} {p₂ : AnalyticMap P N₂} (O₁ : TopologicalSpace.Opens N₁.carrier) (O₂ : TopologicalSpace.Opens N₂.carrier) : ⇑p₁ '' ↑(restrictOpens p₁ p₂ O₁ O₂) ⊆ ↑O₁

theorem Manifold.IsFibreProduct.image_snd_restrictOpens {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N₁ N₂ P : AnalyticManifold 𝕜 E} {p₁ : AnalyticMap P N₁} {p₂ : AnalyticMap P N₂} (O₁ : TopologicalSpace.Opens N₁.carrier) (O₂ : TopologicalSpace.Opens N₂.carrier) : ⇑p₂ '' ↑(restrictOpens p₁ p₂ O₁ O₂) ⊆ ↑O₂

theorem Manifold.IsFibreProduct.image_fst_restrictOpens_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N₁ N₂ P : AnalyticManifold 𝕜 E} {g₁ : AnalyticMap N₁ M} {g₂ : AnalyticMap N₂ M} {p₁ : AnalyticMap P N₁} {p₂ : AnalyticMap P N₂} (hp : IsFibreProduct g₁ g₂ p₁ p₂) {O₁ : TopologicalSpace.Opens N₁.carrier} {O₂ : TopologicalSpace.Opens N₂.carrier} (h : ⇑g₁ '' ↑O₁ ⊆ ⇑g₂ '' ↑O₂) : ⇑p₁ '' ↑(restrictOpens p₁ p₂ O₁ O₂) = ↑O₁

The first projection maps p₁⁻¹(O₁) ∩ p₂⁻¹(O₂) onto O₁ when g₁(O₁) ⊆ g₂(O₂).

theorem Manifold.IsFibreProduct.image_snd_restrictOpens_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N₁ N₂ P : AnalyticManifold 𝕜 E} {g₁ : AnalyticMap N₁ M} {g₂ : AnalyticMap N₂ M} {p₁ : AnalyticMap P N₁} {p₂ : AnalyticMap P N₂} (hp : IsFibreProduct g₁ g₂ p₁ p₂) {O₁ : TopologicalSpace.Opens N₁.carrier} {O₂ : TopologicalSpace.Opens N₂.carrier} (h : ⇑g₂ '' ↑O₂ ⊆ ⇑g₁ '' ↑O₁) : ⇑p₂ '' ↑(restrictOpens p₁ p₂ O₁ O₂) = ↑O₂

The second projection maps p₁⁻¹(O₁) ∩ p₂⁻¹(O₂) onto O₂ when g₂(O₂) ⊆ g₁(O₁).

theorem Manifold.IsFibreProduct.isFibreProduct_restrict {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N₁ N₂ P : AnalyticManifold 𝕜 E} {g₁ : AnalyticMap N₁ M} {g₂ : AnalyticMap N₂ M} {p₁ : AnalyticMap P N₁} {p₂ : AnalyticMap P N₂} (hp : IsFibreProduct g₁ g₂ p₁ p₂) (O₁ : TopologicalSpace.Opens N₁.carrier) (O₂ : TopologicalSpace.Opens N₂.carrier) (V : TopologicalSpace.Opens M.carrier) (h₁ : ⇑g₁ '' ↑O₁ ⊆ ↑V) (h₂ : ⇑g₂ '' ↑O₂ ⊆ ↑V) : IsFibreProduct (Hironaka.Manifold.AnalyticMap.restrictMap g₁ O₁ V h₁) (Hironaka.Manifold.AnalyticMap.restrictMap g₂ O₂ V h₂) (Hironaka.Manifold.AnalyticMap.restrictMap p₁ (restrictOpens p₁ p₂ O₁ O₂) O₁ ⋯) (Hironaka.Manifold.AnalyticMap.restrictMap p₂ (restrictOpens p₁ p₂ O₁ O₂) O₂ ⋯)

The restriction of a fibre product to opens O₁ ⊆ N₁, O₂ ⊆ N₂ mapping into V ⊆ M is a fibre product of the restricted maps g₁|_{O₁}, g₂|_{O₂} : Oᵢ → V.

theorem Manifold.IsFibreProduct.isCompact_closure_restrictOpens {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N₁ N₂ P : AnalyticManifold 𝕜 E} {g₁ : AnalyticMap N₁ M} {g₂ : AnalyticMap N₂ M} {p₁ : AnalyticMap P N₁} {p₂ : AnalyticMap P N₂} (hp : IsFibreProduct g₁ g₂ p₁ p₂) (hg₂ : IsCoprodOfOpenEmbeddings g₂) {O₁ : TopologicalSpace.Opens N₁.carrier} (hO₁ : IsCompact (closure ↑O₁)) {O₂ : TopologicalSpace.Opens N₂.carrier} (hO₂ : IsCompact (closure ↑O₂)) : IsCompact (closure ↑(restrictOpens p₁ p₂ O₁ O₂))

Relative compactness descends to the fibre product: the closure of p₁⁻¹(O₁) ∩ p₂⁻¹(O₂) lies in the preimage of the compact closure O₁ × closure O₂ under the closed embedding (p₁, p₂).