OAI/Geometry/Arnold/Involution.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArnoldCounterexample.Quadric.involutionLinear line 13

    Source documentation

    The linear involution fixing the first coordinate.

    def involutionLinear : CV ≃ₗ[ℂ] CV where
…

    Mentions: OAI.ArnoldCounterexample.CV

  2. lemma OAI.ArnoldCounterexample.Quadric.involutionLinear_apply line 21
  3. lemma OAI.ArnoldCounterexample.Quadric.involutionLinear_twice line 24
  4. lemma OAI.ArnoldCounterexample.Quadric.involutionLinear_quadricPolynomial line 27
  5. lemma OAI.ArnoldCounterexample.Quadric.involutionLinear_normSquared line 33
  6. lemma OAI.ArnoldCounterexample.Quadric.involutionLinear_unit line 39
  7. lemma OAI.ArnoldCounterexample.Quadric.linearEquiv_ne_zero line 45

    Source documentation

    An injective complex-linear symmetry of the cone acts on the actual projective quadric, not on a substitute abstract model.

    lemma linearEquiv_ne_zero (D : CV ≃ₗ[ℂ] CV) {z : CV} (hz : z ≠ 0) : D z ≠ 0 := by
…

    Mentions: OAI.ArnoldCounterexample.CV

  8. def OAI.ArnoldCounterexample.Quadric.map line 49
  9. lemma OAI.ArnoldCounterexample.Quadric.map_mk line 57
  10. def OAI.ArnoldCounterexample.Quadric.involution line 65

    Source documentation

    The Hamiltonian involution's underlying projective equivalence.

    def involution : Q3 ≃ Q3 where
…

    Mentions: OAI.ArnoldCounterexample.Q3

  11. theorem OAI.ArnoldCounterexample.Quadric.involution_sq line 83
  12. lemma OAI.ArnoldCounterexample.Quadric.involution_project line 86
  13. theorem OAI.ArnoldCounterexample.Quadric.involution_fixed_project_iff line 91

    Source documentation

    The +1 eigenline is not on the quadric. All projectively fixed lines therefore lie in precisely the hyperplane z0=0.

    theorem involution_fixed_project_iff (z : UnitQuadric) :
    involution (project z) = project z ↔ (z : CV) 0 = 0 := by
…

    Mentions: OAI.ArnoldCounterexample.UnitQuadric, OAI.ArnoldCounterexample.Quadric.involution, OAI.ArnoldCounterexample.project, OAI.ArnoldCounterexample.CV