Observer-Type Irreplaceability for A5

Abstract

A5 is invisible to every finite p-group observer but has a faithful characteristic-five linear observer.

Theorem 1.1 (Prime-power quotient and residue-linear observers are not interchangeable).

$$\begin{gathered} \exists G:\mathrm{Type},[\mathrm{Group}(G)],[\mathrm{Finite}(G)],\mathrm{Nonempty}(\mathrm{GroupIso}(G,A_5))\wedge \\ (\forall p:\mathbb{N},\mathrm{Prime}(p)\Rightarrow \forall P:\mathrm{Type},[\mathrm{Group}(P)],[\mathrm{Finite}(P)],\mathrm{IsPGroup}(p,P)\Rightarrow \forall q\in \mathrm{Hom}(G,P),\neg \mathrm{Injective}(q))\wedge \\ (\exists V:\mathrm{Type},[\mathrm{AddCommGroup}(V)],[\mathrm{Module}(\mathrm{ZMod}(5),V)],\exists \rho \in \mathrm{Hom}(G,\mathrm{GL}(\mathrm{ZMod}(5),V)),\mathrm{Injective}(\rho ))\wedge \\ (\exists o_q,o_{\rho }\in \mathrm{LocalObserverAtPrime}(5,G),\mathrm{Kind}(o_q)=PrimePowerQuotient\wedge \mathrm{Kind}(o_{\rho })=ResidueLinear\wedge \mathrm{Kind}(o_q)\ne \mathrm{Kind}(o_{\rho })\wedge \neg \mathrm{Faithful}(o_q)\wedge \mathrm{Faithful}(o_{\rho })). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Factorization/ObserverTypes/AlternatingFiveObserverTypeIrreplaceability.alternating_five_observer_type_irreplaceability (✓ std3). ∎

Source. Repository-derived.

Commentary.

There is a finite group G isomorphic to A5 such that, for every prime p, every finite p-group P, and every homomorphism from G to P, the homomorphism is noninjective. This universal clause is inherited from the repository theorem that all such homomorphisms are trivial.

For the same group G there is a module V over Z/5Z and an injective homomorphism from G to the general linear group of V. The witness is the left regular representation, so the existential observer is constructed rather than postulated.

At the single prime 5, these witnesses are also objects of one common fixed-prime observer category. Their kinds are distinct and their fidelity is opposite, so local observation at one prime is not a single interchangeable notion.

References

• Truth anchor: D5/S3/Factorization/ObserverTypes/AlternatingFiveObserverTypeIrreplaceability.alternating_five_observer_type_irreplaceability
• Dependency: D5/S3/Factorization/PrimePowers/SimpleToPGroupTrivial