OAI/Geometry/ComplexBundle/Replacement.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Quantitative bundle rank margins and repeated-line replacement maps.

  1. theorem OAI.Kaplansky.small_incidence line 15
  2. theorem OAI.Kaplansky.small_rank_endpoint line 24
  3. theorem OAI.Kaplansky.large_incidence line 28
  4. theorem OAI.Kaplansky.replacement_rank line 37
  5. theorem OAI.Kaplansky.prefix_dimension_margin line 39
  6. theorem OAI.Kaplansky.retained_trivial_rank_bound line 43
  7. theorem OAI.Kaplansky.Incidence.fresh_incidence_dimension line 53
  8. theorem OAI.Kaplansky.Incidence.source_incidence_dimension_iff line 73
  9. theorem OAI.Kaplansky.Incidence.exists_sixteen_replacement_maps line 96
  10. theorem OAI.Kaplansky.Incidence.exists_eight_fresh_bundle_maps line 147
  11. def OAI.Kaplansky.scalarTensor line 185

    Source documentation

    A scalar matrix tensored with the identity of a line fiber. This formula uses only scalar multiplication, not a choice of a vector in that line.

    def scalarTensor (T : (Fin d → ℂ) →ₗ[ℂ] (Fin r → ℂ)) :
    (Fin d → L) →ₗ[ℂ] (Fin r → L) where
…
  12. def OAI.Kaplansky.lineCoordinates line 193
  13. theorem OAI.Kaplansky.scalarTensor_coordinates line 201
  14. theorem OAI.Kaplansky.scalarTensor_eq_conjugate line 212
  15. theorem OAI.Kaplansky.scalarTensor_expanding line 223

    Source documentation

    Tensoring an expanding scalar family with a line preserves expansion for all subspaces, and the tensor maps themselves are independent of the frame.

    theorem scalarTensor_expanding (m : ℕ) (T : Fin n → (Fin d → ℂ) →ₗ[ℂ] (Fin r → ℂ))
    (e : L ≃ₗ[ℂ] ℂ) (hT : ExpandingThrough m T) :
    ExpandingThrough m (fun i => scalarTensor (L := L) (T i)) := by
…

    Mentions: OAI.Kaplansky.ExpandingThrough, OAI.Kaplansky.scalarTensor

  16. theorem OAI.Kaplansky.exists_sixteen_line_replacement_maps line 229
  17. theorem OAI.Kaplansky.scalarTensor_expanding_rank_one line 237

    Source documentation

    Rank one is enough; the line coordinate equivalence is constructed.

    theorem scalarTensor_expanding_rank_one [FiniteDimensional ℂ L]
    (hL : Module.finrank ℂ L=1) (m : ℕ)
    (T : Fin n → (Fin d → ℂ) →ₗ[ℂ] (Fin r → ℂ)) (hT : ExpandingThrough m T) :
    ExpandingThrough m (fun i => scalarTensor (L := L) (T i)) := by
…

    Mentions: OAI.Kaplansky.ExpandingThrough, OAI.Kaplansky.scalarTensor

  18. theorem OAI.Kaplansky.scalarTensor_natural line 246

    Source documentation

    Tensoring commutes with every linear change of line coordinates.

    theorem scalarTensor_natural {M : Type*} [AddCommGroup M] [Module ℂ M]
    (T : (Fin d → ℂ) →ₗ[ℂ] (Fin r → ℂ)) (f : L →ₗ[ℂ] M) (v : Fin d → L) :
    (fun a => f (scalarTensor T v a))=scalarTensor T (fun j => f (v j)) := by
…

    Mentions: OAI.Kaplansky.scalarTensor

  19. theorem OAI.Kaplansky.exists_line_block_replacements line 254

    Source documentation

    The actual replacement maps on a finite sum of line-multiplicity blocks expand correlated subspaces. Each scalar family is constructed, not assumed.

    theorem exists_line_block_replacements (k m : ℕ) (hm : 0<m) (r : Fin k → ℕ)
    (hr : ∀ j, 16*m≤r j) (L : Fin k → Type*)
    [∀ j, AddCommGroup (L j)] [∀ j, Module ℂ (L j)] [∀ j, FiniteDimensional ℂ (L j)]
    (hL : ∀ j, Module.finrank ℂ (L j)=1) :
    ∃ T : ∀ j, Incidence.MatrixTuple 16 (4*r j) (r j),
      ExpandingThrough m (blockDiagonal (fun j i => scalarTensor (L := L j) (T j i).toLinearMap)) := by
…

    Mentions: OAI.Kaplansky.Incidence.MatrixTuple, OAI.Kaplansky.ExpandingThrough, OAI.Kaplansky.blockDiagonal, OAI.Kaplansky.scalarTensor

  20. theorem OAI.Kaplansky.exists_uniform_line_block_replacements line 276

    Source documentation

    The same scalar choices work simultaneously over every base point, including for nontrivial line bundles; fiber coordinates are not input.

    theorem exists_uniform_line_block_replacements {B : Type*}
    (k m : ℕ) (hm : 0<m) (r : Fin k → ℕ) (hr : ∀ j, 16*m≤r j)
    (L : Fin k → B → Type*)
    [∀ j x, AddCommGroup (L j x)] [∀ j x, Module ℂ (L j x)]
    [∀ j x, FiniteDimensional ℂ (L j x)]
    (hL : ∀ j x, finrank ℂ (L j x)=1) :
    ∃ T : ∀ j, Incidence.MatrixTuple 16 (4*r j) (r j),
      ∀ x, ExpandingThrough m
        (blockDiagonal (fun j i => scalarTensor (L := L j x) (T j i).toLinearMap)) := by
…

    Mentions: OAI.Kaplansky.Incidence.MatrixTuple, OAI.Kaplansky.ExpandingThrough, OAI.Kaplansky.blockDiagonal, OAI.Kaplansky.scalarTensor

  21. theorem OAI.Kaplansky.scalarTensor_smooth_section_components line 306

    Source documentation

    The frame-independent tensor formula preserves smooth sections in every output component. Thus the scalar tensor maps have the required local smoothness; no smooth global frame for the line is assumed.

    theorem scalarTensor_smooth_section_components {d r : ℕ}
    (T : (Fin d → ℂ) →ₗ[ℂ] (Fin r → ℂ)) (s : Fin d → ∀ x, E x)
    (hs : ∀ j, ContMDiff I (I.prod 𝓘(ℝ,F)) ∞
      (fun x => TotalSpace.mk' F x (s j x))) (a : Fin r) :
    ContMDiff I (I.prod 𝓘(ℝ,F)) ∞
      (fun x => TotalSpace.mk' F x (scalarTensor T (fun j => s j x) a)) :=
…

    Mentions: OAI.Kaplansky.scalarTensor

  22. abbrev OAI.Kaplansky.RepeatedLineModel line 325
  23. def OAI.Kaplansky.repeatedLineCore line 327
  24. def OAI.Kaplansky.repeatedLineFiberEquiv line 329
  25. def OAI.Kaplansky.repeatedLineMap line 340

    Source documentation

    The actual bundle map obtained by tensoring each scalar block with its line identity, expressed in the finite-sum core fibers.

    def repeatedLineMap (D E : Fin k → ℕ)
    (T : ∀ s, (Fin (D s) → ℂ) →ₗ[ℂ] (Fin (E s) → ℂ)) (x : B) :
    (repeatedLineCore C D).Fiber x →ₗ[ℂ] (repeatedLineCore C E).Fiber x :=
…

    Mentions: OAI.Kaplansky.repeatedLineCore

  26. theorem OAI.Kaplansky.repeatedLineMap_apply line 347
  27. theorem OAI.Kaplansky.repeatedLineMap_chart line 354

    Source documentation

    The local chart formula is exactly the same scalar tensor expression. In particular it contains no arbitrary choice of line frame.

    theorem repeatedLineMap_chart (D E : Fin k → ℕ)
    (T : ∀ s, (Fin (D s) → ℂ) →ₗ[ℂ] (Fin (E s) → ℂ)) (x y : B)
    (v : (repeatedLineCore C D).Fiber y) (s : Fin k) (b : Fin (E s)) :
    ((trivializationAt (RepeatedLineModel E) (repeatedLineCore C E).Fiber x)
      ⟨y,repeatedLineMap C D E T y v⟩).2 ⟨s,b⟩ =
    ∑ a, T s (Pi.single a 1) b *
      ((trivializationAt (RepeatedLineModel D) (repeatedLineCore C D).Fiber x) ⟨y,v⟩).2 ⟨s,a⟩ := by
…

    Mentions: OAI.Kaplansky.repeatedLineCore, OAI.Kaplansky.RepeatedLineModel, OAI.Kaplansky.repeatedLineMap

  28. theorem OAI.Kaplansky.continuous_repeatedLineMap line 370

    Source documentation

    Componentwise smooth-section formulas alone do not establish this claim: the map on the actual finite-sum total spaces is continuous.

    theorem continuous_repeatedLineMap (D E : Fin k → ℕ)
    (T : ∀ s, (Fin (D s) → ℂ) →ₗ[ℂ] (Fin (E s) → ℂ)) :
    Continuous (fun z : TotalSpace (RepeatedLineModel D) (repeatedLineCore C D).Fiber =>
      TotalSpace.mk' (RepeatedLineModel E) z.proj (repeatedLineMap C D E T z.proj z.2)) := by
…

    Mentions: OAI.Kaplansky.RepeatedLineModel, OAI.Kaplansky.repeatedLineCore, OAI.Kaplansky.repeatedLineMap

  29. theorem OAI.Kaplansky.exists_continuous_repeatedLine_replacements line 406

    Source documentation

    The constructed uniform scalar choices give continuous total-space maps on the actual bundles and expand every small fiber subspace.

    theorem exists_continuous_repeatedLine_replacements
    (m : ℕ) (hm : 0<m) (r : Fin k → ℕ) (hr : ∀ s, 16*m≤r s) :
    ∃ A : ∀ x, Fin 16 →
      (repeatedLineCore C (fun s => 4*r s)).Fiber x →ₗ[ℂ] (repeatedLineCore C r).Fiber x,
      (∀ i, Continuous (fun z : TotalSpace (RepeatedLineModel (fun s => 4*r s))
        (repeatedLineCore C (fun s => 4*r s)).Fiber =>
        TotalSpace.mk' (RepeatedLineModel r) z.proj (A z.proj i z.2))) ∧
      ∀ x, ExpandingThrough m (A x) := by
…

    Mentions: OAI.Kaplansky.repeatedLineCore, OAI.Kaplansky.RepeatedLineModel, OAI.Kaplansky.ExpandingThrough