Module

IntegralLocalFactor.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Adele.IntegralLocalFactor

23 declarations indexed from sourceView source ↗

Module documentation

Integral finite local factors of the relative idele group

For a finite place w of the base field, the canonical local tensor decomposition identifies K_w ⊗_K L with the product of the completions of L above w. This file packages each projection as an actual ring homomorphism and defines the subgroup of tensor units whose value and inverse are integral in every completion factor. Thus the integrality predicate used for the restricted product is closed under all group operations for structural, rather than coordinate-dependent, reasons.

Imports10

Imported by4

def

finitePlaceLocalTensorDecompositionComponentRingHom

L51 ↗

Documentation

The projection of the finite local tensor algebra to one completion factor in the canonical local tensor decomposition, as a ring homomorphism.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
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 finitePlaceLocalTensorDecompositionComponentRingHom
    (w : HeightOneSpectrum (𝓞 K))
    (wL : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K w) L) :
    (w.adicCompletion K ⊗[K] L) →+* wL.1.Completion

theorem

finitePlaceLocalTensorDecompositionComponentRingHom_apply

L76 ↗

Documentation

The ring-homomorphism packaging evaluates to the original relative-tensor component map.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
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 finitePlaceLocalTensorDecompositionComponentRingHom_apply
    (w : HeightOneSpectrum (𝓞 K))
    (wL : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K w) L)
    (x : w.adicCompletion K ⊗[K] L) :
    finitePlaceLocalTensorDecompositionComponentRingHom
        (K := K) (L := L) w wL x =
      finitePlaceLocalTensorDecompositionComponent
        (K := K) (L := L) w wL x

theorem

finitePlaceLocalTensorDecompositionComponent_zero

L90 ↗

Documentation

Every relative-tensor component map sends zero to zero.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
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 finitePlaceLocalTensorDecompositionComponent_zero
    (w : HeightOneSpectrum (𝓞 K))
    (wL : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K w) L) :
    finitePlaceLocalTensorDecompositionComponent
        (K := K) (L := L) w wL 0 = 0

theorem

finitePlaceLocalTensorDecompositionComponent_add

L103 ↗

Documentation

Relative-tensor component maps preserve addition.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
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 finitePlaceLocalTensorDecompositionComponent_add
    (w : HeightOneSpectrum (𝓞 K))
    (wL : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K w) L)
    (x y : w.adicCompletion K ⊗[K] L) :
    finitePlaceLocalTensorDecompositionComponent
        (K := K) (L := L) w wL (x + y) =
      finitePlaceLocalTensorDecompositionComponent
          (K := K) (L := L) w wL x +
        finitePlaceLocalTensorDecompositionComponent
          (K := K) (L := L) w wL y

def

finitePlaceLocalTensorDecompositionUnitsComponent

L119 ↗

Documentation

The corresponding component homomorphism on units.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
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 finitePlaceLocalTensorDecompositionUnitsComponent
    (w : HeightOneSpectrum (𝓞 K))
    (wL : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K w) L) :
    (w.adicCompletion K ⊗[K] L)ˣ →*
      wL.1.Completionˣ

def

finitePlaceLocalTensorDecompositionUnitsEquiv

L131 ↗

Documentation

The canonical local tensor decomposition on the complete group of units of the finite local tensor algebra.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
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 finitePlaceLocalTensorDecompositionUnitsEquiv
    (w : HeightOneSpectrum (𝓞 K)) :
    (w.adicCompletion K ⊗[K] L)ˣ ≃*
      ∀ wL : AbsoluteValueExtension
          (HeightOneSpectrum.adicAbv K w) L,
        wL.1.Completionˣ

theorem

finitePlaceLocalTensorDecompositionUnitsEquiv_apply

L156 ↗

Documentation

The product equivalence on units evaluates componentwise through the corresponding unit homomorphism.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
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 finitePlaceLocalTensorDecompositionUnitsEquiv_apply
    (w : HeightOneSpectrum (𝓞 K))
    (x : (w.adicCompletion K ⊗[K] L)ˣ)
    (wL : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K w) L) :
    finitePlaceLocalTensorDecompositionUnitsEquiv
        (K := K) (L := L) w x wL =
      finitePlaceLocalTensorDecompositionUnitsComponent
        (K := K) (L := L) w wL x

theorem

finitePlaceLocalTensorDecompositionUnitsComponent_coe

L171 ↗

Documentation

Coercing a unit component to the completion agrees with applying the underlying tensor component map.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
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 finitePlaceLocalTensorDecompositionUnitsComponent_coe
    (w : HeightOneSpectrum (𝓞 K))
    (wL : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K w) L)
    (x : (w.adicCompletion K ⊗[K] L)ˣ) :
    ((finitePlaceLocalTensorDecompositionUnitsComponent
        (K := K) (L := L) w wL x :
          wL.1.Completionˣ) :
        wL.1.Completion) =
      finitePlaceLocalTensorDecompositionComponent
        (K := K) (L := L) w wL
        (x : w.adicCompletion K ⊗[K] L)

theorem

conjugateExtensionCompletionRingEquiv_norm_eq

L189 ↗

Documentation

The completion equivalence induced by conjugation preserves the norm exactly.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
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 K] [NumberField L]
    [FiniteDimensional K L] in

Lean source · statement

theorem conjugateExtensionCompletionRingEquiv_norm_eq
    (vK : AbsoluteValue K ℝ)
    (wL : AbsoluteValueExtension vK L)
    (σ : L ≃ₐ[K] L)
    (x :
      (absoluteValueExtensionConjugate
        vK wL σ).1.Completion) :
    ‖conjugateExtensionCompletionRingEquiv vK wL σ x‖ =
      ‖x‖

theorem

conjugateExtensionCompletionRingEquiv_mem_integers_iff

L211 ↗

Documentation

The conjugate-completion equivalence identifies the two valuation rings.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
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 K] [NumberField L]
    [FiniteDimensional K L] in

Lean source · statement

theorem
    conjugateExtensionCompletionRingEquiv_mem_integers_iff
    (vK : AbsoluteValue K ℝ)
    (hvK : IsNonarchimedean (vK : K → ℝ))
    (wL : AbsoluteValueExtension vK L)
    (σ : L ≃ₐ[K] L)
    (x :
      (absoluteValueExtensionConjugate
        vK wL σ).1.Completion) :
    conjugateExtensionCompletionRingEquiv vK wL σ x ∈
        absoluteValueCompletionIntegers wL.1
          (absoluteValueExtension_isNonarchimedean
            vK hvK wL) ↔
      x ∈
        absoluteValueCompletionIntegers
          (absoluteValueExtensionConjugate
            vK wL σ).1
          (absoluteValueExtension_isNonarchimedean
            vK hvK
            (absoluteValueExtensionConjugate
              vK wL σ))

theorem

finitePlaceLocalTensorDecompositionComponent_scalarTensorConjugation

L240 ↗

Documentation

Galois conjugation sends the component at wL to the component at the conjugate extension, transported by the canonical completion isometry.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
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 finitePlaceLocalTensorDecompositionComponent_scalarTensorConjugation
    (w : HeightOneSpectrum (𝓞 K))
    (wL : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K w) L)
    (σ : L ≃ₐ[K] L)
    (x : w.adicCompletion K ⊗[K] L) :
    finitePlaceLocalTensorDecompositionComponent
        (K := K) (L := L) w wL
        (scalarTensorConjugation
          (K := K) (L := L)
          (A := w.adicCompletion K) σ x) =
      conjugateExtensionCompletionRingEquiv
        (HeightOneSpectrum.adicAbv K w) wL σ
        (finitePlaceLocalTensorDecompositionComponent
          (K := K) (L := L) w
          (absoluteValueExtensionConjugate
            (HeightOneSpectrum.adicAbv K w) wL σ) x)

theorem

relativeLocalTensorDecompositionIntegralAt_scalarTensorConjugation

L294 ↗

Documentation

Valuation-ring integrality of a tensor element is preserved by Galois conjugation.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
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 relativeLocalTensorDecompositionIntegralAt_scalarTensorConjugation
    (w : HeightOneSpectrum (𝓞 K))
    (σ : L ≃ₐ[K] L)
    {x : w.adicCompletion K ⊗[K] L}
    (hx : RelativeLocalTensorDecompositionIntegralAt
      (K := K) (L := L) w x) :
    RelativeLocalTensorDecompositionIntegralAt
      (K := K) (L := L) w
      (scalarTensorConjugation
        (K := K) (L := L)
        (A := w.adicCompletion K) σ x)

theorem

relativeLocalTensorDecompositionIntegralUnitAt_smul

L321 ↗

Documentation

The integral tensor-unit condition is stable under the natural Galois action.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
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 · full declaration

theorem relativeLocalTensorDecompositionIntegralUnitAt_smul
    (w : HeightOneSpectrum (𝓞 K))
    (σ : L ≃ₐ[K] L)
    (x : (w.adicCompletion K ⊗[K] L)ˣ)
    (hx : RelativeLocalTensorDecompositionIntegralUnitAt
      (K := K) (L := L) w x) :
    letI := scalarTensorUnitsAction
      (K := K) (L := L)
      (A := w.adicCompletion K)
    RelativeLocalTensorDecompositionIntegralUnitAt
      (K := K) (L := L) w (σ • x) := by
  let := scalarTensorUnitsAction
    (K := K) (L := L)
    (A := w.adicCompletion K)
  constructor
  · change
      RelativeLocalTensorDecompositionIntegralAt
        (K := K) (L := L) w
        (↑(σ • x) :
          w.adicCompletion K ⊗[K] L)
    rw [scalarTensorUnitsAction_coe]
    exact
      relativeLocalTensorDecompositionIntegralAt_scalarTensorConjugation
        (K := K) (L := L) w σ hx.1
  · change
      RelativeLocalTensorDecompositionIntegralAt
        (K := K) (L := L) w
        (↑((σ • x)⁻¹) :
          w.adicCompletion K ⊗[K] L)
    rw [← smul_inv', scalarTensorUnitsAction_coe]
    exact
      relativeLocalTensorDecompositionIntegralAt_scalarTensorConjugation
        (K := K) (L := L) w σ hx.2

theorem

relativeLocalTensorDecompositionIntegralUnitAt_iff

L358 ↗

Documentation

Integrality of a tensor unit is exactly membership of every relative-tensor component in the unit subgroup of its valuation ring.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
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 relativeLocalTensorDecompositionIntegralUnitAt_iff
    (w : HeightOneSpectrum (𝓞 K))
    (x : (w.adicCompletion K ⊗[K] L)ˣ) :
    RelativeLocalTensorDecompositionIntegralUnitAt
        (K := K) (L := L) w x ↔
      ∀ wL : AbsoluteValueExtension
          (HeightOneSpectrum.adicAbv K w) L,
        finitePlaceLocalTensorDecompositionUnitsComponent
            (K := K) (L := L) w wL x ∈
          (absoluteValueCompletionIntegers wL.1
            (absoluteValueExtension_isNonarchimedean
              (HeightOneSpectrum.adicAbv K w)
              (HeightOneSpectrum.isNonarchimedean_adicAbv K w)
              wL)).units

def

relativeLocalTensorDecompositionIntegralUnitSubgroup

L394 ↗

Documentation

The actual integral-unit subgroup in a finite local tensor factor.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
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 relativeLocalTensorDecompositionIntegralUnitSubgroup
    (w : HeightOneSpectrum (𝓞 K)) :
    Subgroup (w.adicCompletion K ⊗[K] L)ˣ

abbrev

FinitePlaceLocalTensorDecompositionIntegralUnitProduct

L412 ↗

Documentation

The product of the actual valuation-ring unit groups in all completion factors above a finite base place.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
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 FinitePlaceLocalTensorDecompositionIntegralUnitProduct
    (w : HeightOneSpectrum (𝓞 K))

def

finitePlaceLocalTensorDecompositionIntegralUnitProductEquivPi

L425 ↗

Documentation

A product subgroup is the product of its component subgroup types.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
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 · full declaration

def
    finitePlaceLocalTensorDecompositionIntegralUnitProductEquivPi
    (w : HeightOneSpectrum (𝓞 K)) :
    FinitePlaceLocalTensorDecompositionIntegralUnitProduct
        (K := K) (L := L) w ≃*
      ∀ wL : AbsoluteValueExtension
          (HeightOneSpectrum.adicAbv K w) L,
        (absoluteValueCompletionIntegers wL.1
          (absoluteValueExtension_isNonarchimedean
            (HeightOneSpectrum.adicAbv K w)
            (HeightOneSpectrum.isNonarchimedean_adicAbv K w)
            wL)).units where
  toFun x wL :=
    ⟨x.1 wL, x.2 wL (Set.mem_univ wL)⟩
  invFun x :=
    ⟨fun wL => x wL, by
      intro wL hwL
      exact (x wL).2⟩
  left_inv x := by
    apply Subtype.ext
    rfl
  right_inv x := by
    funext wL
    apply Subtype.ext
    rfl
  map_mul' x y := by
    funext wL
    apply Subtype.ext
    rfl

def

finitePlaceLocalTensorDecompositionIntegralUnitProductEquivPiUnits

L457 ↗

Documentation

Replace each valuation-ring unit subgroup by the intrinsic unit group of the valuation ring.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
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
    finitePlaceLocalTensorDecompositionIntegralUnitProductEquivPiUnits
    (w : HeightOneSpectrum (𝓞 K)) :
    FinitePlaceLocalTensorDecompositionIntegralUnitProduct
        (K := K) (L := L) w ≃*
      ∀ wL : AbsoluteValueExtension
          (HeightOneSpectrum.adicAbv K w) L,
        (absoluteValueCompletionIntegers wL.1
          (absoluteValueExtension_isNonarchimedean
            (HeightOneSpectrum.adicAbv K w)
            (HeightOneSpectrum.isNonarchimedean_adicAbv K w)
            wL))ˣ

theorem

mem_relativeLocalTensorDecompositionIntegralUnitSubgroup_iff

L482 ↗

Documentation

Membership in the integral tensor-unit subgroup is exactly the pointwise valuation-ring integrality condition.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
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_relativeLocalTensorDecompositionIntegralUnitSubgroup_iff
    (w : HeightOneSpectrum (𝓞 K))
    (x : (w.adicCompletion K ⊗[K] L)ˣ) :
    x ∈ relativeLocalTensorDecompositionIntegralUnitSubgroup
        (K := K) (L := L) w ↔
      RelativeLocalTensorDecompositionIntegralUnitAt
        (K := K) (L := L) w x

def

relativeLocalTensorDecompositionIntegralUnitSubgroupAction

L497 ↗

Documentation

The restricted Galois action on the integral tensor-unit subgroup.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
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
    relativeLocalTensorDecompositionIntegralUnitSubgroupAction
    (w : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction
      (L ≃ₐ[K] L)
      (relativeLocalTensorDecompositionIntegralUnitSubgroup
        (K := K) (L := L) w)

theorem

relativeLocalTensorDecompositionIntegralUnitSubgroupAction_coe

L550 ↗

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
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 · full declaration

theorem
    relativeLocalTensorDecompositionIntegralUnitSubgroupAction_coe
    (w : HeightOneSpectrum (𝓞 K))
    (σ : L ≃ₐ[K] L)
    (x : relativeLocalTensorDecompositionIntegralUnitSubgroup
      (K := K) (L := L) w) :
    letI :=
      relativeLocalTensorDecompositionIntegralUnitSubgroupAction
        (K := K) (L := L) w
    ((σ • x :
        relativeLocalTensorDecompositionIntegralUnitSubgroup
          (K := K) (L := L) w) :
      (w.adicCompletion K ⊗[K] L)ˣ) =
      letI := scalarTensorUnitsAction
        (K := K) (L := L)
        (A := w.adicCompletion K)
      σ •
        (x : (w.adicCompletion K ⊗[K] L)ˣ) :=
  rfl

def

relativeLocalTensorDecompositionIntegralUnitSubgroupEquivProduct

L572 ↗

Documentation

The integral local tensor-unit subgroup is exactly the product of the valuation-ring unit groups occurring in the canonical local tensor decomposition.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
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 · full declaration

def
    relativeLocalTensorDecompositionIntegralUnitSubgroupEquivProduct
    (w : HeightOneSpectrum (𝓞 K)) :
    relativeLocalTensorDecompositionIntegralUnitSubgroup
        (K := K) (L := L) w ≃*
      FinitePlaceLocalTensorDecompositionIntegralUnitProduct
        (K := K) (L := L) w where
  toFun x := ⟨finitePlaceLocalTensorDecompositionUnitsEquiv
      (K := K) (L := L) w x, by
    have hx := x.property
    rw [mem_relativeLocalTensorDecompositionIntegralUnitSubgroup_iff,
      relativeLocalTensorDecompositionIntegralUnitAt_iff] at hx
    rw [Subgroup.mem_pi]
    intro wL hwL
    simpa only [finitePlaceLocalTensorDecompositionUnitsEquiv_apply] using
      (hx wL)⟩
  invFun y := ⟨(finitePlaceLocalTensorDecompositionUnitsEquiv
      (K := K) (L := L) w).symm y, by
    rw [mem_relativeLocalTensorDecompositionIntegralUnitSubgroup_iff,
      relativeLocalTensorDecompositionIntegralUnitAt_iff]
    intro wL
    have hy :
        finitePlaceLocalTensorDecompositionUnitsEquiv
            (K := K) (L := L) w
            ((finitePlaceLocalTensorDecompositionUnitsEquiv
              (K := K) (L := L) w).symm y) wL ∈
          (absoluteValueCompletionIntegers wL.1
            (absoluteValueExtension_isNonarchimedean
              (HeightOneSpectrum.adicAbv K w)
              (HeightOneSpectrum.isNonarchimedean_adicAbv K w)
              wL)).units := by
      rw [(finitePlaceLocalTensorDecompositionUnitsEquiv
        (K := K) (L := L) w).apply_symm_apply]
      exact y.property wL (Set.mem_univ wL)
    simpa only [finitePlaceLocalTensorDecompositionUnitsEquiv_apply] using hy⟩
  left_inv x := by
    apply Subtype.ext
    exact
      (finitePlaceLocalTensorDecompositionUnitsEquiv
        (K := K) (L := L) w).symm_apply_apply x
  right_inv y := by
    apply Subtype.ext
    exact
      (finitePlaceLocalTensorDecompositionUnitsEquiv
        (K := K) (L := L) w).apply_symm_apply y
  map_mul' x y := by
    apply Subtype.ext
    exact
      (finitePlaceLocalTensorDecompositionUnitsEquiv
        (K := K) (L := L) w).map_mul x y

def

relativeLocalTensorDecompositionIntegralUnitSubgroupEquivPiUnits

L625 ↗

Documentation

Final local form: the integral tensor units are the product of the intrinsic unit groups of all completion valuation rings above w.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
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
    relativeLocalTensorDecompositionIntegralUnitSubgroupEquivPiUnits
    (w : HeightOneSpectrum (𝓞 K)) :
    relativeLocalTensorDecompositionIntegralUnitSubgroup
        (K := K) (L := L) w ≃*
      ∀ wL : AbsoluteValueExtension
          (HeightOneSpectrum.adicAbv K w) L,
        (absoluteValueCompletionIntegers wL.1
          (absoluteValueExtension_isNonarchimedean
            (HeightOneSpectrum.adicAbv K w)
            (HeightOneSpectrum.isNonarchimedean_adicAbv K w)
            wL))ˣ

Module documentation

Integral finite local factors of the relative idele group

Declarations