Module

IdeleClassDirectLimitFixedPoints.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.IdeleClassDirectLimitFixedPoints

10 declarations indexed from sourceView source ↗

Module documentation

Fixed points of the rational idele-class direct limit

The actual idele class group of a finite rational intermediate field is identified with the corresponding fixed subgroup of the direct limit.

Imports2

Imported by2

theorem

rationalRelativeAdeleEmbedding_fixed_of_mem_fixingSubgroup

L26 ↗

GlobalClassFieldTheory.Reciprocity.rationalRelativeAdeleEmbedding_fixed_of_mem_fixingSubgroup

Documentation

Scalar extension of a rational relative adele is fixed by every absolute Galois element fixing the source field.

Source context 3 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

theorem
    rationalRelativeAdeleEmbedding_fixed_of_mem_fixingSubgroup
    {K : IntermediateField ℚ (SeparableClosure ℚ)}
    [FiniteDimensional ℚ K]
    {N : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ)}
    (hKN : K ≤ (N :
      IntermediateField ℚ (SeparableClosure ℚ)))
    (σ : SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)
    (hσ : σ ∈ K.fixingSubgroup)
    (z : RelativeAdeleRing ℚ K) :
    RelativeIdeleGroup.conjugation ℚ N
        (AlgEquiv.restrictNormalHom N σ)
        (RelativeIdeleGroup.adeleEmbedding (K := ℚ) (L := K) (M := N)
          (IntermediateField.inclusion hKN) z) =
      RelativeIdeleGroup.adeleEmbedding (K := ℚ) (L := K) (M := N)
        (IntermediateField.inclusion hKN) z

theorem

rationalRelativeIdeleClassEmbedding_fixed_of_mem_fixingSubgroup

L68 ↗

GlobalClassFieldTheory.Reciprocity.rationalRelativeIdeleClassEmbedding_fixed_of_mem_fixingSubgroup

Documentation

Scalar extension of a rational relative idele class is fixed by every absolute Galois element fixing the source field.

Source context 3 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

theorem
    rationalRelativeIdeleClassEmbedding_fixed_of_mem_fixingSubgroup
    {K : IntermediateField ℚ (SeparableClosure ℚ)}
    [FiniteDimensional ℚ K]
    {N : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ)}
    (hKN : K ≤ (N :
      IntermediateField ℚ (SeparableClosure ℚ)))
    (σ : SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)
    (hσ : σ ∈ K.fixingSubgroup)
    (c : RelativeIdeleGroup.ClassGroup ℚ K) :
    σ • RelativeIdeleGroup.classEmbedding (K := ℚ) (L := K) (M := N)
        (IntermediateField.inclusion hKN) c =
      RelativeIdeleGroup.classEmbedding (K := ℚ) (L := K) (M := N)
        (IntermediateField.inclusion hKN) c

theorem

rationalIntermediateIdeleClassToDirectLimit_conjugation

L104 ↗

GlobalClassFieldTheory.Reciprocity.rationalIntermediateIdeleClassToDirectLimit_conjugation

Documentation

The map from an intermediate idele class group to the direct limit intertwines compatible finite and absolute Galois actions.

Source context 3 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

theorem rationalIntermediateIdeleClassToDirectLimit_conjugation
    (E : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ E]
    (σ : SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)
    (τ : E ≃ₐ[ℚ] E)
    (hστ : ∀ x : E,
      ((τ x : E) : SeparableClosure ℚ) =
        σ (x : SeparableClosure ℚ))
    (c : RelativeIdeleGroup.ClassGroup ℚ E) :
    σ • rationalIntermediateIdeleClassToDirectLimit E
        (_root_.relativeIdeleClassBaseChangeMulEquiv
          (K := ℚ) (L := E) c) =
      rationalIntermediateIdeleClassToDirectLimit E
        (_root_.relativeIdeleClassBaseChangeMulEquiv
          (K := ℚ) (L := E) (τ • c))

theorem

rationalIntermediateIdeleClassToDirectLimit_ambientAlgEquiv

L177 ↗

GlobalClassFieldTheory.Reciprocity.rationalIntermediateIdeleClassToDirectLimit_ambientAlgEquiv

Documentation

The canonical direct-limit realization of idèle classes is natural under an equivalence between two finite rational intermediate fields which is induced by an automorphism of the rational separable closure.

Source context 3 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

theorem rationalIntermediateIdeleClassToDirectLimit_ambientAlgEquiv
    {E F : IntermediateField ℚ (SeparableClosure ℚ)}
    [FiniteDimensional ℚ E] [FiniteDimensional ℚ F]
    (σ : SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)
    (e : E ≃ₐ[ℚ] F)
    (hσe : ∀ x : E,
      ((e x : F) : SeparableClosure ℚ) =
        σ (x : SeparableClosure ℚ))
    (c : IdeleClassGroup E) :
    σ • rationalIntermediateIdeleClassToDirectLimit E c =
      rationalIntermediateIdeleClassToDirectLimit F
        (ideleClassCongr e c)

theorem

rationalIntermediateIdeleClassToDirectLimit_fixed

L382 ↗

GlobalClassFieldTheory.Reciprocity.rationalIntermediateIdeleClassToDirectLimit_fixed

Documentation

The image in the direct limit of an idele class over K is fixed by the absolute Galois subgroup fixing 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 rationalIntermediateIdeleClassToDirectLimit_fixed
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K]
    (c : IdeleClassGroup K)
    (σ : SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)
    (hσ : σ ∈ K.fixingSubgroup) :
    σ • rationalIntermediateIdeleClassToDirectLimit K c =
      rationalIntermediateIdeleClassToDirectLimit K c

theorem

rationalIntermediateIdeleClassToDirectLimit_mem_fixed

L459 ↗

GlobalClassFieldTheory.Reciprocity.rationalIntermediateIdeleClassToDirectLimit_mem_fixed

Documentation

Additive idele classes map into the fixed subgroup of the rational idele-class representation.

Source context 3 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

theorem rationalIntermediateIdeleClassToDirectLimit_mem_fixed
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K]
    (c : Additive (IdeleClassGroup K)) :
    MonoidHom.toAdditive
        (rationalIntermediateIdeleClassToDirectLimit K) c ∈
      KummerTheory.ambientFixedAddSubgroup
        rationalIdeleClassRepresentation
        (RamificationTheory.closedFixingSubgroup
          ℚ (SeparableClosure ℚ) K)

def

rationalIntermediateIdeleClassToFixed

L493 ↗

GlobalClassFieldTheory.Reciprocity.rationalIntermediateIdeleClassToFixed

Documentation

The canonical additive homomorphism from the idele class group of a finite rational intermediate field to the corresponding 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 rationalIntermediateIdeleClassToFixed
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K] :
    Additive (IdeleClassGroup K) →+
      KummerTheory.ambientFixedAddSubgroup
        rationalIdeleClassRepresentation
        (RamificationTheory.closedFixingSubgroup
          ℚ (SeparableClosure ℚ) K)

theorem

rationalIntermediateIdeleClassToFixed_injective

L511 ↗

GlobalClassFieldTheory.Reciprocity.rationalIntermediateIdeleClassToFixed_injective

Documentation

The canonical map from a finite rational idele class group to the corresponding fixed subgroup is injective.

Source context 3 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

theorem rationalIntermediateIdeleClassToFixed_injective
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K] :
    Function.Injective
      (rationalIntermediateIdeleClassToFixed K)

theorem

rationalIntermediateIdeleClassToFixed_surjective

L552 ↗

GlobalClassFieldTheory.Reciprocity.rationalIntermediateIdeleClassToFixed_surjective

Documentation

The canonical map from a finite rational idele class group to the corresponding fixed subgroup is surjective.

Source context 3 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

theorem rationalIntermediateIdeleClassToFixed_surjective
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K] :
    Function.Surjective
      (rationalIntermediateIdeleClassToFixed K)

def

rationalIdeleClassEquivFixed

L586 ↗

GlobalClassFieldTheory.Reciprocity.rationalIdeleClassEquivFixed

Documentation

The subgroup of the absolute idele-class direct limit fixed by the absolute Galois group over a finite rational intermediate field is exactly that field's actual idele class group.

Source context 3 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

def rationalIdeleClassEquivFixed
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K] :
    Additive (IdeleClassGroup K) ≃+
      KummerTheory.ambientFixedAddSubgroup
        rationalIdeleClassRepresentation
        (RamificationTheory.closedFixingSubgroup
          ℚ (SeparableClosure ℚ) K)

Module documentation

Fixed points of the rational idele-class direct limit

Declarations