Module

IdeleClassDirectLimitExtension.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.IdeleClassDirectLimitExtension

12 declarations indexed from sourceView source ↗

Module documentation

Finite extensions in the rational idele-class representation

The fixed representation of a finite abstract extension is compared with the relative idele class group of its two actual fixed fields.

Imports1

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.IdeleClassDirectLimitAbstractFixedField

Imported by3

instance

rationalAbstractTowerClassGroupCommGroup

L27 ↗

GlobalClassFieldTheory.Reciprocity.rationalAbstractTowerClassGroupCommGroup

Source context 6 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology

Lean source · statement

instance
    rationalAbstractTowerClassGroupCommGroup
    (F E : Type)
    [Field F] [NumberField F]
    [Field E] [NumberField E]
    [Algebra ℚ F] [Algebra F E] [Algebra ℚ E]
    [IsScalarTower ℚ F E]
    [FiniteDimensional ℚ F] [FiniteDimensional F E] :
    CommGroup (TowerRelativeIdeleGroup.ClassGroup ℚ F E)

instance

rationalAbstractTowerClassGroupMul

L42 ↗

GlobalClassFieldTheory.Reciprocity.rationalAbstractTowerClassGroupMul

Source context 6 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology

Lean source · statement

instance
    rationalAbstractTowerClassGroupMul
    (F E : Type)
    [Field F] [NumberField F]
    [Field E] [NumberField E]
    [Algebra ℚ F] [Algebra F E] [Algebra ℚ E]
    [IsScalarTower ℚ F E]
    [FiniteDimensional ℚ F] [FiniteDimensional F E] :
    Mul (TowerRelativeIdeleGroup.ClassGroup ℚ F E)

instance

rationalAbstractTowerClassGroupMulOneClass

L53 ↗

GlobalClassFieldTheory.Reciprocity.rationalAbstractTowerClassGroupMulOneClass

Source context 6 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology

Lean source · statement

instance
    rationalAbstractTowerClassGroupMulOneClass
    (F E : Type)
    [Field F] [NumberField F]
    [Field E] [NumberField E]
    [Algebra ℚ F] [Algebra F E] [Algebra ℚ E]
    [IsScalarTower ℚ F E]
    [FiniteDimensional ℚ F] [FiniteDimensional F E] :
    MulOneClass (TowerRelativeIdeleGroup.ClassGroup ℚ F E)

instance

rationalAbstractRelativeClassGroupCommGroup

L64 ↗

GlobalClassFieldTheory.Reciprocity.rationalAbstractRelativeClassGroupCommGroup

Source context 6 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology

Lean source · statement

instance
    rationalAbstractRelativeClassGroupCommGroup
    (F E : Type)
    [Field F] [NumberField F]
    [Field E] [NumberField E]
    [Algebra F E] [FiniteDimensional F E] :
    CommGroup (RelativeIdeleGroup.ClassGroup F E)

instance

rationalAbstractRelativeClassGroupMul

L77 ↗

GlobalClassFieldTheory.Reciprocity.rationalAbstractRelativeClassGroupMul

Source context 6 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology

Lean source · statement

instance
    rationalAbstractRelativeClassGroupMul
    (F E : Type)
    [Field F] [NumberField F]
    [Field E] [NumberField E]
    [Algebra F E] [FiniteDimensional F E] :
    Mul (RelativeIdeleGroup.ClassGroup F E)

instance

rationalAbstractRelativeClassGroupMulOneClass

L86 ↗

GlobalClassFieldTheory.Reciprocity.rationalAbstractRelativeClassGroupMulOneClass

Source context 6 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology

Lean source · statement

instance
    rationalAbstractRelativeClassGroupMulOneClass
    (F E : Type)
    [Field F] [NumberField F]
    [Field E] [NumberField E]
    [Algebra F E] [FiniteDimensional F E] :
    MulOneClass (RelativeIdeleGroup.ClassGroup F E)

def

rationalAbstractExtensionIdeleClassEquiv

L99 ↗

GlobalClassFieldTheory.Reciprocity.rationalAbstractExtensionIdeleClassEquiv

Documentation

The coefficient representation attached to a finite abstract extension is the existing relative idele class group of its two actual fixed fields. This packages the fixed-part and tower base-change comparisons into the endpoint used by finite reciprocity.

Source context 6 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology

Lean source · full declaration

def rationalAbstractExtensionIdeleClassEquiv
    (K L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hnormal : (extensionSubgroup K L hLK).Normal)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)] :
    let F :=
      LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) K
    let E :=
      LocalClassFieldTheory.abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) hLK
    letI := hnormal
    letI : FiniteDimensional ℚ F :=
      LocalClassFieldTheory.abstractFixedField_finiteDimensional
        ℚ (SeparableClosure ℚ) K hKfinite
    letI : FiniteDimensional F E :=
      LocalClassFieldTheory.abstractRelativeFixedField_finiteDimensional
        ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
    letI : IsScalarTower ℚ F E :=
      IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
    letI : FiniteDimensional ℚ E :=
      FiniteDimensional.trans ℚ F E
    letI : NumberField F := NumberField.of_module_finite ℚ F
    letI : NumberField E := NumberField.of_module_finite ℚ E
    (extensionFixedRepresentation rationalIdeleClassRepresentation
      K L hLK hnormal).V ≃+
      Additive (RelativeIdeleGroup.ClassGroup F E) := by
  let F :=
    LocalClassFieldTheory.abstractFixedField
      ℚ (SeparableClosure ℚ) K
  let E :=
    LocalClassFieldTheory.abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) hLK
  letI := hnormal
  letI : FiniteDimensional ℚ F :=
    LocalClassFieldTheory.abstractFixedField_finiteDimensional
      ℚ (SeparableClosure ℚ) K hKfinite
  letI : FiniteDimensional F E :=
    LocalClassFieldTheory.abstractRelativeFixedField_finiteDimensional
      ℚ (SeparableClosure ℚ) K L hLK hKfinite hfinite
  letI : IsScalarTower ℚ F E :=
    IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
  letI : FiniteDimensional ℚ E :=
    FiniteDimensional.trans ℚ F E
  letI : NumberField F := NumberField.of_module_finite ℚ F
  letI : NumberField E := NumberField.of_module_finite ℚ E
  let eFixed :
      Additive (IdeleClassGroup E) ≃+
        KummerTheory.ambientFixedAddSubgroup
          rationalIdeleClassRepresentation L :=
    rationalAbstractRelativeFixedFieldIdeleClassEquivFixedOfFiniteDimensional K L hLK
  let eRelative :
      Additive (RelativeIdeleGroup.ClassGroup ℚ E) ≃+
        Additive (IdeleClassGroup E) :=
    MulEquiv.toAdditive
      (_root_.relativeIdeleClassBaseChangeMulEquiv
        (K := ℚ) (L := E))
  let eTower :
      Additive (RelativeIdeleGroup.ClassGroup ℚ E) ≃+
        Additive (RelativeIdeleGroup.ClassGroup F E) :=
    MulEquiv.toAdditive
      ((TowerRelativeIdeleGroup.classGroupEquiv
        ℚ F E).symm.trans
          (towerRelativeIdeleClassBaseChangeMulEquiv
            ℚ F E))
  exact
    (((extensionFixedRepresentationEquiv
      rationalIdeleClassRepresentation K L hLK hnormal).trans
        eFixed.symm).trans eRelative.symm).trans eTower

theorem

rationalIdeleClassEquivFixed_relativeCosetAction_coe

L181 ↗

GlobalClassFieldTheory.Reciprocity.rationalIdeleClassEquivFixed_relativeCosetAction_coe

Documentation

In the direct-limit fixed-part comparison, one absolute left-coset action is the idele-class embedding selected by the corresponding embedding into the canonical normal closure.

Source context 6 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology

Lean source · statement

theorem rationalIdeleClassEquivFixed_relativeCosetAction_coe
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K]
    (c : RelativeIdeleGroup.ClassGroup ℚ K)
    (q :
      (RamificationTheory.closedFixingSubgroup
          ℚ (SeparableClosure ℚ)
          (⊥ : IntermediateField ℚ (SeparableClosure ℚ))).toSubgroup ⧸
        extensionSubgroup
          (RamificationTheory.closedFixingSubgroup
            ℚ (SeparableClosure ℚ)
            (⊥ : IntermediateField ℚ (SeparableClosure ℚ)))
          (RamificationTheory.closedFixingSubgroup
            ℚ (SeparableClosure ℚ) K)
          (LocalClassFieldTheory.fixingSubgroupLeBase
            ℚ (SeparableClosure ℚ) K)) :
    (relativeCosetAction rationalIdeleClassRepresentation
        (RamificationTheory.closedFixingSubgroup
          ℚ (SeparableClosure ℚ)
          (⊥ : IntermediateField ℚ (SeparableClosure ℚ)))
        (RamificationTheory.closedFixingSubgroup
          ℚ (SeparableClosure ℚ) K)
        (LocalClassFieldTheory.fixingSubgroupLeBase
          ℚ (SeparableClosure ℚ) K)
        (rationalIdeleClassEquivFixed K
          (Additive.ofMul
            (_root_.relativeIdeleClassBaseChangeMulEquiv
              (K := ℚ) (L := K) c))) q :
      rationalIdeleClassRepresentation.V) =
    Additive.ofMul
      (rationalRelativeIdeleClassToDirectLimit
        (rationalNormalClosure K)
        (RelativeIdeleGroup.classEmbedding
          (rationalBaseFixingCosetEquivNormalClosure K q) c))

theorem

rationalIdeleClassEquivFixed_relativeNorm_coe

L298 ↗

GlobalClassFieldTheory.Reciprocity.rationalIdeleClassEquivFixed_relativeNorm_coe

Documentation

The abstract class-formation norm in the rational idele-class direct limit is the ordinary relative idele-class norm, embedded at the canonical normal closure.

Source context 6 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology

Lean source · statement

theorem rationalIdeleClassEquivFixed_relativeNorm_coe
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K]
    (c : RelativeIdeleGroup.ClassGroup ℚ K) :
    (relativeNorm rationalIdeleClassRepresentation
        (RamificationTheory.closedFixingSubgroup
          ℚ (SeparableClosure ℚ)
          (⊥ : IntermediateField ℚ (SeparableClosure ℚ)))
        (RamificationTheory.closedFixingSubgroup
          ℚ (SeparableClosure ℚ) K)
        (LocalClassFieldTheory.fixingSubgroupLeBase
          ℚ (SeparableClosure ℚ) K)
        (rationalIdeleClassEquivFixed K
          (Additive.ofMul
            (_root_.relativeIdeleClassBaseChangeMulEquiv
              (K := ℚ) (L := K) c))) :
      KummerTheory.ambientFixedAddSubgroup
        rationalIdeleClassRepresentation
        (RamificationTheory.closedFixingSubgroup
          ℚ (SeparableClosure ℚ)
          (⊥ : IntermediateField ℚ (SeparableClosure ℚ)))).1 =
      Additive.ofMul
        (rationalRelativeIdeleClassToDirectLimit
          (rationalNormalClosure K)
          (RelativeIdeleGroup.classInclusion
            ℚ (rationalNormalClosure K)
            (RelativeIdeleGroup.Cohomology.ideleClassNorm ℚ K c)))

theorem

rationalAbstractFixedFieldIdeleClassEquivFixed_normToBase_coe

L465 ↗

GlobalClassFieldTheory.Reciprocity.rationalAbstractFixedFieldIdeleClassEquivFixed_normToBase_coe

Documentation

For a finite abstract rational field, the abstract norm to the base has the ordinary relative idele-class norm as its underlying direct-limit class. The two closed-subgroup indices are transported through their actual fixed fields; no new norm is introduced.

Source context 6 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology

Lean source · statement

theorem
    rationalAbstractFixedFieldIdeleClassEquivFixed_normToBase_coe
    (H : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    [hfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          H (le_baseField H))]
    (c : RelativeIdeleGroup.ClassGroup ℚ
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H)) :
    (normToBase rationalIdeleClassRepresentation H
        (rationalAbstractFixedFieldIdeleClassEquivFixed H
          (Additive.ofMul
            (_root_.relativeIdeleClassBaseChangeMulEquiv
              (K := ℚ)
              (L := LocalClassFieldTheory.abstractFixedField
                ℚ (SeparableClosure ℚ) H) c))) :
      KummerTheory.ambientFixedAddSubgroup
        rationalIdeleClassRepresentation
        (baseField
          (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))).1 =
      Additive.ofMul
        (rationalRelativeIdeleClassToDirectLimit
          (rationalNormalClosure
            (LocalClassFieldTheory.abstractFixedField
              ℚ (SeparableClosure ℚ) H))
          (RelativeIdeleGroup.classInclusion
            ℚ
            (rationalNormalClosure
              (LocalClassFieldTheory.abstractFixedField
                ℚ (SeparableClosure ℚ) H))
            (RelativeIdeleGroup.Cohomology.ideleClassNorm ℚ
              (LocalClassFieldTheory.abstractFixedField
                ℚ (SeparableClosure ℚ) H) c)))

instance

rationalFiniteAbstractField_quotient_finite

L559 ↗

GlobalClassFieldTheory.Reciprocity.rationalFiniteAbstractField_quotient_finite

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
section AbstractFixedFieldOrdinaryNorm
variable
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))

Lean source · statement

instance rationalFiniteAbstractField_quotient_finite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          H.field (le_baseField H.field))

theorem

rationalAbstractFixedFieldNormToBase_eq_ordinaryIdeleClassNorm

L572 ↗

GlobalClassFieldTheory.Reciprocity.rationalAbstractFixedFieldNormToBase_eq_ordinaryIdeleClassNorm

Documentation

Pulling the abstract base norm of an actual fixed-field idele class back through the distinguished rational fixed-part equivalence is the ordinary idele-class norm of that class.

Source context 9 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
section AbstractFixedFieldOrdinaryNorm
variable
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
local instance rationalFiniteAbstractField_quotient_finite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          H.field (le_baseField H.field)) :=
  H.finite

Lean source · statement

theorem
    rationalAbstractFixedFieldNormToBase_eq_ordinaryIdeleClassNorm
    (c : Additive
      (IdeleClassGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field))) :
    rationalIdeleClassEquivBaseFixed.symm
        (normToBase rationalIdeleClassRepresentation H.field
          (rationalAbstractFixedFieldIdeleClassEquivFixed
            H.field c)) =
      Additive.ofMul
        (_root_.ideleClassNorm ℚ
          (LocalClassFieldTheory.abstractFixedField
            ℚ (SeparableClosure ℚ) H.field)
          (Additive.toMul c))

Module documentation

Finite extensions in the rational idele-class representation

Declarations