3.7. Forms.Cover🔗

Jacobians.Forms.Cover — source

iUnion_chartAt_source_eq_univ

Chart sources cover X.

theorem iUnion_chartAt_source_eq_univ {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] :
    (⋃ x : X, (chartAt ℂ x).source) = Set.univ

exists_finite_chart_cover

Compactness of X yields a FINITE set of points whose chart sources cover X.

theorem exists_finite_chart_cover {X : Type*} [TopologicalSpace X] [CompactSpace X]
    [ChartedSpace ℂ X] :
    ∃ (s : Finset X), (⋃ x ∈ s, (chartAt ℂ x).source) = Set.univ

chartCover

The canonical finite chart cover of compact X.

noncomputable def chartCover {X : Type*} [TopologicalSpace X] [CompactSpace X] [ChartedSpace ℂ X] :
    Finset X

chartCover_cover

theorem chartCover_cover {X : Type*} [TopologicalSpace X] [CompactSpace X] [ChartedSpace ℂ X] :
    (⋃ x ∈ (chartCover : Finset X), (chartAt ℂ x).source) = Set.univ

chartCover_nonempty

The canonical finite chart cover is non-empty.

theorem chartCover_nonempty {X : Type*} [TopologicalSpace X] [CompactSpace X] [Nonempty X]
    [ChartedSpace ℂ X] : ((chartCover : Finset X)).Nonempty

chartOpen

The outer open family: each chartOpen x is open, closure contained in coverOpen x = (chartAt ℂ x).source for x ∈ chartCover, and the family covers X.

noncomputable def chartOpen {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] (x : X) : Set X

chartOpen_isOpen

theorem chartOpen_isOpen {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] (x : X) : IsOpen (chartOpen (X := X) x)

closure_chartOpen_subset_coverOpen

theorem closure_chartOpen_subset_coverOpen {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X] (x : X) :
    closure (chartOpen (X := X) x) ⊆ coverOpen (X := X) x

iUnion_chartOpen_eq

theorem iUnion_chartOpen_eq {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] : (⋃ x : X, chartOpen (X := X) x) = Set.univ

innerChartOpen

The inner open family: each innerChartOpen x is open, closure contained in the outer chartOpen x, still covering X.

noncomputable def innerChartOpen {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] (x : X) : Set X

innerChartOpen_isOpen

theorem innerChartOpen_isOpen {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] (x : X) : IsOpen (innerChartOpen (X := X) x)

closure_innerChartOpen_subset_chartOpen

theorem closure_innerChartOpen_subset_chartOpen {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X] (x : X) :
    closure (innerChartOpen (X := X) x) ⊆ chartOpen (X := X) x

iUnion_innerChartOpen_eq

theorem iUnion_innerChartOpen_eq {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] : (⋃ x : X, innerChartOpen (X := X) x) = Set.univ

shrunkChart

Outer closed shrinkage: shrunkChart x := closure (chartOpen x). Has the same API as the previous single-pass shrinkage (closed, ⊆ chart source, covers X), plus the key extra structure chartOpen x ⊆ shrunkChart x with chartOpen x open, which gives innerShrunkChart x ⊆ chartOpen x ⊆ interior (shrunkChart x).

noncomputable def shrunkChart {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] (x : X) : Set X

shrunkChart_isClosed

theorem shrunkChart_isClosed {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] (x : X) : IsClosed (shrunkChart (X := X) x)

shrunkChart_isCompact

theorem shrunkChart_isCompact {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] (x : X) : IsCompact (shrunkChart (X := X) x)

chartOpen_subset_shrunkChart

chartOpen x ⊆ shrunkChart x — the open interior layer inside outer.

theorem chartOpen_subset_shrunkChart {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] (x : X) :
    chartOpen (X := X) x ⊆ shrunkChart (X := X) x

iUnion_shrunkChart_eq

theorem iUnion_shrunkChart_eq {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] : (⋃ x : X, shrunkChart (X := X) x) = Set.univ

shrunkChart_subset_source

shrunkChart x ⊆ (chartAt ℂ x).source when x ∈ chartCover.

theorem shrunkChart_subset_source {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] (x : X) (hx : x ∈ (chartCover : Finset X)) :
    shrunkChart (X := X) x ⊆ (chartAt ℂ x).source

shrunkChart_eq_empty

For x ∉ chartCover, the shrunkChart is empty.

theorem shrunkChart_eq_empty {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] (x : X) (hx : x ∉ (chartCover : Finset X)) :
    shrunkChart (X := X) x = ∅

iUnion_shrunkChart_chartCover_eq

Restricted cover: the shrunkCharts indexed by chartCover still cover X.

theorem iUnion_shrunkChart_chartCover_eq {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X] :
    (⋃ x ∈ (chartCover : Finset X), shrunkChart (X := X) x) = Set.univ

innerShrunkChart

Inner closed shrinkage: innerShrunkChart x := closure (innerChartOpen x). Strictly inside the outer's open interior layer chartOpen x, still covering X.

noncomputable def innerShrunkChart {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] (x : X) : Set X

innerShrunkChart_isClosed

theorem innerShrunkChart_isClosed {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] (x : X) : IsClosed (innerShrunkChart (X := X) x)

innerShrunkChart_isCompact

theorem innerShrunkChart_isCompact {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] (x : X) : IsCompact (innerShrunkChart (X := X) x)

innerShrunkChart_subset_chartOpen

The inner closed set sits inside the outer's open interior.

theorem innerShrunkChart_subset_chartOpen {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X] (x : X) :
    innerShrunkChart (X := X) x ⊆ chartOpen (X := X) x

innerShrunkChart_subset_shrunkChart

Key wiggle-room property: inner ⊆ open ⊆ outer.

theorem innerShrunkChart_subset_shrunkChart {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X] (x : X) :
    innerShrunkChart (X := X) x ⊆ shrunkChart (X := X) x

iUnion_innerShrunkChart_eq

theorem iUnion_innerShrunkChart_eq {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] : (⋃ x : X, innerShrunkChart (X := X) x) = Set.univ

innerChartOpen_eq_empty

For x ∉ chartCover, innerChartOpen is empty (via chartOpen x = ∅ and innerChartOpen ⊆ closure (innerChartOpen) ⊆ chartOpen).

theorem innerChartOpen_eq_empty {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] (x : X) (hx : x ∉ (chartCover : Finset X)) :
    innerChartOpen (X := X) x = ∅

innerShrunkChart_eq_empty

For x ∉ chartCover, innerShrunkChart is empty (since innerChartOpen = ∅).

theorem innerShrunkChart_eq_empty {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] (x : X) (hx : x ∉ (chartCover : Finset X)) :
    innerShrunkChart (X := X) x = ∅

iUnion_innerShrunkChart_chartCover_eq

Restricted cover over chartCover: inner closed sets still cover X.

theorem iUnion_innerShrunkChart_chartCover_eq {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X] :
    (⋃ x ∈ (chartCover : Finset X), innerShrunkChart (X := X) x) = Set.univ

iUnion_innerChartOpen_chartCover_eq

Restricted cover over chartCover: inner OPEN sets cover X. Useful for chart-neighborhood arguments (e.g., Path 2 smoothness).

theorem iUnion_innerChartOpen_chartCover_eq {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X] :
    (⋃ x ∈ (chartCover : Finset X), innerChartOpen (X := X) x) = Set.univ