Documentation

Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Matrices with fixed determinant #

This file defines the type of matrices with fixed determinant m and proves some basic results about them.

We also prove that the subgroup of SL(2,โ„ค) generated by S and T is the whole group.

Note: Some of this was done originally in Lean 3 in the kbb (https://github.com/kim-em/kbb/tree/master) repository, so credit to those authors.

source
๐Ÿ”ธ coverage
def FixedDetMatrix (n : Type u_1) [DecidableEq n] [Fintype n] (R : Type u_2) [CommRing R] (m : R) :
Type (max 0 u_1 u_2)

The subtype of matrices with fixed determinant m

Instances For
    source
    theorem FixedDetMatrices.ext' (n : Type u_1) [DecidableEq n] [Fintype n] (R : Type u_2) [CommRing R] {m : R} {A B : FixedDetMatrix n R m} (h : โ†‘A = โ†‘B) :
    A = B

    Extensionality theorem for FixedDetMatrix with respect to the underlying matrix, not entrywise.

    source
    theorem FixedDetMatrices.ext (n : Type u_1) [DecidableEq n] [Fintype n] (R : Type u_2) [CommRing R] {m : R} {A B : FixedDetMatrix n R m} (h : โˆ€ (i j : n), โ†‘A i j = โ†‘B i j) :
    A = B
    source
    ๐Ÿ“ coverage
    theorem FixedDetMatrices.ext_iff {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommRing R] {m : R} {A B : FixedDetMatrix n R m} :
    A = B โ†” โˆ€ (i j : n), โ†‘A i j = โ†‘B i j
    source
    ๐Ÿ”ธ coverage
    @[implicit_reducible]
    instance FixedDetMatrices.instSMulSpecialLinearGroupFixedDetMatrix (n : Type u_1) [DecidableEq n] [Fintype n] (R : Type u_2) [CommRing R] (m : R) :
    SMul (Matrix.SpecialLinearGroup n R) (FixedDetMatrix n R m)
    source
    ๐Ÿ“ coverage
    theorem FixedDetMatrices.smul_def (n : Type u_1) [DecidableEq n] [Fintype n] (R : Type u_2) [CommRing R] (m : R) (g : Matrix.SpecialLinearGroup n R) (A : FixedDetMatrix n R m) :
    g โ€ข A = โŸจโ†‘g * โ†‘A, โ‹ฏโŸฉ
    source
    ๐Ÿ”ธ coverage
    @[implicit_reducible]
    instance FixedDetMatrices.instMulActionSpecialLinearGroupFixedDetMatrix (n : Type u_1) [DecidableEq n] [Fintype n] (R : Type u_2) [CommRing R] (m : R) :
    MulAction (Matrix.SpecialLinearGroup n R) (FixedDetMatrix n R m)
    source
    ๐Ÿ“ coverage
    theorem FixedDetMatrices.smul_coe (n : Type u_1) [DecidableEq n] [Fintype n] (R : Type u_2) [CommRing R] (m : R) (g : Matrix.SpecialLinearGroup n R) (A : FixedDetMatrix n R m) :
    โ†‘(g โ€ข A) = โ†‘g * โ†‘A
    source
    ๐Ÿ”ธ coverage
    def FixedDetMatrices.reps (m : โ„ค) :
    Set (FixedDetMatrix (Fin 2) โ„ค m)

    Set of representatives for the orbits under S and T

    Instances For
      source
      ๐Ÿ”ธ coverage
      def FixedDetMatrices.reduceStep {m : โ„ค} (A : FixedDetMatrix (Fin 2) โ„ค m) :
      FixedDetMatrix (Fin 2) โ„ค m

      Reduction step for matrices in ฮ” m which moves the matrices towards reps

      Instances For
        source
        ๐Ÿ”ธ coverage
        @[irreducible]
        def FixedDetMatrices.reduce_rec {m : โ„ค} {C : FixedDetMatrix (Fin 2) โ„ค m โ†’ Sort u_3} (base : (A : FixedDetMatrix (Fin 2) โ„ค m) โ†’ โ†‘A 1 0 = 0 โ†’ C A) (step : (A : FixedDetMatrix (Fin 2) โ„ค m) โ†’ โ†‘A 1 0 โ‰  0 โ†’ C (reduceStep A) โ†’ C A) (A : FixedDetMatrix (Fin 2) โ„ค m) :
        C A

        Reduction lemma for integral FixedDetMatrices.

        Instances For
          source
          ๐Ÿ”ธ coverage
          @[irreducible]
          def FixedDetMatrices.reduce {m : โ„ค} :
          FixedDetMatrix (Fin 2) โ„ค m โ†’ FixedDetMatrix (Fin 2) โ„ค m

          Map from ฮ” m โ†’ ฮ” m which reduces a FixedDetMatrix towards a representative element in reps

          Instances For
            source
            ๐Ÿ“ coverage
            theorem FixedDetMatrices.reduce_of_pos {m : โ„ค} {A : FixedDetMatrix (Fin 2) โ„ค m} (hc : โ†‘A 1 0 = 0) (ha : 0 < โ†‘A 0 0) :
            reduce A = ModularGroup.T ^ (-(โ†‘A 0 1 / โ†‘A 1 1)) โ€ข A
            source
            ๐Ÿ“ coverage
            theorem FixedDetMatrices.reduce_of_not_pos {m : โ„ค} {A : FixedDetMatrix (Fin 2) โ„ค m} (hc : โ†‘A 1 0 = 0) (ha : ยฌ0 < โ†‘A 0 0) :
            reduce A = ModularGroup.T ^ (-(-โ†‘A 0 1 / -โ†‘A 1 1)) โ€ข ModularGroup.S โ€ข ModularGroup.S โ€ข A
            source
            ๐Ÿ“ coverage
            @[simp]
            theorem FixedDetMatrices.reduce_reduceStep {m : โ„ค} {A : FixedDetMatrix (Fin 2) โ„ค m} (hc : โ†‘A 1 0 โ‰  0) :
            reduce (reduceStep A) = reduce A
            source
            ๐Ÿ“ coverage
            theorem FixedDetMatrices.reps_entries_le_m' {m : โ„ค} {A : FixedDetMatrix (Fin 2) โ„ค m} (h : A โˆˆ reps m) (i j : Fin 2) :
            โ†‘A i j โˆˆ Finset.Icc (-|m|) |m|

            An auxiliary result bounding the size of the entries of the representatives in reps

            source
            ๐Ÿ“ coverage
            @[simp]
            theorem FixedDetMatrices.reps_zero_empty :
            reps 0 = โˆ…
            source
            ๐Ÿ”ธ coverage
            @[implicit_reducible]
            noncomputable instance FixedDetMatrices.repsFintype (k : โ„ค) :
            Fintype โ†‘(reps k)
            source
            ๐Ÿ“ coverage
            @[simp]
            theorem FixedDetMatrices.S_smul_four {m : โ„ค} (A : FixedDetMatrix (Fin 2) โ„ค m) :
            ModularGroup.S โ€ข ModularGroup.S โ€ข ModularGroup.S โ€ข ModularGroup.S โ€ข A = A
            source
            ๐Ÿ“ coverage
            @[simp]
            theorem FixedDetMatrices.T_S_rel_smul {m : โ„ค} (A : FixedDetMatrix (Fin 2) โ„ค m) :
            ModularGroup.S โ€ข ModularGroup.S โ€ข ModularGroup.S โ€ข ModularGroup.T โ€ข ModularGroup.S โ€ข ModularGroup.T โ€ข ModularGroup.S โ€ข A = ModularGroup.Tโปยน โ€ข A
            source
            ๐Ÿ“ coverage
            theorem FixedDetMatrices.reduce_mem_reps {m : โ„ค} (hm : m โ‰  0) (A : FixedDetMatrix (Fin 2) โ„ค m) :
            reduce A โˆˆ reps m
            source
            theorem FixedDetMatrices.induction_on {m : โ„ค} {C : FixedDetMatrix (Fin 2) โ„ค m โ†’ Prop} {A : FixedDetMatrix (Fin 2) โ„ค m} (hm : m โ‰  0) (h0 : โˆ€ (A : FixedDetMatrix (Fin 2) โ„ค m), โ†‘A 1 0 = 0 โ†’ 0 < โ†‘A 0 0 โ†’ 0 โ‰ค โ†‘A 0 1 โ†’ |โ†‘A 0 1| < |โ†‘A 1 1| โ†’ C A) (hS : โˆ€ (B : FixedDetMatrix (Fin 2) โ„ค m), C B โ†’ C (ModularGroup.S โ€ข B)) (hT : โˆ€ (B : FixedDetMatrix (Fin 2) โ„ค m), C B โ†’ C (ModularGroup.T โ€ข B)) :
            C A
            source
            ๐Ÿ“ coverage
            theorem FixedDetMatrices.reps_one_id (A : FixedDetMatrix (Fin 2) โ„ค 1) (a1 : โ†‘A 1 0 = 0) (a4 : 0 < โ†‘A 0 0) (a6 : |โ†‘A 0 1| < |โ†‘A 1 1|) :
            A = 1
            source
            ๐Ÿ“ coverage
            theorem SpecialLinearGroup.SL2Z_generators :
            Subgroup.closure {ModularGroup.S, ModularGroup.T} = โŠค

            SL(2, โ„ค) is generated by S and T.