19.13. Finiteness.CechModelDelta🔗

Jacobians.Finiteness.CechModelDelta — source

coverSetImage

The chart-image of cover set a — the open set in ℂ (in chart-a coordinates) where the 0-cochain component over a is bounded-holomorphic.

noncomputable def coverSetImage (a : Fin ((chartCover : Finset X).card)) : Set ℂ

isOpen_coverSetImage

theorem isOpen_coverSetImage {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] (a : Fin ((chartCover : Finset X).card)) :
    IsOpen (coverSetImage (X := X) a)

Cochain0Model

Sup-norm 0-cochains. Bounded-holomorphic on each cover set's chart-image — the genuine Čech C⁰ for the chart cover, in the BddHol representation.

abbrev Cochain0Model : Type

coverTripleImage

Open chart-a image of the triple outer overlap chartOpen a ∩ chartOpen b ∩ chartOpen c.

noncomputable def coverTripleImage (t : Fin ((chartCover : Finset X).card) ×
    Fin ((chartCover : Finset X).card) × Fin ((chartCover : Finset X).card)) : Set ℂ

isOpen_coverTripleImage

theorem isOpen_coverTripleImage {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] (t : Fin ((chartCover : Finset X).card) ×
    Fin ((chartCover : Finset X).card) × Fin ((chartCover : Finset X).card)) :
    IsOpen (coverTripleImage (X := X) t)

coverTripleShrink

Compact chart-a image of the triple inner overlap innerShrunkChart a ∩ innerShrunkChart b ∩ innerShrunkChart c (the shrinking, ⊆ coverTripleImage).

noncomputable def coverTripleShrink (t : Fin ((chartCover : Finset X).card) ×
    Fin ((chartCover : Finset X).card) × Fin ((chartCover : Finset X).card)) : Set ℂ

isCompact_coverTripleShrink

theorem isCompact_coverTripleShrink {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] (t : Fin ((chartCover : Finset X).card) ×
    Fin ((chartCover : Finset X).card) × Fin ((chartCover : Finset X).card)) :
    IsCompact (coverTripleShrink (X := X) t)

Cochain2CovModel

Sup-norm 2-cochains, cover side C²cov — bounded-holomorphic on each open triple chart-image (target of the cover-side δ¹).

abbrev Cochain2CovModel : Type

Cochain2Model

Sup-norm 2-cochains, shrinking side C² — bounded-continuous on each compact inner triple chart-image (target of the shrinking-side δ¹).

abbrev Cochain2Model : Type