How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Galois fixed points recover finite-dimensional scalar extensions
Statement
Let be finite Galois with group , and let be a finite-dimensional semilinear -space. Then is an -linear isomorphism. If is an -algebra and the action is by semilinear algebra automorphisms, this is an algebra isomorphism. For a finite-dimensional -space with the canonical action on , Here is injective, so is a copy of . Consequently , respecting algebra multiplication and units when is an -algebra.
Facts & Assumptions
Semilinear actions and canonical tensor actions have the formulas in Semilinear Galois actions, twists, and split central idempotents.
Finite Galois implies and : Equivalent characterizations of a finite Galois extension.
The trace pairing of a finite separable extension is nondegenerate: The trace form of a finite extension is nondegenerate exactly when the extension is separable.
For a separable extension, trace is the sum of the distinct embeddings: Norm and trace from embeddings, with the inseparable exponent in the norm formula. Here normality makes those embeddings precisely .
Distinct multiplicative characters of a group are linearly independent over the target field: Dedekind's linear independence theorem for distinct characters.
Tensor products of free modules have the product basis, including empty bases: The elementary tensors of two bases form the product basis of the tensor product.
Proof
Given: , , and as stated. All bases and sums used below are finite.
Put , choose an -basis of , and form its trace Gram matrix . Separability and nondegeneracy make invertible. Set . Then . The invertible coefficient matrix also shows that is a basis.
Any finite -independent list in is -independent. Indeed, if a relation exists, select one with the least positive number of nonzero coefficients and normalize one of those coefficients to . Applying and subtracting produces a relation with that coefficient zero; minimality forces every other coefficient to be fixed by every . They all lie in , contradicting -independence. A one-term relation is already impossible since a nonzero scalar cannot annihilate a nonzero vector.
For the canonical action, choose a finite -basis of . Each tensor has a unique expression : the product -basis in F6, regrouped by the , proves existence and uniqueness of its coefficients in . Such a tensor is fixed exactly when for every , equivalently each . It then equals . Conversely every is fixed. This also proves that is injective, including the empty-basis case.
Let and . A relation among the rows of vanishes on the , hence by -linearity on every ; restricting to and using independence of the distinct automorphisms as multiplicative characters makes every coefficient zero. Thus is invertible. The trace formula gives , so . Its row at yields .
Any tensor in the kernel is a finite sum . By eliminating dependent members of the finite list , rewrite it as with the -independent and invariant. Its image is , so step 1.2 forces every . Hence the tensor is zero and is injective. For the domain and codomain are zero and the same argument uses the empty list.
For define . For , semilinearity gives , since permutes the finite group. Moreover . Thus , and is onto. The formula is -balanced and -linear.
If is an algebra, its fixed space is an -subalgebra containing . For invariant and , and . Distributing over finite sums proves multiplicativity on all tensors. Together with bijectivity, this proves both algebra assertions. If , and the map is the usual multiplication ; the proof divides by no group order in any characteristic. [F1, step 3.1, step 2.2, step 1.3, algebra] QED
Remarks
The local trace-dual formula refines the evaluation-matrix proof in Zheng, Theorem 3.8.1, pp.132–133. Its injectivity argument uses finite lists, so no choice of an infinite invariant basis is needed.
Depends on
- Semilinear Galois actions, twists, and split central idempotents
- Equivalent characterizations of a finite Galois extension
- The trace form of a finite extension is nondegenerate exactly when the extension is separable
- Norm and trace from embeddings, with the inseparable exponent in the norm formula
- Dedekind's linear independence theorem for distinct characters
- The elementary tensors of two bases form the product basis of the tensor product
Used by
Dependency tree · two levels
36 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Weizhe Zheng, Lectures on Algebra (10 January 2025) (standard reference, not scraped)