OAI/Geometry/BundleTests/Retained.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kaplansky.labelFiberProdEquiv line 17
2. def OAI.Kaplansky.labelFiberSigmaEquiv line 24
3. theorem OAI.Kaplansky.labelFiberProd_card line 31
4. theorem OAI.Kaplansky.labelFiberSigma_card line 36
5. theorem OAI.Kaplansky.constantLabelFiber_card line 41
6. abbrev OAI.Kaplansky.RetainedSlot line 55
7. def OAI.Kaplansky.retainedLabel line 57
8. def OAI.Kaplansky.retainedBundleCore line 60
9. abbrev OAI.Kaplansky.RetainedBundle line 62
10. instance OAI.Kaplansky.retainedBundle_norm line 64
11. instance OAI.Kaplansky.retainedBundle_inner line 66
12. def OAI.Kaplansky.retainedFiberEquiv line 70

    Source documentation

    Grouping the fiber coordinates recovers m copies of every stage bundle.

    def retainedFiberEquiv (m R : ℕ) (P : SmoothTestBase m R) :
        RetainedBundle m R P ≃ₗ[ℂ] (∀ _ : Fin m, ∀ j : Fin (R+1),
          SmoothTestBundle m R R j.val (Nat.le_refl R) (Nat.le_of_lt_succ j.isLt) P) where
    …

    Mentions: OAI.Kaplansky.SmoothTestBase, OAI.Kaplansky.RetainedBundle, OAI.Kaplansky.SmoothTestBundle

13. theorem OAI.Kaplansky.continuous_retainedStage line 86

    Source documentation

    Each stage projection is continuous for the actual total-space topology.

    theorem continuous_retainedStage (m R : ℕ) (a : Fin m) (j : Fin (R+1)) :
        Continuous (fun z : TotalSpace (EuclideanSpace ℂ (RetainedSlot m R)) (RetainedBundle m R) =>
          TotalSpace.mk' (EuclideanSpace ℂ (TestBundleSlot m R j.val)) z.proj
            (retainedFiberEquiv m R z.proj z.2 a j)) := by
    …

    Mentions: OAI.Kaplansky.RetainedSlot, OAI.Kaplansky.RetainedBundle, OAI.Kaplansky.TestBundleSlot, OAI.Kaplansky.retainedFiberEquiv

14. theorem OAI.Kaplansky.retainedBundle_finrank line 96
15. theorem OAI.Kaplansky.testSummandLineIndex_eq_none line 113
16. theorem OAI.Kaplansky.retainedLabel_card_sum line 124
17. theorem OAI.Kaplansky.retainedLabel_none_card line 145
18. theorem OAI.Kaplansky.testSummandLineIndex_eq_some line 162
19. theorem OAI.Kaplansky.retainedLabel_some_stage_sum line 170
20. def OAI.Kaplansky.suffixReverseEquiv line 189
21. theorem OAI.Kaplansky.sum_suffix_reverse line 204
22. theorem OAI.Kaplansky.retainedLabel_some_card line 229

    Source documentation

    Each K_i is the count of actual occurrences of its hyperplane line in G, including all m copies and every retained stage.

    theorem retainedLabel_some_card (m R : ℕ) (i : Fin R) :
        Fintype.card {s : RetainedSlot m R // retainedLabel m R s=some i} = testProjectiveDimension m R i := by
    …

    Mentions: OAI.Kaplansky.RetainedSlot, OAI.Kaplansky.retainedLabel, OAI.Kaplansky.testProjectiveDimension

23. def OAI.Kaplansky.groupingByLabel line 246
24. def OAI.Kaplansky.retainedLineRank line 256
25. abbrev OAI.Kaplansky.RetainedGroupedSlot line 260
26. theorem OAI.Kaplansky.retainedLabel_card line 262
27. def OAI.Kaplansky.retainedGroupingEquiv line 269

    Source documentation

    Every retained line occurrence is accounted for exactly once.

    def retainedGroupingEquiv (m R : ℕ) : RetainedSlot m R ≃ RetainedGroupedSlot m R :=
    …

    Mentions: OAI.Kaplansky.RetainedSlot, OAI.Kaplansky.RetainedGroupedSlot

28. theorem OAI.Kaplansky.retainedGrouping_label line 274
29. def OAI.Kaplansky.lineSumRelabelUnitary line 279

    Source documentation

    Relabeling justified by an exact slot bijection preserves topology and metric, as well as the fiber linear structure.

    def lineSumRelabelUnitary {S T ι : Type*} [Fintype S] [Fintype T] [Fintype ι]
        (K : ι → ℕ) (a : T → Option ι) (b : S → Option ι) (e : T ≃ S)
        (h : ∀ t, a t=b (e t)) :
        UnitaryBundleEquiv (EuclideanSpace ℂ T) (EuclideanSpace ℂ S)
          (SmoothLineSumBundle K a) (SmoothLineSumBundle K b) := by
    …

    Mentions: OAI.Kaplansky.UnitaryBundleEquiv

30. def OAI.Kaplansky.retainedRegroupingUnitary line 288
31. theorem OAI.Kaplansky.retainedBundle_rank_decomposition line 296

    Source documentation

    The total rank in the actual Chern-decomposition presentation.

    theorem retainedBundle_rank_decomposition (m R : ℕ) (y : SmoothTestBase m R) :
        Module.finrank ℂ (RetainedBundle m R y) = retainedTrivialMultiplicity m R +
          ∑ i : Fin R, testProjectiveDimension m R i := by
    …

    Mentions: OAI.Kaplansky.SmoothTestBase, OAI.Kaplansky.RetainedBundle, OAI.Kaplansky.retainedTrivialMultiplicity, OAI.Kaplansky.testProjectiveDimension

32. theorem OAI.Kaplansky.retained_complement_rank_lt line 315