OAI/NumberTheory/DukePrimeDegree/Geometry/RootPairCoordinates.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Coordinates for an arbitrary opposite-root pair

Any two distinct coordinates can be placed first, with a nonempty complement when the degree is at least three. This removes the coordinate choice from the centralizer-orbit exclusion.

  1. lemma OAI.DukePrimeDegree.exists_rootPair_coordinates line 20
  2. theorem OAI.DukePrimeDegree.no_neutral_invariant_rootPair_orbit line 49

    Source documentation

    The centralizer-orbit exclusion for any pair of distinct coordinates, with no coordinate or weight choices remaining in the assumptions.

    theorem no_neutral_invariant_rootPair_orbit {n : ℕ} (hn : 2 < n)
    {i j : Fin n} (hij : i ≠ j)
    (μ : Measure (X n)) [IsFiniteMeasure μ] [NeZero μ]
    (x : X n)
    (hfull : ∀ᵐ y ∂μ, ∃ h : rootPairCentralizer hij, rightAction x (h : G n) = y)
    (hinv : ∀ (ell : Fin n → ℝ) (hell : ∑ r, ell r = 0), ell i = ell j →
      μ.map (fun y => rightAction y (diagonalOneParameter ell hell 1)) = μ) : False := by
…

    Mentions: OAI.DukePrimeDegree.rootPairCentralizer