OAI/Geometry/ComplexBundle/SmoothLine.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Smooth projective lines, product lines, finite sums, and restrictions.

  1. theorem OAI.Kaplansky.ComplexGrassmann.contDiff_graphLineVector line 18
  2. theorem OAI.Kaplansky.ComplexGrassmann.contDiff_vectorOuter line 25
  3. theorem OAI.Kaplansky.ComplexGrassmann.contDiff_graphLineProjection_val line 36
  4. theorem OAI.Kaplansky.ComplexGrassmann.contMDiff_projectiveProjection_matrix line 48

    Source documentation

    The actual projector matrix of a line is a smooth function on complex projective space, viewed as a real manifold.

    theorem contMDiff_projectiveProjection_matrix :
    ContMDiff ๐“˜(โ„,GraphSlope 1 k) ๐“˜(โ„,Matrix (Fin (1+k)) (Fin (1+k)) โ„‚) โˆž
      (fun P : Grassmann 1 k => ((projectiveProjectionEquiv k).symm P).val) := by
โ€ฆ

    Mentions: OAI.Kaplansky.ComplexGrassmann.GraphSlope, OAI.Kaplansky.ComplexGrassmann.Grassmann, OAI.Kaplansky.ComplexGrassmann.projectiveProjectionEquiv

  5. def OAI.Kaplansky.ComplexGrassmann.projectiveProjectionMap line 74
  6. def OAI.Kaplansky.ComplexGrassmann.projectiveHyperplaneCore line 77
  7. def OAI.Kaplansky.ComplexGrassmann.matrixColumnLinear line 80
  8. theorem OAI.Kaplansky.ComplexGrassmann.contMDiff_projectiveColumn line 86
  9. theorem OAI.Kaplansky.ComplexGrassmann.contDiffAt_normalize line 93
  10. theorem OAI.Kaplansky.ComplexGrassmann.contMDiffOn_projectiveUnitColumn line 97
  11. theorem OAI.Kaplansky.ComplexGrassmann.projectiveHyperplaneCore_transition_smooth line 105

    Source documentation

    The actual dual tautological-line transitions are real smooth.

    theorem projectiveHyperplaneCore_transition_smooth (a b : Fin (1+k)) :
    ContMDiffOn ๐“˜(โ„,GraphSlope 1 k) ๐“˜(โ„,โ„‚ โ†’L[โ„‚] โ„‚) โˆž
      ((projectiveHyperplaneCore k).coordChange a b)
      ((projectiveHyperplaneCore k).baseSet a โˆฉ (projectiveHyperplaneCore k).baseSet b) := by
โ€ฆ

    Mentions: OAI.Kaplansky.ComplexGrassmann.GraphSlope, OAI.Kaplansky.ComplexGrassmann.projectiveHyperplaneCore

  12. def OAI.Kaplansky.ComplexGrassmann.productLineChartIndex line 130
  13. def OAI.Kaplansky.ComplexGrassmann.productLineCore line 135

    Source documentation

    Lโ‚€ is trivial; Lแตข is the actual hyperplane line pulled back from factor i.

    def productLineCore (i : Option ฮน) :
    VectorBundleCore โ„‚ (ProjectiveProduct K) โ„‚ (productLineChartIndex K i) :=
โ€ฆ

    Mentions: OAI.Kaplansky.ComplexGrassmann.ProjectiveProduct, OAI.Kaplansky.ComplexGrassmann.productLineChartIndex

  14. theorem OAI.Kaplansky.ComplexGrassmann.productLineCore_transition_smooth line 141
  15. theorem OAI.Kaplansky.ComplexGrassmann.productLineCore_unitary line 153
  16. instance OAI.Kaplansky.ComplexGrassmann.productLineCore_contMDiffVectorBundle line 166
  17. def OAI.Kaplansky.ComplexGrassmann.smoothLineSumCore line 176

    Source documentation

    The ordinary smooth Hermitian direct sum of the specified hyperplane pullbacks and trivial lines on the actual projective product.

    def smoothLineSumCore := finiteLineSumCore (fun s => productLineCore K (label s))

    Mentions: OAI.Kaplansky.finiteLineSumCore, OAI.Kaplansky.ComplexGrassmann.productLineCore

  18. abbrev OAI.Kaplansky.ComplexGrassmann.SmoothLineSumBundle line 177
  19. instance OAI.Kaplansky.ComplexGrassmann.smoothLineSum_norm line 179
  20. instance OAI.Kaplansky.ComplexGrassmann.smoothLineSum_inner line 181
  21. instance OAI.Kaplansky.ComplexGrassmann.smoothLineSum_contMDiffVectorBundle line 184
  22. theorem OAI.Kaplansky.ComplexGrassmann.smoothLineSum_finrank line 191
  23. theorem OAI.Kaplansky.ComplexGrassmann.smoothLineSum_inner_continuousOn line 197
  24. def OAI.Kaplansky.ComplexGrassmann.projectiveRestrict line 213
  25. theorem OAI.Kaplansky.ComplexGrassmann.continuous_productLine_restrict_iff line 219

    Source documentation

    Restricting the base preserves the actual local line coordinates, for both the trivial line and every hyperplane pullback.

    theorem continuous_productLine_restrict_iff (i : Option ฮน)
    (g : X โ†’ ProjectiveProduct K) (v : X โ†’ โ„‚) (hg : Continuous g) :
    Continuous (fun x => TotalSpace.mk' โ„‚ (E := (productLineCore K (i.map f)).Fiber) (g x) (v x)) โ†”
โ€ฆ

    Mentions: OAI.Kaplansky.ComplexGrassmann.ProjectiveProduct, OAI.Kaplansky.ComplexGrassmann.productLineCore

  26. theorem OAI.Kaplansky.ComplexGrassmann.continuous_lineSum_restrict_iff line 245

    Source documentation

    The finite orthogonal sum has the ordinary pullback topology under coordinate restriction. The base and fiber coordinates are explicit.

    theorem continuous_lineSum_restrict_iff {S : Type*} [Fintype S]
    (label : S โ†’ Option ฮน) (g : X โ†’ ProjectiveProduct K)
    (v : X โ†’ EuclideanSpace โ„‚ S) (hg : Continuous g) :
    Continuous (fun x => TotalSpace.mk' (EuclideanSpace โ„‚ S)
      (E := SmoothLineSumBundle K (fun s => (label s).map f)) (g x) (v x)) โ†”
โ€ฆ

    Mentions: OAI.Kaplansky.ComplexGrassmann.ProjectiveProduct, OAI.Kaplansky.ComplexGrassmann.SmoothLineSumBundle