NYLL
Module

FrobeniusLift.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Degree.FrobeniusLift
13 declarations indexed from sourceView source ↗

Module documentation

normalized degree and Frobenius theory: lifting finite Galois automorphisms

This file defines the Frobenius semigroup in G(\widetilde L|K) and proves the lifting statement of the finite degree-quotient decomposition. Positivity is explicit, so the convention 0 ∉ ℕ is not lost in Lean's natural numbers.

Imports1
Imported by4

Declarations

theorem

exists_positive_nsmul_one_sub_mem_of_index_ne_zero

L31 ↗
ClassFormation.exists_positive_nsmul_one_sub_mem_of_index_ne_zero
Documentation

In a finite cyclic quotient of ℤ̂, every class is represented by a strictly positive natural multiple of 1.

Source context 5 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem exists_positive_nsmul_one_sub_mem_of_index_ne_zero
    (H : AddSubgroup ZHat) (hH : H.index ≠ 0) (z : ZHat) :
    ∃ n : ℕ, 0 < n ∧ z - n • (1 : ZHat) ∈ H
def

extensionInertiaWithin

L58 ↗
ClassFormation.DegreeData.extensionInertiaWithin
Documentation

I_L, viewed inside G_K; this is G_{\widetilde L}.

Source context 6 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
def extensionInertiaWithin (D : DegreeData G) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup) : Subgroup K.toSubgroup
instance

extensionInertiaWithin_normal

L65 ↗
ClassFormation.DegreeData.extensionInertiaWithin_normal
Documentation

The relative inertia subgroup is normal whenever the full extension subgroup is normal.

Source context 6 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
instance extensionInertiaWithin_normal (D : DegreeData G)
    (K L : ClosedSubgroup G) (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L hLK).Normal] :
    (D.extensionInertiaWithin K L hLK).Normal
theorem

extensionInertiaWithin_le_normalizedDegree_ker

L72 ↗
ClassFormation.DegreeData.extensionInertiaWithin_le_normalizedDegree_ker
Source context 6 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem extensionInertiaWithin_le_normalizedDegree_ker
    (D : DegreeData G) (K : FiniteResidueAbstractField D)
    (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup) :
    D.extensionInertiaWithin K.field L hLK ≤
      (D.normalizedDegree K).toMonoidHom.ker
def

extensionNormalizedDegree

L83 ↗
ClassFormation.DegreeData.extensionNormalizedDegree
Documentation

The factorized map d_K : G(\widetilde L|K) → ℤ̂.

Source context 6 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
def extensionNormalizedDegree (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal] :
    (K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK) →* ZHatMul
theorem

extensionNormalizedDegree_mk

L97 ↗
ClassFormation.DegreeData.extensionNormalizedDegree_mk
Documentation

Establishes the identity D.extensionNormalizedDegree K L hLK (QuotientGroup.mk k) = D.normalizedDegree K k.

Source context 6 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem extensionNormalizedDegree_mk (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    (k : K.field.toSubgroup) :
    D.extensionNormalizedDegree K L hLK (QuotientGroup.mk k) =
      D.normalizedDegree K k
def

extensionRestriction

L107 ↗
ClassFormation.DegreeData.extensionRestriction
Documentation

Restriction from G(\widetilde L|K) to G(L|K).

Source context 6 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
def extensionRestriction (D : DegreeData G) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L hLK).Normal] :
    (K.toSubgroup ⧸ D.extensionInertiaWithin K L hLK) →*
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)
theorem

extensionRestriction_mk

L120 ↗
ClassFormation.DegreeData.extensionRestriction_mk
Documentation

Establishes the identity D.extensionRestriction K L hLK (QuotientGroup.mk k) = QuotientGroup.mk k.

Source context 6 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem extensionRestriction_mk (D : DegreeData G)
    (K L : ClosedSubgroup G) (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L hLK).Normal]
    (k : K.toSubgroup) :
    D.extensionRestriction K L hLK (QuotientGroup.mk k) =
      QuotientGroup.mk k
def

FrobeniusElements

L130 ↗
ClassFormation.DegreeData.FrobeniusElements
Documentation

The semigroup Frob(\widetilde L|K): elements whose normalized degree is a strictly positive natural.

Source context 6 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
def FrobeniusElements (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal] : Type u
def

frobeniusRestriction

L140 ↗
ClassFormation.DegreeData.frobeniusRestriction
Documentation

The restriction map occurring in the finite degree-quotient decomposition.

Source context 6 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
def frobeniusRestriction (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 →
      (K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK)
def

normalizedExtensionImageAdd

L148 ↗
ClassFormation.DegreeData.normalizedExtensionImageAdd
Source context 6 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
def normalizedExtensionImageAdd (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup) : AddSubgroup ZHat
theorem

normalizedExtensionImageAdd_index_ne_zero

L155 ↗
ClassFormation.DegreeData.normalizedExtensionImageAdd_index_ne_zero
Source context 6 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem normalizedExtensionImageAdd_index_ne_zero
    (D : DegreeData G) (K : FiniteResidueAbstractField D)
    (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [Finite (K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK)] :
    (D.normalizedExtensionImageAdd K L hLK).index ≠ 0
theorem

frobeniusRestriction_surjective

L179 ↗
ClassFormation.DegreeData.frobeniusRestriction_surjective
Documentation

the finite degree-quotient decomposition. For a finite Galois extension L | K, restriction maps the Frobenius semigroup onto G(L|K).

Source context 6 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem frobeniusRestriction_surjective (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    [hLfinite : Finite (K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK)] :
    Function.Surjective (D.frobeniusRestriction K L hLK)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.