Hypersurface families glued along an open-embedding chain

Włodarczyk's exceptional divisor E on the glued space M̃ of a locally finite embedded desingularization [Wlo09, Theorem 2.0.2] is the union of the exceptional divisors of the successions over the members of an exhaustion, which agree on the overlaps up to the empty blow-ups ([Wlo09, Theorem 2.0.3 (4)]; [Kol07, Proposition 37, (37.2)]: the subschemes of the pieces glue). This module glues a chain of hypersurface families, one on each piece X m of an open-embedding chain c (OpenEmbeddingChain), into one family on the limit c.Limit, given order embeddings ε m of the index sets matching the members of consecutive levels (FamilyChain): the trace on X m of the member ε m j of level m + 1 is the member j, and a member of level m + 1 not in the range of ε m has empty trace on X m.

• FamilyChain.iter: the composite embeddings of the index sets, with their traces (preimage_iter_hyp_iter, preimage_iter_hyp_eq_empty).
• FamilyChain.Born: a member of level m is born at m when it is not the image of a member of level m - 1; every member has a unique born ancestor (exists_born, eq_of_born_of_iter_eq, birth).
• FamilyChain.glue: the glued family, indexed by the pairs (m, j) in the lexicographic order, the member of a born j being the union over the higher levels of the images of its descendants (and empty otherwise). Its trace on every piece is a member of that piece's family or empty (preimage_toLimit_glueHyp), its members are closed when those of the pieces are (isClosed_glueHyp), its support traces to the supports of the pieces (preimage_toLimit_support_glue), and it is a simple normal crossings family when every piece's family is (isSnc_glue): the adapted and snc charts of a piece, read on the limit through the inclusion of the piece (limitChart, limitChart_mem_maximalAtlas), serve for the glued family, whose members through a point correspond to the members of the piece through the point by the birth correspondence.

Not in the sources beyond the statements cited; bookkeeping.

Closed sets of the limit, and charts of the pieces read on the limit

theorem Manifold.OpenEmbeddingChain.isClosed_iff_forall_preimage_toLimit {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (s : Set c.Limit) : IsClosed s ↔ ∀ (n : ℕ), IsClosed (c.toLimit n ⁻¹' s)

A subset of the limit is closed iff its preimage in every piece is (the quotient topology of the sigma type).

theorem Manifold.OpenEmbeddingChain.limitChart_mem_maximalAtlas {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) [Nonempty (c.X n).carrier] {φ : OpenPartialHomeomorph (c.X n).carrier E} (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ (c.X n).carrier) : c.limitChart n φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ c.Limit

A chart of the maximal atlas of a piece, read on the limit through the inclusion of the piece, is a chart of the maximal atlas of the limit (mem_maximalAtlas_of_contMDiffOn: analytic with analytic inverse).

theorem Manifold.OpenEmbeddingChain.toLimit_mem_limitChart_source {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) [Nonempty (c.X n).carrier] (φ : OpenPartialHomeomorph (c.X n).carrier E) {x : (c.X n).carrier} (hx : x ∈ φ.source) : c.toLimit n x ∈ (c.limitChart n φ).source

A point of the limit over a piece lies in the source of the limit chart of a chart of the piece containing its preimage.

theorem Manifold.OpenEmbeddingChain.exists_eq_toLimit_of_mem_limitChart_source {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) [Nonempty (c.X n).carrier] (φ : OpenPartialHomeomorph (c.X n).carrier E) {q : c.Limit} (hq : q ∈ (c.limitChart n φ).source) : ∃ x ∈ φ.source, c.toLimit n x = q

A point of the source of a limit chart is the image of a point of the chart's source.

theorem Manifold.OpenEmbeddingChain.limitChart_toLimit {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) [Nonempty (c.X n).carrier] (φ : OpenPartialHomeomorph (c.X n).carrier E) (x : (c.X n).carrier) : ↑(c.limitChart n φ) (c.toLimit n x) = ↑φ x

The limit chart at the image of a point of the piece is the chart at the point.

A chain of hypersurface families

structure Manifold.OpenEmbeddingChain.FamilyChain {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) : Type (u + 1)

A chain of hypersurface families on the pieces of c, with order embeddings of the index sets matching the members of consecutive levels: the trace on X m of the member ε m j of level m + 1 is the member j of level m, and a member of level m + 1 outside the range of ε m has empty trace on X m ([Kol07, Proposition 37, (37.2)]; the empty blow-ups arising from restriction, [Kol07, 34.1]).

• H (m : ℕ) : HypersurfaceFamily (c.X m).carrier

  The family on the piece X m.

• ε (m : ℕ) : (self.H m).ι ↪o (self.H (m + 1)).ι

  The matching of the members of level m with members of level m + 1.

• preimage_hyp_ε (m : ℕ) (j : (self.H m).ι) : ⇑(c.ι m) ⁻¹' (self.H (m + 1)).hyp ((self.ε m) j) = (self.H m).hyp j

  The trace of a matched member is the member.

• preimage_hyp_eq_empty (m : ℕ) (b : (self.H (m + 1)).ι) : b ∉ Set.range ⇑(self.ε m) → ⇑(c.ι m) ⁻¹' (self.H (m + 1)).hyp b = ∅

  An unmatched member of level m + 1 has empty trace on level m.

The composite embeddings of the index sets

def Manifold.OpenEmbeddingChain.FamilyChain.iter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) {m m' : ℕ} : m ≤ m' → (D.H m).ι ↪o (D.H m').ι

The composite embedding (H m).ι ↪o (H m').ι for m ≤ m', ε (m'-1) ∘ ⋯ ∘ ε m (Nat.leRecOn, as OpenEmbeddingChain.iter).

Equations

• D.iter h = Nat.leRecOn h (fun {k : ℕ} (f : (D.H m).ι ↪o (D.H k).ι) => RelEmbedding.trans f (D.ε k)) (RelEmbedding.refl fun (x1 x2 : (D.H m).ι) => x1 ≤ x2)

theorem Manifold.OpenEmbeddingChain.FamilyChain.iter_self {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) (m : ℕ) : D.iter ⋯ = RelEmbedding.refl fun (x1 x2 : (D.H m).ι) => x1 ≤ x2

theorem Manifold.OpenEmbeddingChain.FamilyChain.iter_self_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) (m : ℕ) (h : m ≤ m) (j : (D.H m).ι) : (D.iter h) j = j

theorem Manifold.OpenEmbeddingChain.FamilyChain.iter_succ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) {m m' : ℕ} (h : m ≤ m') (h' : m ≤ m' + 1) : D.iter h' = RelEmbedding.trans (D.iter h) (D.ε m')

theorem Manifold.OpenEmbeddingChain.FamilyChain.iter_succ_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) {m m' : ℕ} (h : m ≤ m') (h' : m ≤ m' + 1) (j : (D.H m).ι) : (D.iter h') j = (D.ε m') ((D.iter h) j)

theorem Manifold.OpenEmbeddingChain.FamilyChain.iter_trans {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) {m m' k : ℕ} (h₁ : m ≤ m') (h₂ : m' ≤ k) (j : (D.H m).ι) : (D.iter h₂) ((D.iter h₁) j) = (D.iter ⋯) j

theorem Manifold.OpenEmbeddingChain.FamilyChain.preimage_iter_hyp_iter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) {m m' : ℕ} (h : m ≤ m') (j : (D.H m).ι) : ⇑(c.iter h) ⁻¹' (D.H m').hyp ((D.iter h) j) = (D.H m).hyp j

The trace on X m of the descendant at level m' of a member of level m is the member.

theorem Manifold.OpenEmbeddingChain.FamilyChain.preimage_iter_hyp_eq_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) {m m' : ℕ} (h : m ≤ m') (b : (D.H m').ι) (hb : b ∉ Set.range ⇑(D.iter h)) : ⇑(c.iter h) ⁻¹' (D.H m').hyp b = ∅

A member of level m' which is not the descendant of a member of level m has empty trace on X m.

Birth

def Manifold.OpenEmbeddingChain.FamilyChain.Born {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) (m : ℕ) : (D.H m).ι → Prop

A member of level m is born at m when it is not the image of a member of level m - 1 (every member of level 0 is born at 0).

Equations

• D.Born 0 x_2 = True
• D.Born m.succ j = (j ∉ Set.range ⇑(D.ε m))

theorem Manifold.OpenEmbeddingChain.FamilyChain.born_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) (j : (D.H 0).ι) : D.Born 0 j

theorem Manifold.OpenEmbeddingChain.FamilyChain.born_succ_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) (m : ℕ) (j : (D.H (m + 1)).ι) : D.Born (m + 1) j ↔ j ∉ Set.range ⇑(D.ε m)

theorem Manifold.OpenEmbeddingChain.FamilyChain.exists_born {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) (m' : ℕ) (b : (D.H m').ι) : ∃ (m : ℕ) (h : m ≤ m') (j : (D.H m).ι), D.Born m j ∧ (D.iter h) j = b

Every member has a born ancestor.

theorem Manifold.OpenEmbeddingChain.FamilyChain.not_lt_of_born_of_iter_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) {m₁ m₂ m' : ℕ} (h₁ : m₁ ≤ m') (h₂ : m₂ ≤ m') {j₁ : (D.H m₁).ι} {j₂ : (D.H m₂).ι} (hb₂ : D.Born m₂ j₂) (heq : (D.iter h₁) j₁ = (D.iter h₂) j₂) : ¬m₁ < m₂

A born member is no descendant of a member of a lower level.

theorem Manifold.OpenEmbeddingChain.FamilyChain.eq_of_born_of_iter_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) {m₁ m₂ m' : ℕ} (h₁ : m₁ ≤ m') (h₂ : m₂ ≤ m') {j₁ : (D.H m₁).ι} {j₂ : (D.H m₂).ι} (hb₁ : D.Born m₁ j₁) (hb₂ : D.Born m₂ j₂) (heq : (D.iter h₁) j₁ = (D.iter h₂) j₂) : ⟨m₁, j₁⟩ = ⟨m₂, j₂⟩

The born ancestor of a member is unique.

noncomputable def Manifold.OpenEmbeddingChain.FamilyChain.birth {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) (m' : ℕ) (b : (D.H m').ι) : (m : ℕ) × (D.H m).ι

The born ancestor of a member (chosen).

Equations

• D.birth m' b = ⟨⋯.choose, ⋯.choose⟩

theorem Manifold.OpenEmbeddingChain.FamilyChain.birth_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) (m' : ℕ) (b : (D.H m').ι) : (D.birth m' b).fst ≤ m'

theorem Manifold.OpenEmbeddingChain.FamilyChain.born_birth {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) (m' : ℕ) (b : (D.H m').ι) : D.Born (D.birth m' b).fst (D.birth m' b).snd

theorem Manifold.OpenEmbeddingChain.FamilyChain.iter_birth {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) (m' : ℕ) (b : (D.H m').ι) : (D.iter ⋯) (D.birth m' b).snd = b

theorem Manifold.OpenEmbeddingChain.FamilyChain.iter_congr_sigma {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) {m' : ℕ} {p q : (m : ℕ) × (D.H m).ι} (hp : p.fst ≤ m') (hq : q.fst ≤ m') (h : p = q) : (D.iter hp) p.snd = (D.iter hq) q.snd

The composite embedding read on equal pairs.

theorem Manifold.OpenEmbeddingChain.FamilyChain.eq_of_birth_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) {m' : ℕ} {b₁ b₂ : (D.H m').ι} (h : D.birth m' b₁ = D.birth m' b₂) : b₁ = b₂

The birth map is injective.

theorem Manifold.OpenEmbeddingChain.FamilyChain.birth_iter_of_born {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) {m m' : ℕ} (h : m ≤ m') {j : (D.H m).ι} (hj : D.Born m j) : D.birth m' ((D.iter h) j) = ⟨m, j⟩

The birth of the descendant of a born member is the member.

The glued family

def Manifold.OpenEmbeddingChain.FamilyChain.glueHyp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) (m : ℕ) (j : (D.H m).ι) : Set c.Limit

The glued member of the pair (m, j): for j born at m, the union over the levels m' ≥ m of the images in the limit of its descendants; empty otherwise.

Equations

• D.glueHyp m j = if D.Born m j then ⋃ (m' : ℕ), ⋃ (h : m ≤ m'), c.toLimit m' '' (D.H m').hyp ((D.iter h) j) else ∅

def Manifold.OpenEmbeddingChain.FamilyChain.glue {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) : HypersurfaceFamily c.Limit

The glued hypersurface family on the limit, indexed by the pairs (m, j) in the lexicographic order.

Equations

• D.glue = { ι := Σₗ (m : ℕ), (D.H m).ι, countable := ⋯, linearOrder := Sigma.Lex.linearOrder, hyp := fun (p : Σₗ (m : ℕ), (D.H m).ι) => D.glueHyp (ofLex p).fst (ofLex p).snd }

theorem Manifold.OpenEmbeddingChain.FamilyChain.glue_hyp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) (p : Σₗ (m : ℕ), (D.H m).ι) : D.glue.hyp p = D.glueHyp (ofLex p).fst (ofLex p).snd

theorem Manifold.OpenEmbeddingChain.FamilyChain.glueHyp_of_not_born {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) {m : ℕ} {j : (D.H m).ι} (hj : ¬D.Born m j) : D.glueHyp m j = ∅

theorem Manifold.OpenEmbeddingChain.FamilyChain.preimage_toLimit_glueHyp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) {m : ℕ} {j : (D.H m).ι} (hj : D.Born m j) (m'' : ℕ) : c.toLimit m'' ⁻¹' D.glueHyp m j = if h : m ≤ m'' then (D.H m'').hyp ((D.iter h) j) else ∅

The trace of a glued member on a piece: the descendant of the member at that level, if the level is at or above the birth level, and empty below it.

theorem Manifold.OpenEmbeddingChain.FamilyChain.preimage_toLimit_glueHyp_birth {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) (m' : ℕ) (b : (D.H m').ι) : c.toLimit m' ⁻¹' D.glueHyp (D.birth m' b).fst (D.birth m' b).snd = (D.H m').hyp b

The trace of the glued member of the birth of a member b of a piece is b.

theorem Manifold.OpenEmbeddingChain.FamilyChain.toLimit_mem_glueHyp_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) (m : ℕ) (j : (D.H m).ι) (m'' : ℕ) (x : (c.X m'').carrier) : c.toLimit m'' x ∈ D.glueHyp m j ↔ D.Born m j ∧ ∃ (h : m ≤ m''), x ∈ (D.H m'').hyp ((D.iter h) j)

The membership of a point of the limit over a piece in a glued member.

theorem Manifold.OpenEmbeddingChain.FamilyChain.isClosed_glueHyp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) (hcl : ∀ (m : ℕ) (j : (D.H m).ι), IsClosed ((D.H m).hyp j)) (m : ℕ) (j : (D.H m).ι) : IsClosed (D.glueHyp m j)

The glued members are closed when the members of the pieces are.

theorem Manifold.OpenEmbeddingChain.FamilyChain.preimage_toLimit_support_glue {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) (m'' : ℕ) : c.toLimit m'' ⁻¹' D.glue.support = (D.H m'').support

The support of the glued family traces to the supports of the pieces.

Charts of a piece read on the limit

theorem Manifold.OpenEmbeddingChain.isAdaptedChart_limitChart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (m : ℕ) [Nonempty (c.X m).carrier] {Y' : Set c.Limit} {Y : Set (c.X m).carrier} (hY : c.toLimit m ⁻¹' Y' = Y) {φ : OpenPartialHomeomorph (c.X m).carrier E} {k : ℕ} {σ : Fin k ↪ Fin n} (hφ : IsAdaptedChart ψ Y φ σ) : IsAdaptedChart ψ Y' (c.limitChart m φ) σ

A chart of a piece adapted to the trace of a subset Y' of the limit, read on the limit, is adapted to Y'.

theorem Manifold.OpenEmbeddingChain.FamilyChain.isClosedSubmanifold_glueHyp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (hH : ∀ (m : ℕ), HypersurfaceFamily.IsSnc ψ (D.H m)) (m : ℕ) (j : (D.H m).ι) : IsClosedSubmanifold ψ (D.glueHyp m j) 1

The glued member of a born pair is a closed submanifold of codimension one when the members of the pieces are: the adapted chart of the trace, read on the limit.

def Manifold.OpenEmbeddingChain.FamilyChain.glueIdx {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) {m'' : ℕ} {x : (c.X m'').carrier} (p : { p : D.glue.ι // c.toLimit m'' x ∈ D.glue.hyp p }) : { b : (D.H m'').ι // x ∈ (D.H m'').hyp b }

The member of a piece through x corresponding to a glued member through the image of x: its descendant at that level (toLimit_mem_glueHyp_iff).

Equations

• D.glueIdx p = ⟨(D.iter ⋯) (ofLex ↑p).snd, ⋯⟩

theorem Manifold.OpenEmbeddingChain.FamilyChain.glueIdx_injective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) {m'' : ℕ} {x : (c.X m'').carrier} : Function.Injective D.glueIdx

theorem Manifold.OpenEmbeddingChain.FamilyChain.isSncChartAt_glue_limitChart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {m'' : ℕ} [Nonempty (c.X m'').carrier] {x : (c.X m'').carrier} {φ : OpenPartialHomeomorph (c.X m'').carrier E} {cidx : { j : (D.H m'').ι // x ∈ (D.H m'').hyp j } → Fin n} (hc : HypersurfaceFamily.IsSncChartAt ψ (D.H m'') φ x cidx) : HypersurfaceFamily.IsSncChartAt ψ D.glue (c.limitChart m'' φ) (c.toLimit m'' x) fun (p : { j : D.glue.ι // c.toLimit m'' x ∈ D.glue.hyp j }) => cidx (D.glueIdx p)

An snc chart of a piece's family at x, read on the limit, is an snc chart of the glued family at the image of x, with the indices of the glued members through the point those of their descendants in the piece (glueIdx).

theorem Manifold.OpenEmbeddingChain.FamilyChain.locallyFinite_glue {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) (hH : ∀ (m : ℕ), LocallyFinite (D.H m).hyp) : LocallyFinite D.glue.hyp

The glued family is locally finite when the families of the pieces are: a neighbourhood of a point of a piece meeting finitely many members of the piece, read on the limit, meets only the glued members of their born ancestors.

theorem Manifold.OpenEmbeddingChain.FamilyChain.isSnc_glue {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : OpenEmbeddingChain 𝕜 E} (D : c.FamilyChain) {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (hH : ∀ (m : ℕ), HypersurfaceFamily.IsSnc ψ (D.H m)) : HypersurfaceFamily.IsSnc ψ D.glue

The glued family of a chain of simple normal crossings families has simple normal crossings: closed smooth hypersurfaces (isClosedSubmanifold_glueHyp), locally finite (locallyFinite_glue), and the snc chart of a piece at a point, read on the limit, is an snc chart of the glued family, the members through the point corresponding to those of the piece through it by the birth correspondence.