19.12. Finiteness.CechModelBridge🔗

Jacobians.Finiteness.CechModelBridge — source

bcfCompContinuousₗ

Bounded-continuous precomposition f ↦ f ∘ g as a ℂ-linear map (α →ᵇ ℂ) →ₗ[ℂ] (β →ᵇ ℂ) for g : C(β, α).

noncomputable def bcfCompContinuousₗ {α β : Type*} [TopologicalSpace α] [TopologicalSpace β]
    (g : C(β, α)) : (α →ᵇ ℂ) →ₗ[ℂ] (β →ᵇ ℂ) where

bcfCompContinuousₗ_apply

@[simp] theorem bcfCompContinuousₗ_apply {α β : Type*} [TopologicalSpace α] [TopologicalSpace β]
    (g : C(β, α)) (f : α →ᵇ ℂ) : bcfCompContinuousₗ g f = f.compContinuous g

bcfCompContinuousCLM

Bounded-continuous precomposition continuous-linear map (α →ᵇ ℂ) →L[ℂ] (β →ᵇ ℂ) for g : C(β, α), operator norm ≤ 1. The shrinking-side transport of a sup-norm cochain component (through a chart transition or an inclusion of compacts).

noncomputable def bcfCompContinuousCLM {α β : Type*} [TopologicalSpace α] [TopologicalSpace β]
    (g : C(β, α)) : (α →ᵇ ℂ) →L[ℂ] (β →ᵇ ℂ)

bcfCompContinuousCLM_apply

@[simp] theorem bcfCompContinuousCLM_apply {α β : Type*} [TopologicalSpace α] [TopologicalSpace β]
    (g : C(β, α)) (f : α →ᵇ ℂ) : bcfCompContinuousCLM g f = f.compContinuous g

toFun_neg

@[simp] theorem toFun_neg (f : BddHol U) : (-f).toFun = -f.toFun

toFun_sub

@[simp] theorem toFun_sub (f g : BddHol U) : (f - g).toFun = f.toFun - g.toFun

ofAnalyticOn

The BddHol codomain constructor (most-upstream K-bridge atom). An analytic, bounded function on an open U ⊆ ℂ gives a BddHol U element, via the canonical extend-by-zero normal form off U (which BddHolCarrier requires and which changes nothing on U).

noncomputable def ofAnalyticOn (g : ℂ → ℂ) (ha : AnalyticOn ℂ g U)
    (hb : ∃ C, ∀ z ∈ U, ‖g z‖ ≤ C) : BddHol U

ofAnalyticOn_toFun_of_mem

@[simp] theorem ofAnalyticOn_toFun_of_mem (g : ℂ → ℂ) (ha : AnalyticOn ℂ g U)
    (hb : ∃ C, ∀ z ∈ U, ‖g z‖ ≤ C) {z : ℂ} (hz : z ∈ U) :
    (ofAnalyticOn g ha hb).toFun z = g z

bddOn_of_analyticOn_subset_compact

Boundedness on a relatively-compact piece. An analytic function on U is bounded on any compact K ⊆ U (it is continuous, hence bounded on the compact). This supplies the BddHol boundedness hypothesis: a cochain holomorphic on a cover-open is bounded on the (relatively-compact) shrinking.

theorem bddOn_of_analyticOn_subset_compact {g : ℂ → ℂ} {U K : Set ℂ}
    (hg : AnalyticOn ℂ g U) (hK : IsCompact K) (hKU : K ⊆ U) :
    ∃ C, ∀ z ∈ K, ‖g z‖ ≤ C

ofAnalyticOnOfRelCompact

The practical K-bridge constructor. A function analytic on an open U, restricted to an open U' whose closure is a compact subset of U (U' ⋐ U), is a BddHol U' element — the boundedness is automatic on the relatively-compact piece. This is the shape the germ→BddHol cochain map uses: cover-cochains are holomorphic on the cover-open U, the model lives on the shrinking U' ⋐ U.

noncomputable def ofAnalyticOnOfRelCompact {g : ℂ → ℂ} {U U' : Set ℂ} (hg : AnalyticOn ℂ g U)
    (hsub : closure U' ⊆ U) (hcpt : IsCompact (closure U')) : BddHol U'

ofAnalyticOnOfRelCompact_toFun_of_mem

@[simp] theorem ofAnalyticOnOfRelCompact_toFun_of_mem {g : ℂ → ℂ} {U U' : Set ℂ}
    (hg : AnalyticOn ℂ g U) (hsub : closure U' ⊆ U) (hcpt : IsCompact (closure U'))
    {z : ℂ} (hz : z ∈ U') :
    (ofAnalyticOnOfRelCompact hg hsub hcpt).toFun z = g z

precompHol

Transport g : BddHol U across an analytic reindexing τ : U' → U, landing in BddHol U' (value g ∘ τ, extended by zero off U'). The cross-chart cover-side transport of a sup-norm cochain component.

noncomputable def precompHol {U U' : Set ℂ} {τ : ℂ → ℂ} (hτ : AnalyticOn ℂ τ U')
    (hτmaps : Set.MapsTo τ U' U) (g : BddHol U) : BddHol U'

precompHol_toFun_of_mem

@[simp] theorem precompHol_toFun_of_mem {U U' : Set ℂ} {τ : ℂ → ℂ} (hτ : AnalyticOn ℂ τ U')
    (hτmaps : Set.MapsTo τ U' U) (g : BddHol U) {z : ℂ} (hz : z ∈ U') :
    (precompHol hτ hτmaps g).toFun z = g.toFun (τ z)

precompHol_add

theorem precompHol_add {U U' : Set ℂ} {τ : ℂ → ℂ} (hτ : AnalyticOn ℂ τ U')
    (hτmaps : Set.MapsTo τ U' U) (g₁ g₂ : BddHol U) :
    precompHol hτ hτmaps (g₁ + g₂) = precompHol hτ hτmaps g₁ + precompHol hτ hτmaps g₂

precompHol_smul

theorem precompHol_smul {U U' : Set ℂ} {τ : ℂ → ℂ} (hτ : AnalyticOn ℂ τ U')
    (hτmaps : Set.MapsTo τ U' U) (c : ℂ) (g : BddHol U) :
    precompHol hτ hτmaps (c • g) = c • precompHol hτ hτmaps g

precompHolₗ

Cross-chart transport as a ℂ-linear map BddHol U →ₗ[ℂ] BddHol U'.

noncomputable def precompHolₗ {U U' : Set ℂ} {τ : ℂ → ℂ} (hτ : AnalyticOn ℂ τ U')
    (hτmaps : Set.MapsTo τ U' U) : BddHol U →ₗ[ℂ] BddHol U' where

precompHolCLM

Cross-chart transport continuous-linear map BddHol U →L[ℂ] BddHol U' for τ analytic U' → U, operator norm ≤ 1. The open-set (analytic) counterpart of precompCLM, used to transport cover-side sup-norm cochain components across the holomorphic chart transitions.

noncomputable def precompHolCLM {U U' : Set ℂ} {τ : ℂ → ℂ} (hτ : AnalyticOn ℂ τ U')
    (hτmaps : Set.MapsTo τ U' U) : BddHol U →L[ℂ] BddHol U'

precompHolCLM_apply

@[simp] theorem precompHolCLM_apply {U U' : Set ℂ} {τ : ℂ → ℂ} (hτ : AnalyticOn ℂ τ U')
    (hτmaps : Set.MapsTo τ U' U) (g : BddHol U) :
    precompHolCLM hτ hτmaps g = precompHol hτ hτmaps g

restrictOpenCLM

Open-subset restriction g ↦ g|_{U'} as a BddHol U →L[ℂ] BddHol U' (U' ⊆ U open), operator norm ≤ 1. The same-chart (diagonal) cover-side transport of a sup-norm cochain component: precompHol with the identity reindexing.

noncomputable def restrictOpenCLM {U U' : Set ℂ} (hsub : U' ⊆ U) : BddHol U →L[ℂ] BddHol U'

restrictOpenCLM_toFun_of_mem

@[simp] theorem restrictOpenCLM_toFun_of_mem {U U' : Set ℂ} (hsub : U' ⊆ U) (g : BddHol U)
    {z : ℂ} (hz : z ∈ U') : (restrictOpenCLM hsub g).toFun z = g.toFun z

uniformEquicontinuousOn_of_bounded_analyticOn_of_compact

Uniform equicontinuity of a bounded analytic family on a non-convex compact. A family of functions analytic on an open U ⊆ ℂ and uniformly bounded by C on U is uniformly equicontinuous on *any* compact K ⊆ U, with no convexity assumption (cf. Montel.uniformEquicontinuousOn_of_bounded_analyticOn which requires Convex ℝ K).

theorem uniformEquicontinuousOn_of_bounded_analyticOn_of_compact
    {ι : Type*} {U K : Set ℂ} {f : ι → ℂ → ℂ} {C : ℝ}
    (hU : IsOpen U) (hKcpt : IsCompact K) (hKU : K ⊆ U) (hCnn : 0 ≤ C)
    (hf : ∀ i, AnalyticOn ℂ (f i) U)
    (hfb : ∀ i, ∀ z ∈ U, ‖f i z‖ ≤ C) :
    UniformEquicontinuousOn f K

isCompact_closure_restrict_bddHolo_of_compact

Non-convex Montel atom. A sup-M-bounded family of functions holomorphic on an open U ⊆ ℂ, restricted to *any* compact K ⋐ U, is relatively compact in K →ᵇ ℂ — the convexity-free analogue of CechFiniteness.isCompact_closure_restrict_bddHolo. Convexity is no longer needed thanks to uniformEquicontinuousOn_of_bounded_analyticOn_of_compact.

theorem isCompact_closure_restrict_bddHolo_of_compact
    {U K : Set ℂ} (hU : IsOpen U) (hKcpt : IsCompact K) (hKU : K ⊆ U)
    {M : ℝ} (hMnn : 0 ≤ M)
    {S : Type*} (g : S → ℂ → ℂ)
    (hg_an : ∀ s, AnalyticOn ℂ (g s) U) (hg_bd : ∀ s, ∀ z ∈ U, ‖g s z‖ ≤ M)
    (hg_cont : ∀ s, ContinuousOn (g s) U) :
    letI : CompactSpace K

isCompactOperator_restrictCLM_of_compact

Restriction is a compact operator for a general (non-convex) compact K ⋐ U. The convexity-free generalization of BddHol.isCompactOperator_restrictCLM: for U open and K ⊆ U compact (no Convex ℝ K), restrictCLM : BddHol U →L[ℂ] (K →ᵇ ℂ) is a compact operator. Same Montel reduction (isCompactOperator_iff_isCompact_closure_image_closedBall), now feeding the non-convex atom isCompact_closure_restrict_bddHolo_of_compact. This unblocks DiskOverlapData for cross-chart overlaps, whose chart-images are not convex.

theorem isCompactOperator_restrictCLM_of_compact {U K : Set ℂ} [CompactSpace K]
    (hU : IsOpen U) (hKcpt : IsCompact K) (hKU : K ⊆ U) :
    IsCompactOperator (restrictCLM (U := U) hKU)

isCompactOperator_restrictCLM_toBcf_of_compact

Restriction to a relatively compact open, viewed as a bounded-continuous function on U', is compact via the compact closure closure U'. This is the corrected-model bridge: first restrict to the compact closure, then postcompose by inclusion U' ↪ closure U'.

theorem isCompactOperator_restrictCLM_toBcf_of_compact {U U' : Set ℂ} [CompactSpace (closure U')]
    (hU : IsOpen U) (hKcpt : IsCompact (closure U')) (hsub : closure U' ⊆ U) :
    IsCompactOperator (fun f : BddHol U =>
      (restrictCLM (U := U) (K := closure U') hsub f).compContinuous
        (ContinuousMap.inclusion (subset_closure : U' ⊆ closure U')))

restrictCLM_toBcf_eq_restrictOpenCLM_toBcf

The U'-level bounded-continuous restriction obtained by restricting to closure U' and then including U' ↪ closure U' is the same as the direct open restriction BddHol U → BddHol U' followed by toBcf. This is the exact bridge a corrected holomorphic-shrinking model will consume.

@[simp] theorem restrictCLM_toBcf_eq_restrictOpenCLM_toBcf {U U' : Set ℂ}
    [CompactSpace (closure U')] (hsub : closure U' ⊆ U) (f : BddHol U) :
    (bcfCompContinuousCLM (ContinuousMap.inclusion (subset_closure : U' ⊆ closure U')))
      (restrictCLM (U := U) (K := closure U') hsub f) =
      (restrictOpenCLM (U := U) (U' := U') (subset_closure.trans hsub) f).toBcf

isCompactOperator_restrictOpenCLM_of_compact

The open-to-open holomorphic restriction BddHol U → BddHol U' is compact when U' ⋐ U. We prove compactness after embedding into U' →ᵇ ℂ via toBcf, then pull compactness back through the closed embedding toBcf.

theorem isCompactOperator_restrictOpenCLM_of_compact {U U' : Set ℂ}
    (hU : IsOpen U) (hU' : IsOpen U') (hKcpt : IsCompact (closure U')) (hsub : closure U' ⊆ U) :
    IsCompactOperator (restrictOpenCLM (U := U) (U' := U') (subset_closure.trans hsub))