NYLL
Module

Support.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Relative.Support
25 declarations indexed from sourceView source β†—

Module documentation

Finite coefficient support for relative ideles

This file supplies the finite-support input for the actual scalar-extension model

𝔸_K βŠ—[K] L.

Fixing the canonical chosen K-basis of L, every relative adele has finitely many base-adele coefficients. For a relative idele we take the union of the nonintegral finite places of the coefficients of the idele and of its inverse. Outside this finite set both local tensor components therefore lie in the lattice spanned by that basis over the local valuation ring.

This produces the finite support from a basis lattice. Passing from that lattice to the product of local integer rings additionally requires integral compatibility of the relative tensor decomposition.

Imports1
Imported by3

Declarations

abbrev

RelativeAdeleBasisIndex

L43 β†—
Documentation

The finite index type of the canonical chosen K-basis of L.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source Β· statement
abbrev RelativeAdeleBasisIndex
def

relativeExtensionBasis

L48 β†—
Documentation

The canonical chosen K-basis used to extract base-adele coefficients.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source Β· statement
def relativeExtensionBasis :
    Module.Basis (RelativeAdeleBasisIndex (K := K) (L := L)) K L
def

relativeAdeleBasis

L53 β†—
Documentation

Scalar extension of the chosen basis from K to 𝔸_K.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source Β· statement
def relativeAdeleBasis :
    Module.Basis (RelativeAdeleBasisIndex (K := K) (L := L))
      (NumberField.AdeleRing (π“ž K) K)
      (RelativeAdeleRing K L)
def

relativeAdeleCoefficient

L62 β†—
Documentation

The i-th base-adele coefficient of a relative adele.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source Β· statement
def relativeAdeleCoefficient
    (z : RelativeAdeleRing K L)
    (i : RelativeAdeleBasisIndex (K := K) (L := L)) :
    NumberField.AdeleRing (π“ž K) K
theorem

relativeAdele_eq_sum_tmul_coefficients

L70 β†—
Documentation

Expansion of a relative adele in the chosen extension basis.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem relativeAdele_eq_sum_tmul_coefficients
    (z : RelativeAdeleRing K L) :
    z =
      βˆ‘ i : RelativeAdeleBasisIndex (K := K) (L := L),
        relativeAdeleCoefficient
            (K := K) (L := L) z i βŠ—β‚œ[K]
          relativeExtensionBasis (K := K) (L := L) i
theorem

relativeAdeleFiniteComponent_eq_sum_tmul_coefficients

L87 β†—
Documentation

Evaluation at a finite place is coefficientwise in the chosen basis expansion.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem relativeAdeleFiniteComponent_eq_sum_tmul_coefficients
    (z : RelativeAdeleRing K L)
    (w : HeightOneSpectrum (π“ž K)) :
    relativeAdeleFiniteComponent
        (K := K) (L := L) w z =
      βˆ‘ i : RelativeAdeleBasisIndex (K := K) (L := L),
        (relativeAdeleCoefficient
            (K := K) (L := L) z i).2 w βŠ—β‚œ[K]
          relativeExtensionBasis (K := K) (L := L) i
theorem

relativeAdeleInfiniteComponent_eq_sum_tmul_coefficients

L108 β†—
Documentation

Evaluation at an infinite place is coefficientwise in the chosen basis expansion.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem relativeAdeleInfiniteComponent_eq_sum_tmul_coefficients
    (z : RelativeAdeleRing K L)
    (w : InfinitePlace K) :
    relativeAdeleInfiniteComponent
        (K := K) (L := L) w z =
      βˆ‘ i : RelativeAdeleBasisIndex (K := K) (L := L),
        (relativeAdeleCoefficient
            (K := K) (L := L) z i).1 w βŠ—β‚œ[K]
          relativeExtensionBasis (K := K) (L := L) i
theorem

finite_adeleNonIntegralPlaces

L128 β†—
Documentation

The set of places at which a base adele is not in the local valuation ring is finite.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source Β· statement
theorem finite_adeleNonIntegralPlaces
    (a : NumberField.AdeleRing (π“ž K) K) :
    {w : HeightOneSpectrum (π“ž K) |
      a.2 w βˆ‰ w.adicCompletionIntegers K}.Finite
def

adeleNonIntegralPlaces

L136 β†—
Documentation

The exceptional finite places at which a base adele is not in the local valuation ring.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source Β· statement
def adeleNonIntegralPlaces
    (a : NumberField.AdeleRing (π“ž K) K) :
    Finset (HeightOneSpectrum (π“ž K))
theorem

mem_adeleNonIntegralPlaces_iff

L142 β†—
Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source Β· statement
theorem mem_adeleNonIntegralPlaces_iff
    (a : NumberField.AdeleRing (π“ž K) K)
    (w : HeightOneSpectrum (π“ž K)) :
    w ∈ adeleNonIntegralPlaces (K := K) a ↔
      a.2 w βˆ‰ w.adicCompletionIntegers K
theorem

adele_component_mem_integers_of_notMem

L153 β†—
Documentation

Away from its exact exceptional finset, a base adele has integral finite component.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source Β· statement
theorem adele_component_mem_integers_of_notMem
    (a : NumberField.AdeleRing (π“ž K) K)
    (w : HeightOneSpectrum (π“ž K))
    (hw : w βˆ‰ adeleNonIntegralPlaces (K := K) a) :
    a.2 w ∈ w.adicCompletionIntegers K
def

relativeAdeleCoefficientSupport

L165 β†—
Documentation

Exact union of all exceptional coefficient places of a relative adele.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source Β· statement
def relativeAdeleCoefficientSupport
    (z : RelativeAdeleRing K L) :
    Finset (HeightOneSpectrum (π“ž K))
theorem

mem_relativeAdeleCoefficientSupport_iff

L177 β†—
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem mem_relativeAdeleCoefficientSupport_iff
    (z : RelativeAdeleRing K L)
    (w : HeightOneSpectrum (π“ž K)) :
    w ∈ relativeAdeleCoefficientSupport
        (K := K) (L := L) z ↔
      βˆƒ i : RelativeAdeleBasisIndex (K := K) (L := L),
        (relativeAdeleCoefficient
            (K := K) (L := L) z i).2 w βˆ‰
          w.adicCompletionIntegers K
def

relativeIdeleCoefficientSupport

L191 β†—
Documentation

The exact coefficient support of a relative idele contains the exceptional places of the idele and its inverse.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source Β· statement
def relativeIdeleCoefficientSupport
    (z : RelativeIdeleGroup K L) :
    Finset (HeightOneSpectrum (π“ž K))
theorem

mem_relativeIdeleCoefficientSupport_iff

L206 β†—
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem mem_relativeIdeleCoefficientSupport_iff
    (z : RelativeIdeleGroup K L)
    (w : HeightOneSpectrum (π“ž K)) :
    w ∈ relativeIdeleCoefficientSupport
        (K := K) (L := L) z ↔
      (βˆƒ i : RelativeAdeleBasisIndex (K := K) (L := L),
        (relativeAdeleCoefficient
            (K := K) (L := L)
            (z : RelativeAdeleRing K L) i).2 w βˆ‰
          w.adicCompletionIntegers K) ∨
      (βˆƒ i : RelativeAdeleBasisIndex (K := K) (L := L),
        (relativeAdeleCoefficient
            (K := K) (L := L)
            ((z⁻¹ : RelativeIdeleGroup K L) :
              RelativeAdeleRing K L) i).2 w βˆ‰
          w.adicCompletionIntegers K)
theorem

relativeIdele_coefficients_integral_of_notMem

L229 β†—
Documentation

Outside the exact coefficient support, every coefficient of both the relative idele and its inverse is integral at the given finite place.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem relativeIdele_coefficients_integral_of_notMem
    (z : RelativeIdeleGroup K L)
    (w : HeightOneSpectrum (π“ž K))
    (hw : w βˆ‰ relativeIdeleCoefficientSupport
      (K := K) (L := L) z) :
    (βˆ€ i : RelativeAdeleBasisIndex (K := K) (L := L),
      (relativeAdeleCoefficient
          (K := K) (L := L)
          (z : RelativeAdeleRing K L) i).2 w ∈
        w.adicCompletionIntegers K) ∧
    (βˆ€ i : RelativeAdeleBasisIndex (K := K) (L := L),
      (relativeAdeleCoefficient
          (K := K) (L := L)
          ((z⁻¹ : RelativeIdeleGroup K L) :
            RelativeAdeleRing K L) i).2 w ∈
        w.adicCompletionIntegers K)
theorem

relativeIdeleCoefficientSupport_minimal

L264 β†—
Documentation

The exact support is the least finset outside which all coefficients of the idele and its inverse are integral.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem relativeIdeleCoefficientSupport_minimal
    (z : RelativeIdeleGroup K L)
    (S : Finset (HeightOneSpectrum (π“ž K)))
    (hS :
      βˆ€ w, w βˆ‰ S β†’
        (βˆ€ i : RelativeAdeleBasisIndex (K := K) (L := L),
          (relativeAdeleCoefficient
              (K := K) (L := L)
              (z : RelativeAdeleRing K L) i).2 w ∈
            w.adicCompletionIntegers K) ∧
        (βˆ€ i : RelativeAdeleBasisIndex (K := K) (L := L),
          (relativeAdeleCoefficient
              (K := K) (L := L)
              ((z⁻¹ : RelativeIdeleGroup K L) :
                RelativeAdeleRing K L) i).2 w ∈
            w.adicCompletionIntegers K)) :
    relativeIdeleCoefficientSupport
        (K := K) (L := L) z βŠ† S
def

RelativeBasisIntegralAt

L296 β†—
Documentation

Basis-lattice integrality in the local tensor algebra: all coordinates in the fixed extension basis belong to the valuation ring of K_w.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
def RelativeBasisIntegralAt
    (w : HeightOneSpectrum (π“ž K))
    (x : w.adicCompletion K βŠ—[K] L) : Prop
def

RelativeBasisIntegralUnitAt

L311 β†—
Documentation

A local tensor unit is basis-integral when both it and its inverse belong to the local valuation-ring coefficient lattice.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
def RelativeBasisIntegralUnitAt
    (w : HeightOneSpectrum (π“ž K))
    (x : (w.adicCompletion K βŠ—[K] L)Λ£) : Prop
theorem

relativeIdele_finiteComponent_eq_sum_tmul_coefficients

L325 β†—
Documentation

The finite component of a relative idele is given by the evaluated base-adele coefficients.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem relativeIdele_finiteComponent_eq_sum_tmul_coefficients
    (z : RelativeIdeleGroup K L)
    (w : HeightOneSpectrum (π“ž K)) :
    ((RelativeIdeleGroup.finiteComponent
        (K := K) (L := L) w z :
        (w.adicCompletion K βŠ—[K] L)Λ£) :
        w.adicCompletion K βŠ—[K] L) =
      βˆ‘ i : RelativeAdeleBasisIndex (K := K) (L := L),
        (relativeAdeleCoefficient
            (K := K) (L := L)
            (z : RelativeAdeleRing K L) i).2 w βŠ—β‚œ[K]
          relativeExtensionBasis (K := K) (L := L) i
theorem

relativeIdele_finiteComponent_basisIntegral_of_notMem

L346 β†—
Documentation

Outside the coefficient support, the actual finite component lies in the local lattice spanned by the chosen extension basis.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem relativeIdele_finiteComponent_basisIntegral_of_notMem
    (z : RelativeIdeleGroup K L)
    (w : HeightOneSpectrum (π“ž K))
    (hw : w βˆ‰ relativeIdeleCoefficientSupport
      (K := K) (L := L) z) :
    RelativeBasisIntegralAt
      (K := K) (L := L) w
      ((RelativeIdeleGroup.finiteComponent
          (K := K) (L := L) w z :
          (w.adicCompletion K βŠ—[K] L)Λ£) :
          w.adicCompletion K βŠ—[K] L)
theorem

relativeIdele_inverse_finiteComponent_basisIntegral_of_notMem

L374 β†—
Documentation

Outside the same support, the actual finite component of the inverse lies in the same local basis lattice.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem relativeIdele_inverse_finiteComponent_basisIntegral_of_notMem
    (z : RelativeIdeleGroup K L)
    (w : HeightOneSpectrum (π“ž K))
    (hw : w βˆ‰ relativeIdeleCoefficientSupport
      (K := K) (L := L) z) :
    RelativeBasisIntegralAt
      (K := K) (L := L) w
      ((RelativeIdeleGroup.finiteComponent
          (K := K) (L := L) w
          (z⁻¹ : RelativeIdeleGroup K L) :
          (w.adicCompletion K βŠ—[K] L)Λ£) :
          w.adicCompletion K βŠ—[K] L)
theorem

relativeIdele_finiteComponent_inv_basisIntegral_of_notMem

L405 β†—
Documentation

Equivalently, the inverse of the actual local unit component lies in the same basis lattice outside the coefficient support.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem relativeIdele_finiteComponent_inv_basisIntegral_of_notMem
    (z : RelativeIdeleGroup K L)
    (w : HeightOneSpectrum (π“ž K))
    (hw : w βˆ‰ relativeIdeleCoefficientSupport
      (K := K) (L := L) z) :
    RelativeBasisIntegralAt
      (K := K) (L := L) w
      ((((RelativeIdeleGroup.finiteComponent
          (K := K) (L := L) w z)⁻¹ :
          (w.adicCompletion K βŠ—[K] L)Λ£) :
          w.adicCompletion K βŠ—[K] L))
theorem

relativeIdele_finiteComponent_basisIntegralUnit_of_notMem

L423 β†—
Documentation

Thus the actual local unit component is basis-integral outside the explicit coefficient support.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem relativeIdele_finiteComponent_basisIntegralUnit_of_notMem
    (z : RelativeIdeleGroup K L)
    (w : HeightOneSpectrum (π“ž K))
    (hw : w βˆ‰ relativeIdeleCoefficientSupport
      (K := K) (L := L) z) :
    RelativeBasisIntegralUnitAt
      (K := K) (L := L) w
      (RelativeIdeleGroup.finiteComponent
        (K := K) (L := L) w z)
theorem

exists_relativeIdele_coefficientSupport

L441 β†—
Documentation

A source-producing finite-support theorem: one explicit minimal finset simultaneously controls the local basis integrality of the relative idele and its inverse.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· statement
theorem exists_relativeIdele_coefficientSupport
    (z : RelativeIdeleGroup K L) :
    βˆƒ S : Finset (HeightOneSpectrum (π“ž K)),
      (βˆ€ w, w βˆ‰ S β†’
        (βˆ€ i : RelativeAdeleBasisIndex (K := K) (L := L),
          (relativeAdeleCoefficient
              (K := K) (L := L)
              (z : RelativeAdeleRing K L) i).2 w ∈
            w.adicCompletionIntegers K) ∧
        (βˆ€ i : RelativeAdeleBasisIndex (K := K) (L := L),
          (relativeAdeleCoefficient
              (K := K) (L := L)
              ((z⁻¹ : RelativeIdeleGroup K L) :
                RelativeAdeleRing K L) i).2 w ∈
            w.adicCompletionIntegers K)) ∧
      (βˆ€ w, w βˆ‰ S β†’
        RelativeBasisIntegralAt
          (K := K) (L := L) w
          ((RelativeIdeleGroup.finiteComponent
              (K := K) (L := L) w z :
              (w.adicCompletion K βŠ—[K] L)Λ£) :
              w.adicCompletion K βŠ—[K] L) ∧
        RelativeBasisIntegralAt
          (K := K) (L := L) w
          ((((RelativeIdeleGroup.finiteComponent
              (K := K) (L := L) w z)⁻¹ :
              (w.adicCompletion K βŠ—[K] L)Λ£) :
              w.adicCompletion K βŠ—[K] L)))

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