Module

IdeleClassDirectLimitFixedPointDescent.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.IdeleClassDirectLimitFixedPointDescent

3 declarations indexed from sourceView source ↗

Module documentation

Finite-level and direct-limit fixed-point descent endpoints

This endpoint leaf turns the reusable fixed-point comparisons into actual descent witnesses first at one finite Galois level and then in the rational idèle-class direct limit.

Imports1

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.IdeleClassDirectLimitFixedPointDescentCore

Imported by2

theorem

rationalRelativeIdeleClass_descent_square

L27 ↗

GlobalClassFieldTheory.Reciprocity.rationalRelativeIdeleClass_descent_square

Documentation

The tower base-change equivalence carries extension of a rational relative idele class along K ↪ U to relative class inclusion of the corresponding idele class of K. This is the actual commuting square used for descent.

Source context 3 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

theorem rationalRelativeIdeleClass_descent_square
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K]
    (U : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ))
    [Algebra K U]
    [IsScalarTower ℚ K U]
    [FiniteDimensional K U]
    [IsGalois K U]
    (hKU :
      K ≤ (U : IntermediateField ℚ (SeparableClosure ℚ)))
    (h_algebraMap : ∀ x : K,
      ((algebraMap K U x : U) : SeparableClosure ℚ) =
        (x : SeparableClosure ℚ))
    (q : IdeleClassGroup K) :
    rationalRelativeIdeleClassTowerBaseChangeEquiv K U
        (RelativeIdeleGroup.classEmbedding (K := ℚ) (L := K) (M := U)
          (IntermediateField.inclusion hKU)
          ((_root_.relativeIdeleClassBaseChangeMulEquiv
            (K := ℚ) (L := K)).symm q)) =
      RelativeIdeleGroup.classInclusion K U q

theorem

rationalRelativeIdeleClass_exists_descent_of_tower_fixed

L97 ↗

GlobalClassFieldTheory.Reciprocity.rationalRelativeIdeleClass_exists_descent_of_tower_fixed

Documentation

A rational relative idele class at a finite Galois level whose actual tower base change is fixed over K descends to an actual idele class of K. The conclusion is the commuting square with relative scalar extension, not merely an abstract preimage.

Source context 3 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

theorem rationalRelativeIdeleClass_exists_descent_of_tower_fixed
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K]
    (U : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ))
    [Algebra K U]
    [IsScalarTower ℚ K U]
    [FiniteDimensional K U]
    [IsGalois K U]
    (hKU :
      K ≤ (U : IntermediateField ℚ (SeparableClosure ℚ)))
    (h_algebraMap : ∀ x : K,
      ((algebraMap K U x : U) : SeparableClosure ℚ) =
        (x : SeparableClosure ℚ))
    (d : RelativeIdeleGroup.ClassGroup ℚ U)
    (hd_fixed :
      towerRelativeIdeleClassBaseChangeMulEquiv ℚ K U
            ((TowerRelativeIdeleGroup.classGroupEquiv
              ℚ K U).symm d) ∈
        RelativeIdeleGroup.galoisFixedClassSubgroup K U) :
    ∃ q : IdeleClassGroup K,
      RelativeIdeleGroup.classEmbedding (K := ℚ) (L := K) (M := U)
          (IntermediateField.inclusion hKU)
          ((_root_.relativeIdeleClassBaseChangeMulEquiv
            (K := ℚ) (L := K)).symm q) =
        d

theorem

rationalDirectLimit_fixed_exists_ideleClass

L168 ↗

GlobalClassFieldTheory.Reciprocity.rationalDirectLimit_fixed_exists_ideleClass

Documentation

Every rational direct-limit idele class fixed by the absolute Galois subgroup over a finite intermediate field comes from an actual idele class of that field. The proof chooses an actual finite-Galois representative and descends it through the tower comparison.

Source context 3 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

theorem rationalDirectLimit_fixed_exists_ideleClass
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K]
    (z : rationalIdeleClassDirectLimit)
    (hz_fixed :
      ∀ σ : SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ,
        σ ∈ K.fixingSubgroup → σ • z = z) :
    ∃ q : IdeleClassGroup K,
      rationalIntermediateIdeleClassToDirectLimit K q = z

Module documentation

Finite-level and direct-limit fixed-point descent endpoints

Declarations

rationalRelativeIdeleClass_descent_square

rationalRelativeIdeleClass_exists_descent_of_tower_fixed

rationalDirectLimit_fixed_exists_ideleClass