Module

AbsoluteCyclotomicOrientation.lean

Nyll.Yamaguchi26AbfaithfulGalois.FormalHilbert90.AbsoluteCyclotomicOrientation

3 declarations indexed from sourceView source ↗

Module documentation

Cyclotomic formal Hilbert 90 in every field characteristic

Restriction to the separable closure supplies the orientation on the actual algebraic-closure Galois group, including imperfect base fields.

Imports5

Imported by4

def

absoluteCyclotomicOrientation

L25 ↗

Yamaguchi26AbfaithfulGalois.absoluteCyclotomicOrientation

Documentation

The cyclotomic orientation on the absolute Galois group.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
universe u
variable (p : ℕ) [Fact p.Prime] (K : Type u) [Field K]

Lean source · statement

def absoluteCyclotomicOrientation :
    Orientation p Gal(AlgebraicClosure K/K)

theorem

formalHilbert90_absoluteCyclotomicOrientation

L32 ↗

Yamaguchi26AbfaithfulGalois.formalHilbert90_absoluteCyclotomicOrientation

Documentation

Formal Hilbert 90 for primes different from the field characteristic.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
universe u
variable (p : ℕ) [Fact p.Prime] (K : Type u) [Field K]

Lean source · statement

theorem formalHilbert90_absoluteCyclotomicOrientation [NeZero (p : K)] :
    FormalHilbert90 (absoluteCyclotomicOrientation p K)

theorem

infinite_range_absoluteCyclotomicOrientation_of_finite_primary

L47 ↗

Yamaguchi26AbfaithfulGalois.infinite_range_absoluteCyclotomicOrientation_of_finite_primary

Documentation

Finiteness of primary roots on finite extensions forces the absolute cyclotomic orientation to have infinite image, also over imperfect fields.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
universe u
variable (p : ℕ) [Fact p.Prime] (K : Type u) [Field K]

Lean source · statement

theorem infinite_range_absoluteCyclotomicOrientation_of_finite_primary
    [NeZero (p : K)]
    (hRoots : ∀ L : IntermediateField K (AlgebraicClosure K), FiniteDimensional K L →
      Finite (CommGroup.primaryComponent Lˣ p)) :
    Set.Infinite (Set.range (absoluteCyclotomicOrientation p K))

Module documentation

Cyclotomic formal Hilbert 90 in every field characteristic

Declarations

absoluteCyclotomicOrientation

formalHilbert90_absoluteCyclotomicOrientation

infinite_range_absoluteCyclotomicOrientation_of_finite_primary