For a finite normal intermediate field in a separable closure, 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 Ω] [IsSepClosure K Ω]
(L : IntermediateField K Ω) [FiniteDimensional K L]instance separableClosureOverIntermediate : IsSepClosure 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 Ω] [IsSepClosure K Ω]
(L : IntermediateField K Ω) [FiniteDimensional K L]
local instance separableClosureOverIntermediate : IsSepClosure L Ω :=
⟨IsSepClosure.sep_closed K, Algebra.isSeparable_tower_top_of_isSeparable K L Ω⟩def fixingSubgroupSeparableAbsoluteAbelianizationEquiv :
_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 Ω] [IsSepClosure K Ω]
(L : IntermediateField K Ω) [FiniteDimensional K L]
local instance separableClosureOverIntermediate : IsSepClosure L Ω :=
⟨IsSepClosure.sep_closed K, Algebra.isSeparable_tower_top_of_isSeparable K L Ω⟩theorem fixingSubgroupSeparableAbsoluteAbelianizationEquiv_apply_mk (σ : L.fixingSubgroup) :
fixingSubgroupSeparableAbsoluteAbelianizationEquiv L
(TopologicalAbelianization.mk L.fixingSubgroup σ) =
TopologicalAbelianization.mk Gal(AlgebraicClosure L/L)
(separableAbsoluteGaloisClosureEquiv 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 Ω] [IsSepClosure K Ω]
(L : IntermediateField K Ω) [FiniteDimensional K L]
local instance separableClosureOverIntermediate : IsSepClosure L Ω :=
⟨IsSepClosure.sep_closed K, Algebra.isSeparable_tower_top_of_isSeparable K L Ω⟩
variable [Normal K L]
attribute [local instance] fixingSubgroup_normaltheorem fixingSubgroupSeparableAbsoluteAbelianizationEquiv_quotient_conjugation
(σ : Gal(Ω/K)) (x : _root_.TopologicalAbelianization L.fixingSubgroup) :
fixingSubgroupSeparableAbsoluteAbelianizationEquiv L
(quotientConjugationTopologicalAbelianizationMap L.fixingSubgroup
(QuotientGroup.mk' L.fixingSubgroup σ) x) =
absoluteGaloisAbelianizationAction (σ.restrictNormal L).toRingEquiv
(fixingSubgroupSeparableAbsoluteAbelianizationEquiv L x)