NYLL
Module

IdeleClassDirectLimitAbstractFixedField.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.IdeleClassDirectLimitAbstractFixedField
7 declarations indexed from sourceView source ↗

Module documentation

Abstract fixed fields in the rational idele-class representation

Fixed-point comparisons for finite-index closed subgroups and their actual abstract fixed fields.

Imports2
Imported by3

Declarations

def

rationalIdeleClassEquivBaseFixed

L32 ↗
GlobalClassFieldTheory.Reciprocity.rationalIdeleClassEquivBaseFixed
Documentation

The ordinary rational idele class group is the fixed part at the distinguished base subgroup. This is rationalIdeleClassEquivFixed at the bottom intermediate field, transported along mathlib's canonical ℚ ≃ₐ[ℚ] ⊥ equivalence and the identity Gal(ℚ̄/⊥) = baseField.

Source context 5 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
Lean source · statement
def rationalIdeleClassEquivBaseFixed :
    Additive (IdeleClassGroup ℚ) ≃+
      KummerTheory.ambientFixedAddSubgroup
        rationalIdeleClassRepresentation
        (baseField
          (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
theorem

rationalIdeleClassEquivFixed_extension_coe

L68 ↗
GlobalClassFieldTheory.Reciprocity.rationalIdeleClassEquivFixed_extension_coe
Documentation

Scalar extension between finite rational intermediate fields becomes the literal inclusion between their fixed parts in the absolute idele-class representation.

Source context 5 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
Lean source · statement
theorem rationalIdeleClassEquivFixed_extension_coe
    {F E : IntermediateField ℚ (SeparableClosure ℚ)}
    [FiniteDimensional ℚ F] [FiniteDimensional ℚ E]
    (hFE : F ≤ E)
    (c : RelativeIdeleGroup.ClassGroup ℚ F) :
    (rationalIdeleClassEquivFixed E
        (Additive.ofMul
          (_root_.relativeIdeleClassBaseChangeMulEquiv
            (K := ℚ) (L := E)
            (RelativeIdeleGroup.classEmbedding (K := ℚ) (L := F) (M := E)
              (IntermediateField.inclusion hFE) c)))).1 =
      (rationalIdeleClassEquivFixed F
        (Additive.ofMul
          (_root_.relativeIdeleClassBaseChangeMulEquiv
            (K := ℚ) (L := F) c))).1
theorem

rationalIdeleClassEquivBaseFixed_coe

L100 ↗
GlobalClassFieldTheory.Reciprocity.rationalIdeleClassEquivBaseFixed_coe
Documentation

The distinguished base fixed-part equivalence sends an ordinary rational idele class to its diagonal class at every finite Galois level of the absolute direct limit.

Source context 5 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
Lean source · statement
theorem rationalIdeleClassEquivBaseFixed_coe
    (E : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ))
    (c : IdeleClassGroup ℚ) :
    (rationalIdeleClassEquivBaseFixed
        (Additive.ofMul c)).1 =
      Additive.ofMul
        (rationalRelativeIdeleClassToDirectLimit E
          (RelativeIdeleGroup.classInclusion ℚ E c))
instance

(anonymous instance)

L205 ↗
Source context 5 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
Lean source · statement
instance
    (K : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    [hfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))] :
    NumberField
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) K)
def

rationalAbstractFixedFieldIdeleClassEquivFixed

L232 ↗
GlobalClassFieldTheory.Reciprocity.rationalAbstractFixedFieldIdeleClassEquivFixed
Documentation

The actual idele class group of the fixed field represented by a finite-index closed subgroup is the corresponding fixed part of the rational absolute idele-class representation. This is the closed-subgroup endpoint of rationalIdeleClassEquivFixed.

Source context 5 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
Lean source · statement
def rationalAbstractFixedFieldIdeleClassEquivFixed
    (K : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    [hfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))] :
    Additive
        (IdeleClassGroup
          (LocalClassFieldTheory.abstractFixedField
            ℚ (SeparableClosure ℚ) K)) ≃+
      KummerTheory.ambientFixedAddSubgroup
        rationalIdeleClassRepresentation K
theorem

rationalAbstractFixedFieldIdeleClassEquivFixed_coe

L275 ↗
GlobalClassFieldTheory.Reciprocity.rationalAbstractFixedFieldIdeleClassEquivFixed_coe
Documentation

The closed-subgroup fixed-field endpoint has the same underlying direct-limit class as the intermediate-field comparison from which it is transported.

Source context 5 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
Lean source · statement
theorem rationalAbstractFixedFieldIdeleClassEquivFixed_coe
    (K : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    [hfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    (c : Additive
      (IdeleClassGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) K))) :
    (rationalAbstractFixedFieldIdeleClassEquivFixed K c).1 =
      (rationalIdeleClassEquivFixed
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) K) c).1
def

rationalAbstractRelativeFixedFieldIdeleClassEquivFixedOfFiniteDimensional

L303 ↗
GlobalClassFieldTheory.Reciprocity.rationalAbstractRelativeFixedFieldIdeleClassEquivFixedOfFiniteDimensional
Documentation

The relative abstract fixed-field idele class group, identified with the fixed part at the upper closed subgroup when finite dimensionality is already available.

Source context 5 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
Lean source · statement
def
    rationalAbstractRelativeFixedFieldIdeleClassEquivFixedOfFiniteDimensional
    (K L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [FiniteDimensional ℚ
      (LocalClassFieldTheory.abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) hLK)]
    [NumberField
      (LocalClassFieldTheory.abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) hLK)] :
    Additive
        (IdeleClassGroup
          (LocalClassFieldTheory.abstractRelativeFixedField
            ℚ (SeparableClosure ℚ) hLK)) ≃+
      KummerTheory.ambientFixedAddSubgroup
        rationalIdeleClassRepresentation L

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