19.19. Finiteness.CechRefinementInjective🔗

Jacobians.Finiteness.CechRefinementInjective — source

Gext_eventuallyEq_of_subOpen

A germ-class agreement between two ↥W-functions on a sub-open A ≤ W upgrades, near each point of A, to a punctured-neighbourhood agreement of their extensions-by-zero on X. (Pull the ↥(A)-germ agreement back to X via eventually_nhdsNE_of_subtype; on the overlap the extensions are the functions themselves by Gext_apply_mem.)

theorem Gext_eventuallyEq_of_subOpen {X : Type*} [TopologicalSpace X] {W A : Opens X}
    (hAW : A ≤ W) (fa fb : W → ℂ)
    (hagree : toGerm A (fa ∘ openIncl hAW) = toGerm A (fb ∘ openIncl hAW))
    {x : X} (hx : x ∈ A) :
    Gext fa =ᶠ[𝓝[≠] x] Gext fb

omegaDGerm_separated

Sheaf axiom I (separation) for germ-class 𝒪_D-sections. If two germ-classes on an open W restrict to the *same* germ-class on every member A k of a cover of W, they are equal. (Each point of ↥W lies in some A k, where the two agree; that agreement pulls back to a punctured-neighbourhood agreement on ↥W.)

theorem omegaDGerm_separated {X : Type*} [TopologicalSpace X] {W : Opens X} {K : Type*}
    (A : K → Opens X) (hAW : ∀ k, A k ≤ W)
    (hcov : ⨆ k, A k = W) (a b : MGerm W)
    (hagree : ∀ k, rawRestrictG (hAW k) a = rawRestrictG (hAW k) b) :
    a = b

isMeromorphic_of_Gext_meromorphicAt

A function on ↥U is meromorphic on ↥U once its extension-by-zero Gext g is meromorphic at each point of U (read in X's chart) — the converse direction of Gext_meromorphicAt, via the same Gext_chart_bridge.

theorem isMeromorphic_of_Gext_meromorphicAt {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    {U : Opens X}
    {g : U → ℂ}
    (h : ∀ y ∈ U,
      MeromorphicAt (Gext g ∘ (chartAt (H := ℂ) y).symm) ((chartAt (H := ℂ) y) y)) :
    IsMeromorphic (U : Type _) g

omegaDGerm_glue

Sheaf axiom II (gluing) for germ-class 𝒪_D-sections. A matching family (s k)_k of 𝒪_D-germs over a cover (A k)_k of an open W glues to a single h ∈ OmegaDGerm D W whose restriction to each A k is s k. This is the W-local form of CechH0.cechRestrictL_surjective: extract honest representatives gA k ∈ OmegaD D (A k), extend each by 0, and glue them by the per-point meromorphic-normal-form recipe (toMeromorphicNFAt). The glued function agrees off a discrete set near every point of W with the local member whose patch contains the point, so it is meromorphic on ↥W, satisfies the order bound, and has the prescribed germ on each A k.

theorem omegaDGerm_glue {W : Opens X} {K : Type*} (A : K → Opens X) (hAW : ∀ k, A k ≤ W)
    (hcov : ⨆ k, A k = W) (s : Π k, MGerm (A k)) (hs : ∀ k, s k ∈ OmegaDGerm D (A k))
    (hmatch : ∀ k l, rawRestrictG (inf_le_left : A k ⊓ A l ≤ A k) (s k)
      = rawRestrictG (inf_le_right : A k ⊓ A l ≤ A l) (s l)) :
    ∃ h ∈ OmegaDGerm D W, ∀ k, rawRestrictG (hAW k) h = s k

coverInf_iSup

The cover {𝔘.U i ⊓ 𝔙.U k}_k of the coarse set 𝔘.U i (used per coarse index in Forster 12.4).

theorem coverInf_iSup {X : Type*} [TopologicalSpace X] {𝔙 𝔘 : FiniteCover X} (i : 𝔘.ι) :
    ⨆ k, (𝔘.U i ⊓ 𝔙.U k) = 𝔘.U i

coverInf2_iSup

The cover {𝔘.U i ⊓ 𝔘.U j ⊓ 𝔙.U k}_k of the coarse overlap 𝔘.U i ⊓ 𝔘.U j.

theorem coverInf2_iSup {X : Type*} [TopologicalSpace X] {𝔙 𝔘 : FiniteCover X} (i j : 𝔘.ι) :
    ⨆ k, (𝔘.U i ⊓ 𝔘.U j ⊓ 𝔙.U k) = 𝔘.U i ⊓ 𝔘.U j

cocycleRel

The Čech cocycle relation g_{ac} = g_{ab} + g_{bc} on the triple overlap, extracted from δ¹ g = 0 (the alternating-sum identity of cechDelta1). Stated as germ equality on 𝔘.U a ⊓ 𝔘.U b ⊓ 𝔘.U c, ready to be further restricted via rawRestrictG_comp_apply.

theorem cocycleRel {X : Type*} [TopologicalSpace X] {𝔘 : FiniteCover X} {gc : 𝔘.Cochain1}
    (hg : gc ∈ LinearMap.ker 𝔘.cechDelta1) (a b c : 𝔘.ι) :
    rawRestrictG (le_inf (inf_le_left.trans inf_le_left) inf_le_right :
        𝔘.U a ⊓ 𝔘.U b ⊓ 𝔘.U c ≤ 𝔘.U a ⊓ 𝔘.U c) (gc (a, c))
      = rawRestrictG (inf_le_left : 𝔘.U a ⊓ 𝔘.U b ⊓ 𝔘.U c ≤ 𝔘.U a ⊓ 𝔘.U b) (gc (a, b))
        + rawRestrictG (le_inf (inf_le_left.trans inf_le_right) inf_le_right :
            𝔘.U a ⊓ 𝔘.U b ⊓ 𝔘.U c ≤ 𝔘.U b ⊓ 𝔘.U c) (gc (b, c))

refinementDescend_unconditional

Forster 12.4 (unconditional injectivity), the descend predicate. For ANY refinement hr : IsRefinement 𝔙 𝔘 r, a 𝔘-cocycle whose refinement is a 𝔙-coboundary is itself a 𝔘-coboundary. No acyclicity / Leray hypothesis (cf. the conditional refinementDescend_of_isDiskAcyclic). The proof is the standard sheaf-gluing argument; the only nontrivial inputs are the germ-class 𝒪_D sheaf gluing (omegaDGerm_glue) and separation (omegaDGerm_separated).

theorem refinementDescend_unconditional (hr : IsRefinement 𝔙 𝔘 r) :
    RefinementDescend hr D

refineH1_injective_unconditional

Forster 12.4: the refinement map on H¹ is injective UNCONDITIONALLY. For ANY refinement hr : IsRefinement 𝔙 𝔘 r, refineH1 hr is injective — with NO acyclicity / Leray hypothesis on either cover (contrast refineH1_injective, which needs a back-refinement). Immediate from refinementDescend_unconditional via refineH1_injective_iff_descend.

theorem refineH1_injective_unconditional (hr : IsRefinement 𝔙 𝔘 r) :
    Function.Injective (hr.refineH1 D)