19.29. Finiteness.SkyscraperAssembly🔗

Jacobians.Finiteness.SkyscraperAssembly — source

coeffB0

The component-i principal-part coefficient functional on B0 = sections0(D+P): b ↦ coeffGermLin (b i) at the cover-set U i ∋ P.

noncomputable def coeffB0 {i : 𝔘.ι} (hP : P ∈ 𝔘.U i) :
    ↥(𝔘.sections0 (D + Finsupp.single P 1)) →ₗ[ℂ] ℂ

coeffB0_apply

@[simp] theorem coeffB0_apply {i : 𝔘.ι} (hP : P ∈ 𝔘.U i)
    (b : ↥(𝔘.sections0 (D + Finsupp.single P 1))) :
    𝔘.coeffB0 D P hP b
      = coeffGermLin hP (⟨(b : 𝔘.Cochain0) i, b.2 i⟩ :
          OmegaDGerm (D + Finsupp.single P 1) (𝔘.U i))

mem_OmegaDGerm_of_overlap_diff

Overlap transport up to 𝒪_D (the case P ∈ V). If on the overlap U ⊓ V the difference of the two germs is an 𝒪_D-germ (hdiff), with γU ∈ OmegaDGerm D U and γV ∈ OmegaDGerm (D+P) V, then γV already lies in the smaller OmegaDGerm D V. The order of γV at P (read on V) equals the order of γU + (difference) at P (via the overlap), and both summands have order ≥ −(D P), so mem_OmegaD_iff_ordU_at_P upgrades γV's membership. Generalises mem_OmegaDGerm_of_overlap_match (exact match = zero difference).

theorem mem_OmegaDGerm_of_overlap_diff {U V : Opens X} {D : Divisor X} {P : X}
    (hPU : P ∈ U) (hPV : P ∈ V) {γU : MGerm U} {γV : MGerm V}
    (hγU : γU ∈ OmegaDGerm D U) (hγV : γV ∈ OmegaDGerm (D + Finsupp.single P 1) V)
    (hdiff : rawRestrictG (inf_le_right : U ⊓ V ≤ V) γV
        - rawRestrictG (inf_le_left : U ⊓ V ≤ U) γU
      ∈ OmegaDGerm D (U ⊓ V)) :
    γV ∈ OmegaDGerm D V

sections1_matching_diff

The quotient-cocycle matching extracted from δ⁰b ∈ sections1 D: on each overlap U i ⊓ U j, the difference rawRestrictG b_j − rawRestrictG b_i is an 𝒪_D-germ. (For a genuine cocycle δ⁰b = 0 this difference is 0; here it is only required to be 𝒪_D, the H0Q/quotient condition.)

theorem sections1_matching_diff {b : 𝔘.Cochain0}
    (hb : 𝔘.cechDelta0 b ∈ 𝔘.sections1 D) (i j : 𝔘.ι) :
    rawRestrictG (inf_le_right : 𝔘.U i ⊓ 𝔘.U j ≤ 𝔘.U j) (b j)
        - rawRestrictG (inf_le_left : 𝔘.U i ⊓ 𝔘.U j ≤ 𝔘.U i) (b i)
      ∈ OmegaDGerm D (𝔘.U i ⊓ 𝔘.U j)

quotient_component_mem_iff_all

Quotient-cocycle propagation of 𝒪_D-membership. For a 𝒪_{D+P}-cochain b whose Čech coboundary is an 𝒪_D-cochain (δ⁰b ∈ sections1 D — the H0Q condition) and a star vertex U i ∋ P, the component on U i lies in 𝒪_D iff *every* component lies in 𝒪_D (i.e. b is an 𝒪_D-cochain). Forward is trivial; backward propagates: off the star (P ∉ U j) the order bounds coincide, and on the star the order at P transports from U i across the overlap up to an 𝒪_D-germ (mem_OmegaDGerm_of_overlap_diff).

theorem quotient_component_mem_iff_all {i : 𝔘.ι} (hP : P ∈ 𝔘.U i)
    {b : 𝔘.Cochain0} (hbsec : b ∈ 𝔘.sections0 (D + Finsupp.single P 1))
    (hbcoc : 𝔘.cechDelta0 b ∈ 𝔘.sections1 D) :
    b i ∈ OmegaDGerm D (𝔘.U i) ↔ ∀ j, b j ∈ OmegaDGerm D (𝔘.U j)

sections0_le_ker_coeffB0

A0 = sections0 D ≤ ker (coeffB0): an 𝒪_D-cochain has vanishing principal-part coefficient at P (its component on U i lies in 𝒪_D, so coeffGermLin = 0 by ker_coeffGermLin).

theorem sections0_le_ker_coeffB0 {i : 𝔘.ι} (hP : P ∈ 𝔘.U i) :
    (𝔘.sections0 D).submoduleOf (𝔘.sections0 (D + Finsupp.single P 1))
      ≤ LinearMap.ker (𝔘.coeffB0 D P hP)

coeffQ0

The principal-part coefficient descended to the quotient Q0 = B0/A0 (kills A0 by sections0_le_ker_coeffB0). coeffQ0 (mk b) = coeffB0 b.

noncomputable def coeffQ0 {i : 𝔘.ι} (hP : P ∈ 𝔘.U i) :
    (𝔘.skyscraperTwoStep D P).Q0 →ₗ[ℂ] ℂ

coeffQ0_mk

@[simp] theorem coeffQ0_mk {i : 𝔘.ι} (hP : P ∈ 𝔘.U i)
    (b : (𝔘.skyscraperTwoStep D P).B0) :
    𝔘.coeffQ0 D P hP (Submodule.Quotient.mk b) = 𝔘.coeffB0 D P hP b

e0Lin

The realization map H0Q → ℂ: the principal-part coefficient coeffQ0 precomposed with the inclusion H0Q ↪ Q0.

noncomputable def e0Lin {i : 𝔘.ι} (hP : P ∈ 𝔘.U i) :
    (𝔘.skyscraperTwoStep D P).H0Q →ₗ[ℂ] ℂ

e0Lin_apply

@[simp] theorem e0Lin_apply {i : 𝔘.ι} (hP : P ∈ 𝔘.U i)
    (x : (𝔘.skyscraperTwoStep D P).H0Q) :
    𝔘.e0Lin D P hP x = 𝔘.coeffQ0 D P hP (x : (𝔘.skyscraperTwoStep D P).Q0)

cechDelta0_mem_sections1_of_mem_H0Q

A H0Q = ker dQ0 element, lifted to B0, has δ⁰-coboundary in sections1 D (the quotient cocycle condition dQ0[b] = 0 unfolds to δ⁰b ∈ A1 = sections1 D).

theorem cechDelta0_mem_sections1_of_mem_H0Q (b : (𝔘.skyscraperTwoStep D P).B0)
    (hq : Submodule.Quotient.mk b ∈ (𝔘.skyscraperTwoStep D P).H0Q) :
    𝔘.cechDelta0 (b.1 : 𝔘.Cochain0) ∈ 𝔘.sections1 D

e0Lin_injective

Injectivity of the realization map. If the principal-part coefficient at U i vanishes for a H0Q-class [b], then (since δ⁰b ∈ 𝒪_D, the H0Q condition) every component of b lies in 𝒪_D (quotient_component_mem_iff_all), so b ∈ A0 and [b] = 0.

theorem e0Lin_injective {i : 𝔘.ι} (hP : P ∈ 𝔘.U i) :
    Function.Injective (𝔘.e0Lin D P hP)

witnessCochain

The single-cover-set witness cochain: the scaled principal part on U i, 0 elsewhere.

noncomputable def witnessCochain {i : 𝔘.ι} (hP : P ∈ 𝔘.U i) (a : ℂ) : 𝔘.Cochain0

witnessCochain_self

theorem witnessCochain_self {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (𝔘 : FiniteCover X) (D : Divisor X) (P : X) [DecidableEq 𝔘.ι] {i : 𝔘.ι}
    (hP : P ∈ 𝔘.U i) (a : ℂ) :
    𝔘.witnessCochain D P hP a i
      = toGerm (𝔘.U i) (a • witnessFn (⟨P, hP⟩ : 𝔘.U i) (-(D P) - 1))

witnessCochain_of_ne

theorem witnessCochain_of_ne {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (𝔘 : FiniteCover X) (D : Divisor X) (P : X) [DecidableEq 𝔘.ι] {i : 𝔘.ι}
    (hP : P ∈ 𝔘.U i) (a : ℂ) {j : 𝔘.ι} (hj : j ≠ i) :
    𝔘.witnessCochain D P hP a j = 0

witnessCochain_self_mem

The witness germ on U i (scaled by a) is an 𝒪_{D+P}-germ, given the witness membership hwit.

theorem witnessCochain_self_mem {i : 𝔘.ι} (hP : P ∈ 𝔘.U i) (a : ℂ)
    (hwit : witnessFn (⟨P, hP⟩ : 𝔘.U i) (-(D P) - 1) ∈ OmegaD (D + Finsupp.single P 1) (𝔘.U i)) :
    𝔘.witnessCochain D P hP a i ∈ OmegaDGerm (D + Finsupp.single P 1) (𝔘.U i)

witnessCochain_mem_sections0

The witness cochain lies in B0 = sections0(D+P) (component i from hwit, others are 0).

theorem witnessCochain_mem_sections0 {i : 𝔘.ι} (hP : P ∈ 𝔘.U i) (a : ℂ)
    (hwit : witnessFn (⟨P, hP⟩ : 𝔘.U i) (-(D P) - 1) ∈ OmegaD (D + Finsupp.single P 1) (𝔘.U i)) :
    𝔘.witnessCochain D P hP a ∈ 𝔘.sections0 (D + Finsupp.single P 1)

witness_restrict_mem_omegaD_off_P

Under the singleton-star hypothesis, any overlap-set W ≤ U i that also lies in some U k with k ≠ i avoids P (P ∈ W → P ∈ U k → k = i), so the witness germ restricted to W is an 𝒪_D-germ (the D and D+P bounds coincide off P).

theorem witness_restrict_mem_omegaD_off_P {i : 𝔘.ι} (hP : P ∈ 𝔘.U i) (a : ℂ)
    (hwit : witnessFn (⟨P, hP⟩ : 𝔘.U i) (-(D P) - 1) ∈ OmegaD (D + Finsupp.single P 1) (𝔘.U i))
    {W : Opens X} (hWi : W ≤ 𝔘.U i) (hPW : P ∉ W) :
    rawRestrictG hWi (𝔘.witnessCochain D P hP a i) ∈ OmegaDGerm D W

cechDelta0_witnessCochain_mem_sections1

The witness cochain is a Q-cocycle (its Čech coboundary is an 𝒪_D-cochain), under the singleton-star hypothesis. The only nonzero component is b i, so each overlap component (δ⁰b)_{jk} is ± the witness restricted to an overlap with the star vertex U i; by hstar such an overlap with a *different* cover-set avoids P, where the witness is an 𝒪_D-germ.

theorem cechDelta0_witnessCochain_mem_sections1 {i : 𝔘.ι} (hP : P ∈ 𝔘.U i) (a : ℂ)
    (hwit : witnessFn (⟨P, hP⟩ : 𝔘.U i) (-(D P) - 1) ∈ OmegaD (D + Finsupp.single P 1) (𝔘.U i))
    (hstar : ∀ j, P ∈ 𝔘.U j → j = i) :
    𝔘.cechDelta0 (𝔘.witnessCochain D P hP a) ∈ 𝔘.sections1 D

witnessB0

The witness cochain, as an element of B0 = sections0(D+P).

noncomputable def witnessB0 {i : 𝔘.ι} (hP : P ∈ 𝔘.U i) (a : ℂ)
    (hwit : witnessFn (⟨P, hP⟩ : 𝔘.U i) (-(D P) - 1) ∈ OmegaD (D + Finsupp.single P 1) (𝔘.U i)) :
    (𝔘.skyscraperTwoStep D P).B0

witnessB0_mk_mem_H0Q

The witness class lies in H0Q = ker dQ0 (the cocycle condition δ⁰b ∈ 𝒪_D).

theorem witnessB0_mk_mem_H0Q {i : 𝔘.ι} (hP : P ∈ 𝔘.U i) (a : ℂ)
    (hwit : witnessFn (⟨P, hP⟩ : 𝔘.U i) (-(D P) - 1) ∈ OmegaD (D + Finsupp.single P 1) (𝔘.U i))
    (hstar : ∀ j, P ∈ 𝔘.U j → j = i) :
    Submodule.Quotient.mk (𝔘.witnessB0 D P hP a hwit) ∈ (𝔘.skyscraperTwoStep D P).H0Q

coeffGermLin_witnessCochain

The realization reads the witness coefficient as a: coeffGermLin (a • witness) = a.

theorem coeffGermLin_witnessCochain {i : 𝔘.ι} (hP : P ∈ 𝔘.U i) (a : ℂ)
    (hwit : witnessFn (⟨P, hP⟩ : 𝔘.U i) (-(D P) - 1) ∈ OmegaD (D + Finsupp.single P 1) (𝔘.U i)) :
    coeffGermLin hP (⟨𝔘.witnessCochain D P hP a i, 𝔘.witnessCochain_self_mem D P hP a hwit⟩ :
      OmegaDGerm (D + Finsupp.single P 1) (𝔘.U i)) = a

e0Lin_surjective

Surjectivity of the realization map, under the singleton-star hypothesis (plus the witness membership hwit): the witness class realises coefficient a.

theorem e0Lin_surjective {i : 𝔘.ι} (hP : P ∈ 𝔘.U i)
    (hwit : witnessFn (⟨P, hP⟩ : 𝔘.U i) (-(D P) - 1) ∈ OmegaD (D + Finsupp.single P 1) (𝔘.U i))
    (hstar : ∀ j, P ∈ 𝔘.U j → j = i) :
    Function.Surjective (𝔘.e0Lin D P hP)

e0

The local-realization isomorphism e0 : H0Q ≃ₗ[ℂ] ℂ, under the witness membership hwit and the singleton-star hypothesis hstar. The principal-part coefficient e0Lin is bijective (e0Lin_injective / e0Lin_surjective).

noncomputable def e0 {i : 𝔘.ι} (hP : P ∈ 𝔘.U i)
    (hwit : witnessFn (⟨P, hP⟩ : 𝔘.U i) (-(D P) - 1) ∈ OmegaD (D + Finsupp.single P 1) (𝔘.U i))
    (hstar : ∀ j, P ∈ 𝔘.U j → j = i) :
    (𝔘.skyscraperTwoStep D P).H0Q ≃ₗ[ℂ] ℂ

e0_apply

@[simp] theorem e0_apply {i : 𝔘.ι} (hP : P ∈ 𝔘.U i)
    (hwit : witnessFn (⟨P, hP⟩ : 𝔘.U i) (-(D P) - 1) ∈ OmegaD (D + Finsupp.single P 1) (𝔘.U i))
    (hstar : ∀ j, P ∈ 𝔘.U j → j = i) (x : (𝔘.skyscraperTwoStep D P).H0Q) :
    𝔘.e0 D P hP hwit hstar x = 𝔘.e0Lin D P hP x

e0_hcompat

Compatibility of e0 with the principal-part arrow h0ToSky: h0ToSky = e0 ∘ h0Map. Both sides read the order-(−D(P)−1) coefficient of the component on U i; h0Map is mkQ, and e0 is the descended coefficient, so this is definitional up to the (germ-only-dependent) coefficient functional.

theorem e0_hcompat {i : 𝔘.ι} (hP : P ∈ 𝔘.U i)
    (hwit : witnessFn (⟨P, hP⟩ : 𝔘.U i) (-(D P) - 1) ∈ OmegaD (D + Finsupp.single P 1) (𝔘.U i))
    (hstar : ∀ j, P ∈ 𝔘.U j → j = i) :
    𝔘.h0ToSky D P hP
      = (𝔘.e0 D P hP hwit hstar : (𝔘.skyscraperTwoStep D P).H0Q →ₗ[ℂ] ℂ).comp
          (𝔘.skyscraperTwoStep D P).h0Map

sections1_component_omegaD_off_diag

Off the diagonal (i,i), a sections1 (D+P)-component is automatically a sections1 D-component (the overlap avoids P by hstar, so the order bounds coincide).

theorem sections1_component_omegaD_off_diag {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (𝔘 : FiniteCover X) (D : Divisor X) (P : X) {i : 𝔘.ι}
    (hstar : ∀ j, P ∈ 𝔘.U j → j = i) {g : 𝔘.Cochain1}
    (hg : g ∈ 𝔘.sections1 (D + Finsupp.single P 1)) {j k : 𝔘.ι} (hjk : ¬(j = i ∧ k = i)) :
    g (j, k) ∈ OmegaDGerm D (𝔘.U j ⊓ 𝔘.U k)

mem_OmegaDGerm_of_restrict_triple

Membership reflection across the idempotent triple overlap. For the diagonal triple U i ⊓ U i ⊓ U i (which equals the double U i ⊓ U i), restriction reflects 𝒪_D-membership: if the restriction of γ : MGerm (U i ⊓ U i) to the triple lies in 𝒪_D, then so does γ (compose with the reverse inclusion, which round-trips to the identity).

theorem mem_OmegaDGerm_of_restrict_triple {i : 𝔘.ι} {γ : MGerm (𝔘.U i ⊓ 𝔘.U i)}
    (h : rawRestrictG
        (le_inf (inf_le_left.trans inf_le_right) inf_le_right :
          𝔘.U i ⊓ 𝔘.U i ⊓ 𝔘.U i ≤ 𝔘.U i ⊓ 𝔘.U i) γ
      ∈ OmegaDGerm D (𝔘.U i ⊓ 𝔘.U i ⊓ 𝔘.U i)) :
    γ ∈ OmegaDGerm D (𝔘.U i ⊓ 𝔘.U i)

sections1_component_omegaD_diag

On the diagonal (i,i), the cocycle condition δ¹g ∈ 𝒪_D (component (i,i,i)) forces the component g_{ii} to be an 𝒪_D-germ. The three terms of (δ¹g)_{iii} are restrictions of the SAME component g_{ii} (all indices are i); two cancel (proof-irrelevant equal inclusions), leaving one restriction to the triple overlap, which lies in 𝒪_D; reflection (mem_OmegaDGerm_of_restrict_triple) brings it back to the double overlap.

theorem sections1_component_omegaD_diag {i : 𝔘.ι} {g : 𝔘.Cochain1}
    (hcoc : 𝔘.cechDelta1 g ∈ 𝔘.sections2 D) :
    g (i, i) ∈ OmegaDGerm D (𝔘.U i ⊓ 𝔘.U i)

dQ1_mk_eq_zero_imp

A Q1-element mk gB in ker dQ1 is 0: the cocycle condition δ¹(gB) ∈ 𝒪_D plus hstar puts every component of gB in 𝒪_D (off-diagonal automatically, on the diagonal via the triple-overlap reflection), so gB ∈ A1 and [gB] = 0.

theorem dQ1_mk_eq_zero_imp {i : 𝔘.ι} (hP : P ∈ 𝔘.U i)
    (hstar : ∀ j, P ∈ 𝔘.U j → j = i) (gB : (𝔘.skyscraperTwoStep D P).B1)
    (hq : (𝔘.skyscraperTwoStep D P).dQ1 (Submodule.Quotient.mk gB) = 0) :
    (Submodule.Quotient.mk gB : (𝔘.skyscraperTwoStep D P).Q1) = 0

subsingleton_H1Q

Acyclicity H¹(Q) = 0 under the singleton-star hypothesis: every Q-1-cocycle is 0 in Q1 (dQ1_mk_eq_zero_imp), so ker dQ1 = ⊥ and H¹(Q) = ker dQ1 / range dQ0 is trivial.

theorem subsingleton_H1Q {i : 𝔘.ι} (hP : P ∈ 𝔘.U i)
    (hstar : ∀ j, P ∈ 𝔘.U j → j = i) :
    Subsingleton (𝔘.skyscraperTwoStep D P).H1Q

localRealizationData

The LocalRealizationData datum, under the witness membership hwit and the singleton-star hypothesis hstar (both standard chart-disk-cover properties), with H⁰(𝒪_{D+P}) finiteness supplied as an instance. This is the deliverable that SkyscraperSnake.skyscraperLES_of_localRealization consumes to produce the four remaining SkyscraperLES fields, completing CohomologicalRR.exists_skyscraperLES via the 1-line wire exists_skyscraperLES := ⟨skyscraperLES_of_localRealization (𝔘.localRealizationData …)⟩.

e0/hcompat/hQac are proven above (e0, e0_hcompat, subsingleton_H1Q); finH1D/finH1DP come from finiteDimensional_cechH1_wired (the only axiom route, via the finiteness track).

noncomputable def localRealizationData {i : 𝔘.ι} (hP : P ∈ 𝔘.U i)
    (hwit : witnessFn (⟨P, hP⟩ : 𝔘.U i) (-(D P) - 1) ∈ OmegaD (D + Finsupp.single P 1) (𝔘.U i))
    (hstar : ∀ j, P ∈ 𝔘.U j → j = i)
    [FiniteDimensional ℂ ↥(𝔘.globalSections (D + Finsupp.single P 1))] :
    𝔘.LocalRealizationData D P

localRealizationData_of_chartDisk

LocalRealizationData from the chart-disk-cover hypotheses (discharging hwit via witnessFn_mem_OmegaD_add_single): on a cover-set U i ∋ P whose ↥(U i)-chart source covers all of U i (hWsrc) and where D is supported on U i only at P (hDsupp), with the singleton-star property hstar and H⁰(𝒪_{D+P}) finiteness, the realization datum exists.

noncomputable def localRealizationData_of_chartDisk {i : 𝔘.ι} (hP : P ∈ 𝔘.U i)
    (hWsrc : ∀ Q : 𝔘.U i, Q ∈ (chartAt (H := ℂ) (⟨P, hP⟩ : 𝔘.U i)).source)
    (hDsupp : ∀ Q : 𝔘.U i, Q ≠ ⟨P, hP⟩ → D Q.1 = 0)
    (hstar : ∀ j, P ∈ 𝔘.U j → j = i)
    [FiniteDimensional ℂ ↥(𝔘.globalSections (D + Finsupp.single P 1))] :
    𝔘.LocalRealizationData D P

skyscraperLES_of_chartDisk

LocalRealizationData from the chart-disk-cover hypotheses (discharging hwit via witnessFn_mem_OmegaD_add_single): on a cover-set U i ∋ P whose ↥(U i)-chart source covers all of U i (hWsrc) and where D is supported on U i only at P (hDsupp), with the singleton-star property hstar and H⁰(𝒪_{D+P}) finiteness, the realization datum exists. -/ noncomputable def localRealizationData_of_chartDisk {i : 𝔘.ι} (hP : P ∈ 𝔘.U i) (hWsrc : ∀ Q : 𝔘.U i, Q ∈ (chartAt (H := ℂ) (⟨P, hP⟩ : 𝔘.U i)).source) (hDsupp : ∀ Q : 𝔘.U i, Q ≠ ⟨P, hP⟩ → D Q.1 = 0) (hstar : ∀ j, P ∈ 𝔘.U j → j = i) [FiniteDimensional ℂ ↥(𝔘.globalSections (D + Finsupp.single P 1))] : 𝔘.LocalRealizationData D P := 𝔘.localRealizationData D P hP (witnessFn_mem_OmegaD_add_single hP hWsrc hDsupp) hstar

/-! ### The skyscraper LES from the chart-disk-cover hypotheses (the full assembly, discharged)

This is CohomologicalRR.exists_skyscraperLES with its genuine geometric prerequisites made *explicit* rather than (impossibly) derived from IsLeray. It feeds the chart-disk realization datum (localRealizationData_of_chartDisk) through the snake assembly (skyscraperLES_of_localRealization) — and the *only* axiom dependency beyond propext/Classical.choice/Quot.sound is the finiteness axiom carried by the H¹-finiteness instances (finiteDimensional_cechH1_wired, axiom-backed via the OTHER track exists_cechModel). Together with the H⁰(𝒪_{D+P}) finiteness *instance* hypothesis (Forster compactness, l(D+P) < ∞; no such lemma exists in the repo, kept honest as an instance), it pins down *exactly* the residual content of exists_skyscraperLES:

exists_skyscraperLES 𝔘 hL D P reduces to supplying, for the given D/P, 1. a cover-set U i ∋ P (hP), 2. hWsrc: ↥(U i)'s chart at P has source all of U i, 3. hDsupp: D is supported on U i only at P, 4. hstar: the star of P is the single vertex i, 5. [FiniteDimensional ℂ H⁰(𝒪_{D+P})], none of which follow from IsLeray alone (a generic Leray cover need not be a chart-disk cover with a singleton star at P and D supported only at P). The snake lemma, local realization, witness surjectivity, and H¹(Q) = 0 are all proven above.

noncomputable def skyscraperLES_of_chartDisk {i : 𝔘.ι} (hP : P ∈ 𝔘.U i)
    (hWsrc : ∀ Q : 𝔘.U i, Q ∈ (chartAt (H := ℂ) (⟨P, hP⟩ : 𝔘.U i)).source)
    (hDsupp : ∀ Q : 𝔘.U i, Q ≠ ⟨P, hP⟩ → D Q.1 = 0)
    (hstar : ∀ j, P ∈ 𝔘.U j → j = i)
    [FiniteDimensional ℂ ↥(𝔘.globalSections (D + Finsupp.single P 1))] :
    SkyscraperLES 𝔘 D P