Compatible carriers and finite Frobenius separation

One useful completion mechanism is available when the desired packet already occurs as a semisimple summand of a known compatible carrier.

Permalink · Source line 1049

Characteristic-zero independence is now Lean-checked for actual finite-dimensional irreducible representations of arbitrary monoids. Finiteness of the group and algebraic closedness of the field are not needed for this result. The proof uses the actual monoid algebra and Jacobson density to select constituent actions. Jointly continuous coordinate actions have continuous characters. Coverage in every open normal quotient of a compact totally disconnected group implies density of the conjugacy-saturated samples and hence the finite separator. General arithmetic Frobenius coverage remains unformalized. Block 25 now proves the bridge from componentwise nonisomorphic systems to nonisomorphic members at the selected coefficient prime, under density on the required good-place overlaps. It also proves the complete restricted separator for a fixed finite cyclotomic Galois group over \({\mathbf Q}\), with arithmetic coverage derived from the proved Dirichlet theorem. The full arithmetic theorem remains partial. Selection is existential and gives no effective upper bound on the selected primes. A common algebraic matrix is still distinct from an ordinary unramified trace comparison at all coefficient primes simultaneously.

Permalink · Source line 1085

The system equivalence used here is componentwise representation isomorphism:

For finite-dimensional irreducible representations of any monoid over a characteristic-zero field, the new character-rigidity theorem proves that equality of characters is equivalent to an actual equivariant linear isomorphism. Neither a finite group nor an algebraically closed coefficient field is needed.

Suppose two members are isomorphic at \(\lambda_0\). Injectivity of the common coefficient embedding gives \(t_i(v)=t_j(v)\) at every place good for \(\lambda_0\). At another coefficient prime \(\lambda\), this equality compares actual member traces on the intersection of the two good-place sets. Conjugacy density of that intersection and continuity extend the equality to the whole group; character rigidity then gives an actual isomorphism at \(\lambda\). Thus the nonisomorphism of systems supplies the required nonisomorphism of members. Equality of optional labels or record fields is not used as a substitute for representation equivalence.

The generic separator now derives this bridge and permits any additional finite set of excluded places. Its coverage premise retains every finite deletion: for each finite excluded set and each open normal quotient, every quotient class contains a conjugate of an allowed sample. This implies density on each pair of cofinite good-place sets; no all-coefficient-prime common ordinary-trace domain is assumed.

Permalink · Source line 1103

Let \(n>0\) and let \(L={\mathbf Q}(\zeta_n)\) be a cyclotomic number field. The canonical isomorphism

defines \(\sigma_p\) by \(\sigma_p(\zeta_n)=\zeta_n^p\) when \(p\nmid n\). For every automorphism \(\sigma\), finite set \(B\subset\mathbb N\) and bound \(b\), Lean proves that there is a rational prime \(p>b\), with \(p\notin B\) and \(p\nmid n\), such that \(\sigma_p=\sigma\). The prime-existence step uses the proved Dirichlet theorem in the pinned Mathlib dependency.

The arithmetic attachment is checked in this finite cyclotomic case. There is an actual maximal prime \(\mathfrak P\) of \(\mathcal O_L\) above \((p)\), its ramification index is one, and \(\sigma_p\) belongs to its decomposition group. For every integral \(x\in\mathcal O_L\),

The residue identity is proved on all integral elements using \(\mathcal O_L=\mathbb Z[\zeta_n]\). Existence of \(\mathfrak P\) is obtained by lying over, rather than assumed. This specifies arithmetic Frobenius, with \(p\)-power residue action. The action and unramifiedness statements also hold for every maximal prime above the selected \(p\).

Consequently, for pairwise componentwise nonisomorphic compatible irreducible representation families of this fixed finite Galois group, the common algebraic trace matrix can be selected at distinct rational primes outside any prescribed finite set, with nonzero determinant. Every coefficient embedding preserves its nonvanishing; actual member trace comparisons retain that member's good-prime condition. No coverage or character-continuity hypothesis is added in this cyclotomic specialization: the prime coverage is proved, and the finite extension's Krull topology is discrete. A concrete conductor-four instance uses the actual field \({\mathbf Q}(\zeta_4)\).

This is a complete restricted arithmetic case of Claim 9.1. It does not establish coverage in arbitrary finite quotients of the absolute Galois group, nor the Hodge–Tate and Weil–Deligne comparisons of Claim 9.2. The source-claim ledger therefore remains seventeen checked and three partial.

Permalink · Source line 1132

Fix a cyclotomic number field \(L={\mathbf Q}(\zeta_n)\) with \(n>0\) and an embedding \(j:L\hookrightarrow\overline{{\mathbf Q}}\). The new restriction map

is an actual continuous surjective homomorphism with open kernel. Surjectivity is derived by extending automorphisms to the algebraic closure. Pullback along a surjective homomorphism preserves and reflects equivariant linear isomorphisms, invariant subspaces, and irreducibility. These assertions keep the underlying linear maps and submodules and do not assume a finite acting group. In particular, the equivalence relation for systems is preserved and reflected componentwise.

The arithmetic witnesses use the integral closure \(\mathcal A\) of \(\mathbb Z\) in \(\overline{{\mathbf Q}}\). For each rational prime \(p\), Lean constructs a maximal ideal \(\mathfrak Q\) of \(\mathcal A\) above \((p)\) and an actual element \(\gamma_p\in G_{{\mathbf Q}}\) such that

The existence argument applies Mathlib's proved profinite stabilizer-surjectivity theorem to this actual invariant ring. The residue \(p\)-power map is proved bijective by taking \(p\)-th roots in \(\overline{{\mathbf Q}}\) and showing that they remain integral when their \(p\)-th powers are integral. This constructs an arithmetic Frobenius witness in the prime-ideal decomposition group; it does not assert that an arbitrary global lift belongs to that group.

When \(p\nmid n\), the comparison with the finite cyclotomic sample is proved:

Reduction distinguishes \(n\)-th roots of unity at such a prime. Indeed, if \(x^n=y^n=1\) and their reductions agree, the factorization of \(x^n-y^n\) gives

The second factor reduces to \(n\overline y^{\,n-1}\ne0\), so the domain property gives \(x=y\). This proves both Frobenius recognition on the cyclotomic generator and triviality of its inertia action. Consequently, every representation pulled back through \(q_L\) is unramified there.

The valuation formulation is checked separately. For any valuation subring \(A\subset\overline{{\mathbf Q}}\) with residue characteristic \(p\nmid n\), its actual residue-action kernel fixes every \(n\)-th root of unity. A supplied element of its decomposition subgroup with \(p\)-power residue action restricts to \(\sigma_p\). These statements use Mathlib's valuation inertia and decomposition subgroups. No identification of the valuation and integral-closure prime models is assumed in the formal comparison.

For a compatible family \(\rho_{i,\lambda}\) of representations of the fixed finite group, set \(V_{i,\lambda}=\rho_{i,\lambda}\circ q_L\). Suppose the actual absolute-Galois members are irreducible and the systems are pairwise componentwise nonisomorphic. The finite prime separator now yields distinct permitted rational primes \(p_j\), actual prime ideals \(\mathfrak Q_j\) and arithmetic Frobenius witnesses \(\gamma_j\) as above, outside any prescribed finite set, such that the common algebraic trace matrix has nonzero determinant. Every coefficient embedding preserves this nonvanishing, and

whenever \(p_j\) is good for that coefficient member. The operator and trace values agree for every global lift with the same cyclotomic restriction. Neither Frobenius-witness existence nor quotient coverage is a supplied hypothesis in this restricted arithmetic theorem. The common cyclotomic factorization and the compatible trace data remain explicit hypotheses.

This completes the passage to actual absolute-Galois Frobenius witnesses for the fixed cyclotomic class. It does not establish prime coverage for arbitrary finite Galois extensions. Claim 9.1 therefore remains partial, and the source ledger remains seventeen checked and three partial.

The boundaries are formalized as well. Pullback along a nonsurjective homomorphism can make inequivalent irreducible representations isomorphic. Samples can cover one quotient while missing an open quotient of the full group. Finally, in \(\mathbb Z_2\), the distinct square roots \(1\) and \(-1\) have the same residue, so the condition that the root order be a unit cannot be discarded.

Permalink · Source line 1173

Let \(L/{\mathbf Q}\) now be any finite normal number field, with a chosen embedding \(j:L\hookrightarrow\overline{{\mathbf Q}}\). Write \(\mathcal A\) for the integral closure of \(\mathbb Z\) in \(\overline{{\mathbf Q}}\). The embedding restricts to an injective map \(\mathcal O_L\to\mathcal A\) which intertwines the actual Galois actions. If \(\mathfrak Q\subset\mathcal A\) is maximal above \((p)\), its contraction \(\mathfrak P\subset\mathcal O_L\) is a nonzero maximal ideal above \((p)\), and the induced residue map is injective.

Restriction carries the actual decomposition group at \(\mathfrak Q\) into that at \(\mathfrak P\), carries ideal inertia into ideal inertia, and preserves the arithmetic \(p\)-power residue action. Thus the absolute Frobenius constructed in Block 26 gives a simultaneous finite Frobenius at the contracted prime. This assertion applies to arbitrary finite normal number fields and does not require a cyclotomic generator.

The exceptional primes are controlled by the actual field discriminant:

This set is finite. For \(p\notin S_L\), every prime of \(\mathcal O_L\) above \((p)\) is unramified. Lean proves that the actual inertia cardinality is the ramification index. It follows that inertia is trivial and the arithmetic Frobenius at a fixed finite prime is unique as a field automorphism. Neither trivial inertia nor uniqueness is assumed in place of the arithmetic unramifiedness condition.

The choice of absolute prime and Frobenius lift is also controlled. Let \((\mathfrak Q_u,\gamma_u)\) and \((\mathfrak Q_v,\gamma_v)\) be any two actual arithmetic witnesses at the same rational prime. Transitivity on primes of \(\mathcal A\) above \((p)\) gives \(a\in G_{{\mathbf Q}}\) with

Consequently, any representation trivial on \(I_{\mathfrak Q_v}\) has the same trace on the two witnesses. For representations factoring through \(L\), triviality on this actual absolute inertia is derived whenever \(p\notin S_L\). The restrictions of all absolute witnesses at such a prime therefore form a single conjugacy class. This conclusion requires only the indicated finite factorization and the discriminant exclusion.

There is a final compatibility between embeddings. For a normal subfield \(L\subset\overline{{\mathbf Q}}\), restriction defined through a chosen embedding is conjugate to canonical restriction by one fixed automorphism of \(L\). This identifies their conjugacy classes and lets the arithmetic comparison apply directly to the fixed fields of open normal subgroups of \(G_{{\mathbf Q}}\). Those fixed fields are proved to be finite Galois number fields, with the original open normal subgroup as the kernel of restriction.

The remaining prime-existence obligation now has a precise formulation. For every finite Galois subfield \(L\), every finite set \(B\) of rational primes, and every \(\sigma\in\operatorname{Gal}(L/{\mathbf Q})\), require a prime \(p\notin B\cup S_L\) and an actual absolute arithmetic witness \(\gamma_p\) such that

Lean proves that this assertion is equivalent to the cofinite quotient coverage required by the general separator, for any fixed choice of actual Frobenius witnesses. The equivalence derives independence from the witness choices; it does not supply the displayed prime-existence assertion. Arbitrary finite exclusions absorb \(S_L\), and the resulting conditional density theorem preserves the separate good-prime sets of coefficient members. General prime coverage remains unproved, so Claim 9.1 remains partial. The source ledger is still seventeen checked and three partial. This new arithmetic interface has base \({\mathbf Q}\). For the source's general-base instances involving \(G_{F,S}\), the analogous actual-prime and norm-power Frobenius attachment and coverage over \(F\), or a proved transfer to the rational-base result, also remain necessary.

Permalink · Source line 1257

In the actual discrete group \(C_2=\{1,a\}\), set \(s(0)=a\) and \(s(m+1)=1\). The original samples are surjective and satisfy quotient coverage. Removing index zero leaves only the identity, so both density and quotient coverage fail. The actual rational sign and trivial characters agree on the remaining samples but differ globally. This checked example explains why ordinary coverage alone cannot justify deleting the bad places in the system comparison.

Permalink · Source line 1328

For a certified square separator the coefficient vector is \(C^{-1}t\). This is a valid carrier multiplicity vector only when every entry is a nonnegative integer and satisfies its capacity bound \(m_i\le c_i\). Those tests and uniqueness of natural multiplicities in characteristic zero are separately Lean-checked, as is transport through a field embedding. Reduction modulo a residue characteristic is not a field embedding and may lose rank. The representation construction and common-polynomial part are now Lean-checked as described below. The full strictly compatible arithmetic statement, including its local conditions, remains partially formalized.

Permalink · Source line 1369

Claim 9.2 supplies the compatible carrier, its decomposition, and the compatible constituent systems. Constructing unknown such objects is not required by that conditional theorem. The remaining formal obligation is that finite sums preserve the intended actual local arithmetic structures, together with the arithmetic separator input. The algebraic monodromy results below do not by themselves identify attached Weil–Deligne representations or Hodge–Tate comparison data.

Permalink · Source line 1380

Let \(K\) be a field, let \(G\) be a monoid, and let \(\rho_i:G\to\operatorname{End}_K(W_i)\) be actual representations on finite-dimensional spaces, indexed by a finite set \(I\). For natural numbers \(m_i\le c_i\), set

These finite products realize the corresponding finite direct sums. The representation on \(U_m\) acts componentwise. Define \(j:U_m\to U_c\) by retaining the first \(m_i\) copies and filling every remaining coordinate with zero. Define \(r:U_c\to U_m\) by restriction to the selected copies. Lean proves

The image of \(j\) is exactly the subspace whose unused coordinates vanish. Consequently \(jr\) is an equivariant idempotent. A supplied equivariant isomorphism \(D:W\xrightarrow{\sim}U_c\) gives the split maps \(D^{-1}j\) and \(rD\) inside the original carrier. The decomposition \(D\) is an input; these statements do not construct a decomposition of an unknown arithmetic carrier.

The same formalization proves, for each \(g\in G\),

Constituents may have different dimensions. Zero multiplicities, zero-dimensional constituents, and the empty index set are included. If at a permitted sample \(g\) the constituent polynomials are the images of \(P_{i,g}\in E[X]\) under a specified map \(E\to K\), the summand polynomial is the image of \(\prod_iP_{i,g}^{m_i}\). Applying this independently at each coefficient field preserves a supplied common polynomial family. This does not establish the Hodge–Tate or Weil–Deligne conditions in strict compatibility.

Joint continuity of the constituent actions implies joint continuity of the constructed action. The inclusion and retraction are continuous for the product topologies, and triviality on a supplied subgroup is preserved. Neither continuity nor triviality is inferred for a carrier whose corresponding hypothesis has not been supplied. The maps transported by \(D\) are proved algebraically; their topological interpretation additionally requires the appropriate continuity of \(D\) and its inverse.

For the three-character example below, the construction produces an actual three-dimensional summand inside the carrier of dimension seven. At the sample \((0,1)\) its characteristic polynomial is \((X-1)^2(X+1)\). A separate checked counterexample uses the coordinate inclusion \(\mathbf Q\to\mathbf Q^2\), its coordinate retraction, and the swap involution: the split law holds, but compression sends the swap to zero and therefore fails to preserve its square. Thus selecting whole constituent copies, with the proved equivariance, is essential to this construction.

Permalink · Source line 1388

Fix a field \(K\) and a nonzero scalar \(q\in K^\times\). On each constituent \(W_i\), supply an automorphism \(F_i\) and a nilpotent endomorphism \(N_i\) with \(F_iN_iF_i^{-1}=qN_i\). The scalar \(q\) is common to this finite family. The componentwise operators \(F_m,N_m\) on \(U_m\) satisfy the same relation; \(F_m\) is invertible and \(N_m\) is nilpotent. The split maps constructed above intertwine both operators. The proof first identifies the independently defined kernel through an equivariant linear isomorphism

The relation, with \(q\ne0\), proves that both \(F_i\) and its inverse preserve \(\ker N_i\). Thus \(F_i|_{\ker N_i}\) is an actual automorphism, and Lean proves

The corresponding kernel dimensions and traces are additive with multiplicity. Common constituent kernel polynomials, when supplied through a coefficient-ring map, give the mapped product polynomial for the summand. Whole-space Frobenius polynomials are not substituted for these kernel polynomials.

The exact special chain has basis \(e_0,\ldots,e_{n-1}\) and operators

Lean proves \(N^n=0\), and for \(n>0\) also \(N^{n-1}\ne0\) and \(\ker N=Ke_0\). Consequently its kernel polynomial is \(X-a\), whereas its whole-space polynomial is \(\prod_{j=0}^{n-1}(X-aq^{-j})\). The zero-length chain is included as a zero-dimensional space; the assertion \(\ker N=Ke_0\) is made only for positive length.

For \(n>1\), replacing \(N\) by zero retains exactly the same \(F\) and the same whole-space characteristic polynomial, while changing the degree of the kernel polynomial from one to \(n\). Both pairs still satisfy the algebraic monodromy relation. This Lean-checked example shows that whole Frobenius data alone do not determine the monodromy kernel polynomial. It is not asserted to be a counterexample among the intended strictly compatible arithmetic systems.

These statements concern supplied algebraic pairs. No Weil-group or inertia action, Hodge–Tate object, arithmetic comparison, or realization of the pair from a Galois representation is constructed here. The polynomial convention is \(\det(XI-F|_{\ker N})\); no identification with an inertia-dependent local Euler factor is asserted. Claim 9.2 remains partial at its full arithmetic scope.

Permalink · Source line 1446

Let \(K\) be a field, \(G\) a group, and \(\nu:G\to K^\times\) a character. The new datum consists of an actual representation \(r\) and nilpotent \(N\) with \(r(g)N=\nu(g)Nr(g)\) for every \(g\). For a supplied subgroup \(H\), define

This is the intersection of independently defined kernel and actual invariant subspaces. For normal \(H\), the restricted whole-group representation and its inverse automorphisms are constructed. A change from \(\varphi\) to \(\varphi h\), with \(h\in H\), leaves the restricted operator itself unchanged.

For a finite family of finite-dimensional constituents and natural multiplicities, the actual local space of the constructed sum is linearly equivalent to the sum of the constituent local spaces, equivariantly for every group element. Its characteristic polynomials multiply, its dimensions and traces add, and maps intertwining both the group and \(N\) restrict to the local spaces. The explicit bounded-copy inclusion and retraction still split there. Finite inertia image and an open inertia kernel are preserved.

Writing \(Q_D(T)\) for the reversed local characteristic polynomial, Lean proves

The abstract formulas do not need characteristic zero. Normality and finite dimension appear explicitly where used. Arithmetic identification of \(G,H,\nu\) and \(\varphi\) remains separate. In the geometric-Frobenius convention, \(\nu(\varphi)\) is the inverse residue cardinality; it is this unit, rather than the residue cardinality, that enters the earlier special-chain parameter.

An explicit action of \(C_2\times\mathbb Z\) has \(\nu(\varphi)=1/3\), \(F=\operatorname{diag}(2,6,18)\) and \(Ne_1=e_0\), \(Ne_2=e_1\), \(Ne_0=0\). Trivial inertia gives local dimension one and denominator \(1-2T\); scalar sign inertia gives dimension zero and denominator one. The entire \(F\) and \(N\) are equal in these two examples, and \(N^2\ne0\). Thus inertia cannot be omitted. Conversely, unramified chains of lengths one and three have equal Euler denominators while only the first has \(N=0\). Euler factors therefore do not identify complete monodromy data.

The remaining arithmetic comparison is \(\operatorname{WD}(\bigoplus_i V_i^{\oplus m_i})\cong \bigoplus_i\operatorname{WD}(V_i)^{\oplus m_i}\) for the actual attached functor, intertwining the Weil action and monodromy, together with the intended coefficient and Hodge–Tate comparisons. These are not supplied by the abstract datum. Claim 9.2 remains partial at its full arithmetic scope.

Recovered multiplicities determine the semisimple isomorphism type relative to the specified constituents, not a canonical embedding or projector inside a repeated isotypic component. For example, the two projectors \(\operatorname{diag}(1,0)\) and \(\operatorname{diag}(0,1)\) on a two-dimensional trivial representation are distinct equivariant idempotents with trace one.

Permalink · Source line 1493

The theorem is substantial only when a suitable compatible carrier and its irreducible compatible constituents are already known. It does not assert that every geometric representation embeds into such a carrier.

Permalink · Source line 1568

Let \(K\) be a characteristic-zero field and let \((r,N)\) be supplied group data with nilpotent \(N\) and \(r(g)N=\nu(g)Nr(g)\). For a supplied scalar map satisfying

the formalization constructs

Lean proves the representation laws, actual finite-copy and split-map compatibility, and joint continuity from continuity of \(N\), \(r\) and \(t\) with the stated continuous vector-space operations. The monodromy fixed kernel intersected with subgroup invariants is unchanged by this twist. For normal inertia, its restricted action and finite-dimensional Euler denominator agree. Twisting again by \(-t\) recovers the datum with \(N\) still supplied.

Block 13 also established an extracted inverse on the explicit class \(N^3=0\):

Both exponential/logarithmic inverse identities are checked on the cubic nilpotent and unipotent loci. If a supplied common sample \(u\) has \(r_D(u)=r_E(u)=I\) and \(t(u)\ne0\), an intertwiner of the reconstructed cubic actions recovers both original group equivariance and monodromy equivariance. The general nilpotence exponential theorem is not restricted to this cubic class, but the extracted inverse in Block 13 was. Block 20 below removes that restriction by using the full finite logarithm.

The rational affine-group example has \(u=(1,1)\), \(d=(0,1/3)\) and

Reversing the factor order or dropping the quadratic term gives checked failures. For the length-four chain, the quadratic logarithm has erroneous \(e_3\)-to-\(e_0\) coefficient \(-1/3\), so its cubic restriction is substantive. A zero-parameter sample also fails to recover \(N\).

No arithmetic group, tame cocycle or required sample is constructed by these statements. The attached comparison for every intended representation, coefficient comparisons and Hodge–Tate/period data remain separate. Finite inertia image and an open inertia kernel of \(r\) are not asserted to persist under this twist to \(\rho\). Claim 9.2 remains partial.

Permalink · Source line 1572