The trace of a divisor on a closed submanifold

Kollár's restriction of a blow-up sequence to a closed subvariety S [Kol07, 30.2] works on the strict transforms S_i with the traces E_i ∩ S_i of the boundaries. This module defines the trace of a family of hypersurfaces F on a closed submanifold S (IsClosedSubmanifold.traceFamily: the components F^j ∩ S, read on the bundled manifold S) and proves that it is a simple normal crossings divisor of S when S has simple normal crossings with F properly (isSnc_traceFamily): in the proper chart at a point of S (adapted to S, snc for F, component coordinates off the S-block) the induced chart of S (inducedChart, the complementary coordinates) is an snc chart of the trace with the component coordinates re-indexed through complEquiv (isSncChartAt_inducedChart). When moreover Z ⊆ S has simple normal crossings with F, Z — as the submanifold Z ∩ S of S — has simple normal crossings with the trace (hasSncWith_traceFamily; Kollár's centres Z_i ∩ S_i with simple normal crossings with E_i ∩ S_i): the simultaneous chart of Hironaka/Manifold/Snc/FlagProtected.lean (exists_isSncChartAt_flag_proper) induces the chart of S adapted to Z ∩ S (isAdaptedChart_chartOn_flag) which is an snc chart of the trace. These are the boundaries of the restricted sequences of the embedded resolution (Hironaka/Resolution/Analytic/Restrict/BoundaryTrace.lean).

def Manifold.IsClosedSubmanifold.traceFamily {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) (F : HypersurfaceFamily M) : HypersurfaceFamily hS.toAnalyticManifold.carrier

The trace of the family F on the closed submanifold S: the components F^j ∩ S, in the order of F, read on the bundled manifold S (toAnalyticManifold) — Kollár's boundary E_i ∩ S_i of a restricted blow-up sequence [Kol07, 30.2].

Equations

• hS.traceFamily F = { ι := F.ι, countable := ⋯, linearOrder := F.linearOrder, hyp := fun (j : F.ι) => hS.preimageVal (F.hyp j) }

theorem Manifold.IsClosedSubmanifold.traceFamily_hyp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) (F : HypersurfaceFamily M) (j : (hS.traceFamily F).ι) : (hS.traceFamily F).hyp j = hS.preimageVal (F.hyp j)

theorem Manifold.IsClosedSubmanifold.traceFamily_support {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) (F : HypersurfaceFamily M) : (hS.traceFamily F).support = hS.preimageVal F.support

The support of the trace is the trace of the support.

theorem Manifold.IsClosedSubmanifold.isSncChartAt_inducedChart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} {F : HypersurfaceFamily M} (hS : IsClosedSubmanifold ψ S s) {φ : OpenPartialHomeomorph M E} {σ' : Fin s ↪ Fin n} (hφS : IsAdaptedChart ψ S φ σ') {b : hS.toAnalyticManifold.carrier} {cidx : { j : F.ι // ↑b ∈ F.hyp j } → Fin n} (hc : HypersurfaceFamily.IsSncChartAt ψ F φ (↑b) cidx) (hproper : ∀ (j : { j : F.ι // ↑b ∈ F.hyp j }), cidx j ∉ Set.range ⇑σ') : HypersurfaceFamily.IsSncChartAt (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (hS.traceFamily F) (hS.inducedChart hφS ⋯) b fun (j : { j : (hS.traceFamily F).ι // b ∈ (hS.traceFamily F).hyp j }) => (complEquiv σ') ⟨cidx ⟨↑j, ⋯⟩, ⋯⟩

In a chart adapted to S which is an snc chart of F at a point of S with the component coordinates off the S-block, the induced chart of S (the complementary coordinates, inducedChart) is an snc chart of the trace of F on S, with the component coordinates re-indexed through complEquiv.

theorem Manifold.IsClosedSubmanifold.isSnc_traceFamily {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} {F : HypersurfaceFamily M} (hS : IsClosedSubmanifold ψ S s) (hF : HypersurfaceFamily.IsSnc ψ F) (hFS : HypersurfaceFamily.HasSncWithProper ψ F S s) : HypersurfaceFamily.IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (hS.traceFamily F)

If the closed submanifold S has simple normal crossings with the snc divisor F properly, the trace of F on S is a simple normal crossings divisor of S [Kol07, 30.2]: its components are closed hypersurfaces of S (the induced charts of the proper charts), locally finite (preimages of a locally finite family), with the induced charts as snc charts (isSncChartAt_inducedChart).

theorem Manifold.IsClosedSubmanifold.hasSncWith_traceFamily {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} {F : HypersurfaceFamily M} (hS : IsClosedSubmanifold ψ S s) (hF : HypersurfaceFamily.IsSnc ψ F) {Z : Set M} {c : ℕ} (hZ : IsClosedSubmanifold ψ Z c) (hZS : Z ⊆ S) (hFZ : HypersurfaceFamily.HasSncWith ψ F Z c) (hFS : HypersurfaceFamily.HasSncWithProper ψ F S s) : HypersurfaceFamily.HasSncWith (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (hS.traceFamily F) (hS.preimageVal Z) (c - s)

If Z ⊆ S has simple normal crossings with the snc divisor F and S has simple normal crossings with F properly, then Z — the submanifold Z ∩ S of S, of codimension c − s — has simple normal crossings with the trace of F on S (Kollár's centres Z_i ∩ S_i and boundaries E_i ∩ S_i, [Kol07, 30.2]). At a point of Z, the simultaneous chart (exists_isSncChartAt_flag_proper) induces the chart of S adapted to Z ∩ S (isAdaptedChart_chartOn_flag), which is an snc chart of the trace.