Local Laurent windows and the skyscraper data (CC8, D7, proof plan §6.8)

Unit: cech-cohomology (docs/design/cech-cohomology.md §4.6).

• ordGe p m: germs at the chart source of p with order ≥ m at p.
• tailGerm p m: the local tail germ (z − z_p)^m (junk off the chart source).
• leadCoeff p m: the one-step leading-coefficient functional (D7) — no iterative Laurent coefficient extraction.
• WindowAt p d d': the abstract Laurent window at p between orders −d' and −d.
• diffSupp, Window D D': the skyscraper ⊕_q ℂ^{(D'−D)(q)} in abstract form.
• windowMap: the truncation L(D') → Window D D' (purely structural).

The explicit dimension counts finrank_windowAt/finrank_window (finiteness-and-chi's χ-ledger inputs) are exported from WindowRank.lean instead, via a one-step splitting WindowAt p d d' ≃ₗ WindowAt p d (d'-1) × ℂ and induction (no θ-basis/independence argument needed); the structural exactness in this file does not depend on them.

ordGe

noncomputable def RS.Cech.ordGe {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (p : X) (m : ℤ) : Submodule ℂ (MeroGermOn X (chartAt ℂ p).source)

Germs at the chart source of p with order ≥ m at p.

Equations

• RS.Cech.ordGe p m = { carrier := {ψ : RS.MeroGermOn X (chartAt ℂ p).source | ↑m ≤ ψ.ord p}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem RS.Cech.mem_ordGe_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {p : X} {m : ℤ} {ψ : MeroGermOn X (chartAt ℂ p).source} : ψ ∈ ordGe p m ↔ ↑m ≤ ψ.ord p

tailGerm

theorem RS.Cech.meromorphicOnX_tailGerm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (p : X) (m : ℤ) : MeromorphicOnX (fun (y : X) => (↑(chartAt ℂ p) y - ↑(chartAt ℂ p) p) ^ m) (chartAt ℂ p).source

noncomputable def RS.Cech.tailGerm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (p : X) (m : ℤ) : MeroGermOn X (chartAt ℂ p).source

The local tail germ (z − z_p)^m (junk off the chart source).

Equations

• RS.Cech.tailGerm p m = RS.MeroGermOn.mk (fun (y : X) => (↑(chartAt ℂ p) y - ↑(chartAt ℂ p) p) ^ m) ⋯

theorem RS.Cech.ord_tailGerm_self {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (p : X) (m : ℤ) : (tailGerm p m).ord p = ↑m

noncomputable def RS.Cech.leadCoeff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (p : X) (m : ℤ) : ↥(ordGe p m) →ₗ[ℂ] ℂ

The one-step leading-coefficient functional (D7): ψ ↦ (θ_{p,−m}·ψ).evalAt p on ordGe p m.

Equations

• RS.Cech.leadCoeff p m = { toFun := fun (ψ : ↥(RS.Cech.ordGe p m)) => (RS.Cech.tailGerm p (-m) * ↑ψ).evalAt p, map_add' := ⋯, map_smul' := ⋯ }

WindowAt (the abstract Laurent window)

@[reducible, inline]

noncomputable abbrev RS.Cech.WindowAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (p : X) (d d' : ℤ) : Type u_1

The Laurent window at p between orders −d' and −d, as an abstract quotient (D7) — no coefficient recursion.

Equations

• RS.Cech.WindowAt p d d' = (↥(RS.Cech.ordGe p (-d')) ⧸ Submodule.comap (RS.Cech.ordGe p (-d')).subtype (RS.Cech.ordGe p (-d)))

noncomputable def RS.Cech.WindowAt.mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (p : X) (d d' : ℤ) : ↥(ordGe p (-d')) →ₗ[ℂ] WindowAt p d d'

The quotient map onto the window at p: a germ of order at least -d', taken modulo those of order at least -d.

Equations

• RS.Cech.WindowAt.mk p d d' = (Submodule.comap (RS.Cech.ordGe p (-d')).subtype (RS.Cech.ordGe p (-d))).mkQ

theorem RS.Cech.WindowAt.mk_eq_zero_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {p : X} {d d' : ℤ} (ψ : ↥(ordGe p (-d'))) : (mk p d d') ψ = 0 ↔ ↑(-d) ≤ (↑ψ).ord p

diffSupp, Window

noncomputable def RS.Cech.diffSupp {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] (D D' : Divisor X) : Finset X

Support of the difference divisor, as a Finset (compactness).

Equations

• RS.Cech.diffSupp D D' = ⋯.toFinset

theorem RS.Cech.mem_diffSupp_iff {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] {D D' : Divisor X} {q : X} : q ∈ diffSupp D D' ↔ D q ≠ D' q

@[reducible, inline]

noncomputable abbrev RS.Cech.Window {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T2Space X] [CompactSpace X] (D D' : Divisor X) : Type u_1

The skyscraper window ⊕_q ℂ^{(D'−D)(q)} in abstract form.

Equations

• RS.Cech.Window D D' = ((q : ↥(RS.Cech.diffSupp D D')) → RS.Cech.WindowAt (↑q) (D ↑q) (D' ↑q))

windowMap

noncomputable def RS.Cech.restrictToChart {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D' : Divisor X) (q : X) : ↥(LinSys D') →ₗ[ℂ] ↥(ordGe q (-D' q))

Restriction of a global section to the chart source at q, landing in the ordGe bound coming from L(D')-membership.

Equations

• RS.Cech.restrictToChart D' q = LinearMap.codRestrict (RS.Cech.ordGe q (-D' q)) ((RS.MeroGermOn.restrict ⋯).toLinearMap ∘ₗ (RS.LinSys D').subtype) ⋯

theorem RS.Cech.restrictToChart_apply_coe {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D' : Divisor X) (q : X) (φ : ↥(LinSys D')) : ↑((restrictToChart D' q) φ) = (MeroGermOn.restrict ⋯) ↑φ

noncomputable def RS.Cech.windowMap {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T2Space X] [CompactSpace X] {D D' : Divisor X} (_h : D ≤ D') : ↥(LinSys D') →ₗ[ℂ] Window D D'

Truncation β : L(D') → Window D D' — purely structural (D7).

Equations

• RS.Cech.windowMap _h = LinearMap.pi fun (q : ↥(RS.Cech.diffSupp D D')) => RS.Cech.WindowAt.mk (↑q) (D ↑q) (D' ↑q) ∘ₗ RS.Cech.restrictToChart D' ↑q

theorem RS.Cech.windowMap_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T2Space X] [CompactSpace X] {D D' : Divisor X} (h : D ≤ D') (φ : ↥(LinSys D')) (q : ↥(diffSupp D D')) : (windowMap h) φ q = (WindowAt.mk (↑q) (D ↑q) (D' ↑q)) ((restrictToChart D' ↑q) φ)

theorem RS.Cech.windowMap_eq_zero_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T2Space X] [CompactSpace X] {D D' : Divisor X} (h : D ≤ D') (φ : ↥(LinSys D')) : (windowMap h) φ = 0 ↔ ↑φ ∈ LinSys D

theorem RS.Cech.exact_inclusion_windowMap {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T2Space X] [CompactSpace X] {D D' : Divisor X} (h : D ≤ D') : Function.Exact ⇑(Submodule.inclusion ⋯) ⇑(windowMap h)

Exactness at L(D'): the window map's kernel is exactly L(D) (bottom half of the six-term fragment, Skyscraper.lean supplies the top half).

theorem RS.Cech.inclusion_injective {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D D' : Divisor X} (h : D ≤ D') : Function.Injective ⇑(Submodule.inclusion ⋯)

Dimension counts: see WindowRank.lean

finrank_windowAt (h : d ≤ d') : Module.finrank ℂ (WindowAt p d d') = (d' - d).toNat and finrank_window (h : D ≤ D') : Module.finrank ℂ (Window D D') = ((D' - D).degree).toNat, plus the FiniteDimensional instances, are proved in WindowRank.lean (which imports this file) — via a one-step splitting WindowAt p d d' ≃ₗ WindowAt p d (d'-1) × ℂ (LinearMap.quotKerEquivRange on an explicit "subtract off the leading term" map) and induction on (d' - d).toNat, not the θ-basis/independence argument originally planned in design §6.8 (that argument needed leadCoeff to be defined on the whole numerator ordGe p (-d') for every basis index simultaneously, which it isn't; the one-step splitting sidesteps this by only ever using leadCoeff p (-d'), which is defined on the whole numerator). Every export in this file (ordGe, tailGerm, leadCoeff, WindowAt, Window, windowMap and its exactness/injectivity) is proved with zero sorries and does not depend on the dimension counts.