QuantumComputinglib learn · inspect · formalize
Checked on this commit 4,524 public declarations commit 4e2c5b2c0be5 Build record

Quantum Information / Representation Qit

Representation Qit

Exercise PLAN-101

basic · proof · test_public

primary source nl only. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.

Assumptions and conventions

      Question

      Let (G, .) and (H, *) be groups with identities e_G and e_H, and let phi: G -> H be a group homomorphism, meaning phi(x.y) = phi(x)*phi(y) for all x, y in G. Prove from the homomorphism property alone (without assuming phi is injective, surjective, or that G or H is finite) that phi(e_G) = e_H and that phi(g^{-1}) = phi(g)^{-1} for every g in G. State explicitly which group axioms (uniqueness of identity, uniqueness of inverses, cancellation) you invoke at each step, and explain why these two facts justify the standing claims that every representation phi satisfies phi(e) = 1_V and phi(g^{-1}) = phi(g)^{-1}.

      Hint: mathematical route

      A homomorphism automatically preserves the identity and inverses, which is exactly why a representation phi satisfies phi(e)=1_V and phi(g^{-1})=phi(g)^{-1} with invertibility free.

      1. Applying phi to e_G . g = g gives phi(e_G)*phi(g) = phi(g).
      2. Cancellation / uniqueness of identity in H forces phi(e_G) = e_H.
      3. Applying phi to g.g^{-1} = e_G = g^{-1}.g gives phi(g)*phi(g^{-1}) = e_H = phi(g^{-1})*phi(g).
      4. Uniqueness of inverses in H forces phi(g^{-1}) = phi(g)^{-1}.
      5. Specializing H = GL(V) yields phi(e) = 1_V and phi(g^{-1}) = phi(g)^{-1}, so each phi(g) is invertible automatically.
      Reference solution

      For the identity: pick any g in G and write g = e_G . g, so phi(g) = phi(e_G . g) = phi(e_G) * phi(g). Thus phi(e_G) * phi(g) = phi(g) = e_H * phi(g). Right-multiplying both sides by phi(g)^{-1} in H (which exists because H is a group) and cancelling gives phi(e_G) = e_H; equivalently, phi(e_G) acts as a left identity on phi(g), and since the identity of H is unique, phi(e_G) = e_H. For the inverse: fix g in G. Then e_H = phi(e_G) = phi(g . g^{-1}) = phi(g) * phi(g^{-1}), and likewise e_H = phi(g^{-1} . g) = phi(g^{-1}) * phi(g). So phi(g^{-1}) is a two-sided inverse of phi(g) in H; because inverses in a group are unique, phi(g^{-1}) = phi(g)^{-1}. The only axioms used are the homomorphism identity, the group axioms e_G . g = g and g . g^{-1} = g^{-1} . g = e_G in G, existence of inverses in H (to cancel), and uniqueness of the identity and of inverses in H. Applied to a representation phi: G -> GL(V) with H = GL(V) and identity 1_V, these say precisely phi(e) = 1_V and phi(g^{-1}) = phi(g)^{-1}; in particular every phi(g) is automatically invertible with the stated inverse, so invertibility need not be postulated separately.

      Assessment rubric
      1. Derives phi(e_G) = e_H by applying the homomorphism identity to g = e_G . g and cancelling / invoking uniqueness of the identity in H (1 weight)
      2. Derives phi(g^{-1}) = phi(g)^{-1} by showing phi(g^{-1}) is a two-sided inverse of phi(g) and invoking uniqueness of inverses in H (1 weight)
      3. Identifies the specific group axioms used (homomorphism property, identity/inverse axioms in G, cancellation/uniqueness in H) rather than asserting the results (1 weight)
      4. Connects the two facts to the representation statements phi(e) = 1_V and phi(g^{-1}) = phi(g)^{-1}, noting invertibility of phi(g) is a consequence not a hypothesis (1 weight)

      Graph-grounded prerequisites

      These are support/source anchors, not an automatically extracted theorem-dependency proof.

      • Operator and semigroup theory (frozen curriculum anchor; see graph registry)
      • Matrix analysis (frozen curriculum anchor; see graph registry)

      Download the shared core registry

      Lean view and evidence boundary

      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

      Sources and provenance

      Contract: d3a3d241db8eecdd33b4356e425bb4ffe1ffcccf143ceb8b290b6db59ac79a12

      Item digest: 39cf1c51e2f1204e64df33d8a8210e06de5ea44fdc2525809858621ecd97be1a

      Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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