Module

FiniteRestrictionKernel.lean

Nyll.GaloisCohomology.ArtinSchreier.FiniteRestrictionKernel

3 declarations indexed from sourceView source ↗

Module documentation

Finite kernels of restriction on Artin–Schreier classes

Imports3

Nyll.GaloisCohomology.ArtinSchreier.RootCharacter
Mathlib.FieldTheory.Galois.Infinite
Mathlib.GroupTheory.QuotientGroup.Basic

Imported by2

def

classMap

L21 ↗

ArtinSchreierTheory.classMap

Documentation

Restrict additive Artin–Schreier classes along a field embedding.

Source context 4 commands

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

namespace ArtinSchreierTheory
universe u v
variable (p : ℕ) [Fact p.Prime]
variable {K : Type u} {L : Type v} [Field K] [Field L]
  [CharP K p] [CharP L p]

Lean source · statement

def classMap (f : K →+* L) :
    K ⧸ ((frobenius K p).toAddMonoidHom - AddMonoidHom.id K).range →+
      L ⧸ ((frobenius L p).toAddMonoidHom - AddMonoidHom.id L).range

theorem

classMap_mk

L31 ↗

ArtinSchreierTheory.classMap_mk

Source context 4 commands

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

namespace ArtinSchreierTheory
universe u v
variable (p : ℕ) [Fact p.Prime]
variable {K : Type u} {L : Type v} [Field K] [Field L]
  [CharP K p] [CharP L p]

Lean source · statement

theorem classMap_mk (f : K →+* L) (a : K) :
    classMap p f (a : K ⧸
      ((frobenius K p).toAddMonoidHom - AddMonoidHom.id K).range) =
        (f a : L ⧸ ((frobenius L p).toAddMonoidHom - AddMonoidHom.id L).range)

theorem

finite_classMap_kernel

L39 ↗

ArtinSchreierTheory.finite_classMap_kernel

Documentation

In a finite Galois extension, restriction kills only finitely many Artin–Schreier classes. Such a class injects into its root-difference character on the finite relative Galois group.

Source context 4 commands

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

namespace ArtinSchreierTheory
universe u v
variable (p : ℕ) [Fact p.Prime]
variable {K : Type u} {L : Type v} [Field K] [Field L]
  [CharP K p] [CharP L p]

Lean source · statement

theorem finite_classMap_kernel [Algebra K L] [FiniteDimensional K L] [IsGalois K L] :
    Finite (classMap p (algebraMap K L)).ker

Module documentation

Finite kernels of restriction on Artin–Schreier classes

Declarations

classMap

classMap_mk

finite_classMap_kernel