Module

CyclotomicOrientation.lean

Nyll.Yamaguchi26AbfaithfulGalois.FormalHilbert90.CyclotomicOrientation

2 declarations indexed from sourceView source ↗

Module documentation

Cyclotomic orientations satisfy formal Hilbert 90

The orientation is the actual cyclotomic character on the field automorphisms. Hilbert 90 supplies the cohomology reduction on every open subgroup.

Imports3

Nyll.Yamaguchi26AbfaithfulGalois.FormalHilbert90.FiniteH1Surjectivity
Nyll.GaloisCohomology.Kummer.Concrete.CyclotomicOpenCocycleLifting
Mathlib.Topology.Instances.ZMod

Imported by3

def

galoisCyclotomicOrientation

L24 ↗

Yamaguchi26AbfaithfulGalois.galoisCyclotomicOrientation

Documentation

The field-theoretic cyclotomic character as a continuous orientation.

Source context 4 commands

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

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

Lean source · full declaration

def galoisCyclotomicOrientation : Orientation p Gal(Ω/K) where
  toMonoidHom :=
    (cyclotomicCharacter Ω p).comp (MulSemiringAction.toRingAut Gal(Ω/K) Ω)
  continuous_toFun := cyclotomicCharacter.continuous p K Ω

theorem

formalHilbert90_galoisCyclotomicOrientation

L30 ↗

Yamaguchi26AbfaithfulGalois.formalHilbert90_galoisCyclotomicOrientation