Module

ChosenDegreeOneFrobenius.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.ChosenDegreeOneFrobenius

2 declarations indexed from sourceView source ↗

Module documentation

The chosen degree-one Frobenius element

Surjectivity of the normalized degree supplies a Frobenius-semigroup element of exponent one. The chosen object and its specification are kept together here so the multiplicativity proof can consume a named choice boundary.

Imports1

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.Universal

Imported by2

def

chosenDegreeOneFrobeniusElement

L33 ↗

ClassFormation.DegreeData.chosenDegreeOneFrobeniusElement

Documentation

A chosen degree-one element of G(\widetilde L/K), packaged as an element of the Frobenius semigroup.

Source context 6 commands

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

universe u
namespace ClassFormation
open CyclicCohomology
noncomputable section
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

def chosenDegreeOneFrobeniusElement (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal] :
    D.FrobeniusElements K L hLK

theorem

frobeniusExponent_chosenDegreeOneFrobeniusElement

L49 ↗

ClassFormation.DegreeData.frobeniusExponent_chosenDegreeOneFrobeniusElement