Exercise PLAN-104

Functional equivariance does not imply linearity, even for entire maps on finite unitary irreps. Once common-field linearity is an explicit conditional premise, invariant kernel/image subspaces yield zero-or-linear-isomorphism; scalar Schur additionally needs an eigenvalue route.

1. The literal functional-equation reading is refuted by nonlinear maps on the complex sign irrep; with explicit F-linearity, kernel closure and equivariance give a G-invariant linear subspace.
2. For nonzero linear f, irreducibility forces ker(f)=0, and linear differences—not the zero fiber alone—give injectivity.
3. Linearity supplies image-subspace closure and equivariance supplies G-invariance; invariant nonlinear images need not be vector spaces.
4. Irreducibility forces a nonzero linear image to equal V_2, so the same f is surjective.
5. The inverse is F-linear and intertwines backwards, giving an algebraic representation isomorphism; zero-space and field/topology boundaries are explicit, and105 uses this as a subproof rather than an alias.

The literal functional-equation statement is false. Let G={+1,-1} with multiplication, V_1=V_2=C, and phi_i(epsilon)z=epsilon*z. This is a one-dimensional nonzero complex representation and therefore irreducible: the only complex-linear subspaces are0 and C. It is unitary; with the discrete topology G is finite and compact and its action is continuous. The map f(z)=z^3 is an entire, hence continuous, function with f(epsilon*z)=epsilon^3*z^3=epsilon*f(z), so it satisfies exactly the displayed functional equivariance. It is nonzero, but f(1)=f(omega)=1 for omega=(-1+i*sqrt(3))/2!=1 and omega^3=1. Thus it is not injective and cannot be a representation isomorphism. It is also not complex-linear: f(2)=8!=2*f(1). Continuity, holomorphicity, finite dimension and unitary irreducibility do not recover the missing linear-map hypothesis.

Two variants locate the proof failures precisely. In the same sign representation h(z)=z^3-z is equivariant and entire, but its zero fiber is{-1,0,1}; it contains1 while1+1=2 is not in it, since h(2)=6. That G-invariant zero fiber is not a vector subspace, so irreducibility cannot be applied to it. In the cube example the zero fiber happens to be{0} and its image is C, yet f is not injective: the implication ker(f)={0}=>injective uses linearity, namely f(v-w)=f(v)-f(w), and is not a set-theoretic fact.

The image-subspace assertion can also fail under an actual continuous compact-group action. Let G=U(1) act on C by u*z and let q(z)=z/(1+|z|^2). Then q(u*z)=u*q(z), q is continuous and the one-dimensional unitary representation is irreducible. Its image is the closed disk of radius1/2: r/(1+r^2) lies in[0,1/2] because (r-1)^2>=0, with equality at r1, and on r in[0,1] it continuously attains every radius in that interval. This nonzero bounded disk is not a complex vector subspace. The example is not claimed holomorphic; the finite-group polynomial examples already meet the stronger holomorphic requirement. Functional equivariance does preserve the zero fiber and image as SETS under the group action, but it does not supply their vector-space closure.

For the corrected theorem let f be F-linear over the specified common field. Its kernel K contains0; if v,w are in K and a,b in F then f(av+bw)=a f(v)+b f(w)=0, so av+bw lies in K. Its image I contains f(0)=0; if y=f(v),z=f(w), then ay+bz=f(av+bw) is again in I. These are the vector-subspace facts missing above, not consequences of equivariance alone.

Equivariance now gives f(phi_1(g)v)=phi_2(g)f(v)=0 when v is in K, since each representation operator is linear and maps0 to0. Thus K is G-invariant. Likewise phi_2(g)f(v)=f(phi_1(g)v) belongs to I, so I is G-invariant. Stability for all g, including g^(-1), also gives equality of the translated subsets if that version of invariance is used. These facts establish the actual hypotheses of algebraic irreducibility.

If f=0 the first alternative holds. Otherwise some v has f(v)!=0, so K!=V_1 and I!={0}. Irreducibility forces K={0} and I=V_2. For linear f, f(v)=f(w) implies f(v-w)=0 and hence v=w; image V_2 is surjectivity. Thus f is a bijection. If y=f(v),z=f(w), uniqueness of preimages gives f^(-1)(ay+bz)=av+bw=a f^(-1)(y)+b f^(-1)(z), proving inverse linearity. For any y=f(v), f^(-1)(phi_2(g)y)=f^(-1)(f(phi_1(g)v))=phi_1(g)v, proving f^(-1)phi_2(g)=phi_1(g)f^(-1). This is a representation isomorphism in the linear sense.

This conditional proof works over any common field, with no algebraic closure, characteristic, finite-group, finite-dimensional, unitarity, inner-product or continuity requirement. It uses algebraic irreducibility (all invariant linear subspaces), not merely absence of proper CLOSED invariant subspaces in an infinite-dimensional topology. It proves an algebraic inverse, not an extra topological inverse theorem. If either carrier is0, its only linear map to/from the other carrier is zero and the zero alternative applies. If both are0 that map is also an isomorphism, so the alternatives need not be exclusive. If irreducibility is conventionally defined only for nonzero spaces, these degenerate cases are simply outside that convention, not an eigenvector justification.

Plan105 uses this linear zero-or-isomorphism result on f-lambda*I after obtaining an eigenvalue. That is a genuine shared subproof and requires the shift itself to be linear. Classifying all commuting endomorphisms as scalars additionally needs the appropriate eigenvalue hypothesis, supplied there by nonzero finite dimension and algebraic closure. The two full targets are therefore related by a dependency, not proved aliases, and no global deduplication or new graph theorem follows from sharing the counterexample or argument.

1. Refutes functional equivariance alone using an explicit nonlinear continuous/holomorphic map on a genuine finite-group complex irreducible unitary representation; identifies invariant-subset versus linear-subspace closure and the failure of zero-fiber=>injective without linearity. (1 weight)
2. Under the QUESTION'S explicit common-field F-linearity condition, proves kernel and image vector-subspace closure and their G-invariance using the correct domain/codomain representations. (1 weight)
3. Applies algebraic irreducibility only after proving subspace hypotheses, and for nonzero f proves injectivity and surjectivity; establishes a linear, reverse-intertwining inverse rather than only a bijective function. (1 weight)
4. Correctly states the absence of algebraic-closure/characteristic/finite-group/finite-dimensional/topological requirements for this algebraic theorem, handles zero carriers if admitted, and distinguishes the shared104 lemma from105's additional eigenvalue/scalar target without changing any standing convention. (1 weight)

No aligned Lean view has been admitted for this native core in this textbook checkpoint. This is not a claim that the underlying mathematics lacks a formal proof. Contributions must preserve this exact target contract and split.

Read the Lean track and existing diagnostic warmups

• website/research/sources.json

  leditzky-2025-repth-qit

  Source SHA-256: 9f85f45f20ed5a46931ad0dec3b94ee09748bc56e39fae29b0aefe910440b0ae · MIT metadata only
• Primary source

Contract: a3065731e3b29568ab9eb2c692a90f89eb2b2c854f49ab505d8a67974a7914ff

Item digest: 13b6f669e57a3907666048faeab66a97af43cf90ecf45b4d5e283426a2bf2760

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

Authored support steps: 5. This is not measured graph distance or model difficulty.

{ "question_version": 2, "predecessor_key": "qcb-core-plan-104-schur-lemma-equivariant-zero-or-iso", "predecessor_item_digest": "d8ceef23276e205705f3522d7ecd45f9dbb7362521e202b42ef77ddf1828bfd4", "predecessor_contract_hash": "50738c89ced0281d39cb9294217c84dbd8c958ee8bf75e0ca18bd89f7b23d3d1", "current_contract_hash": "a3065731e3b29568ab9eb2c692a90f89eb2b2c854f49ab505d8a67974a7914ff", "changed_contract_fields": [ "question" ], "repair_record": "shared/repairs/plan-104-functional-equivariance-linearity-question-successor.json", "repair_record_digest": "944bf81b6986c0f9099005558126eb1e68eb45e1503176af98c5576030aeb9dc", "review_record": "reports/textbook-v1/repairs/plan-104-functional-equivariance-linearity-question-successor-review.json", "review_digest": "2c114b56905ad9222a6aaf041eac3fb459a1ee2b697ba020b4a70638330ec1e3", "equivalence_to_predecessor_claimed": false, "additional_core_count": 0 }