Documentation

LeanPool.MarkoffModP.BGS.Markoff.Core.EvenSignAction

Even sign changes on the Markoff surface #

Changing the signs of exactly two coordinates preserves the Markoff equation. The four transformations form a Klein four-group. Vieta involutions commute with them, and coordinate transpositions permute them. Thus Gamma normalizes the even-sign subgroup.

source
inductive BGS.Markoff.EvenSign :
Type

The four sign vectors with product one.

Instances For
    source
    @[instance_reducible]
    instance BGS.Markoff.instDecidableEqEvenSign :
    DecidableEq EvenSign
    Equations
    source
    @[instance_reducible]
    instance BGS.Markoff.instReprEvenSign :
    Repr EvenSign
    Equations
    source
    def BGS.Markoff.instReprEvenSign.repr :
    EvenSign → ℕ → Std.Format
    Equations
    Instances For
      source
      @[instance_reducible]
      instance BGS.Markoff.instFintypeEvenSign :
      Fintype EvenSign
      Equations
      source
      def BGS.Markoff.EvenSign.mul :
      EvenSign → EvenSign → EvenSign

      Multiplication in the four-element even-sign group.

      Equations
      Instances For
        source
        @[instance_reducible]
        instance BGS.Markoff.EvenSign.instOne :
        One EvenSign
        Equations
        source
        @[instance_reducible]
        instance BGS.Markoff.EvenSign.instMul :
        Mul EvenSign
        Equations
        source
        @[instance_reducible]
        instance BGS.Markoff.EvenSign.instInv :
        Inv EvenSign
        Equations
        source
        @[instance_reducible]
        instance BGS.Markoff.EvenSign.instCommGroup :
        CommGroup EvenSign
        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[simp]
        theorem BGS.Markoff.EvenSign.one_eq_id :
        1 = id
        source
        @[simp]
        theorem BGS.Markoff.EvenSign.inv_eq_self (s : EvenSign) :
        s⁻¹ = s
        source
        @[simp]
        theorem BGS.Markoff.EvenSign.card_eq_four :
        Fintype.card EvenSign = 4
        source
        def BGS.Markoff.evenSignPoint {R : Type u} [CommRing R] :
        EvenSign → Point R → Point R

        Apply an even sign vector to an affine point.

        Equations
        Instances For
          source
          @[simp]
          theorem BGS.Markoff.evenSignPoint_id {R : Type u} [CommRing R] (x : Point R) :
          evenSignPoint EvenSign.id x = x
          source
          @[simp]
          theorem BGS.Markoff.evenSignPoint_mul {R : Type u} [CommRing R] (s t : EvenSign) (x : Point R) :
          evenSignPoint (s * t) x = evenSignPoint s (evenSignPoint t x)
          source
          @[simp]
          theorem BGS.Markoff.markoffPolynomial_evenSignPoint {R : Type u} [CommRing R] (s : EvenSign) (x : Point R) :
          markoffPolynomial (evenSignPoint s x) = markoffPolynomial x
          source
          @[simp]
          theorem BGS.Markoff.isMarkoff_evenSignPoint {R : Type u} [CommRing R] (s : EvenSign) (x : Point R) :
          IsMarkoff (evenSignPoint s x) ↔ IsMarkoff x
          source
          @[instance_reducible]
          instance BGS.Markoff.evenSignMulActionMarkoffSurface {R : Type u} [CommRing R] :
          MulAction EvenSign (MarkoffSurface R)
          Equations
          source
          @[simp]
          theorem BGS.Markoff.evenSign_smul_surface_coe {R : Type u} [CommRing R] (s : EvenSign) (x : MarkoffSurface R) :
          ↑(s • x) = evenSignPoint s ↑x
          source
          @[simp]
          theorem BGS.Markoff.evenSign_smul_surfaceOrigin {R : Type u} [CommRing R] (s : EvenSign) :
          s • surfaceOrigin R = surfaceOrigin R
          source
          theorem BGS.Markoff.evenSign_smul_ne_surfaceOrigin_iff {R : Type u} [CommRing R] (s : EvenSign) (x : MarkoffSurface R) :
          s • x ≠ surfaceOrigin R ↔ x ≠ surfaceOrigin R
          source
          @[instance_reducible]
          instance BGS.Markoff.evenSignMulActionPuncturedMarkoffSurface {R : Type u} [CommRing R] :
          MulAction EvenSign (PuncturedMarkoffSurface R)
          Equations
          source
          @[simp]
          theorem BGS.Markoff.evenSign_smul_punctured_coe {R : Type u} [CommRing R] (s : EvenSign) (x : PuncturedMarkoffSurface R) :
          ↑(s • x) = s • ↑x
          source
          def BGS.Markoff.evenSignSurfacePermHom (R : Type u) [CommRing R] :
          EvenSign →* Equiv.Perm (MarkoffSurface R)

          The permutation representation of the even-sign action on the Markoff surface.

          Equations
          Instances For
            source
            @[simp]
            theorem BGS.Markoff.evenSignSurfacePermHom_apply {R : Type u} [CommRing R] (s : EvenSign) (x : MarkoffSurface R) :
            ((evenSignSurfacePermHom R) s) x = s • x
            source
            def BGS.Markoff.evenSignSurfaceSubgroup (R : Type u) [CommRing R] :
            Subgroup (Equiv.Perm (MarkoffSurface R))

            The subgroup of surface permutations generated by even-sign changes.

            Equations
            Instances For
              source
              @[simp]
              theorem BGS.Markoff.vieta1_evenSignPoint {R : Type u} [CommRing R] (s : EvenSign) (x : Point R) :
              vieta1 (evenSignPoint s x) = evenSignPoint s (vieta1 x)
              source
              @[simp]
              theorem BGS.Markoff.vieta2_evenSignPoint {R : Type u} [CommRing R] (s : EvenSign) (x : Point R) :
              vieta2 (evenSignPoint s x) = evenSignPoint s (vieta2 x)
              source
              @[simp]
              theorem BGS.Markoff.vieta3_evenSignPoint {R : Type u} [CommRing R] (s : EvenSign) (x : Point R) :
              vieta3 (evenSignPoint s x) = evenSignPoint s (vieta3 x)
              source
              def BGS.Markoff.EvenSign.swap12 :
              EvenSign → EvenSign

              The even-sign action conjugated by the swap of the first two coordinates.

              Equations
              Instances For
                source
                def BGS.Markoff.EvenSign.swap23 :
                EvenSign → EvenSign

                The even-sign action conjugated by the swap of the last two coordinates.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem BGS.Markoff.EvenSign.swap12_swap12 (s : EvenSign) :
                  s.swap12.swap12 = s
                  source
                  @[simp]
                  theorem BGS.Markoff.EvenSign.swap23_swap23 (s : EvenSign) :
                  s.swap23.swap23 = s
                  source
                  @[simp]
                  theorem BGS.Markoff.swap12_evenSignPoint {R : Type u} [CommRing R] (s : EvenSign) (x : Point R) :
                  swap12 (evenSignPoint s x) = evenSignPoint s.swap12 (swap12 x)
                  source
                  @[simp]
                  theorem BGS.Markoff.swap23_evenSignPoint {R : Type u} [CommRing R] (s : EvenSign) (x : Point R) :
                  swap23 (evenSignPoint s x) = evenSignPoint s.swap23 (swap23 x)
                  source
                  theorem BGS.Markoff.vieta1SurfacePerm_commute_evenSign {R : Type u} [CommRing R] (s : EvenSign) :
                  vieta1SurfacePerm R * (evenSignSurfacePermHom R) s = (evenSignSurfacePermHom R) s * vieta1SurfacePerm R
                  source
                  theorem BGS.Markoff.vieta2SurfacePerm_commute_evenSign {R : Type u} [CommRing R] (s : EvenSign) :
                  vieta2SurfacePerm R * (evenSignSurfacePermHom R) s = (evenSignSurfacePermHom R) s * vieta2SurfacePerm R
                  source
                  theorem BGS.Markoff.vieta3SurfacePerm_commute_evenSign {R : Type u} [CommRing R] (s : EvenSign) :
                  vieta3SurfacePerm R * (evenSignSurfacePermHom R) s = (evenSignSurfacePermHom R) s * vieta3SurfacePerm R
                  source
                  theorem BGS.Markoff.swap12SurfacePerm_mul_evenSign {R : Type u} [CommRing R] (s : EvenSign) :
                  swap12SurfacePerm R * (evenSignSurfacePermHom R) s = (evenSignSurfacePermHom R) s.swap12 * swap12SurfacePerm R
                  source
                  theorem BGS.Markoff.swap23SurfacePerm_mul_evenSign {R : Type u} [CommRing R] (s : EvenSign) :
                  swap23SurfacePerm R * (evenSignSurfacePermHom R) s = (evenSignSurfacePermHom R) s.swap23 * swap23SurfacePerm R
                  source
                  theorem BGS.Markoff.Gamma_le_evenSignSurfaceSubgroup_normalizer (R : Type u) [CommRing R] :
                  Gamma R ≤ Subgroup.normalizer ↑(evenSignSurfaceSubgroup R)

                  Every Markoff-group element normalizes the subgroup of even sign changes.

                  source
                  theorem BGS.Markoff.exists_evenSign_smul_Gamma_smul {R : Type u} [CommRing R] (s : EvenSign) (g : ↥(Gamma R)) :
                  ∃ (t : EvenSign), ∀ (x : PuncturedMarkoffSurface R), s • g • x = g • t • x

                  An even sign change can be moved through an arbitrary Gamma word.