Module

GaloisCohomology.lean

Nyll.GaloisCohomology.Kummer.Concrete.GaloisCohomology

9 declarations indexed from sourceView source ↗

Module documentation

Galois cohomology for Kummer theory

Hilbert 90 and multiplicative cocycle statements used by the concrete Kummer correspondence.

Imports1

Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Imported by4

theorem

noetherHilbert90_exists_mul

L27 ↗

KummerTheory.noetherHilbert90_exists_mul

Documentation

Rearranged unit-valued form of Noether's Hilbert theorem 90.

Source context 5 commands

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

namespace KummerTheory
open groupCohomology
section NoetherHilbert90
variable {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
variable {f : Gal(L/K) → Lˣ}

Lean source · statement

theorem noetherHilbert90_exists_mul (hf : IsMulCocycle₁ f) :
    ∃ β : Lˣ, ∀ σ : Gal(L/K), σ • β = f σ * β

theorem

noetherHilbert90_exists_nonzero_div

L38 ↗

KummerTheory.noetherHilbert90_exists_nonzero_div

Documentation

Field-valued version of Noether's Hilbert theorem 90.

Source context 5 commands

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

namespace KummerTheory
open groupCohomology
section NoetherHilbert90
variable {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
variable {f : Gal(L/K) → Lˣ}

Lean source · statement

theorem noetherHilbert90_exists_nonzero_div (hf : IsMulCocycle₁ f) :
    ∃ β : L, β ≠ 0 ∧ ∀ σ : Gal(L/K), σ β / β = f σ

theorem

noetherHilbert90_exists_nonzero_mul

L48 ↗

KummerTheory.noetherHilbert90_exists_nonzero_mul

Documentation

Rearranged field-valued form of Noether's Hilbert theorem 90.

Source context 5 commands

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

namespace KummerTheory
open groupCohomology
section NoetherHilbert90
variable {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
variable {f : Gal(L/K) → Lˣ}

Lean source · statement

theorem noetherHilbert90_exists_nonzero_mul (hf : IsMulCocycle₁ f) :
    ∃ β : L, β ≠ 0 ∧ ∀ σ : Gal(L/K), σ β = f σ * β

theorem

cyclicHilbert90_exists_div_of_norm_eq_one

L65 ↗

KummerTheory.cyclicHilbert90_exists_div_of_norm_eq_one

Documentation

Cyclic Hilbert theorem 90: a norm-one element in a cyclic extension is y / σ(y).

Source context 5 commands

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

namespace KummerTheory
open groupCohomology
section CyclicHilbert90
variable {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
variable [IsGalois K L]

Lean source · statement

theorem cyclicHilbert90_exists_div_of_norm_eq_one
    {g : Gal(L/K)} (hg : ∀ σ : Gal(L/K), σ ∈ Subgroup.zpowers g) {x : L}
    (hx : Algebra.norm K x = 1) :
    ∃ y : Lˣ, ↑y / g ↑y = x

theorem

cyclicHilbert90_exists_nonzero_div_of_norm_eq_one

L75 ↗

KummerTheory.cyclicHilbert90_exists_nonzero_div_of_norm_eq_one

Documentation

Field-valued version of Cyclic Hilbert theorem 90.

Source context 5 commands

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

namespace KummerTheory
open groupCohomology
section CyclicHilbert90
variable {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
variable [IsGalois K L]

Lean source · statement

theorem cyclicHilbert90_exists_nonzero_div_of_norm_eq_one
    {g : Gal(L/K)} (hg : ∀ σ : Gal(L/K), σ ∈ Subgroup.zpowers g) {x : L}
    (hx : Algebra.norm K x = 1) :
    ∃ y : L, y ≠ 0 ∧ y / g y = x

theorem

cyclicHilbert90_exists_gal_div_of_norm_eq_one

L88 ↗

KummerTheory.cyclicHilbert90_exists_gal_div_of_norm_eq_one

Documentation

The β^{σ-1} orientation of Hilbert 90. Mathlib's standard endpoint uses β / σ(β); applying it to the inverse generator gives the ambient-power quotient σ(β) / β for the specified generator.

Source context 5 commands

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

namespace KummerTheory
open groupCohomology
section CyclicHilbert90
variable {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
variable [IsGalois K L]

Lean source · statement

theorem cyclicHilbert90_exists_gal_div_of_norm_eq_one
    {g : Gal(L/K)} (hg : ∀ σ : Gal(L/K), σ ∈ Subgroup.zpowers g) {x : L}
    (hx : Algebra.norm K x = 1) :
    ∃ y : Lˣ, g (y : L) / y = x

theorem

cyclicHilbert90_exists_unit_div_of_norm_eq_one

L105 ↗

KummerTheory.cyclicHilbert90_exists_unit_div_of_norm_eq_one

Documentation

Unit-valued version of Cyclic Hilbert theorem 90.

Source context 5 commands

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

namespace KummerTheory
open groupCohomology
section CyclicHilbert90
variable {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
variable [IsGalois K L]

Lean source · statement

theorem cyclicHilbert90_exists_unit_div_of_norm_eq_one
    {g : Gal(L/K)} (hg : ∀ σ : Gal(L/K), σ ∈ Subgroup.zpowers g) {x : Lˣ}
    (hx : Algebra.norm K (x : L) = 1) :
    ∃ y : Lˣ, x = y / (g • y)

theorem

cyclicHilbert90_exists_unit_mul_gal_of_norm_eq_one

L118 ↗

KummerTheory.cyclicHilbert90_exists_unit_mul_gal_of_norm_eq_one

Documentation

Rearranged unit-valued version of Cyclic Hilbert theorem 90.

Source context 5 commands

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

namespace KummerTheory
open groupCohomology
section CyclicHilbert90
variable {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
variable [IsGalois K L]

Lean source · statement

theorem cyclicHilbert90_exists_unit_mul_gal_of_norm_eq_one
    {g : Gal(L/K)} (hg : ∀ σ : Gal(L/K), σ ∈ Subgroup.zpowers g) {x : Lˣ}
    (hx : Algebra.norm K (x : L) = 1) :
    ∃ y : Lˣ, x * (g • y) = y

theorem

cyclicHilbert90_exists_mul_galRestrict_of_norm_eq_one

L139 ↗

KummerTheory.cyclicHilbert90_exists_mul_galRestrict_of_norm_eq_one

Documentation

Integral Hilbert 90 for a cyclic Galois extension.

Source context 9 commands

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

namespace KummerTheory
open groupCohomology
section IntegralHilbert90
variable {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
variable [IsGalois K L]
variable {A B : Type*} [CommRing A] [CommRing B]
variable [Algebra A B] [Algebra A L] [Algebra A K] [Algebra B L]
variable [IsScalarTower A B L] [IsScalarTower A K L] [IsFractionRing A K]
variable [IsDomain A] [IsIntegralClosure B A L]

Lean source · statement

theorem cyclicHilbert90_exists_mul_galRestrict_of_norm_eq_one
    {g : Gal(L/K)} (hg : ∀ σ : Gal(L/K), σ ∈ Subgroup.zpowers g) {η : B}
    (hη : Algebra.norm K ((algebraMap B L) η) = 1) :
    ∃ ε : B, ε ≠ 0 ∧ η * ((galRestrict A K L B) g) ε = ε

Module documentation

Galois cohomology for Kummer theory

Declarations