Module

FrobeniusFixedField.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Degree.FrobeniusFixedField

46 declarations indexed from sourceView source ↗

Module documentation

normalized degree and Frobenius theory: the fixed field of a Frobenius lift

This file gives the group-dual form of the Frobenius fixed-field theorem. If σ is a Frobenius lift in G(\widetilde L | K), the subgroup Γ fixing the field Σ is the closed subgroup topologically generated by σ.

Imports3

Imported by5

def

continuousQuotientMk

L31 ↗

ClassFormation.continuousQuotientMk

Documentation

The quotient projection with its quotient topology, used locally below.

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 · full declaration

def continuousQuotientMk
    {A : Type*} [Group A] [TopologicalSpace A]
    (N : Subgroup A) [N.Normal] : A →ₜ* A ⧸ N where
  toMonoidHom := QuotientGroup.mk' N
  continuous_toFun := continuous_quotient_mk'

def

continuousQuotientLift

L39 ↗

ClassFormation.continuousQuotientLift

Documentation

The continuous lift of a homomorphism through a quotient, used locally below.

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

def continuousQuotientLift
    {A : Type*} {B : Type*} [Group A] [TopologicalSpace A]
    [Group B] [TopologicalSpace B]
    (N : Subgroup A) [N.Normal] (f : A →ₜ* B)
    (hN : N ≤ f.toMonoidHom.ker) : A ⧸ N →ₜ* B

def

continuousSubgroupSubtype

L53 ↗

ClassFormation.continuousSubgroupSubtype

Documentation

Inclusion of a subgroup with its subtype topology, used locally below.

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 · full declaration

def continuousSubgroupSubtype
    {A : Type*} [Group A] [TopologicalSpace A]
    (H : Subgroup A) : H →ₜ* A where
  toMonoidHom := H.subtype
  continuous_toFun := continuous_subtype_val

def

continuousMulEquivOfBijectiveCompactToT2

L61 ↗

ClassFormation.continuousMulEquivOfBijectiveCompactToT2

Documentation

A bijective continuous homomorphism from a compact group to a Hausdorff group is a continuous multiplicative equivalence.

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

def continuousMulEquivOfBijectiveCompactToT2
    {A : Type*} {B : Type*} [Group A] [TopologicalSpace A]
    [Group B] [TopologicalSpace B] [CompactSpace A] [T2Space B]
    (φ : A →* B) (hφcont : Continuous φ) (hφ : Function.Bijective φ) :
    A ≃ₜ* B

theorem

exists_openNormalSubgroup_not_mem

L73 ↗

ClassFormation.exists_openNormalSubgroup_not_mem

Documentation

A nonidentity element of a profinite group is omitted by some open normal subgroup.

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_openNormalSubgroup_not_mem
    {A : Type*} [Group A] [TopologicalSpace A] [IsTopologicalGroup A]
    [CompactSpace A] [T2Space A] [TotallyDisconnectedSpace A]
    {x : A} (hx : x ≠ 1) :
    ∃ U : OpenNormalSubgroup A, x ∉ (U : Subgroup A)

def

zHatPowNat

L93 ↗

ClassFormation.zHatPowNat

Documentation

Multiplication by n on ℤ̂, in the multiplicative presentation.

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 · full declaration

def zHatPowNat (n : ℕ) : ZHatMul →ₜ* ZHatMul where
  toFun z := Multiplicative.ofAdd (zHatMulNat n z.toAdd)
  map_one' := by
    apply Multiplicative.ext
    simp [zHatMulNat]
  map_mul' x y := by
    apply Multiplicative.ext
    exact nsmul_add x.toAdd y.toAdd n
  continuous_toFun := map_continuous (zHatMulNat n)

theorem

zHatPowNat_apply_toAdd

L105 ↗

ClassFormation.zHatPowNat_apply_toAdd

Documentation

The additive coordinate of a natural profinite power is multiplication by that natural.

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 zHatPowNat_apply_toAdd (n : ℕ) (z : ZHatMul) :
    (zHatPowNat n z).toAdd = n • z.toAdd

theorem

zHatPowNat_one

L111 ↗

ClassFormation.zHatPowNat_one

Documentation

The natural profinite power map sends one to the multiplicative generator.

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 zHatPowNat_one (n : ℕ) :
    zHatPowNat n
        (Multiplicative.ofAdd (1 : ZHat)) =
      (Multiplicative.ofAdd (1 : ZHat)) ^ n

def

zHatReductionMul

L119 ↗

ClassFormation.zHatReductionMul

Documentation

Reduction modulo n, in the multiplicative presentation.

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 · full declaration

def zHatReductionMul (n : ℕ) (hn : 0 < n) :
    ZHatMul →ₜ* Multiplicative (ZMod n) where
  toFun z := Multiplicative.ofAdd (zHatReduction n hn z.toAdd)
  map_one' := by
    apply Multiplicative.ext
    exact map_zero (zHatReduction n hn)
  map_mul' x y := by
    apply Multiplicative.ext
    exact map_add (zHatReduction n hn) x.toAdd y.toAdd
  continuous_toFun := map_continuous (zHatReduction n hn)

theorem

zHatReductionMul_apply_toAdd

L132 ↗

ClassFormation.zHatReductionMul_apply_toAdd

Documentation

Reduction followed by multiplication has the expected additive-coordinate formula.

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 zHatReductionMul_apply_toAdd (n : ℕ) (hn : 0 < n)
    (z : ZHatMul) :
    (zHatReductionMul n hn z).toAdd = zHatReduction n hn z.toAdd

theorem

injective_of_topologicallyGenerates_zHat_one

L140 ↗

ClassFormation.injective_of_topologicallyGenerates_zHat_one

Documentation

The cardinal comparison used in the classical proof of the Frobenius fixed-field theorem: a continuous map from a profinite procyclic group to ℤ̂ which sends a topological generator to 1 is injective.

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 injective_of_topologicallyGenerates_zHat_one
    {A : Type*} [CommGroup A] [TopologicalSpace A]
    [IsTopologicalGroup A] [CompactSpace A] [T2Space A]
    [TotallyDisconnectedSpace A]
    (f : A →ₜ* ZHatMul) (x : A)
    (hxgen : TopologicallyGenerates ({x} : Set A))
    (hfx : f x = Multiplicative.ofAdd (1 : ZHat)) :
    Function.Injective f

def

frobeniusExponent

L302 ↗

ClassFormation.DegreeData.frobeniusExponent

Documentation

The positive integer d_K(σ) attached to a Frobenius lift.

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 frobeniusExponent (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_pos

L309 ↗

ClassFormation.DegreeData.frobeniusExponent_pos

Documentation

The Frobenius exponent attached to a finite extension is strictly positive.

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 frobeniusExponent_pos (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) :
    0 < D.frobeniusExponent K L hLK σ

theorem

extensionNormalizedDegree_frobenius_eq_pow

L318 ↗

ClassFormation.DegreeData.extensionNormalizedDegree_frobenius_eq_pow

Documentation

The normalized degree of Frobenius is the corresponding natural profinite power.

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_frobenius_eq_pow (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) :
    D.extensionNormalizedDegree K L hLK σ.1 =
      (Multiplicative.ofAdd (1 : ZHat)) ^
          D.frobeniusExponent K L hLK σ

theorem

frobeniusExponent_unique

L330 ↗

ClassFormation.DegreeData.frobeniusExponent_unique

Documentation

The normalized-degree equation uniquely determines the natural Frobenius exponent.

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 frobeniusExponent_unique (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) (n : ℕ)
    (hn :
      D.extensionNormalizedDegree K L hLK σ.1 =
        (Multiplicative.ofAdd (1 : ZHat)) ^ n) :
    n = D.frobeniusExponent K L hLK σ

def

extensionNormalizedDegreeContinuous

L344 ↗

ClassFormation.DegreeData.extensionNormalizedDegreeContinuous

Documentation

The factorized normalized degree as a continuous homomorphism.

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 extensionNormalizedDegreeContinuous (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

extensionNormalizedDegreeContinuous_apply

L360 ↗

ClassFormation.DegreeData.extensionNormalizedDegreeContinuous_apply

Documentation

The continuous normalized-degree map evaluates as the algebraic normalized-degree map.

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 extensionNormalizedDegreeContinuous_apply (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    (x : K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK) :
    D.extensionNormalizedDegreeContinuous K L hLK x =
      D.extensionNormalizedDegree K L hLK x

theorem

extensionNormalizedDegreeContinuous_toMonoidHom

L371 ↗

ClassFormation.DegreeData.extensionNormalizedDegreeContinuous_toMonoidHom

Documentation

Forgetting continuity recovers the underlying normalized-degree monoid homomorphism.

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 extensionNormalizedDegreeContinuous_toMonoidHom (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal] :
    (D.extensionNormalizedDegreeContinuous K L hLK).toMonoidHom =
      D.extensionNormalizedDegree K L hLK

theorem

extensionNormalizedDegreeContinuous_surjective

L380 ↗

ClassFormation.DegreeData.extensionNormalizedDegreeContinuous_surjective

Documentation

The continuous normalized-degree map of the extension is surjective.

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 extensionNormalizedDegreeContinuous_surjective (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal] :
    Function.Surjective
      (D.extensionNormalizedDegreeContinuous K L hLK)

def

extensionDegreeKernelRestriction

L393 ↗

ClassFormation.DegreeData.extensionDegreeKernelRestriction

Documentation

Restriction embeds the kernel of d_K on G(\widetilde L|K) into the finite group 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 extensionDegreeKernelRestriction (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal] :
    (D.extensionNormalizedDegreeContinuous K L hLK).toMonoidHom.ker →*
      (K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK)

theorem

extensionDegreeKernelRestriction_injective

L403 ↗

ClassFormation.DegreeData.extensionDegreeKernelRestriction_injective

Documentation

Restriction to the degree kernel is injective on the extension subgroup.

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 extensionDegreeKernelRestriction_injective (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal] :
    Function.Injective
      (D.extensionDegreeKernelRestriction K L hLK)

theorem

extensionInertiaWithin_isClosed

L446 ↗

ClassFormation.DegreeData.extensionInertiaWithin_isClosed

Documentation

The extension's inertia subgroup is closed inside its base subgroup.

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_isClosed (D : DegreeData G)
    [IsTopologicalGroup G]
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup) :
    IsClosed (D.extensionInertiaWithin K.field L hLK : Set K.field.toSubgroup)

def

frobeniusClosure

L467 ↗

ClassFormation.DegreeData.frobeniusClosure

Documentation

The closed cyclic subgroup Γ = closure ⟨σ⟩ fixing the field Σ of the Frobenius fixed-field theorem.

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 frobeniusClosure (D : DegreeData G) [IsTopologicalGroup 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) :
    ClosedSubgroup
      (K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK)

def

frobeniusInClosure

L478 ↗

ClassFormation.DegreeData.frobeniusInClosure

Documentation

The chosen Frobenius lift, regarded as an element of Γ.

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 frobeniusInClosure (D : DegreeData G) [IsTopologicalGroup 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) :
    D.frobeniusClosure K L hLK σ

instance

frobeniusClosure_isTopologicalGroup

L487 ↗

ClassFormation.DegreeData.frobeniusClosure_isTopologicalGroup

Documentation

The closure of the Frobenius-generated subgroup inherits a topological group structure.

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 frobeniusClosure_isTopologicalGroup
    (D : DegreeData G) [IsTopologicalGroup 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) :
    IsTopologicalGroup (D.frobeniusClosure K L hLK σ)

def

frobeniusClosureCommGroup

L499 ↗

ClassFormation.DegreeData.frobeniusClosureCommGroup

Documentation

Defines frobeniusClosureCommGroup.

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 frobeniusClosureCommGroup
    (D : DegreeData G) [IsTopologicalGroup G] [T2Space 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) :
    CommGroup (D.frobeniusClosure K L hLK σ)

theorem

frobeniusInClosure_topologicallyGenerates

L534 ↗

ClassFormation.DegreeData.frobeniusInClosure_topologicallyGenerates

Documentation

By construction, σ topologically generates Γ.

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 frobeniusInClosure_topologicallyGenerates
    (D : DegreeData G) [IsTopologicalGroup 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) :
    TopologicallyGenerates
      ({D.frobeniusInClosure K L hLK σ} : Set
        (D.frobeniusClosure K L hLK σ))

def

frobeniusClosureDegree

L565 ↗

ClassFormation.DegreeData.frobeniusClosureDegree

Documentation

The normalized degree restricted to Γ.

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 frobeniusClosureDegree (D : DegreeData G) [IsTopologicalGroup 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) :
    D.frobeniusClosure K L hLK σ →ₜ* ZHatMul

theorem

frobeniusClosureDegree_generator

L577 ↗

ClassFormation.DegreeData.frobeniusClosureDegree_generator

Documentation

The degree map sends the canonical Frobenius-closure generator to its expected value.

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 frobeniusClosureDegree_generator (D : DegreeData G)
    [IsTopologicalGroup 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) :
    D.frobeniusClosureDegree K L hLK σ
        (D.frobeniusInClosure K L hLK σ) =
      (Multiplicative.ofAdd (1 : ZHat)) ^
          D.frobeniusExponent K L hLK σ

theorem

frobeniusClosureDegree_range

L599 ↗

ClassFormation.DegreeData.frobeniusClosureDegree_range

Documentation

The image of d_K on Γ is precisely n ℤ̂, where n = d_K(σ). This is the group-dual residue-degree calculation in the Frobenius fixed-field residue-degree formula.

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 frobeniusClosureDegree_range (D : DegreeData G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space 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) :
    (D.frobeniusClosureDegree K L hLK σ).toMonoidHom.range =
      AddSubgroup.toSubgroup
        ((zHatMulNat (D.frobeniusExponent K L hLK σ)).toAddMonoidHom.range)

theorem

frobeniusClosureDegree_range_index

L698 ↗

ClassFormation.DegreeData.frobeniusClosureDegree_range_index

Documentation

The Frobenius fixed-field residue-degree formula, stated as the index of the normalized degree image: the relative residue degree of the fixed field Σ over K is d_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 frobeniusClosureDegree_range_index (D : DegreeData G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space 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) :
    (Subgroup.toAddSubgroup'
      (D.frobeniusClosureDegree K L hLK σ).toMonoidHom.range).index =
      D.frobeniusExponent K L hLK σ

def

frobeniusClosureDegreeInMulNatRange

L712 ↗

ClassFormation.DegreeData.frobeniusClosureDegreeInMulNatRange

Documentation

The value of d_K on Γ, regarded in the subgroup n ℤ̂.

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 frobeniusClosureDegreeInMulNatRange (D : DegreeData G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space 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)
    (a : D.frobeniusClosure K L hLK σ) :
    (zHatMulNat (D.frobeniusExponent K L hLK σ)).toAddMonoidHom.range

theorem

frobeniusClosureDegreeInMulNatRange_coe

L729 ↗

ClassFormation.DegreeData.frobeniusClosureDegreeInMulNatRange_coe

Documentation

The restricted Frobenius-closure degree has the stated underlying profinite value.

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 frobeniusClosureDegreeInMulNatRange_coe (D : DegreeData G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space 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)
    (a : D.frobeniusClosure K L hLK σ) :
    (D.frobeniusClosureDegreeInMulNatRange K L hLK σ a).1 =
      (D.frobeniusClosureDegree K L hLK σ a).toAdd

def

fixedFieldNormalizedDegree

L741 ↗

ClassFormation.DegreeData.fixedFieldNormalizedDegree

Documentation

The normalized degree d_Σ = (1/n)d_K on Γ.

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 · full declaration

def fixedFieldNormalizedDegree (D : DegreeData G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space 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) :
    D.frobeniusClosure K L hLK σ →ₜ* ZHatMul where
  toFun a := Multiplicative.ofAdd
    (zHatDivide (D.frobeniusExponent K L hLK σ)
      (D.frobeniusExponent_pos K L hLK σ)
      (D.frobeniusClosureDegreeInMulNatRange K L hLK σ a))
  map_one' := by
    apply Multiplicative.ext
    rw [show D.frobeniusClosureDegreeInMulNatRange K L hLK σ 1 = 0 by
      apply Subtype.ext
      exact congrArg Multiplicative.toAdd
        (map_one (D.frobeniusClosureDegree K L hLK σ))]
    exact map_zero (zHatDivide
      (D.frobeniusExponent K L hLK σ)
      (D.frobeniusExponent_pos K L hLK σ))
  map_mul' a b := by
    apply Multiplicative.ext
    rw [show D.frobeniusClosureDegreeInMulNatRange K L hLK σ (a * b) =
        D.frobeniusClosureDegreeInMulNatRange K L hLK σ a +
          D.frobeniusClosureDegreeInMulNatRange K L hLK σ b by
      apply Subtype.ext
      exact congrArg Multiplicative.toAdd
        (map_mul (D.frobeniusClosureDegree K L hLK σ) a b)]
    exact map_add (zHatDivide
      (D.frobeniusExponent K L hLK σ)
      (D.frobeniusExponent_pos K L hLK σ)) _ _
  continuous_toFun := by
    apply (map_continuous (zHatDivide
      (D.frobeniusExponent K L hLK σ)
      (D.frobeniusExponent_pos K L hLK σ))).comp
    exact Continuous.subtype_mk
      (D.frobeniusClosureDegree K L hLK σ).continuous_toFun
      (fun a =>
        (D.frobeniusClosureDegreeInMulNatRange K L hLK σ a).2)

theorem

frobeniusExponent_nsmul_fixedFieldNormalizedDegree

L782 ↗

ClassFormation.DegreeData.frobeniusExponent_nsmul_fixedFieldNormalizedDegree

Documentation

The defining identity n d_Σ = d_K on Γ.

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 frobeniusExponent_nsmul_fixedFieldNormalizedDegree
    (D : DegreeData G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space 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)
    (a : D.frobeniusClosure K L hLK σ) :
    D.frobeniusExponent K L hLK σ •
        (D.fixedFieldNormalizedDegree K L hLK σ a).toAdd =
      (D.frobeniusClosureDegree K L hLK σ a).toAdd

theorem

fixedFieldNormalizedDegree_generator

L800 ↗

ClassFormation.DegreeData.fixedFieldNormalizedDegree_generator

Documentation

The chosen lift has normalized degree 1 over its fixed field.

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 fixedFieldNormalizedDegree_generator (D : DegreeData G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space 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) :
    D.fixedFieldNormalizedDegree K L hLK σ
        (D.frobeniusInClosure K L hLK σ) =
      Multiplicative.ofAdd (1 : ZHat)

theorem

fixedFieldNormalizedDegree_surjective

L825 ↗

ClassFormation.DegreeData.fixedFieldNormalizedDegree_surjective

Documentation

The normalized degree on Γ is onto.

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 fixedFieldNormalizedDegree_surjective (D : DegreeData G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space 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) :
    Function.Surjective
      (D.fixedFieldNormalizedDegree K L hLK σ)

theorem

frobeniusClosure_totallyDisconnectedSpace

L851 ↗

ClassFormation.DegreeData.frobeniusClosure_totallyDisconnectedSpace

Documentation

The closed cyclic group Γ is totally disconnected.

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 frobeniusClosure_totallyDisconnectedSpace (D : DegreeData G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace 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) :
    TotallyDisconnectedSpace (D.frobeniusClosure K L hLK σ)

theorem

frobeniusFixedField_finiteIndex

L872 ↗

ClassFormation.DegreeData.frobeniusFixedField_finiteIndex

Documentation

finiteness of the Frobenius fixed field, in the Galois-dual form: the closed subgroup Γ = closure ⟨σ⟩ has finite index in G(\widetilde L|K), hence its fixed field Σ is finite over 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 frobeniusFixedField_finiteIndex (D : DegreeData G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space 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)]
    (σ : D.FrobeniusElements K L hLK) :
    Finite
      ((K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK) ⧸
        (D.frobeniusClosure K L hLK σ).toSubgroup)

theorem

frobeniusFixedField_normalizedDegree_injective

L935 ↗

ClassFormation.DegreeData.frobeniusFixedField_normalizedDegree_injective

Documentation

The procyclic degree isomorphism, kernel form: d_Σ has trivial kernel. The proof is the comparison of the finite quotients Γ/Γ^m with ℤ̂/mℤ̂.

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 frobeniusFixedField_normalizedDegree_injective (D : DegreeData G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace 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) :
    Function.Injective
      (D.fixedFieldNormalizedDegree K L hLK σ)

theorem

frobeniusClosure_index_le_extensionIndex_of_exponent_eq_one

L964 ↗

ClassFormation.DegreeData.frobeniusClosure_index_le_extensionIndex_of_exponent_eq_one

Documentation

The index estimate in the proof of finiteness of the Frobenius fixed field. When the chosen Frobenius lift has degree one, the degree of its fixed field is at most the degree of the finite Galois extension from which the lift was chosen.

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 frobeniusClosure_index_le_extensionIndex_of_exponent_eq_one
    (D : DegreeData G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace 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)]
    (σ : D.FrobeniusElements K L hLK)
    (hσ : D.frobeniusExponent K L hLK σ = 1) :
    (D.frobeniusClosure K L hLK σ).toSubgroup.index ≤
      (extensionSubgroup K.field L hLK).index

def

frobeniusFixedField_normalizedDegreeEquiv

L1059 ↗

ClassFormation.DegreeData.frobeniusFixedField_normalizedDegreeEquiv

Documentation

The procyclic degree isomorphism: d_Σ identifies Γ continuously with ℤ̂. On the field side its trivial kernel says exactly \widetilde Σ = \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 frobeniusFixedField_normalizedDegreeEquiv (D : DegreeData G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace 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) :
    D.frobeniusClosure K L hLK σ ≃ₜ* ZHatMul

theorem

frobeniusFixedField_normalizedDegreeEquiv_apply

L1084 ↗

ClassFormation.DegreeData.frobeniusFixedField_normalizedDegreeEquiv_apply

Documentation

The normalized-degree equivalence on the Frobenius fixed field evaluates by restriction.

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 frobeniusFixedField_normalizedDegreeEquiv_apply (D : DegreeData G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace 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)
    (a : D.frobeniusClosure K L hLK σ) :
    D.frobeniusFixedField_normalizedDegreeEquiv K L hLK σ a =
      D.fixedFieldNormalizedDegree K L hLK σ a

theorem

frobeniusFixedField_kernel

L1097 ↗

ClassFormation.DegreeData.frobeniusFixedField_kernel

Documentation

The explicit kernel-triviality form of the procyclic degree isomorphism.

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 frobeniusFixedField_kernel (D : DegreeData G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace 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) :
    (D.fixedFieldNormalizedDegree K L hLK σ).toMonoidHom.ker = ⊥

def

fixedFieldFrobenius

L1109 ↗

ClassFormation.DegreeData.fixedFieldFrobenius

Documentation

The Frobenius over the fixed field Σ, defined by d_Σ(φ_Σ)=1.

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 fixedFieldFrobenius (D : DegreeData G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace 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) :
    D.frobeniusClosure K L hLK σ

theorem

frobeniusFixedField_frobenius

L1122 ↗

ClassFormation.DegreeData.frobeniusFixedField_frobenius

Documentation

The Frobenius characterization of the chosen lift: the original lift σ is the Frobenius of its fixed field Σ.

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 frobeniusFixedField_frobenius (D : DegreeData G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace 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) :
    D.frobeniusInClosure K L hLK σ =
      D.fixedFieldFrobenius K L hLK σ

Module documentation

normalized degree and Frobenius theory: the fixed field of a Frobenius lift

Declarations