Module

ResidueAlgebraicClosureDegree.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.ResidueAlgebraicClosureDegree

22 declarations indexed from sourceView source ↗

Module documentation

Finite local reciprocity: degree coordinates on any residue algebraic closure

The residue field obtained from a valuation ring in a separable closure is not definitionally Mathlib's chosen AlgebraicClosure. The construction of the degree map must therefore work on any algebraically closed algebraic extension of the finite residue field.

This file repeats the inverse-limit detection argument in that intrinsic setting. The resulting map is the inverse of the canonical arithmetic Frobenius homomorphism itself; no equivalence with a chosen algebraic closure and no generator of a finite cyclic group enters its definition.

Imports2

Imported by3

instance

finiteResidueBaseRingCharPrime

L44 ↗

LocalClassFieldTheory.finiteResidueBaseRingCharPrime

Source context 11 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
open RamificationTheory.Field.absoluteGaloisGroup
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
variable (Omega : Type v) [Field Omega] [Algebra k Omega]
  [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega]
omit [Fintype k] in

Lean source · statement

instance finiteResidueBaseRingCharPrime [Finite k] : Fact (ringChar k).Prime

instance

residueAlgebraicClosureIsAlgClosure

L47 ↗

LocalClassFieldTheory.residueAlgebraicClosureIsAlgClosure

Source context 10 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
open RamificationTheory.Field.absoluteGaloisGroup
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
variable (Omega : Type v) [Field Omega] [Algebra k Omega]
  [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega]

Lean source · statement

instance residueAlgebraicClosureIsAlgClosure : IsAlgClosure k Omega

instance

residueAlgebraicClosureIsGalois

L51 ↗

LocalClassFieldTheory.residueAlgebraicClosureIsGalois

Source context 11 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
open RamificationTheory.Field.absoluteGaloisGroup
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
variable (Omega : Type v) [Field Omega] [Algebra k Omega]
  [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega]
omit [Fintype k] in

Lean source · statement

instance residueAlgebraicClosureIsGalois [Finite k] : IsGalois k Omega

instance

residueAlgebraicClosureGaloisT2

L54 ↗

LocalClassFieldTheory.residueAlgebraicClosureGaloisT2

Source context 10 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
open RamificationTheory.Field.absoluteGaloisGroup
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
variable (Omega : Type v) [Field Omega] [Algebra k Omega]
  [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega]

Lean source · statement

instance residueAlgebraicClosureGaloisT2 :
    T2Space (Omega ≃ₐ[k] Omega)

def

finiteResidueExtensionEmbeddingInto

L61 ↗

LocalClassFieldTheory.finiteResidueExtensionEmbeddingInto

Documentation

Embed the degree-n finite extension of k into the given residue algebraic closure. This choice is used only to prove that all profinite coordinates are detected.

Source context 10 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
open RamificationTheory.Field.absoluteGaloisGroup
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
variable (Omega : Type v) [Field Omega] [Algebra k Omega]
  [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega]

Lean source · statement

def finiteResidueExtensionEmbeddingInto
    (n : ℕ) [NeZero n] :
    FiniteField.Extension k (ringChar k) n →ₐ[k] Omega

def

finiteResidueIntermediateFieldIn

L72 ↗

LocalClassFieldTheory.finiteResidueIntermediateFieldIn

Documentation

The image of the degree-n finite extension in the given residue algebraic closure.

Source context 10 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
open RamificationTheory.Field.absoluteGaloisGroup
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
variable (Omega : Type v) [Field Omega] [Algebra k Omega]
  [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega]

Lean source · statement

def finiteResidueIntermediateFieldIn
    (n : ℕ) [NeZero n] : IntermediateField k Omega

def

finiteResidueExtensionEquivIntermediateIn

L79 ↗

LocalClassFieldTheory.finiteResidueExtensionEquivIntermediateIn

Documentation

The model finite field is canonically isomorphic to its embedded image.

Source context 10 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
open RamificationTheory.Field.absoluteGaloisGroup
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
variable (Omega : Type v) [Field Omega] [Algebra k Omega]
  [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega]

Lean source · statement

def finiteResidueExtensionEquivIntermediateIn
    (n : ℕ) [NeZero n] :
    FiniteField.Extension k (ringChar k) n ≃ₐ[k]
      finiteResidueIntermediateFieldIn k Omega n

def

finiteResidueGaloisIntermediateFieldIn

L89 ↗

LocalClassFieldTheory.finiteResidueGaloisIntermediateFieldIn

Documentation

An actual degree-n finite Galois intermediate field in any residue algebraic closure.

Source context 10 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
open RamificationTheory.Field.absoluteGaloisGroup
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
variable (Omega : Type v) [Field Omega] [Algebra k Omega]
  [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega]

Lean source · full declaration

def finiteResidueGaloisIntermediateFieldIn
    (n : ℕ) [NeZero n] : FiniteGaloisIntermediateField k Omega where
  toIntermediateField := finiteResidueIntermediateFieldIn k Omega n
  finiteDimensional := Module.Finite.equiv
    (finiteResidueExtensionEquivIntermediateIn k Omega n).toLinearEquiv
  isGalois := IsGalois.of_algEquiv
    (finiteResidueExtensionEquivIntermediateIn k Omega n)

theorem

finrank_finiteResidueGaloisIntermediateFieldIn

L100 ↗

LocalClassFieldTheory.finrank_finiteResidueGaloisIntermediateFieldIn

Documentation

States the theorem finrank_finiteResidueGaloisIntermediateFieldIn.

Source context 11 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
open RamificationTheory.Field.absoluteGaloisGroup
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
variable (Omega : Type v) [Field Omega] [Algebra k Omega]
  [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega]
omit [Algebra.IsAlgebraic k Omega] in

Lean source · statement

theorem finrank_finiteResidueGaloisIntermediateFieldIn
    (n : ℕ) [NeZero n] :
    Module.finrank k
        (finiteResidueGaloisIntermediateFieldIn k Omega n) = n

theorem

residueAbsoluteFrobenius_isAlgClosure_injective

L115 ↗

LocalClassFieldTheory.residueAbsoluteFrobenius_isAlgClosure_injective

Documentation

Finite subextensions of every positive degree detect every coordinate of the canonical Frobenius homomorphism on an arbitrary residue algebraic closure.

Source context 10 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
open RamificationTheory.Field.absoluteGaloisGroup
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
variable (Omega : Type v) [Field Omega] [Algebra k Omega]
  [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega]

Lean source · statement

theorem residueAbsoluteFrobenius_isAlgClosure_injective :
    Function.Injective (residueAbsoluteFrobenius k Omega)

theorem

mem_range_algebraMap_iff_frobenius_fixed_in

L148 ↗

LocalClassFieldTheory.mem_range_algebraMap_iff_frobenius_fixed_in

Documentation

In any algebraic closure of a finite field, the fixed points of arithmetic Frobenius are exactly the base field.

Source context 11 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
open RamificationTheory.Field.absoluteGaloisGroup
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
variable (Omega : Type v) [Field Omega] [Algebra k Omega]
  [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega]
omit [IsAlgClosed Omega] in

Lean source · statement

theorem mem_range_algebraMap_iff_frobenius_fixed_in
    (x : Omega) :
    x ∈ Set.range (algebraMap k Omega) ↔
      FiniteField.frobeniusAlgEquivOfAlgebraic k Omega x = x

def

residueAbsoluteFrobeniusRangeIn

L173 ↗

LocalClassFieldTheory.residueAbsoluteFrobeniusRangeIn

Documentation

The compact image of the intrinsic Frobenius homomorphism.

Source context 10 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
open RamificationTheory.Field.absoluteGaloisGroup
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
variable (Omega : Type v) [Field Omega] [Algebra k Omega]
  [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega]

Lean source · full declaration

def residueAbsoluteFrobeniusRangeIn :
    ClosedSubgroup (Omega ≃ₐ[k] Omega) where
  toSubgroup := (residueAbsoluteFrobenius k Omega).toMonoidHom.range
  isClosed' := by
    change IsClosed (Set.range (residueAbsoluteFrobenius k Omega))
    exact (isCompact_range
      (residueAbsoluteFrobenius k Omega).continuous_toFun).isClosed

theorem

fixedField_residueAbsoluteFrobeniusRangeIn

L182 ↗

LocalClassFieldTheory.fixedField_residueAbsoluteFrobeniusRangeIn

Documentation

The compact Frobenius image fixes precisely the finite base field.

Source context 10 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
open RamificationTheory.Field.absoluteGaloisGroup
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
variable (Omega : Type v) [Field Omega] [Algebra k Omega]
  [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega]

Lean source · statement

theorem fixedField_residueAbsoluteFrobeniusRangeIn :
    IntermediateField.fixedField
        (residueAbsoluteFrobeniusRangeIn k Omega).toSubgroup = ⊥

theorem

residueAbsoluteFrobeniusRangeIn_eq_top

L204 ↗

LocalClassFieldTheory.residueAbsoluteFrobeniusRangeIn_eq_top

Documentation

The intrinsic Frobenius image is the whole residue absolute Galois group.

Source context 10 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
open RamificationTheory.Field.absoluteGaloisGroup
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
variable (Omega : Type v) [Field Omega] [Algebra k Omega]
  [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega]

Lean source · statement

theorem residueAbsoluteFrobeniusRangeIn_eq_top :
    (residueAbsoluteFrobeniusRangeIn k Omega).toSubgroup = ⊤

theorem

residueAbsoluteFrobenius_isAlgClosure_surjective

L213 ↗

LocalClassFieldTheory.residueAbsoluteFrobenius_isAlgClosure_surjective

Documentation

The intrinsic Frobenius homomorphism is surjective.

Source context 10 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
open RamificationTheory.Field.absoluteGaloisGroup
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
variable (Omega : Type v) [Field Omega] [Algebra k Omega]
  [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega]

Lean source · statement

theorem residueAbsoluteFrobenius_isAlgClosure_surjective :
    Function.Surjective (residueAbsoluteFrobenius k Omega)

def

residueAbsoluteFrobeniusEquivIn

L224 ↗

LocalClassFieldTheory.residueAbsoluteFrobeniusEquivIn

Documentation

Arithmetic Frobenius gives the canonical topological equivalence between ZHatMul and the Galois group of any algebraic closure of a finite field.

Source context 10 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
open RamificationTheory.Field.absoluteGaloisGroup
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
variable (Omega : Type v) [Field Omega] [Algebra k Omega]
  [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega]

Lean source · full declaration

def residueAbsoluteFrobeniusEquivIn :
    ZHatMul ≃ₜ* (Omega ≃ₐ[k] Omega) where
  toMulEquiv := MulEquiv.ofBijective
    (residueAbsoluteFrobenius k Omega).toMonoidHom
    ⟨residueAbsoluteFrobenius_isAlgClosure_injective k Omega,
      residueAbsoluteFrobenius_isAlgClosure_surjective k Omega⟩
  continuous_toFun := (residueAbsoluteFrobenius k Omega).continuous_toFun
  continuous_invFun :=
    Continuous.continuous_symm_of_equiv_compact_to_t2
      (f := (MulEquiv.ofBijective
        (residueAbsoluteFrobenius k Omega).toMonoidHom
        ⟨residueAbsoluteFrobenius_isAlgClosure_injective k Omega,
          residueAbsoluteFrobenius_isAlgClosure_surjective k Omega⟩).toEquiv)
      (residueAbsoluteFrobenius k Omega).continuous_toFun

def

residueAbsoluteDegreeIn

L241 ↗

LocalClassFieldTheory.residueAbsoluteDegreeIn

Documentation

Finite local reciprocity, intrinsic residue degree. This is the inverse of arithmetic Frobenius coordinates on the actual residue algebraic closure.

Source context 10 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
open RamificationTheory.Field.absoluteGaloisGroup
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
variable (Omega : Type v) [Field Omega] [Algebra k Omega]
  [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega]

Lean source · statement

def residueAbsoluteDegreeIn :
    (Omega ≃ₐ[k] Omega) →ₜ* ZHatMul

theorem

residueAbsoluteDegreeIn_semilinear_conjugation

L250 ↗

LocalClassFieldTheory.residueAbsoluteDegreeIn_semilinear_conjugation

Documentation

Intrinsic residue degree is unchanged by simultaneous semilinear equivalence of the finite residue base and its algebraic closure. The conjugate automorphism is written locally in the statement, so no parallel restriction or automorphism-conjugation API is introduced.

Source context 10 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
open RamificationTheory.Field.absoluteGaloisGroup
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
variable (Omega : Type v) [Field Omega] [Algebra k Omega]
  [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega]

Lean source · full declaration

theorem residueAbsoluteDegreeIn_semilinear_conjugation
    {k' : Type u} {Omega' : Type v}
    [Field k'] [Fintype k']
    [Field Omega'] [Algebra k' Omega']
    [Algebra.IsAlgebraic k' Omega'] [IsAlgClosed Omega']
    (tau : k ≃+* k') (e : Omega ≃+* Omega')
    (he : ∀ x : k,
      e (algebraMap k Omega x) = algebraMap k' Omega' (tau x))
    (sigma : Omega ≃ₐ[k] Omega) :
    let sigma' : Omega' ≃ₐ[k'] Omega' :=
      { e.symm.trans (sigma.toRingEquiv.trans e) with
        commutes' := fun x => by
          change e (sigma (e.symm (algebraMap k' Omega' x))) =
            algebraMap k' Omega' x
          have hpre :
              e.symm (algebraMap k' Omega' x) =
                algebraMap k Omega (tau.symm x) := by
            apply e.injective
            rw [e.apply_symm_apply, he, tau.apply_symm_apply]
          rw [hpre, sigma.commutes, he, tau.apply_symm_apply] }
    residueAbsoluteDegreeIn k' Omega' sigma' =
      residueAbsoluteDegreeIn k Omega sigma := by
  let conjugate (g : Omega ≃ₐ[k] Omega) :
      Omega' ≃ₐ[k'] Omega' :=
    AlgEquiv.ofRingEquiv
      (f := e.symm.trans (g.toRingEquiv.trans e)) (fun x => by
        change e (g (e.symm (algebraMap k' Omega' x))) =
          algebraMap k' Omega' x
        have hpre :
            e.symm (algebraMap k' Omega' x) =
              algebraMap k Omega (tau.symm x) := by
          apply e.injective
          rw [e.apply_symm_apply, he, tau.apply_symm_apply]
        rw [hpre, g.commutes, he, tau.apply_symm_apply])
  have conjugate_one : conjugate 1 = 1 := by
    apply AlgEquiv.ext
    intro x
    simp [conjugate]
  have conjugate_mul (g h : Omega ≃ₐ[k] Omega) :
      conjugate (g * h) = conjugate g * conjugate h := by
    apply AlgEquiv.ext
    intro x
    simp [conjugate, AlgEquiv.mul_apply]
  let conjugation :
      (Omega ≃ₐ[k] Omega) →* (Omega' ≃ₐ[k'] Omega') :=
    { toFun := conjugate
      map_one' := conjugate_one
      map_mul' := conjugate_mul }
  let conjugationContinuous :
      (Omega ≃ₐ[k] Omega) →ₜ* (Omega' ≃ₐ[k'] Omega') :=
    { toMonoidHom := conjugation
      continuous_toFun :=
        RamificationTheory.Field.absoluteGaloisGroup.semilinear_conjugation_continuous
          tau e he conjugation (fun _ => rfl) }
  let lhs : ZHatMul →ₜ* (Omega' ≃ₐ[k'] Omega') :=
    conjugationContinuous.comp (residueAbsoluteFrobenius k Omega)
  let rhs : ZHatMul →ₜ* (Omega' ≃ₐ[k'] Omega') :=
    residueAbsoluteFrobenius k' Omega'
  have hgenerator :
      lhs (Multiplicative.ofAdd (1 : ZHat)) =
        rhs (Multiplicative.ofAdd (1 : ZHat)) := by
    change conjugation
        (residueAbsoluteFrobenius k Omega
          (Multiplicative.ofAdd (1 : ZHat))) =
      residueAbsoluteFrobenius k' Omega'
        (Multiplicative.ofAdd (1 : ZHat))
    rw [residueAbsoluteFrobenius_one, residueAbsoluteFrobenius_one]
    apply AlgEquiv.ext
    intro x
    change e ((e.symm x) ^ Fintype.card k) =
      x ^ Fintype.card k'
    rw [map_pow, e.apply_symm_apply,
      Fintype.card_congr tau.toEquiv]
  let iota : Multiplicative ℤ →* ZHatMul :=
    AddMonoidHom.toMultiplicative
      (Int.castRingHom ZHat).toAddMonoidHom
  have hiota : DenseRange iota := by
    have hOfAdd :
        DenseRange (Multiplicative.ofAdd : ZHat → ZHatMul) :=
      (show Function.Surjective
          (Multiplicative.ofAdd : ZHat → ZHatMul) from
        fun x => ⟨Multiplicative.toAdd x, rfl⟩).denseRange
    have hCast :
        DenseRange
          (Multiplicative.ofAdd ∘ fun a : ℤ => (a : ZHat)) :=
      hOfAdd.comp denseRange_intCast_zHat continuous_id
    have hToAdd :
        DenseRange (Multiplicative.toAdd : Multiplicative ℤ → ℤ) :=
      (show Function.Surjective
          (Multiplicative.toAdd : Multiplicative ℤ → ℤ) from
        fun a => ⟨Multiplicative.ofAdd a, rfl⟩).denseRange
    simpa [iota, Function.comp_def] using
      hCast.comp hToAdd continuous_of_discreteTopology
  have hcomp :
      lhs.toMonoidHom.comp iota = rhs.toMonoidHom.comp iota := by
    apply MonoidHom.ext_mint
    simpa [iota] using hgenerator
  have heq (w : ZHatMul) : lhs w = rhs w := by
    have hfun :=
      hiota.equalizer lhs.continuous_toFun rhs.continuous_toFun <| by
        funext n
        exact DFunLike.congr_fun hcomp n
    exact congrFun hfun w
  let z := residueAbsoluteDegreeIn k Omega sigma
  have hz :
      conjugation (residueAbsoluteFrobenius k Omega z) =
        residueAbsoluteFrobenius k' Omega' z := by
    exact heq z
  apply (residueAbsoluteFrobeniusEquivIn k' Omega').injective
  change
    (residueAbsoluteFrobeniusEquivIn k' Omega')
        ((residueAbsoluteFrobeniusEquivIn k' Omega').symm
          (conjugation sigma)) =
      (residueAbsoluteFrobeniusEquivIn k' Omega')
        ((residueAbsoluteFrobeniusEquivIn k Omega).symm sigma)
  rw [(residueAbsoluteFrobeniusEquivIn k' Omega').apply_symm_apply]
  change conjugation sigma =
    residueAbsoluteFrobenius k' Omega' z
  have hsigma :
      sigma = residueAbsoluteFrobenius k Omega z := by
    change sigma =
      (residueAbsoluteFrobeniusEquivIn k Omega)
        ((residueAbsoluteFrobeniusEquivIn k Omega).symm sigma)
    exact
      ((residueAbsoluteFrobeniusEquivIn k Omega).apply_symm_apply sigma).symm
  exact (congrArg conjugation hsigma).trans hz

theorem

residueAbsoluteFrobenius_restrictScalars

L381 ↗

LocalClassFieldTheory.residueAbsoluteFrobenius_restrictScalars

Documentation

Arithmetic Frobenius is compatible with changing the finite residue base from k to a finite intermediate field E: after forgetting the E-linear structure, the Frobenius coordinate is multiplied by [E : k].

Source context 10 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
open RamificationTheory.Field.absoluteGaloisGroup
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
variable (Omega : Type v) [Field Omega] [Algebra k Omega]
  [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega]

Lean source · full declaration

theorem residueAbsoluteFrobenius_restrictScalars
    (E : IntermediateField k Omega) [FiniteDimensional k E]
    (z : ZHatMul) :
    letI : Finite E := Module.finite_of_finite k
    letI : Fintype E := Fintype.ofFinite E
    (residueAbsoluteFrobenius E Omega z).restrictScalars k =
      residueAbsoluteFrobenius k Omega
        (Multiplicative.ofAdd
          ((Module.finrank k E) • z.toAdd)) := by
  let : Finite E := Module.finite_of_finite k
  let : Fintype E := Fintype.ofFinite E
  let scaleHom : ZHatMul →* ZHatMul :=
    AddMonoidHom.toMultiplicative
      (zHatMulNat (Module.finrank k E)).toAddMonoidHom
  let scale : ZHatMul →ₜ* ZHatMul :=
    { toMonoidHom := scaleHom
      continuous_toFun :=
        continuous_ofAdd.comp
          ((zHatMulNat (Module.finrank k E)).continuous_toFun.comp
            continuous_toAdd) }
  let inclusion : (Omega ≃ₐ[E] Omega) →ₜ* (Omega ≃ₐ[k] Omega) :=
    { toMonoidHom := ofIntermediateFieldInExtension E
      continuous_toFun := ofIntermediateFieldInExtension_continuous E }
  let lhs : ZHatMul →ₜ* (Omega ≃ₐ[k] Omega) :=
    inclusion.comp (residueAbsoluteFrobenius E Omega)
  let rhs : ZHatMul →ₜ* (Omega ≃ₐ[k] Omega) :=
    (residueAbsoluteFrobenius k Omega).comp scale
  have hgenerator :
      lhs (Multiplicative.ofAdd (1 : ZHat)) =
        rhs (Multiplicative.ofAdd (1 : ZHat)) := by
    change
      (residueAbsoluteFrobenius E Omega
          (Multiplicative.ofAdd (1 : ZHat))).restrictScalars k =
        residueAbsoluteFrobenius k Omega
          (Multiplicative.ofAdd
            ((Module.finrank k E) • (1 : ZHat)))
    rw [residueAbsoluteFrobenius_one]
    have hscale :
        Multiplicative.ofAdd
            ((Module.finrank k E) • (1 : ZHat)) =
          (Multiplicative.ofAdd (1 : ZHat)) ^ Module.finrank k E := by
      apply Multiplicative.ext
      simp
    rw [hscale, map_pow, residueAbsoluteFrobenius_one]
    apply AlgEquiv.ext
    intro x
    change
      FiniteField.frobeniusAlgEquivOfAlgebraic E Omega x =
        (FiniteField.frobeniusAlgEquivOfAlgebraic k Omega ^
          Module.finrank k E) x
    rw [FiniteField.coe_frobeniusAlgEquivOfAlgebraic,
      AlgEquiv.coe_pow,
      FiniteField.coe_frobeniusAlgEquivOfAlgebraic_iterate,
      Module.card_eq_pow_finrank (K := k) (V := E)]
  let iota : Multiplicative ℤ →* ZHatMul :=
    AddMonoidHom.toMultiplicative
      (Int.castRingHom ZHat).toAddMonoidHom
  have hiota : DenseRange iota := by
    have hOfAdd :
        DenseRange (Multiplicative.ofAdd : ZHat → ZHatMul) :=
      (show Function.Surjective
          (Multiplicative.ofAdd : ZHat → ZHatMul) from
        fun x => ⟨Multiplicative.toAdd x, rfl⟩).denseRange
    have hCast :
        DenseRange
          (Multiplicative.ofAdd ∘ fun a : ℤ => (a : ZHat)) :=
      hOfAdd.comp denseRange_intCast_zHat continuous_id
    have hToAdd :
        DenseRange (Multiplicative.toAdd : Multiplicative ℤ → ℤ) :=
      (show Function.Surjective
          (Multiplicative.toAdd : Multiplicative ℤ → ℤ) from
        fun a => ⟨Multiplicative.ofAdd a, rfl⟩).denseRange
    simpa [iota, Function.comp_def] using
      hCast.comp hToAdd continuous_of_discreteTopology
  have hcomp :
      lhs.toMonoidHom.comp iota = rhs.toMonoidHom.comp iota := by
    apply MonoidHom.ext_mint
    simpa [iota] using hgenerator
  have heq (w : ZHatMul) : lhs w = rhs w := by
    have hfun :=
      hiota.equalizer lhs.continuous_toFun rhs.continuous_toFun <| by
        funext n
        exact DFunLike.congr_fun hcomp n
    exact congrFun hfun w
  exact heq z

theorem

residueAbsoluteDegreeIn_restrictScalars

L469 ↗

LocalClassFieldTheory.residueAbsoluteDegreeIn_restrictScalars

Documentation

The intrinsic absolute residue degree has the corresponding finite-base-change formula.

Source context 10 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
open RamificationTheory.Field.absoluteGaloisGroup
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
variable (Omega : Type v) [Field Omega] [Algebra k Omega]
  [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega]

Lean source · full declaration

theorem residueAbsoluteDegreeIn_restrictScalars
    (E : IntermediateField k Omega) [FiniteDimensional k E]
    (sigma : Omega ≃ₐ[E] Omega) :
    letI : Finite E := Module.finite_of_finite k
    letI : Fintype E := Fintype.ofFinite E
    residueAbsoluteDegreeIn k Omega (sigma.restrictScalars k) =
      Multiplicative.ofAdd
        ((Module.finrank k E) •
          (residueAbsoluteDegreeIn E Omega sigma).toAdd) := by
  let : Finite E := Module.finite_of_finite k
  let : Fintype E := Fintype.ofFinite E
  apply (residueAbsoluteFrobeniusEquivIn k Omega).injective
  change
    (residueAbsoluteFrobeniusEquivIn k Omega)
        ((residueAbsoluteFrobeniusEquivIn k Omega).symm
          (sigma.restrictScalars k)) =
      (residueAbsoluteFrobeniusEquivIn k Omega)
        (Multiplicative.ofAdd
          ((Module.finrank k E) •
            ((residueAbsoluteFrobeniusEquivIn E Omega).symm sigma).toAdd))
  rw [(residueAbsoluteFrobeniusEquivIn k Omega).apply_symm_apply]
  change sigma.restrictScalars k =
    residueAbsoluteFrobenius k Omega
      (Multiplicative.ofAdd
        ((Module.finrank k E) •
          ((residueAbsoluteFrobeniusEquivIn E Omega).symm sigma).toAdd))
  rw [← residueAbsoluteFrobenius_restrictScalars]
  exact congrArg (fun g : Omega ≃ₐ[E] Omega => g.restrictScalars k)
    ((residueAbsoluteFrobeniusEquivIn E Omega).apply_symm_apply sigma).symm

theorem

residueAbsoluteDegreeIn_frobenius

L501 ↗

LocalClassFieldTheory.residueAbsoluteDegreeIn_frobenius

Documentation

The intrinsic degree map sends arithmetic Frobenius to 1.

Source context 10 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
open RamificationTheory.Field.absoluteGaloisGroup
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
variable (Omega : Type v) [Field Omega] [Algebra k Omega]
  [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega]

Lean source · statement

theorem residueAbsoluteDegreeIn_frobenius :
    residueAbsoluteDegreeIn k Omega
        (FiniteField.frobeniusAlgEquivOfAlgebraic k Omega) =
      Multiplicative.ofAdd (1 : ZHat)

theorem

finiteResidueFrobeniusExponentEquiv_symm_restrict_in

L515 ↗

LocalClassFieldTheory.finiteResidueFrobeniusExponentEquiv_symm_restrict_in

Documentation

Finite-coordinate compatibility for the intrinsic residue degree.

Source context 10 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
open RamificationTheory.Field.absoluteGaloisGroup
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
variable (Omega : Type v) [Field Omega] [Algebra k Omega]
  [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega]

Lean source · full declaration

theorem finiteResidueFrobeniusExponentEquiv_symm_restrict_in
    (sigma : Omega ≃ₐ[k] Omega)
    (E : FiniteGaloisIntermediateField k Omega) :
    letI : Finite E := Module.finite_of_finite k
    (finiteResidueFrobeniusExponentEquiv k E).symm
        (AlgEquiv.restrictNormalHom E sigma) =
      Multiplicative.ofAdd
        (zHatReduction (Module.finrank k E) Module.finrank_pos
          (residueAbsoluteDegreeIn k Omega sigma).toAdd) := by
  let : Finite E := Module.finite_of_finite k
  apply (finiteResidueFrobeniusExponentEquiv k E).injective
  rw [(finiteResidueFrobeniusExponentEquiv k E).apply_symm_apply]
  change AlgEquiv.restrictNormalHom E sigma =
    finiteResidueFrobeniusIntermediate k Omega E
      (residueAbsoluteDegreeIn k Omega sigma)
  rw [← restrictNormalHom_residueAbsoluteFrobenius]
  congr 1
  exact ((residueAbsoluteFrobeniusEquivIn k Omega).apply_symm_apply sigma).symm

Module documentation

Finite local reciprocity: degree coordinates on any residue algebraic closure

Declarations