NYLL
Module

IdeleClassDirectLimitFiniteLevel.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.IdeleClassDirectLimitFiniteLevel
6 declarations indexed from sourceView source ↗

Module documentation

Tensor comparison and injectivity at finite rational levels

This endpoint leaf contains the tensor-unflattening comparisons and the resulting injectivity theorems. The finite-level normal-closure maps and their tower compatibility live in the reusable core leaf.

Imports1
Imported by2

Declarations

instance

rationalFiniteLevelEndpointNumberField

L32 ↗
GlobalClassFieldTheory.Reciprocity.rationalFiniteLevelEndpointNumberField
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
attribute [local instance]
  relativeAdeleRingIntermediateAlgebra
Lean source · statement
instance rationalFiniteLevelEndpointNumberField
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K] : NumberField K
theorem

rationalRelativeAdeleEmbedding_unflatten

L38 ↗
GlobalClassFieldTheory.Reciprocity.rationalRelativeAdeleEmbedding_unflatten
Documentation

Rational relative-adele scalar extension agrees with unflattening the corresponding fixed-bottom tensor tower.

Source context 8 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
attribute [local instance]
  relativeAdeleRingIntermediateAlgebra
local instance rationalFiniteLevelEndpointNumberField
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K] : NumberField K :=
  NumberField.of_module_finite ℚ K
Lean source · full declaration
theorem rationalRelativeAdeleEmbedding_unflatten
    {K N : IntermediateField ℚ (SeparableClosure ℚ)}
    [FiniteDimensional ℚ K] [FiniteDimensional ℚ N]
    (hKN : K ≤ N)
    (a : RelativeAdeleRing ℚ K) :
    letI : Algebra K N :=
      (IntermediateField.inclusion hKN).toRingHom.toAlgebra
    letI : IsScalarTower ℚ K N :=
      IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
    letI : FiniteDimensional K N :=
      FiniteDimensional.right ℚ K N
    towerRelativeAdeleUnflatten ℚ K N
        (RelativeIdeleGroup.adeleEmbedding (K := ℚ) (L := K) (M := N)
          (IntermediateField.inclusion hKN) a) =
      a ⊗ₜ[K] (1 : N) := by
  let : Algebra K N :=
    (IntermediateField.inclusion hKN).toRingHom.toAlgebra
  let : IsScalarTower ℚ K N :=
    IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
  let : FiniteDimensional K N :=
    FiniteDimensional.right ℚ K N
  have hflatten :
      towerRelativeAdeleFlatten ℚ K N
          (towerRelativeAdeleUnflatten ℚ K N
            (RelativeIdeleGroup.adeleEmbedding (K := ℚ) (L := K) (M := N)
              (IntermediateField.inclusion hKN) a)) =
        RelativeIdeleGroup.adeleEmbedding (K := ℚ) (L := K) (M := N)
          (IntermediateField.inclusion hKN) a :=
    (towerRelativeAdeleRingEquiv ℚ K N).apply_symm_apply
      (RelativeIdeleGroup.adeleEmbedding (K := ℚ) (L := K) (M := N)
        (IntermediateField.inclusion hKN) a)
  apply
    (towerRelativeAdeleRingEquiv ℚ K N).injective
  change
    towerRelativeAdeleFlatten ℚ K N
        (towerRelativeAdeleUnflatten ℚ K N
          (RelativeIdeleGroup.adeleEmbedding (K := ℚ) (L := K) (M := N)
            (IntermediateField.inclusion hKN) a)) =
      towerRelativeAdeleFlatten ℚ K N
        (a ⊗ₜ[K] (1 : N))
  rw [hflatten]
  rw [towerRelativeAdeleFlatten_tmul]
  simp only [map_one, mul_one]
  rfl
theorem

rationalRelativeIdeleEmbedding_unflatten

L85 ↗
GlobalClassFieldTheory.Reciprocity.rationalRelativeIdeleEmbedding_unflatten
Documentation

Rational relative-idele scalar extension agrees with unflattening the corresponding fixed-bottom tensor tower.

Source context 8 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
attribute [local instance]
  relativeAdeleRingIntermediateAlgebra
local instance rationalFiniteLevelEndpointNumberField
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K] : NumberField K :=
  NumberField.of_module_finite ℚ K
Lean source · full declaration
theorem rationalRelativeIdeleEmbedding_unflatten
    {K N : IntermediateField ℚ (SeparableClosure ℚ)}
    [FiniteDimensional ℚ K] [FiniteDimensional ℚ N]
    (hKN : K ≤ N)
    (a : RelativeIdeleGroup ℚ K) :
    letI : Algebra K N :=
      (IntermediateField.inclusion hKN).toRingHom.toAlgebra
    letI : IsScalarTower ℚ K N :=
      IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
    letI : FiniteDimensional K N :=
      FiniteDimensional.right ℚ K N
    letI : Algebra K (RelativeAdeleRing ℚ K) :=
      relativeAdeleRingIntermediateAlgebra ℚ K
    (towerRelativeIdeleEquiv ℚ K N).symm
        (RelativeIdeleGroup.ideleEmbedding (K := ℚ) (L := K) (M := N)
          (IntermediateField.inclusion hKN) a) =
      (Units.map
        (@Algebra.TensorProduct.includeLeft
          K K (RelativeAdeleRing ℚ K) N
          inferInstance inferInstance
          (relativeAdeleRingIntermediateAlgebra ℚ K)
          inferInstance
          ((IntermediateField.inclusion hKN).toRingHom.toAlgebra)
          inferInstance
          (relativeAdeleRingIntermediateAlgebra ℚ K)
          (smulCommClass_self K (RelativeAdeleRing ℚ K))).toRingHom a :
        TowerRelativeIdeleGroup ℚ K N) := by
  let : Algebra K N :=
    (IntermediateField.inclusion hKN).toRingHom.toAlgebra
  let : IsScalarTower ℚ K N :=
    IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
  let : FiniteDimensional K N :=
    FiniteDimensional.right ℚ K N
  let : Algebra K (RelativeAdeleRing ℚ K) :=
    relativeAdeleRingIntermediateAlgebra ℚ K
  apply Units.ext
  exact
    rationalRelativeAdeleEmbedding_unflatten
      hKN (a : RelativeAdeleRing ℚ K)
theorem

rationalRelativeIdeleClassEmbedding_towerBaseChange

L127 ↗
GlobalClassFieldTheory.Reciprocity.rationalRelativeIdeleClassEmbedding_towerBaseChange
Documentation

Rational relative idele-class scalar extension agrees with the fixed-bottom tower base-change equivalence.

Source context 8 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
attribute [local instance]
  relativeAdeleRingIntermediateAlgebra
local instance rationalFiniteLevelEndpointNumberField
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K] : NumberField K :=
  NumberField.of_module_finite ℚ K
Lean source · full declaration
theorem
    rationalRelativeIdeleClassEmbedding_towerBaseChange
    {K N : IntermediateField ℚ (SeparableClosure ℚ)}
    [FiniteDimensional ℚ K] [FiniteDimensional ℚ N]
    (hKN : K ≤ N)
    (c : RelativeIdeleGroup.ClassGroup ℚ K) :
    letI : Algebra K N :=
      (IntermediateField.inclusion hKN).toRingHom.toAlgebra
    letI : IsScalarTower ℚ K N :=
      IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
    letI : FiniteDimensional K N :=
      FiniteDimensional.right ℚ K N
    towerRelativeIdeleClassBaseChangeMulEquiv ℚ K N
        ((TowerRelativeIdeleGroup.classGroupEquiv ℚ K N).symm
          (RelativeIdeleGroup.classEmbedding (K := ℚ) (L := K) (M := N)
            (IntermediateField.inclusion hKN) c)) =
      RelativeIdeleGroup.classInclusion K N
        (_root_.relativeIdeleClassBaseChangeMulEquiv
          (K := ℚ) (L := K) c) := by
  let : Algebra K N :=
    (IntermediateField.inclusion hKN).toRingHom.toAlgebra
  let : IsScalarTower ℚ K N :=
    IsScalarTower.of_algebraMap_eq' (RingHom.ext_rat _ _)
  let : FiniteDimensional K N :=
    FiniteDimensional.right ℚ K N
  refine QuotientGroup.induction_on c ?_
  intro a
  change
    QuotientGroup.mk'
        (RelativeIdeleGroup.principalSubgroup K N)
        (towerRelativeIdeleBaseChangeMulEquiv ℚ K N
          ((towerRelativeIdeleEquiv ℚ K N).symm
            (RelativeIdeleGroup.ideleEmbedding (K := ℚ) (L := K) (M := N)
              (IntermediateField.inclusion hKN) a))) =
      QuotientGroup.mk'
        (RelativeIdeleGroup.principalSubgroup K N)
        (RelativeIdeleGroup.inclusion K N
          (relativeIdeleBaseChangeMulEquiv
            (K := ℚ) (L := K) a))
  apply congrArg
    (QuotientGroup.mk'
      (RelativeIdeleGroup.principalSubgroup K N))
  rw [rationalRelativeIdeleEmbedding_unflatten hKN a]
  exact
    towerRelativeIdeleBaseChangeMulEquiv_includeLeft
      ℚ K N a
theorem

rationalRelativeIdeleClassEmbedding_injective

L176 ↗
GlobalClassFieldTheory.Reciprocity.rationalRelativeIdeleClassEmbedding_injective
Documentation

Scalar extension between finite rational relative idele class groups is injective.

Source context 8 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
attribute [local instance]
  relativeAdeleRingIntermediateAlgebra
local instance rationalFiniteLevelEndpointNumberField
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K] : NumberField K :=
  NumberField.of_module_finite ℚ K
Lean source · statement
theorem rationalRelativeIdeleClassEmbedding_injective
    {K N : IntermediateField ℚ (SeparableClosure ℚ)}
    [FiniteDimensional ℚ K] [FiniteDimensional ℚ N]
    (hKN : K ≤ N) :
    Function.Injective
      (RelativeIdeleGroup.classEmbedding (K := ℚ) (L := K) (M := N)
        (IntermediateField.inclusion hKN))
theorem

rationalRelativeIdeleClassToDirectLimit_injective

L207 ↗
GlobalClassFieldTheory.Reciprocity.rationalRelativeIdeleClassToDirectLimit_injective
Documentation

Each finite-level relative idele class group embeds into the rational idele-class direct limit.

Source context 8 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
attribute [local instance]
  relativeAdeleRingIntermediateAlgebra
local instance rationalFiniteLevelEndpointNumberField
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K] : NumberField K :=
  NumberField.of_module_finite ℚ K
Lean source · statement
theorem rationalRelativeIdeleClassToDirectLimit_injective
    (E : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ)) :
    Function.Injective
      (rationalRelativeIdeleClassToDirectLimit E)

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