ClassFieldTower.Martinet.Shafarevich.rootsDownstairs_fixedSubgroup_quotient_action_faithful
The actual quotient group acts faithfully on the abelianization of the open normal fixing subgroup under the original roots-downstairs conditions.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory ProCGroups.Abelian
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω] [CharZero K]
[IsAlgClosure K Ω] (L : IntermediateField K Ω)
[FiniteDimensional K L] [IsGalois K L]
attribute [local instance] fixingSubgroup_normalLean source · statement
theorem rootsDownstairs_fixedSubgroup_quotient_action_faithful
{p : ℕ} (hp : p.Prime) (hdeg : Module.finrank K L = p)
(hμ : (primitiveRoots p K).Nonempty)
(hfinite : Set.Finite {ξ : L | ∃ m : ℕ, ξ ^ (p ^ m) = 1})
(hdown : ∀ ξ : L, (∃ m : ℕ, ξ ^ (p ^ m) = 1) →
ξ ∈ Set.range (algebraMap K L)) :
Function.Injective
(quotientConjugationTopologicalAbelianizationMap L.fixingSubgroup)