NYLL
Module

IdeleClassDirectLimitCore.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.IdeleClassDirectLimitCore
29 declarations indexed from sourceView source ↗

Module documentation

The rational absolute idele-class direct limit

Finite Galois relative idele class groups over ℚ, their scalar-extension maps, and the induced absolute Galois representation.

Imports4
Imported by2

Declarations

instance

rationalSeparableClosureAlgebra

L36 ↗
GlobalClassFieldTheory.Reciprocity.rationalSeparableClosureAlgebra
Documentation

The rational algebra structure on the chosen separable closure is the one induced by its realization inside the algebraic closure.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · statement
instance rationalSeparableClosureAlgebra :
    Algebra ℚ (SeparableClosure ℚ)
instance

rationalIntermediateFieldAlgebra

L46 ↗
GlobalClassFieldTheory.Reciprocity.rationalIntermediateFieldAlgebra
Documentation

A rational intermediate field uses its actual inclusion into the chosen separable closure as its algebra structure.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · statement
instance rationalIntermediateFieldAlgebra
    (E : IntermediateField ℚ (SeparableClosure ℚ)) :
    Algebra ℚ E
instance

rationalIntermediateFieldNumberField

L53 ↗
GlobalClassFieldTheory.Reciprocity.rationalIntermediateFieldNumberField
Documentation

Every finite-dimensional rational intermediate field is a number field.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · statement
instance rationalIntermediateFieldNumberField
    (E : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ E] :
    NumberField E
instance

rationalClosedSubgroupQuotientFintype

L61 ↗
GlobalClassFieldTheory.Reciprocity.rationalClosedSubgroupQuotientFintype
Documentation

A finite quotient of nested closed rational absolute Galois subgroups carries its canonical finite type.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · statement
instance rationalClosedSubgroupQuotientFintype
    (K L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)] :
    Fintype (K.toSubgroup ⧸ extensionSubgroup K L hLK)
theorem

rationalRelativeIdeleClassEmbedding_classInclusion

L72 ↗
GlobalClassFieldTheory.Reciprocity.rationalRelativeIdeleClassEmbedding_classInclusion
Documentation

Extending the diagonal rational idele class through two nested intermediate fields is the diagonal class at the larger field.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · statement
theorem rationalRelativeIdeleClassEmbedding_classInclusion
    {E F : IntermediateField ℚ (SeparableClosure ℚ)}
    [NumberField E] [NumberField F]
    (h : E ≤ F)
    (c : IdeleClassGroup ℚ) :
    RelativeIdeleGroup.classEmbedding (IntermediateField.inclusion h)
        (RelativeIdeleGroup.classInclusion ℚ E c) =
      RelativeIdeleGroup.classInclusion ℚ F c
def

rationalAbsoluteGaloisIdeleClassAction

L87 ↗
GlobalClassFieldTheory.Reciprocity.rationalAbsoluteGaloisIdeleClassAction
Documentation

The action of the rational absolute Galois group on one finite relative idele class group, obtained by restricting automorphisms.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · statement
def rationalAbsoluteGaloisIdeleClassAction
    (E : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ)) :
    MulDistribMulAction
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)
      (RelativeIdeleGroup.ClassGroup ℚ E)
instance

rationalFiniteGaloisIdeleClassMulDistribMulAction

L103 ↗
GlobalClassFieldTheory.Reciprocity.rationalFiniteGaloisIdeleClassMulDistribMulAction
Documentation

The rational absolute Galois action on every finite-Galois relative idele class group.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · statement
instance rationalFiniteGaloisIdeleClassMulDistribMulAction
    (E : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ)) :
    MulDistribMulAction
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)
      (RelativeIdeleGroup.ClassGroup ℚ E)
instance

(anonymous instance)

L110 ↗
Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · statement
instance
    (E : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ)) :
    Monoid (RelativeIdeleGroup.ClassGroup ℚ E)
instance

(anonymous instance)

L115 ↗
Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · statement
instance :
    ∀ E : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ),
      MulDistribMulAction
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)
        (RelativeIdeleGroup.ClassGroup ℚ E)
instance

(anonymous instance)

L122 ↗
Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · statement
instance :
    ∀ E : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ),
      SMul
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)
        (RelativeIdeleGroup.ClassGroup ℚ E)
theorem

rationalAbsoluteGaloisIdeleClass_smul_mk

L130 ↗
GlobalClassFieldTheory.Reciprocity.rationalAbsoluteGaloisIdeleClass_smul_mk
Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · statement
theorem rationalAbsoluteGaloisIdeleClass_smul_mk
    (E : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ))
    (σ : SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)
    (a : RelativeIdeleGroup ℚ E) :
    σ • QuotientGroup.mk'
          (RelativeIdeleGroup.principalSubgroup ℚ E) a =
      QuotientGroup.mk'
        (RelativeIdeleGroup.principalSubgroup ℚ E)
        ((AlgEquiv.restrictNormalHom E σ) • a)
theorem

rationalRelativeAdeleEmbedding_conjugation_of_restrict

L143 ↗
GlobalClassFieldTheory.Reciprocity.rationalRelativeAdeleEmbedding_conjugation_of_restrict
Documentation

Relative-adele scalar extension intertwines conjugation with the restriction of an absolute Galois automorphism.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · statement
theorem rationalRelativeAdeleEmbedding_conjugation_of_restrict
    {E : IntermediateField ℚ (SeparableClosure ℚ)}
    [FiniteDimensional ℚ E]
    {F : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ)}
    (h : E ≤ (F : IntermediateField ℚ (SeparableClosure ℚ)))
    (σ : SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)
    (τ : E ≃ₐ[ℚ] E)
    (hστ : ∀ x : E,
      ((τ x : E) : SeparableClosure ℚ) =
        σ (x : SeparableClosure ℚ))
    (z : RelativeAdeleRing ℚ E) :
    RelativeIdeleGroup.adeleEmbedding (IntermediateField.inclusion h)
        (RelativeIdeleGroup.conjugation ℚ E τ z) =
      RelativeIdeleGroup.conjugation ℚ F
        (AlgEquiv.restrictNormalHom F σ)
        (RelativeIdeleGroup.adeleEmbedding (IntermediateField.inclusion h) z)
theorem

rationalRelativeIdeleEmbedding_conjugation_of_restrict

L183 ↗
GlobalClassFieldTheory.Reciprocity.rationalRelativeIdeleEmbedding_conjugation_of_restrict
Documentation

Relative-idele scalar extension intertwines conjugation with the restriction of an absolute Galois automorphism.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · statement
theorem rationalRelativeIdeleEmbedding_conjugation_of_restrict
    {E : IntermediateField ℚ (SeparableClosure ℚ)}
    [FiniteDimensional ℚ E]
    {F : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ)}
    (h : E ≤ (F : IntermediateField ℚ (SeparableClosure ℚ)))
    (σ : SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)
    (τ : E ≃ₐ[ℚ] E)
    (hστ : ∀ x : E,
      ((τ x : E) : SeparableClosure ℚ) =
        σ (x : SeparableClosure ℚ))
    (a : RelativeIdeleGroup ℚ E) :
    RelativeIdeleGroup.ideleEmbedding (IntermediateField.inclusion h)
        (τ • a) =
      (AlgEquiv.restrictNormalHom F σ) •
        RelativeIdeleGroup.ideleEmbedding (IntermediateField.inclusion h) a
theorem

rationalRelativeIdeleClassEmbedding_conjugation_of_restrict

L206 ↗
GlobalClassFieldTheory.Reciprocity.rationalRelativeIdeleClassEmbedding_conjugation_of_restrict
Documentation

Relative idele-class scalar extension intertwines conjugation with the restriction of an absolute Galois automorphism.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · statement
theorem
    rationalRelativeIdeleClassEmbedding_conjugation_of_restrict
    {E : IntermediateField ℚ (SeparableClosure ℚ)}
    [FiniteDimensional ℚ E]
    {F : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ)}
    (h : E ≤ (F : IntermediateField ℚ (SeparableClosure ℚ)))
    (σ : SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)
    (τ : E ≃ₐ[ℚ] E)
    (hστ : ∀ x : E,
      ((τ x : E) : SeparableClosure ℚ) =
        σ (x : SeparableClosure ℚ))
    (c : RelativeIdeleGroup.ClassGroup ℚ E) :
    RelativeIdeleGroup.classEmbedding (IntermediateField.inclusion h) (τ • c) =
      σ • RelativeIdeleGroup.classEmbedding (IntermediateField.inclusion h) c
theorem

rationalRelativeIdeleClassEmbedding_smul

L230 ↗
GlobalClassFieldTheory.Reciprocity.rationalRelativeIdeleClassEmbedding_smul
Documentation

The transition map between finite Galois relative idele class groups is equivariant for the rational absolute Galois action.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · statement
theorem rationalRelativeIdeleClassEmbedding_smul
    {E F : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ)}
    (h : E ≤ F)
    (σ : SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)
    (c : RelativeIdeleGroup.ClassGroup ℚ E) :
    RelativeIdeleGroup.classEmbedding (IntermediateField.inclusion h) (σ • c) =
      σ • RelativeIdeleGroup.classEmbedding (IntermediateField.inclusion h) c
theorem

rationalRelativeIdeleClassEmbedding_smul_eq_classEmbedding

L244 ↗
GlobalClassFieldTheory.Reciprocity.rationalRelativeIdeleClassEmbedding_smul_eq_classEmbedding
Documentation

Acting after scalar extension agrees with the class embedding induced by the resulting restricted field embedding.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · statement
theorem
    rationalRelativeIdeleClassEmbedding_smul_eq_classEmbedding
    {E : IntermediateField ℚ (SeparableClosure ℚ)}
    [FiniteDimensional ℚ E]
    {F : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ)}
    (h : E ≤ F)
    (σ : SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)
    (c : RelativeIdeleGroup.ClassGroup ℚ E) :
    (AlgEquiv.restrictNormalHom F σ) •
        RelativeIdeleGroup.classEmbedding (IntermediateField.inclusion h) c =
      RelativeIdeleGroup.classEmbedding
        ((AlgEquiv.restrictNormalHom F σ).toAlgHom.comp
          (IntermediateField.inclusion h)) c
def

rationalRelativeIdeleClassTransition

L284 ↗
GlobalClassFieldTheory.Reciprocity.rationalRelativeIdeleClassTransition
Documentation

The equivariant scalar-extension transition map in the finite-Galois idele-class system.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · full declaration
def rationalRelativeIdeleClassTransition
    {E F : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ)}
    (h : E ≤ F) :
    MulDistribMulActionHom
      (MonoidHom.id
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
      (RelativeIdeleGroup.ClassGroup ℚ E)
      (RelativeIdeleGroup.ClassGroup ℚ F) where
  toMonoidHom :=
    RelativeIdeleGroup.classEmbedding (IntermediateField.inclusion h)
  map_smul' σ c := by
    simpa using rationalRelativeIdeleClassEmbedding_smul h σ c
theorem

rationalRelativeAdeleEmbedding_self

L299 ↗
GlobalClassFieldTheory.Reciprocity.rationalRelativeAdeleEmbedding_self
Documentation

Scalar extension of relative adeles along the identity inclusion is the identity.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · full declaration
theorem rationalRelativeAdeleEmbedding_self
    (E : IntermediateField ℚ (SeparableClosure ℚ))
    [NumberField E]
    (z : RelativeAdeleRing ℚ E) :
    RelativeIdeleGroup.adeleEmbedding
      (IntermediateField.inclusion (show E ≤ E from le_rfl)) z = z := by
  induction z using TensorProduct.inductionOn with
  | tmul a x =>
      simp only [RelativeIdeleGroup.adeleEmbedding,
        RelativeIdeleGroup.scalarEmbedding_tmul]
      congr 1
  | add x y hx hy =>
      simp only [map_add, hx, hy]
theorem

rationalRelativeAdeleEmbedding_comp

L315 ↗
GlobalClassFieldTheory.Reciprocity.rationalRelativeAdeleEmbedding_comp
Documentation

Scalar extension of relative adeles is transitive in a tower of intermediate fields.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · statement
theorem rationalRelativeAdeleEmbedding_comp
    {E F H : IntermediateField ℚ (SeparableClosure ℚ)}
    [NumberField E] [NumberField F] [NumberField H]
    (hEF : E ≤ F) (hFH : F ≤ H)
    (z : RelativeAdeleRing ℚ E) :
    RelativeIdeleGroup.adeleEmbedding (IntermediateField.inclusion hFH)
        (RelativeIdeleGroup.adeleEmbedding (IntermediateField.inclusion hEF) z) =
      RelativeIdeleGroup.adeleEmbedding
        (IntermediateField.inclusion (hEF.trans hFH)) z
theorem

rationalRelativeIdeleClassEmbedding_self

L334 ↗
GlobalClassFieldTheory.Reciprocity.rationalRelativeIdeleClassEmbedding_self
Documentation

Scalar extension of relative idele classes along the identity inclusion is the identity.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · full declaration
theorem rationalRelativeIdeleClassEmbedding_self
    (E : IntermediateField ℚ (SeparableClosure ℚ))
    [NumberField E]
    (c : RelativeIdeleGroup.ClassGroup ℚ E) :
    RelativeIdeleGroup.classEmbedding
      (IntermediateField.inclusion (show E ≤ E from le_rfl)) c = c := by
  refine QuotientGroup.induction_on c ?_
  intro a
  exact congrArg
    (QuotientGroup.mk'
      (RelativeIdeleGroup.principalSubgroup ℚ E))
    (Units.ext
      (rationalRelativeAdeleEmbedding_self E
        (a : RelativeAdeleRing ℚ E)))
theorem

rationalRelativeIdeleClassEmbedding_comp

L351 ↗
GlobalClassFieldTheory.Reciprocity.rationalRelativeIdeleClassEmbedding_comp
Documentation

Scalar extension of relative idele classes is transitive in a tower of intermediate fields.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · statement
theorem rationalRelativeIdeleClassEmbedding_comp
    {E F H : IntermediateField ℚ (SeparableClosure ℚ)}
    [NumberField E] [NumberField F] [NumberField H]
    (hEF : E ≤ F) (hFH : F ≤ H)
    (c : RelativeIdeleGroup.ClassGroup ℚ E) :
    RelativeIdeleGroup.classEmbedding (IntermediateField.inclusion hFH)
        (RelativeIdeleGroup.classEmbedding (IntermediateField.inclusion hEF) c) =
      RelativeIdeleGroup.classEmbedding
        (IntermediateField.inclusion (hEF.trans hFH)) c
instance

(anonymous instance)

L369 ↗
Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · full declaration
instance :
    DirectedSystem
      (fun E : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ) =>
        RelativeIdeleGroup.ClassGroup ℚ E)
      (fun _ _ h => rationalRelativeIdeleClassTransition h) where
  map_self {i} c :=
    rationalRelativeIdeleClassEmbedding_self
      (i : IntermediateField ℚ (SeparableClosure ℚ)) c
  map_map {k} {j} {i} hIJ hJK c :=
    rationalRelativeIdeleClassEmbedding_comp
      (E := (i : IntermediateField ℚ (SeparableClosure ℚ)))
      (F := (j : IntermediateField ℚ (SeparableClosure ℚ)))
      (H := (k : IntermediateField ℚ (SeparableClosure ℚ)))
      hIJ hJK c
abbrev

rationalIdeleClassDirectLimit

L386 ↗
GlobalClassFieldTheory.Reciprocity.rationalIdeleClassDirectLimit
Documentation

The direct limit of the actual idele class groups of the finite Galois subextensions of SeparableClosure ℚ / ℚ.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · statement
abbrev rationalIdeleClassDirectLimit
instance

rationalIdeleClassDirectLimitMonoid

L394 ↗
GlobalClassFieldTheory.Reciprocity.rationalIdeleClassDirectLimitMonoid
Documentation

The multiplicative structure on the rational absolute idele-class direct limit supplied by Mathlib's directed-limit construction.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · statement
instance rationalIdeleClassDirectLimitMonoid :
    Monoid rationalIdeleClassDirectLimit
theorem

rationalIdeleClassDirectLimit_mk_apply

L398 ↗
GlobalClassFieldTheory.Reciprocity.rationalIdeleClassDirectLimit_mk_apply
Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · statement
theorem rationalIdeleClassDirectLimit_mk_apply
    {E F : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ)}
    (c : RelativeIdeleGroup.ClassGroup ℚ E)
    (h : E ≤ F) :
    (⟦⟨F, RelativeIdeleGroup.classEmbedding (IntermediateField.inclusion h) c⟩⟧ :
        rationalIdeleClassDirectLimit) =
      ⟦⟨E, c⟩⟧
def

rationalRelativeIdeleClassToDirectLimit

L416 ↗
GlobalClassFieldTheory.Reciprocity.rationalRelativeIdeleClassToDirectLimit
Documentation

The canonical map from one finite-level relative idele class group to the directed limit.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · full declaration
def rationalRelativeIdeleClassToDirectLimit
    (E : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ)) :
    RelativeIdeleGroup.ClassGroup ℚ E →*
      rationalIdeleClassDirectLimit where
  toFun c := ⟦⟨E, c⟩⟧
  map_one' := by
    exact
      (DirectLimit.one_def
        (G := fun E :
          FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ) =>
            RelativeIdeleGroup.ClassGroup ℚ E)
        (f := fun _ _ h =>
          rationalRelativeIdeleClassTransition h)
        E).symm
  map_mul' c d := by
    exact
      (DirectLimit.mul_def
        (G := fun E :
          FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ) =>
            RelativeIdeleGroup.ClassGroup ℚ E)
        (f := fun _ _ h =>
          rationalRelativeIdeleClassTransition h)
        E c d).symm
instance

rationalIdeleClassDirectLimitMulDistribMulAction

L442 ↗
GlobalClassFieldTheory.Reciprocity.rationalIdeleClassDirectLimitMulDistribMulAction
Documentation

The rational absolute Galois action on the idele-class direct limit, supplied by Mathlib from the equivariant transition maps.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · statement
instance
    rationalIdeleClassDirectLimitMulDistribMulAction :
    MulDistribMulAction
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)
      rationalIdeleClassDirectLimit
instance

rationalIdeleClassDirectLimitSMul

L451 ↗
GlobalClassFieldTheory.Reciprocity.rationalIdeleClassDirectLimitSMul
Documentation

The scalar action underlying the canonical absolute Galois action on the rational idele-class direct limit.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · statement
instance rationalIdeleClassDirectLimitSMul :
    SMul
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)
      rationalIdeleClassDirectLimit
def

rationalIdeleClassRepresentation

L460 ↗
GlobalClassFieldTheory.Reciprocity.rationalIdeleClassRepresentation
Documentation

The coefficient representation of the global class formation: the rational absolute Galois group acts on the direct limit of the actual finite-level idele class groups.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
universe u
Lean source · statement
def rationalIdeleClassRepresentation :
    Rep ℤ (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.