BundleIncidence.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Rank transport and smooth bundle-incidence families.

theorem OAI.Kaplansky.Incidence.rank_expansion_of_coordinates line 19

Source documentation

Strict collective-image rank bounds are invariant under actual fiber coordinate equivalences.

theorem rank_expansion_of_coordinates (T : ι → E →ₗ[𝕜] F) (C : ι → D →ₗ[𝕜] R)
    (e : E ≃ₗ[𝕜] D) (f : F ≃ₗ[𝕜] R)
    (hcomm : ∀ i x, f (T i x)=C i (e x)) {s t : ℕ}
    (hC : ∀ S : Submodule 𝕜 D, finrank 𝕜 S=s →
      t<finrank 𝕜 (⨆ i, S.map (C i) : Submodule 𝕜 R)) :
    ∀ S : Submodule 𝕜 E, finrank 𝕜 S=s →
      t<finrank 𝕜 (⨆ i, S.map (T i) : Submodule 𝕜 F) := by
…

theorem OAI.Kaplansky.Incidence.exists_bundle_incidence_maps line 65

Source documentation

The bundle incidence construction on a compact smooth manifold without boundary. The conclusion gives actual fiber maps, smooth in every frame, and strict image-rank bounds for every subspace of each original fiber. Global generation, incidence nullity and the good tuple are all constructed.

theorem exists_bundle_incidence_maps (pairs : Finset (ℕ × ℕ))
    (hpairs : ∀ p ∈ pairs, p.1≤d ∧ p.2≤r ∧
      finrank ℝ X+2*p.1*(d-p.1)+2*p.2*(r-p.2)<2*q*p.1*(r-p.2)) :
    ∃ T : Fin q → ∀ y, E y →L[ℂ] F y,
      (∀ i (e : Trivialization (Fin d → ℂ) (π (Fin d → ℂ) E))
        (f : Trivialization (Fin r → ℂ) (π (Fin r → ℂ) F))
        [MemTrivializationAtlas e] [MemTrivializationAtlas f],
        ContMDiffOn 𝓘(ℝ,X) 𝓘(ℝ,(Fin d → ℂ) →L[ℂ] (Fin r → ℂ)) ∞
          (complexHomCoordinates E F e f (T i)) (e.baseSet ∩ f.baseSet)) ∧
      ∀ y p, p ∈ pairs → ∀ S : Submodule ℂ (E y), finrank ℂ S=p.1 →
        p.2<finrank ℂ (⨆ i, S.map (T i y).toLinearMap : Submodule ℂ (F y)) := by
…

Mentions: OAI.Kaplansky.complexHomCoordinates

theorem OAI.Kaplansky.Incidence.exists_smooth_bundle_incidence_maps line 147