14.8. Cech.CechSection🔗

Jacobians.Cech.CechSection — source

ordU

Order of a bare function on the open submanifold ↥U, read in U's own chart at x. (Chart-invariant; intrinsic to ↥U.)

noncomputable def ordU [ChartedSpace ℂ X] {U : Opens X} (f : U → ℂ) (x : U) : WithTop ℤ

ordU_zero

The order of the zero function on ↥U is ⊤.

theorem ordU_zero [ChartedSpace ℂ X] {U : Opens X} (x : U) : ordU (0 : U → ℂ) x = ⊤

OmegaD

Sections of 𝒪_D over an open U (Forster's 𝒪_D(U)): functions meromorphic on the open submanifold ↥U whose order is ≥ −D at every point of U. A Submodule ℂ of ↥U → ℂ.

noncomputable def OmegaD [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (D : Divisor X) (U : Opens X) : Submodule ℂ (U → ℂ) where

mem_OmegaD

@[simp] theorem mem_OmegaD [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] {D : Divisor X} {U : Opens X} {f : U → ℂ} :
    f ∈ OmegaD D U ↔ IsMeromorphic (U : Type _) f ∧ ∀ x : U, (-(D x.1) : WithTop ℤ) ≤ ordU f x

openIncl

The open inclusion ↥V → ↥U for V ≤ U.

def openIncl (h : V ≤ U) : V → U

openIncl_val

@[simp] theorem openIncl_val (h : V ≤ U) (v : V) : (openIncl h v).1 = v.1

restrict_chart_aux

The base point and the chart-pullback agree between ↥V's chart at v and ↥U's chart at openIncl h v: both charts are subtypeRestrs of the *same* ambient chart chartAt ℂ v.1 (Opens.chartAt_eq), so they read f at the same ambient point near v. The shared core of the two restriction lemmas.

theorem restrict_chart_aux [ChartedSpace ℂ X] (h : V ≤ U) (f : U → ℂ) (v : V) :
    (chartAt (H := ℂ) v) v = (chartAt (H := ℂ) (openIncl h v)) (openIncl h v) ∧
    ((f ∘ openIncl h) ∘ (chartAt (H := ℂ) v).symm) =ᶠ[𝓝 ((chartAt (H := ℂ) v) v)]
      (f ∘ (chartAt (H := ℂ) (openIncl h v)).symm)

ordU_comp_openIncl

Restriction preserves the order at corresponding points (chart bookkeeping via Opens.chartAt_eq + subtypeRestr).

theorem ordU_comp_openIncl [ChartedSpace ℂ X] (h : V ≤ U) (f : U → ℂ) (v : V) :
    ordU (f ∘ openIncl h) v = ordU f (openIncl h v)

isMeromorphic_comp_openIncl

Meromorphy on ↥U restricts to the open sub-submanifold ↥V.

theorem isMeromorphic_comp_openIncl [ChartedSpace ℂ X] (h : V ≤ U) {f : U → ℂ}
    (hf : IsMeromorphic (U : Type _) f) : IsMeromorphic (V : Type _) (f ∘ openIncl h)

OmegaD.restrict

Restriction of sections 𝒪_D(U) → 𝒪_D(V) for V ≤ U.

noncomputable def OmegaD.restrict [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] {D : Divisor X} (h : V ≤ U) :
    OmegaD D U →ₗ[ℂ] OmegaD D V

MGerm

Germ-class functions on ↥U: (↥U → ℂ) modulo codiscrete equality — the junk-free section space. A ℂ-module via Filter.Germ.

abbrev MGerm (U : Opens X) : Type _

toGerm

The germ projection (↥U → ℂ) →ₗ[ℂ] MGerm U (quotient by germ-zero junk).

def toGerm (U : Opens X) : (U → ℂ) →ₗ[ℂ] MGerm U where

tendsto_openIncl

The open inclusion ↥V → ↥U pulls codiscrete sets back to codiscrete sets (it is an open embedding), so precomposition descends to germ-classes.

theorem tendsto_openIncl (h : V ≤ U) :
    Filter.Tendsto (openIncl h) (Filter.codiscreteWithin (Set.univ : Set V))
      (Filter.codiscreteWithin (Set.univ : Set U))

rawRestrictG

Restriction on germ-classes MGerm U →ₗ[ℂ] MGerm V (V ≤ U): precomposition with the open inclusion, descended to germs.

noncomputable def rawRestrictG (h : V ≤ U) : MGerm U →ₗ[ℂ] MGerm V where

rawRestrictG_coe

@[simp] theorem rawRestrictG_coe (h : V ≤ U) (f : U → ℂ) :
    rawRestrictG h (toGerm U f) = toGerm V (f ∘ openIncl h)

rawRestrictG_le_rfl

Germ restriction along the reflexive containment U ≤ U is the identity (openIncl h is the identity map on ↥U for any h : U ≤ U, so the germ pullback is the identity). The ≤-proof is taken explicitly so this canonical form covers every call site (le_rfl, le_refl U, or a generic h : U ≤ U); the @[simp] form fires regardless of which proof is supplied.

@[simp] theorem rawRestrictG_le_rfl {U : Opens X} (h : U ≤ U) (f : MGerm U) :
    rawRestrictG h f = f

OmegaDGerm

𝒪_D-sections as germ-classes: the image of OmegaD under the germ projection — junk-free, no quotient.

noncomputable def OmegaDGerm [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (D : Divisor X) (U : Opens X) : Submodule ℂ (MGerm U)

rawRestrictG_omegaDGerm

Germ restriction preserves 𝒪_D-sections.

theorem rawRestrictG_omegaDGerm [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] {D : Divisor X} {U V : Opens X} (h : V ≤ U) {f : MGerm U}
    (hf : f ∈ OmegaDGerm D U) : rawRestrictG h f ∈ OmegaDGerm D V