14.6. Cech.CechRefinement🔗

Jacobians.Cech.CechRefinement — source

IsRefinement

r : 𝔙.ι → 𝔘.ι exhibits 𝔙 as a refinement of 𝔘: each refining set 𝔙.U j is contained in the chosen larger set 𝔘.U (r j). This is exactly the data that induces a restriction map of Čech cochains Cochain^k 𝔘 → Cochain^k 𝔙 (reindex by r, restrict along 𝔙.U j ≤ 𝔘.U (r j)). (𝔙 being a cover is recorded in 𝔙.covers; the refinement datum only needs the per-index containment.)

def IsRefinement (𝔙 𝔘 : FiniteCover X) (r : 𝔙.ι → 𝔘.ι) : Prop

pair_le

On a pairwise overlap, the refining overlap sits inside the reindexed coarse overlap: 𝔙.U a ⊓ 𝔙.U b ≤ 𝔘.U (r a) ⊓ 𝔘.U (r b).

theorem pair_le (h : IsRefinement 𝔙 𝔘 r) (a b : 𝔙.ι) :
    𝔙.U a ⊓ 𝔙.U b ≤ 𝔘.U (r a) ⊓ 𝔘.U (r b)

triple_le

On a triple overlap, the refining overlap sits inside the reindexed coarse triple overlap.

theorem triple_le (h : IsRefinement 𝔙 𝔘 r) (a b c : 𝔙.ι) :
    𝔙.U a ⊓ 𝔙.U b ⊓ 𝔙.U c ≤ 𝔘.U (r a) ⊓ 𝔘.U (r b) ⊓ 𝔘.U (r c)

refineC0

Refinement on 0-cochains: (refineC0 c)_j = c_{r j} |_{𝔙.U j}.

noncomputable def refineC0 : 𝔘.Cochain0 →ₗ[ℂ] 𝔙.Cochain0

refineC0_apply

@[simp] theorem refineC0_apply (c : 𝔘.Cochain0) (j : 𝔙.ι) :
    h.refineC0 c j = rawRestrictG (h j) (c (r j))

refineC1

Refinement on 1-cochains: (refineC1 g)_{ab} = g_{(r a)(r b)} |_{𝔙.U a ⊓ 𝔙.U b}.

noncomputable def refineC1 : 𝔘.Cochain1 →ₗ[ℂ] 𝔙.Cochain1

refineC1_apply

@[simp] theorem refineC1_apply (g : 𝔘.Cochain1) (p : 𝔙.ι × 𝔙.ι) :
    h.refineC1 g p = rawRestrictG (h.pair_le p.1 p.2) (g (r p.1, r p.2))

refineC2

Refinement on 2-cochains.

noncomputable def refineC2 : 𝔘.Cochain2 →ₗ[ℂ] 𝔙.Cochain2

refineC2_apply

@[simp] theorem refineC2_apply (g : 𝔘.Cochain2) (t : 𝔙.ι × 𝔙.ι × 𝔙.ι) :
    h.refineC2 g t = rawRestrictG (h.triple_le t.1 t.2.1 t.2.2) (g (r t.1, r t.2.1, r t.2.2))

refineC1_comp_cechDelta0

δ⁰ is natural for refinement. δ⁰_𝔙 ∘ refineC0 = refineC1 ∘ δ⁰_𝔘: refining then taking the fine coboundary equals taking the coarse coboundary then refining. Componentwise on (a,b) both sides are c_{r b}|_{𝔙ab} − c_{r a}|_{𝔙ab} (nested restrictions collapse).

theorem refineC1_comp_cechDelta0 :
    𝔙.cechDelta0 ∘ₗ h.refineC0 = h.refineC1 ∘ₗ 𝔘.cechDelta0

refineC2_comp_cechDelta1

δ¹ is natural for refinement. δ¹_𝔙 ∘ refineC1 = refineC2 ∘ δ¹_𝔘. Componentwise on the triple (a,b,c) both sides are the alternating sum g_{(rb)(rc)} − g_{(ra)(rc)} + g_{(ra)(rb)}, each germ-restricted to 𝔙.U a ⊓ 𝔙.U b ⊓ 𝔙.U c (nested restrictions collapse).

theorem refineC2_comp_cechDelta1 :
    𝔙.cechDelta1 ∘ₗ h.refineC1 = h.refineC2 ∘ₗ 𝔘.cechDelta1

refineC0_mem_sections0

Refinement maps 𝒪_D 0-sections to 𝒪_D 0-sections.

theorem refineC0_mem_sections0 [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    {c : 𝔘.Cochain0} (hc : c ∈ 𝔘.sections0 D) :
    h.refineC0 c ∈ 𝔙.sections0 D

refineC1_mem_sections1

Refinement maps 𝒪_D 1-sections to 𝒪_D 1-sections.

theorem refineC1_mem_sections1 [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    {g : 𝔘.Cochain1} (hg : g ∈ 𝔘.sections1 D) :
    h.refineC1 g ∈ 𝔙.sections1 D

refineC1_mem_cocycles1

Refinement maps 𝒪_D 1-cocycles to 𝒪_D 1-cocycles (refineC1 sends ker δ¹_𝔘 into ker δ¹_𝔙 by the chain-map property, and preserves the 𝒪_D sections).

theorem refineC1_mem_cocycles1 [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    {g : 𝔘.Cochain1} (hg : g ∈ 𝔘.cocycles1 D) :
    h.refineC1 g ∈ 𝔙.cocycles1 D

refineC1_mem_coboundaries1

Refinement maps 𝒪_D 1-coboundaries to 𝒪_D 1-coboundaries (a coboundary δ⁰_𝔘 c with c an 𝒪_D 0-section refines to δ⁰_𝔙 (refineC0 c) via the chain-map property, with refineC0 c again an 𝒪_D 0-section).

theorem refineC1_mem_coboundaries1 [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    {g : 𝔘.Cochain1} (hg : g ∈ 𝔘.coboundaries1 D) :
    h.refineC1 g ∈ 𝔙.coboundaries1 D

refineZ1

The cocycle-level refinement map Z¹(𝔘, 𝒪_D) →ₗ[ℂ] Z¹(𝔙, 𝒪_D): refineC1 corestricted to the cocycle subspaces (using refineC1_mem_cocycles1).

noncomputable def refineZ1 [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] :
    ↥(𝔘.cocycles1 D) →ₗ[ℂ] ↥(𝔙.cocycles1 D)

refineH1

The induced map on Čech H¹ cechH1 𝔘 D →ₗ[ℂ] cechH1 𝔙 D (refineH1). The cocycle-level refinement refineZ1 sends 𝒪_D-coboundaries on 𝔘 to 𝒪_D-coboundaries on 𝔙 (refineC1_mem_coboundaries1), so it descends to the H¹ = Z¹/B¹ quotients (Submodule.mapQ). This is the comparison arrow the Leray cover-independence isomorphism is built on — the standard chain-homotopy argument shows it is a bijection when both covers are Leray (CechRefinementLeray).

noncomputable def refineH1 [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] : 𝔘.cechH1 D →ₗ[ℂ] 𝔙.cechH1 D

refineH1_mk

@[simp] theorem refineH1_mk [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    (g : ↥(𝔘.cocycles1 D)) :
    h.refineH1 D (Submodule.Quotient.mk g) = Submodule.Quotient.mk (h.refineZ1 D g)

id

The identity is a refinement of a cover by itself (𝔘.U i ≤ 𝔘.U (id i)).

theorem id (𝔘 : FiniteCover X) : IsRefinement 𝔘 𝔘 id

comp

A composite of refinement-index maps s : 𝔚.ι → 𝔙.ι, r : 𝔙.ι → 𝔘.ι is a refinement-index map 𝔚 → 𝔘 via r ∘ s.

theorem comp {s : 𝔚.ι → 𝔙.ι} {r : 𝔙.ι → 𝔘.ι}
    (hs : IsRefinement 𝔚 𝔙 s) (hr : IsRefinement 𝔙 𝔘 r) :
    IsRefinement 𝔚 𝔘 (r ∘ s)