Complement.lean`

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Local and global topology and splitting of frame complement bundles.

theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.analysis_ker line 21
Source documentation
The complement is the kernel of the actual frame coefficient map.
```
theorem analysis_ker (y : ProjectiveProduct K) :
    LinearMap.ker (frameAnalysis (f.vector y)) =
      (Submodule.span ℂ (Set.range (f.vector y)))ᗮ := by
…
```
Mentions: OAI.Kaplansky.frameAnalysis
theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.analysis_surjective line 44
theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.analysis_kernel_finrank line 49
Source documentation
The actual kernel has constant rank, with no complement-bundle premise.
```
theorem analysis_kernel_finrank (y : ProjectiveProduct K) :
    Module.finrank ℂ (LinearMap.ker (frameAnalysis (f.vector y))) = Fintype.card a.Slot-d := by
…
```
Mentions: OAI.Kaplansky.frameAnalysis
def OAI.Kaplansky.ContinuousOrthonormalStageFrame.localAnalysis line 63
Source documentation
The coefficient map in an ambient chart.
```
def localAnalysis (y : e.baseSet) : a.Model →L[ℂ] EuclideanSpace ℂ (Fin d) :=
…
```
theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.continuous_localAnalysis line 66
theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.localAnalysis_surjective line 77
def OAI.Kaplansky.ContinuousOrthonormalStageFrame.localKernelFamily line 86
Source documentation
A continuous surjective family on every ambient chart, constructed from an arbitrary continuous orthonormal frame.
```
def localKernelFamily : SmoothKernel.SurjectiveFamily e.baseSet a.Model (EuclideanSpace ℂ (Fin d)) where
…
```
Mentions: OAI.Kaplansky.SmoothKernel.SurjectiveFamily
abbrev OAI.Kaplansky.ContinuousOrthonormalStageFrame.ComplementTotal line 98
Source documentation
The actual complement, with the ambient bundle's subspace topology.
```
abbrev ComplementTotal := {z : TotalSpace a.Model a.Fiber //
…
```
abbrev OAI.Kaplansky.ContinuousOrthonormalStageFrame.LocalComplementTotal line 102
def OAI.Kaplansky.ContinuousOrthonormalStageFrame.complementToLocalKernel line 104
def OAI.Kaplansky.ContinuousOrthonormalStageFrame.localKernelToComplement line 113
theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.continuous_complementToLocalKernel line 119
theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.continuous_localKernelToComplement line 130
def OAI.Kaplansky.ContinuousOrthonormalStageFrame.localComplementKernelHomeomorph line 145
Source documentation
A homeomorphism to the genuine kernel incidence set over an ambient chart. Both spaces retain their ambient subspace topologies.
```
def localComplementKernelHomeomorph : f.LocalComplementTotal e ≃ₜ
    (f.localKernelFamily e).IncidenceTotal where
…
```
def OAI.Kaplansky.ContinuousOrthonormalStageFrame.localComplementBundleHomeomorph line 164
Source documentation
The local ordinary kernel bundle realizes the exact orthogonal complement, not an independently assigned topology on the same fibers.
```
def localComplementBundleHomeomorph :
    TotalSpace (SmoothKernel.KernelModel a.Model (EuclideanSpace ℂ (Fin d)))
      (f.localKernelFamily e).realCore.Fiber ≃ₜ f.LocalComplementTotal e :=
…
```
Mentions: OAI.Kaplansky.SmoothKernel.KernelModel
abbrev OAI.Kaplansky.ContinuousOrthonormalStageFrame.ComplementModel line 175
abbrev OAI.Kaplansky.ContinuousOrthonormalStageFrame.ComplementFiber line 176
def OAI.Kaplansky.ContinuousOrthonormalStageFrame.complementTotalEquiv line 179
instance OAI.Kaplansky.ContinuousOrthonormalStageFrame.complementTotalTopology line 185
def OAI.Kaplansky.ContinuousOrthonormalStageFrame.complementTotalHomeomorph line 188
def OAI.Kaplansky.ContinuousOrthonormalStageFrame.complementInclusion line 191
theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.complementInclusion_isInducing line 194
theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.complement_totalSpaceMk_isInducing line 197
def OAI.Kaplansky.ContinuousOrthonormalStageFrame.complementLocalTriv line 211
theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.complementLocalTriv_apply line 216
def OAI.Kaplansky.ContinuousOrthonormalStageFrame.complementAmbientTriv line 223
Source documentation
Extend the locally constructed kernel chart over its open base into the actual global complement total space.
```
def complementAmbientTriv (i : e.baseSet) : Trivialization f.ComplementModel
    (fun z : f.ComplementTotal => z.val.proj) :=
…
```
def OAI.Kaplansky.ContinuousOrthonormalStageFrame.complementTriv line 229
theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.complementTriv_baseSet line 233
theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.complementTriv_apply line 236
instance OAI.Kaplansky.ContinuousOrthonormalStageFrame.complementTriv_isLinear line 250
def OAI.Kaplansky.ContinuousOrthonormalStageFrame.complementTrivializationAt line 268
theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.mem_complementTrivializationAt line 273
instance OAI.Kaplansky.ContinuousOrthonormalStageFrame.complementFiberBundle line 278
instance OAI.Kaplansky.ContinuousOrthonormalStageFrame.complementTrivializationAt_isLinear line 285
theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.continuousOn_complement_coordChange line 290
instance OAI.Kaplansky.ContinuousOrthonormalStageFrame.complementVectorBundle line 306
Source documentation
The full orthogonal complement is an ordinary complex vector bundle, with charts constructed from the frame and the inherited ambient topology.
```
instance complementVectorBundle : VectorBundle ℂ f.ComplementModel f.ComplementFiber where
…
```
theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.complementBundle_rank line 314
theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.analysis_complement line 332
theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.projection_synthesis line 338
def OAI.Kaplansky.ContinuousOrthonormalStageFrame.complementSplitLinearEquiv line 345
Source documentation
The actual fiber decomposition into the full orthogonal complement and the trivial frame summand. No alignment with the original line summands.
```
def complementSplitLinearEquiv (y : ProjectiveProduct K) :
    (f.ComplementFiber y × EuclideanSpace ℂ (Fin d)) ≃ₗ[ℂ] a.Fiber y where
…
```
abbrev OAI.Kaplansky.ContinuousOrthonormalStageFrame.ComplementSplitTotal line 371
def OAI.Kaplansky.ContinuousOrthonormalStageFrame.complementAssemble line 374
def OAI.Kaplansky.ContinuousOrthonormalStageFrame.complementDisassemble line 377
theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.continuous_complementAssemble line 381
theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.continuous_complementDisassemble line 403
def OAI.Kaplansky.ContinuousOrthonormalStageFrame.complementSplitHomeomorph line 412
Source documentation
Global topological splitting of the actual bundle. The first factor is the constructed complement vector bundle and the other factor is trivial.
```
def complementSplitHomeomorph : f.ComplementSplitTotal ≃ₜ TotalSpace a.Model a.Fiber where
…
```
theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.complementSplitHomeomorph_base line 427