Module

FrobeniusSemigroup.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.FrobeniusSemigroup

5 declarations indexed from sourceView source ↗

Module documentation

The abstract reciprocity construction: the Frobenius semigroup

The set Frob(\widetilde L | K) from is closed under multiplication: normalized degrees are positive natural numbers and add under products.

Imports1

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Degree.FrobeniusFixedField

Imported by3

def

frobeniusMul

ClassFormation.DegreeData.frobeniusMul

Documentation

Multiplication in this construction's Frobenius semigroup.

Source context 5 commands

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

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

Lean source · statement

def frobeniusMul (D : DegreeData G) (K : FiniteResidueAbstractField D)
    (L : ClosedSubgroup G) (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (CyclicCohomology.extensionSubgroup (G := G)
      K.field L hLK).Normal]
    (σ τ : D.FrobeniusElements K L hLK) :
    D.FrobeniusElements K L hLK

instance

frobeniusElementsMul

ClassFormation.DegreeData.frobeniusElementsMul

Documentation

Multiplication of Frobenius elements is induced by multiplication of their quotient representatives.

Source context 5 commands

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

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

Lean source · statement

instance frobeniusElementsMul (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (CyclicCohomology.extensionSubgroup (G := G)
      K.field L hLK).Normal] :
    Mul (D.FrobeniusElements K L hLK)

theorem

frobeniusMul_coe

ClassFormation.DegreeData.frobeniusMul_coe

Documentation

Establishes the identity (σ * τ).1 = σ.1 * τ.1.

Source context 5 commands

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

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

Lean source · statement

theorem frobeniusMul_coe (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (CyclicCohomology.extensionSubgroup (G := G)
      K.field L hLK).Normal]
    (σ τ : D.FrobeniusElements K L hLK) :
    (σ * τ).1 = σ.1 * τ.1

instance

frobeniusElementsSemigroup

ClassFormation.DegreeData.frobeniusElementsSemigroup

Documentation

The induced multiplication makes the Frobenius elements a semigroup.

Source context 5 commands

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

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

Lean source · full declaration

instance frobeniusElementsSemigroup (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (CyclicCohomology.extensionSubgroup (G := G)
      K.field L hLK).Normal] :
    Semigroup (D.FrobeniusElements K L hLK) where
  mul_assoc σ τ υ := by
    apply Subtype.ext
    change (σ.1 * τ.1) * υ.1 = σ.1 * (τ.1 * υ.1)
    exact mul_assoc σ.1 τ.1 υ.1

theorem

extensionNormalizedDegree_frobenius_mul

ClassFormation.DegreeData.extensionNormalizedDegree_frobenius_mul

Documentation

extensionNormalizedDegree_frobenius satisfies the multiplication formula D.extensionNormalizedDegree K L hLK (σ * τ).1 = D.extensionNormalizedDegree K L hLK σ.1 * D.extensionNormalizedDegree K L hLK τ.1.

Source context 5 commands

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

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

Lean source · statement

theorem extensionNormalizedDegree_frobenius_mul (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (CyclicCohomology.extensionSubgroup (G := G)
      K.field L hLK).Normal]
    (σ τ : D.FrobeniusElements K L hLK) :
    D.extensionNormalizedDegree K L hLK (σ * τ).1 =
      D.extensionNormalizedDegree K L hLK σ.1 *
        D.extensionNormalizedDegree K L hLK τ.1