ModuleFixedSubgroupTopology.lean
Nyll.GaloisCohomology.Kummer.Concrete.FixedSubgroupTopology
7 declarations indexed from sourceView source ↗ Module documentation
The topology of a finite intermediate field's fixing subgroup
The usual algebraic identification of the fixing subgroup with the relative Galois group is a homeomorphism for the Krull topologies. Finiteness of the intermediate field suffices; no normality or algebraicity of the ambient extension is needed.
Imports5
- Mathlib.FieldTheory.KrullTopology
- Mathlib.FieldTheory.Galois.Basic
- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
- Mathlib.Topology.Algebra.Group.Basic
- Mathlib.Topology.Algebra.ContinuousMonoidHom
Imported by10
Declarations
KummerTheory.fixingSubgroupEquiv_apply
DocumentationThe fixing subgroup equivalence preserves evaluation in the ambient field.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open scoped Topology
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]
(L : IntermediateField K Ω)
KummerTheory.fixingSubgroupEquiv_symm_apply
DocumentationThe inverse fixing subgroup equivalence preserves ambient evaluation.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open scoped Topology
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]
(L : IntermediateField K Ω)
KummerTheory.fixingSubgroupEquiv_continuous
DocumentationReinterpreting an ambient fixing automorphism as an L-automorphism is continuous.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open scoped Topology
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]
(L : IntermediateField K Ω)
variable [FiniteDimensional K L]
KummerTheory.fixingSubgroupEquiv_symm_continuous
DocumentationRestricting scalars from L back to K is continuous into the fixing subgroup.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open scoped Topology
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]
(L : IntermediateField K Ω)
variable [FiniteDimensional K L]
KummerTheory.fixingSubgroupContinuousEquiv
DocumentationThe finite intermediate field's fixing subgroup is its relative Galois group, with the same Krull topology.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open scoped Topology
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]
(L : IntermediateField K Ω)
variable [FiniteDimensional K L]
KummerTheory.fixingSubgroupContinuousEquiv_apply
DocumentationEvaluation of the continuous fixing subgroup equivalence.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open scoped Topology
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]
(L : IntermediateField K Ω)
variable [FiniteDimensional K L]
KummerTheory.fixingSubgroupContinuousEquiv_symm_apply
DocumentationEvaluation of the inverse continuous fixing subgroup equivalence.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open scoped Topology
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]
(L : IntermediateField K Ω)
variable [FiniteDimensional K L]