Hyperplane.lean`

46 declarations, 0 contain sorry, 0 declared as axioms

Hyperplane sections, dual evaluation, graph coordinates, and their zero.

def OAI.Kaplansky.hyperplaneFunctionalSection line 19
Source documentation
Restrict an ambient linear functional to each actual tautological line, viewed as a section of its dual, the hyperplane bundle.
```
def hyperplaneFunctionalSection (L : EuclideanSpace ℂ (Fin d) →ₗ[ℂ] ℂ)
    (p : projectionSpace d 1) : (projectionDualLineCore d).Fiber p :=
…
```
Mentions: OAI.Kaplansky.projectionSpace, OAI.Kaplansky.projectionDualLineCore
theorem OAI.Kaplansky.hyperplaneFunctionalSection_chart line 23
theorem OAI.Kaplansky.continuous_hyperplaneFunctionalSection line 38
theorem OAI.Kaplansky.hyperplaneFunctionalSection_realization line 53
Source documentation
The section's actual dual-line realization is exactly restriction of L.
```
theorem hyperplaneFunctionalSection_realization (L : EuclideanSpace ℂ (Fin d) →ₗ[ℂ] ℂ)
    (p : projectionSpace d 1) (v : projectionLine p) :
    projectionDualLineFiberEquiv p (hyperplaneFunctionalSection L p) v = L v.val := by
…
```
Mentions: OAI.Kaplansky.projectionSpace, OAI.Kaplansky.projectionLine, OAI.Kaplansky.projectionDualLineFiberEquiv, OAI.Kaplansky.hyperplaneFunctionalSection
theorem OAI.Kaplansky.hyperplaneFunctionalSection_eq_zero_iff line 62
def OAI.Kaplansky.coordinateFunctional line 73
theorem OAI.Kaplansky.coordinateFunctional_apply line 76
def OAI.Kaplansky.positiveCoordinate line 87
def OAI.Kaplansky.firstCoordinateVector line 89
theorem OAI.Kaplansky.firstCoordinateVector_ne_zero line 92
def OAI.Kaplansky.firstCoordinateProjection line 97
theorem OAI.Kaplansky.firstCoordinateProjection_line line 100
theorem OAI.Kaplansky.vector_eq_firstCoordinate_of_positive_zero line 104
theorem OAI.Kaplansky.hyperplaneCoordinateSections_common_zero line 123
Source documentation
The K coordinate sections of O(1) on CP^K have exactly one common zero, the first coordinate line. This is an actual zero-set statement, not yet an identification or nonvanishing theorem for the top Chern class.
```
theorem hyperplaneCoordinateSections_common_zero {k : ℕ} (p : projectionSpace (1+k) 1) :
    (∀ i : Fin k, hyperplaneFunctionalSection (coordinateFunctional (positiveCoordinate k i)) p=0) ↔
      p=firstCoordinateProjection k := by
…
```
Mentions: OAI.Kaplansky.projectionSpace, OAI.Kaplansky.hyperplaneFunctionalSection, OAI.Kaplansky.coordinateFunctional, OAI.Kaplansky.positiveCoordinate, OAI.Kaplansky.firstCoordinateProjection
def OAI.Kaplansky.hyperplaneEvaluationEquiv line 157
Source documentation
Evaluation at any nonzero vector is a genuine coordinate on the dual of its one-dimensional line.
```
def hyperplaneEvaluationEquiv (p : projectionSpace d 1) (v : projectionLine p) (hv : v≠0) :
    (projectionDualLineCore d).Fiber p ≃ₗ[ℂ] ℂ := by
…
```
Mentions: OAI.Kaplansky.projectionSpace, OAI.Kaplansky.projectionLine, OAI.Kaplansky.projectionDualLineCore
theorem OAI.Kaplansky.hyperplaneEvaluationEquiv_apply line 172
theorem OAI.Kaplansky.hyperplaneEvaluation_chart line 178
Source documentation
In every chart the actual pairing is chart coefficient times the coordinate of v in the unit local line frame.
```
theorem hyperplaneEvaluation_chart (p : projectionSpace d 1) (v : projectionLine p)
    (z : (projectionDualLineCore d).Fiber p) (i : Fin d) (hi : p ∈ projectionChartSet i) :
    projectionDualLineFiberEquiv p z v =
      ((projectionDualLineCore d).localTriv i ⟨p,z⟩).2 * inner ℂ (unitProjectionColumn p i) v.val := by
…
```
Mentions: OAI.Kaplansky.projectionSpace, OAI.Kaplansky.projectionLine, OAI.Kaplansky.projectionDualLineCore, OAI.Kaplansky.projectionChartSet, OAI.Kaplansky.projectionDualLineFiberEquiv, OAI.Kaplansky.unitProjectionColumn

theorem OAI.Kaplansky.continuous_hyperplaneEvaluation line 196

Source documentation

Pairing is continuous for actual continuously varying dual fibers and line vectors. The line-membership premise only identifies its genuine domain.

theorem continuous_hyperplaneEvaluation {X : Type*} [TopologicalSpace X]
    (p : X → projectionSpace d 1) (hp : Continuous p)
    (v : X → EuclideanSpace ℂ (Fin d)) (hvm : ∀ x, v x ∈ projectionLine (p x))
    (hv : Continuous v) (z : ∀ x, (projectionDualLineCore d).Fiber (p x))
    (hz : Continuous (fun x => TotalSpace.mk' ℂ (p x) (z x))) :
    Continuous (fun x => projectionDualLineFiberEquiv (p x) (z x) ⟨v x,hvm x⟩) := by
…

Mentions: OAI.Kaplansky.projectionSpace, OAI.Kaplansky.projectionLine, OAI.Kaplansky.projectionDualLineCore, OAI.Kaplansky.projectionDualLineFiberEquiv

abbrev OAI.Kaplansky.evaluationPullbackCore line 225
def OAI.Kaplansky.pullbackEvaluationEquiv line 227
theorem OAI.Kaplansky.evaluation_inner_ne_zero line 231
theorem OAI.Kaplansky.pullbackEvaluation_inverse_chart line 238
theorem OAI.Kaplansky.continuous_evaluationPullback_toOriginal line 250
def OAI.Kaplansky.hyperplaneEvaluationHomeomorph line 264
Source documentation
Evaluation at a nonvanishing continuous line vector trivializes the actual pullback hyperplane bundle, with its ordinary bundle topology.
```
def hyperplaneEvaluationHomeomorph : TotalSpace ℂ (evaluationPullbackCore p).Fiber ≃ₜ X × ℂ where
…
```
Mentions: OAI.Kaplansky.evaluationPullbackCore
theorem OAI.Kaplansky.hyperplaneEvaluationHomeomorph_base line 294
def OAI.Kaplansky.ComplexGrassmann.graphVerticalFunctional line 307
theorem OAI.Kaplansky.ComplexGrassmann.graphVerticalFunctional_vector line 312
def OAI.Kaplansky.ComplexGrassmann.graphHyperplaneBase line 317
theorem OAI.Kaplansky.ComplexGrassmann.graphLineVector_mem line 320
def OAI.Kaplansky.ComplexGrassmann.graphHyperplaneTrivialization line 327
Source documentation
Genuine bundle coordinates obtained by evaluating a dual-line vector on the nonvanishing graph representative.
```
def graphHyperplaneTrivialization (F : GraphFrame 1 k) :
    TotalSpace ℂ (evaluationPullbackCore (graphHyperplaneBase F)).Fiber ≃ₜ GraphSlope 1 k × ℂ :=
…
```
Mentions: OAI.Kaplansky.ComplexGrassmann.GraphFrame, OAI.Kaplansky.evaluationPullbackCore, OAI.Kaplansky.ComplexGrassmann.graphHyperplaneBase, OAI.Kaplansky.ComplexGrassmann.GraphSlope
def OAI.Kaplansky.ComplexGrassmann.graphHyperplaneSectionCoordinates line 334
Source documentation
The actual K hyperplane sections, expressed in the genuine evaluation trivialization over a projective graph chart.
```
def graphHyperplaneSectionCoordinates (F : GraphFrame 1 k) (A : GraphSlope 1 k) : GraphVertical k :=
…
```
Mentions: OAI.Kaplansky.ComplexGrassmann.GraphFrame, OAI.Kaplansky.ComplexGrassmann.GraphSlope, OAI.Kaplansky.ComplexGrassmann.GraphVertical
theorem OAI.Kaplansky.ComplexGrassmann.graphHyperplaneSectionCoordinates_eq line 338
def OAI.Kaplansky.ComplexGrassmann.slopeEvaluationOneEquiv line 346
theorem OAI.Kaplansky.ComplexGrassmann.graphHyperplaneSectionCoordinates_hasFDerivAt line 367
Source documentation
In these actual local bundle coordinates, the derivative at the sole zero is a complex-linear isomorphism. This supplies regular-zero data; its Euler/Chern interpretation remains a separate topological theorem.
```
theorem graphHyperplaneSectionCoordinates_hasFDerivAt (F : GraphFrame 1 k) (A : GraphSlope 1 k) :
    HasFDerivAt (graphHyperplaneSectionCoordinates F)
      (slopeEvaluationOneEquiv k).toContinuousLinearMap A := by
…
```
Mentions: OAI.Kaplansky.ComplexGrassmann.GraphFrame, OAI.Kaplansky.ComplexGrassmann.GraphSlope, OAI.Kaplansky.ComplexGrassmann.graphHyperplaneSectionCoordinates, OAI.Kaplansky.ComplexGrassmann.slopeEvaluationOneEquiv
theorem OAI.Kaplansky.ComplexGrassmann.graphHyperplaneSectionCoordinates_zero_iff line 375
def OAI.Kaplansky.finiteLineEvaluationEquiv line 389
def OAI.Kaplansky.finiteLineEvaluationHomeomorph line 396
Source documentation
Simultaneous evaluation trivializes the actual finite sum of dual lines, with the original finite-sum topology and linear fibers.
```
def finiteLineEvaluationHomeomorph :
    TotalSpace (EuclideanSpace ℂ S)
      (finiteLineSumCore (fun s => evaluationPullbackCore (p s))).Fiber ≃ₜ A × (S → ℂ) where
…
```
Mentions: OAI.Kaplansky.finiteLineSumCore, OAI.Kaplansky.evaluationPullbackCore
theorem OAI.Kaplansky.finiteLineEvaluationHomeomorph_base line 418
theorem OAI.Kaplansky.finiteLineEvaluationHomeomorph_zero_iff line 422
def OAI.Kaplansky.ComplexGrassmann.standardLineGraphFrame line 434
theorem OAI.Kaplansky.ComplexGrassmann.standardLineGraphFrame_vertical line 438
theorem OAI.Kaplansky.ComplexGrassmann.standardLineGraphFrame_horizontal line 445
theorem OAI.Kaplansky.ComplexGrassmann.standard_verticalFunctional line 451
theorem OAI.Kaplansky.ComplexGrassmann.standard_graphVector_zero line 457
theorem OAI.Kaplansky.ComplexGrassmann.standard_graphProjection_zero line 474
Source documentation
The graph-chart origin is exactly the unique zero previously identified in the canonical coordinate sections of the actual hyperplane bundle.
```
theorem standard_graphProjection_zero (k : ℕ) :
    graphLineProjection (standardLineGraphFrame k) 0=firstCoordinateProjection k := by
…
```
Mentions: OAI.Kaplansky.ComplexGrassmann.graphLineProjection, OAI.Kaplansky.ComplexGrassmann.standardLineGraphFrame, OAI.Kaplansky.firstCoordinateProjection
theorem OAI.Kaplansky.ComplexGrassmann.canonical_hyperplaneSections_regular line 481
Source documentation
The canonical sections used in the global zero-set theorem, expressed in a genuine bundle trivialization, have an invertible complex derivative.
```
theorem canonical_hyperplaneSections_regular (k : ℕ) :
    HasFDerivAt (fun A : GraphSlope 1 k => fun i : Fin k =>
      (graphHyperplaneTrivialization (standardLineGraphFrame k)
        ⟨A,hyperplaneFunctionalSection (coordinateFunctional (positiveCoordinate k i))
          (graphLineProjection (standardLineGraphFrame k) A)⟩).2)
      (slopeEvaluationOneEquiv k).toContinuousLinearMap 0 ∧
      Function.Bijective (slopeEvaluationOneEquiv k) := by
…
```
Mentions: OAI.Kaplansky.ComplexGrassmann.GraphSlope, OAI.Kaplansky.ComplexGrassmann.graphHyperplaneTrivialization, OAI.Kaplansky.ComplexGrassmann.standardLineGraphFrame, OAI.Kaplansky.hyperplaneFunctionalSection, OAI.Kaplansky.coordinateFunctional, OAI.Kaplansky.positiveCoordinate, OAI.Kaplansky.ComplexGrassmann.graphLineProjection, OAI.Kaplansky.ComplexGrassmann.slopeEvaluationOneEquiv