3.1. Ideal sheaves, submanifolds and blow-ups🔗

Lean names in this section are shown relative to Manifold, AnalyticManifold, TopologicalSpace, Topology, Filter, Set.

The analytic theorems are written in a vocabulary collected in the namespace AnalyticManifold, built on an infrastructure in the namespace Manifold: the sheaf of analytic functions on a manifold and its germs, locally finitely generated ideal sheaves, closed submanifolds and blow-ups with smooth centre in the sense of Bierstone–Milman [BM88, Definition 4.1], simple normal crossings families of hypersurfaces, and the Jacobian ideal. The field is 𝕜 (ℝ for the main theorems, ℝ or ℂ where RCLike 𝕜 suffices) and the model space a normed space E.

3.1.1. Analytic manifolds and maps🔗

Definition3.1.1.1source[Hir64, pp. 119–121] ↗

uses 0

Used by 31

Reverse dependency previews

Preview

Definition 3.1.3.3

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

An AnalyticManifold 𝕜 E is a bundled analytic manifold modelled on E: a type of points (carrier) with a topology (top), a charted-space structure (charted) with analytic chart changes (manifold, Mathlib's IsManifold at smoothness \omega), Hausdorff (t2) and second countable (secondCountable), without boundary; the coercion instCoeSortType lets M stand for its type of points. For E finite-dimensional this is a pure-dimensional non-singular analytic \mathbb{K}-space in Hironaka's sense; his non-singular spaces may have components of different dimensions.

An AnalyticMap M N is a bundled analytic map (Mathlib's C^ω maps). An open subset U of M is again an analytic manifold, M.restrict U, with the inclusion M.inclusion U; this is how Włodarczyk's neighbourhoods U_K of compact sets become manifolds.

Lean code for Definition3.1.1.1●11 declarations

structure(6 fields)defined in Hironaka/Manifold/AnalyticManifold/Defs.lean

complete

structure AnalyticManifold (𝕜 : Type u_1) [NontriviallyNormedField 𝕜]
  (E : Type u_2) [NormedAddCommGroup E] [NormedSpace 𝕜 E] :
  Type (max (u + 1) u_2)

structure AnalyticManifold (𝕜 : Type u_1)
  [NontriviallyNormedField 𝕜]
  (E : Type u_2) [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] :
  Type (max (u + 1) u_2)

A bundled analytic manifold over 𝕜 modelled on E: Hausdorff, second countable, without boundary, with analytic (C^ω) chart changes — for E finite-dimensional, Hironaka's non-singular analytic 𝕜-space [Hir64, pp. 119–121].

Fields

carrier : Type u

The underlying type of points.

top : TopologicalSpace self.carrier

charted : ChartedSpace E self.carrier

manifold : IsManifold 𝓘(𝕜, E) ⊤ self.carrier

t2 : T2Space self.carrier

secondCountable : SecondCountableTopology self.carrier

abbrevdefined in Hironaka/Manifold/AnalyticManifold/Defs.lean

complete

abbrev carrier {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  (self : AnalyticManifold 𝕜 E) : Type u :=
  self.1

abbrev carrier {𝕜 : Type u_1}
  [NontriviallyNormedField 𝕜]
  {E : Type u_2} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E]
  (self : AnalyticManifold 𝕜 E) : Type u :=
  self.1

The underlying type of points.

abbrevdefined in Hironaka/Manifold/AnalyticManifold/Defs.lean

complete

abbrev top {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  (self : AnalyticManifold 𝕜 E) : TopologicalSpace self.carrier

abbrev top {𝕜 : Type u_1}
  [NontriviallyNormedField 𝕜]
  {E : Type u_2} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E]
  (self : AnalyticManifold 𝕜 E) :
  TopologicalSpace self.carrier

abbrevdefined in Hironaka/Manifold/AnalyticManifold/Defs.lean

complete

abbrev charted {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  (self : AnalyticManifold 𝕜 E) : ChartedSpace E self.carrier

abbrev charted {𝕜 : Type u_1}
  [NontriviallyNormedField 𝕜]
  {E : Type u_2} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E]
  (self : AnalyticManifold 𝕜 E) :
  ChartedSpace E self.carrier

theoremdefined in Hironaka/Manifold/AnalyticManifold/Defs.lean

complete

theorem manifold {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  (self : AnalyticManifold 𝕜 E) : IsManifold 𝓘(𝕜, E) ⊤ self.carrier

theorem manifold {𝕜 : Type u_1}
  [NontriviallyNormedField 𝕜]
  {E : Type u_2} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E]
  (self : AnalyticManifold 𝕜 E) :
  IsManifold 𝓘(𝕜, E) ⊤ self.carrier

theoremdefined in Hironaka/Manifold/AnalyticManifold/Defs.lean

complete

theorem t2 {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  (self : AnalyticManifold 𝕜 E) : T2Space self.carrier

theorem t2 {𝕜 : Type u_1}
  [NontriviallyNormedField 𝕜]
  {E : Type u_2} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E]
  (self : AnalyticManifold 𝕜 E) :
  T2Space self.carrier

theoremdefined in Hironaka/Manifold/AnalyticManifold/Defs.lean

complete

theorem secondCountable {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  (self : AnalyticManifold 𝕜 E) : SecondCountableTopology self.carrier

theorem secondCountable {𝕜 : Type u_1}
  [NontriviallyNormedField 𝕜]
  {E : Type u_2} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E]
  (self : AnalyticManifold 𝕜 E) :
  SecondCountableTopology self.carrier

defdefined in Hironaka/Manifold/AnalyticManifold/Defs.lean

complete

def instCoeSortType {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] :
  CoeSort (AnalyticManifold 𝕜 E) (Type u)

def instCoeSortType {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] :
  CoeSort (AnalyticManifold 𝕜 E) (Type u)

abbrevdefined in Hironaka/Manifold/AnalyticManifold/Defs.lean

complete

abbrev AnalyticMap {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  (M N : AnalyticManifold 𝕜 E) : Type u :=
  C^⊤⟮𝓘(𝕜, E), M.carrier; 𝓘(𝕜, E), N.carrier⟯

abbrev AnalyticMap {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E]
  (M N : AnalyticManifold 𝕜 E) : Type u :=
  C^⊤⟮𝓘(𝕜, E), M.carrier; 𝓘(𝕜, E),
    N.carrier⟯

Analytic maps between analytic manifolds: Mathlib's bundled C^ω maps.

defdefined in Hironaka/Manifold/AnalyticManifold/Defs.lean

complete

def restrict {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : AnalyticManifold 𝕜 E)
  (U : Opens M.carrier) : AnalyticManifold 𝕜 E :=
  { carrier := ↥U, top := instTopologicalSpaceSubtype,
    charted := U.instChartedSpace, manifold := ⋯, t2 := ⋯,
    secondCountable := ⋯ }

def restrict {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E]
  (M : AnalyticManifold 𝕜 E)
  (U : Opens M.carrier) :
  AnalyticManifold 𝕜 E :=
  { carrier := ↥U,
    top := instTopologicalSpaceSubtype,
    charted := U.instChartedSpace,
    manifold := ⋯, t2 := ⋯,
    secondCountable := ⋯ }

The open subset U of M as an analytic manifold (Włodarczyk's neighbourhood U ⊃ Z of a compact set and the stages U_i over it, [Wlo09, Theorem 2.0.3 (1)]): Mathlib's charted-space and IsManifold instances on Opens; Hausdorff and second countable as a subspace of M.

defdefined in Hironaka/Manifold/AnalyticManifold/Defs.lean

complete

def inclusion {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : AnalyticManifold 𝕜 E)
  (U : Opens M.carrier) : AnalyticMap (M.restrict U) M :=
  ⟨Subtype.val, ⋯⟩

def inclusion {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E]
  (M : AnalyticManifold 𝕜 E)
  (U : Opens M.carrier) :
  AnalyticMap (M.restrict U) M :=
  ⟨Subtype.val, ⋯⟩

The inclusion U → M of an open subset as an analytic map (Mathlib's contMDiff_subtype_val).

3.1.2. The sheaf of analytic functions and germs🔗

Definition3.1.2.1source[BM97, (0.3)] ↗

uses 0

Used by 26

Reverse dependency previews

Preview

Definition 3.1.2.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

The structure sheaf structureSheaf 𝕜 E M is the sheaf of commutative rings U \mapsto \{f \colon U \to \mathbb{K} \text{ analytic}\}, the sheaf of regular functions of an analytic manifold. It is built from the sheaf of C^n functions to a C^n ring (contMDiffLocalPredicate, contMDiffSheaf, contMDiffPresheafCommRing with its ring instance, contMDiffSheafCommRing) at n = \omega; a section is a function on its open set (the coercions coeFun of the three sheaves). Its stalks are local rings, as the order of an ideal sheaf at a point requires (Definition 3.1.3.1). The constants give its \mathbb{K}-algebra structure (constSection, constHom), and a chart \varphi with linear coordinates \psi gives coordinate functions \psi_i \circ \varphi as sections (chartSection) and as germs (coord).

Lean code for Definition3.1.2.1●13 definitions

defdefined in Hironaka/Manifold/StructureSheaf/Defs.lean

complete

def contMDiffLocalPredicate {𝕜 : Type} [NontriviallyNormedField 𝕜]
  {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM]
  {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4}
  [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞)
  (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (N : Type)
  [TopologicalSpace N] [ChartedSpace H N] :
  TopCat.LocalPredicate fun x => N :=
  {
    pred := fun {U} f =>
      ChartedSpace.LiftProp (ContDiffWithinAtProp IM I n) f,
    res := ⋯, locality := ⋯ }

def contMDiffLocalPredicate {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {EM : Type u_1} [NormedAddCommGroup EM]
  [NormedSpace 𝕜 EM] {HM : Type u_2}
  [TopologicalSpace HM]
  (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_3} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {H : Type u_4}
  [TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H)
  (n : WithTop ℕ∞) (M : Type u)
  [TopologicalSpace M] [ChartedSpace HM M]
  (N : Type) [TopologicalSpace N]
  [ChartedSpace H N] :
  TopCat.LocalPredicate fun x => N :=
  {
    pred := fun {U} f =>
      ChartedSpace.LiftProp
        (ContDiffWithinAtProp IM I n) f,
    res := ⋯, locality := ⋯ }

The local predicate "f : U → N is C^n" on the open sets of M: Mathlib's LocalInvariantProp.localPredicate for contDiffWithinAt_localInvariantProp n, with the target in Type (Mathlib's version needs M and N in one universe).

defdefined in Hironaka/Manifold/StructureSheaf/Defs.lean

complete

def contMDiffSheaf {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1}
  [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2}
  [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_3}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4}
  [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞)
  (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (N : Type)
  [TopologicalSpace N] [ChartedSpace H N] : TopCat.Sheaf (Type u) ↧M :=
  TopCat.subsheafToTypes (contMDiffLocalPredicate IM I n M N)

def contMDiffSheaf {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {EM : Type u_1} [NormedAddCommGroup EM]
  [NormedSpace 𝕜 EM] {HM : Type u_2}
  [TopologicalSpace HM]
  (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_3} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {H : Type u_4}
  [TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H)
  (n : WithTop ℕ∞) (M : Type u)
  [TopologicalSpace M] [ChartedSpace HM M]
  (N : Type) [TopologicalSpace N]
  [ChartedSpace H N] :
  TopCat.Sheaf (Type u) ↧M :=
  TopCat.subsheafToTypes
    (contMDiffLocalPredicate IM I n M N)

The sheaf of types of C^n functions from M to N.

defdefined in Hironaka/Manifold/StructureSheaf/Defs.lean

complete

def contMDiffPresheafCommRing {𝕜 : Type} [NontriviallyNormedField 𝕜]
  {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM]
  {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4}
  [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞)
  (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (R : Type)
  [CommRing R] [TopologicalSpace R] [ChartedSpace H R]
  [ContMDiffRing I n R] : TopCat.Presheaf CommRingCat ↧M :=
  { obj := fun U => ↧((contMDiffSheaf IM I n M R).presheaf.obj U),
    map := fun {X Y} h =>
      CommRingCat.ofHom (ContMDiffMap.restrictRingHom IM I R ⋯),
    map_id := ⋯, map_comp := ⋯ }

def contMDiffPresheafCommRing {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {EM : Type u_1} [NormedAddCommGroup EM]
  [NormedSpace 𝕜 EM] {HM : Type u_2}
  [TopologicalSpace HM]
  (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_3} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {H : Type u_4}
  [TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H)
  (n : WithTop ℕ∞) (M : Type u)
  [TopologicalSpace M] [ChartedSpace HM M]
  (R : Type) [CommRing R]
  [TopologicalSpace R] [ChartedSpace H R]
  [ContMDiffRing I n R] :
  TopCat.Presheaf CommRingCat ↧M :=
  {
    obj := fun U =>
      ↧((contMDiffSheaf IM I n M
                R).presheaf.obj
          U),
    map := fun {X Y} h =>
      CommRingCat.ofHom
        (ContMDiffMap.restrictRingHom IM I
          R ⋯),
    map_id := ⋯, map_comp := ⋯ }

The presheaf of C^n functions from M to a C^n commutative ring R, as a presheaf of commutative rings.

defdefined in Hironaka/Manifold/StructureSheaf/Defs.lean

complete

def instCommRingObjOppositeOpensCarrierOfPresheafContMDiffSheaf {𝕜 : Type}
  [NontriviallyNormedField 𝕜] {EM : Type u_1} [NormedAddCommGroup EM]
  [NormedSpace 𝕜 EM] {HM : Type u_2} [TopologicalSpace HM]
  (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_3} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (M : Type u)
  [TopologicalSpace M] [ChartedSpace HM M] (R : Type) [CommRing R]
  [TopologicalSpace R] [ChartedSpace H R] [ContMDiffRing I n R]
  (U : (Opens ↑↧M)ᵒᵖ) :
  CommRing ((contMDiffSheaf IM I n M R).presheaf.obj U)

def instCommRingObjOppositeOpensCarrierOfPresheafContMDiffSheaf
  {𝕜 : Type} [NontriviallyNormedField 𝕜]
  {EM : Type u_1} [NormedAddCommGroup EM]
  [NormedSpace 𝕜 EM] {HM : Type u_2}
  [TopologicalSpace HM]
  (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_3} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {H : Type u_4}
  [TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H)
  (n : WithTop ℕ∞) (M : Type u)
  [TopologicalSpace M] [ChartedSpace HM M]
  (R : Type) [CommRing R]
  [TopologicalSpace R] [ChartedSpace H R]
  [ContMDiffRing I n R]
  (U : (Opens ↑↧M)ᵒᵖ) :
  CommRing
    ((contMDiffSheaf IM I n M
            R).presheaf.obj
      U)

defdefined in Hironaka/Manifold/StructureSheaf/Defs.lean

complete

def contMDiffSheafCommRing {𝕜 : Type} [NontriviallyNormedField 𝕜]
  {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM]
  {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4}
  [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞)
  (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (R : Type)
  [CommRing R] [TopologicalSpace R] [ChartedSpace H R]
  [ContMDiffRing I n R] : TopCat.Sheaf CommRingCat ↧M :=
  { obj := contMDiffPresheafCommRing IM I n M R, property := ⋯ }

def contMDiffSheafCommRing {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {EM : Type u_1} [NormedAddCommGroup EM]
  [NormedSpace 𝕜 EM] {HM : Type u_2}
  [TopologicalSpace HM]
  (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_3} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {H : Type u_4}
  [TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H)
  (n : WithTop ℕ∞) (M : Type u)
  [TopologicalSpace M] [ChartedSpace HM M]
  (R : Type) [CommRing R]
  [TopologicalSpace R] [ChartedSpace H R]
  [ContMDiffRing I n R] :
  TopCat.Sheaf CommRingCat ↧M :=
  {
    obj :=
      contMDiffPresheafCommRing IM I n M
        R,
    property := ⋯ }

The sheaf of C^n functions from M to a C^n commutative ring R, as a sheaf of commutative rings.

defdefined in Hironaka/Manifold/StructureSheaf/Defs.lean

complete

def structureSheaf (𝕜 : Type) [NontriviallyNormedField 𝕜] (E : Type u_1)
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : Type u)
  [TopologicalSpace M] [ChartedSpace E M] : TopCat.Sheaf CommRingCat ↧M :=
  contMDiffSheafCommRing 𝓘(𝕜, E) 𝓘(𝕜, 𝕜) ⊤ M 𝕜

def structureSheaf (𝕜 : Type)
  [NontriviallyNormedField 𝕜]
  (E : Type u_1) [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] (M : Type u)
  [TopologicalSpace M]
  [ChartedSpace E M] :
  TopCat.Sheaf CommRingCat ↧M :=
  contMDiffSheafCommRing 𝓘(𝕜, E) 𝓘(𝕜, 𝕜) ⊤
    M 𝕜

The structure sheaf 𝒪_M of analytic functions on the manifold M modelled on E over 𝕜: the sheaf of commutative rings U ↦ {f : U → 𝕜 : ContMDiff 𝓘(𝕜, E) 𝓘(𝕜) ω f}, the sheaf of regular functions of an analytic manifold [BM97, (0.3); §3, "Regular coordinate charts"].

defdefined in Hironaka/Manifold/StructureSheaf/Defs.lean

complete

def constSection (𝕜 : Type) [NontriviallyNormedField 𝕜] (E : Type u_1)
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : Type u)
  [TopologicalSpace M] [ChartedSpace E M] (c : 𝕜) :
  ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op ⊤)) :=
  ⟨fun x => c, ⋯⟩

def constSection (𝕜 : Type)
  [NontriviallyNormedField 𝕜]
  (E : Type u_1) [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] (M : Type u)
  [TopologicalSpace M] [ChartedSpace E M]
  (c : 𝕜) :
  ↑((structureSheaf 𝕜 E M).presheaf.obj
      (Opposite.op ⊤)) :=
  ⟨fun x => c, ⋯⟩

The constant section c over M.

defdefined in Hironaka/Manifold/StructureSheaf/Defs.lean

complete

def constHom (𝕜 : Type) [NontriviallyNormedField 𝕜] (E : Type u_1)
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : Type u)
  [TopologicalSpace M] [ChartedSpace E M] :
  𝕜 →+* ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op ⊤)) :=
  { toFun := constSection 𝕜 E M, map_one' := ⋯, map_mul' := ⋯,
    map_zero' := ⋯, map_add' := ⋯ }

def constHom (𝕜 : Type)
  [NontriviallyNormedField 𝕜]
  (E : Type u_1) [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] (M : Type u)
  [TopologicalSpace M]
  [ChartedSpace E M] :
  𝕜 →+*
    ↑((structureSheaf 𝕜 E M).presheaf.obj
        (Opposite.op ⊤)) :=
  { toFun := constSection 𝕜 E M,
    map_one' := ⋯, map_mul' := ⋯,
    map_zero' := ⋯, map_add' := ⋯ }

The constants as the 𝕜-algebra structure of 𝒪_M: the ring homomorphism 𝕜 →+* Γ(M, 𝒪_M), c ↦ the constant section c (the structure used when M is regarded as an analytic space over 𝕜).

defdefined in Hironaka/Manifold/StructureSheaf/Defs.lean

complete

def chartSection {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M]
  {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E)
  (hφ : φ ∈ IsManifold.maximalAtlas 𝓘(𝕜, E) ⊤ M) (i : Fin n) :
  ↑((structureSheaf 𝕜 E M).presheaf.obj
      (Opposite.op { carrier := φ.source, is_open' := ⋯ })) :=
  ⟨fun x => ψ (↑φ ↑x) i, ⋯⟩

def chartSection {𝕜 : Type} [RCLike 𝕜]
  (E : Type u_1) [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {M : Type u}
  [TopologicalSpace M] [ChartedSpace E M]
  {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜)
  (φ : OpenPartialHomeomorph M E)
  (hφ :
    φ ∈
      IsManifold.maximalAtlas 𝓘(𝕜, E) ⊤ M)
  (i : Fin n) :
  ↑((structureSheaf 𝕜 E M).presheaf.obj
      (Opposite.op
        { carrier := φ.source,
          is_open' := ⋯ })) :=
  ⟨fun x => ψ (↑φ ↑x) i, ⋯⟩

A chart φ of the maximal atlas with coordinates ψ: the coordinate function ψ_i ∘ φ as a section of 𝒪_M over the source of φ.

defdefined in Hironaka/Manifold/StructureSheaf/Defs.lean

complete

def coord {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M]
  {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E)
  (hφ : φ ∈ IsManifold.maximalAtlas 𝓘(𝕜, E) ⊤ M) {a : M}
  (ha : a ∈ φ.source) (i : Fin n) :
  ↑((structureSheaf 𝕜 E M).presheaf.stalk a) :=
  (CategoryTheory.ConcreteCategory.hom
      ((structureSheaf 𝕜 E M).presheaf.germ
        { carrier := φ.source, is_open' := ⋯ } a ha))
    (chartSection E ψ φ hφ i)

def coord {𝕜 : Type} [RCLike 𝕜] (E : Type u_1)
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {M : Type u} [TopologicalSpace M]
  [ChartedSpace E M] {n : ℕ}
  (ψ : E ≃L[𝕜] Fin n → 𝕜)
  (φ : OpenPartialHomeomorph M E)
  (hφ :
    φ ∈
      IsManifold.maximalAtlas 𝓘(𝕜, E) ⊤ M)
  {a : M} (ha : a ∈ φ.source)
  (i : Fin n) :
  ↑((structureSheaf 𝕜 E M).presheaf.stalk
      a) :=
  (CategoryTheory.ConcreteCategory.hom
      ((structureSheaf 𝕜 E
              M).presheaf.germ
        { carrier := φ.source,
          is_open' := ⋯ }
        a ha))
    (chartSection E ψ φ hφ i)

The coordinate germs x_i := ψ_i ∘ φ ∈ 𝒪_{M,a} of a chart φ of the maximal atlas containing a, with coordinates ψ.

defdefined in Hironaka/Manifold/StructureSheaf/Defs.lean

complete

def contMDiffSheaf.coeFun {𝕜 : Type} [NontriviallyNormedField 𝕜]
  {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM]
  {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4}
  [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞)
  {M : Type u} [TopologicalSpace M] [ChartedSpace HM M] (N : Type)
  [TopologicalSpace N] [ChartedSpace H N] (U : (Opens ↑↧M)ᵒᵖ) :
  CoeFun ((contMDiffSheaf IM I n M N).presheaf.obj U) fun x =>
    ↥(Opposite.unop U) → N

def contMDiffSheaf.coeFun {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {EM : Type u_1} [NormedAddCommGroup EM]
  [NormedSpace 𝕜 EM] {HM : Type u_2}
  [TopologicalSpace HM]
  (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_3} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {H : Type u_4}
  [TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H)
  (n : WithTop ℕ∞) {M : Type u}
  [TopologicalSpace M] [ChartedSpace HM M]
  (N : Type) [TopologicalSpace N]
  [ChartedSpace H N] (U : (Opens ↑↧M)ᵒᵖ) :
  CoeFun
    ((contMDiffSheaf IM I n M
            N).presheaf.obj
      U)
    fun x => ↥(Opposite.unop U) → N

defdefined in Hironaka/Manifold/StructureSheaf/Defs.lean

complete

def contMDiffSheafCommRing.coeFun {𝕜 : Type} [NontriviallyNormedField 𝕜]
  {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM]
  {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4}
  [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞)
  (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (R : Type)
  [CommRing R] [TopologicalSpace R] [ChartedSpace H R]
  [ContMDiffRing I n R] (U : (Opens ↑↧M)ᵒᵖ) :
  CoeFun ↑((contMDiffSheafCommRing IM I n M R).presheaf.obj U) fun x =>
    ↥(Opposite.unop U) → R

def contMDiffSheafCommRing.coeFun {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {EM : Type u_1} [NormedAddCommGroup EM]
  [NormedSpace 𝕜 EM] {HM : Type u_2}
  [TopologicalSpace HM]
  (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_3} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {H : Type u_4}
  [TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H)
  (n : WithTop ℕ∞) (M : Type u)
  [TopologicalSpace M] [ChartedSpace HM M]
  (R : Type) [CommRing R]
  [TopologicalSpace R] [ChartedSpace H R]
  [ContMDiffRing I n R]
  (U : (Opens ↑↧M)ᵒᵖ) :
  CoeFun
    ↑((contMDiffSheafCommRing IM I n M
              R).presheaf.obj
        U)
    fun x => ↥(Opposite.unop U) → R

defdefined in Hironaka/Manifold/StructureSheaf/Defs.lean

complete

def structureSheaf.coeFun (𝕜 : Type) [NontriviallyNormedField 𝕜]
  (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : Type u)
  [TopologicalSpace M] [ChartedSpace E M] (U : (Opens ↑↧M)ᵒᵖ) :
  CoeFun ↑((structureSheaf 𝕜 E M).presheaf.obj U) fun x =>
    ↥(Opposite.unop U) → 𝕜

def structureSheaf.coeFun (𝕜 : Type)
  [NontriviallyNormedField 𝕜]
  (E : Type u_1) [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] (M : Type u)
  [TopologicalSpace M] [ChartedSpace E M]
  (U : (Opens ↑↧M)ᵒᵖ) :
  CoeFun
    ↑((structureSheaf 𝕜 E M).presheaf.obj
        U)
    fun x => ↥(Opposite.unop U) → 𝕜

Definition3.1.2.2

uses 1

Used by 4

Reverse dependency previews

Preview

Definition 3.1.3.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

The stalk of the structure sheaf at a is identified with a subring of the ring of function germs at a: a section over a neighbourhood of a, extended by zero (extendBy0), has a germ (germAt); these form a cocone over the neighbourhoods (stalkToGermCocone), whence the ring map from the stalk to germs (stalkToGermHom, stalkToGerm), which is injective. Composition of germs with a map tending to the base point is a ring map (germCompRingHom); it underlies the stalk maps of analytic maps (Definition 3.1.3.2).

Lean code for Definition3.1.2.2●6 definitions

defdefined in Hironaka/Manifold/StructureSheaf/Defs.lean

complete

def extendBy0 {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1}
  [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2}
  [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) (n : WithTop ℕ∞)
  (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] {U : Opens M}
  (f :
    ↑((contMDiffSheafCommRing IM 𝓘(𝕜, 𝕜) n M 𝕜).presheaf.obj
        (Opposite.op U))) :
  M → 𝕜 :=
  if h : x ∈ U then ↑f ⟨x, h⟩ else 0

def extendBy0 {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {EM : Type u_1} [NormedAddCommGroup EM]
  [NormedSpace 𝕜 EM] {HM : Type u_2}
  [TopologicalSpace HM]
  (IM : ModelWithCorners 𝕜 EM HM)
  (n : WithTop ℕ∞) (M : Type u)
  [TopologicalSpace M] [ChartedSpace HM M]
  {U : Opens M}
  (f :
    ↑((contMDiffSheafCommRing IM 𝓘(𝕜, 𝕜) n
              M 𝕜).presheaf.obj
        (Opposite.op U))) :
  M → 𝕜 :=
  if h : x ∈ U then ↑f ⟨x, h⟩ else 0

The extension by zero of a C^n section over U (valued in 𝕜) to a function on M.

defdefined in Hironaka/Manifold/StructureSheaf/Defs.lean

complete

def germAt {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1}
  [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2}
  [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) (n : WithTop ℕ∞)
  (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (a : ↑↧M)
  (U : Opens M) (ha : a ∈ U) :
  ↑((contMDiffSheafCommRing IM 𝓘(𝕜, 𝕜) n M 𝕜).presheaf.obj
        (Opposite.op U)) →+*
    (𝓝 a).Germ 𝕜 :=
  { toFun := fun f => ↑(extendBy0 IM n M f), map_one' := ⋯,
    map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

def germAt {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {EM : Type u_1} [NormedAddCommGroup EM]
  [NormedSpace 𝕜 EM] {HM : Type u_2}
  [TopologicalSpace HM]
  (IM : ModelWithCorners 𝕜 EM HM)
  (n : WithTop ℕ∞) (M : Type u)
  [TopologicalSpace M] [ChartedSpace HM M]
  (a : ↑↧M) (U : Opens M) (ha : a ∈ U) :
  ↑((contMDiffSheafCommRing IM 𝓘(𝕜, 𝕜) n M
              𝕜).presheaf.obj
        (Opposite.op U)) →+*
    (𝓝 a).Germ 𝕜 :=
  {
    toFun := fun f =>
      ↑(extendBy0 IM n M f),
    map_one' := ⋯, map_mul' := ⋯,
    map_zero' := ⋯, map_add' := ⋯ }

The germ at a of the extension by zero, on the sections over an open neighbourhood U of a, as a ring homomorphism (on U ∈ 𝓝 a the extensions of sums and products are the pointwise sums and products).

defdefined in Hironaka/Manifold/StructureSheaf/Defs.lean

complete

def stalkToGermCocone {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1}
  [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2}
  [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) (n : WithTop ℕ∞)
  (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (a : ↑↧M) :
  CategoryTheory.Limits.Cocone
    ((OpenNhds.inclusion a).op.comp
      (contMDiffSheafCommRing IM 𝓘(𝕜, 𝕜) n M 𝕜).presheaf) :=
  { pt := ↧((𝓝 a).Germ 𝕜),
    ι :=
      {
        app := fun U =>
          CommRingCat.ofHom
            (germAt IM n M a
              ((OpenNhds.inclusion a).obj (Opposite.unop U)) ⋯),
        naturality := ⋯ } }

def stalkToGermCocone {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {EM : Type u_1} [NormedAddCommGroup EM]
  [NormedSpace 𝕜 EM] {HM : Type u_2}
  [TopologicalSpace HM]
  (IM : ModelWithCorners 𝕜 EM HM)
  (n : WithTop ℕ∞) (M : Type u)
  [TopologicalSpace M] [ChartedSpace HM M]
  (a : ↑↧M) :
  CategoryTheory.Limits.Cocone
    ((OpenNhds.inclusion a).op.comp
      (contMDiffSheafCommRing IM 𝓘(𝕜, 𝕜) n
          M 𝕜).presheaf) :=
  { pt := ↧((𝓝 a).Germ 𝕜),
    ι :=
      {
        app := fun U =>
          CommRingCat.ofHom
            (germAt IM n M a
              ((OpenNhds.inclusion a).obj
                (Opposite.unop U))
              ⋯),
        naturality := ⋯ } }

The cocone of the germs at a of the extensions by zero over the open neighbourhoods of a.

defdefined in Hironaka/Manifold/StructureSheaf/Defs.lean

complete

def stalkToGermHom {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1}
  [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2}
  [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) (n : WithTop ℕ∞)
  (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (a : ↑↧M) :
  (contMDiffSheafCommRing IM 𝓘(𝕜, 𝕜) n M 𝕜).presheaf.stalk a ⟶
    ↧((𝓝 a).Germ 𝕜) :=
  CategoryTheory.Limits.colimit.desc
    ((OpenNhds.inclusion a).op.comp
      (contMDiffSheafCommRing IM 𝓘(𝕜, 𝕜) n M 𝕜).presheaf)
    (stalkToGermCocone IM n M a)

def stalkToGermHom {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {EM : Type u_1} [NormedAddCommGroup EM]
  [NormedSpace 𝕜 EM] {HM : Type u_2}
  [TopologicalSpace HM]
  (IM : ModelWithCorners 𝕜 EM HM)
  (n : WithTop ℕ∞) (M : Type u)
  [TopologicalSpace M] [ChartedSpace HM M]
  (a : ↑↧M) :
  (contMDiffSheafCommRing IM 𝓘(𝕜, 𝕜) n M
            𝕜).presheaf.stalk
      a ⟶
    ↧((𝓝 a).Germ 𝕜) :=
  CategoryTheory.Limits.colimit.desc
    ((OpenNhds.inclusion a).op.comp
      (contMDiffSheafCommRing IM 𝓘(𝕜, 𝕜) n
          M 𝕜).presheaf)
    (stalkToGermCocone IM n M a)

The stalk as germs: the ring homomorphism 𝒪_{M,a} →+* Filter.Germ (𝓝 a) 𝕜 sending the germ of a section to the germ of its extension by zero, as a morphism of CommRingCat (the germ ring Filter.Germ (𝓝 a) 𝕜 lives in the universe of M).

defdefined in Hironaka/Manifold/StructureSheaf/Defs.lean

complete

def stalkToGerm {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1}
  [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2}
  [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) (n : WithTop ℕ∞)
  (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (a : M) :
  ↑((contMDiffSheafCommRing IM 𝓘(𝕜, 𝕜) n M 𝕜).presheaf.stalk a) →+*
    (𝓝 a).Germ 𝕜 :=
  CommRingCat.Hom.hom (stalkToGermHom IM n M a)

def stalkToGerm {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {EM : Type u_1} [NormedAddCommGroup EM]
  [NormedSpace 𝕜 EM] {HM : Type u_2}
  [TopologicalSpace HM]
  (IM : ModelWithCorners 𝕜 EM HM)
  (n : WithTop ℕ∞) (M : Type u)
  [TopologicalSpace M] [ChartedSpace HM M]
  (a : M) :
  ↑((contMDiffSheafCommRing IM 𝓘(𝕜, 𝕜) n M
              𝕜).presheaf.stalk
        a) →+*
    (𝓝 a).Germ 𝕜 :=
  CommRingCat.Hom.hom
    (stalkToGermHom IM n M a)

The stalk as germs, stalkToGerm : 𝒪_{M,a} →+* Filter.Germ (𝓝 a) 𝕜.

defdefined in Hironaka/Manifold/StructureSheaf/Defs.lean

complete

def germCompRingHom {𝕜 : Type} [NontriviallyNormedField 𝕜] {α : Type u_1}
  {β : Type u_2} {l : Filter α} {l' : Filter β} (g : α → β)
  (hg : Tendsto g l l') : l'.Germ 𝕜 →+* l.Germ 𝕜 :=
  { toFun := fun f => f.compTendsto g hg, map_one' := ⋯, map_mul' := ⋯,
    map_zero' := ⋯, map_add' := ⋯ }

def germCompRingHom {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {α : Type u_1} {β : Type u_2}
  {l : Filter α} {l' : Filter β}
  (g : α → β) (hg : Tendsto g l l') :
  l'.Germ 𝕜 →+* l.Germ 𝕜 :=
  { toFun := fun f => f.compTendsto g hg,
    map_one' := ⋯, map_mul' := ⋯,
    map_zero' := ⋯, map_add' := ⋯ }

Composition of germs of 𝕜-valued functions with a map g tending to the base point, as a ring homomorphism Filter.Germ l' 𝕜 →+* Filter.Germ l 𝕜 (Mathlib's Filter.Germ.compTendsto bundled; the stalk maps below, the chart transport and the coordinate change are its instances).

3.1.3. Ideal sheaves🔗

Definition3.1.3.1source[Hir64, Main Theorem II″(N), p. 158] ↗

uses 0

Used by 28

Reverse dependency previews

Preview

Definition 3.1.3.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

For a sheaf of commutative rings \mathcal{O} on a space X, Manifold.IdealSheaf 𝒪 is a locally finitely generated ideal sheaf: ideals of sections over every open set (carrier), closed under restriction (res_mem), satisfying the sheaf condition, whose stalk ideals (stalkIdealOf, stalkIdeal) are generated near every point by finitely many sections (HasLocalGenerators). This is Hironaka's "coherent sheaf of ideals", with "coherent" read as locally finitely generated.

An ideal sheaf can be given by its stalks: ofStalks builds it from a family of stalk ideals with local generators. The unit ideal ⊤, the zero ideal ⊥ and products J * J' are built this way (hasLocalGenerators_top, _bot, _mul and the instances instTop, instBot, instMul). The support V(J) = \{a : J_a \ne \mathcal{O}_a\} (support, Kollár's cosupport) is the set of points of the closed subspace defined by J; IsNonzeroEverywhere asks every stalk to be nonzero; and J.ord a is the order \nu_a(J) = \max\{p : J_a \subseteq \mathfrak m_a^p\}, the order IsLocalRing.ord of the stalk ideal (Definition 2.1.3.2).

Lean code for Definition3.1.3.1●13 declarations

structure(4 fields)defined in Hironaka/Manifold/IdealSheaf/Defs.lean

complete

structure IdealSheaf {X : TopCat} (𝒪 : TopCat.Sheaf CommRingCat X) : Type u

structure IdealSheaf {X : TopCat}
  (𝒪 : TopCat.Sheaf CommRingCat X) :
  Type u

A locally finitely generated ideal sheaf of the sheaf of rings 𝒪: a sub-presheaf of ideals satisfying the sheaf condition, whose stalk ideals are generated near every point by finitely many sections.

Fields

carrier : (U : Opens ↑X) → Ideal ↑(𝒪.presheaf.obj (Opposite.op U))

The ideal of sections over each open set.

res_mem : ∀ {U V : Opens ↑X} (i : U ⟶ V),
  ∀ f ∈ self.carrier V, (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.map i.op)) f ∈ self.carrier U

Restriction preserves the ideals (a sub-presheaf).

mem_of_locally : ∀ (U : Opens ↑X) (f : ↑(𝒪.presheaf.obj (Opposite.op U))),
  (∀ x ∈ U, ∃ V i, x ∈ V ∧ (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.map i.op)) f ∈ self.carrier V) →
    f ∈ self.carrier U

The sheaf condition of a sub-presheaf: a section locally in the ideal is in the ideal.

locallyFG : ∀ (a : ↑X),
  ∃ U,
    ∃ (_ : a ∈ U),
      ∃ k f,
        (∀ (i : Fin k), f i ∈ self.carrier U) ∧
          ∀ (b : ↑X) (hb : b ∈ U),
            stalkIdealOf 𝒪 self.carrier ⋯ b =
              Ideal.span (range fun i => (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ U b hb)) (f i))

Local finite generation.

abbrevdefined in Hironaka/Manifold/IdealSheaf/Defs.lean

complete

abbrev IdealSheaf.carrier {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X}
  (self : Manifold.IdealSheaf 𝒪) (U : Opens ↑X) :
  Ideal ↑(𝒪.presheaf.obj (Opposite.op U)) :=
  self.1

abbrev IdealSheaf.carrier {X : TopCat}
  {𝒪 : TopCat.Sheaf CommRingCat X}
  (self : Manifold.IdealSheaf 𝒪)
  (U : Opens ↑X) :
  Ideal ↑(𝒪.presheaf.obj (Opposite.op U)) :=
  self.1

The ideal of sections over each open set.

theoremdefined in Hironaka/Manifold/IdealSheaf/Defs.lean

complete

theorem IdealSheaf.res_mem {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X}
  (self : Manifold.IdealSheaf 𝒪) {U V : Opens ↑X} (i : U ⟶ V)
  (f : ↑(𝒪.presheaf.obj (Opposite.op V))) :
  f ∈ self.carrier V →
    (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.map i.op)) f ∈
      self.carrier U

theorem IdealSheaf.res_mem {X : TopCat}
  {𝒪 : TopCat.Sheaf CommRingCat X}
  (self : Manifold.IdealSheaf 𝒪)
  {U V : Opens ↑X} (i : U ⟶ V)
  (f :
    ↑(𝒪.presheaf.obj (Opposite.op V))) :
  f ∈ self.carrier V →
    (CategoryTheory.ConcreteCategory.hom
          (𝒪.presheaf.map i.op))
        f ∈
      self.carrier U

Restriction preserves the ideals (a sub-presheaf).

defdefined in Hironaka/Manifold/IdealSheaf/Defs.lean

complete

def stalkIdealOf {X : TopCat} (𝒪 : TopCat.Sheaf CommRingCat X)
  (carrier : (U : Opens ↑X) → Ideal ↑(𝒪.presheaf.obj (Opposite.op U)))
  (res_mem :
    ∀ {U V : Opens ↑X} (i : U ⟶ V),
      ∀ f ∈ carrier V,
        (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.map i.op)) f ∈
          carrier U)
  (b : ↑X) : Ideal ↑(𝒪.presheaf.stalk b) :=
  {
    carrier :=
      {s |
        ∃ V,
          ∃ (hb : b ∈ V),
            ∃ g ∈ carrier V,
              (CategoryTheory.ConcreteCategory.hom
                    (𝒪.presheaf.germ V b hb))
                  g =
                s},
    add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

def stalkIdealOf {X : TopCat}
  (𝒪 : TopCat.Sheaf CommRingCat X)
  (carrier :
    (U : Opens ↑X) →
      Ideal
        ↑(𝒪.presheaf.obj (Opposite.op U)))
  (res_mem :
    ∀ {U V : Opens ↑X} (i : U ⟶ V),
      ∀ f ∈ carrier V,
        (CategoryTheory.ConcreteCategory.hom
              (𝒪.presheaf.map i.op))
            f ∈
          carrier U)
  (b : ↑X) : Ideal ↑(𝒪.presheaf.stalk b) :=
  {
    carrier :=
      {s |
        ∃ V,
          ∃ (hb : b ∈ V),
            ∃ g ∈ carrier V,
              (CategoryTheory.ConcreteCategory.hom
                    (𝒪.presheaf.germ V b
                      hb))
                  g =
                s},
    add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }

The stalk ideal at b of a family of ideals of sections closed under restriction: the germs at b of the sections of the ideals (an ideal by common refinement of the open sets).

abbrevdefined in Hironaka/Manifold/IdealSheaf/Defs.lean

complete

abbrev IdealSheaf.stalkIdeal {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X}
  (J : Manifold.IdealSheaf 𝒪) (b : ↑X) : Ideal ↑(𝒪.presheaf.stalk b) :=
  stalkIdealOf 𝒪 J.carrier ⋯ b

abbrev IdealSheaf.stalkIdeal {X : TopCat}
  {𝒪 : TopCat.Sheaf CommRingCat X}
  (J : Manifold.IdealSheaf 𝒪) (b : ↑X) :
  Ideal ↑(𝒪.presheaf.stalk b) :=
  stalkIdealOf 𝒪 J.carrier ⋯ b

The stalk ideal J_b ⊆ 𝒪_b.

defdefined in Hironaka/Manifold/IdealSheaf/Defs.lean

complete

def IdealSheaf.HasLocalGenerators {X : TopCat}
  {𝒪 : TopCat.Sheaf CommRingCat X}
  (I : (x : ↑X) → Ideal ↑(𝒪.presheaf.stalk x)) : Prop :=
  ∀ (a : ↑X),
    ∃ U,
      ∃ (_ : a ∈ U),
        ∃ ι x f,
          ∀ (b : ↑X) (hb : b ∈ U),
            I b =
              Ideal.span
                (range fun i =>
                  (CategoryTheory.ConcreteCategory.hom
                      (𝒪.presheaf.germ U b hb))
                    (f i))

def IdealSheaf.HasLocalGenerators {X : TopCat}
  {𝒪 : TopCat.Sheaf CommRingCat X}
  (I :
    (x : ↑X) →
      Ideal ↑(𝒪.presheaf.stalk x)) :
  Prop :=
  ∀ (a : ↑X),
    ∃ U,
      ∃ (_ : a ∈ U),
        ∃ ι x f,
          ∀ (b : ↑X) (hb : b ∈ U),
            I b =
              Ideal.span
                (range fun i =>
                  (CategoryTheory.ConcreteCategory.hom
                      (𝒪.presheaf.germ U b
                        hb))
                    (f i))

A family of stalk ideals has local generators when every point has an open neighbourhood and finitely many sections over it whose germs span the ideals at every point of it.

defdefined in Hironaka/Manifold/IdealSheaf/Defs.lean

complete

def IdealSheaf.ofStalks {X : TopCat} (𝒪 : TopCat.Sheaf CommRingCat X)
  (I : (x : ↑X) → Ideal ↑(𝒪.presheaf.stalk x))
  (hI : IdealSheaf.HasLocalGenerators I) : Manifold.IdealSheaf 𝒪 :=
  {
    carrier := fun U =>
      ⨅ x,
        ⨅ (hx : x ∈ U),
          Ideal.comap (CommRingCat.Hom.hom (𝒪.presheaf.germ U x hx))
            (I x),
    res_mem := ⋯, mem_of_locally := ⋯, locallyFG := ⋯ }

def IdealSheaf.ofStalks {X : TopCat}
  (𝒪 : TopCat.Sheaf CommRingCat X)
  (I :
    (x : ↑X) →
      Ideal ↑(𝒪.presheaf.stalk x))
  (hI : IdealSheaf.HasLocalGenerators I) :
  Manifold.IdealSheaf 𝒪 :=
  {
    carrier := fun U =>
      ⨅ x,
        ⨅ (hx : x ∈ U),
          Ideal.comap
            (CommRingCat.Hom.hom
              (𝒪.presheaf.germ U x hx))
            (I x),
    res_mem := ⋯, mem_of_locally := ⋯,
    locallyFG := ⋯ }

The ideal sheaf with prescribed stalk ideals: the sections whose germs lie in the stalk ideals.

defdefined in Hironaka/Manifold/IdealSheaf/Defs.lean

complete

def IdealSheaf.instTop {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} :
  Top (Manifold.IdealSheaf 𝒪)

def IdealSheaf.instTop {X : TopCat}
  {𝒪 : TopCat.Sheaf CommRingCat X} :
  Top (Manifold.IdealSheaf 𝒪)

defdefined in Hironaka/Manifold/IdealSheaf/Defs.lean

complete

def IdealSheaf.instBot {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} :
  Bot (Manifold.IdealSheaf 𝒪)

def IdealSheaf.instBot {X : TopCat}
  {𝒪 : TopCat.Sheaf CommRingCat X} :
  Bot (Manifold.IdealSheaf 𝒪)

defdefined in Hironaka/Manifold/IdealSheaf/Defs.lean

complete

def IdealSheaf.instMul {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} :
  Mul (Manifold.IdealSheaf 𝒪)

def IdealSheaf.instMul {X : TopCat}
  {𝒪 : TopCat.Sheaf CommRingCat X} :
  Mul (Manifold.IdealSheaf 𝒪)

defdefined in Hironaka/Manifold/IdealSheaf/Defs.lean

complete

def IdealSheaf.support {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X}
  (J : Manifold.IdealSheaf 𝒪) : Set ↑X :=
  {x | J.stalkIdeal x ≠ ⊤}

def IdealSheaf.support {X : TopCat}
  {𝒪 : TopCat.Sheaf CommRingCat X}
  (J : Manifold.IdealSheaf 𝒪) : Set ↑X :=
  {x | J.stalkIdeal x ≠ ⊤}

The cosupport V(J) = {a | J_a ≠ 𝒪_a}, the set of points of the closed subspace defined by J (Kollár's cosupp; [BM97, Introduction]).

defdefined in Hironaka/Manifold/IdealSheaf/Defs.lean

complete

def IdealSheaf.IsNonzeroEverywhere {X : TopCat}
  {𝒪 : TopCat.Sheaf CommRingCat X} (J : Manifold.IdealSheaf 𝒪) : Prop :=
  ∀ (x : ↑X), J.stalkIdeal x ≠ ⊥

def IdealSheaf.IsNonzeroEverywhere
  {X : TopCat}
  {𝒪 : TopCat.Sheaf CommRingCat X}
  (J : Manifold.IdealSheaf 𝒪) : Prop :=
  ∀ (x : ↑X), J.stalkIdeal x ≠ ⊥

Hironaka's "coherent sheaf of non-zero ideals" [Hir64, Main Theorem II''(N), p. 158]: every stalk is nonzero.

defdefined in Hironaka/Manifold/IdealSheaf/Defs.lean

complete

def IdealSheaf.ord {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X}
  [∀ (x : ↑X), IsLocalRing ↑(𝒪.presheaf.stalk x)]
  (J : Manifold.IdealSheaf 𝒪) (x : ↑X) : ℕ∞ :=
  IsLocalRing.ord (J.stalkIdeal x)

def IdealSheaf.ord {X : TopCat}
  {𝒪 : TopCat.Sheaf CommRingCat X}
  [∀ (x : ↑X),
      IsLocalRing ↑(𝒪.presheaf.stalk x)]
  (J : Manifold.IdealSheaf 𝒪) (x : ↑X) :
  ℕ∞ :=
  IsLocalRing.ord (J.stalkIdeal x)

The order ν_a(J) = max {p | J_a ⊆ 𝔪_a^p} of the ideal sheaf at a (Hironaka's ν(J_x) [Hir64, p. 133]; [Kol07, Definition 47]; [BM97, §3]): the Hironaka library's IsLocalRing.ord of the stalk ideal.

Definition3.1.3.2source[BM97, Theorem 1.10] ↗

Statement uses 3

Statement dependency previews

Preview

Definition 3.1.2.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 12

Reverse dependency previews

Preview

Definition 3.1.3.3

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

The pull-back \varphi^* J of an ideal sheaf along an analytic map is the ideal sheaf generated by the f \circ \varphi, f a section of J: Hironaka's total transform, Bierstone–Milman's \sigma^{-1}(I). It is built stalkwise: the stalk map of \varphi at b, s \mapsto s \circ \varphi (germMapOn, germMap), is defined through germ composition (stalkGermComp, with stalkGermComp_mem_range, stalkEquivRange, tendsto_of_contMDiffOn_of_eq), and the images of local generators are local generators (hasLocalGenerators_pullback).

Lean code for Definition3.1.3.2●5 definitions

defdefined in Hironaka/Manifold/IdealSheaf/Defs.lean

complete

def IdealSheaf.pullback {𝕜 : Type} [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u}
  [TopologicalSpace M] [ChartedSpace E M] {E' : Type u_2}
  [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v}
  [TopologicalSpace N] [ChartedSpace E' N] (φ : N → M)
  (hφ : ContMDiff 𝓘(𝕜, E') 𝓘(𝕜, E) ⊤ φ)
  (J : Manifold.IdealSheaf (structureSheaf 𝕜 E M)) :
  Manifold.IdealSheaf (structureSheaf 𝕜 E' N) :=
  IdealSheaf.ofStalks (structureSheaf 𝕜 E' N)
    (fun b => Ideal.map (germMap φ hφ b) (J.stalkIdeal (φ b))) ⋯

def IdealSheaf.pullback {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {M : Type u}
  [TopologicalSpace M] [ChartedSpace E M]
  {E' : Type u_2} [NormedAddCommGroup E']
  [NormedSpace 𝕜 E'] {N : Type v}
  [TopologicalSpace N] [ChartedSpace E' N]
  (φ : N → M)
  (hφ : ContMDiff 𝓘(𝕜, E') 𝓘(𝕜, E) ⊤ φ)
  (J :
    Manifold.IdealSheaf
      (structureSheaf 𝕜 E M)) :
  Manifold.IdealSheaf
    (structureSheaf 𝕜 E' N) :=
  IdealSheaf.ofStalks
    (structureSheaf 𝕜 E' N)
    (fun b =>
      Ideal.map (germMap φ hφ b)
        (J.stalkIdeal (φ b)))
    ⋯

The pullback φ^* J of an ideal sheaf under an analytic map, the ideal sheaf generated by the f ∘ φ, f a section of J (Hironaka's total transform [Hir64, pp. 141–142]; Bierstone–Milman's σ⁻¹(I) [BM97, Theorem 1.10]).

defdefined in Hironaka/Manifold/StructureSheaf/Defs.lean

complete

def germMapOn {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u}
  [TopologicalSpace M] [ChartedSpace E M] {E' : Type u_2}
  [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v}
  [TopologicalSpace N] [ChartedSpace E' N] (φ : N → M) {V : Opens N}
  (hφ : ContMDiffOn 𝓘(𝕜, E') 𝓘(𝕜, E) ⊤ φ ↑V) {b : N} (hb : b ∈ V)
  {c : M} (hc : φ b = c) :
  ↑((structureSheaf 𝕜 E M).presheaf.stalk c) →+*
    ↑((structureSheaf 𝕜 E' N).presheaf.stalk b) :=
  (stalkEquivRange b).symm.toRingHom.comp
    ((stalkGermComp φ hφ hb hc).codRestrict
      (stalkToGerm 𝓘(𝕜, E') ⊤ N b).range ⋯)

def germMapOn {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {M : Type u}
  [TopologicalSpace M] [ChartedSpace E M]
  {E' : Type u_2} [NormedAddCommGroup E']
  [NormedSpace 𝕜 E'] {N : Type v}
  [TopologicalSpace N] [ChartedSpace E' N]
  (φ : N → M) {V : Opens N}
  (hφ :
    ContMDiffOn 𝓘(𝕜, E') 𝓘(𝕜, E) ⊤ φ ↑V)
  {b : N} (hb : b ∈ V) {c : M}
  (hc : φ b = c) :
  ↑((structureSheaf 𝕜 E M).presheaf.stalk
        c) →+*
    ↑((structureSheaf 𝕜 E'
              N).presheaf.stalk
        b) :=
  (stalkEquivRange b).symm.toRingHom.comp
    ((stalkGermComp φ hφ hb
          hc).codRestrict
      (stalkToGerm 𝓘(𝕜, E') ⊤ N b).range
      ⋯)

The stalk map of an analytic map φ, analytic on the open V ∋ b, with φ b = c: the ring homomorphism 𝒪_{M,c} →+* 𝒪_{N,b}, s ↦ s ∘ φ.

abbrevdefined in Hironaka/Manifold/StructureSheaf/Defs.lean

complete

abbrev germMap {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u}
  [TopologicalSpace M] [ChartedSpace E M] {E' : Type u_2}
  [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v}
  [TopologicalSpace N] [ChartedSpace E' N] (φ : N → M)
  (hφ : ContMDiff 𝓘(𝕜, E') 𝓘(𝕜, E) ⊤ φ) (b : N) :
  ↑((structureSheaf 𝕜 E M).presheaf.stalk (φ b)) →+*
    ↑((structureSheaf 𝕜 E' N).presheaf.stalk b) :=
  germMapOn φ ⋯ ⋯ ⋯

abbrev germMap {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {M : Type u}
  [TopologicalSpace M] [ChartedSpace E M]
  {E' : Type u_2} [NormedAddCommGroup E']
  [NormedSpace 𝕜 E'] {N : Type v}
  [TopologicalSpace N] [ChartedSpace E' N]
  (φ : N → M)
  (hφ : ContMDiff 𝓘(𝕜, E') 𝓘(𝕜, E) ⊤ φ)
  (b : N) :
  ↑((structureSheaf 𝕜 E M).presheaf.stalk
        (φ b)) →+*
    ↑((structureSheaf 𝕜 E'
              N).presheaf.stalk
        b) :=
  germMapOn φ ⋯ ⋯ ⋯

The stalk map 𝒪_{M, φ b} →+* 𝒪_{N, b} of a global analytic map.

defdefined in Hironaka/Manifold/StructureSheaf/Defs.lean

complete

def stalkGermComp {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u}
  [TopologicalSpace M] [ChartedSpace E M] {E' : Type u_2}
  [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v}
  [TopologicalSpace N] [ChartedSpace E' N] (φ : N → M) {V : Opens N}
  (hφ : ContMDiffOn 𝓘(𝕜, E') 𝓘(𝕜, E) ⊤ φ ↑V) {b : N} (hb : b ∈ V)
  {c : M} (hc : φ b = c) :
  ↑((structureSheaf 𝕜 E M).presheaf.stalk c) →+* (𝓝 b).Germ 𝕜 :=
  (germCompRingHom φ ⋯).comp (stalkToGerm 𝓘(𝕜, E) ⊤ M c)

def stalkGermComp {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {M : Type u}
  [TopologicalSpace M] [ChartedSpace E M]
  {E' : Type u_2} [NormedAddCommGroup E']
  [NormedSpace 𝕜 E'] {N : Type v}
  [TopologicalSpace N] [ChartedSpace E' N]
  (φ : N → M) {V : Opens N}
  (hφ :
    ContMDiffOn 𝓘(𝕜, E') 𝓘(𝕜, E) ⊤ φ ↑V)
  {b : N} (hb : b ∈ V) {c : M}
  (hc : φ b = c) :
  ↑((structureSheaf 𝕜 E M).presheaf.stalk
        c) →+*
    (𝓝 b).Germ 𝕜 :=
  (germCompRingHom φ ⋯).comp
    (stalkToGerm 𝓘(𝕜, E) ⊤ M c)

The germ at c = φ b of a section of 𝒪_M, composed with φ, as a germ at b.

defdefined in Hironaka/Manifold/StructureSheaf/Defs.lean

complete

def stalkEquivRange {𝕜 : Type} [NontriviallyNormedField 𝕜] {E' : Type u_2}
  [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v}
  [TopologicalSpace N] [ChartedSpace E' N] (b : N) :
  ↑((structureSheaf 𝕜 E' N).presheaf.stalk b) ≃+*
    ↥(stalkToGerm 𝓘(𝕜, E') ⊤ N b).range :=
  RingEquiv.ofBijective (stalkToGerm 𝓘(𝕜, E') ⊤ N b).rangeRestrict ⋯

def stalkEquivRange {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {E' : Type u_2} [NormedAddCommGroup E']
  [NormedSpace 𝕜 E'] {N : Type v}
  [TopologicalSpace N] [ChartedSpace E' N]
  (b : N) :
  ↑((structureSheaf 𝕜 E' N).presheaf.stalk
        b) ≃+*
    ↥(stalkToGerm 𝓘(𝕜, E') ⊤ N b).range :=
  RingEquiv.ofBijective
    (stalkToGerm 𝓘(𝕜, E') ⊤ N
        b).rangeRestrict
    ⋯

The stalk as its own image in the germs, a ring isomorphism.

Definition3.1.3.3source[Hir64, Main Theorem II″(N), p. 158] ↗

Statement uses 3

Statement dependency previews

Preview

Definition 3.1.1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 20

Reverse dependency previews

Preview

Definition 3.1.4.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

The statements use the names of AnalyticManifold: IdealSheaf M is a locally finitely generated ideal sheaf of the structure sheaf of M, whose stalk rings are stalkRing M x. Closed analytic subspaces (centres, boundaries) are given by their ideal sheaves. The operations are the inverse image f^{-1}(J) \cdot \mathcal{O}_M along an analytic map (J.pullback f f.contMDiff) and the restriction J|_U to an open set (J.restrict U); the unit ideal sheaf \mathcal{O}_M (⊤), products, the set of points J.support (the cosupport) and Hironaka's order \nu(J_x) (J.ord x) are those of the general ideal sheaves (Definition 3.1.3.1). The predicates are:

IsNonzeroEverywhere (of the general ideal sheaves): every stalk is nonzero, Hironaka's "sheaf of non-zero ideals";
IsNonsingular: every point of the subspace is simple, \mathcal{O}_{M,x}/J_x regular; vacuous on the empty subspace;
IsReduced: the subspace is reduced, every stalk J_x a radical ideal.

J.regularLocus is the set of simple points of the subspace, the points at which \mathcal{O}_{M,x}/J_x is a regular local ring: Włodarczyk's \operatorname{Reg}(Y) [Wlo09, Theorem 2.0.2 (2)]. A point off the subspace is not in it, the zero ring not being local, and J.IsNonsingular holds exactly when the support lies in the simple locus.

Hironaka's "reduced" and "everywhere of codimension one" for the boundary are not hypotheses of Main Theorem II″(N): they follow from the simple normal crossings hypothesis IsSncBoundary (Definition 3.1.5.1, Theorem 4.3.1.2). IsReduced is the hypothesis on the embedded subspace of Włodarczyk's embedded desingularization (Theorem 4.3.4.6).

Lean code for Definition3.1.3.3●7 definitions

abbrevdefined in Hironaka/Manifold/IdealSheaf/Defs.lean

complete

abbrev IdealSheaf {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : AnalyticManifold 𝕜 E) :
  Type u :=
  Manifold.IdealSheaf (structureSheaf 𝕜 E M.carrier)

abbrev IdealSheaf {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E]
  (M : AnalyticManifold 𝕜 E) : Type u :=
  Manifold.IdealSheaf
    (structureSheaf 𝕜 E M.carrier)

A locally finitely generated ideal sheaf of the sheaf of analytic functions on M: Hironaka's "coherent sheaf of ideals" on a non-singular analytic space [Hir64, Main Theorem II''(N), p. 158]. Closed analytic subspaces of M (centres, boundaries) are given by their ideal sheaves.

abbrevdefined in Hironaka/Manifold/IdealSheaf/Defs.lean

complete

abbrev IdealSheaf.stalkRing {𝕜 : Type} [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  (M : AnalyticManifold 𝕜 E) (x : M.carrier) : Type u :=
  ↑((structureSheaf 𝕜 E M.carrier).presheaf.stalk x)

abbrev IdealSheaf.stalkRing {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E]
  (M : AnalyticManifold 𝕜 E)
  (x : M.carrier) : Type u :=
  ↑((structureSheaf 𝕜 E
            M.carrier).presheaf.stalk
      x)

The stalk 𝒪_{M,x} of the sheaf of analytic functions at x, named so that the predicates below can speak of it.

defdefined in Hironaka/Manifold/IdealSheaf/Defs.lean

complete

def IdealSheaf.pullback {𝕜 : Type} [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u}
  [TopologicalSpace M] [ChartedSpace E M] {E' : Type u_2}
  [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v}
  [TopologicalSpace N] [ChartedSpace E' N] (φ : N → M)
  (hφ : ContMDiff 𝓘(𝕜, E') 𝓘(𝕜, E) ⊤ φ)
  (J : Manifold.IdealSheaf (structureSheaf 𝕜 E M)) :
  Manifold.IdealSheaf (structureSheaf 𝕜 E' N) :=
  IdealSheaf.ofStalks (structureSheaf 𝕜 E' N)
    (fun b => Ideal.map (germMap φ hφ b) (J.stalkIdeal (φ b))) ⋯

def IdealSheaf.pullback {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {M : Type u}
  [TopologicalSpace M] [ChartedSpace E M]
  {E' : Type u_2} [NormedAddCommGroup E']
  [NormedSpace 𝕜 E'] {N : Type v}
  [TopologicalSpace N] [ChartedSpace E' N]
  (φ : N → M)
  (hφ : ContMDiff 𝓘(𝕜, E') 𝓘(𝕜, E) ⊤ φ)
  (J :
    Manifold.IdealSheaf
      (structureSheaf 𝕜 E M)) :
  Manifold.IdealSheaf
    (structureSheaf 𝕜 E' N) :=
  IdealSheaf.ofStalks
    (structureSheaf 𝕜 E' N)
    (fun b =>
      Ideal.map (germMap φ hφ b)
        (J.stalkIdeal (φ b)))
    ⋯

abbrevdefined in Hironaka/Manifold/IdealSheaf/Defs.lean

complete

abbrev IdealSheaf.restrict {𝕜 : Type} [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {M : AnalyticManifold 𝕜 E} (J : M.IdealSheaf) (U : Opens M.carrier) :
  (M.restrict U).IdealSheaf :=
  IdealSheaf.pullback ⇑(M.inclusion U) ⋯ J

abbrev IdealSheaf.restrict {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E]
  {M : AnalyticManifold 𝕜 E}
  (J : M.IdealSheaf)
  (U : Opens M.carrier) :
  (M.restrict U).IdealSheaf :=
  IdealSheaf.pullback ⇑(M.inclusion U) ⋯ J

The restriction J|_U of an ideal sheaf to an open subset: the inverse image ideal sheaf along the inclusion (along an open embedding the inverse image is the restriction, the stalks at the points of U being those of J).

defdefined in Hironaka/Manifold/IdealSheaf/Defs.lean

complete

def IdealSheaf.IsNonsingular {𝕜 : Type} [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {M : AnalyticManifold 𝕜 E} (J : M.IdealSheaf) : Prop :=
  ∀ x ∈ IdealSheaf.support J,
    IsRegularLocalRing
      (IdealSheaf.stalkRing M x ⧸ IdealSheaf.stalkIdeal J x)

def IdealSheaf.IsNonsingular {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E]
  {M : AnalyticManifold 𝕜 E}
  (J : M.IdealSheaf) : Prop :=
  ∀ x ∈ IdealSheaf.support J,
    IsRegularLocalRing
      (IdealSheaf.stalkRing M x ⧸
        IdealSheaf.stalkIdeal J x)

The closed analytic subspace defined by J is non-singular: every point of it is simple, i.e. the local ring 𝒪_{M,x}/J_x is regular [Hir64, p. 121] (Hironaka: by the Jacobian criterion and the implicit function theorem, a simple point has a neighbourhood isomorphic to an open subset of 𝕜ⁿ). Vacuous on the empty subspace.

defdefined in Hironaka/Manifold/IdealSheaf/Defs.lean

complete

def IdealSheaf.IsReduced {𝕜 : Type} [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {M : AnalyticManifold 𝕜 E} (J : M.IdealSheaf) : Prop :=
  ∀ (x : M.carrier), (IdealSheaf.stalkIdeal J x).IsRadical

def IdealSheaf.IsReduced {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E]
  {M : AnalyticManifold 𝕜 E}
  (J : M.IdealSheaf) : Prop :=
  ∀ (x : M.carrier),
    (IdealSheaf.stalkIdeal J x).IsRadical

The closed analytic subspace defined by J is reduced: its structure sheaf 𝒪_M/J has no nilpotent elements [Hir64, p. 111], i.e. every stalk J_x is a radical ideal (𝓘_{X_red} = √𝓘_X, [BM97, Remark 3.14]).

defdefined in Hironaka/Manifold/IdealSheaf/Defs.lean

complete

def IdealSheaf.regularLocus {𝕜 : Type} [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {M : AnalyticManifold 𝕜 E} (J : M.IdealSheaf) : Set M.carrier :=
  {x |
    IsRegularLocalRing
      (IdealSheaf.stalkRing M x ⧸ IdealSheaf.stalkIdeal J x)}

def IdealSheaf.regularLocus {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E]
  {M : AnalyticManifold 𝕜 E}
  (J : M.IdealSheaf) : Set M.carrier :=
  {x |
    IsRegularLocalRing
      (IdealSheaf.stalkRing M x ⧸
        IdealSheaf.stalkIdeal J x)}

The simple locus Reg(Y) of the closed analytic subspace Y defined by J: the points x at which the local ring 𝒪_{M,x}/J_x of Y is regular, Hironaka's simple points of Y [Hir64, p. 121] and Włodarczyk's "set Reg(Y) of points where Y is smooth" [Wlo09, Theorem 2.0.2 (2)]. A point off Y is not in it: there J_x = 𝒪_{M,x}, and the zero ring is not local, so not regular. J is non-singular (IsNonsingular) exactly when its support lies in its simple locus.

Definition3.1.3.4source[Hir64, Main Theorem II′(N) (iii), p. 156] ↗

uses 1

Used by 4

Reverse dependency previews

Preview

Definition 3.1.4.3

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

A function germ at x vanishes on Z if some representative is zero on Z near x (Germ.VanishesOn); such germs form an ideal (vanishingGermIdeal), and its trace on the stalk of the structure sheaf is the vanishing ideal vanishingStalk Z x. These are the stalks of Hironaka's reduced structure \mathrm{red} on a closed set, used for boundaries (Definition 3.1.4.3, Definition 3.1.5.1).

Lean code for Definition3.1.3.4●3 definitions

defdefined in Hironaka/Manifold/IdealSheaf/Defs.lean

complete

def Germ.VanishesOn {𝕜 : Type} [NontriviallyNormedField 𝕜] {M : Type u_1}
  [TopologicalSpace M] (Z : Set M) (x : M) (g : (𝓝 x).Germ 𝕜) : Prop :=
  g.liftOn (fun f => ∀ᶠ (y : M) in 𝓝[Z] x, f y = 0) ⋯

def Germ.VanishesOn {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {M : Type u_1} [TopologicalSpace M]
  (Z : Set M) (x : M) (g : (𝓝 x).Germ 𝕜) :
  Prop :=
  g.liftOn
    (fun f =>
      ∀ᶠ (y : M) in 𝓝[Z] x, f y = 0)
    ⋯

The function germ g at x vanishes on Z near x: some (equivalently every) representative is zero on Z ∩ N for a neighbourhood N of x.

defdefined in Hironaka/Manifold/IdealSheaf/Defs.lean

complete

def vanishingGermIdeal {𝕜 : Type} [NontriviallyNormedField 𝕜] {M : Type u_1}
  [TopologicalSpace M] (Z : Set M) (x : M) : Ideal ((𝓝 x).Germ 𝕜) :=
  { carrier := {g | Germ.VanishesOn Z x g}, add_mem' := ⋯,
    zero_mem' := ⋯, smul_mem' := ⋯ }

def vanishingGermIdeal {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {M : Type u_1} [TopologicalSpace M]
  (Z : Set M) (x : M) :
  Ideal ((𝓝 x).Germ 𝕜) :=
  {
    carrier :=
      {g | Germ.VanishesOn Z x g},
    add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }

The function germs at x vanishing on Z near x form an ideal of the germ ring.

defdefined in Hironaka/Manifold/IdealSheaf/Defs.lean

complete

def vanishingStalk {𝕜 : Type} [NontriviallyNormedField 𝕜] {M : Type u_1}
  [TopologicalSpace M] {E : Type u_2} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] [ChartedSpace E M] (Z : Set M) (x : M) :
  Ideal ↑((structureSheaf 𝕜 E M).presheaf.stalk x) :=
  Ideal.comap (stalkToGerm 𝓘(𝕜, E) ⊤ M x) (vanishingGermIdeal Z x)

def vanishingStalk {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {M : Type u_1} [TopologicalSpace M]
  {E : Type u_2} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] [ChartedSpace E M]
  (Z : Set M) (x : M) :
  Ideal
    ↑((structureSheaf 𝕜 E
              M).presheaf.stalk
        x) :=
  Ideal.comap (stalkToGerm 𝓘(𝕜, E) ⊤ M x)
    (vanishingGermIdeal Z x)

The vanishing ideal of Z at x: the germs of analytic functions at x (stalk of 𝒪_M) whose function germ vanishes on Z near x; the stalk of Hironaka's reduced structure red on the closed set Z [Hir64, Main Theorem II'(N) (iii), p. 156]. It depends on Z only through closure Z (a continuous germ vanishing on Z near x vanishes on closure Z near x); it is applied to closed sets.

3.1.4. Closed submanifolds and blow-ups🔗

Definition3.1.4.1

Statement uses 2

Statement dependency previews

Preview

Definition 3.1.2.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 5

Reverse dependency previews

Preview

Definition 3.1.4.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Fix linear coordinates \psi \colon E \cong \mathbb{K}^n. A chart \varphi is adapted to Y (IsAdaptedChart) if on its source Y is a coordinate subspace \{z_\sigma = 0\} of the coordinates \psi \circ \varphi. A closed submanifold of codimension c (IsClosedSubmanifold ψ Y c) is a closed set with an adapted chart at each of its points. Its ideal sheaf is specified by IsIdealSheafOf (cosupport Y, stalks at the points of Y spanned by the adapted coordinates) and chosen by IsClosedSubmanifold.idealSheaf (the unit ideal sheaf if none exists; existence and uniqueness are lemmas of the library).

Lean code for Definition3.1.4.1●4 definitions

defdefined in Hironaka/Manifold/Submanifold/Defs.lean

complete

def IsAdaptedChart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u}
  [TopologicalSpace M] [ChartedSpace E M] {n : ℕ}
  (ψ : E ≃L[𝕜] Fin n → 𝕜) (Y : Set M) (φ : OpenPartialHomeomorph M E)
  {c : ℕ} (σ : Fin c ↪ Fin n) : Prop :=
  φ ∈ IsManifold.maximalAtlas 𝓘(𝕜, E) ⊤ M ∧
    ∀ x ∈ φ.source, x ∈ Y ↔ ∀ (i : Fin c), ψ (↑φ x) (σ i) = 0

def IsAdaptedChart {𝕜 : Type} [RCLike 𝕜]
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {M : Type u}
  [TopologicalSpace M] [ChartedSpace E M]
  {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜)
  (Y : Set M)
  (φ : OpenPartialHomeomorph M E) {c : ℕ}
  (σ : Fin c ↪ Fin n) : Prop :=
  φ ∈
      IsManifold.maximalAtlas 𝓘(𝕜, E) ⊤
        M ∧
    ∀ x ∈ φ.source,
      x ∈ Y ↔
        ∀ (i : Fin c), ψ (↑φ x) (σ i) = 0

An adapted chart for Y: a chart φ of the maximal atlas on whose source Y is the coordinate subspace {z_σ = 0} of the coordinates ψ ∘ φ.

structure(2 fields)defined in Hironaka/Manifold/Submanifold/Defs.lean

complete

structure IsClosedSubmanifold {𝕜 : Type} [RCLike 𝕜] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u}
  [TopologicalSpace M] [ChartedSpace E M] {n : ℕ}
  (ψ : E ≃L[𝕜] Fin n → 𝕜) (Y : Set M) (c : ℕ) : Prop

structure IsClosedSubmanifold {𝕜 : Type} [RCLike 𝕜]
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {M : Type u}
  [TopologicalSpace M] [ChartedSpace E M]
  {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜)
  (Y : Set M) (c : ℕ) : Prop

A closed analytic submanifold of codimension c: a closed set with an adapted chart at each of its points [BM88, Definition 4.1 (2)].

Fields

isClosed : IsClosed Y

exists_adaptedChart : ∀ a ∈ Y, ∃ φ σ, a ∈ φ.source ∧ IsAdaptedChart ψ Y φ σ

defdefined in Hironaka/Manifold/Submanifold/Defs.lean

complete

def IsIdealSheafOf {𝕜 : 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 : Manifold.IdealSheaf (structureSheaf 𝕜 E M)) : Prop :=
  J.support = Y ∧
    ∀ (φ : OpenPartialHomeomorph M E) (σ : Fin c ↪ Fin n)
      (hφ : IsAdaptedChart ψ Y φ σ) (a : M) (ha : a ∈ φ.source),
      a ∈ Y →
        J.stalkIdeal a =
          Ideal.span (range fun i => coord E ψ φ ⋯ ha (σ i))

def IsIdealSheafOf {𝕜 : 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 :
    Manifold.IdealSheaf
      (structureSheaf 𝕜 E M)) :
  Prop :=
  J.support = Y ∧
    ∀ (φ : OpenPartialHomeomorph M E)
      (σ : Fin c ↪ Fin n)
      (hφ : IsAdaptedChart ψ Y φ σ)
      (a : M) (ha : a ∈ φ.source),
      a ∈ Y →
        J.stalkIdeal a =
          Ideal.span
            (range fun i =>
              coord E ψ φ ⋯ ha (σ i))

J is the ideal sheaf of the closed submanifold Y: its cosupport is Y and, at every point of Y in an adapted chart φ with indices σ, its stalk is spanned by the germs of the adapted coordinates x_{σ i} = ψ_{σ i} ∘ φ.

defdefined in Hironaka/Manifold/Submanifold/Defs.lean

complete

def IsClosedSubmanifold.idealSheaf {𝕜 : 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 : ℕ}
  (_hY : IsClosedSubmanifold ψ Y c) :
  Manifold.IdealSheaf (structureSheaf 𝕜 E M) :=
  if h : ∃ J, IsIdealSheafOf ψ Y c J then Classical.choose h else ⊤

def IsClosedSubmanifold.idealSheaf {𝕜 : 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 : ℕ}
  (_hY : IsClosedSubmanifold ψ Y c) :
  Manifold.IdealSheaf
    (structureSheaf 𝕜 E M) :=
  if h : ∃ J, IsIdealSheafOf ψ Y c J then
    Classical.choose h
  else ⊤

The ideal sheaf I_Y of a closed submanifold: the unique ideal sheaf satisfying the specification IsIdealSheafOf ψ Y c (cosupport Y, stalks spanned by the adapted coordinates), when one exists; the unit ideal sheaf otherwise. Existence and uniqueness are proved in Hironaka.Manifold.BlowUp.Transform.Object.

Definition3.1.4.2

Statement uses 2

Statement dependency previews

Preview

Definition 3.1.1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 3

Reverse dependency previews

Preview

Definition 3.1.4.3

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Blow-ups of manifolds are characterized rather than constructed, following Bierstone–Milman's definition of blowing up [BM88, Definition 4.1]. IsBlowUp ψ Y c π says that \pi \colon M' \to M is the blowing-up of M with centre the closed submanifold Y: M' is an analytic manifold, \pi is proper and analytic (IsBlowUp.contMDiff), (1) \pi is an analytic isomorphism M' \setminus \pi^{-1}(Y) \to M \setminus Y, and (2) over every adapted chart of Y the standard blow-up charts exist and cover \pi^{-1}(U). A blow-up chart of index i (IsBlowUpChart) is a chart \Phi of M' in which \pi reads as the model map blowUpChartMap σ i: the i-th coordinate of the block is the scaling variable and the other block coordinates are ratios multiplied by it. The ideal of the exceptional divisor, I_F = \pi^* I_Y, is the pull-back hY.idealSheaf.pullback π h.contMDiff along the blow-up.

AnalyticMap.IsMonoidalTransformation f D is the form used in the statements: for some coordinates and codimension, the cosupport of D is a closed submanifold, D is its ideal sheaf, and f is a blowing-up with that centre. The coordinates are existential inside the predicate, so the statements carry no model isomorphism.

Lean code for Definition3.1.4.2●5 declarations

defdefined in Hironaka/Manifold/BlowUp/Defs.lean

complete

def blowUpChartMap {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n)
  (i : Fin c) : (Fin n → 𝕜) → Fin n → 𝕜 :=
  if ∃ k, k ≠ i ∧ σ k = j then u (σ i) * u j else u j

def blowUpChartMap {𝕜 : Type} [RCLike 𝕜]
  {n c : ℕ} (σ : Fin c ↪ Fin n)
  (i : Fin c) : (Fin n → 𝕜) → Fin n → 𝕜 :=
  if ∃ k, k ≠ i ∧ σ k = j then
    u (σ i) * u j
  else u j

The chart map π_i of the i-th blow-up chart in block form [BM88, Definition 4.1]: slot σ i is the scaling variable, the other block slots σ k are ratio variables multiplied by it, and the coordinates off the block pass through.

structure(4 fields)defined in Hironaka/Manifold/BlowUp/Defs.lean

complete

structure IsBlowUpChart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ}
  (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M]
  {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] (π : M' → M)
  (φ : OpenPartialHomeomorph M E) {c : ℕ} (σ : Fin c ↪ Fin n)
  (i : Fin c) (Φ : OpenPartialHomeomorph M' E) : Prop

structure IsBlowUpChart {𝕜 : Type} [RCLike 𝕜]
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {n : ℕ}
  (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u}
  [TopologicalSpace M] {M' : Type u}
  [TopologicalSpace M']
  [ChartedSpace E M'] (π : M' → M)
  (φ : OpenPartialHomeomorph M E) {c : ℕ}
  (σ : Fin c ↪ Fin n) (i : Fin c)
  (Φ : OpenPartialHomeomorph M' E) : Prop

Condition (2) of [BM88, Definition 4.1] in coordinates: Φ is a blow-up chart of index i over the chart φ of M with block indices σ, for the map π : M' → M, when it is a chart of the maximal atlas of M' with source inside π⁻¹(φ.source) and target the chart domain π_i⁻¹(ψ(φ.target)) of the local model, on which ψ ∘ φ ∘ π = π_i ∘ ψ ∘ Φ.

Fields

mem_maximalAtlas : Φ ∈ IsManifold.maximalAtlas 𝓘(𝕜, E) ⊤ M'

source_subset : Φ.source ⊆ π ⁻¹' φ.source

mem_target_iff : ∀ (v : E), v ∈ Φ.target ↔ blowUpChartMap σ i (ψ v) ∈ ⇑ψ '' φ.target

comm : ∀ p ∈ Φ.source, ψ (↑φ (π p)) = blowUpChartMap σ i (ψ (↑Φ p))

structure(6 fields)defined in Hironaka/Manifold/BlowUp/Defs.lean

complete

structure IsBlowUp {𝕜 : 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'] (Y : Set M) (c : ℕ)
  [IsManifold 𝓘(𝕜, E) ⊤ M'] [T2Space M'] [SecondCountableTopology M']
  (π : M' → M) : Prop

structure IsBlowUp {𝕜 : 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'] (Y : Set M) (c : ℕ)
  [IsManifold 𝓘(𝕜, E) ⊤ M'] [T2Space M']
  [SecondCountableTopology M']
  (π : M' → M) : Prop

π : M' → M is the blowing-up of M with centre Y [BM88, Definition 4.1], for Y a closed submanifold of codimension c (the hypotheses on Y are carried by the theorems, not by this predicate): M' is an analytic manifold (Hausdorff, second countable), π is proper and analytic, (1) π restricts to an analytic isomorphism M' ∖ π⁻¹(Y) → M ∖ Y, and (2) over every adapted chart of Y the blow-up charts of every index exist and their sources cover π⁻¹(U).

Fields

contMDiff : ContMDiff 𝓘(𝕜, E) 𝓘(𝕜, E) ⊤ π

isProperMap : IsProperMap π

isLocalDiffeomorphOn_compl : IsLocalDiffeomorphOn 𝓘(𝕜, E) 𝓘(𝕜, E) ⊤ π (π ⁻¹' Yᶜ)

bijOn_compl : BijOn π (π ⁻¹' Yᶜ) Yᶜ

exists_chart : ∀ (φ : OpenPartialHomeomorph M E) (σ : Fin c ↪ Fin n),
  IsAdaptedChart ψ Y φ σ → ∀ (i : Fin c), ∃ Φ, IsBlowUpChart ψ π φ σ i Φ

cover : ∀ (φ : OpenPartialHomeomorph M E) (σ : Fin c ↪ Fin n),
  IsAdaptedChart ψ Y φ σ → ∀ (p : M'), π p ∈ φ.source → ∃ i Φ, IsBlowUpChart ψ π φ σ i Φ ∧ p ∈ Φ.source

theoremdefined in Hironaka/Manifold/BlowUp/Defs.lean

complete

theorem IsBlowUp.contMDiff {𝕜 : 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'] {Y : Set M} {c : ℕ} [IsManifold 𝓘(𝕜, E) ⊤ M']
  [T2Space M'] [SecondCountableTopology M'] {π : M' → M}
  (self : IsBlowUp ψ Y c π) : ContMDiff 𝓘(𝕜, E) 𝓘(𝕜, E) ⊤ π

theorem IsBlowUp.contMDiff {𝕜 : 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'] {Y : Set M} {c : ℕ}
  [IsManifold 𝓘(𝕜, E) ⊤ M'] [T2Space M']
  [SecondCountableTopology M']
  {π : M' → M} (self : IsBlowUp ψ Y c π) :
  ContMDiff 𝓘(𝕜, E) 𝓘(𝕜, E) ⊤ π

defdefined in Hironaka/Manifold/BlowUp/Defs.lean

complete

def AnalyticMap.IsMonoidalTransformation {𝕜 : Type} [RCLike 𝕜]
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {M M' : AnalyticManifold 𝕜 E} (f : AnalyticMap M' M)
  (D : M.IdealSheaf) : Prop :=
  ∃ n ψ c,
    IsClosedSubmanifold ψ (IdealSheaf.support D) c ∧
      IsIdealSheafOf ψ (IdealSheaf.support D) c D ∧
      IsBlowUp ψ (IdealSheaf.support D) c ⇑f

def AnalyticMap.IsMonoidalTransformation
  {𝕜 : Type} [RCLike 𝕜] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {M M' : AnalyticManifold 𝕜 E}
  (f : AnalyticMap M' M)
  (D : M.IdealSheaf) : Prop :=
  ∃ n ψ c,
    IsClosedSubmanifold ψ
        (IdealSheaf.support D) c ∧
      IsIdealSheafOf ψ
        (IdealSheaf.support D) c D ∧
      IsBlowUp ψ (IdealSheaf.support D) c
        ⇑f

f : M' → M is the monoidal transformation of M with centre the closed analytic subspace defined by D (Hironaka's monoidal transformation; the blowing-up of [BM88, Definition 4.1]): for some coordinates ψ : E ≃ 𝕜ⁿ and some codimension c, the cosupport Y of D is a closed analytic submanifold of codimension c (IsClosedSubmanifold), D is the ideal sheaf of Y (IsIdealSheafOf: cosupport Y, stalks at the points of Y spanned by the adapted coordinates), and f is a blowing-up of M with centre Y (IsBlowUp: proper analytic, an analytic isomorphism off Y, with the blow-up charts over every adapted chart).

Definition3.1.4.3source[Hir64, Ch. 0, §5, p. 142] ↗

Statement uses 6

Statement dependency previews

Preview

Definition 3.1.1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

Transforms of an ideal sheaf along a blow-up of manifolds:

the total transform \pi^{-1}(I) = \pi^* I \cdot \mathcal{O}_{M'} (IdealSheaf.totalTransform);
the order of J along a centre, \nu_{D,a}(J) = \sup\{p : J_a \subseteq D_a^p\} (ordAlongIdeal, [BM97, §3]), and its generic value along the connected component of the centre through a (genericOrdAlong);
IsDivExceptional: J' is the quotient of the total transform by the exceptional ideal to the generic order, stalkwise a colon ideal;
weakTransform f J D (AnalyticManifold.IdealSheaf.weakTransform): Hironaka's weak transform, the ideal sheaf with that property, chosen when it exists (Hironaka shows that it does along a monoidal transformation) and the unit ideal otherwise;
reducedTransform f E D: Hironaka's \mathrm{red}(f^{-1}(E) \cup f^{-1}(D)), the reduced subspace on that set through vanishing ideals (Definition 3.1.3.4), when these have local generators (as they do in the main theorems), and the product f^*E \cdot f^*D otherwise, which has the same points;
the strict transform of a closed subspace, stalkwise the saturation of the total transform by the exceptional ideal (saturationStalk, strictTransformSubspace).

The exponent of the weak transform may vary along the centre: it is the generic order along each connected component.

Lean code for Definition3.1.4.3●7 definitions

defdefined in Hironaka/Manifold/BlowUp/Transform/Defs.lean

complete

def IdealSheaf.ordAlongIdeal {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X}
  (D J : Manifold.IdealSheaf 𝒪) (a : ↑X) : ℕ∞ :=
  ⨆ p, ⨆ (_ : J.stalkIdeal a ≤ D.stalkIdeal a ^ p), ↑p

def IdealSheaf.ordAlongIdeal {X : TopCat}
  {𝒪 : TopCat.Sheaf CommRingCat X}
  (D J : Manifold.IdealSheaf 𝒪) (a : ↑X) :
  ℕ∞ :=
  ⨆ p,
    ⨆ (_ :
      J.stalkIdeal a ≤
        D.stalkIdeal a ^ p),
      ↑p

The order of J along the centre with ideal sheaf D at a, ν_{D,a}(J) = sup {p | J_a ⊆ D_a^p} (in ℕ∞; ⊤ when J_a = 0) [BM97, §3].

defdefined in Hironaka/Manifold/BlowUp/Transform/Defs.lean

complete

def IdealSheaf.genericOrdAlong {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X}
  (D J : Manifold.IdealSheaf 𝒪) (a : ↑X) : ℕ∞ :=
  ⨅ y ∈ connectedComponentIn D.support a, D.ordAlongIdeal J y

def IdealSheaf.genericOrdAlong {X : TopCat}
  {𝒪 : TopCat.Sheaf CommRingCat X}
  (D J : Manifold.IdealSheaf 𝒪) (a : ↑X) :
  ℕ∞ :=
  ⨅ y ∈ connectedComponentIn D.support a,
    D.ordAlongIdeal J y

The generic order of J along the connected component of the centre D through a: the infimum of ν_{D,y}(J) over that component (the order at the generic point of the component, [Kol07, Definition 47]).

defdefined in Hironaka/Manifold/BlowUp/Transform/Defs.lean

complete

def IdealSheaf.IsDivExceptional {X : TopCat}
  {𝒪 : TopCat.Sheaf CommRingCat X} (Itot IF : Manifold.IdealSheaf 𝒪)
  (m : ↑X → ℕ) (J' : Manifold.IdealSheaf 𝒪) : Prop :=
  ∀ (a : ↑X),
    J'.stalkIdeal a =
      Submodule.colon (Itot.stalkIdeal a) ↑(IF.stalkIdeal a ^ m a)

def IdealSheaf.IsDivExceptional {X : TopCat}
  {𝒪 : TopCat.Sheaf CommRingCat X}
  (Itot IF : Manifold.IdealSheaf 𝒪)
  (m : ↑X → ℕ)
  (J' : Manifold.IdealSheaf 𝒪) : Prop :=
  ∀ (a : ↑X),
    J'.stalkIdeal a =
      Submodule.colon (Itot.stalkIdeal a)
        ↑(IF.stalkIdeal a ^ m a)

J' is the m-fold quotient of Itot by IF: at every point a its stalk is the colon ideal (Itot_a : IF_a^{m a}), the germs g with g · IF_a^{m a} ⊆ Itot_a ([Hir64, Ch. 0, §5, p. 142]; [Kol07, Definition 60, (60.1)]). The exponent may vary with the point: Hironaka's weak transform divides by the generic order along each component of the centre.

defdefined in Hironaka/Manifold/BlowUp/Transform/Defs.lean

complete

def IdealSheaf.weakTransform {𝕜 : Type} [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {M M' : AnalyticManifold 𝕜 E} (f : AnalyticMap M' M)
  (J D : M.IdealSheaf) : M'.IdealSheaf :=
  if hex :
      ∃ J',
        (IdealSheaf.pullback ⇑f ⋯ J).IsDivExceptional
          (IdealSheaf.pullback ⇑f ⋯ D)
          (fun a' => (IdealSheaf.genericOrdAlong D J (f a')).toNat)
          J' then
    Classical.choose hex
  else ⊤

def IdealSheaf.weakTransform {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E]
  {M M' : AnalyticManifold 𝕜 E}
  (f : AnalyticMap M' M)
  (J D : M.IdealSheaf) : M'.IdealSheaf :=
  if hex :
      ∃ J',
        (IdealSheaf.pullback ⇑f ⋯
              J).IsDivExceptional
          (IdealSheaf.pullback ⇑f ⋯ D)
          (fun a' =>
            (IdealSheaf.genericOrdAlong D
                J (f a')).toNat)
          J' then
    Classical.choose hex
  else ⊤

Hironaka's weak transform of J by the monoidal transformation f with centre D [Hir64, p. 142]: f⁻¹(J) divided by the m-th power of the ideal of f⁻¹(D), m the order of J at the generic point of (each component of) D. Formally: the ideal sheaf whose stalk at every a' is the colon ideal (f⁻¹(J)_{a'} : f⁻¹(D)_{a'}^m), m the generic order of J along the connected component of the cosupport of D through f a' (IdealSheaf.genericOrdAlong, read in ℕ; IdealSheaf.IsDivExceptional), chosen when such an ideal sheaf exists — Hironaka shows that it does when f is the monoidal transformation with centre D — and the unit ideal sheaf otherwise. The total transform f⁻¹(J) is IdealSheaf.pullback.

defdefined in Hironaka/Manifold/BlowUp/Transform/Defs.lean

complete

def IdealSheaf.reducedTransform {𝕜 : Type} [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {M M' : AnalyticManifold 𝕜 E} (f : AnalyticMap M' M) :
  M.IdealSheaf → (D : M.IdealSheaf) → M'.IdealSheaf :=
  if h :
      IdealSheaf.HasLocalGenerators fun x =>
        vanishingStalk
          (⇑f ⁻¹' IdealSheaf.support E ∪ ⇑f ⁻¹' IdealSheaf.support D)
          x then
    IdealSheaf.ofStalks (structureSheaf 𝕜 E✝ M'.carrier)
      (fun x =>
        vanishingStalk
          (⇑f ⁻¹' IdealSheaf.support E ∪ ⇑f ⁻¹' IdealSheaf.support D) x)
      h
  else IdealSheaf.pullback ⇑f ⋯ E * IdealSheaf.pullback ⇑f ⋯ D

def IdealSheaf.reducedTransform {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E]
  {M M' : AnalyticManifold 𝕜 E}
  (f : AnalyticMap M' M) :
  M.IdealSheaf →
    (D : M.IdealSheaf) → M'.IdealSheaf :=
  if h :
      IdealSheaf.HasLocalGenerators
        fun x =>
        vanishingStalk
          (⇑f ⁻¹' IdealSheaf.support E ∪
            ⇑f ⁻¹' IdealSheaf.support D)
          x then
    IdealSheaf.ofStalks
      (structureSheaf 𝕜 E✝ M'.carrier)
      (fun x =>
        vanishingStalk
          (⇑f ⁻¹' IdealSheaf.support E ∪
            ⇑f ⁻¹' IdealSheaf.support D)
          x)
      h
  else
    IdealSheaf.pullback ⇑f ⋯ E *
      IdealSheaf.pullback ⇑f ⋯ D

Hironaka's red(f⁻¹(E) ∪ f⁻¹(D)) [Hir64, Main Theorem II'(N) (iii), p. 156]; Włodarczyk's exceptional divisor of a composite of blow-ups [Wlo09, Remark (1) after Theorem 2.0.3]: the reduced closed analytic subspace of M' whose set of points is f⁻¹(E) ∪ f⁻¹(D) — the ideal sheaf whose stalks are the vanishing ideals of that closed set (vanishingStalk, the germs vanishing on the set near the point), when these stalks have local generators (they do when E is a normal crossings divisor and f the monoidal transformation with centre D, the case of the main theorems: Hironaka/Manifold/FiniteSuccession/BoundaryFamily.lean), and otherwise the product f^*E · f^*D, which has the same set of points.

defdefined in Hironaka/Manifold/BlowUp/Transform/Defs.lean

complete

def saturationStalk {𝕜 : 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 : ℕ} {M' : Type u}
  [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold 𝓘(𝕜, E) ⊤ M']
  [T2Space M'] [SecondCountableTopology M'] {π : M' → M}
  (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π)
  (I : Manifold.IdealSheaf (structureSheaf 𝕜 E M)) (a' : M') :
  Ideal ↑((structureSheaf 𝕜 E M').presheaf.stalk a') :=
  ⨆ k,
    Submodule.colon ((IdealSheaf.pullback π ⋯ I).stalkIdeal a')
      ↑((IdealSheaf.pullback π ⋯ hY.idealSheaf).stalkIdeal a' ^ k)

def saturationStalk {𝕜 : 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 : ℕ} {M' : Type u}
  [TopologicalSpace M']
  [ChartedSpace E M']
  [IsManifold 𝓘(𝕜, E) ⊤ M'] [T2Space M']
  [SecondCountableTopology M']
  {π : M' → M}
  (hY : IsClosedSubmanifold ψ Y c)
  (h : IsBlowUp ψ Y c π)
  (I :
    Manifold.IdealSheaf
      (structureSheaf 𝕜 E M))
  (a' : M') :
  Ideal
    ↑((structureSheaf 𝕜 E
              M').presheaf.stalk
        a') :=
  ⨆ k,
    Submodule.colon
      ((IdealSheaf.pullback π ⋯
            I).stalkIdeal
        a')
      ↑((IdealSheaf.pullback π ⋯
                hY.idealSheaf).stalkIdeal
            a' ^
          k)

The saturation of the total transform (the pull-back π⁻¹(I) along the blow-up) with respect to the exceptional divisor at a', ⋃_k (π⁻¹(I)_{a'} : I_{F,a'}^k) — the germs g with y_exc^k g ∈ π⁻¹(I)_{a'} for some k.

defdefined in Hironaka/Manifold/BlowUp/Transform/Defs.lean

complete

def strictTransformSubspace {𝕜 : 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 : ℕ} {M' : Type u}
  [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold 𝓘(𝕜, E) ⊤ M']
  [T2Space M'] [SecondCountableTopology M'] {π : M' → M}
  (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π)
  (I : Manifold.IdealSheaf (structureSheaf 𝕜 E M)) :
  Manifold.IdealSheaf (structureSheaf 𝕜 E M') :=
  if hex : IdealSheaf.HasLocalGenerators (saturationStalk hY h I) then
    IdealSheaf.ofStalks (structureSheaf 𝕜 E M') (saturationStalk hY h I)
      hex
  else ⊤

def strictTransformSubspace {𝕜 : 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 : ℕ}
  {M' : Type u} [TopologicalSpace M']
  [ChartedSpace E M']
  [IsManifold 𝓘(𝕜, E) ⊤ M'] [T2Space M']
  [SecondCountableTopology M']
  {π : M' → M}
  (hY : IsClosedSubmanifold ψ Y c)
  (h : IsBlowUp ψ Y c π)
  (I :
    Manifold.IdealSheaf
      (structureSheaf 𝕜 E M)) :
  Manifold.IdealSheaf
    (structureSheaf 𝕜 E M') :=
  if hex :
      IdealSheaf.HasLocalGenerators
        (saturationStalk hY h I) then
    IdealSheaf.ofStalks
      (structureSheaf 𝕜 E M')
      (saturationStalk hY h I) hex
  else ⊤

The strict transform X' of the closed subspace X ⊆ M with ideal sheaf I under the blowing-up π with centre Y — the ideal sheaf whose stalks are the saturations ⋃_k (π⁻¹(I)_{a'} : I_{F,a'}^k) (of finite type since X is locally Noetherian, as Bierstone–Milman remark after Proposition 3.13), taken when that stalk family has local generators, the unit ideal sheaf otherwise (the pattern of the weak transform).

3.1.5. Simple normal crossings boundaries🔗

Definition3.1.5.1source[Kol07, Definition 24] ↗

Statement uses 4

Statement dependency previews

Preview

Definition 3.1.1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 6

Reverse dependency previews

Preview

Definition 3.1.5.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

A HypersurfaceFamily M is an ordered countable family of subsets hyp j of M (indexed by ι), the components E^j of a divisor E = \sum E^j, with support \bigcup_j E^j. It is a simple normal crossings divisor (IsSnc) if every component is a closed smooth hypersurface, the family is locally finite, and every point has an snc chart (IsSncChartAt): a chart in which each component through the point is its own coordinate hyperplane. HasSncWith adds a closed submanifold Y cut out by some of the coordinates of such charts. idealSheaf is the reduced ideal sheaf of the divisor, through the vanishing ideals of its support.

The statements use two predicates on an ideal sheaf B:

IsSncBoundary B: B is the reduced ideal sheaf of a simple normal crossings hypersurface family, for some coordinates;
IsSncBoundaryWith B D: moreover the family has simple normal crossings with the closed subspace D [Kol07, Definition 24 (4)]; [Wlo09, Definition 3.2.4 (2)].

IsNormalCrossingsDivisor is Bierstone–Milman's normal-crossings divisor: a principal ideal sheaf generated at every point by a monomial \prod z_i^{\alpha_i} in a regular system of parameters (Definition 2.1.2.2) [BM97, Theorem 1.10].

Lean code for Definition3.1.5.1●11 definitions

structure(4 fields)defined in Hironaka/Manifold/Snc/Defs.lean

complete
structure HypersurfaceFamily (M : Type u) : Type (u + 1)
structure HypersurfaceFamily (M : Type u) : Type (u + 1)
An ordered, countable family of subsets of M: the components E^j of a divisor E = ∑ E^j [Kol07, Definition 24]. The snc property is the predicate HypersurfaceFamily.IsSnc.
Fields

ι : Type u

The index set of the components, countable and linearly ordered.

countable : Countable self.ι

linearOrder : LinearOrder self.ι

hyp : self.ι → Set M

The component E^j.

abbrevdefined in Hironaka/Manifold/Snc/Defs.lean

complete

abbrev HypersurfaceFamily.ι {M : Type u} (self : HypersurfaceFamily M) : Type u :=
  self.1

abbrev HypersurfaceFamily.ι {M : Type u}
  (self : HypersurfaceFamily M) : Type u :=
  self.1

The index set of the components, countable and linearly ordered.

abbrevdefined in Hironaka/Manifold/Snc/Defs.lean

complete

abbrev HypersurfaceFamily.hyp {M : Type u} (self : HypersurfaceFamily M) :
  self.ι → Set M :=
  self.4

abbrev HypersurfaceFamily.hyp {M : Type u}
  (self : HypersurfaceFamily M) :
  self.ι → Set M :=
  self.4

The component E^j.

defdefined in Hironaka/Manifold/Snc/Defs.lean

complete

def HypersurfaceFamily.support {M : Type u} (F : HypersurfaceFamily M) :
  Set M :=
  ⋃ j, F.hyp j

def HypersurfaceFamily.support {M : Type u}
  (F : HypersurfaceFamily M) : Set M :=
  ⋃ j, F.hyp j

The support |F| = ⋃_j E^j of the family.

defdefined in Hironaka/Manifold/Snc/Defs.lean

complete

def HypersurfaceFamily.IsSncChartAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ}
  (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M]
  [ChartedSpace E M] (F : HypersurfaceFamily M)
  (φ : OpenPartialHomeomorph M E) (a : M)
  (c : { j // a ∈ F.hyp j } → Fin n) : Prop :=
  φ ∈ IsManifold.maximalAtlas 𝓘(𝕜, E) ⊤ M ∧
    a ∈ φ.source ∧
    ∀ (j : { j // a ∈ F.hyp j }),
      ∀ x ∈ φ.source, x ∈ F.hyp ↑j ↔ ψ (↑φ x) (c j) = 0 ∧
    Function.Injective c

def HypersurfaceFamily.IsSncChartAt {𝕜 : Type}
  [RCLike 𝕜] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜)
  {M : Type u} [TopologicalSpace M]
  [ChartedSpace E M]
  (F : HypersurfaceFamily M)
  (φ : OpenPartialHomeomorph M E) (a : M)
  (c : { j // a ∈ F.hyp j } → Fin n) :
  Prop :=
  φ ∈
      IsManifold.maximalAtlas 𝓘(𝕜, E) ⊤
        M ∧
    a ∈ φ.source ∧
    ∀ (j : { j // a ∈ F.hyp j }),
      ∀ x ∈ φ.source,
        x ∈ F.hyp ↑j ↔
          ψ (↑φ x) (c j) = 0 ∧
    Function.Injective c

The chart φ of the maximal atlas is an snc chart of F at a ∈ φ.source with coordinate indices c — a function on the components through a — when every component through a is, on the source of φ, the coordinate hyperplane {z_{c j} = 0}, and distinct components through a have distinct indices [Kol07, Definition 24 (1)–(3)].

defdefined in Hironaka/Manifold/Snc/Defs.lean

complete

def HypersurfaceFamily.IsSnc {𝕜 : Type} [RCLike 𝕜] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ}
  (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M]
  [ChartedSpace E M] (F : HypersurfaceFamily M) : Prop :=
  (∀ (j : F.ι), IsClosedSubmanifold ψ (F.hyp j) 1) ∧
    LocallyFinite F.hyp ∧
    ∀ (a : M), ∃ φ c, HypersurfaceFamily.IsSncChartAt ψ F φ a c

def HypersurfaceFamily.IsSnc {𝕜 : Type}
  [RCLike 𝕜] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜)
  {M : Type u} [TopologicalSpace M]
  [ChartedSpace E M]
  (F : HypersurfaceFamily M) : Prop :=
  (∀ (j : F.ι),
      IsClosedSubmanifold ψ (F.hyp j) 1) ∧
    LocallyFinite F.hyp ∧
    ∀ (a : M),
      ∃ φ c,
        HypersurfaceFamily.IsSncChartAt ψ
          F φ a c

F is a simple normal crossings divisor [Kol07, Definition 24]: each component is a closed smooth hypersurface, the family is locally finite, and every point of M has an snc chart. Hironaka's "E has only normal crossings" [Hir64, Definition 2, p. 141], read on the global components.

defdefined in Hironaka/Manifold/Snc/Defs.lean

complete

def HypersurfaceFamily.HasSncWith {𝕜 : Type} [RCLike 𝕜] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ}
  (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M]
  [ChartedSpace E M] (F : HypersurfaceFamily M) (Y : Set M) (c : ℕ) :
  Prop :=
  ∀ a ∈ Y,
    ∃ φ σ cidx,
      IsAdaptedChart ψ Y φ σ ∧
        HypersurfaceFamily.IsSncChartAt ψ F φ a cidx

def HypersurfaceFamily.HasSncWith {𝕜 : Type}
  [RCLike 𝕜] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜)
  {M : Type u} [TopologicalSpace M]
  [ChartedSpace E M]
  (F : HypersurfaceFamily M) (Y : Set M)
  (c : ℕ) : Prop :=
  ∀ a ∈ Y,
    ∃ φ σ cidx,
      IsAdaptedChart ψ Y φ σ ∧
        HypersurfaceFamily.IsSncChartAt ψ
          F φ a cidx

Y has simple normal crossings with F [Kol07, Definition 24 (4)]: at every point of Y there is a chart adapted to Y which is an snc chart of F there. Some components of F may contain Y (Hironaka's "the ideal of D is generated by some of the z_i" [Hir64, Definition 2, p. 141]; Bierstone–Milman's "C_i and E_i simultaneously have only normal crossings" [BM97, (1.2)]).

defdefined in Hironaka/Manifold/Snc/Defs.lean

complete

def HypersurfaceFamily.idealSheaf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u}
  [TopologicalSpace M] [ChartedSpace E M] (F : HypersurfaceFamily M) :
  Manifold.IdealSheaf (structureSheaf 𝕜 E M) :=
  if h :
      IdealSheaf.HasLocalGenerators fun x =>
        vanishingStalk F.support x then
    IdealSheaf.ofStalks (structureSheaf 𝕜 E M)
      (fun x => vanishingStalk F.support x) h
  else ⊤

def HypersurfaceFamily.idealSheaf {𝕜 : Type}
  [RCLike 𝕜] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {M : Type u} [TopologicalSpace M]
  [ChartedSpace E M]
  (F : HypersurfaceFamily M) :
  Manifold.IdealSheaf
    (structureSheaf 𝕜 E M) :=
  if h :
      IdealSheaf.HasLocalGenerators
        fun x =>
        vanishingStalk F.support x then
    IdealSheaf.ofStalks
      (structureSheaf 𝕜 E M)
      (fun x =>
        vanishingStalk F.support x)
      h
  else ⊤

The reduced ideal sheaf of the divisor (Hironaka's red, [Hir64, Main Theorem II'(N) (iii), p. 156]; [BM97, Remark 3.14]): the ideal sheaf whose stalks are the vanishing ideals of the support (vanishingStalk), when these have local generators (they do for an snc divisor: the product of the coordinate equations of the components through the point, Hironaka/Manifold/Snc/Coherence.lean); the unit ideal sheaf otherwise.

defdefined in Hironaka/Manifold/Snc/Defs.lean

complete
def IdealSheaf.IsSncBoundary {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (B : M.IdealSheaf) : Prop := ∃ n ψ G, HypersurfaceFamily.IsSnc ψ G ∧ G.idealSheaf = B
def IdealSheaf.IsSncBoundary {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (B : M.IdealSheaf) : Prop := ∃ n ψ G, HypersurfaceFamily.IsSnc ψ G ∧ G.idealSheaf = B
The boundary predicate of the analytic main theorems: B is the reduced ideal sheaf of a simple normal crossings hypersurface family — for some coordinates ψ : E ≃ 𝕜ⁿ there is a locally finite family G of closed smooth hypersurfaces with a simple normal crossings chart at every point (HypersurfaceFamily.IsSnc; [Kol07, Definition 24; Wlo09, Definition 3.2.4]) whose reduced ideal sheaf (HypersurfaceFamily.idealSheaf) is B. The coordinates are existential inside the predicate, as in AnalyticMap.IsMonoidalTransformation: the statements carry no model isomorphism, and Kollár names local coordinates at each point.
defdefined in Hironaka/Manifold/Snc/Defs.lean

complete
def IdealSheaf.IsSncBoundaryWith {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (B D : M.IdealSheaf) : Prop := ∃ n ψ G c, HypersurfaceFamily.IsSnc ψ G ∧ G.idealSheaf = B ∧ HypersurfaceFamily.HasSncWith ψ G (IdealSheaf.support D) c
def IdealSheaf.IsSncBoundaryWith {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (B D : M.IdealSheaf) : Prop := ∃ n ψ G c, HypersurfaceFamily.IsSnc ψ G ∧ G.idealSheaf = B ∧ HypersurfaceFamily.HasSncWith ψ G (IdealSheaf.support D) c
The boundary-with-centre predicate of the analytic main theorems: B is the reduced ideal sheaf of a simple normal crossings hypersurface family G having simple normal crossings with the closed subspace D — at every point of D a chart adapted to the set of points of D (a closed submanifold of some codimension c) which is a simple normal crossings chart of G there (HypersurfaceFamily.HasSncWith; [Kol07, Definition 24 (4)], "some of the E^i are allowed to contain Z"; [Wlo09, Definition 3.2.4 (2)] and [Wlo09, Theorem 2.0.3 (2)], "C_i has simple normal crossings with E_i"). The coordinates and the codimension are existential inside the predicate, as in AnalyticMap.IsMonoidalTransformation.

The predicate thus asserts simple normal crossings of B at every point of M (it implies IsSncBoundary B), and simple normal crossings with D at the points of D. The scheme predicate of the same name (AlgebraicGeometry.Scheme.IdealSheafData.IsSncBoundaryWith) asserts only the condition at the points of D, and nothing about its boundary elsewhere: for D = ⊤ the scheme predicate always holds, while this one is IsSncBoundary B.

defdefined in Hironaka/Manifold/Snc/Defs.lean

complete

def IdealSheaf.IsNormalCrossingsDivisor {𝕜 : Type}
  [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (J : M.IdealSheaf) : Prop :=
  ∀ (x : M.carrier),
    ∃ n z α,
      IsLocalRing.IsRegularSystemOfParameters z ∧
        IdealSheaf.stalkIdeal J x = Ideal.span {∏ i, z i ^ α i}

def IdealSheaf.IsNormalCrossingsDivisor
  {𝕜 : Type} [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E]
  {M : AnalyticManifold 𝕜 E}
  (J : M.IdealSheaf) : Prop :=
  ∀ (x : M.carrier),
    ∃ n z α,
      IsLocalRing.IsRegularSystemOfParameters
          z ∧
        IdealSheaf.stalkIdeal J x =
          Ideal.span {∏ i, z i ^ α i}

Bierstone–Milman's normal-crossings divisor: a principal ideal sheaf generated locally by a monomial in suitable analytic coordinates [BM97, Theorem 1.10] — at every point, by a monomial ∏ z_i^{α_i} in a regular system of parameters (generators of the maximal ideal, as many as the Krull dimension). The form of the conclusions on σ^*(I) and on the Jacobian ideal in the principalization theorem.

Definition3.1.5.2source[Wlo09, Theorem 2.0.2 (3), (6)] ↗

Statement uses 2

Statement dependency previews

Preview

Definition 3.1.1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 3

Reverse dependency previews

Preview

Definition 4.3.3.1

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Two predicates of Włodarczyk's embedded desingularization (Theorem 4.3.4.6), for ideal sheaves B, Y and J:

B.IsSncBoundaryTransversalTo Y: B is the reduced ideal sheaf of a simple normal crossings hypersurface family G with which the closed subspace Y has simple normal crossings transversally: at every point a of Y there is a chart adapted to Y, of the codimension of Y at a, which is an snc chart of G at a, and the coordinates cutting out Y are distinct from those of the hypersurfaces through a. Unlike IsSncBoundaryWith, the codimension may vary from point to point, as it does for the strict transform of a subspace that is not equidimensional; and no component through a may contain Y near a, which Kollár's Definition 24 (4) allows. This is the reading of "\tilde Y has only simple normal crossings with the exceptional divisor E_r" [Wlo09, Theorem 2.0.2 (3)].
J.IsMulBoundaryMonomial Y B: J = I_Y \cdot I_{\tilde E} for a divisor \tilde E that is, near every point, an effective combination of the hypersurfaces of a simple normal crossings family whose reduced ideal sheaf is B: at every point x the stalk J_x is the product of (I_Y)_x with a monomial in the vanishing ideals of hypersurfaces of the family through x (Definition 3.1.3.4), the exponents read at x [Wlo09, Theorem 2.0.2 (6)].

Lean code for Definition3.1.5.2●2 definitions

defdefined in Hironaka/Manifold/Snc/Defs.lean

complete

def IdealSheaf.IsSncBoundaryTransversalTo {𝕜 : Type} [RCLike 𝕜]
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {M : AnalyticManifold 𝕜 E} (B Y : M.IdealSheaf) : Prop :=
  ∃ n ψ G,
    HypersurfaceFamily.IsSnc ψ G ∧
      G.idealSheaf = B ∧
      ∀ a ∈ IdealSheaf.support Y,
        ∃ c φ σ cidx,
          IsAdaptedChart ψ (IdealSheaf.support Y) φ σ ∧
            HypersurfaceFamily.IsSncChartAt ψ G φ a cidx ∧
            ∀ (j : { j // a ∈ G.hyp j }), cidx j ∉ range ⇑σ

def IdealSheaf.IsSncBoundaryTransversalTo
  {𝕜 : Type} [RCLike 𝕜] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {M : AnalyticManifold 𝕜 E}
  (B Y : M.IdealSheaf) : Prop :=
  ∃ n ψ G,
    HypersurfaceFamily.IsSnc ψ G ∧
      G.idealSheaf = B ∧
      ∀ a ∈ IdealSheaf.support Y,
        ∃ c φ σ cidx,
          IsAdaptedChart ψ
              (IdealSheaf.support Y) φ σ ∧
            HypersurfaceFamily.IsSncChartAt
              ψ G φ a cidx ∧
            ∀ (j : { j // a ∈ G.hyp j }),
              cidx j ∉ range ⇑σ

The boundary-with-subspace predicate of Włodarczyk's embedded desingularization: B is the reduced ideal sheaf of a simple normal crossings hypersurface family G with which the closed subspace Y has simple normal crossings transversally — at every point a of Y a chart adapted to the set of points of Y (a closed submanifold near a, of a codimension c read at a) which is a simple normal crossings chart of G at a: simple normal crossings in the sense of [Kol07, Definition 24 (4)]. Moreover, and this is an addition to Kollár's definition, which allows components to contain Y, the coordinates cutting out Y are distinct from those of the components of G through a, so that no component through a contains Y near a (Kollár's case "E does not contain Z"). This is the reading of [Wlo09, Theorem 2.0.2 (3)], "Ỹ has only simple normal crossings with the exceptional divisor E_r", for the strict transform. Unlike IsSncBoundaryWith, the codimension may vary from point to point, as it does for the strict transform of a subspace that is not equidimensional.

defdefined in Hironaka/Manifold/Snc/Defs.lean

complete

def IdealSheaf.IsMulBoundaryMonomial {𝕜 : Type} [RCLike 𝕜] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E}
  (J Y B : M.IdealSheaf) : Prop :=
  ∃ n ψ G,
    HypersurfaceFamily.IsSnc ψ G ∧
      G.idealSheaf = B ∧
      ∀ (x : M.carrier),
        ∃ s α,
          (∀ j ∈ s, x ∈ G.hyp j) ∧
            IdealSheaf.stalkIdeal J x =
              IdealSheaf.stalkIdeal Y x *
                ∏ j ∈ s, vanishingStalk (G.hyp j) x ^ α j

def IdealSheaf.IsMulBoundaryMonomial
  {𝕜 : Type} [RCLike 𝕜] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {M : AnalyticManifold 𝕜 E}
  (J Y B : M.IdealSheaf) : Prop :=
  ∃ n ψ G,
    HypersurfaceFamily.IsSnc ψ G ∧
      G.idealSheaf = B ∧
      ∀ (x : M.carrier),
        ∃ s α,
          (∀ j ∈ s, x ∈ G.hyp j) ∧
            IdealSheaf.stalkIdeal J x =
              IdealSheaf.stalkIdeal Y x *
                ∏ j ∈ s,
                  vanishingStalk (G.hyp j)
                      x ^
                    α j

The factorization predicate of Włodarczyk's embedded desingularization: J = I_Y · I_Ẽ for a divisor Ẽ that is, near every point, an effective combination of the components of a simple normal crossings hypersurface family G whose reduced ideal sheaf is B — at every point x the stalk J_x is the product of (I_Y)_x with a monomial ∏_{j ∈ s} (I_{G^j})_x^{α_j} in the vanishing ideals of finitely many components G^j through x, the exponents read at x ([Wlo09, Theorem 2.0.2 (6)], "σ^*(I_Y) = I_Ỹ I_Ẽ, where I_Ỹ is the sheaf of ideals of the subvariety Ỹ ⊂ M̃ and I_Ẽ is the sheaf of ideals of a simple normal crossing divisor Ẽ which is a locally finite combination of the irreducible components of the divisor E_{U_r}"; the strengthening of Bravo–Villamayor). For Y = ⊤ it says that J is, near every point, the ideal of an effective combination of the hypersurfaces of G [Wlo09, Theorem 2.0.3 (3)].

3.1.6. The Jacobian ideal and analytic isomorphisms🔗

Definition3.1.6.1source[BM97, Theorem 1.10] ↗

Statement uses 3

Statement dependency previews

Preview

Definition 3.1.1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 5

Reverse dependency previews

Preview

Definition 3.2.2.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

jacobianFun 𝕜 f χ φ' y is the Jacobian determinant \det D(\chi \circ f \circ \varphi'^{-1}) of f in the charts \chi (target) and \varphi' (source). jacobianStalk f a' is the ideal of \mathcal{O}_{N,a'} generated by its germ in the standard charts, and AnalyticMap.jacobianIdeal f is the ideal sheaf with these stalks: the ideal generated locally, in any analytic coordinates, by the Jacobian determinant, independent of the coordinates since a change of charts multiplies the determinant by a unit.

AnalyticMap.IsIsoOver f U: f restricts to an analytic isomorphism f^{-1}(U) \to U, that is, a local diffeomorphism on f^{-1}(U) and a bijection onto U (condition (1) of [BM88, Definition 4.1], off the centre).

Lean code for Definition3.1.6.1●4 definitions

defdefined in Hironaka/Manifold/Jacobian/Defs.lean

complete

def jacobianFun (𝕜 : Type) [NontriviallyNormedField 𝕜] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u}
  [TopologicalSpace M] {N : Type u} [TopologicalSpace N] (f : N → M)
  (χ : OpenPartialHomeomorph M E) (φ' : OpenPartialHomeomorph N E)
  (y : N) : 𝕜 :=
  (fderiv 𝕜 (↑χ ∘ f ∘ ↑φ'.symm) (↑φ' y)).det

def jacobianFun (𝕜 : Type)
  [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {M : Type u}
  [TopologicalSpace M] {N : Type u}
  [TopologicalSpace N] (f : N → M)
  (χ : OpenPartialHomeomorph M E)
  (φ' : OpenPartialHomeomorph N E)
  (y : N) : 𝕜 :=
  (fderiv 𝕜 (↑χ ∘ f ∘ ↑φ'.symm)
      (↑φ' y)).det

The Jacobian determinant of f : N → M in the charts χ (target) and φ' (source) at y, det D(χ ∘ f ∘ φ'⁻¹)(φ' y) — the determinant (ContinuousLinearMap.det, coordinate-free on E) of the derivative of the chart representative of f ("the Jacobian determinant of σ", [BM97, Theorem 1.10, the sentence after it]). The scalar field is explicit, as in fderiv 𝕜.

defdefined in Hironaka/Manifold/Jacobian/Defs.lean

complete

def jacobianStalk {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u}
  [TopologicalSpace M] [ChartedSpace E M] {N : Type u}
  [TopologicalSpace N] [ChartedSpace E N] (f : N → M) (a' : N) :
  Ideal ↑((structureSheaf 𝕜 E N).presheaf.stalk a') :=
  Ideal.span
    (⇑(stalkToGerm 𝓘(𝕜, E) ⊤ N a') ⁻¹'
      {↑(jacobianFun 𝕜 f (chartAt E (f a')) (chartAt E a'))})

def jacobianStalk {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {M : Type u}
  [TopologicalSpace M] [ChartedSpace E M]
  {N : Type u} [TopologicalSpace N]
  [ChartedSpace E N] (f : N → M)
  (a' : N) :
  Ideal
    ↑((structureSheaf 𝕜 E
              N).presheaf.stalk
        a') :=
  Ideal.span
    (⇑(stalkToGerm 𝓘(𝕜, E) ⊤ N a') ⁻¹'
      {↑(jacobianFun 𝕜 f
            (chartAt E (f a'))
            (chartAt E a'))})

The stalk at a' of the Jacobian ideal of f: the ideal of 𝒪_{N,a'} generated by the germs whose function germ (stalkToGerm) is the germ at a' of the Jacobian determinant of f in the standard charts chartAt E (f a') and chartAt E a'. The generating set is the single germ of that analytic function when it is analytic near a' (which holds for every analytic f), and empty otherwise.

defdefined in Hironaka/Manifold/Jacobian/Defs.lean

complete

def AnalyticMap.jacobianIdeal {𝕜 : Type} [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {M M' : AnalyticManifold 𝕜 E} (f : AnalyticMap M' M) : M'.IdealSheaf :=
  if h : IdealSheaf.HasLocalGenerators (jacobianStalk ⇑f) then
    IdealSheaf.ofStalks (structureSheaf 𝕜 E M'.carrier)
      (jacobianStalk ⇑f) h
  else ⊤

def AnalyticMap.jacobianIdeal {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E]
  {M M' : AnalyticManifold 𝕜 E}
  (f : AnalyticMap M' M) : M'.IdealSheaf :=
  if h :
      IdealSheaf.HasLocalGenerators
        (jacobianStalk ⇑f) then
    IdealSheaf.ofStalks
      (structureSheaf 𝕜 E M'.carrier)
      (jacobianStalk ⇑f) h
  else ⊤

The ideal sheaf generated locally, in any analytic coordinates on source and target, by the Jacobian determinant of f [BM97, Theorem 1.10, the sentence after it] — independent of the coordinates, since a chart change multiplies the determinant by a unit: the ideal sheaf whose stalk at a' is generated by the germ of the Jacobian determinant of f in the standard charts chartAt (f a') and chartAt a' (Manifold.jacobianStalk), when these stalks have local generators (they do for every analytic f: the Jacobian determinant is analytic and its germ at a nearby point is a unit multiple of the germ in the charts at that point, Hironaka/Manifold/Jacobian/), and the unit ideal sheaf otherwise.

defdefined in Hironaka/Manifold/AnalyticManifold/Defs.lean

complete

def AnalyticMap.IsIsoOver {𝕜 : Type} [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {M M' : AnalyticManifold 𝕜 E} (f : AnalyticMap M' M)
  (U : Set M.carrier) : Prop :=
  IsLocalDiffeomorphOn 𝓘(𝕜, E) 𝓘(𝕜, E) ⊤ (⇑f) (⇑f ⁻¹' U) ∧
    BijOn (⇑f) (⇑f ⁻¹' U) U

def AnalyticMap.IsIsoOver {𝕜 : Type}
  [NontriviallyNormedField 𝕜]
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E]
  {M M' : AnalyticManifold 𝕜 E}
  (f : AnalyticMap M' M)
  (U : Set M.carrier) : Prop :=
  IsLocalDiffeomorphOn 𝓘(𝕜, E) 𝓘(𝕜, E) ⊤
      (⇑f) (⇑f ⁻¹' U) ∧
    BijOn (⇑f) (⇑f ⁻¹' U) U

f restricts to an analytic isomorphism f⁻¹(U) → U over the open set U: f is a local diffeomorphism on f⁻¹(U) and a bijection f⁻¹(U) → U — condition (1) of Bierstone–Milman's blowing-up [BM88, Definition 4.1], off the centre; the clause "σ is an isomorphism off the cosupport of I" of the principalization theorem.