AnabelianGeometry.KummerTheory.exists_power_relation_of_rootField_eq_and_cyclotomic
A root-field comparison yields a relation over the original base, with the precise loss given by the chosen cyclotomic displacement.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped IsMulCommutative
namespace AnabelianGeometry.KummerTheory
variable {K L : Type*} [Field K] [Field L] [Algebra K L]Lean source · statement
theorem exists_power_relation_of_rootField_eq_and_cyclotomic
(C : IntermediateField K L) [IsSepClosure C L] [IsGalois K C]
[IsMulCommutative (C ≃ₐ[K] C)]
(n : ℕ+) (hn : ((n : ℕ) : C) ≠ 0)
(hmu : (primitiveRoots (n : ℕ) C).Nonempty)
(m : ℕ) (σ : C ≃ₐ[K] C)
(hσ : ∀ ξ : C, ξ ^ (n : ℕ) = 1 → σ ξ = ξ ^ (m + 1))
(a b : Kˣ)
(h : rootField (L := L) n (a : K) = rootField (L := L) n (b : K)) :
∃ k : ℤ, ∃ d : Kˣ, b ^ m = (a ^ k) ^ m * d ^ (n : ℕ)