ClassFieldTower.Martinet.Shafarevich.rootsDownstairs_openSubgroup_quotient_action_faithful
An open normal subgroup of prime index has faithful quotient conjugation when its fixed field satisfies the original roots-downstairs conditions.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Martinet.Shafarevich
open ProCGroups.Abelian
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω] [CharZero K]
[IsAlgClosure K Ω]Lean source · statement
theorem rootsDownstairs_openSubgroup_quotient_action_faithful
(N : OpenSubgroup Gal(Ω/K)) [N.toSubgroup.Normal]
{p : ℕ} (hp : p.Prime) (hcard : Nat.card (Gal(Ω/K) ⧸ N.toSubgroup) = p)
(hμ : (primitiveRoots p K).Nonempty)
(hfinite : Set.Finite {ξ : IntermediateField.fixedField N.toSubgroup |
∃ m : ℕ, ξ ^ (p ^ m) = 1})
(hdown : ∀ ξ : IntermediateField.fixedField N.toSubgroup,
(∃ m : ℕ, ξ ^ (p ^ m) = 1) →
ξ ∈ Set.range (algebraMap K (IntermediateField.fixedField N.toSubgroup))) :
Function.Injective (quotientConjugationTopologicalAbelianizationMap N.toSubgroup)