NYLL
Module

SupportedBridge.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Cohomology.SupportedBridge
19 declarations indexed from sourceView source ↗

Module documentation

A sufficiently large unramified support for the idele-class calculation

This file constructs the finite set used in the idele-class Herbrand calculation. It contains the contractions of a sufficiently large set of places of L and every finite place of K at which some place of L ramifies.

It also compares the concrete tensor-coordinate supported subgroup of relative ideles with the ordinary supported idele subgroup of L.

Imports8
Imported by7

Declarations

def

finitePlacesAbove

L43 ↗
Documentation

The finite set of places of L lying above a finite set of places of K.

Source context 4 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def finitePlacesAbove
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    Finset (HeightOneSpectrum (𝓞 L))
theorem

mem_finitePlacesAbove_iff

L51 ↗
Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem mem_finitePlacesAbove_iff
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (W : HeightOneSpectrum (𝓞 L)) :
    W ∈ finitePlacesAbove (K := K) (L := L) S ↔
      finitePlaceBelow (K := K) W ∈ S
theorem

finitePlaceBelow_finitePlaceEquiv

L62 ↗
Documentation

Galois conjugation does not change the place lying below a finite place of the extension field.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem finitePlaceBelow_finitePlaceEquiv
    (σ : L ≃ₐ[K] L)
    (W : HeightOneSpectrum (𝓞 L)) :
    finitePlaceBelow (K := K) (finitePlaceEquiv K L σ W) =
      finitePlaceBelow (K := K) W
theorem

finitePlacesAbove_isGaloisStable

L89 ↗
Documentation

The full set of extension places above a base support is stable under the concrete Galois action.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem finitePlacesAbove_isGaloisStable
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    IsGaloisStableFinitePlaces K L
      (finitePlacesAbove (K := K) (L := L) S)
theorem

relativeIdeleBaseChange_mem_supportedAt_iff

L105 ↗
Documentation

Scalar extension carries the concrete supported relative ideles exactly to the ordinary ideles supported at all places above the same base support.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [IsGalois K L] in
Lean source · statement
theorem relativeIdeleBaseChange_mem_supportedAt_iff
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (z : RelativeIdeleGroup K L) :
    z ∈ relativeIdeleLocalTensorDecompositionSupportedSubgroup
          (K := K) (L := L) S ↔
      relativeIdeleBaseChangeMulEquiv
          (K := K) (L := L) z ∈
        IdeleGroup.supportedAt (K := L)
          (finitePlacesAbove (K := K) (L := L) S : Set _)
theorem

relativeIdeleLocalTensorDecompositionSupportedSubgroup_map_baseChange

L159 ↗
Documentation

Subgroup-level form of relativeIdeleBaseChange_mem_supportedAt_iff.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [IsGalois K L] in
Lean source · statement
theorem relativeIdeleLocalTensorDecompositionSupportedSubgroup_map_baseChange
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    (relativeIdeleLocalTensorDecompositionSupportedSubgroup
        (K := K) (L := L) S).map
      (relativeIdeleBaseChangeMulEquiv
        (K := K) (L := L)).toMonoidHom =
      IdeleGroup.supportedAt (K := L)
        (finitePlacesAbove (K := K) (L := L) S : Set _)
theorem

relativeIdeleSupported_sup_principal_eq_top

L188 ↗
Documentation

If the supported ordinary ideles and principal ideles generate I_L, then their relative counterparts generate the full relative idele group.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [IsGalois K L] in
Lean source · statement
theorem relativeIdeleSupported_sup_principal_eq_top
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (hOrdinary :
      IdeleGroup.supportedAt (K := L)
          (finitePlacesAbove (K := K) (L := L) S : Set _) ⊔
        IdeleGroup.principalSubgroup L = ⊤) :
    relativeIdeleLocalTensorDecompositionSupportedSubgroup
          (K := K) (L := L) S ⊔
        RelativeIdeleGroup.principalSubgroup K L =
  ⊤
theorem

principalIdele_mem_supportedAt_iff_sUnit

L217 ↗
Documentation

A diagonal idele is supported at T exactly when its defining field unit is a T-unit.

Source context 4 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem principalIdele_mem_supportedAt_iff_sUnit
    (T : Finset (HeightOneSpectrum (𝓞 L)))
    (x : Lˣ) :
    IdeleGroup.principalIdele L x ∈
        IdeleGroup.supportedAt (K := L) (T : Set _) ↔
      x ∈ SUnitGroup (K := L) T
def

sUnitToRelativePrincipalSupportedIntersection

L254 ↗
Documentation

The diagonal map from extension-field S-units into the intersection of the relative principal and supported subgroups.

Source context 4 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · full declaration
def sUnitToRelativePrincipalSupportedIntersection
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    SUnitGroup (K := L)
        (finitePlacesAbove (K := K) (L := L) S) →*
      (RelativeIdeleGroup.principalSubgroup K L).subgroupOf
        (relativeIdeleLocalTensorDecompositionSupportedSubgroup
          (K := K) (L := L) S) where
  toFun x := by
    have hOrdinary :
        IdeleGroup.principalIdele L (x : Lˣ) ∈
          IdeleGroup.supportedAt (K := L)
            (finitePlacesAbove (K := K) (L := L) S : Set _) :=
      (principalIdele_mem_supportedAt_iff_sUnit
        (L := L)
        (finitePlacesAbove (K := K) (L := L) S)
        (x : Lˣ)).2 x.property
    have hRelative :
        RelativeIdeleGroup.principalIdele K L (x : Lˣ) ∈
          relativeIdeleLocalTensorDecompositionSupportedSubgroup
            (K := K) (L := L) S := by
      apply
        (relativeIdeleBaseChange_mem_supportedAt_iff
          (K := K) (L := L) S _).2
      simpa using hOrdinary
    exact
      ⟨⟨RelativeIdeleGroup.principalIdele K L (x : Lˣ),
          hRelative⟩,
        ⟨(x : Lˣ), rfl⟩⟩
  map_one' := by
    apply Subtype.ext
    apply Subtype.ext
    simp
  map_mul' x y := by
    apply Subtype.ext
    apply Subtype.ext
    simp
def

sUnitEquivRelativePrincipalSupportedIntersection

L294 ↗
Documentation

The intersection of the relative principal ideles with the relative S-idele subgroup is precisely the ordinary group of S-units of L.

Source context 4 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def sUnitEquivRelativePrincipalSupportedIntersection
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    SUnitGroup (K := L)
        (finitePlacesAbove (K := K) (L := L) S) ≃*
      (RelativeIdeleGroup.principalSubgroup K L).subgroupOf
        (relativeIdeleLocalTensorDecompositionSupportedSubgroup
          (K := K) (L := L) S)
def

relativePrincipalSupportedIntersectionAction

L358 ↗
Documentation

The restricted Galois action on the intersection of the relative principal and supported subgroups.

Source context 4 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def relativePrincipalSupportedIntersectionAction
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    MulDistribMulAction (L ≃ₐ[K] L)
      ((RelativeIdeleGroup.principalSubgroup K L).subgroupOf
        (relativeIdeleLocalTensorDecompositionSupportedSubgroup
          (K := K) (L := L) S))
theorem

sUnitEquivRelativePrincipalSupportedIntersection_smul

L397 ↗
Documentation

The S-unit description of the principal-supported intersection is equivariant for the genuine Galois actions.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [IsGalois K L] in
Lean source · full declaration
theorem
    sUnitEquivRelativePrincipalSupportedIntersection_smul
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (σ : L ≃ₐ[K] L)
    (x :
      SUnitGroup (K := L)
        (finitePlacesAbove (K := K) (L := L) S)) :
    letI :=
      sUnitMulDistribMulAction K L
        (finitePlacesAbove (K := K) (L := L) S)
        (finitePlacesAbove_isGaloisStable
          (K := K) (L := L) S)
    letI :=
      relativePrincipalSupportedIntersectionAction
        (K := K) (L := L) S
    sUnitEquivRelativePrincipalSupportedIntersection
        (K := K) (L := L) S (σ • x) =
      σ •
        sUnitEquivRelativePrincipalSupportedIntersection
          (K := K) (L := L) S x := by
  let :=
    sUnitMulDistribMulAction K L
      (finitePlacesAbove (K := K) (L := L) S)
      (finitePlacesAbove_isGaloisStable
        (K := K) (L := L) S)
  let :=
    relativePrincipalSupportedIntersectionAction
      (K := K) (L := L) S
  apply Subtype.ext
  apply Subtype.ext
  change
    RelativeIdeleGroup.principalIdele K L
        (((σ • x :
          SUnitGroup (K := L)
            (finitePlacesAbove (K := K) (L := L) S)) :
          Lˣ)) =
      σ • RelativeIdeleGroup.principalIdele K L (x : Lˣ)
  rw [sUnit_smul_coe]
  exact
    (RelativeIdeleGroup.smul_principalIdele
      K L σ (x : Lˣ)).symm
def

ramifiedBaseFinitePlaces

L441 ↗
Documentation

The finite base places at which at least one extension prime is ramified.

Source context 4 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def ramifiedBaseFinitePlaces :
    Finset (HeightOneSpectrum (𝓞 K))
theorem

mem_ramifiedBaseFinitePlaces_iff

L448 ↗
Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem mem_ramifiedBaseFinitePlaces_iff
    (v : HeightOneSpectrum (𝓞 K)) :
    v ∈ ramifiedBaseFinitePlaces (K := K) (L := L) ↔
      ∃ W : HeightOneSpectrum (𝓞 L),
        W.asIdeal.LiesOver v.asIdeal ∧
          ¬ Algebra.IsUnramifiedAt (𝓞 K) W.asIdeal
def

ideleClassHerbrandSupport

L458 ↗
Documentation

The idele-class Herbrand support: contractions of a sufficiently large support for I_L, together with every ramified base finite place.

Source context 4 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def ideleClassHerbrandSupport :
    Finset (HeightOneSpectrum (𝓞 K))
theorem

sufficientlyLargeFiniteSet_subset_finitePlacesAbove_support

L469 ↗
Documentation

Every place in the sufficiently large support of L lies above the chosen base support.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem sufficientlyLargeFiniteSet_subset_finitePlacesAbove_support :
    (IdeleGroup.sufficientlyLargeFiniteSet (K := L) :
        Set (HeightOneSpectrum (𝓞 L))) ⊆
      ((finitePlacesAbove
          (K := K) (L := L)
          (ideleClassHerbrandSupport (K := K) (L := L)) :
            Finset (HeightOneSpectrum (𝓞 L))) :
        Set (HeightOneSpectrum (𝓞 L)))
theorem

supportedAboveHerbrandSupport_sup_principal_eq_top

L489 ↗
Documentation

The ordinary ideles supported above the chosen base support, together with principal ideles, generate all of I_L.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem supportedAboveHerbrandSupport_sup_principal_eq_top :
    IdeleGroup.supportedAt (K := L)
        (finitePlacesAbove
          (K := K) (L := L)
          (ideleClassHerbrandSupport (K := K) (L := L)) : Set _) ⊔
      IdeleGroup.principalSubgroup L = ⊤
theorem

relativeSupportedAboveHerbrandSupport_sup_principal_eq_top

L508 ↗
Documentation

The relative ideles supported at the Herbrand support, together with the relative principal ideles, generate the full relative idele group.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [IsGalois K L] in
Lean source · statement
theorem relativeSupportedAboveHerbrandSupport_sup_principal_eq_top :
    relativeIdeleLocalTensorDecompositionSupportedSubgroup
          (K := K) (L := L)
          (ideleClassHerbrandSupport (K := K) (L := L)) ⊔
        RelativeIdeleGroup.principalSubgroup K L =
      ⊤
theorem

isUnramifiedAt_of_notMem_ideleClassHerbrandSupport

L523 ↗
Documentation

Outside the chosen base support, every finite place of L is algebraically unramified over K.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem isUnramifiedAt_of_notMem_ideleClassHerbrandSupport
    (v : HeightOneSpectrum (𝓞 K))
    (hv :
      v ∉ ideleClassHerbrandSupport (K := K) (L := L))
    (W : HeightOneSpectrum (𝓞 L))
    (hW : finitePlaceBelow (K := K) W = v) :
    Algebra.IsUnramifiedAt (𝓞 K) W.asIdeal

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