OAI/Geometry/ComplexBundle/OpenIncidence.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Kaplansky.SmoothKernel.open_kernel_incidence_image_null line 21

   Source documentation

   Nullity for a surjective family defined smoothly only on an open domain. Values outside that domain need not be smooth, continuous or surjective.

   theorem open_kernel_incidence_image_null [MeasurableSpace V] [BorelSpace V]
       (a : X → V →L[ℂ] W) (U : Set X) (hU : IsOpen U)
       (ha : ContDiffOn ℝ ∞ a U) (hs : ∀ x ∈ U, Function.Surjective (a x))
       (hd : finrank ℝ (X × KernelModel V W)<finrank ℝ V) :
       μH[finrank ℝ V] {v : V | ∃ x ∈ U, a x v=0}=0 := by
   …

   Mentions: OAI.Kaplansky.SmoothKernel.KernelModel

2. theorem OAI.Kaplansky.Incidence.graphEvaluation_smoothOn line 76
3. theorem OAI.Kaplansky.Incidence.open_graph_incidence_image_null line 88

   Source documentation

   Actual graph incidence over an open base chart is null under the real dimension gap; no extension of its evaluation map off the chart is assumed.

   theorem open_graph_incidence_image_null [MeasurableSpace V] [BorelSpace V]
       (hU : IsOpen U) (he : ContDiffOn ℝ ∞ ev U)
       (hs : ∀ y ∈ U, Function.Surjective (ev y))
       (hgap : finrank ℝ Y+2*s*k+2*t*l<2*q*s*l) :
       μH[finrank ℝ V] {v : V | ∃ y ∈ U, ∃ (a : GraphSlope s k) (b : GraphSlope t l),
         ∀ i, ∀ x ∈ a.toLinearMap.graph, ev y v i x ∈ b.toLinearMap.graph}=0 := by
   …

4. def OAI.Kaplansky.Incidence.OpenFrameBad line 133
5. theorem OAI.Kaplansky.Incidence.openFrameBad_null line 137
6. def OAI.Kaplansky.Incidence.OpenRankBad line 182
7. theorem OAI.Kaplansky.Incidence.openRankBad_null line 185
8. theorem OAI.Kaplansky.Incidence.exists_countable_chart_incidence_parameter line 207

   Source documentation

   A single parameter avoids every forbidden rank pair on every chart of a countable family. The maps, kernels, graph coverage and nullity are actual; only the smooth surjective coordinate evaluation data enter as hypotheses.

   theorem exists_countable_chart_incidence_parameter {ι : Type*} [Countable ι]
       (ev : ι → Y → V →L[ℂ] MatrixTuple q d r) (U : ι → Set Y)
       (hU : ∀ j, IsOpen (U j)) (he : ∀ j, ContDiffOn ℝ ∞ (ev j) (U j))
       (hs : ∀ j y, y ∈ U j → Function.Surjective (ev j y))
       (pairs : Finset (ℕ × ℕ))
       (hpairs : ∀ p ∈ pairs, p.1≤d ∧ p.2≤r ∧
         finrank ℝ Y+2*p.1*(d-p.1)+2*p.2*(r-p.2)<2*q*p.1*(r-p.2)) :
       ∃ v : V, ∀ j y, y ∈ U j → ∀ p ∈ pairs, ∀ S : Submodule ℂ (Fin d → ℂ),
         finrank ℂ S=p.1 → p.2<finrank ℂ
           (⨆ i, S.map (ev j y v i).toLinearMap : Submodule ℂ (Fin r → ℂ)) := by
   …

   Mentions: OAI.Kaplansky.Incidence.MatrixTuple