OAI/Geometry/ComplexBundle/Kernel.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

Smooth splittings, kernel charts, and realization of kernel bundles.

  1. def OAI.Kaplansky.SmoothKernel.localRightInverse line 28

    Source documentation

    Right inverse on the open neighborhood where A R is invertible.

    def localRightInverse (R : W →L[ℂ] V) (A : V →L[ℂ] W) : W →L[ℂ] V :=
…
  2. def OAI.Kaplansky.SmoothKernel.kernelProjection line 31
  3. def OAI.Kaplansky.SmoothKernel.splitDomain line 34
  4. theorem OAI.Kaplansky.SmoothKernel.splitDomain_open line 36
  5. theorem OAI.Kaplansky.SmoothKernel.localRightInverse_right line 40
  6. theorem OAI.Kaplansky.SmoothKernel.localRightInverse_on_range line 44
  7. theorem OAI.Kaplansky.SmoothKernel.kernelProjection_mem line 49
  8. theorem OAI.Kaplansky.SmoothKernel.kernelProjection_fix line 54
  9. theorem OAI.Kaplansky.SmoothKernel.kernelProjection_kill line 59
  10. theorem OAI.Kaplansky.SmoothKernel.kernelProjection_absorb line 64
  11. def OAI.Kaplansky.SmoothKernel.kernelEquiv line 72

    Source documentation

    Explicit linear identification of the actual kernels throughout the split neighborhood. Both maps are restrictions of the constructed projections.

    def kernelEquiv (R : W →L[ℂ] V) (L A : V →L[ℂ] W)
    (hL : L ∈ splitDomain R) (hA : A ∈ splitDomain R) :
    LinearMap.ker L.toLinearMap ≃ₗ[ℂ] LinearMap.ker A.toLinearMap where
…

    Mentions: OAI.Kaplansky.SmoothKernel.splitDomain

  12. theorem OAI.Kaplansky.SmoothKernel.localRightInverse_smooth line 88
  13. theorem OAI.Kaplansky.SmoothKernel.kernelProjection_smooth line 96
  14. theorem OAI.Kaplansky.SmoothKernel.kernelProjection_apply_smooth line 100
  15. def OAI.Kaplansky.SmoothKernel.kernelRetraction line 110
  16. abbrev OAI.Kaplansky.SmoothKernel.SplitBase line 114
  17. abbrev OAI.Kaplansky.SmoothKernel.SplitIncidence line 117

    Source documentation

    The actual incidence subset, with the topology induced from parameters and V.

    abbrev SplitIncidence (R : W →L[ℂ] V) := {p : SplitBase R × V // p.1.val p.2=0}

    Mentions: OAI.Kaplansky.SmoothKernel.SplitBase

  18. def OAI.Kaplansky.SmoothKernel.kernelChartHomeomorph line 121

    Source documentation

    A homeomorphism over the parameter base between the actual local kernel incidence space and the product with one fixed kernel.

    def kernelChartHomeomorph (R : W →L[ℂ] V) (L : V →L[ℂ] W) (hL : L ∈ splitDomain R) :
    SplitIncidence R ≃ₜ SplitBase R × LinearMap.ker L.toLinearMap where
…

    Mentions: OAI.Kaplansky.SmoothKernel.splitDomain, OAI.Kaplansky.SmoothKernel.SplitIncidence, OAI.Kaplansky.SmoothKernel.SplitBase

  19. def OAI.Kaplansky.SmoothKernel.kernelCoordinateChange line 151

    Source documentation

    The fiber coordinate transition really is projection onto the second fixed kernel after reconstruction in the varying kernel.

    def kernelCoordinateChange (R R' : W →L[ℂ] V) (L L' : V →L[ℂ] W)
    (hL' : L' ∈ splitDomain R') (A : V →L[ℂ] W) :
    LinearMap.ker L.toLinearMap →L[ℂ] LinearMap.ker L'.toLinearMap :=
…

    Mentions: OAI.Kaplansky.SmoothKernel.splitDomain

  20. theorem OAI.Kaplansky.SmoothKernel.kernelCoordinateChange_smooth line 157
  21. theorem OAI.Kaplansky.SmoothKernel.kernelCoordinateChange_smooth_real line 162
  22. abbrev OAI.Kaplansky.SmoothKernel.KernelModel line 176
  23. structure OAI.Kaplansky.SmoothKernel.SurjectiveFamily line 182

    Source documentation

    Ordinary continuous, surjective linear families. No kernel bundle is part of the input: the following construction supplies it.

    structure SurjectiveFamily (B V W : Type*) [TopologicalSpace B]
    [NormedAddCommGroup V] [NormedSpace ℂ V]
    [NormedAddCommGroup W] [NormedSpace ℂ W] where
…
  24. def OAI.Kaplansky.SmoothKernel.SurjectiveFamily.rightInverse line 194
  25. theorem OAI.Kaplansky.SmoothKernel.SurjectiveFamily.rightInverse_spec line 199
  26. theorem OAI.Kaplansky.SmoothKernel.SurjectiveFamily.center_mem line 207
  27. theorem OAI.Kaplansky.SmoothKernel.SurjectiveFamily.kernel_finrank line 213
  28. def OAI.Kaplansky.SmoothKernel.SurjectiveFamily.modelEquiv line 219
  29. def OAI.Kaplansky.SmoothKernel.SurjectiveFamily.baseSet line 224
  30. theorem OAI.Kaplansky.SmoothKernel.SurjectiveFamily.baseSet_open line 227
  31. def OAI.Kaplansky.SmoothKernel.SurjectiveFamily.toModel line 230
  32. def OAI.Kaplansky.SmoothKernel.SurjectiveFamily.fromModel line 234
  33. theorem OAI.Kaplansky.SmoothKernel.SurjectiveFamily.fromModel_mem line 238
  34. theorem OAI.Kaplansky.SmoothKernel.SurjectiveFamily.toModel_fromModel line 242
  35. theorem OAI.Kaplansky.SmoothKernel.SurjectiveFamily.fromModel_toModel line 257
  36. def OAI.Kaplansky.SmoothKernel.SurjectiveFamily.transition line 265
  37. theorem OAI.Kaplansky.SmoothKernel.SurjectiveFamily.transition_self line 268
  38. theorem OAI.Kaplansky.SmoothKernel.SurjectiveFamily.transition_comp line 271
  39. theorem OAI.Kaplansky.SmoothKernel.SurjectiveFamily.continuousOn_fromModel line 278
  40. def OAI.Kaplansky.SmoothKernel.SurjectiveFamily.core line 285

    Source documentation

    The kernel bundle core has the actual rank dim(V)-dim(W), with local transitions constructed from the family and its right inverses.

    def core : VectorBundleCore ℂ B (KernelModel V W) B where
…

    Mentions: OAI.Kaplansky.SmoothKernel.KernelModel

  41. def OAI.Kaplansky.SmoothKernel.SurjectiveFamily.fiberEquiv line 298

    Source documentation

    Every constructed fiber is linearly identified with the actual kernel.

    def fiberEquiv (b : B) : A.core.Fiber b ≃ₗ[ℂ] LinearMap.ker (A.map b).toLinearMap :=
…
  42. def OAI.Kaplansky.SmoothKernel.SurjectiveFamily.realCore line 313
  43. instance OAI.Kaplansky.SmoothKernel.SurjectiveFamily.realFiberComplexModule line 326
  44. def OAI.Kaplansky.SmoothKernel.SurjectiveFamily.realFiberEquiv line 329
  45. theorem OAI.Kaplansky.SmoothKernel.SurjectiveFamily.kernel_model_real_finrank line 333
  46. theorem OAI.Kaplansky.SmoothKernel.SurjectiveFamily.transition_contDiffAt line 341
  47. theorem OAI.Kaplansky.SmoothKernel.SurjectiveFamily.realCore_isContMDiff line 353

    Source documentation

    A genuinely smooth kernel bundle, derived from smoothness and surjectivity of the original family. Smoothness of the kernel bundle is not an assumption.

    theorem realCore_isContMDiff (hD : ContDiff ℝ ∞ D.map) :
    D.realCore.IsContMDiff 𝓘(ℝ,X) ∞ where
…
  48. theorem OAI.Kaplansky.SmoothKernel.SurjectiveFamily.fromModel_center line 373
  49. abbrev OAI.Kaplansky.SmoothKernel.SurjectiveFamily.IncidenceTotal line 377
  50. def OAI.Kaplansky.SmoothKernel.SurjectiveFamily.realization line 379
  51. theorem OAI.Kaplansky.SmoothKernel.SurjectiveFamily.realization_chart line 382
  52. theorem OAI.Kaplansky.SmoothKernel.SurjectiveFamily.continuous_realization line 388
  53. def OAI.Kaplansky.SmoothKernel.SurjectiveFamily.toIncidence line 403
  54. def OAI.Kaplansky.SmoothKernel.SurjectiveFamily.fromIncidence line 406
  55. theorem OAI.Kaplansky.SmoothKernel.SurjectiveFamily.fromIncidence_chart line 409
  56. theorem OAI.Kaplansky.SmoothKernel.SurjectiveFamily.continuous_fromIncidence line 415
  57. def OAI.Kaplansky.SmoothKernel.SurjectiveFamily.incidenceHomeomorph line 428

    Source documentation

    The constructed smooth real bundle realizes the exact complex kernel incidence subset, including its ambient subspace topology.

    def incidenceHomeomorph : TotalSpace (KernelModel V W) A.realCore.Fiber ≃ₜ A.IncidenceTotal where
…

    Mentions: OAI.Kaplansky.SmoothKernel.KernelModel