Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Galois Structure and the Absolute Different

Abstract

The rational automorphism structure and absolute different of actual common golden cubic fields.

Theorem 1.1 (Semidirect product of actual automorphisms).

Lean statement: D5/S3/Factorization/Galois/GoldenCubicCommonDifferentSupport.actual_common_cubic_semidirect

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/GoldenCubicCommonDifferentSupport.actual_common_cubic_semidirect (✓ std3). ∎

Source. Repository-derived.

Commentary.

For J actual golden blocks, the rational automorphism group of their common splitting field is the semidirect product of J independent cyclic cubic coordinates by a cyclic group of order two. Its generator acts by inversion on every cubic coordinate.

Theorem 1.2 (Ramification at a noncubic block valuation).

Lean statement: D5/S3/Factorization/Galois/GoldenCubicCommonDifferentSupport.actual_common_cubic_ramification_three_divides

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/GoldenCubicCommonDifferentSupport.actual_common_cubic_ramification_three_divides (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let a rational prime divide one of the first J golden blocks with valuation not divisible by three. At every prime of the actual common field above it, three divides the absolute ramification index. The proof uses the valuation of the chosen positive cubic root in that same field.

Theorem 1.3 (Unramified primes outside the radical support).

Lean statement: D5/S3/Factorization/Galois/GoldenCubicCommonDifferentSupport.actual_common_cubic_unramified_outside_support

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/GoldenCubicCommonDifferentSupport.actual_common_cubic_unramified_outside_support (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a rational prime other than three whose valuation in every golden block through J is divisible by three, every prime of the actual common field above it has absolute ramification index one. Inertia fixes the cubic root of unity and every positive-root generator.

Theorem 1.4 (Sixth power of the absolute different).

Lean statement: D5/S3/Factorization/Galois/GoldenCubicCommonDifferentSupport.actual_common_cubic_absolute_different_sixth_power

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/GoldenCubicCommonDifferentSupport.actual_common_cubic_absolute_different_sixth_power (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let R be the product, over the first J golden blocks, of the radicals of each block after removal of its largest cubic divisor. In the ring of integers of the actual common field, the sixth power of the different over the rational integers equals the product of the cube of the ideal generated by three and the fourth power of the ideal generated by R. The proof checks multiplicity at every prime ideal, including the distinct cases over three, over R, and outside both supports.

References