Module

Frobenius.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Degree.Frobenius

24 declarations indexed from sourceView source ↗

Module documentation

normalized degree and Frobenius theory: normalized degree maps and Frobenius

For a field of finite residue degree, this file constructs the map d_K = (1 / f_K) d; division is performed only after proving that d(G_K) = f_K ℤ̂. The Frobenius is then the unique class mapping to 1.

Imports1

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Degree.Fields

Imported by4

def

fieldImageAdd

L28 ↗

ClassFormation.DegreeData.fieldImageAdd

Documentation

The image d(G_K), written additively inside ℤ̂.

Source context 4 commands

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

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

Lean source · statement

def fieldImageAdd (D : DegreeData G) (K : ClosedSubgroup G) : AddSubgroup ZHat

theorem

fieldImageAdd_index

L33 ↗

ClassFormation.DegreeData.fieldImageAdd_index

Documentation

The additive degree image has index equal to the field's positive residue degree.

Source context 4 commands

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

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

Lean source · statement

theorem fieldImageAdd_index (D : DegreeData G)
    (K : FiniteResidueAbstractField D) :
    (D.fieldImageAdd K.field).index = (K.residueDegree : ℕ)

theorem

fieldImageAdd_eq_mulNat_range

L42 ↗

ClassFormation.DegreeData.fieldImageAdd_eq_mulNat_range

Documentation

Finite residue degree identifies d(G_K) with f_K ℤ̂.

Source context 4 commands

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

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

Lean source · statement

theorem fieldImageAdd_eq_mulNat_range (D : DegreeData G)
    (K : FiniteResidueAbstractField D) :
    D.fieldImageAdd K.field =
      (zHatMulNat (K.residueDegree : ℕ)).toAddMonoidHom.range

def

restrictedDegreeInMulNatRange

L51 ↗

ClassFormation.DegreeData.restrictedDegreeInMulNatRange

Documentation

The raw value d(k) regarded as an element of the subgroup f_K ℤ̂.

Source context 4 commands

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

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

Lean source · statement

def restrictedDegreeInMulNatRange (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (k : K.field.toSubgroup) :
    (zHatMulNat (K.residueDegree : ℕ)).toAddMonoidHom.range

theorem

restrictedDegreeInMulNatRange_coe

L61 ↗

ClassFormation.DegreeData.restrictedDegreeInMulNatRange_coe

Documentation

The restricted degree in the natural-multiple range has the original additive value.

Source context 4 commands

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

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

Lean source · statement

theorem restrictedDegreeInMulNatRange_coe (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (k : K.toSubgroup) :
    (D.restrictedDegreeInMulNatRange K k).1 = (D.degree k.1).toAdd

def

normalizedDegree

L67 ↗

ClassFormation.DegreeData.normalizedDegree

Documentation

The normalized degree map d_K = (1 / f_K)d.

Source context 4 commands

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

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

Lean source · full declaration

def normalizedDegree (D : DegreeData G) (K : FiniteResidueAbstractField D) :
    K.field.toSubgroup →ₜ* ZHatMul where
  toFun k := Multiplicative.ofAdd
    (zHatDivide (K.residueDegree : ℕ) K.residueDegree.property
      (D.restrictedDegreeInMulNatRange K k))
  map_one' := by
    apply Multiplicative.ext
    change zHatDivide (K.residueDegree : ℕ) K.residueDegree.property
      (D.restrictedDegreeInMulNatRange K 1) = 0
    rw [show D.restrictedDegreeInMulNatRange K 1 = 0 by
      apply Subtype.ext
      exact congrArg Multiplicative.toAdd (map_one D.degree)]
    exact map_zero (zHatDivide (K.residueDegree : ℕ) K.residueDegree.property)
  map_mul' x y := by
    apply Multiplicative.ext
    change zHatDivide (K.residueDegree : ℕ) K.residueDegree.property
        (D.restrictedDegreeInMulNatRange K (x * y)) =
      zHatDivide (K.residueDegree : ℕ) K.residueDegree.property
          (D.restrictedDegreeInMulNatRange K x) +
        zHatDivide (K.residueDegree : ℕ) K.residueDegree.property
          (D.restrictedDegreeInMulNatRange K y)
    rw [show D.restrictedDegreeInMulNatRange K (x * y) =
        D.restrictedDegreeInMulNatRange K x +
          D.restrictedDegreeInMulNatRange K y by
      apply Subtype.ext
      exact congrArg Multiplicative.toAdd
        (map_mul D.degree x.1 y.1)]
    exact map_add (zHatDivide (K.residueDegree : ℕ) K.residueDegree.property) _ _
  continuous_toFun := by
    apply (map_continuous
      (zHatDivide (K.residueDegree : ℕ) K.residueDegree.property)).comp
    exact Continuous.subtype_mk
      (D.restrictedDegree K.field).continuous_toFun
      (fun k => (D.restrictedDegreeInMulNatRange K k).2)

theorem

normalizedDegree_apply_toAdd

L104 ↗

ClassFormation.DegreeData.normalizedDegree_apply_toAdd

Documentation

The additive coordinate of normalized degree is obtained by dividing by the residue degree.

Source context 4 commands

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

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

Lean source · statement

theorem normalizedDegree_apply_toAdd (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (k : K.field.toSubgroup) :
    (D.normalizedDegree K k).toAdd =
      zHatDivide (K.residueDegree : ℕ) K.residueDegree.property
        (D.restrictedDegreeInMulNatRange K k)

theorem

residueDegree_nsmul_normalizedDegree

L112 ↗

ClassFormation.DegreeData.residueDegree_nsmul_normalizedDegree

Documentation

The defining identity f_K d_K = d.

Source context 4 commands

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

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

Lean source · statement

theorem residueDegree_nsmul_normalizedDegree (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (k : K.field.toSubgroup) :
    (K.residueDegree : ℕ) • (D.normalizedDegree K k).toAdd =
      (D.degree k.1).toAdd

theorem

normalizedDegree_surjective

L121 ↗

ClassFormation.DegreeData.normalizedDegree_surjective

Documentation

The normalized map is surjective, exactly as asserted before the normalized Frobenius definition.

Source context 4 commands

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

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

Lean source · statement

theorem normalizedDegree_surjective (D : DegreeData G)
    (K : FiniteResidueAbstractField D) :
    Function.Surjective (D.normalizedDegree K)

theorem

normalizedDegree_ker

L141 ↗

ClassFormation.DegreeData.normalizedDegree_ker

Documentation

The kernel of d_K is the inertia group I_K.

Source context 4 commands

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

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

Lean source · statement

theorem normalizedDegree_ker (D : DegreeData G)
    (K : FiniteResidueAbstractField D) :
    (D.normalizedDegree K).toMonoidHom.ker = D.fieldInertiaWithin K.field

theorem

fieldInertiaWithin_le_normalizedDegree_ker

L162 ↗

ClassFormation.DegreeData.fieldInertiaWithin_le_normalizedDegree_ker

Source context 4 commands

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

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

Lean source · statement

theorem fieldInertiaWithin_le_normalizedDegree_ker
    (D : DegreeData G) (K : FiniteResidueAbstractField D) :
    D.fieldInertiaWithin K.field ≤ (D.normalizedDegree K).toMonoidHom.ker

def

maximalUnramifiedDegreeEquiv

L168 ↗

ClassFormation.DegreeData.maximalUnramifiedDegreeEquiv

Documentation

The isomorphism d_K : G(\widetilde K|K) ≃ ℤ̂.

Source context 4 commands

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

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

Lean source · statement

def maximalUnramifiedDegreeEquiv (D : DegreeData G)
    (K : FiniteResidueAbstractField D) :
    (K.field.toSubgroup ⧸ D.fieldInertiaWithin K.field) ≃* ZHatMul

theorem

maximalUnramifiedDegreeEquiv_mk

L196 ↗

ClassFormation.DegreeData.maximalUnramifiedDegreeEquiv_mk

Documentation

On quotient representatives, the maximal-unramified degree equivalence is normalized degree.

Source context 4 commands

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

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

Lean source · statement

theorem maximalUnramifiedDegreeEquiv_mk (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (k : K.field.toSubgroup) :
    D.maximalUnramifiedDegreeEquiv K (QuotientGroup.mk k) =
      D.normalizedDegree K k

def

frobenius

L204 ↗

ClassFormation.DegreeData.frobenius

Documentation

the normalized Frobenius definition. The Frobenius over K, characterized by d_K(φ_K)=1.

Source context 4 commands

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

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

Lean source · statement

def frobenius (D : DegreeData G) (K : FiniteResidueAbstractField D) :
    K.field.toSubgroup ⧸ D.fieldInertiaWithin K.field

theorem

maximalUnramifiedDegreeEquiv_frobenius

L211 ↗

ClassFormation.DegreeData.maximalUnramifiedDegreeEquiv_frobenius

Documentation

The maximal-unramified degree equivalence sends Frobenius to the generator one.

Source context 4 commands

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

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

Lean source · statement

theorem maximalUnramifiedDegreeEquiv_frobenius (D : DegreeData G)
    (K : FiniteResidueAbstractField D) :
    D.maximalUnramifiedDegreeEquiv K (D.frobenius K) =
      Multiplicative.ofAdd (1 : ZHat)

theorem

eq_frobenius_iff

L218 ↗

ClassFormation.DegreeData.eq_frobenius_iff

Documentation

Uniqueness clause in the normalized Frobenius definition.

Source context 4 commands

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

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

Lean source · statement

theorem eq_frobenius_iff (D : DegreeData G)
    (K : FiniteResidueAbstractField D)
    (σ : K.field.toSubgroup ⧸ D.fieldInertiaWithin K.field) :
    σ = D.frobenius K ↔
      D.maximalUnramifiedDegreeEquiv K σ =
        Multiplicative.ofAdd (1 : ZHat)

theorem

residueDegree_mul_absoluteResidueDegree

L233 ↗

ClassFormation.DegreeData.FiniteResidueAbstractExtension.residueDegree_mul_absoluteResidueDegree

Documentation

For a finite extension, its positive residue degree times the absolute residue degree of the base is the absolute residue degree of the field.

Source context 4 commands

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

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

Lean source · statement

theorem FiniteResidueAbstractExtension.residueDegree_mul_absoluteResidueDegree
    (D : DegreeData G) (E : FiniteResidueAbstractExtension D) :
    (E.residueDegree : ℕ) * (E.base.residueDegree : ℕ) =
      (E.field.residueDegree : ℕ)

theorem

frobeniusRestrictionNaturality_residueDegree

L250 ↗

ClassFormation.DegreeData.frobeniusRestrictionNaturality_residueDegree

Documentation

Frobenius residue-degree compatibility (residue degrees). If f_K and f_L are finite, then f_{L|K} = f_L / f_K.

Source context 4 commands

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

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

Lean source · statement

theorem frobeniusRestrictionNaturality_residueDegree (D : DegreeData G)
    (E : FiniteResidueAbstractExtension D) :
    (E.residueDegree : ℕ) =
      (E.field.residueDegree : ℕ) / (E.base.residueDegree : ℕ)

theorem

frobeniusRestrictionNaturality_normalizedDegree

L260 ↗

ClassFormation.DegreeData.frobeniusRestrictionNaturality_normalizedDegree

Documentation

Frobenius residue-degree compatibility (commutative square). On G_L, the normalized degree maps satisfy d_K = f_{L|K} d_L.

Source context 4 commands

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

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

Lean source · statement

theorem frobeniusRestrictionNaturality_normalizedDegree (D : DegreeData G)
    (E : FiniteResidueAbstractExtension D)
    (l : E.field.field.toSubgroup) :
    (D.normalizedDegree E.base (Subgroup.inclusion E.below l)).toAdd =
      (E.residueDegree : ℕ) •
        (D.normalizedDegree E.field l).toAdd

theorem

fieldInertiaWithin_le_comap_inclusion

L278 ↗

ClassFormation.DegreeData.fieldInertiaWithin_le_comap_inclusion

Source context 4 commands

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

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

Lean source · statement

theorem fieldInertiaWithin_le_comap_inclusion
    (D : DegreeData G) {L K : ClosedSubgroup G}
    (hLK : L.toSubgroup ≤ K.toSubgroup) :
    D.fieldInertiaWithin L ≤
      (D.fieldInertiaWithin K).comap (Subgroup.inclusion hLK)

def

maximalUnramifiedRestriction

L287 ↗

ClassFormation.DegreeData.maximalUnramifiedRestriction

Documentation

Restriction G(\widetilde L/L) → G(\widetilde K/K) for L | K.

Source context 4 commands

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

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

Lean source · statement

def maximalUnramifiedRestriction (D : DegreeData G) {L K : ClosedSubgroup G}
    (hLK : L.toSubgroup ≤ K.toSubgroup) :
    (L.toSubgroup ⧸ D.fieldInertiaWithin L) →*
      (K.toSubgroup ⧸ D.fieldInertiaWithin K)

theorem

maximalUnramifiedRestriction_mk

L297 ↗

ClassFormation.DegreeData.maximalUnramifiedRestriction_mk

Documentation

Maximal-unramified restriction sends a quotient representative to its restricted representative.

Source context 4 commands

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

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

Lean source · statement

theorem maximalUnramifiedRestriction_mk (D : DegreeData G)
    {L K : ClosedSubgroup G} (hLK : L.toSubgroup ≤ K.toSubgroup)
    (l : L.toSubgroup) :
    D.maximalUnramifiedRestriction hLK (QuotientGroup.mk l) =
      QuotientGroup.mk (Subgroup.inclusion hLK l)

theorem

frobeniusRestrictionNaturality_quotient_square

L305 ↗

ClassFormation.DegreeData.frobeniusRestrictionNaturality_quotient_square

Documentation

The quotient form of the commutative square in Frobenius residue-degree compatibility.

Source context 4 commands

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

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

Lean source · statement

theorem frobeniusRestrictionNaturality_quotient_square (D : DegreeData G)
    (E : FiniteResidueAbstractExtension D)
    (σ : E.field.field.toSubgroup ⧸ D.fieldInertiaWithin E.field.field) :
    (D.maximalUnramifiedDegreeEquiv E.base
      (D.maximalUnramifiedRestriction E.below σ)).toAdd =
      (E.residueDegree : ℕ) •
        (D.maximalUnramifiedDegreeEquiv E.field σ).toAdd

theorem

frobenius_restriction_eq_power

L318 ↗

ClassFormation.DegreeData.frobenius_restriction_eq_power

Documentation

The final assertion of Frobenius residue-degree compatibility: φ_L|_{\widetilde K} = φ_K ^ f_{L|K}.

Source context 4 commands

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

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

Lean source · statement

theorem frobenius_restriction_eq_power (D : DegreeData G)
    (E : FiniteResidueAbstractExtension D) :
    D.maximalUnramifiedRestriction E.below (D.frobenius E.field) =
      (D.frobenius E.base) ^ (E.residueDegree : ℕ)

Module documentation

normalized degree and Frobenius theory: normalized degree maps and Frobenius

Declarations