ModuleContinuousCharacters.lean
Nyll.GaloisCohomology.Kummer.Concrete.ContinuousCharacters
3 declarations indexed from sourceView source ↗ Module documentation
Finite-stage factorization of continuous Galois characters
A continuous character from an infinite Galois group to a discrete group factors through the Galois group of a finite Galois intermediate field.
Imports3
- Mathlib.FieldTheory.Galois.Infinite
- Mathlib.FieldTheory.Galois.Profinite
- Mathlib.Topology.Algebra.ContinuousMonoidHom
Imported by2
Declarations
KummerTheory.continuousCharacterIsOpenKer
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
open scoped Topology
variable {K Ω A : Type*}
[Field K] [Field Ω] [Algebra K Ω]
[Group A] [TopologicalSpace A] [DiscreteTopology A]
KummerTheory.continuousCharacterExistsFiniteGaloisFixingSubgroupLeKer
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
open scoped Topology
variable {K Ω A : Type*}
[Field K] [Field Ω] [Algebra K Ω]
[Group A] [TopologicalSpace A] [DiscreteTopology A]
variable [IsGalois K Ω]
KummerTheory.continuousCharacter_factors_through_finiteGalois
DocumentationEvery continuous character of an infinite Galois group into a discrete group factors through the Galois group of a finite Galois intermediate field.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
open scoped Topology
variable {K Ω A : Type*}
[Field K] [Field Ω] [Algebra K Ω]
[Group A] [TopologicalSpace A] [DiscreteTopology A]
variable [IsGalois K Ω]