The gluing of the blowing-up: pieces and transition maps

The blowing-up M' of M with centre Y is obtained by gluing the local blowings-up π⁻¹(U) = V' × W over the adapted charts φ : U → V × W [BM88, Definition 4.1]. Here the pieces are indexed by an adapted chart (φ, σ) of Y (shrunk to the universe of M) together with a chart index i < c: the piece is the chart domain S = π_i⁻¹(ψ(φ(U))) of the local model (blowUpChartMap), and its blow-down is β = φ⁻¹ ∘ ψ⁻¹ ∘ π_i : S → U. Two pieces (φ, σ, i) and (φ', σ', i') are glued along the transition domain {u ∈ S | β u ∈ U' ∧ D_{i'}(u) ≠ 0} by the transition map, the lift (Hironaka.Manifold.BlowUp.Lift) of the coordinate change ψ ∘ φ' ∘ φ⁻¹ ∘ ψ⁻¹ from chart i to chart i'. The transition maps commute with the blow-downs, are the identity on a piece with itself, and satisfy the inverse and cocycle laws, every law being an instance of the uniqueness of lifts (two continuous lifts of the same coordinate change through the same chart agree, by density of the complement of the exceptional hyperplane) or of the cocycle of the direction quotients.

This file builds the pieces, the transition data and their laws; Hironaka.Manifold.BlowUp.Glued feeds them to TopCat.GlueData.mk'. The gluing is not carried out in the source, which states the result.

The pieces

@[reducible, inline]

abbrev Manifold.BlowUpGlue.AdaptedChart {𝕜 : 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 (max u u_1)

The adapted charts of Y with their block embeddings.

Equations

• Manifold.BlowUpGlue.AdaptedChart ψ Y c = { x : OpenPartialHomeomorph M E × (Fin c ↪ Fin n) // Manifold.IsAdaptedChart ψ Y x.1 x.2 }

instance Manifold.BlowUpGlue.small_adaptedChart {𝕜 : 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 : ℕ) : Small.{u, max u_1 u} (AdaptedChart ψ Y c)

The adapted charts form a small type in the universe of M: a chart is determined by its map, its inverse and its source, and E ≃ Kⁿ.

@[reducible, inline]

abbrev Manifold.BlowUpGlue.PieceIdx {𝕜 : 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 index type of the pieces: an adapted chart (shrunk to the universe of M) and a chart index i < c.

Equations

• Manifold.BlowUpGlue.PieceIdx ψ Y c = (Shrink.{?u.2, max ?u.1 ?u.2} (Manifold.BlowUpGlue.AdaptedChart ψ Y c) × Fin c)

noncomputable def Manifold.BlowUpGlue.pieceData {𝕜 : 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) : AdaptedChart ψ Y c

The adapted chart of a piece.

Equations

• Manifold.BlowUpGlue.pieceData j = (equivShrink (Manifold.BlowUpGlue.AdaptedChart ψ Y c)).symm j.1

noncomputable def Manifold.BlowUpGlue.pieceChart {𝕜 : 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) : OpenPartialHomeomorph M E

The chart of a piece.

Equations

• Manifold.BlowUpGlue.pieceChart j = (↑(Manifold.BlowUpGlue.pieceData j)).1

noncomputable def Manifold.BlowUpGlue.pieceEmb {𝕜 : 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) : Fin c ↪ Fin n

The block embedding of a piece.

Equations

• Manifold.BlowUpGlue.pieceEmb j = (↑(Manifold.BlowUpGlue.pieceData j)).2

theorem Manifold.BlowUpGlue.isAdaptedChart_piece {𝕜 : 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) : IsAdaptedChart ψ Y (pieceChart j) (pieceEmb j)

The chart of a piece is adapted to Y, with the piece's block indices.

theorem Manifold.BlowUpGlue.mem_maximalAtlas_piece {𝕜 : 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) : pieceChart j ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M

The chart of a piece lies in the maximal atlas of M.

theorem Manifold.BlowUpGlue.exists_piece {𝕜 : 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 : ℕ} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} (hφ : IsAdaptedChart ψ Y φ σ) (i : Fin c) : ∃ (j : PieceIdx ψ Y c), pieceChart j = φ ∧ pieceEmb j = σ ∧ j.2 = i

Every adapted chart with every index is a piece.

@[reducible, inline]

noncomputable abbrev Manifold.BlowUpGlue.pieceMap {𝕜 : 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) : (Fin n → 𝕜) → Fin n → 𝕜

The chart map π_i of a piece.

Equations

• Manifold.BlowUpGlue.pieceMap j = Manifold.blowUpChartMap (Manifold.BlowUpGlue.pieceEmb j) j.2

def Manifold.BlowUpGlue.pieceSet {𝕜 : 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) : Set (Fin n → 𝕜)

The chart domain π_i⁻¹(ψ(φ(U))) of a piece.

Equations

• Manifold.BlowUpGlue.pieceSet j = Manifold.BlowUpGlue.pieceMap j ⁻¹' ⇑ψ '' (Manifold.BlowUpGlue.pieceChart j).target

theorem Manifold.BlowUpGlue.isOpen_pieceSet {𝕜 : 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) : IsOpen (pieceSet j)

The coordinate set of a piece is open (the preimage of an open set under the polynomial π_i).

noncomputable def Manifold.BlowUpGlue.blowDown {𝕜 : 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 : Fin n → 𝕜) : M

The blow-down β = φ⁻¹ ∘ ψ⁻¹ ∘ π_i of a piece.

Equations

• Manifold.BlowUpGlue.blowDown j u = ↑(Manifold.BlowUpGlue.pieceChart j).symm (ψ.symm (Manifold.BlowUpGlue.pieceMap j u))

theorem Manifold.BlowUpGlue.symm_pieceMap_mem_target {𝕜 : 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 : Fin n → 𝕜} (hu : u ∈ pieceSet j) : ψ.symm (pieceMap j u) ∈ (pieceChart j).target

For u in the piece set, ψ⁻¹(π_i u) lies in the target of the piece's chart.

theorem Manifold.BlowUpGlue.blowDown_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 : Fin n → 𝕜} (hu : u ∈ pieceSet j) : blowDown j u ∈ (pieceChart j).source

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

theorem Manifold.BlowUpGlue.apply_blowDown {𝕜 : 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 : Fin n → 𝕜} (hu : u ∈ pieceSet j) : ψ (↑(pieceChart j) (blowDown j u)) = pieceMap j u

The blow-down commutes with the chart: ψ (φ (blowDown j u)) = π_i u (condition (2) of [BM88, Definition 4.1], chartwise).

theorem Manifold.BlowUpGlue.continuousOn_blowDown {𝕜 : 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) : ContinuousOn (blowDown j) (pieceSet j)

The blow-down of a piece is continuous on the piece set.

The transition data

@[reducible, inline]

noncomputable abbrev Manifold.BlowUpGlue.pieceChange {𝕜 : 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) : (Fin n → 𝕜) → Fin n → 𝕜

The coordinate change between the charts of two pieces.

Equations

• Manifold.BlowUpGlue.pieceChange j j' = Manifold.chartChange ψ (Manifold.BlowUpGlue.pieceChart j) (Manifold.BlowUpGlue.pieceChart j')

@[reducible, inline]

abbrev Manifold.BlowUpGlue.pieceChangeDom {𝕜 : 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) : Set (Fin n → 𝕜)

The domain of the coordinate change between the charts of two pieces.

Equations

• Manifold.BlowUpGlue.pieceChangeDom j j' = Manifold.chartChangeDom ψ (Manifold.BlowUpGlue.pieceChart j) (Manifold.BlowUpGlue.pieceChart j')

@[reducible, inline]

noncomputable abbrev Manifold.BlowUpGlue.transDir {𝕜 : 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) : (Fin n → 𝕜) → 𝕜

The direction quotient D_{i'} of the lift of the coordinate change from chart i of the first piece to chart i' of the second.

Equations

• Manifold.BlowUpGlue.transDir j j' = Manifold.liftDir (Manifold.BlowUpGlue.pieceEmb j) (Manifold.BlowUpGlue.pieceEmb j') j.2 (Manifold.BlowUpGlue.pieceChange j j') j'.2

def Manifold.BlowUpGlue.transDom {𝕜 : 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) : Set (Fin n → 𝕜)

The transition domain: the points of the first piece over the second chart whose direction lies in chart i'.

Equations

• Manifold.BlowUpGlue.transDom j j' = Manifold.BlowUpGlue.pieceMap j ⁻¹' Manifold.BlowUpGlue.pieceChangeDom j j' ∩ {v : Fin n → 𝕜 | Manifold.BlowUpGlue.transDir j j' v ≠ 0}

noncomputable def Manifold.BlowUpGlue.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) : (Fin n → 𝕜) → Fin n → 𝕜

The transition map: the lift of the coordinate change to the blow-up charts.

Equations

• Manifold.BlowUpGlue.transMap j j' = Manifold.liftMap (Manifold.BlowUpGlue.pieceEmb j) (Manifold.BlowUpGlue.pieceEmb j') j.2 (Manifold.BlowUpGlue.pieceChange j j') j'.2

theorem Manifold.BlowUpGlue.isOpen_pieceChangeDom {𝕜 : 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) : IsOpen (pieceChangeDom j j')

The domain of the coordinate change between two pieces is open.

theorem Manifold.BlowUpGlue.analyticOnNhd_pieceChange {𝕜 : 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) : AnalyticOnNhd 𝕜 (pieceChange j j') (pieceChangeDom j j')

The coordinate change between two pieces is analytic on its domain.

theorem Manifold.BlowUpGlue.mem_center_iff_pieceChange {𝕜 : 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 : Fin n → 𝕜} (hx : x ∈ pieceChangeDom j j') : x ∈ blowUpCenter (pieceEmb j) ↔ pieceChange j j' x ∈ blowUpCenter (pieceEmb j')

The coordinate change between two pieces preserves the centre in both directions (both charts are adapted to Y).

theorem Manifold.BlowUpGlue.transDom_subset {𝕜 : 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) : transDom j j' ⊆ pieceSet j

The transition domain lies in the piece set.

theorem Manifold.BlowUpGlue.isOpen_transDom {𝕜 : 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) : IsOpen (transDom j j')

The transition domain is open.

theorem Manifold.BlowUpGlue.analyticOnNhd_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) : AnalyticOnNhd 𝕜 (transMap j j') (transDom j j')

The transition map is analytic on the transition domain.

theorem Manifold.BlowUpGlue.analyticOnNhd_transDir {𝕜 : 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) : AnalyticOnNhd 𝕜 (transDir j j') (pieceMap j ⁻¹' pieceChangeDom j j')

The direction quotient of the transition is analytic where the coordinate change is defined.

theorem Manifold.BlowUpGlue.pieceMap_mem_pieceChangeDom_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 : Fin n → 𝕜} (hu : u ∈ pieceSet j) : pieceMap j u ∈ pieceChangeDom j j' ↔ blowDown j u ∈ (pieceChart j').source

The points of the first piece over the second chart.

theorem Manifold.BlowUpGlue.pieceMap_mem_pieceChangeDom_self {𝕜 : 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 : Fin n → 𝕜} (hu : u ∈ pieceSet j) : pieceMap j u ∈ pieceChangeDom j j

π_i u lies in the domain of the trivial coordinate change of a piece with itself.

theorem Manifold.BlowUpGlue.pieceMap_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 : Fin n → 𝕜} (hu : u ∈ transDom j j') : pieceMap j' (transMap j j' u) = pieceChange j j' (pieceMap j u)

The transition map commutes with the chart maps: π_{i'} ∘ T = g ∘ π_i.

theorem Manifold.BlowUpGlue.blowDown_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 : Fin n → 𝕜} (hu : u ∈ transDom j j') : blowDown j' (transMap j j' u) = blowDown j u

The transition map commutes with the blow-downs.

theorem Manifold.BlowUpGlue.transMap_mem_pieceSet {𝕜 : 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 : Fin n → 𝕜} (hu : u ∈ transDom j j') : transMap j j' u ∈ pieceSet j'

The transition map carries the transition domain into the target piece set.

theorem Manifold.BlowUpGlue.transDir_self {𝕜 : 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 : Fin n → 𝕜} (hu : u ∈ pieceSet j) : transDir j j u = 1

The direction quotient of a piece with itself is 1.

theorem Manifold.BlowUpGlue.transDom_self {𝕜 : 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} : transDom j j = pieceSet j

The transition domain of a piece with itself is the whole piece set.

theorem Manifold.BlowUpGlue.transMap_self {𝕜 : 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 : Fin n → 𝕜} (hu : u ∈ pieceSet j) : transMap j j u = u

The transition map of a piece with itself is the identity.

theorem Manifold.BlowUpGlue.transDir_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' j'' : PieceIdx ψ Y c} {u : Fin n → 𝕜} (hu : u ∈ transDom j j') (hu' : pieceMap j u ∈ pieceChangeDom j j'') : transDir j j'' u = transDir j j' u * transDir j' j'' (transMap j j' u)

The cocycle of the direction quotients through a third piece.

theorem Manifold.BlowUpGlue.transMap_mem {𝕜 : 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 : Fin n → 𝕜} (hu : u ∈ transDom j j') : transMap j j' u ∈ transDom j' j

The transition map lands in the reverse transition domain: D^{-1}(T u) ≠ 0, by the cocycle of the direction quotients through the first piece itself (D_i^{id} = 1).

theorem Manifold.BlowUpGlue.transMap_mem_of_mem {𝕜 : 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' j'' : PieceIdx ψ Y c} {u : Fin n → 𝕜} (hu : u ∈ transDom j j') (hu' : u ∈ transDom j j'') : transMap j j' u ∈ transDom j' j''

The transition map carries the transition domain towards a third piece into the transition domain of the second piece towards it.

theorem Manifold.BlowUpGlue.transMap_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' j'' : PieceIdx ψ Y c} {u : Fin n → 𝕜} (hu : u ∈ transDom j j') (hu' : u ∈ transDom j j'') : transMap j' j'' (transMap j j' u) = transMap j j'' u

The cocycle law of the transition maps: two continuous lifts of the same coordinate change through the same chart agree (uniqueness of lifts, eqOn_of_lift_blowUpChartMap).