Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Noncommutative actual corner orbits

Abstract

The actual corner relation of the noncommutative face pairing is the specified subgroup orbit relation.

Definition 1.1 (Right action convention).

Lean statement: D5/S3/Geometry/Hyperideal/NoncommutativeCornerOrbits.act

Formalization. D5/S3/Geometry/Hyperideal/NoncommutativeCornerOrbits.act (✓ std3).

Source. Repository-derived.

Commentary.

For any group G, type Omega and left action of the opposite group on Omega, act(x,g) is op(g) acting on x. Thus it represents the right action of G on Omega.

Theorem 1.2 (Identity acts trivially).

Lean statement: D5/S3/Geometry/Hyperideal/NoncommutativeCornerOrbits.act_one

Proof. Machine-checked in Lean as D5/S3/Geometry/Hyperideal/NoncommutativeCornerOrbits.act_one (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every x in Omega, act(x,1)=x.

Theorem 1.3 (Composition of right actions).

Lean statement: D5/S3/Geometry/Hyperideal/NoncommutativeCornerOrbits.act_mul

Proof. Machine-checked in Lean as D5/S3/Geometry/Hyperideal/NoncommutativeCornerOrbits.act_mul (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every x in Omega and g,h in G, act(act(x,g),h)=act(x,g*h). The multiplication order is that of a right action.

Definition 1.4 (The actual whole-face pairing).

Lean statement: D5/S3/Geometry/Hyperideal/NoncommutativeCornerOrbits.facePair

Formalization. D5/S3/Geometry/Hyperideal/NoncommutativeCornerOrbits.facePair (✓ std3).

Source. Repository-derived.

Commentary.

For arbitrary u,v in G, the face pairing sends (x,0) to (act(x,u),3), (x,1) to (act(x,v),2), (x,2) to (act(x,v inverse),1), and (x,3) to (act(x,u inverse),0).

Definition 1.5 (The actual corner slot maps).

Lean statement: D5/S3/Geometry/Hyperideal/NoncommutativeCornerOrbits.slotMap

Formalization. D5/S3/Geometry/Hyperideal/NoncommutativeCornerOrbits.slotMap (✓ std3).

Source. Repository-derived.

Commentary.

For omitted faces 0,1,2,3, respectively, the permutations of the three increasing corner slots are [0,1,2], [2,0,1], [1,2,0], and [0,1,2]. The displayed nonidentity maps are inverse to one another.

Definition 1.6 (A whole-face Pairing in the existing interface).

Lean statement: D5/S3/Geometry/Hyperideal/NoncommutativeCornerOrbits.pairing

Formalization. D5/S3/Geometry/Hyperideal/NoncommutativeCornerOrbits.pairing (✓ std3).

Source. Repository-derived.

Commentary.

For any u,v in G, the whole-face table and slot maps form ActualCornerTransport.Pairing Omega. The face involution is fixed point free because the omitted-face labels change. Its corner-slot maps obey the required inverse compatibility. No freeness, finiteness, transitivity or generation assumption is required.

Definition 1.7 (The representative sheet of a corner).

Lean statement: D5/S3/Geometry/Hyperideal/NoncommutativeCornerOrbits.normalize

Formalization. D5/S3/Geometry/Hyperideal/NoncommutativeCornerOrbits.normalize (✓ std3).

Source. Repository-derived.

Commentary.

For u in G and an actual corner c=(x,j), normalize(u,c)=act(x,u to the natural power j.val). This is a sheet in Omega, not a new definition of the actual corner equivalence relation.

Definition 1.8 (The first boundary return word).

Lean statement: D5/S3/Geometry/Hyperideal/NoncommutativeCornerOrbits.sWord

Formalization. D5/S3/Geometry/Hyperideal/NoncommutativeCornerOrbits.sWord (✓ std3).

Source. Repository-derived.

Commentary.

For u,v in G, sWord(u,v)=(u squared) inverse times v.

Definition 1.9 (The second boundary return word).

Lean statement: D5/S3/Geometry/Hyperideal/NoncommutativeCornerOrbits.tWord

Formalization. D5/S3/Geometry/Hyperideal/NoncommutativeCornerOrbits.tWord (✓ std3).

Source. Repository-derived.

Commentary.

For u,v in G, tWord(u,v)=(u cubed) inverse times v times u, in this order.

Definition 1.10 (The third boundary return word).

Lean statement: D5/S3/Geometry/Hyperideal/NoncommutativeCornerOrbits.kWord

Formalization. D5/S3/Geometry/Hyperideal/NoncommutativeCornerOrbits.kWord (✓ std3).

Source. Repository-derived.

Commentary.

For u,v in G, kWord(u,v)=v times u cubed.

Definition 1.11 (The subgroup generated by the three return words).

Lean statement: D5/S3/Geometry/Hyperideal/NoncommutativeCornerOrbits.boundaryGroup

Formalization. D5/S3/Geometry/Hyperideal/NoncommutativeCornerOrbits.boundaryGroup (✓ std3).

Source. Repository-derived.

Commentary.

For u,v in G, boundaryGroup(u,v) is Subgroup.closure of the set containing sWord(u,v), tWord(u,v) and kWord(u,v). It is the subgroup generated by these words, with no normal-closure operation.

Theorem 1.12 (The original face-slot corner step).

Proof. Machine-checked in Lean as D5/S3/Geometry/Hyperideal/NoncommutativeCornerOrbits.actual_step (✓ std3). ∎

Source. Repository-derived.

Commentary.

Here G ranges over all groups and Omega over all types equipped with a left action of the opposite group, written as a right action of G. For every u,v in G, x in Omega, f in Fin(4) and r in Fin(3), the displayed corners are related in the equivalence closure of the original cornerRel for pairing(u,v). Fin(n) means the integers from zero through n-1, and first and second denote pair projections. No finiteness, faithfulness or freeness assumption is imposed. This existing helper is now public for direct reuse by ActualLinkCornerChains.move_carrier. Its statement and proof are unchanged: each actual face slot supplies a generator of the original corner EqvGen. The affine link construction uses this exact step to preserve the same corner-class tag; no copied private proof or alternative orbit relation is introduced.

Theorem 1.13 (Actual corner equivalence is exactly the subgroup orbit relation).

Lean statement: D5/S3/Geometry/Hyperideal/NoncommutativeCornerOrbits.actual_corner_orbit_iff

Proof. Machine-checked in Lean as D5/S3/Geometry/Hyperideal/NoncommutativeCornerOrbits.actual_corner_orbit_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every group G, arbitrary type Omega with an action of the opposite group, u,v in G and actual corners c,d in Omega times Fin(4), the equivalence closure of ActualCornerTransport.cornerRel for pairing(u,v) relates c and d if and only if there exists g in boundaryGroup(u,v) with act(normalize(u,c),g)=normalize(u,d). The proof constructs actual face-slot paths from each corner to its normalized corner at vertex zero, constructs actual paths for the three subgroup generators, extends those paths over subgroup products and inverses, and proves that every original face-slot generator preserves the specified orbit relation. Empty Omega, infinite groups, nonfaithful actions and stabilizers are included. This statement supplies the corner-relation characterization only; it does not assert edge periods, Euler characteristic, surface links, manifold charts or a geometric metric.

The right-coset application takes a finite group G, elements u,v generating G, and an arbitrary subgroup C. A sheet is the right coset Cg, represented by Quotient (QuotientGroup.rightRel C), and rightMul C a sends Cg to C(ga). Thus act(act(q,a),b)=act(q,ab), implemented as a left action of the opposite group. The full G action is transitive: right multiplication by g inverse times h sends Cg to Ch. Write s=(u squared) inverse times v, t=(u cubed) inverse times v times u, k=v times u cubed, and K=boundaryGroup(u,v), the ordinary subgroup generated by s,t,k. No normality assumption on C or K is imposed.

At the sheet Cg, an element a of K fixes the sheet exactly when gag inverse belongs to C. The K stabilizer therefore consists of K intersect g inverseCg. Since G is finite, orbit-stabilizer gives the cardinality of {C(ga) : a in K} as [K : K intersect g inverseCg]. In Lean the conjugate subgroup is C.comap (MulAut.conj g).toMonoidHom, because MulAut.conj g sends a to ga*g inverse; the displayed cardinality is (K intersect C.comap (MulAut.conj g).toMonoidHom).relIndex K. Transitivity of the full G action does not by itself imply transitivity of this restricted K action.

Two sheets Cg and Ch lie in the same K orbit exactly when h=cga for some c in C and a in K, equivalently when g and h represent the same double coset in C\G/K. Applying actual_corner_orbit_iff to the original face-slot relation first normalizes the actual corner (Cg,i) to C(gu to the natural power i.val). Consequently (Cg,i) and (Ch,j) are related by the original corner EqvGen exactly when gu to the natural power i.val and hu to the natural power j.val lie in the same C-K double coset: hu to the natural power j.val=c*(g*u to the natural power i.val)*a for some c in C and a in K. This identifies the actual corner classes with the double-coset classes using their normalized representatives.

The regular SL(2,F_5) application takes u=[[0,1],[4,1]] and v=[[1,1],[0,1]]. The low return v inverse times u squared is [[0,1],[4,0]], and the high return v squared times u is [[3,3],[4,1]]. Their squares and cubes, respectively, are minus the identity and the identity. The high return is nonidentity, so the return orders are four and three. Also u cubed is minus the identity, v to the fifth power is the identity and v is nonidentity, and u*v is the low return.

The powers of v give every upper transvection over F_5. Conjugating the upper transvection with parameter minus c by the low return gives the lower transvection with parameter c. Matrix.SL2.transvection_induction therefore puts every determinant-one matrix in the subgroup generated by u and v. This group has 120 elements: its first column has 24 nonzero choices, and each first column admits five second columns with determinant one.

For these same matrices, write s=(u squared) inverse times v and k=v times u cubed, using the actual sWord and kWord. The identities s squared times k=v and s inverse times v inverse=u show that boundaryGroup contains both original generators. Since boundaryGroup is the subgroup generated by sWord, tWord and kWord, it equals the entire SL(2,F_5).

In a field of characteristic different from two, a determinant-one two-by-two matrix A with A squared equal to the identity is either the identity or minus the identity. Indeed A inverse=A, while the explicit inverse interchanges the diagonal entries and negates the off-diagonal entries. Thus the diagonal entries agree, the off-diagonal entries vanish, and the determinant forces the diagonal scalar to have square one. In SL(2,F_5), minus the identity is nonidentity and has order two.

Matrix.SpecialLinearGroup.mem_center_iff identifies the center of SL(2,F_5) with the identity and minus the identity. If the image of an arbitrary A in the native quotient PSL(2,F_5) is nonidentity with square one, then A squared lies in this center. A squared cannot be the identity, since the preceding classification would make A itself central. Hence A squared is minus the identity and A has order four. This conclusion applies to every lift of the given projective element.

The original whole-face table also has a literal retained-quotient interpretation for every finite sheet type Omega with a right G action and arbitrary u,v. Each raw tetrahedron consists of four nonnegative real barycentric coordinates summing to one, with every coordinate at most 3/4. At a zero coordinate, the original face involution identifies the two points by the corresponding affine permutation of all four coordinates. The quotient carries the topology induced by this same generated raw relation. Converting the increasing face-slot order to the opposite-vertex order uses the existing chi permutations; this conversion preserves the stated facePair and slotMap corner data.

For these same raw face maps, the directed local edges have a Boolean orientation preserved across every allowed face transition and reversed when the two edge endpoints are exchanged. Consequently no chain of original face transitions reverses an ordered edge. This argument applies to arbitrary actions, including actions with stabilizers and nonfaithful actions; generation and transitivity are not needed for this no-reversal conclusion.

The original finite raw-pairing chart construction therefore applies to each such retained quotient. In its inherited quotient topology it is compact, Hausdorff and second countable, with boundary-adapted three-dimensional half-space charts. In every chart, a point has zero boundary coordinate exactly when it belongs to the actual image of the cap faces, where one original barycentric coordinate equals 3/4. The empty sheet type is allowed, giving the empty quotient.

This application establishes the topological chart structure of the original finite group-action quotients. Connectedness from a specified transitive action, three-dimensional orientation, actual return-cycle degrees, the topology and genus of each individual link component, and a physical hyperbolic realization require their corresponding additional arguments.

These algebraic relations supply the marked matrices, generation, central-lift orders and the actual corner return subgroup. Geometric realization, actual edge-cycle degrees, link-surface counts and genus require their corresponding face-pairing and topology arguments.

References