Window dimension counts (CC8, D7, proof plan §6.8) #

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

evalAt_eq_zero_iff [Compat]: chart-transported analogue of mathlib's tendsto_zero_iff_meromorphicOrderAt_pos, filed as a request to meromorphic-and-divisors (docs/requests/meromorphic-and-divisors.md) but not upstreamed — proved here from exported chart-transport lemmas only.
leadCoeff_eq_zero_iff: the one-step leading-coefficient functional detects the exact order.
finrank_windowAt/finrank_window: the θ-basis dimension counts (design §6.8), via an explicit one-step splitting WindowAt p d d' ≃ₗ WindowAt p d (d'-1) × ℂ and induction on (d' - d).toNat (no explicit basis/independence argument needed).

Compat: chart-transported vanishing criterion for `evalAt` #

theorem RS.Cech.tendsto_zero_iff_ordAtX_pos {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} (hf : MeromorphicAtX f x) :

Filter.Tendsto f (nhdsWithin x {x}ᶜ) (nhds 0) ↔ 0 < ordAtX f x

Compat (requested from meromorphic-and-divisors, not upstreamed): chart-transported analogue of mathlib's tendsto_zero_iff_meromorphicOrderAt_pos.

source

theorem RS.Cech.MeroGermOn.evalAt_eq_zero_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {x : X} (hU : IsOpen U) (hx : x ∈ U) (φ : MeroGermOn X U) (h : 0 ≤ φ.ord x) :

φ.evalAt x = 0 ↔ 0 < φ.ord x

Compat (requested from meromorphic-and-divisors §1.4(b), not upstreamed): evalAt vanishes (given 0 ≤ ord) iff the order is strictly positive.

`leadCoeff` detects the exact order #

source

theorem RS.Cech.leadCoeff_eq_zero_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (p : X) (m : ℤ) (ψ : ↥(ordGe p m)) :

(leadCoeff p m) ψ = 0 ↔ ↑(m + 1) ≤ (↑ψ).ord p

source

theorem RS.Cech.leadCoeff_tailGerm_self_ne_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (p : X) (m : ℤ) :

(leadCoeff p m) ⟨tailGerm p m, ⋯⟩ ≠ 0

Leading-coefficient normalization (up to a nonzero scalar, all that induction needs): leadCoeff p m (θ_{p,m}) ≠ 0.

The one-step splitting `WindowAt p d d' ≃ₗ WindowAt p d (d'-1) × ℂ` #

The dimension count, by induction on `(d' - d).toNat` #

source

theorem RS.Cech.finrank_windowAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {p : X} {d d' : ℤ} (h : d ≤ d') :

Module.finrank ℂ (WindowAt p d d') = (d' - d).toNat

source

theorem RS.Cech.finiteDimensional_windowAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (p : X) {d d' : ℤ} (h : d ≤ d') :

FiniteDimensional ℂ (WindowAt p d d')

`finrank_window`: the global (Pi-of-windows) dimension count #

source

@[instance_reducible]

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

AddCommGroup (WindowAt p d d')

Registered explicitly (same reason as Jacobian/Cech/Cochains.lean's Z1/H1Cover instances): Window D D' := ∀ q, WindowAt (q:X) (D q) (D' q) is a Pi type, so its Module ℂ/Module.Free ℂ structure needs these per-factor instances solved as a dependent Pi-instance goal — the newer toolchain's synthInstance no longer reliably re-derives that from WindowAt's own (quotient) definition on demand. Supplying them once, directly, for the generic WindowAt p d d' lets every downstream Pi-dependent lookup match verbatim instead of re-deriving them.