OAI/Geometry/Arnold/Projective.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ArnoldCounterexample.Quadric.normSquared_eq_zero_iff line 10
2. lemma OAI.ArnoldCounterexample.Quadric.normSquared_nonneg line 15
3. lemma OAI.ArnoldCounterexample.Quadric.normSquared_pos line 18
4. lemma OAI.ArnoldCounterexample.Quadric.quadricPolynomial_smul line 21
5. lemma OAI.ArnoldCounterexample.Quadric.normSquared_smul line 25
6. theorem OAI.ArnoldCounterexample.Quadric.project_surjective line 31

   Source documentation

   Every projective quadric point has a unit representative, proved without assuming the standard quotient geometry.

   theorem project_surjective : Function.Surjective project := by
   …

   Mentions: OAI.ArnoldCounterexample.project

7. lemma OAI.ArnoldCounterexample.Quadric.horizontal_smul line 53
8. lemma OAI.ArnoldCounterexample.Quadric.omega_I line 71
9. theorem OAI.ArnoldCounterexample.Quadric.omega_horizontal_nondegenerate line 85

   Source documentation

   Positivity on complex lines proves the actual horizontal form nondegenerate, with the factor 2 normalization.

   theorem omega_horizontal_nondegenerate {z v : CV} (hv : Horizontal z v)
       (hvanish : ∀ w : CV, Horizontal z w → omega v w = 0) : v = 0 := by
   …

   Mentions: OAI.ArnoldCounterexample.CV, OAI.ArnoldCounterexample.Horizontal, OAI.ArnoldCounterexample.omega

10. def OAI.ArnoldCounterexample.Quadric.bilinear line 97

    Source documentation

    Complex-bilinear pairing defining the quadric.

    def bilinear (z w : CV) : ℂ := ∑ j, z j * w j

    Mentions: OAI.ArnoldCounterexample.CV

11. lemma OAI.ArnoldCounterexample.Quadric.bilinear_comm line 99
12. lemma OAI.ArnoldCounterexample.Quadric.bilinear_add_left line 105
13. lemma OAI.ArnoldCounterexample.Quadric.bilinear_add_right line 108
14. lemma OAI.ArnoldCounterexample.Quadric.bilinear_smul_left line 111
15. lemma OAI.ArnoldCounterexample.Quadric.bilinear_smul_right line 114
16. lemma OAI.ArnoldCounterexample.Quadric.bilinear_self line 117
17. lemma OAI.ArnoldCounterexample.Quadric.bilinear_star_self line 120
18. lemma OAI.ArnoldCounterexample.Quadric.quadricPolynomial_star line 128
19. lemma OAI.ArnoldCounterexample.Quadric.quadricPolynomial_add line 131
20. def OAI.ArnoldCounterexample.Quadric.tangentConstraint line 140

    Source documentation

    The tangent space is the kernel of two independent complex linear forms.

    def tangentConstraint (z : CV) : CV →ₗ[ℂ] ℂ × ℂ where
    …

    Mentions: OAI.ArnoldCounterexample.CV

21. lemma OAI.ArnoldCounterexample.Quadric.horizontal_iff_constraint line 145
22. lemma OAI.ArnoldCounterexample.Quadric.tangentConstraint_surjective line 149
23. theorem OAI.ArnoldCounterexample.Quadric.horizontal_finrank line 164

    Source documentation

    Actual complex dimension three, hence real dimension six, of the horizontal tangent.

    theorem horizontal_finrank (z : UnitQuadric) :
        Module.finrank ℂ (LinearMap.ker (tangentConstraint z)) = 3 := by
    …

    Mentions: OAI.ArnoldCounterexample.UnitQuadric, OAI.ArnoldCounterexample.Quadric.tangentConstraint

24. def OAI.ArnoldCounterexample.Quadric.localSection line 174

    Source documentation

    A concrete polynomial parametrization transverse to the complex scaling. For horizontal v it stays on the quadric and its first derivative at zero is v. This makes the horizontal tangent identification independent of any assumed atlas.

    def localSection (z v : CV) : CV := z + v + (-(quadricPolynomial v / 2)) • star z

    Mentions: OAI.ArnoldCounterexample.CV, OAI.ArnoldCounterexample.quadricPolynomial

25. lemma OAI.ArnoldCounterexample.Quadric.localSection_on_quadric line 176
26. lemma OAI.ArnoldCounterexample.Quadric.localSection_gauge line 188
27. lemma OAI.ArnoldCounterexample.Quadric.localSection_ne_zero line 196