19.6. Finiteness.CechFinitenessAbstract🔗

Jacobians.Finiteness.CechFinitenessAbstract — source

finiteDimensional_h1_of_leray_compact

Abstract finiteness reduction (Forster 14.9 core). Let δ : C0 →L Z1V (the coboundary C⁰(𝔙) → Z¹(𝔙)) and ρ : Z1U →L Z1V (the restriction Z¹(𝔘) → Z¹(𝔙)) be maps of Banach spaces such that the combined map (η,ξ) ↦ δη + ρξ is surjective (the Leray condition — restriction is onto on H¹) and ρ is a compact operator (Montel). Then Z1V ⧸ range δ (i.e. H¹(𝔙)) is finite-dimensional.

Proof: with A := δ⊕ρ (surjective) and K := 0⊕(−ρ) (compact), A + K = δ⊕0 so range (A+K) = range δ = B¹; the Schwartz lemma gives Z1V ⧸ range δ finite-dimensional.

theorem finiteDimensional_h1_of_leray_compact
    {C0 Z1U Z1V : Type*}
    [NormedAddCommGroup C0] [NormedSpace ℂ C0] [CompleteSpace C0]
    [NormedAddCommGroup Z1U] [NormedSpace ℂ Z1U] [CompleteSpace Z1U]
    [NormedAddCommGroup Z1V] [NormedSpace ℂ Z1V] [CompleteSpace Z1V]
    (δ : C0 →L[ℂ] Z1V) (ρ : Z1U →L[ℂ] Z1V)
    (hsurj : Function.Surjective (fun p : C0 × Z1U => δ p.1 + ρ p.2))
    (hρ : IsCompactOperator ρ) :
    FiniteDimensional ℂ (Z1V ⧸ LinearMap.range δ.toLinearMap)

isCompactOperator_pi

Finite product of compact operators is compact. For a finite index ι, the product map Πᵢ Kᵢ : (∀ i, E i) →L (∀ i, F i) of compact operators Kᵢ is compact (it is the finite sum ∑ᵢ single_i ∘ Kᵢ ∘ proj_i). This makes the cochain restriction C^q(𝔘) → C^q(𝔙) (componentwise over the finite pair-index of the cover) a compact operator from the per-overlap BddHol.isCompactOperator_restrictCLM, providing the ρ input of finiteDimensional_h1_of_leray_compact.

theorem isCompactOperator_pi {ι : Type*} [Fintype ι] [DecidableEq ι] {E F : ι → Type*}
    [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace ℂ (E i)]
    [∀ i, NormedAddCommGroup (F i)] [∀ i, NormedSpace ℂ (F i)]
    (K : ∀ i, E i →L[ℂ] F i) (hK : ∀ i, IsCompactOperator (K i)) :
    IsCompactOperator (pi (fun i => (K i).comp (proj i)) : (∀ i, E i) →L[ℂ] (∀ i, F i))

isCompactOperator_of_subtypeL_comp

A compact operator into a closed subspace is compact. If g : E →L p (into a *closed* submodule p ≤ F) becomes compact after including into F (p.subtypeL ∘ g compact), then g is compact. Needed so the cochain restriction ρ, viewed as landing in the closed cocycle subspace Z¹(𝔙), is a compact operator (the ρ input of finiteDimensional_h1_of_leray_compact).

theorem isCompactOperator_of_subtypeL_comp {E F : Type*}
    [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F]
    {p : Submodule ℂ F} (hp : IsClosed (p : Set F)) (g : E →L[ℂ] p)
    (h : IsCompactOperator (p.subtypeL.comp g)) : IsCompactOperator g