Finite covers and their refinement preorder (CC8, D2/D3/D4)

Unit: cech-cohomology (docs/design/cech-cohomology.md §4.1, D2–D4, proof plans §6.2–§6.3).

• FinCover Ω (Ω : Opens X): a Fin n-indexed family of opens contained in Ω and covering it. Small (Type u, no universe bump).
• Refinement preorder: 𝒰 ≤ 𝒱 iff 𝒱 refines 𝒰 (IsRefIdx, chosenRefIdx); FinCover.meet gives pairwise meets, hence IsDirectedOrder.
• IsChartDisk/FinCover.IsGood: chart-disk covers, a cofinal class (exists_good_refinement, exists_good_refinement_closure).
• FinCover.IsAdapted: adapted covers (Miranda IX Ex. 3.6), exists_adapted_refinement.

FinCover and the refinement preorder (D2/D3)

structure RS.Cech.FinCover {X : Type u_1} [TopologicalSpace X] (Ω : TopologicalSpace.Opens X) : Type u_1

A finite cover of the open set Ω by opens of X, indexed by Fin n (D2).

• n : ℕ

  The number of members of the cover.

• U : Fin self.n → TopologicalSpace.Opens X

  The members of the cover.

• le_base (i : Fin self.n) : self.U i ≤ Ω
• covers (x : X) : x ∈ Ω → ∃ (i : Fin self.n), x ∈ self.U i

def RS.Cech.FinCover.single {X : Type u_1} [TopologicalSpace X] (Ω : TopologicalSpace.Opens X) : FinCover Ω

The trivial one-member cover {Ω}.

Equations

• RS.Cech.FinCover.single Ω = { n := 1, U := fun (x : Fin 1) => Ω, le_base := ⋯, covers := ⋯ }

instance RS.Cech.instNonemptyFinCover {X : Type u_1} [TopologicalSpace X] {Ω : TopologicalSpace.Opens X} : Nonempty (FinCover Ω)

def RS.Cech.IsRefIdx {X : Type u_1} [TopologicalSpace X] {Ω : TopologicalSpace.Opens X} (𝒰 𝒱 : FinCover Ω) (τ : Fin 𝒱.n → Fin 𝒰.n) : Prop

τ is a valid refinement index from 𝒰 to 𝒱: each member of 𝒱 sits inside the τ-indexed member of 𝒰 (D3).

Equations

• RS.Cech.IsRefIdx 𝒰 𝒱 τ = ∀ (k : Fin 𝒱.n), 𝒱.U k ≤ 𝒰.U (τ k)

@[instance_reducible]

instance RS.Cech.instPreorderFinCover {X : Type u_1} [TopologicalSpace X] {Ω : TopologicalSpace.Opens X} : Preorder (FinCover Ω)

Equations

• RS.Cech.instPreorderFinCover = { le := fun (𝒰 𝒱 : RS.Cech.FinCover Ω) => ∃ (τ : Fin 𝒱.n → Fin 𝒰.n), RS.Cech.IsRefIdx 𝒰 𝒱 τ, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

theorem RS.Cech.le_def {X : Type u_1} [TopologicalSpace X] {Ω : TopologicalSpace.Opens X} {𝒰 𝒱 : FinCover Ω} : 𝒰 ≤ 𝒱 ↔ ∃ (τ : Fin 𝒱.n → Fin 𝒰.n), IsRefIdx 𝒰 𝒱 τ

noncomputable def RS.Cech.chosenRefIdx {X : Type u_1} [TopologicalSpace X] {Ω : TopologicalSpace.Opens X} {𝒰 𝒱 : FinCover Ω} (h : 𝒰 ≤ 𝒱) : Fin 𝒱.n → Fin 𝒰.n

A chosen (classical) refinement index witnessing 𝒰 ≤ 𝒱.

Equations

• RS.Cech.chosenRefIdx h = Exists.choose h

theorem RS.Cech.chosenRefIdx_spec {X : Type u_1} [TopologicalSpace X] {Ω : TopologicalSpace.Opens X} {𝒰 𝒱 : FinCover Ω} (h : 𝒰 ≤ 𝒱) : IsRefIdx 𝒰 𝒱 (chosenRefIdx h)

Pairwise meets and directedness

def RS.Cech.FinCover.meet {X : Type u_1} [TopologicalSpace X] {Ω : TopologicalSpace.Opens X} (𝒰 𝒱 : FinCover Ω) : FinCover Ω

The pairwise meet of two covers (member-wise ⊓, reindexed by Fin (m*n) ≃ Fin m × Fin n).

Equations

• 𝒰.meet 𝒱 = { n := 𝒰.n * 𝒱.n, U := fun (p : Fin (𝒰.n * 𝒱.n)) => 𝒰.U (finProdFinEquiv.symm p).1 ⊓ 𝒱.U (finProdFinEquiv.symm p).2, le_base := ⋯, covers := ⋯ }

theorem RS.Cech.le_meet_left {X : Type u_1} [TopologicalSpace X] {Ω : TopologicalSpace.Opens X} (𝒰 𝒱 : FinCover Ω) : 𝒰 ≤ 𝒰.meet 𝒱

theorem RS.Cech.le_meet_right {X : Type u_1} [TopologicalSpace X] {Ω : TopologicalSpace.Opens X} (𝒰 𝒱 : FinCover Ω) : 𝒱 ≤ 𝒰.meet 𝒱

instance RS.Cech.instIsDirectedOrderFinCover {X : Type u_1} [TopologicalSpace X] {Ω : TopologicalSpace.Opens X} : IsDirectedOrder (FinCover Ω)

@[instance_reducible]

noncomputable instance RS.Cech.instDecidableEqFinCover {X : Type u_1} [TopologicalSpace X] {Ω : TopologicalSpace.Opens X} : DecidableEq (FinCover Ω)

Equations

• RS.Cech.instDecidableEqFinCover = Classical.decEq (RS.Cech.FinCover Ω)

Chart-disk covers (D4)

def RS.Cech.IsChartDisk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (V : TopologicalSpace.Opens X) : Prop

V is a chart disk: some chart maps it bijectively onto a round ball (D4).

Equations

• RS.Cech.IsChartDisk V = ∃ (x : X) (r : ℝ), 0 < r ∧ x ∈ V ∧ ↑V ⊆ (chartAt ℂ x).source ∧ ↑(chartAt ℂ x) '' ↑V = Metric.ball (↑(chartAt ℂ x) x) r

def RS.Cech.FinCover.IsGood {X : Type u_1} [TopologicalSpace X] {Ω : TopologicalSpace.Opens X} [ChartedSpace ℂ X] (𝒰 : FinCover Ω) : Prop

A cover all of whose members are chart disks.

Equations

• 𝒰.IsGood = ∀ (i : Fin 𝒰.n), RS.Cech.IsChartDisk (𝒰.U i)

theorem RS.Cech.exists_chartDisk_basis {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {x : X} {W : Set X} (hW : W ∈ nhds x) : ∃ (V : TopologicalSpace.Opens X), IsChartDisk V ∧ x ∈ V ∧ ↑V ⊆ W

Every neighbourhood of a point contains a chart-disk neighbourhood of it (§6.3).

theorem RS.Cech.exists_chartDisk_closure_basis {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T2Space X] {x : X} {W : Set X} (hW : W ∈ nhds x) : ∃ (V : TopologicalSpace.Opens X), IsChartDisk V ∧ x ∈ V ∧ closure ↑V ⊆ W ∧ IsCompact (closure ↑V)

Compact-closure version: the chart-disk neighbourhood can be chosen with compact closure inside the given neighbourhood (§6.3, needs [T2Space X]).

theorem RS.Cech.exists_good_refinement {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [CompactSpace X] (𝒰 : FinCover ⊤) : ∃ (𝒱 : FinCover ⊤), 𝒰 ≤ 𝒱 ∧ 𝒱.IsGood

Chart-disk covers are cofinal (§6.3): every cover of X admits a good refinement.

theorem RS.Cech.exists_good_refinement_closure {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [CompactSpace X] [T2Space X] (𝒰 : FinCover ⊤) : ∃ (𝒱 : FinCover ⊤) (τ : Fin 𝒱.n → Fin 𝒰.n), IsRefIdx 𝒰 𝒱 τ ∧ 𝒱.IsGood ∧ ∀ (k : Fin 𝒱.n), closure ↑(𝒱.U k) ⊆ ↑(𝒰.U (τ k)) ∧ IsCompact (closure ↑(𝒱.U k))

Compact-closure good refinement (§6.3) — the nested-cover input for finiteness-and-chi.

Adapted covers (Miranda IX Ex. 3.6)

def RS.Cech.FinCover.IsAdapted {X : Type u_1} [TopologicalSpace X] {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) (S : Finset X) : Prop

𝒰 is adapted to the finite set S: each point of S lies in exactly one member.

Equations

• 𝒰.IsAdapted S = ∀ p ∈ S, ∃! i : Fin 𝒰.n, p ∈ 𝒰.U i

def RS.Cech.compOpens {X : Type u_1} [TopologicalSpace X] [T1Space X] (T : Finset X) : TopologicalSpace.Opens X

The open complement of a finite set ([T1Space X]).

Equations

• RS.Cech.compOpens T = { carrier := (↑T)ᶜ, is_open' := ⋯ }

theorem RS.Cech.mem_compOpens {X : Type u_1} [TopologicalSpace X] [T1Space X] {T : Finset X} {x : X} : x ∈ compOpens T ↔ x ∉ T

theorem RS.Cech.exists_adapted_refinement {X : Type u_1} [TopologicalSpace X] {Ω : TopologicalSpace.Opens X} [T1Space X] (𝒰 : FinCover Ω) (S : Finset X) (hS : ∀ p ∈ S, p ∈ Ω) (O : X → TopologicalSpace.Opens X) (hO : ∀ p ∈ S, p ∈ O p) : ∃ (𝒱 : FinCover Ω), 𝒰 ≤ 𝒱 ∧ 𝒱.IsAdapted S ∧ ∀ p ∈ S, ∀ (k : Fin 𝒱.n), p ∈ 𝒱.U k → 𝒱.U k ≤ O p

Refine a cover so that it is adapted to a finite set S ⊆ Ω, respecting prescribed neighbourhoods O p of each p ∈ S (§6.2; pure finite-lattice bookkeeping, [T1Space X]). Deviation from the design doc: an explicit hS : ∀ p ∈ S, p ∈ Ω hypothesis is added — without it 𝒱.IsAdapted S is unprovable for points of S outside Ω (every member of a FinCover Ω lies inside Ω); every use site has Ω = ⊤, where the hypothesis is trivial.

theorem RS.Cech.FinCover.IsAdapted.not_mem_inf {X : Type u_1} [TopologicalSpace X] {Ω : TopologicalSpace.Opens X} {𝒰 : FinCover Ω} {S : Finset X} (h𝒰 : 𝒰.IsAdapted S) {p : X} (hp : p ∈ S) {i j : Fin 𝒰.n} (hij : i ≠ j) : p ∉ 𝒰.U i ⊓ 𝒰.U j

If 𝒰 is adapted to S, distinct members meet S in at most disjoint points: no member other than the unique one containing p also contains it (immediate from IsAdapted, kept as a named export for the skyscraper unit).