Module

GaloisDescent.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.GaloisDescent

9 declarations indexed from sourceView source ↗

Module documentation

Galois descent for idele classes

For a finite Galois extension L/K, the Galois action on relative ideles preserves principal ideles and hence descends to the relative idele class group. Noether's form of Hilbert 90 then shows that every fixed class has a fixed representative. Together with fixed-idele descent, this identifies the fixed subgroup with the embedded copy of C_K.

Imports4

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.ClassGroup
Nyll.GaloisCohomology.Kummer.Concrete.GaloisCohomology
Mathlib.Algebra.Group.Action.Basic
Mathlib.GroupTheory.GroupAction.Quotient

Imported by2

theorem

principalIdele_injective

L39 ↗

RelativeIdeleGroup.principalIdele_injective

Documentation

The diagonal copy of Lˣ in the relative ideles is injective.

Source context 6 commands

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

open scoped NumberField
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] [FiniteDimensional K L] in

Lean source · statement

theorem principalIdele_injective :
    Function.Injective (principalIdele K L)

instance

principalQuotientAction

L50 ↗

RelativeIdeleGroup.principalQuotientAction

Documentation

Galois conjugation preserves the principal-relative-idele congruence, so it acts on the quotient class group.

Source context 6 commands

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

open scoped NumberField
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] [FiniteDimensional K L] in

Lean source · full declaration

instance principalQuotientAction :
    MulAction.QuotientAction (L ≃ₐ[K] L)
      (principalSubgroup K L) where
  inv_mul_mem σ {a a'} h := by
    rcases h with ⟨x, hx⟩
    refine
      ⟨Units.map σ.toRingEquiv.toMonoidHom x, ?_⟩
    rw [← smul_principalIdele K L σ x, hx]
    simp [smul_def]

theorem

smul_class_mk

L62 ↗

RelativeIdeleGroup.smul_class_mk

Source context 6 commands

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

open scoped NumberField
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] [FiniteDimensional K L] in

Lean source · statement

theorem smul_class_mk
    (σ : L ≃ₐ[K] L) (a : RelativeIdeleGroup K L) :
    σ •
        (QuotientGroup.mk'
          (principalSubgroup K L) a) =
      QuotientGroup.mk'
        (principalSubgroup K L) (σ • a)

def

relativeIdeleClassMulDistribMulAction

L74 ↗

RelativeIdeleGroup.relativeIdeleClassMulDistribMulAction

Documentation

The quotient Galois action on relative idele classes, viewed as an action by group automorphisms.

Source context 5 commands

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

open scoped NumberField
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup

Lean source · statement

def relativeIdeleClassMulDistribMulAction :
    MulDistribMulAction (L ≃ₐ[K] L) (ClassGroup K L)

def

galoisFixedClassSubgroup

L84 ↗

RelativeIdeleGroup.galoisFixedClassSubgroup

Documentation

The subgroup of relative idele classes fixed by every Galois automorphism.

Source context 5 commands

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

open scoped NumberField
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup

Lean source · statement

def galoisFixedClassSubgroup :
    Subgroup (ClassGroup K L)

theorem

classInclusion_range_le_galoisFixed

L91 ↗

RelativeIdeleGroup.classInclusion_range_le_galoisFixed

Documentation

Every class coming from C_K is Galois fixed.

Source context 6 commands

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

open scoped NumberField
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] [FiniteDimensional K L] in

Lean source · statement

theorem classInclusion_range_le_galoisFixed :
    (classInclusion K L).range ≤
      galoisFixedClassSubgroup K L

theorem

exists_fixed_representative_of_fixed_class

L111 ↗

RelativeIdeleGroup.exists_fixed_representative_of_fixed_class

Documentation

A Galois-fixed relative idele class has a Galois-fixed idele representative. This is the Noether–Hilbert-90 step in idele-class descent.

Source context 6 commands

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

open scoped NumberField
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] in

Lean source · statement

theorem exists_fixed_representative_of_fixed_class
    [IsGalois K L]
    (a : RelativeIdeleGroup K L)
    (ha :
      ∀ σ : L ≃ₐ[K] L,
        σ •
            QuotientGroup.mk'
              (principalSubgroup K L) a =
          QuotientGroup.mk'
            (principalSubgroup K L) a) :
    ∃ a' : RelativeIdeleGroup K L,
      QuotientGroup.mk'
          (principalSubgroup K L) a' =
        QuotientGroup.mk'
          (principalSubgroup K L) a ∧
      ∀ σ : L ≃ₐ[K] L, σ • a' = a'

theorem

galoisFixed_le_classInclusion_range

L216 ↗

RelativeIdeleGroup.galoisFixed_le_classInclusion_range

Documentation

Every Galois-fixed relative idele class comes from C_K.

Source context 6 commands

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

open scoped NumberField
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] in

Lean source · statement

theorem galoisFixed_le_classInclusion_range
    [IsGalois K L] :
    galoisFixedClassSubgroup K L ≤
      (classInclusion K L).range

theorem

classInclusion_range_eq_galoisFixedClassSubgroup

L249 ↗

RelativeIdeleGroup.classInclusion_range_eq_galoisFixedClassSubgroup

Documentation

Galois descent for idele classes, C_L^{Gal(L/K)} = C_K.

Source context 6 commands

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

open scoped NumberField
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] in

Lean source · statement

theorem classInclusion_range_eq_galoisFixedClassSubgroup
    [IsGalois K L] :
    (classInclusion K L).range =
      galoisFixedClassSubgroup K L

Module documentation

Galois descent for idele classes

Declarations