Incidence.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

Linear incidence equations and their graph-coordinate kernel bundles.

def OAI.Kaplansky.Incidence.restrictQuotient line 16
theorem OAI.Kaplansky.Incidence.restrictQuotient_surjective line 22

def OAI.Kaplansky.Incidence.tupleRestriction line 35

Source documentation

The q-fold evaluation/restriction/quotient map used by the incidence locus.

def tupleRestriction {q : ℕ} (S : Submodule ℂ E) (U : Submodule ℂ F)
    (ev : V →ₗ[ℂ] (Fin q → E →ₗ[ℂ] F)) :
    V →ₗ[ℂ] (Fin q → S →ₗ[ℂ] F ⧸ U) where
…

theorem OAI.Kaplansky.Incidence.tupleRestriction_surjective line 42
theorem OAI.Kaplansky.Incidence.mem_tupleRestriction_ker line 53
theorem OAI.Kaplansky.Incidence.incidence_target_finrank line 70

theorem OAI.Kaplansky.Incidence.incidence_kernel_finrank line 78

Source documentation

Exact rank-nullity for the actual incidence fiber in the parameter space V.

theorem incidence_kernel_finrank [FiniteDimensional ℂ V] {q : ℕ}
    (S : Submodule ℂ E) (U : Submodule ℂ F)
    (ev : V →ₗ[ℂ] (Fin q → E →ₗ[ℂ] F)) (hev : Function.Surjective ev) :
    finrank ℂ (LinearMap.ker (tupleRestriction S U ev))=
      finrank ℂ V-q * finrank ℂ S * (finrank ℂ F-finrank ℂ U) := by
…

Mentions: OAI.Kaplansky.Incidence.tupleRestriction

theorem OAI.Kaplansky.Incidence.incidence_kernel_real_finrank line 88
def OAI.Kaplansky.Incidence.graphQuotient line 106
Source documentation
The quotient coordinate of a graph t-plane, (u,v) ↦ v-bu.
```
def graphQuotient (b : GraphSlope t l) : GraphAmbient t l →L[ℂ] GraphVertical l :=
…
```
theorem OAI.Kaplansky.Incidence.graphQuotient_apply line 109
theorem OAI.Kaplansky.Incidence.graphQuotient_zero_iff line 112
theorem OAI.Kaplansky.Incidence.graphQuotient_surjective line 115
def OAI.Kaplansky.Incidence.graphRestriction line 119
theorem OAI.Kaplansky.Incidence.graphRestriction_apply line 127
theorem OAI.Kaplansky.Incidence.graphRestriction_zero_iff line 134
Source documentation
The zero equation for these smooth coordinates is exactly preservation of S into U, with S and U the actual graph subspaces.
```
theorem graphRestriction_zero_iff (a : GraphSlope s k) (b : GraphSlope t l)
    (T : GraphAmbient s k →L[ℂ] GraphAmbient t l) :
    graphRestriction a b T=0 ↔ ∀ v ∈ a.toLinearMap.graph, T v ∈ b.toLinearMap.graph := by
…
```
Mentions: OAI.Kaplansky.Incidence.graphRestriction
theorem OAI.Kaplansky.Incidence.graphRestriction_surjective line 152
Source documentation
A concrete right inverse: place the requested quotient map in the lower left block and set all other blocks to zero.
```
theorem graphRestriction_surjective (a : GraphSlope s k) (b : GraphSlope t l) :
    Function.Surjective (graphRestriction a b) := by
…
```
Mentions: OAI.Kaplansky.Incidence.graphRestriction
theorem OAI.Kaplansky.Incidence.graphQuotient_smooth line 160
theorem OAI.Kaplansky.Incidence.graphInclusion_smooth line 163
theorem OAI.Kaplansky.Incidence.graphRestriction_smooth line 166
theorem OAI.Kaplansky.Incidence.graphRestriction_smooth_real line 177
abbrev OAI.Kaplansky.Incidence.TupleAmbient line 190
abbrev OAI.Kaplansky.Incidence.TupleTarget line 192
def OAI.Kaplansky.Incidence.tupleGraphRestriction line 194
theorem OAI.Kaplansky.Incidence.tupleGraphRestriction_surjective line 198
theorem OAI.Kaplansky.Incidence.tupleGraphRestriction_smooth line 204
theorem OAI.Kaplansky.Incidence.tupleTarget_finrank line 212
def OAI.Kaplansky.Incidence.graphEvaluation line 222
Source documentation
The actual linear family whose zero set is the local incidence locus.
```
def graphEvaluation (p : Y × (GraphSlope s k × GraphSlope t l)) : V →L[ℂ] TupleTarget q s l :=
…
```
Mentions: OAI.Kaplansky.Incidence.TupleTarget
theorem OAI.Kaplansky.Incidence.graphEvaluation_smooth line 225
def OAI.Kaplansky.Incidence.graphFamily line 233
theorem OAI.Kaplansky.Incidence.graphEvaluation_zero_iff line 240
theorem OAI.Kaplansky.Incidence.graph_kernel_finrank line 253
theorem OAI.Kaplansky.Incidence.graph_kernel_bundle_smooth line 263
theorem OAI.Kaplansky.Incidence.incidence_model_finrank line 269