GaloisCohomology.exists_finiteGalois_factor_continuous_pair
A common finite Galois stage controls both coordinates.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace GaloisCohomology
open scoped Topology
open ProCGroups ProCGroups.ProC
universe u v w
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω] [IsGalois K Ω]Lean source · statement
theorem exists_finiteGalois_factor_continuous_pair
{Y : Type w} [TopologicalSpace Y] [Finite Y] [DiscreteTopology Y]
(z : Gal(Ω/K) × Gal(Ω/K) → Y) (hz : Continuous z) :
∃ (E : FiniteGaloisIntermediateField K Ω) (zE : Gal(E/K) → Gal(E/K) → Y),
∀ σ τ : Gal(Ω/K), zE (AlgEquiv.restrictNormalHom E σ)
(AlgEquiv.restrictNormalHom E τ) = z (σ, τ)