Module

Conjugation.lean

Nyll.AnabelianGeometry.KummerTheory.Conjugation

3 declarations indexed from sourceView source ↗

Module documentation

Cyclotomic conjugation of radical automorphisms

Conjugation transports a radical ratio by the action on roots of unity. Only the automorphism being conjugated is required to fix those roots; the conjugating automorphism may act nontrivially on them. This is the finite-level Kummer calculation behind the cyclotomic action on inertia.

Imports2

Nyll.AnabelianGeometry.KummerTheory.RootCocycle
Mathlib.Tactic.Ring

Imported by2

theorem

rootRatio_conjugate

L27 ↗

AnabelianGeometry.KummerTheory.rootRatio_conjugate

Documentation

Conjugation of an automorphism fixing the relevant roots of unity acts on its radical ratio by the conjugating automorphism's cyclotomic action.

Source context 3 commands

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]

Lean source · statement

theorem rootRatio_conjugate {r : L} (hr : r ≠ 0) {n : ℕ} {a : K}
    (ha : r ^ n = algebraMap K L a) (σ τ : L ≃ₐ[K] L)
    (hτ : ∀ ξ : L, ξ ^ n = 1 → τ ξ = ξ) :
    rootRatio r (σ * τ * σ⁻¹) = σ (rootRatio r τ)

theorem

rootRatio_conjugate_eq_pow

L45 ↗

AnabelianGeometry.KummerTheory.rootRatio_conjugate_eq_pow

Documentation

If the action on the relevant roots of unity is given by an exponent, conjugation raises the radical ratio to that same exponent.

Source context 3 commands

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]

Lean source · statement

theorem rootRatio_conjugate_eq_pow {r : L} (hr : r ≠ 0) {n m : ℕ} {a : K}
    (ha : r ^ n = algebraMap K L a) (σ τ : L ≃ₐ[K] L)
    (hτ : ∀ ξ : L, ξ ^ n = 1 → τ ξ = ξ)
    (hσ : ∀ ξ : L, ξ ^ n = 1 → σ ξ = ξ ^ m) :
    rootRatio r (σ * τ * σ⁻¹) = rootRatio r τ ^ m

theorem

rootRatio_aut_pow

L55 ↗

AnabelianGeometry.KummerTheory.rootRatio_aut_pow

Documentation

On an automorphism fixing roots of unity, powers of the automorphism correspond to powers of its radical ratio.

Source context 3 commands

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]

Lean source · statement

theorem rootRatio_aut_pow {r : L} (hr : r ≠ 0) {n : ℕ} {a : K}
    (ha : r ^ n = algebraMap K L a) (τ : L ≃ₐ[K] L)
    (hτ : ∀ ξ : L, ξ ^ n = 1 → τ ξ = ξ) (m : ℕ) :
    rootRatio r (τ ^ m) = rootRatio r τ ^ m

Module documentation

Cyclotomic conjugation of radical automorphisms

Declarations

rootRatio_conjugate

rootRatio_conjugate_eq_pow

rootRatio_aut_pow