Module

ContinuousHilbert90.lean

Nyll.GaloisCohomology.Kummer.Concrete.ContinuousHilbert90

2 declarations indexed from sourceView source ↗

Module documentation

Noether Hilbert 90 for an infinite Galois extension

A locally constant multiplicative cocycle descends to a finite Galois stage. An open normal subgroup in its identity fiber fixes every cocycle value, so the finite-stage cocycle takes values in that actual intermediate field. Finite Noether Hilbert 90 then produces a coboundary in the original extension.

Imports4

Mathlib.FieldTheory.Galois.Infinite
Mathlib.FieldTheory.Galois.Profinite
Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
Mathlib.Topology.LocallyConstant.Basic

Imported by2

theorem

cocycle_finite_stage

L28 ↗

KummerTheory.cocycle_finite_stage

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace KummerTheory
open scoped Topology
open groupCohomology
universe u v
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
  [IsGalois K Ω]

Lean source · statement

theorem cocycle_finite_stage
    (c : Gal(Ω/K) → Ωˣ) (hc : IsMulCocycle₁ c)
    (hlc : IsLocallyConstant c) :
    ∃ (E : FiniteGaloisIntermediateField K Ω) (cE : Gal(E/K) → Eˣ),
      IsMulCocycle₁ cE ∧
      ∀ σ : Gal(Ω/K),
        ((cE (AlgEquiv.restrictNormalHom E σ) : E) : Ω) = (c σ : Ω)

theorem

noetherHilbert90_of_isLocallyConstant

L93 ↗

KummerTheory.noetherHilbert90_of_isLocallyConstant

Documentation

Continuous multiplicative cocycles into the discrete units of an arbitrary Galois extension are coboundaries.