Evaluation.lean`

41 declarations, 0 contain sorry, 0 declared as axioms

Smooth generating sections, evaluation maps, and complex-linear bundle maps.

def OAI.Kaplansky.tupleEvaluation line 25
theorem OAI.Kaplansky.tupleEvaluation_apply line 28
theorem OAI.Kaplansky.tupleEvaluation_surjective line 31
def OAI.Kaplansky.tupleEvaluationLinear line 37
def OAI.Kaplansky.tupleEvaluationMap line 44
theorem OAI.Kaplansky.tupleEvaluation_smooth line 47
theorem OAI.Kaplansky.complex_smul_decomposition line 56

def OAI.Kaplansky.complexOfCommuteI line 63

Source documentation

Upgrade a real-linear map commuting with the complex structure.

def complexOfCommuteI (f : E →ₗ[ℝ] F) (hI : ∀ v, f (Complex.I • v)=Complex.I • f v) :
    E →ₗ[ℂ] F where
…

def OAI.Kaplansky.realComplexPart line 72
Source documentation
The canonical projection from real-linear maps to complex-linear maps.
```
def realComplexPart (f : E →ₗ[ℝ] F) : E →ₗ[ℝ] F where
…
```
theorem OAI.Kaplansky.realComplexPart_commute_I line 79
def OAI.Kaplansky.complexPart line 86
theorem OAI.Kaplansky.complexPart_apply line 91
theorem OAI.Kaplansky.complexPart_restrict line 94
def OAI.Kaplansky.complexProjectionLinear line 100
theorem OAI.Kaplansky.complexPart_natural line 108
def OAI.Kaplansky.complexProjection line 121
theorem OAI.Kaplansky.complexProjection_surjective line 124
theorem OAI.Kaplansky.complexProjection_smooth line 127
theorem OAI.Kaplansky.exists_finite_smooth_spanning_sections line 152
Source documentation
A finite family of actual global smooth sections spanning every fiber. The sections are local frame vectors multiplied by a constructed subordinate partition of unity, so no global generation hypothesis is used.
```
theorem exists_finite_smooth_spanning_sections :
    ∃ (n : ℕ) (s : Fin n → ∀ x, E x),
      (∀ i, ContMDiff I (I.prod 𝓘(ℝ,F)) ∞ (fun x => TotalSpace.mk' F x (s i x))) ∧
      ∀ x, Submodule.span ℝ (Set.range (fun i => s i x)) = ⊤ := by
…
```
def OAI.Kaplansky.sectionEvaluation line 213
Source documentation
Evaluation of the complex coefficients of a finite family of sections.
```
def sectionEvaluation (s : Fin n → ∀ x, E x) (x : B) : (Fin n → ℂ) →ₗ[ℂ] E x where
…
```
theorem OAI.Kaplansky.sectionEvaluation_single line 218

theorem OAI.Kaplansky.sectionEvaluation_surjective line 224

Source documentation

Real spanning suffices for surjectivity of the complex-linear evaluation.

theorem sectionEvaluation_surjective [∀ x, Module ℝ (E x)] [∀ x, IsScalarTower ℝ ℂ (E x)]
    (s : Fin n → ∀ x, E x)
    (hs : ∀ x, Submodule.span ℝ (Set.range (fun i => s i x)) = ⊤) (x : B) :
    Function.Surjective (sectionEvaluation s x) := by
…

Mentions: OAI.Kaplansky.sectionEvaluation

def OAI.Kaplansky.sectionEvaluationCoordinates line 251
Source documentation
The evaluation family in an actual bundle frame, with complex parameter space and real-smooth dependence on the base.
```
def sectionEvaluationCoordinates {n : ℕ} (s : Fin n → ∀ x, E x)
    (e : Trivialization F (π F E)) (x : B) : (Fin n → ℂ) →L[ℂ] F :=
…
```
theorem OAI.Kaplansky.sectionEvaluationCoordinates_apply line 257
theorem OAI.Kaplansky.sectionEvaluationCoordinates_smooth line 269
theorem OAI.Kaplansky.sectionEvaluationCoordinates_surjective line 280

theorem OAI.Kaplansky.sectionEvaluation_smooth line 294

Source documentation

Every fixed complex parameter gives an actual global smooth section.

theorem sectionEvaluation_smooth {n : ℕ} (s : Fin n → ∀ x, E x)
    (hs : ∀ i, ContMDiff I (I.prod 𝓘(ℝ,F)) ∞ (fun x => TotalSpace.mk' F x (s i x)))
    (c : Fin n → ℂ) :
    ContMDiff I (I.prod 𝓘(ℝ,F)) ∞ (fun x => TotalSpace.mk' F x (sectionEvaluation s x c)) := by
…

Mentions: OAI.Kaplansky.sectionEvaluation

theorem OAI.Kaplansky.exists_finite_complex_smooth_evaluation line 312

Source documentation

A constructed finite complex parameter space, with surjective evaluation and smooth coordinate maps in every bundle frame.

theorem exists_finite_complex_smooth_evaluation :
    ∃ (n : ℕ) (s : Fin n → ∀ x, E x),
      (∀ i, ContMDiff I (I.prod 𝓘(ℝ,F)) ∞ (fun x => TotalSpace.mk' F x (s i x))) ∧
      (∀ x, Function.Surjective (sectionEvaluation s x)) ∧
      ∀ (e : Trivialization F (π F E)) [MemTrivializationAtlas e],
        ContMDiffOn I 𝓘(ℝ,(Fin n → ℂ) →L[ℂ] F) ∞
          (sectionEvaluationCoordinates E s e) e.baseSet ∧
        ∀ x ∈ e.baseSet, Function.Surjective (sectionEvaluationCoordinates E s e x) := by
…

Mentions: OAI.Kaplansky.sectionEvaluation, OAI.Kaplansky.sectionEvaluationCoordinates

def OAI.Kaplansky.complexHomCoordinates line 350
theorem OAI.Kaplansky.complexHomCoordinates_projected line 357
theorem OAI.Kaplansky.complexHomCoordinates_projected_smooth line 376

theorem OAI.Kaplansky.exists_finite_smooth_complex_hom_generators line 396

Source documentation

Finite global Hom sections are constructed using the ordinary smooth real Hom bundle and the canonical complex-linear projection. Evaluation is surjective onto actual complex-linear fiber maps, and the projected sections are real-smooth in every pair of actual complex bundle frames.

theorem exists_finite_smooth_complex_hom_generators :
    ∃ (n : ℕ) (s : Fin n → ∀ x, E₁ x →L[ℂ] E₂ x),
      (∀ x, Function.Surjective (sectionEvaluation s x)) ∧
      ∀ i (e₁ : Trivialization F₁ (π F₁ E₁)) (e₂ : Trivialization F₂ (π F₂ E₂))
        [MemTrivializationAtlas e₁] [MemTrivializationAtlas e₂],
        ContMDiffOn I 𝓘(ℝ,F₁ →L[ℂ] F₂) ∞ (complexHomCoordinates E₁ E₂ e₁ e₂ (s i))
          (e₁.baseSet ∩ e₂.baseSet) := by
…

Mentions: OAI.Kaplansky.sectionEvaluation, OAI.Kaplansky.complexHomCoordinates

theorem OAI.Kaplansky.realHomCoordinates_restrict line 440

theorem OAI.Kaplansky.smooth_realHom_of_complex_coordinates line 456

Source documentation

Complex frame-coordinate smoothness implies genuine smoothness of the section of the ordinary real Hom bundle. It is not merely a named predicate.

theorem smooth_realHom_of_complex_coordinates
    (s : ∀ x, E₁ x →L[ℂ] E₂ x)
    (hs : ∀ (e₁ : Trivialization F₁ (π F₁ E₁)) (e₂ : Trivialization F₂ (π F₂ E₂))
      [MemTrivializationAtlas e₁] [MemTrivializationAtlas e₂],
      ContMDiffOn I 𝓘(ℝ,F₁ →L[ℂ] F₂) ∞ (complexHomCoordinates E₁ E₂ e₁ e₂ s)
        (e₁.baseSet ∩ e₂.baseSet)) :
    ContMDiff I (I.prod 𝓘(ℝ,F₁ →L[ℝ] F₂)) ∞
      (fun x => TotalSpace.mk' (F₁ →L[ℝ] F₂) x ((s x).restrictScalars ℝ)) := by
…

Mentions: OAI.Kaplansky.complexHomCoordinates

def OAI.Kaplansky.homFrameLinear line 500
theorem OAI.Kaplansky.homFrameLinear_surjective line 510
theorem OAI.Kaplansky.homFrameLinear_commutes line 526
def OAI.Kaplansky.homEvaluationCoordinates line 536
theorem OAI.Kaplansky.homEvaluationCoordinates_apply line 544
theorem OAI.Kaplansky.homEvaluationCoordinates_smooth line 559
theorem OAI.Kaplansky.exists_finite_smooth_hom_evaluation line 572