Documentation

TauCeti.Combinatorics.PermutationTriple.Passport.Cyclic

Totally ramified passports with cyclic monodromy #

Let r = finRotate n be cyclic rotation of Fin n. The triple (r, r ^ k, (r ^ (k + 1))⁻¹) is TauCeti.PermutationTriple.cyclicPowTriple n k; its monodromy group is the cyclic group generated by r. When k and k + 1 are coprime to n, each of its three components is a single n-cycle, so the triple lies in the passport TauCeti.PassportSpec.cyclicTotallyRamified n: reference group ⟨r⟩ and cycle partition [n] over each of 0, 1 and ∞.

For every nonzero n this passport is classified completely. A triple in it can be relabeled so that its component over 0 is r; its monodromy group then has order n and contains r, so it is ⟨r⟩, and the component over 1 is r ^ k for a unique k < n. The other two cycle partitions say exactly that k and k + 1 are coprime to n. Conversely, a relabeling fixing r commutes with every power of r, so distinct such exponents below n give non-isomorphic triples. For prime p, these exponents are precisely those satisfying 1 ≤ k ≤ p - 2, and the passport therefore has exactly p - 2 isomorphism classes.

In degree 5 this gives the passport with monodromy C₅ and ordered cycle partitions ([5], [5], [5]), whose three classes are represented by (r, r, r³), (r, r², r²) and (r, r³, r). In particular a passport does not determine the isomorphism class of a triple.

Main declarations #

References #

source
theorem TauCeti.ConnectedIsoClass.mk_cyclicPowTriple_eq_mk_cyclicPowTriple_iff {n : ℕ} (hn : n ≠ 0) {j k : ℕ} :
mk ⟨PermutationTriple.cyclicPowTriple n j, ⋯⟩ = mk ⟨PermutationTriple.cyclicPowTriple n k, ⋯⟩ ↔ j ≡ k [MOD n]

In nonzero degree, the triples cyclicPowTriple n j and cyclicPowTriple n k are isomorphic exactly when their exponents are congruent modulo n: a relabeling fixing the rotation r commutes with its powers.

source
theorem TauCeti.ConnectedIsoClass.mk_cyclicPowTriple_eq_mk_cyclicPowTriple_iff_of_lt {n j k : ℕ} (hj : j < n) (hk : k < n) :
mk ⟨PermutationTriple.cyclicPowTriple n j, ⋯⟩ = mk ⟨PermutationTriple.cyclicPowTriple n k, ⋯⟩ ↔ j = k

For exponents below the degree, the triples cyclicPowTriple n j and cyclicPowTriple n k are isomorphic exactly when j = k.

source
def TauCeti.PassportSpec.cyclicTotallyRamified (n : ℕ) :
PassportSpec n

The passport of degree n with reference monodromy group the cyclic group generated by rotation of Fin n, and with the single part n in each of its three cycle partitions: the covers it describes are totally ramified over each of 0, 1 and ∞.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.PassportSpec.cyclicTotallyRamified_G {n : ℕ} :
    (cyclicTotallyRamified n).G = Subgroup.zpowers (finRotate n)
    source
    @[simp]
    theorem TauCeti.PassportSpec.cyclicTotallyRamified_lam0 {n : ℕ} :
    (cyclicTotallyRamified n).lam0 = {n}
    source
    @[simp]
    theorem TauCeti.PassportSpec.cyclicTotallyRamified_lam1 {n : ℕ} :
    (cyclicTotallyRamified n).lam1 = {n}
    source
    @[simp]
    theorem TauCeti.PassportSpec.cyclicTotallyRamified_laminf {n : ℕ} :
    (cyclicTotallyRamified n).laminf = {n}
    source
    @[simp]
    theorem TauCeti.PassportSpec.partition_cyclicTotallyRamified {n : ℕ} (i : Fin 3) :
    (cyclicTotallyRamified n).partition i = {n}

    Each branch point of cyclicTotallyRamified n has the single-part cycle partition [n].

    source
    @[simp]
    theorem TauCeti.PassportSpec.isAdmissible_cyclicTotallyRamified {n : ℕ} :
    (cyclicTotallyRamified n).IsAdmissible ↔ n ≠ 0

    The totally ramified cyclic passport is admissible exactly in nonzero degree.

    source
    theorem TauCeti.PassportSpec.hasPassport_cyclicPowTriple {n k : ℕ} (hk : k.Coprime n) (hk' : (k + 1).Coprime n) :
    HasPassport ⟨PermutationTriple.cyclicPowTriple n k, ⋯⟩ (cyclicTotallyRamified n)

    The triple cyclicPowTriple n k has the passport cyclicTotallyRamified n when k and k + 1 are coprime to n.

    source
    @[simp]
    theorem TauCeti.PassportSpec.hasPassport_cyclicPowTriple_iff {n : ℕ} (hn : n ≠ 0) {k : ℕ} :
    HasPassport ⟨PermutationTriple.cyclicPowTriple n k, ⋯⟩ (cyclicTotallyRamified n) ↔ k.Coprime n ∧ (k + 1).Coprime n

    In nonzero degree, the triple cyclicPowTriple n k has the passport cyclicTotallyRamified n exactly when k and k + 1 are coprime to n.

    source
    theorem TauCeti.PassportSpec.exists_eq_cyclicPowTriple_of_hasPassport {n : ℕ} {s : ConnectedTriple n} (hs : HasPassport s (cyclicTotallyRamified n)) (h0 : (↑s).σ0 = finRotate n) :
    ∃ k < n, k.Coprime n ∧ (k + 1).Coprime n ∧ ↑s = PermutationTriple.cyclicPowTriple n k

    A triple in the passport cyclicTotallyRamified n whose component over 0 is rotation is (r, r ^ k) for a unique-range exponent whose two relevant powers are full cycles.

    source
    theorem TauCeti.PassportSpec.classSet_cyclicTotallyRamified {n : ℕ} (hn : n ≠ 0) :
    (cyclicTotallyRamified n).classSet = Finset.image (fun (k : ℕ) => ConnectedIsoClass.mk ⟨PermutationTriple.cyclicPowTriple n k, ⋯⟩) ({k ∈ Finset.range n | k.Coprime n ∧ (k + 1).Coprime n})

    In nonzero degree, the isomorphism classes in cyclicTotallyRamified n are indexed by the exponents k < n for which both k and k + 1 are coprime to n.

    source
    theorem TauCeti.PassportSpec.classSet_cyclicTotallyRamified_of_prime {p : ℕ} (hp : Nat.Prime p) :
    (cyclicTotallyRamified p).classSet = Finset.image (fun (k : ℕ) => ConnectedIsoClass.mk ⟨PermutationTriple.cyclicPowTriple p k, ⋯⟩) (Finset.Icc 1 (p - 2))

    For prime p, the general cyclic classification is indexed by the interval 1 ≤ k ≤ p - 2.

    source
    theorem TauCeti.PassportSpec.passportSize_cyclicTotallyRamified {p : ℕ} (hp : Nat.Prime p) :
    (cyclicTotallyRamified p).passportSize = p - 2

    For prime p, the passport cyclicTotallyRamified p has exactly p - 2 isomorphism classes.

    source
    theorem TauCeti.PassportSpec.classSet_cyclicTotallyRamified_five :
    (cyclicTotallyRamified 5).classSet = {ConnectedIsoClass.mk ⟨PermutationTriple.cyclicPowTriple 5 1, ⋯⟩, ConnectedIsoClass.mk ⟨PermutationTriple.cyclicPowTriple 5 2, ⋯⟩, ConnectedIsoClass.mk ⟨PermutationTriple.cyclicPowTriple 5 3, ⋯⟩}

    The passport of degree 5 with monodromy C₅ and cycle partitions ([5], [5], [5]) has three isomorphism classes, represented by (r, r, r³), (r, r², r²) and (r, r³, r) for the rotation r.

    source
    theorem TauCeti.PassportSpec.passportSize_cyclicTotallyRamified_five :
    (cyclicTotallyRamified 5).passportSize = 3

    The passport of degree 5 with monodromy C₅ and cycle partitions ([5], [5], [5]) has size three.