Module

IdeleClassDirectLimitFixedPointDescentCore.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.IdeleClassDirectLimitFixedPointDescentCore

5 declarations indexed from sourceView source ↗

Module documentation

Descent of fixed rational idele classes

An element of the rational idele-class direct limit which is fixed over a finite intermediate field is represented at a finite Galois level. Its actual tower base change is Galois-fixed, hence descends to an idele class of the intermediate field.

Imports3

Imported by2

theorem

rationalTowerRelativeIdeleClass_fixed_of_directLimit_fixed

L30 ↗

GlobalClassFieldTheory.Reciprocity.rationalTowerRelativeIdeleClass_fixed_of_directLimit_fixed

Documentation

If a finite-level representative of the rational idele-class direct limit is fixed by the absolute Galois subgroup over K, then its actual tower base change from ℚ to K is fixed by Gal(U/K).

Source context 3 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

theorem rationalTowerRelativeIdeleClass_fixed_of_directLimit_fixed
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K]
    (U : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ))
    [Algebra K U]
    [IsScalarTower ℚ K U]
    [FiniteDimensional K U]
    [IsGalois K U]
    (h_algebraMap : ∀ x : K,
      ((algebraMap K U x : U) : SeparableClosure ℚ) =
        (x : SeparableClosure ℚ))
    (d : RelativeIdeleGroup.ClassGroup ℚ U)
    (z : rationalIdeleClassDirectLimit)
    (hzU :
      z = (⟦⟨U, d⟩⟧ : rationalIdeleClassDirectLimit))
    (hz_fixed :
      ∀ σ : SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ,
        σ ∈ K.fixingSubgroup → σ • z = z) :
    towerRelativeIdeleClassBaseChangeMulEquiv ℚ K U
          ((TowerRelativeIdeleGroup.classGroupEquiv
            ℚ K U).symm d) ∈
      RelativeIdeleGroup.galoisFixedClassSubgroup K U

theorem

rationalIntermediateField_algebra_eq_inclusion

L115 ↗

GlobalClassFieldTheory.Reciprocity.rationalIntermediateField_algebra_eq_inclusion

Documentation

An algebra structure on nested rational intermediate fields is the canonical one induced by intermediate-field inclusion whenever its algebra map agrees with the ambient inclusions.

Source context 3 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

theorem rationalIntermediateField_algebra_eq_inclusion
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    (U : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ))
    [Algebra K U]
    (hKU :
      K ≤ (U : IntermediateField ℚ (SeparableClosure ℚ)))
    (h_algebraMap : ∀ x : K,
      ((algebraMap K U x : U) : SeparableClosure ℚ) =
        (x : SeparableClosure ℚ)) :
    (inferInstance : Algebra K U) =
      (IntermediateField.inclusion hKU).toRingHom.toAlgebra

def

rationalRelativeIdeleClassTowerBaseChangeEquiv

L133 ↗

GlobalClassFieldTheory.Reciprocity.rationalRelativeIdeleClassTowerBaseChangeEquiv

Documentation

The actual tower comparison from rational relative idele classes at U to relative idele classes over the intermediate field K.

Source context 3 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

def rationalRelativeIdeleClassTowerBaseChangeEquiv
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K]
    (U : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ))
    [Algebra K U]
    [IsScalarTower ℚ K U]
    [FiniteDimensional K U]
    [IsGalois K U] :
    RelativeIdeleGroup.ClassGroup ℚ U ≃*
      RelativeIdeleGroup.ClassGroup K U

def

rationalIntermediateIdeleClassEquivGaloisFixed

L151 ↗

GlobalClassFieldTheory.Reciprocity.rationalIntermediateIdeleClassEquivGaloisFixed

Documentation

The actual idele class group of K, identified with the subgroup of relative idele classes at U fixed by Gal(U/K). This transports the Herbrand fixed-subgroup target of baseIdeleClassEquivFixed to the concrete Galois-fixed subgroup.

Source context 3 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

def rationalIntermediateIdeleClassEquivGaloisFixed
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K]
    (U : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ))
    [Algebra K U]
    [IsScalarTower ℚ K U]
    [FiniteDimensional K U]
    [IsGalois K U] :
    IdeleClassGroup K ≃*
      RelativeIdeleGroup.galoisFixedClassSubgroup K U

theorem

rationalIntermediateIdeleClassEquivGaloisFixed_coe

L174 ↗

GlobalClassFieldTheory.Reciprocity.rationalIntermediateIdeleClassEquivGaloisFixed_coe

Documentation

Under the concrete fixed-point equivalence, an idele class maps to its actual relative class inclusion.

Source context 3 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

theorem rationalIntermediateIdeleClassEquivGaloisFixed_coe
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K]
    (U : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ))
    [Algebra K U]
    [IsScalarTower ℚ K U]
    [FiniteDimensional K U]
    [IsGalois K U]
    (q : IdeleClassGroup K) :
    ((rationalIntermediateIdeleClassEquivGaloisFixed K U q :
        RelativeIdeleGroup.galoisFixedClassSubgroup K U) :
      RelativeIdeleGroup.ClassGroup K U) =
        RelativeIdeleGroup.classInclusion K U q

Module documentation

Descent of fixed rational idele classes

Declarations

rationalTowerRelativeIdeleClass_fixed_of_directLimit_fixed

rationalIntermediateField_algebra_eq_inclusion

rationalRelativeIdeleClassTowerBaseChangeEquiv

rationalIntermediateIdeleClassEquivGaloisFixed

rationalIntermediateIdeleClassEquivGaloisFixed_coe