The Markoff group action

This file turns the polynomial identities from BGS.Markoff.Basic into an action on the Markoff surface itself. In particular, membership in the surface is part of the type of every generator. The group Gamma is the subgroup generated by the three Vieta involutions and the two adjacent coordinate transpositions.

The origin is fixed by every generator, hence by all of Gamma. Consequently the same group acts on the punctured surface; this is the action used in finite-field transitivity statements.

@[reducible, inline]

abbrev BGS.Markoff.MarkoffSurface (R : Type u) [CommRing R] : Type u

The Markoff surface as a subtype of affine three-space.

Equations

• BGS.Markoff.MarkoffSurface R = { x : BGS.Markoff.Point R // BGS.Markoff.IsMarkoff x }

def BGS.Markoff.surfaceOrigin (R : Type u) [CommRing R] : MarkoffSurface R

The origin, regarded as a point of the Markoff surface.

Equations

• BGS.Markoff.surfaceOrigin R = ⟨BGS.Markoff.origin, ⋯⟩

@[simp]

theorem BGS.Markoff.isMarkoff_swap12 {R : Type u} [CommRing R] (x : Point R) : IsMarkoff (swap12 x) ↔ IsMarkoff x

@[simp]

theorem BGS.Markoff.isMarkoff_swap23 {R : Type u} [CommRing R] (x : Point R) : IsMarkoff (swap23 x) ↔ IsMarkoff x

def BGS.Markoff.vieta1SurfacePerm (R : Type u) [CommRing R] : Equiv.Perm (MarkoffSurface R)

The first Vieta involution, restricted to the Markoff surface.

Equations

• BGS.Markoff.vieta1SurfacePerm R = Equiv.subtypeEquiv (BGS.Markoff.vieta1Equiv R) ⋯

def BGS.Markoff.vieta2SurfacePerm (R : Type u) [CommRing R] : Equiv.Perm (MarkoffSurface R)

The second Vieta involution, restricted to the Markoff surface.

Equations

• BGS.Markoff.vieta2SurfacePerm R = Equiv.subtypeEquiv (BGS.Markoff.vieta2Equiv R) ⋯

def BGS.Markoff.vieta3SurfacePerm (R : Type u) [CommRing R] : Equiv.Perm (MarkoffSurface R)

The third Vieta involution, restricted to the Markoff surface.

Equations

• BGS.Markoff.vieta3SurfacePerm R = Equiv.subtypeEquiv (BGS.Markoff.vieta3Equiv R) ⋯

def BGS.Markoff.swap12SurfacePerm (R : Type u) [CommRing R] : Equiv.Perm (MarkoffSurface R)

The first coordinate transposition, restricted to the Markoff surface.

Equations

• BGS.Markoff.swap12SurfacePerm R = Equiv.subtypeEquiv (BGS.Markoff.swap12Equiv R) ⋯

def BGS.Markoff.swap23SurfacePerm (R : Type u) [CommRing R] : Equiv.Perm (MarkoffSurface R)

The second coordinate transposition, restricted to the Markoff surface.

Equations

• BGS.Markoff.swap23SurfacePerm R = Equiv.subtypeEquiv (BGS.Markoff.swap23Equiv R) ⋯

@[simp]

theorem BGS.Markoff.coe_vieta1SurfacePerm {R : Type u} [CommRing R] (x : MarkoffSurface R) : ↑((vieta1SurfacePerm R) x) = vieta1 ↑x

@[simp]

theorem BGS.Markoff.coe_vieta2SurfacePerm {R : Type u} [CommRing R] (x : MarkoffSurface R) : ↑((vieta2SurfacePerm R) x) = vieta2 ↑x

@[simp]

theorem BGS.Markoff.coe_vieta3SurfacePerm {R : Type u} [CommRing R] (x : MarkoffSurface R) : ↑((vieta3SurfacePerm R) x) = vieta3 ↑x

@[simp]

theorem BGS.Markoff.coe_swap12SurfacePerm {R : Type u} [CommRing R] (x : MarkoffSurface R) : ↑((swap12SurfacePerm R) x) = swap12 ↑x

@[simp]

theorem BGS.Markoff.coe_swap23SurfacePerm {R : Type u} [CommRing R] (x : MarkoffSurface R) : ↑((swap23SurfacePerm R) x) = swap23 ↑x

@[simp]

theorem BGS.Markoff.vieta1SurfacePerm_surfaceOrigin (R : Type u) [CommRing R] : (vieta1SurfacePerm R) (surfaceOrigin R) = surfaceOrigin R

@[simp]

theorem BGS.Markoff.vieta2SurfacePerm_surfaceOrigin (R : Type u) [CommRing R] : (vieta2SurfacePerm R) (surfaceOrigin R) = surfaceOrigin R

@[simp]

theorem BGS.Markoff.vieta3SurfacePerm_surfaceOrigin (R : Type u) [CommRing R] : (vieta3SurfacePerm R) (surfaceOrigin R) = surfaceOrigin R

@[simp]

theorem BGS.Markoff.swap12SurfacePerm_surfaceOrigin (R : Type u) [CommRing R] : (swap12SurfacePerm R) (surfaceOrigin R) = surfaceOrigin R

@[simp]

theorem BGS.Markoff.swap23SurfacePerm_surfaceOrigin (R : Type u) [CommRing R] : (swap23SurfacePerm R) (surfaceOrigin R) = surfaceOrigin R

@[simp]

theorem BGS.Markoff.vieta1SurfacePerm_ne_origin_iff {R : Type u} [CommRing R] (x : MarkoffSurface R) : (vieta1SurfacePerm R) x ≠ surfaceOrigin R ↔ x ≠ surfaceOrigin R

@[simp]

theorem BGS.Markoff.vieta2SurfacePerm_ne_origin_iff {R : Type u} [CommRing R] (x : MarkoffSurface R) : (vieta2SurfacePerm R) x ≠ surfaceOrigin R ↔ x ≠ surfaceOrigin R

@[simp]

theorem BGS.Markoff.vieta3SurfacePerm_ne_origin_iff {R : Type u} [CommRing R] (x : MarkoffSurface R) : (vieta3SurfacePerm R) x ≠ surfaceOrigin R ↔ x ≠ surfaceOrigin R

@[simp]

theorem BGS.Markoff.swap12SurfacePerm_ne_origin_iff {R : Type u} [CommRing R] (x : MarkoffSurface R) : (swap12SurfacePerm R) x ≠ surfaceOrigin R ↔ x ≠ surfaceOrigin R

@[simp]

theorem BGS.Markoff.swap23SurfacePerm_ne_origin_iff {R : Type u} [CommRing R] (x : MarkoffSurface R) : (swap23SurfacePerm R) x ≠ surfaceOrigin R ↔ x ≠ surfaceOrigin R

@[reducible, inline]

abbrev BGS.Markoff.PuncturedMarkoffSurface (R : Type u) [CommRing R] : Type u

The punctured Markoff surface, expressed as the complement of the surface origin.

Equations

• BGS.Markoff.PuncturedMarkoffSurface R = { x : BGS.Markoff.MarkoffSurface R // x ≠ BGS.Markoff.surfaceOrigin R }

def BGS.Markoff.puncturedSurfaceEquiv (R : Type u) [CommRing R] : PuncturedMarkoffSurface R ≃ ↑(puncturedSurface R)

The action carrier is the same punctured surface as the set defined in Basic.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BGS.Markoff.puncturedSurfaceEquiv_coe {R : Type u} [CommRing R] (x : PuncturedMarkoffSurface R) : ↑((puncturedSurfaceEquiv R) x) = ↑↑x

def BGS.Markoff.restrictPermNe {A : Type u_1} (e : Equiv.Perm A) (a : A) (h : e a = a) : Equiv.Perm { x : A // x ≠ a }

Restrict a permutation to the complement of one of its fixed points.

Equations

• BGS.Markoff.restrictPermNe e a h = { toFun := fun (x : { x : A // x ≠ a }) => ⟨e ↑x, ⋯⟩, invFun := fun (x : { x : A // x ≠ a }) => ⟨(Equiv.symm e) ↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

def BGS.Markoff.vieta1PuncturedPerm (R : Type u) [CommRing R] : Equiv.Perm (PuncturedMarkoffSurface R)

The first Vieta involution on the punctured Markoff surface.

Equations

• BGS.Markoff.vieta1PuncturedPerm R = BGS.Markoff.restrictPermNe (BGS.Markoff.vieta1SurfacePerm R) (BGS.Markoff.surfaceOrigin R) ⋯

def BGS.Markoff.vieta2PuncturedPerm (R : Type u) [CommRing R] : Equiv.Perm (PuncturedMarkoffSurface R)

The second Vieta involution on the punctured Markoff surface.

Equations

• BGS.Markoff.vieta2PuncturedPerm R = BGS.Markoff.restrictPermNe (BGS.Markoff.vieta2SurfacePerm R) (BGS.Markoff.surfaceOrigin R) ⋯

def BGS.Markoff.vieta3PuncturedPerm (R : Type u) [CommRing R] : Equiv.Perm (PuncturedMarkoffSurface R)

The third Vieta involution on the punctured Markoff surface.

Equations

• BGS.Markoff.vieta3PuncturedPerm R = BGS.Markoff.restrictPermNe (BGS.Markoff.vieta3SurfacePerm R) (BGS.Markoff.surfaceOrigin R) ⋯

def BGS.Markoff.swap12PuncturedPerm (R : Type u) [CommRing R] : Equiv.Perm (PuncturedMarkoffSurface R)

The first coordinate transposition on the punctured Markoff surface.

Equations

• BGS.Markoff.swap12PuncturedPerm R = BGS.Markoff.restrictPermNe (BGS.Markoff.swap12SurfacePerm R) (BGS.Markoff.surfaceOrigin R) ⋯

def BGS.Markoff.swap23PuncturedPerm (R : Type u) [CommRing R] : Equiv.Perm (PuncturedMarkoffSurface R)

The second coordinate transposition on the punctured Markoff surface.

Equations

• BGS.Markoff.swap23PuncturedPerm R = BGS.Markoff.restrictPermNe (BGS.Markoff.swap23SurfacePerm R) (BGS.Markoff.surfaceOrigin R) ⋯

def BGS.Markoff.gammaGenerators (R : Type u) [CommRing R] : Set (Equiv.Perm (MarkoffSurface R))

The five standard generators of the Markoff group on the surface.

Equations

• One or more equations did not get rendered due to their size.

def BGS.Markoff.Gamma (R : Type u) [CommRing R] : Subgroup (Equiv.Perm (MarkoffSurface R))

The Markoff group generated by Vieta involutions and coordinate permutations.

Equations

• BGS.Markoff.Gamma R = Subgroup.closure (BGS.Markoff.gammaGenerators R)

theorem BGS.Markoff.vieta1SurfacePerm_mem_Gamma (R : Type u) [CommRing R] : vieta1SurfacePerm R ∈ Gamma R

theorem BGS.Markoff.vieta2SurfacePerm_mem_Gamma (R : Type u) [CommRing R] : vieta2SurfacePerm R ∈ Gamma R

theorem BGS.Markoff.vieta3SurfacePerm_mem_Gamma (R : Type u) [CommRing R] : vieta3SurfacePerm R ∈ Gamma R

theorem BGS.Markoff.swap12SurfacePerm_mem_Gamma (R : Type u) [CommRing R] : swap12SurfacePerm R ∈ Gamma R

theorem BGS.Markoff.swap23SurfacePerm_mem_Gamma (R : Type u) [CommRing R] : swap23SurfacePerm R ∈ Gamma R

def BGS.Markoff.gammaVieta1 (R : Type u) [CommRing R] : ↥(Gamma R)

The first Vieta generator as an element of Gamma.

Equations

• BGS.Markoff.gammaVieta1 R = ⟨BGS.Markoff.vieta1SurfacePerm R, ⋯⟩

def BGS.Markoff.gammaVieta2 (R : Type u) [CommRing R] : ↥(Gamma R)

The second Vieta generator as an element of Gamma.

Equations

• BGS.Markoff.gammaVieta2 R = ⟨BGS.Markoff.vieta2SurfacePerm R, ⋯⟩

def BGS.Markoff.gammaVieta3 (R : Type u) [CommRing R] : ↥(Gamma R)

The third Vieta generator as an element of Gamma.

Equations

• BGS.Markoff.gammaVieta3 R = ⟨BGS.Markoff.vieta3SurfacePerm R, ⋯⟩

def BGS.Markoff.gammaSwap12 (R : Type u) [CommRing R] : ↥(Gamma R)

The first adjacent transposition as an element of Gamma.

Equations

• BGS.Markoff.gammaSwap12 R = ⟨BGS.Markoff.swap12SurfacePerm R, ⋯⟩

def BGS.Markoff.gammaSwap23 (R : Type u) [CommRing R] : ↥(Gamma R)

The second adjacent transposition as an element of Gamma.

Equations

• BGS.Markoff.gammaSwap23 R = ⟨BGS.Markoff.swap23SurfacePerm R, ⋯⟩

@[simp]

theorem BGS.Markoff.gammaVieta1_smul_surface {R : Type u} [CommRing R] (x : MarkoffSurface R) : gammaVieta1 R • x = (vieta1SurfacePerm R) x

@[simp]

theorem BGS.Markoff.gammaVieta2_smul_surface {R : Type u} [CommRing R] (x : MarkoffSurface R) : gammaVieta2 R • x = (vieta2SurfacePerm R) x

@[simp]

theorem BGS.Markoff.gammaVieta3_smul_surface {R : Type u} [CommRing R] (x : MarkoffSurface R) : gammaVieta3 R • x = (vieta3SurfacePerm R) x

@[simp]

theorem BGS.Markoff.gammaSwap12_smul_surface {R : Type u} [CommRing R] (x : MarkoffSurface R) : gammaSwap12 R • x = (swap12SurfacePerm R) x

@[simp]

theorem BGS.Markoff.gammaSwap23_smul_surface {R : Type u} [CommRing R] (x : MarkoffSurface R) : gammaSwap23 R • x = (swap23SurfacePerm R) x

theorem BGS.Markoff.gammaGenerator_fixes_origin {R : Type u} [CommRing R] {g : Equiv.Perm (MarkoffSurface R)} (hg : g ∈ gammaGenerators R) : g (surfaceOrigin R) = surfaceOrigin R

Every standard generator fixes the origin. This is public so that the standalone Comparator specification can reproduce the exact declaration closure without depending on a module-private generated name.

theorem BGS.Markoff.Gamma_le_origin_stabilizer (R : Type u) [CommRing R] : Gamma R ≤ MulAction.stabilizer (Equiv.Perm (MarkoffSurface R)) (surfaceOrigin R)

Every element of Gamma fixes the origin.

@[simp]

theorem BGS.Markoff.Gamma_fixes_surfaceOrigin {R : Type u} [CommRing R] (g : ↥(Gamma R)) : g • surfaceOrigin R = surfaceOrigin R

@[instance_reducible]

instance BGS.Markoff.instMulActionSubtypePermMarkoffSurfaceMemSubgroupGammaPuncturedMarkoffSurface {R : Type u} [CommRing R] : MulAction (↥(Gamma R)) (PuncturedMarkoffSurface R)

The action of Gamma on the surface restricts to its punctured complement.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BGS.Markoff.gammaVieta1_smul_punctured {R : Type u} [CommRing R] (x : PuncturedMarkoffSurface R) : gammaVieta1 R • x = (vieta1PuncturedPerm R) x

@[simp]

theorem BGS.Markoff.gammaVieta2_smul_punctured {R : Type u} [CommRing R] (x : PuncturedMarkoffSurface R) : gammaVieta2 R • x = (vieta2PuncturedPerm R) x

@[simp]

theorem BGS.Markoff.gammaVieta3_smul_punctured {R : Type u} [CommRing R] (x : PuncturedMarkoffSurface R) : gammaVieta3 R • x = (vieta3PuncturedPerm R) x

@[simp]

theorem BGS.Markoff.gammaSwap12_smul_punctured {R : Type u} [CommRing R] (x : PuncturedMarkoffSurface R) : gammaSwap12 R • x = (swap12PuncturedPerm R) x

@[simp]

theorem BGS.Markoff.gammaSwap23_smul_punctured {R : Type u} [CommRing R] (x : PuncturedMarkoffSurface R) : gammaSwap23 R • x = (swap23PuncturedPerm R) x

def BGS.Markoff.gammaOrbit {R : Type u} [CommRing R] (x : MarkoffSurface R) : Set (MarkoffSurface R)

The orbit of a point on the Markoff surface under Gamma.

Equations

• BGS.Markoff.gammaOrbit x = MulAction.orbit (↥(BGS.Markoff.Gamma R)) x

def BGS.Markoff.SameComponent {R : Type u} [CommRing R] (x y : MarkoffSurface R) : Prop

Two surface points lie in the same Markoff component when they are in one Gamma-orbit.

Equations

• BGS.Markoff.SameComponent x y = (y ∈ BGS.Markoff.gammaOrbit x)

theorem BGS.Markoff.sameComponent_iff_exists {R : Type u} [CommRing R] (x y : MarkoffSurface R) : SameComponent x y ↔ ∃ (g : ↥(Gamma R)), g • x = y

theorem BGS.Markoff.sameComponent_refl {R : Type u} [CommRing R] (x : MarkoffSurface R) : SameComponent x x

theorem BGS.Markoff.sameComponent_symm {R : Type u} [CommRing R] {x y : MarkoffSurface R} (h : SameComponent x y) : SameComponent y x

theorem BGS.Markoff.sameComponent_trans {R : Type u} [CommRing R] {x y z : MarkoffSurface R} (hxy : SameComponent x y) (hyz : SameComponent y z) : SameComponent x z

theorem BGS.Markoff.sameComponent_iff_orbit_eq {R : Type u} [CommRing R] (x y : MarkoffSurface R) : SameComponent x y ↔ gammaOrbit x = gammaOrbit y

theorem BGS.Markoff.sameComponent_vieta1 {R : Type u} [CommRing R] (x : MarkoffSurface R) : SameComponent x ((vieta1SurfacePerm R) x)

theorem BGS.Markoff.sameComponent_vieta2 {R : Type u} [CommRing R] (x : MarkoffSurface R) : SameComponent x ((vieta2SurfacePerm R) x)

theorem BGS.Markoff.sameComponent_vieta3 {R : Type u} [CommRing R] (x : MarkoffSurface R) : SameComponent x ((vieta3SurfacePerm R) x)

theorem BGS.Markoff.sameComponent_swap12 {R : Type u} [CommRing R] (x : MarkoffSurface R) : SameComponent x ((swap12SurfacePerm R) x)

theorem BGS.Markoff.sameComponent_swap23 {R : Type u} [CommRing R] (x : MarkoffSurface R) : SameComponent x ((swap23SurfacePerm R) x)

def BGS.Markoff.puncturedGammaOrbit {R : Type u} [CommRing R] (x : PuncturedMarkoffSurface R) : Set (PuncturedMarkoffSurface R)

The orbit of a punctured point under the restricted Gamma action.

Equations

• BGS.Markoff.puncturedGammaOrbit x = MulAction.orbit (↥(BGS.Markoff.Gamma R)) x

def BGS.Markoff.SamePuncturedComponent {R : Type u} [CommRing R] (x y : PuncturedMarkoffSurface R) : Prop

The component relation on the punctured Markoff surface.

Equations

• BGS.Markoff.SamePuncturedComponent x y = (y ∈ BGS.Markoff.puncturedGammaOrbit x)

theorem BGS.Markoff.samePuncturedComponent_iff_exists {R : Type u} [CommRing R] (x y : PuncturedMarkoffSurface R) : SamePuncturedComponent x y ↔ ∃ (g : ↥(Gamma R)), g • x = y

theorem BGS.Markoff.samePuncturedComponent_refl {R : Type u} [CommRing R] (x : PuncturedMarkoffSurface R) : SamePuncturedComponent x x

theorem BGS.Markoff.samePuncturedComponent_symm {R : Type u} [CommRing R] {x y : PuncturedMarkoffSurface R} (h : SamePuncturedComponent x y) : SamePuncturedComponent y x

theorem BGS.Markoff.samePuncturedComponent_trans {R : Type u} [CommRing R] {x y z : PuncturedMarkoffSurface R} (hxy : SamePuncturedComponent x y) (hyz : SamePuncturedComponent y z) : SamePuncturedComponent x z

theorem BGS.Markoff.samePuncturedComponent_vieta1 {R : Type u} [CommRing R] (x : PuncturedMarkoffSurface R) : SamePuncturedComponent x ((vieta1PuncturedPerm R) x)

theorem BGS.Markoff.samePuncturedComponent_vieta2 {R : Type u} [CommRing R] (x : PuncturedMarkoffSurface R) : SamePuncturedComponent x ((vieta2PuncturedPerm R) x)

theorem BGS.Markoff.samePuncturedComponent_vieta3 {R : Type u} [CommRing R] (x : PuncturedMarkoffSurface R) : SamePuncturedComponent x ((vieta3PuncturedPerm R) x)

theorem BGS.Markoff.samePuncturedComponent_swap12 {R : Type u} [CommRing R] (x : PuncturedMarkoffSurface R) : SamePuncturedComponent x ((swap12PuncturedPerm R) x)

theorem BGS.Markoff.samePuncturedComponent_swap23 {R : Type u} [CommRing R] (x : PuncturedMarkoffSurface R) : SamePuncturedComponent x ((swap23PuncturedPerm R) x)