NYLL
Module

ResidueAbsoluteFrobenius.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.ResidueAbsoluteFrobenius
9 declarations indexed from sourceView source ↗

Module documentation

Finite local reciprocity: Frobenius on an infinite residue extension

The finite Frobenius exponent maps are compatible with restriction. This file therefore assembles them in the actual inverse-limit presentation of an infinite Galois group. It produces the canonical continuous homomorphism from the profinite integers to the Galois group of an algebraic Galois extension of a finite field.

For an algebraic closure this is the Frobenius map compared with the degree map in finite local reciprocity. The construction itself does not require a bijectivity hypothesis.

Imports1
Imported by3

Declarations

def

finiteResidueFrobeniusIntermediate

L41 ↗
LocalClassFieldTheory.finiteResidueFrobeniusIntermediate
Documentation

The finite Frobenius action on an intermediate field, with finiteness derived from finite-dimensionality over the finite base.

Source context 7 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u v
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
variable (k : Type u) (Omega : Type v)
  [Field k] [Fintype k] [Field Omega] [Algebra k Omega]
  [IsGalois k Omega]
Lean source · statement
def finiteResidueFrobeniusIntermediate
    (E : FiniteGaloisIntermediateField k Omega) :
    ZHatMul →ₜ* (E ≃ₐ[k] E)
def

residueFrobeniusLimitPoint

L49 ↗
LocalClassFieldTheory.residueFrobeniusLimitPoint
Documentation

The compatible finite Frobenius coordinates attached to one profinite integer.

Source context 7 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u v
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
variable (k : Type u) (Omega : Type v)
  [Field k] [Fintype k] [Field Omega] [Algebra k Omega]
  [IsGalois k Omega]
Lean source · full declaration
def residueFrobeniusLimitPoint (z : ZHatMul) :
    limit (InfiniteGalois.asProfiniteGaloisGroupFunctor k Omega) where
  val := fun E => finiteResidueFrobeniusIntermediate k Omega E.unop z
  property := by
    intro E F f
    algebraize [Subsemiring.inclusion <| leOfHom f.1]
    have : IsScalarTower k F.unop E.unop :=
      IsScalarTower.of_algebraMap_eq (congrFun rfl)
    let : Finite F.unop := Module.finite_of_finite k
    let : Finite E.unop := Module.finite_of_finite k
    change AlgEquiv.restrictNormalHom F.unop
        (finiteResidueFrobeniusFromZHat k E.unop z) =
      finiteResidueFrobeniusFromZHat k F.unop z
    exact restrictNormalHom_finiteResidueFrobeniusFromZHat
      (k := k) (E := F.unop) (F := E.unop) z
def

residueFrobeniusToLimit

L67 ↗
LocalClassFieldTheory.residueFrobeniusToLimit
Documentation

The compatible Frobenius coordinates as a continuous homomorphism into the finite-Galois inverse limit.

Source context 7 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u v
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
variable (k : Type u) (Omega : Type v)
  [Field k] [Fintype k] [Field Omega] [Algebra k Omega]
  [IsGalois k Omega]
Lean source · full declaration
def residueFrobeniusToLimit :
    ZHatMul →ₜ* limit (InfiniteGalois.asProfiniteGaloisGroupFunctor k Omega) where
  toFun := residueFrobeniusLimitPoint k Omega
  map_one' := by
    apply Subtype.ext
    funext E
    exact (finiteResidueFrobeniusIntermediate k Omega E.unop).map_one
  map_mul' x y := by
    apply Subtype.ext
    funext E
    exact (finiteResidueFrobeniusIntermediate k Omega E.unop).map_mul x y
  continuous_toFun := by
    have hcontinuous (E : (FiniteGaloisIntermediateField k Omega)ᵒᵖ) :
        @Continuous ZHatMul (E.unop ≃ₐ[k] E.unop)
          inferInstance (krullTopology k E.unop)
          (finiteResidueFrobeniusIntermediate k Omega E.unop) :=
      (finiteResidueFrobeniusIntermediate k Omega E.unop).continuous_toFun
    let (E : (FiniteGaloisIntermediateField k Omega)ᵒᵖ) :
        TopologicalSpace (E.unop ≃ₐ[k] E.unop) :=
      ((InfiniteGalois.asProfiniteGaloisGroupFunctor k Omega).obj E).toProfinite.toTop.str
    apply Continuous.subtype_mk
    exact continuous_pi fun E => by
      change @Continuous ZHatMul (E.unop ≃ₐ[k] E.unop)
        inferInstance inferInstance
        (finiteResidueFrobeniusIntermediate k Omega E.unop)
      rw [show
        (inferInstance : TopologicalSpace (E.unop ≃ₐ[k] E.unop)) =
          krullTopology k E.unop by
        change (⊥ : TopologicalSpace (E.unop ≃ₐ[k] E.unop)) = krullTopology k E.unop
        exact (@DiscreteTopology.eq_bot _ (krullTopology k E.unop) inferInstance).symm]
      exact hcontinuous E
theorem

residueFrobeniusToLimit_apply_component

L102 ↗
LocalClassFieldTheory.residueFrobeniusToLimit_apply_component
Documentation

States the theorem residueFrobeniusToLimit_apply_component.

Source context 8 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u v
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
variable (k : Type u) (Omega : Type v)
  [Field k] [Fintype k] [Field Omega] [Algebra k Omega]
  [IsGalois k Omega]
omit [IsGalois k Omega] in
Lean source · statement
theorem residueFrobeniusToLimit_apply_component (z : ZHatMul)
    (E : (FiniteGaloisIntermediateField k Omega)ᵒᵖ) :
    (residueFrobeniusToLimit k Omega z).val E =
      finiteResidueFrobeniusIntermediate k Omega E.unop z
def

residueAbsoluteFrobenius

L110 ↗
LocalClassFieldTheory.residueAbsoluteFrobenius
Documentation

The canonical continuous Frobenius-parameter homomorphism ℤ̂ → Gal(Omega/k) for a Galois algebraic extension of a finite field.

Source context 7 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u v
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
variable (k : Type u) (Omega : Type v)
  [Field k] [Fintype k] [Field Omega] [Algebra k Omega]
  [IsGalois k Omega]
Lean source · statement
def residueAbsoluteFrobenius : ZHatMul →ₜ* (Omega ≃ₐ[k] Omega)
theorem

restrictNormalHom_residueAbsoluteFrobenius

L117 ↗
LocalClassFieldTheory.restrictNormalHom_residueAbsoluteFrobenius
Documentation

Restricting the assembled Frobenius to a finite Galois intermediate field gives exactly the finite Frobenius coordinate.

Source context 7 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u v
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
variable (k : Type u) (Omega : Type v)
  [Field k] [Fintype k] [Field Omega] [Algebra k Omega]
  [IsGalois k Omega]
Lean source · statement
theorem restrictNormalHom_residueAbsoluteFrobenius
    (z : ZHatMul) (E : FiniteGaloisIntermediateField k Omega) :
    AlgEquiv.restrictNormalHom E (residueAbsoluteFrobenius k Omega z) =
      finiteResidueFrobeniusIntermediate k Omega E z
theorem

restrictNormalHom_residueAbsoluteFrobenius_one

L128 ↗
LocalClassFieldTheory.restrictNormalHom_residueAbsoluteFrobenius_one
Documentation

The element 1 ∈ ℤ̂ gives the actual arithmetic Frobenius on every finite Galois residue subextension.

Source context 7 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u v
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
variable (k : Type u) (Omega : Type v)
  [Field k] [Fintype k] [Field Omega] [Algebra k Omega]
  [IsGalois k Omega]
Lean source · statement
theorem restrictNormalHom_residueAbsoluteFrobenius_one
    (E : FiniteGaloisIntermediateField k Omega) :
    AlgEquiv.restrictNormalHom E
        (residueAbsoluteFrobenius k Omega
          (Multiplicative.ofAdd (1 : ZHat))) =
      FiniteField.frobeniusAlgEquivOfAlgebraic k E
theorem

restrictNormalHom_frobeniusAlgEquivOfAlgebraic

L140 ↗
LocalClassFieldTheory.restrictNormalHom_frobeniusAlgEquivOfAlgebraic
Documentation

Arithmetic Frobenius on an algebraic Galois extension restricts to arithmetic Frobenius on every finite Galois intermediate field.

Source context 7 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u v
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
variable (k : Type u) (Omega : Type v)
  [Field k] [Fintype k] [Field Omega] [Algebra k Omega]
  [IsGalois k Omega]
Lean source · statement
theorem restrictNormalHom_frobeniusAlgEquivOfAlgebraic
    (E : FiniteGaloisIntermediateField k Omega) :
    AlgEquiv.restrictNormalHom E
        (FiniteField.frobeniusAlgEquivOfAlgebraic k Omega) =
      FiniteField.frobeniusAlgEquivOfAlgebraic k E
theorem

residueAbsoluteFrobenius_one

L164 ↗
LocalClassFieldTheory.residueAbsoluteFrobenius_one
Documentation

The distinguished element 1 ∈ ℤ̂ acts on the whole algebraic Galois extension by the actual arithmetic Frobenius.

Source context 7 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u v
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
variable (k : Type u) (Omega : Type v)
  [Field k] [Fintype k] [Field Omega] [Algebra k Omega]
  [IsGalois k Omega]
Lean source · statement
theorem residueAbsoluteFrobenius_one :
    residueAbsoluteFrobenius k Omega
        (Multiplicative.ofAdd (1 : ZHat)) =
      FiniteField.frobeniusAlgEquivOfAlgebraic k Omega

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