Documentation

Formalizations.RingTheory.FreeField.ThreeAxes.QuaternionResidues

Residues modulo 5 of the quaternions 1 ± 2q #

Finite part of the lemma that no binomial degenerates on the quaternion curve of the three-axes problem (Lemma 4.5). The Lipschitz quaternions map to M₂(𝔽₅) by 𝐢 ↦ diag(2,3), 𝐣 ↦ !![0,1;-1,0]. The six generators 1 ± 2𝐢, 1 ± 2𝐣, 1 ± 2𝐤 reduce to matrices of rank one, and the product of two residues vanishes exactly when the letters are mutually inverse. Hence the residue of the product of a reduced word is never zero.

Main results #

source
theorem ThreeAxes.QuaternionResidues.fact_prime_five :
Fact (Nat.Prime 5)
source
def ThreeAxes.QuaternionResidues.qi :
Matrix (Fin 2) (Fin 2) (ZMod 5)

The image of 𝐢 in M₂(𝔽₅).

Equations
Instances For
    source
    def ThreeAxes.QuaternionResidues.qj :
    Matrix (Fin 2) (Fin 2) (ZMod 5)

    The image of 𝐣 in M₂(𝔽₅).

    Equations
    Instances For
      source
      def ThreeAxes.QuaternionResidues.qk :
      Matrix (Fin 2) (Fin 2) (ZMod 5)

      The image of 𝐤 = 𝐢𝐣 in M₂(𝔽₅).

      Equations
      Instances For
        source
        theorem ThreeAxes.QuaternionResidues.qi_mul_qi :
        qi * qi = -1
        source
        theorem ThreeAxes.QuaternionResidues.qj_mul_qj :
        qj * qj = -1
        source
        theorem ThreeAxes.QuaternionResidues.qk_mul_qk :
        qk * qk = -1
        source
        theorem ThreeAxes.QuaternionResidues.qi_mul_qj :
        qi * qj = qk
        source
        theorem ThreeAxes.QuaternionResidues.qj_mul_qi :
        qj * qi = -qk
        source
        inductive ThreeAxes.QuaternionResidues.Gen :
        Type

        The six generators x = 1 + 2𝐢, X = 1 − 2𝐢, y = 1 + 2𝐣, Y = 1 − 2𝐣, z = 1 + 2𝐤, Z = 1 − 2𝐤 (up to the scalar 5, X = x⁻¹ etc.).

        Instances For
          source
          @[instance_reducible]
          instance ThreeAxes.QuaternionResidues.instDecidableEqGen :
          DecidableEq Gen
          Equations
          source
          def ThreeAxes.QuaternionResidues.Gen.inv :
          Gen → Gen

          The inverse letter.

          Equations
          Instances For
            source
            def ThreeAxes.QuaternionResidues.res :
            Gen → Matrix (Fin 2) (Fin 2) (ZMod 5)

            The residue mod 5 of a generator.

            Equations
            Instances For
              source
              def ThreeAxes.QuaternionResidues.col :
              Gen → Fin 2 → ZMod 5

              Column factor of the rank-one residue.

              Equations
              Instances For
                source
                def ThreeAxes.QuaternionResidues.row :
                Gen → Fin 2 → ZMod 5

                Row factor of the rank-one residue.

                Equations
                Instances For
                  source
                  theorem ThreeAxes.QuaternionResidues.res_eq_vecMulVec (a : Gen) :
                  res a = Matrix.vecMulVec (col a) (row a)
                  source
                  theorem ThreeAxes.QuaternionResidues.det_res (a : Gen) :
                  (res a).det = 0
                  source
                  theorem ThreeAxes.QuaternionResidues.res_ne_zero (a : Gen) :
                  res a ≠ 0
                  source
                  theorem ThreeAxes.QuaternionResidues.rank_pos_of_ne_zero {m : Type u_1} {n : Type u_2} {K : Type u_3} [Fintype m] [Fintype n] [DecidableEq n] [Field K] {A : Matrix m n K} (h : A ≠ 0) :
                  0 < A.rank
                  source
                  theorem ThreeAxes.QuaternionResidues.rank_res (a : Gen) :
                  (res a).rank = 1
                  source
                  theorem ThreeAxes.QuaternionResidues.res_mul_res_eq_zero_iff (a b : Gen) :
                  res a * res b = 0 ↔ b = a.inv

                  The 36 products: res a * res b = 0 exactly when b = a⁻¹.

                  source
                  theorem ThreeAxes.QuaternionResidues.row_dotProduct_col_ne_zero {a b : Gen} (h : b ≠ a.inv) :
                  row a ⬝ᵥ col b ≠ 0
                  source
                  theorem ThreeAxes.QuaternionResidues.vecMulVec_col_row_ne_zero (a b : Gen) :
                  Matrix.vecMulVec (col a) (row b) ≠ 0
                  source
                  theorem ThreeAxes.QuaternionResidues.prod_res_eq_smul (a : Gen) (w : List Gen) (hw : List.IsChain (fun (p q : Gen) => q ≠ p.inv) (a :: w)) :
                  ∃ (c : ZMod 5), c ≠ 0 ∧ (List.map res (a :: w)).prod = c • Matrix.vecMulVec (col a) (row ((a :: w).getLast ⋯))

                  Along a reduced word a :: w (no letter followed by its inverse) the product of the residues is a nonzero multiple of vecMulVec (col a) (row b) for the last letter b.

                  source
                  theorem ThreeAxes.QuaternionResidues.prod_res_ne_zero (w : List Gen) (hne : w ≠ []) (hw : List.IsChain (fun (p q : Gen) => q ≠ p.inv) w) :
                  (List.map res w).prod ≠ 0

                  The residue mod 5 of the product along a nonempty reduced word is nonzero.