The admissible index category and its cofilteredness (Stage B, work order B2)

This file upgrades AdmissibleIndex (the skeletal admissible marked finite groups of Candidate/AdmissibleIndex.lean) to a category whose morphisms are the generator-preserving group homomorphisms, and proves that category is cofiltered.

Cofilteredness is the Lean form of manuscript Lemma 2.1 (finite subdirect closure) and Lemma 2.2 (cofinality): every finite diagram in AdmissibleIndex has a cone, built from the single uniform subdirect construction admissible_subdirect. Two structural facts make this clean:

• Hom uniqueness (admissibleHom_ext): a morphism is pinned by its action on the marking, and the marking generates the source (AdmissibleIndex.admissible.1 : generates A.q), so any two parallel arrows coincide. The index category has no nontrivial parallel-arrow coherence — equalizers are free, and the cone_maps half of cofilteredness is trivial.
• Binary cones (subdirectObj): the skeletalized diagonal subdirect quotient of the family ![A, B] admits coordinate projections to A and B.

GammaA is built (in B3) as the cofiltered limit of this category.

Instance gotcha (inherited from AdmissibleIndex.lean)

Fin n carries the global Fin.instMul (mod-n multiplication), which is not definitionally equal to the group multiplication transported by skeletalize. Whenever a Group/Mul (Fin n) is needed we thread the bundled AdmissibleIndex.groupFin explicitly (@, projection access) so Fin.instMul is never synthesized — otherwise instance synthesis reports a non-defeq clash and the elaborator stalls on isDefEq heartbeats.

structure Q2Presentation.AdmissibleHom (A B : AdmissibleIndex) : Type

A generator-preserving morphism of admissible indices: a homomorphism of the skeletal carriers that intertwines the two markings.

• toMonoidHom : Fin A.n →* Fin B.n

  The underlying homomorphism of skeletal carriers.

• map_q (a : Gen) : self.toMonoidHom (A.q a) = B.q a

  Marking preservation.

theorem Q2Presentation.AdmissibleHom.ext' {A B : AdmissibleIndex} {f g : AdmissibleHom A B} (h : f.toMonoidHom = g.toMonoidHom) : f = g

Two admissible homs are equal once their underlying homomorphisms agree (the marking-preservation field is a proposition).

theorem Q2Presentation.AdmissibleHom.ext'_iff {A B : AdmissibleIndex} {f g : AdmissibleHom A B} : f = g ↔ f.toMonoidHom = g.toMonoidHom

def Q2Presentation.AdmissibleHom.id (A : AdmissibleIndex) : AdmissibleHom A A

The identity admissible hom.

Equations

• Q2Presentation.AdmissibleHom.id A = { toMonoidHom := MonoidHom.id (Fin A.n), map_q := ⋯ }

def Q2Presentation.AdmissibleHom.comp {A B C : AdmissibleIndex} (f : AdmissibleHom A B) (g : AdmissibleHom B C) : AdmissibleHom A C

Composition: comp f g first applies f, then g.

Equations

• f.comp g = { toMonoidHom := g.toMonoidHom.comp f.toMonoidHom, map_q := ⋯ }

instance Q2Presentation.instCategoryAdmissibleIndex : CategoryTheory.Category.{0, 0} AdmissibleIndex

The admissible index category: objects are admissible indices, morphisms are generator-preserving homomorphisms.

Equations

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

theorem Q2Presentation.admissibleHom_ext {A B : AdmissibleIndex} (f g : A ⟶ B) : f = g

Uniqueness of admissible morphisms. Both maps send the marking A.q to the same values (B.q, by map_q), and A.q generates A (A.admissible.1), so they agree on a generating set and hence everywhere (MonoidHom.eq_of_eqOn_dense). Consequently the index category has no nontrivial parallel arrows.

Nonemptiness: the trivial admissible quotient

theorem Q2Presentation.admissible_trivial : Admissible fun (x : Gen) => 1

The trivial group is admissibly marked: generation is automatic in a subsingleton group, both relators evaluate into a subsingleton (so equal 1), and the two wild generators are 1 ∈ O₂.

noncomputable def Q2Presentation.trivialIndex : AdmissibleIndex

The trivial admissible index (carrier Fin 1), witnessing nonemptiness of the index category. Built by skeletalizing the trivial group PUnit, so its group structure is the transported one (never Fin.instMul).

Equations

• Q2Presentation.trivialIndex = Q2Presentation.skeletalize PUnit.{1} (fun (x : Q2Presentation.Gen) => 1) Q2Presentation.admissible_trivial

instance Q2Presentation.instNonemptyAdmissibleIndex : Nonempty AdmissibleIndex

Transporting homomorphisms out of a skeletalization

A morphism out of a skeletalized object is built from a marking-preserving homomorphism out of the original group G, precomposed with the transport equivalence Fin (skeletalize G q h).n ≃* G. The group instance on the skeleton is threaded explicitly so the global Fin.instMul is never synthesized.

noncomputable def Q2Presentation.skelEquiv (G : Type u_1) [Group G] [Finite G] [Nonempty G] (q : Marking G) (h : Admissible q) : Fin (skeletalize G q h).n ≃* G

The transport equivalence underlying skeletalize, as a MulEquiv Fin (skeletalize G q h).n ≃* G. Its multiplication on the skeleton side is forced to be skeletalize's transported one (no Fin.instMul).

Equations

• Q2Presentation.skelEquiv G q h = (Finite.equivFin G).symm.mulEquiv

@[simp]

theorem Q2Presentation.skelEquiv_q {G : Type u_1} [Group G] [Finite G] [Nonempty G] {q : Marking G} {h : Admissible q} (a : Gen) : (skelEquiv G q h) ((skeletalize G q h).q a) = q a

noncomputable def Q2Presentation.skeletalizeHomOut {G : Type u_1} [Group G] [Finite G] [Nonempty G] {q : Marking G} {h : Admissible q} {D : AdmissibleIndex} (ψ : G →* Fin D.n) (hψ : ∀ (a : Gen), ψ (q a) = D.q a) : AdmissibleHom (skeletalize G q h) D

A marking-preserving homomorphism ψ : G →* Fin D.n out of G induces an admissible morphism skeletalize G q h ⟶ D, by precomposing with the transport skelEquiv.

Equations

• Q2Presentation.skeletalizeHomOut ψ hψ = { toMonoidHom := ψ.comp (Q2Presentation.skelEquiv G q h).toMonoidHom, map_q := ⋯ }

Binary subdirect objects

noncomputable def Q2Presentation.subdirectObj (A B : AdmissibleIndex) : AdmissibleIndex

The binary subdirect object of A and B: skeletalize the diagonal subdirect quotient of the two-object family ![A, B] (manuscript Lemma 2.1 with ι = Fin 2).

Equations

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

noncomputable def Q2Presentation.subdirectFst (A B : AdmissibleIndex) : subdirectObj A B ⟶ A

First coordinate projection subdirectObj A B ⟶ A (evaluation at index 0, where ![A, B] 0 is A).

Equations

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

noncomputable def Q2Presentation.subdirectSnd (A B : AdmissibleIndex) : subdirectObj A B ⟶ B

Second coordinate projection subdirectObj A B ⟶ B (evaluation at index 1, where ![A, B] 1 is B).

Equations

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

Cofilteredness

instance Q2Presentation.admissibleIndex_isCofiltered : CategoryTheory.IsCofiltered AdmissibleIndex

The admissible index category is cofiltered (the Lean form of manuscript Lemma 2.1 + Lemma 2.2). Binary cones are the subdirect objects subdirectObj; the cone_maps (equalizer) half is automatic because any two parallel arrows are equal (admissibleHom_ext); nonemptiness is the trivial admissible quotient.

Acceptance checks