Module

ContinuousAdditiveHilbert90.lean

Nyll.GaloisCohomology.FieldTheory.ContinuousAdditiveHilbert90

3 declarations indexed from sourceView source ↗

Module documentation

Additive Hilbert 90 for continuous Galois cocycles

In a finite Galois extension, an element of trace one gives an explicit coboundary. A locally constant cocycle on an infinite Galois group descends to a finite Galois field, so the same construction applies.

Imports5

Mathlib.FieldTheory.Galois.Infinite
Mathlib.FieldTheory.Galois.Profinite
Mathlib.RingTheory.Trace.Basic
Mathlib.Topology.LocallyConstant.Basic
Mathlib.Tactic.Ring

Imported by4

theorem

additiveHilbert90_finite

L28 ↗

GaloisCohomology.additiveHilbert90_finite

Documentation

An additive cocycle on a finite Galois extension is a coboundary.

Source context 4 commands

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

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

Lean source · statement

theorem additiveHilbert90_finite [FiniteDimensional K Ω]
    (c : Gal(Ω/K) → Ω)
    (hc : ∀ σ τ : Gal(Ω/K), c (σ * τ) = σ (c τ) + c σ) :
    ∃ β : Ω, ∀ σ : Gal(Ω/K), σ β - β = c σ

theorem

additive_cocycle_finite_stage

L62 ↗

GaloisCohomology.additive_cocycle_finite_stage

Source context 4 commands

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

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

Lean source · statement

theorem additive_cocycle_finite_stage
    (c : Gal(Ω/K) → Ω)
    (hc : ∀ σ τ : Gal(Ω/K), c (σ * τ) = σ (c τ) + c σ)
    (hlc : IsLocallyConstant c) :
    ∃ (E : FiniteGaloisIntermediateField K Ω) (cE : Gal(E/K) → E),
      (∀ σ τ : Gal(E/K), cE (σ * τ) = σ (cE τ) + cE σ) ∧
      ∀ σ : Gal(Ω/K), (cE (AlgEquiv.restrictNormalHom E σ) : Ω) = c σ

theorem

additiveHilbert90_of_isLocallyConstant

L119 ↗

GaloisCohomology.additiveHilbert90_of_isLocallyConstant

Documentation

Locally constant additive cocycles are coboundaries in any Galois extension.

Source context 4 commands

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

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

Lean source · statement

theorem additiveHilbert90_of_isLocallyConstant
    (c : Gal(Ω/K) → Ω)
    (hc : ∀ σ τ : Gal(Ω/K), c (σ * τ) = σ (c τ) + c σ)
    (hlc : IsLocallyConstant c) :
    ∃ β : Ω, ∀ σ : Gal(Ω/K), σ β - β = c σ

Module documentation

Additive Hilbert 90 for continuous Galois cocycles

Declarations

additiveHilbert90_finite

additive_cocycle_finite_stage

additiveHilbert90_of_isLocallyConstant