The strict transforms of a family under a blowing-up

Kollár's disjoining [Kol07, 72] blows up the m-fold meet locus and continues with "the (π_0 ⋯ π_{t-1})^{-1}_* E_i", the strict transforms of the components — the total transform of [Kol07, Definition 25] without its exceptional member, indexed by the original index set. This module defines that family, HypersurfaceFamily.strictTransforms π Y F, and proves what the disjoining needs of it: it is a simple normal crossings divisor when the total transform is (a subfamily), a point of a strict transform lies over the component, off the centre the strict transforms are the preimages, and a point on m strict transforms lies over a point on the m components. The key statement of [Kol07, 72] — after blowing up the m-fold locus no point lies on m strict transforms — is proved with the adapted chart of the meet locus in Disjoin.lean of this directory.

def Manifold.HypersurfaceFamily.strictTransforms {M M' : Type u} [TopologicalSpace M'] (π : M' → M) (Y : Set M) (F : HypersurfaceFamily M) : HypersurfaceFamily M'

Kollár's "the (π_0 ⋯ π_{t-1})^{-1}_* E_i" [Kol07, 72]: the family of the strict transforms of the components of F under π with centre Y, indexed by the components of F — the total transform of [Kol07, Definition 25] without its exceptional member.

Equations

• Manifold.HypersurfaceFamily.strictTransforms π Y F = { ι := F.ι, countable := ⋯, linearOrder := F.linearOrder, hyp := fun (j : F.ι) => Manifold.strictTransformSet π Y (F.hyp j) }

@[simp]

theorem Manifold.HypersurfaceFamily.strictTransforms_hyp {M M' : Type u} [TopologicalSpace M'] (π : M' → M) (Y : Set M) (F : HypersurfaceFamily M) (j : F.ι) : (strictTransforms π Y F).hyp j = strictTransformSet π Y (F.hyp j)

theorem Manifold.HypersurfaceFamily.strictTransforms_hyp_eq_totalTransform_hyp {M M' : Type u} [TopologicalSpace M'] (π : M' → M) (Y : Set M) (F : HypersurfaceFamily M) (j : F.ι) : (strictTransforms π Y F).hyp j = (totalTransform π Y F).hyp (toLex (Sum.inl j))

The strict transforms are the inl components of the total transform.

theorem Manifold.HypersurfaceFamily.mem_hyp_of_mem_strictTransforms {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {Y : Set M} {F : HypersurfaceFamily M} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {c : ℕ} (h : IsBlowUp ψ Y c π) (hF : IsSnc ψ F) {p : M'} {j : F.ι} (hp : p ∈ (strictTransforms π Y F).hyp j) : π p ∈ F.hyp j

A point of a strict transform lies over the component.

theorem Manifold.HypersurfaceFamily.mem_strictTransforms_iff_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {Y : Set M} {F : HypersurfaceFamily M} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {c : ℕ} (h : IsBlowUp ψ Y c π) (hF : IsSnc ψ F) {p : M'} (hpY : π p ∉ Y) (j : F.ι) : p ∈ (strictTransforms π Y F).hyp j ↔ π p ∈ F.hyp j

Off the centre a strict transform is the preimage of its component.

theorem Manifold.HypersurfaceFamily.mem_meetLocus_of_mem_meetLocus_strictTransforms {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {Y : Set M} {F : HypersurfaceFamily M} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {c : ℕ} (h : IsBlowUp ψ Y c π) (hF : IsSnc ψ F) {m : ℕ} {p : M'} (hp : p ∈ (strictTransforms π Y F).meetLocus m) : π p ∈ F.meetLocus m

A point lying on m strict transforms lies over a point lying on the m components: the meet loci of the strict transforms map into the meet loci of F.

theorem Manifold.HypersurfaceFamily.mem_meetLocus_strictTransforms_iff_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {Y : Set M} {F : HypersurfaceFamily M} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {c : ℕ} (h : IsBlowUp ψ Y c π) (hF : IsSnc ψ F) {m : ℕ} {p : M'} (hpY : π p ∉ Y) : p ∈ (strictTransforms π Y F).meetLocus m ↔ π p ∈ F.meetLocus m

Off the centre the meet loci of the strict transforms are the preimages of the meet loci.

theorem Manifold.HypersurfaceFamily.isSnc_strictTransforms {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {Y : Set M} {F : HypersurfaceFamily M} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) (hF : IsSnc ψ F) (hsnc : HasSncWith ψ F Y c) : IsSnc ψ (strictTransforms π Y F)

The strict transforms form a simple normal crossings divisor when the centre has simple normal crossings with F ([Kol07, Definition 25]): they are a subfamily of the total transform (isSnc_totalTransform) — closed smooth hypersurfaces, locally finite, and at every point the snc chart of the total transform serves with its indices restricted to the strict transforms through the point.