The gluing of the blowing-up: the glued space

The pieces and transition data of Hironaka.Manifold.BlowUp.Glue are fed to Mathlib's TopCat.GlueData.mk' (gluing data given by elements and intersections): the pieces, lifted to the universe of M, are the objects, the transition domains the open subsets, the transition maps the transition homeomorphisms; the identity, inverse and cocycle laws are those proved there. The glued space Glued ψ Y c carries the inclusions toGlued j of the pieces, open embeddings that are jointly surjective, and two points of pieces are identified exactly when the transition map carries one to the other (toGlued_eq_iff). The blow-down gluedProj : Glued ψ Y c → M is defined piecewise and is continuous.

This is the topological space underlying the blowing-up of M with centre Y [BM88, Definition 4.1]; its structure of analytic manifold is the subject of Hironaka.Manifold.BlowUp.GluedCharts.

The gluing data

@[reducible, inline]

abbrev Manifold.BlowUpGlue.pieceSpace {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (j : PieceIdx ψ Y c) : TopCat

A piece as a topological space in the universe of M.

Equations

• Manifold.BlowUpGlue.pieceSpace j = ↧(ULift.{?u.2, 0} ↑(Manifold.BlowUpGlue.pieceSet j))

def Manifold.BlowUpGlue.transOpens {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (j j' : PieceIdx ψ Y c) : TopologicalSpace.Opens ↑(pieceSpace j)

The transition domain as an open subset of the piece.

Equations

• Manifold.BlowUpGlue.transOpens j j' = { carrier := {x : ↑(Manifold.BlowUpGlue.pieceSpace j) | ↑x.down ∈ Manifold.BlowUpGlue.transDom j j'}, is_open' := ⋯ }

theorem Manifold.BlowUpGlue.mem_transOpens_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {j j' : PieceIdx ψ Y c} {x : ↑(pieceSpace j)} : x ∈ transOpens j j' ↔ ↑x.down ∈ transDom j j'

Membership in the transition open of a piece space, unfolded.

noncomputable def Manifold.BlowUpGlue.transHom {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (j j' : PieceIdx ψ Y c) : (TopologicalSpace.Opens.toTopCat (pieceSpace j)).obj (transOpens j j') ⟶ (TopologicalSpace.Opens.toTopCat (pieceSpace j')).obj (transOpens j' j)

The transition homeomorphism between the transition domains.

Equations

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

theorem Manifold.BlowUpGlue.transHom_apply_coe {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (j j' : PieceIdx ψ Y c) (x : ↑((TopologicalSpace.Opens.toTopCat (pieceSpace j)).obj (transOpens j j'))) : ↑(↑((CategoryTheory.ConcreteCategory.hom (transHom j j')) x)).down = transMap j j' ↑(↑x).down

The transition homeomorphism of the gluing data acts by the transition map.

noncomputable def Manifold.BlowUpGlue.glueCore {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (Y : Set M) (c : ℕ) : TopCat.GlueData.MkCore

The gluing data of the blowing-up, in the element-wise form TopCat.GlueData.MkCore.

Equations

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

noncomputable def Manifold.BlowUpGlue.glueData {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (Y : Set M) (c : ℕ) : TopCat.GlueData

The glue data of the blowing-up.

Equations

• Manifold.BlowUpGlue.glueData ψ Y c = TopCat.GlueData.mk' (Manifold.BlowUpGlue.glueCore ψ Y c)

@[reducible, inline]

abbrev Manifold.BlowUpGlue.Glued {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (Y : Set M) (c : ℕ) : Type u

The glued space: the blowing-up of M with centre Y as a topological space.

Equations

• Manifold.BlowUpGlue.Glued ψ Y c = ↑(Manifold.BlowUpGlue.glueData ψ Y c).glued

noncomputable def Manifold.BlowUpGlue.toGlued {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (j : PieceIdx ψ Y c) (u : ↑(pieceSet j)) : Glued ψ Y c

The inclusion of a piece into the glued space.

Equations

• Manifold.BlowUpGlue.toGlued j u = (CategoryTheory.ConcreteCategory.hom ((Manifold.BlowUpGlue.glueData ψ Y c).ι j)) { down := u }

theorem Manifold.BlowUpGlue.continuous_toGlued {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (j : PieceIdx ψ Y c) : Continuous (toGlued j)

The inclusion of a piece into the glued space is continuous.

theorem Manifold.BlowUpGlue.isOpenEmbedding_toGlued {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (j : PieceIdx ψ Y c) : Topology.IsOpenEmbedding (toGlued j)

The inclusion of a piece into the glued space is an open embedding.

theorem Manifold.BlowUpGlue.toGlued_jointly_surjective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (p : Glued ψ Y c) : ∃ (j : PieceIdx ψ Y c) (u : ↑(pieceSet j)), toGlued j u = p

The pieces cover the glued space.

theorem Manifold.BlowUpGlue.isOpen_glued_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (s : Set (Glued ψ Y c)) : IsOpen s ↔ ∀ (j : PieceIdx ψ Y c), IsOpen (toGlued j ⁻¹' s)

A set in the glued space is open iff its preimage in every piece is open.

theorem Manifold.BlowUpGlue.ι_eq_iff_rel' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (j j' : PieceIdx ψ Y c) (x : ↑(pieceSpace j)) (y : ↑(pieceSpace j')) : (CategoryTheory.ConcreteCategory.hom ((glueData ψ Y c).ι j)) x = (CategoryTheory.ConcreteCategory.hom ((glueData ψ Y c).ι j')) y ↔ (glueData ψ Y c).Rel ⟨j, x⟩ ⟨j', y⟩

Two points of two pieces are identified in the glued space iff they are related by the gluing relation (Mathlib's ι_eq_iff_rel with the piece indices made explicit).

theorem Manifold.BlowUpGlue.toGlued_eq_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {j j' : PieceIdx ψ Y c} {u : ↑(pieceSet j)} {u' : ↑(pieceSet j')} : toGlued j u = toGlued j' u' ↔ ∃ (_ : ↑u ∈ transDom j j'), transMap j j' ↑u = ↑u'

Two points of pieces are identified in the glued space exactly when the transition map carries one to the other.

theorem Manifold.BlowUpGlue.toGlued_injective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (j : PieceIdx ψ Y c) : Function.Injective (toGlued j)

The inclusion of a piece into the glued space is injective.

theorem Manifold.BlowUpGlue.toGlued_transMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {j j' : PieceIdx ψ Y c} {u : ↑(pieceSet j)} (hu : ↑u ∈ transDom j j') : toGlued j' ⟨transMap j j' ↑u, ⋯⟩ = toGlued j u

The transition map is compatible with the inclusions: a point and its transition are identified in the glued space.

theorem Manifold.BlowUpGlue.toGlued_mem_range_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {j j' : PieceIdx ψ Y c} {u : ↑(pieceSet j)} : toGlued j u ∈ Set.range (toGlued j') ↔ ↑u ∈ transDom j j'

A point of a piece lies in the image of another piece exactly when it lies in the transition domain.

The blow-down of the glued space

noncomputable def Manifold.BlowUpGlue.pieceOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (p : Glued ψ Y c) : PieceIdx ψ Y c

A piece containing the point p.

Equations

• Manifold.BlowUpGlue.pieceOf p = ⋯.choose

noncomputable def Manifold.BlowUpGlue.pieceElt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (p : Glued ψ Y c) : ↑(pieceSet (pieceOf p))

The coordinates of p in the piece pieceOf p.

Equations

• Manifold.BlowUpGlue.pieceElt p = ⋯.choose

theorem Manifold.BlowUpGlue.toGlued_pieceElt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (p : Glued ψ Y c) : toGlued (pieceOf p) (pieceElt p) = p

Every point of the glued space is the inclusion of its chosen piece element.

noncomputable def Manifold.BlowUpGlue.gluedProj {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (p : Glued ψ Y c) : M

The blow-down π : M' → M of the glued space, defined piecewise.

Equations

• Manifold.BlowUpGlue.gluedProj p = Manifold.BlowUpGlue.blowDown (Manifold.BlowUpGlue.pieceOf p) ↑(Manifold.BlowUpGlue.pieceElt p)

theorem Manifold.BlowUpGlue.gluedProj_toGlued {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (j : PieceIdx ψ Y c) (u : ↑(pieceSet j)) : gluedProj (toGlued j u) = blowDown j ↑u

The blow-down of the glued space restricts to the blow-down of each piece.

theorem Manifold.BlowUpGlue.continuous_gluedProj {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} : Continuous gluedProj

The blow-down of the glued space is continuous.

theorem Manifold.BlowUpGlue.gluedProj_mem_source {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (j : PieceIdx ψ Y c) (u : ↑(pieceSet j)) : gluedProj (toGlued j u) ∈ (pieceChart j).source

The blow-down of a point of piece j lies in the source of the piece's chart.