Absolute scalar height under a field automorphism
Abstract
Absolute scalar height under a field automorphism.
Theorem 1.1 (Absolute scalar height under a field automorphism).
Lean statement: D5/S3/Factorization/Dedekind/GaloisScalarHeight.scalar_mul_height_galois
Proof. Machine-checked in Lean as D5/S3/Factorization/Dedekind/GaloisScalarHeight.scalar_mul_height_galois (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every number field K, every rational field automorphism sigma of K and every x in K, the absolute multiplicative scalar height of sigma(x) equals that of x.
For an integral coordinate pair, the induced automorphism of the ring of integers preserves the absolute norm of its generated ideal. The same automorphism permutes infinite places while preserving real and complex multiplicities. These two calculations preserve the homogeneous pair height; an integral fraction representation supplies every scalar.