Documentation

LeanPool.MarkoffModP.BGS.Markoff.Assembly.EvenSignOrbitDivisibility

Divisibility from the free even-sign action #

For odd characteristic, the Klein four-group of even sign changes acts freely on the punctured Markoff surface. Consequently every finite sign-invariant set is a disjoint union of four-element sign orbits.

source
theorem BGS.Markoff.evenSign_eq_one_of_smul_eq {F : Type u_1} [Field F] (htwo : 2 ≠ 0) (s : EvenSign) (x : PuncturedMarkoffSurface F) (hfixed : s • x = x) :
s = 1

In characteristic different from two, no nontrivial even sign change fixes a punctured Markoff point.

source
theorem BGS.Markoff.evenSign_isCancelSMul_punctured {F : Type u_1} [Field F] (htwo : 2 ≠ 0) :
IsCancelSMul EvenSign (PuncturedMarkoffSurface F)

The even-sign action on the punctured Markoff surface is free in characteristic different from two.

source
noncomputable def BGS.Markoff.evenSignOrbitFinset {R : Type u_1} [CommRing R] (x : PuncturedMarkoffSurface R) :
Finset (PuncturedMarkoffSurface R)

The four-point orbit of a punctured point under even sign changes.

Equations
Instances For
    source
    @[simp]
    theorem BGS.Markoff.mem_evenSignOrbitFinset_iff {R : Type u_1} [CommRing R] {x y : PuncturedMarkoffSurface R} :
    y ∈ evenSignOrbitFinset x ↔ ∃ (s : EvenSign), s • x = y
    source
    theorem BGS.Markoff.evenSignOrbitFinset_eq_of_mem {R : Type u_1} [CommRing R] {x y : PuncturedMarkoffSurface R} (hy : y ∈ evenSignOrbitFinset x) :
    evenSignOrbitFinset y = evenSignOrbitFinset x
    source
    theorem BGS.Markoff.evenSignOrbitFinset_card_eq_four {F : Type u_1} [Field F] (htwo : 2 ≠ 0) (x : PuncturedMarkoffSurface F) :
    (evenSignOrbitFinset x).card = 4
    source
    noncomputable def BGS.Markoff.evenSignOrbitPartition {R : Type u_1} [CommRing R] (C : Finset (PuncturedMarkoffSurface R)) :
    Finset (Finset (PuncturedMarkoffSurface R))

    The finite family of distinct even-sign orbits meeting C.

    Equations
    Instances For
      source
      noncomputable def BGS.Markoff.evenSignOrbitPartitionUnion {R : Type u_1} [CommRing R] (C : Finset (PuncturedMarkoffSurface R)) :
      Finset (PuncturedMarkoffSurface R)

      The union of all even-sign orbits meeting C. This wrapper fixes one classical equality-decider for the nested finite union.

      Equations
      Instances For
        source
        theorem BGS.Markoff.evenSignOrbitPartition_pairwiseDisjoint {R : Type u_1} [CommRing R] (C : Finset (PuncturedMarkoffSurface R)) :
        (↑(evenSignOrbitPartition C)).PairwiseDisjoint id
        source
        theorem BGS.Markoff.evenSignOrbitPartitionUnion_eq {R : Type u_1} [CommRing R] (C : Finset (PuncturedMarkoffSurface R)) (hC : ∀ (s : EvenSign), ∀ x ∈ C, s • x ∈ C) :
        evenSignOrbitPartitionUnion C = C
        source
        theorem BGS.Markoff.four_dvd_finset_card_of_evenSign_invariant {F : Type u_1} [Field F] (htwo : 2 ≠ 0) (C : Finset (PuncturedMarkoffSurface F)) (hC : ∀ (s : EvenSign), ∀ x ∈ C, s • x ∈ C) :
        4 ∣ C.card

        Any finite set of punctured Markoff points preserved by all even sign changes has cardinality divisible by four.