Skeletal admissible index (Stage B, work order B1)

This is the skeletal-transport layer for the candidate group Γ_A. It is pure finite-group theory — no ProfiniteGrp yet.

AdmissibleIndex packages a concrete admissible marked finite group whose carrier is the skeleton Fin n. Pinning the carrier to Fin n keeps the eventual index diagram small (no universe/smallness pain when forming the category-theoretic limit later). An arbitrary finite admissible group is mapped into this skeleton by skeletalize, which transports G's group structure onto Fin (Nat.card G) along the bijection Finite.equivFin.

The transport is justified by admissible_transport_iff: admissibility is invariant under a multiplicative equivalence, because such an equivalence is surjective in both directions and admissibility transports along surjections (admissible_map_surjective, from Foundation/Admissible.lean).

structure Q2Presentation.AdmissibleIndex : Type

A concrete admissible marked finite group with carrier the skeleton Fin n.

Fixing the carrier to Fin n (rather than an arbitrary finite type) keeps the index category used to build Γ_A small. The fields are the size n, a proof that the carrier is nonempty (0 < n), the group structure groupFin, the marking q, and a proof that q is Admissible for that structure.

• n : ℕ

  Cardinality of the skeletal carrier.

• hn : Fact (0 < self.n)

  The carrier is nonempty: Fin n carries a group, so 0 < n.

• groupFin : Group (Fin self.n)

  The group structure on the skeletal carrier Fin n.

• q : Gen → Fin self.n

  The marking of the four generators.

• admissible : Admissible self.q

  q is admissible for groupFin.

def Q2Presentation.transportMarking {G : Type u_1} {H : Type u_2} [Group G] [Group H] (e : G ≃* H) (q : Marking G) : Marking H

Transport a marking along a multiplicative equivalence e : G ≃* H: post-compose each marked generator with e.

Equations

• Q2Presentation.transportMarking e q a = e (q a)

theorem Q2Presentation.admissible_transport_iff {G : Type u_1} {H : Type u_2} [Group G] [Finite G] [Group H] [Finite H] (e : G ≃* H) (q : Marking G) : Admissible (transportMarking e q) ↔ Admissible q

Admissibility is invariant under a multiplicative equivalence.

A MulEquiv is surjective in both directions, so admissibility transports along it both ways via admissible_map_surjective: forwards through e.symm (which cancels e on the nose), backwards through e itself.

noncomputable def Q2Presentation.skeletalize (G : Type u_1) [Group G] [Finite G] [Nonempty G] (q : Marking G) (h : Admissible q) : AdmissibleIndex

Skeletalization. Any admissible marking of an arbitrary nonempty finite group G is realised by an AdmissibleIndex on Fin (Nat.card G).

Transport-of-structure: the bijection e : G ≃ Fin (Nat.card G) (from Finite) induces a Group (Fin (Nat.card G)) via Equiv.group e.symm and a matching MulEquiv via Equiv.mulEquiv e.symm (both use the same transferred multiplication Equiv.mul e.symm, so they are definitionally compatible). Pushing q across that MulEquiv and invoking admissible_transport_iff supplies the admissibility proof.

Equations

• One or more equations did not get rendered due to their size.