The quotient of a conjugate radical by the original radical satisfies the crossed-homomorphism law. Its values are roots of unity when the radical has a power in the base field. When those roots of unity are in the base, the crossed law becomes an ordinary multiplicative character law.
The multiplicative change in a radical under a base-field automorphism.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.KummerTheory
universe u v
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]def rootRatio (r : L) (σ : L ≃ₐ[K] L) : LThe ratio of a conjugate of a nonzero radical is nonzero.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.KummerTheory
universe u v
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]theorem rootRatio_ne_zero {r : L} (hr : r ≠ 0) (σ : L ≃ₐ[K] L) :
rootRatio r σ ≠ 0A radical ratio detects precisely whether the radical is fixed.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.KummerTheory
universe u v
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]theorem rootRatio_eq_one_iff {r : L} (hr : r ≠ 0) (σ : L ≃ₐ[K] L) :
rootRatio r σ = 1 ↔ σ r = rIf the n-th power is in the base field, each radical ratio is an n-th root of unity.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.KummerTheory
universe u v
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]theorem rootRatio_pow_eq_one {r : L} (hr : r ≠ 0) {n : ℕ} {a : K}
(ha : r ^ n = algebraMap K L a) (σ : L ≃ₐ[K] L) :
rootRatio r σ ^ n = 1The crossed-homomorphism law, without assuming roots of unity are fixed.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.KummerTheory
universe u v
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]theorem rootRatio_mul {r : L} (hr : r ≠ 0) (σ τ : L ≃ₐ[K] L) :
rootRatio r (σ * τ) = σ (rootRatio r τ) * rootRatio r σBase-field roots of unity turn the radical cocycle into a character.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.KummerTheory
universe u v
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]theorem rootRatio_mul_of_roots_in_base {r : L} (hr : r ≠ 0)
{n : ℕ} {a : K} (ha : r ^ n = algebraMap K L a)
(hroots : ∀ ξ : L, ξ ^ n = 1 → ∃ b : K, algebraMap K L b = ξ)
(σ τ : L ≃ₐ[K] L) :
rootRatio r (σ * τ) = rootRatio r σ * rootRatio r τThe radical ratio is trivial exactly on the subgroup fixing the generated intermediate field pointwise. No finite-degree or irreducibility hypothesis is needed for this kernel description.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.KummerTheory
universe u v
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]theorem mem_fixingSubgroup_adjoin_iff_rootRatio_eq_one
{r : L} (hr : r ≠ 0) (σ : L ≃ₐ[K] L) :
σ ∈ (IntermediateField.adjoin K ({r} : Set L)).fixingSubgroup ↔
rootRatio r σ = 1