For a finite normal intermediate field, the actual quotient conjugation action on its fixing subgroup agrees with the canonical absolute Galois action after a constructed continuous comparison of the abelianizations.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open ProCGroups.Abelian
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω] [IsAlgClosure K Ω]
(L : IntermediateField K Ω) [FiniteDimensional K L]instance closureOverIntermediate : IsAlgClosure L ΩCompare the actual fixing subgroup's abelianization with the absolute Galois abelianization of the intermediate field.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open ProCGroups.Abelian
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω] [IsAlgClosure K Ω]
(L : IntermediateField K Ω) [FiniteDimensional K L]
local instance closureOverIntermediate : IsAlgClosure L Ω :=
⟨IsAlgClosure.isAlgClosed K, Algebra.IsAlgebraic.tower_top (K := K) L⟩def fixingSubgroupAbsoluteAbelianizationEquiv :
_root_.TopologicalAbelianization L.fixingSubgroup ≃ₜ*
_root_.TopologicalAbelianization Gal(AlgebraicClosure L/L)Evaluation of the comparison on a fixing-subgroup representative.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open ProCGroups.Abelian
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω] [IsAlgClosure K Ω]
(L : IntermediateField K Ω) [FiniteDimensional K L]
local instance closureOverIntermediate : IsAlgClosure L Ω :=
⟨IsAlgClosure.isAlgClosed K, Algebra.IsAlgebraic.tower_top (K := K) L⟩theorem fixingSubgroupAbsoluteAbelianizationEquiv_apply_mk (σ : L.fixingSubgroup) :
fixingSubgroupAbsoluteAbelianizationEquiv L
(TopologicalAbelianization.mk L.fixingSubgroup σ) =
TopologicalAbelianization.mk Gal(AlgebraicClosure L/L)
(absoluteGaloisClosureEquiv L Ω (fixingSubgroupContinuousEquiv L σ))Under the constructed comparison, the quotient action on the actual normal fixing subgroup is the action of the restricted field automorphism.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open ProCGroups.Abelian
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω] [IsAlgClosure K Ω]
(L : IntermediateField K Ω) [FiniteDimensional K L]
local instance closureOverIntermediate : IsAlgClosure L Ω :=
⟨IsAlgClosure.isAlgClosed K, Algebra.IsAlgebraic.tower_top (K := K) L⟩
variable [Normal K L]
attribute [local instance] fixingSubgroup_normaltheorem fixingSubgroupAbsoluteAbelianizationEquiv_quotient_conjugation
(σ : Gal(Ω/K)) (x : _root_.TopologicalAbelianization L.fixingSubgroup) :
fixingSubgroupAbsoluteAbelianizationEquiv L
(quotientConjugationTopologicalAbelianizationMap L.fixingSubgroup
(QuotientGroup.mk' L.fixingSubgroup σ) x) =
absoluteGaloisAbelianizationAction (σ.restrictNormal L).toRingEquiv
(fixingSubgroupAbsoluteAbelianizationEquiv L x)Nontriviality of the canonical absolute action detects the corresponding element of the quotient conjugation action on the fixing subgroup.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open ProCGroups.Abelian
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω] [IsAlgClosure K Ω]
(L : IntermediateField K Ω) [FiniteDimensional K L]
local instance closureOverIntermediate : IsAlgClosure L Ω :=
⟨IsAlgClosure.isAlgClosed K, Algebra.IsAlgebraic.tower_top (K := K) L⟩
variable [Normal K L]
attribute [local instance] fixingSubgroup_normaltheorem fixingSubgroup_quotient_action_ne_one_of_absolute_action_ne_one
(σ : Gal(Ω/K))
(hσ : absoluteGaloisAbelianizationAction (σ.restrictNormal L).toRingEquiv ≠ 1) :
quotientConjugationTopologicalAbelianizationMap L.fixingSubgroup
(QuotientGroup.mk' L.fixingSubgroup σ) ≠ 1