Documentation

TauCeti.Combinatorics.PermutationTriple.ComputedInvariants

Executable invariants of permutation triples #

The canonical cycle data of a permutation triple is executable using Equiv.Perm.computedCycleType, whose finite search lists one length at the least element of each cycle. This file gives executable cycle counts, Euler characteristic, genus, order triple, and geometry type, each identified with its canonical mathematical counterpart. Fixed points are included, and the empty multiset has least common multiple one, so the order computation also applies in degree zero.

The genus computation preserves the canonical truncation on disconnected triples. Its geometric interpretation still requires connectedness; in particular the empty triple has computed genus one. The definitions are exposed so ordinary importing modules can reduce them with kernel decide, as well as evaluating them with #eval.

Computations can use the definitions in this file, while mathematical statements continue to use PermutationTriple.cycleCounts, PermutationTriple.eulerChar, PermutationTriple.genus, PermutationTriple.orderTriple, and PermutationTriple.geometryType.

Main declarations #

References #

source
def TauCeti.PermutationTriple.computedCycleCounts {n : ℕ} (t : PermutationTriple n) :
ℕ × ℕ × ℕ

The ordered numbers of cycles, including fixed points, computed from the full cycle data.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.PermutationTriple.computedCycleCounts_eq {n : ℕ} (t : PermutationTriple n) :
    t.computedCycleCounts = t.cycleCounts

    The executable cycle counts agree with the canonical cycle counts.

    source
    def TauCeti.PermutationTriple.computedEulerChar {n : ℕ} (t : PermutationTriple n) :
    ℤ

    The Euler characteristic of a permutation triple, computed from its executable cycle decompositions.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.PermutationTriple.computedEulerChar_eq {n : ℕ} (t : PermutationTriple n) :
      t.computedEulerChar = t.eulerChar

      The executable Euler characteristic agrees with the canonical Euler characteristic.

      source
      def TauCeti.PermutationTriple.computedGenus {n : ℕ} (t : PermutationTriple n) :
      ℕ

      The genus of a permutation triple, computed from its executable Euler characteristic. As for PermutationTriple.genus, this has its geometric meaning when the triple is connected.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.PermutationTriple.computedGenus_eq {n : ℕ} (t : PermutationTriple n) :
        t.computedGenus = t.genus

        The executable genus agrees with the canonical genus.

        source
        def TauCeti.PermutationTriple.computedOrderTriple {n : ℕ} (t : PermutationTriple n) :
        ℕ × ℕ × ℕ

        The ordered triple of component orders, computed as the least common multiples of the three executable cycle decompositions.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.PermutationTriple.computedOrderTriple_eq {n : ℕ} (t : PermutationTriple n) :
          t.computedOrderTriple = t.orderTriple

          The executable order triple agrees with the canonical order triple.

          source
          def TauCeti.PermutationTriple.computedGeometryType {n : ℕ} (t : PermutationTriple n) :
          GeometryType

          The spherical, Euclidean, or hyperbolic geometry type computed from the executable order triple by exact comparison in ℚ.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem TauCeti.PermutationTriple.computedGeometryType_eq {n : ℕ} (t : PermutationTriple n) :
            t.computedGeometryType = t.geometryType

            The executable geometry type agrees with the canonical geometry type.

            Small computations #

            The examples include an empty triple and a disconnected triple, whose computed genus records the canonical truncation, and connected Euclidean and hyperbolic triples.