Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Finite conjugation subquandles

Abstract

Shared source-attributed definitions for finite conjugation subquandles, used by both Ta counterexamples.

Definition 1.1 (Closure under conjugation).

Formalization. D5/S3/FiniteGroups/Quandles/ConjugationSubquandle.ConjClosed (✓ std3).

Citation. Lực Ta (2025). Good involutions of conjugation subquandles. DOI: 10.48550/arXiv.2505.08090. URL: https://arxiv.org/abs/2505.08090v5.

Commentary.

Ta, Lemma 2.10, printed page 5: “For all subsets X ⊆ G, the pair Conj X := (X, s|_X) is a subquandle of Conj G if and only if X is closed under conjugation by elements of the subgroup ⟨X⟩ of G generated by X.” Here G is a group with decidable equality and X is a finite subset. ConjClosed uses the element-wise closure condition for conjugation by elements of X. For finite X these conjugation maps are injective self-maps and hence permutations; closure then extends to H = ⟨X⟩.

Definition 1.2 (The restricted conjugation operation).

Formalization. D5/S3/FiniteGroups/Quandles/ConjugationSubquandle.s (✓ std3).

Citation. Lực Ta (2025). Good involutions of conjugation subquandles. DOI: 10.48550/arXiv.2505.08090. URL: https://arxiv.org/abs/2505.08090v5.

Commentary.

Ta, Example 2.6, printed page 5: “Let G be a group, and define s : G → S_G by sending each element g ∈ G to the conjugation map defined by s_g(h) := ghg⁻¹ for all h ∈ G. Then Conj G := (G, s) is a quandle called a conjugation quandle or conjugacy quandle. Note that s_g⁻¹ = s_{g⁻¹} for all g ∈ G.” The domain X in s is the subtype of elements of the finite subset; val forgets the membership proof and property supplies it. The argument h : ConjClosed X certifies that the displayed value belongs to X.

Definition 1.3 (Good involutions).

Formalization. D5/S3/FiniteGroups/Quandles/ConjugationSubquandle.Good (✓ std3).

Citation. Lực Ta (2025). Good involutions of conjugation subquandles. DOI: 10.48550/arXiv.2505.08090. URL: https://arxiv.org/abs/2505.08090v5.

Commentary.

Ta, Definition 3.8, printed page 7: “Let R = (X, s) be a rack. A good involution of R is an involution ρ ∈ S_X that satisfies the equalities ρ s_x = s_x ρ, s_{ρ(x)} = s_x⁻¹ for all x ∈ X. We denote the set of good involutions of R by Good R.” Good X h is the subtype of functions ρ : X → X satisfying these conditions. Involutive means ρ(ρ(y)) = y for every y; it implies bijectivity. The two displayed inverse identities encode Function.LeftInverse and Function.RightInverse, respectively, without requiring x⁻¹ ∈ X. The fixed parameter h certifies closure.

Definition 1.4 (Automorphisms).

Formalization. D5/S3/FiniteGroups/Quandles/ConjugationSubquandle.Aut (✓ std3).

Citation. Lực Ta (2025). Good involutions of conjugation subquandles. DOI: 10.48550/arXiv.2505.08090. URL: https://arxiv.org/abs/2505.08090v5.

Commentary.

Ta, Definition 2.17, printed page 6: “Given two racks (X, s) and (Y, t), we say that a map φ : X → Y is a rack homomorphism if φs_x = t_{φ(x)}φ for all x ∈ X. A rack isomorphism is a bijective rack homomorphism, and a rack automorphism of a rack R is a rack isomorphism from R to itself.” Definition 2.20, printed page 6: “We denote the automorphism group of a rack R = (X, s) by Aut R.” Aut X h is the subtype of bijections satisfying the homomorphism identity pointwise for all x and y.

Definition 1.5 (The number of conjugation orbits).

Formalization. D5/S3/FiniteGroups/Quandles/ConjugationSubquandle.orbitCount (✓ std3).

Citation. Lực Ta (2025). Good involutions of conjugation subquandles. DOI: 10.48550/arXiv.2505.08090. URL: https://arxiv.org/abs/2505.08090v5.

Commentary.

Ta, section 6.3.1, printed page 14: “In the following, let X/H denote the set of orbits of X under the action of H by conjugation.” Corollary 6.12 begins: “Let k(X) := |X/H|.” Here H = Subgroup.closure (X : Set G). The image sends each x ∈ X to the finite subset of y ∈ X of the form g x g⁻¹ for some g ∈ H. Its cardinality counts distinct orbit subsets, with duplicates removed by Finset.image. The existential variable g has type G; membership in H is an explicit conjunct. filter and image have the predicate/function first and the finite subset second.

References