NYLL
Module

IdealClass.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.IdealClass
26 declarations indexed from sourceView source ↗

Module documentation

Extension of ideles and ideal classes

For a finite Galois extension of number fields, scalar extension of the relative adele algebra followed by the relative-to-ordinary comparison gives the usual extension map on ideles. This file descends that map to idele classes and compares it with extension of fractional ideals and ideal classes.

Imports5
Imported by5

Declarations

theorem

finitePlaceTensorUnitsEquivAboveAdic_localIdeleInclusion

L43 ↗
Documentation

On a base-field local unit, the finite relative-to-ordinary comparison is the canonical map to the chosen place above it.

Source context 7 commands

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

open scoped NumberField TensorProduct nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v w
variable
    (K : Type u) (L : Type v)
    [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 finitePlaceTensorUnitsEquivAboveAdic_localIdeleInclusion
    (w : HeightOneSpectrum (𝓞 K))
    (W : {W : HeightOneSpectrum (𝓞 L) //
      finitePlaceBelow (K := K) W = w})
    (x : (w.adicCompletion K)ˣ) :
    finitePlaceTensorUnitsEquivAboveAdic
        (K := K) (L := L) w
        (localIdeleInclusion
          (K := K) (L := L) w x) W =
      Units.map
        (finitePlaceAdicCompletionMap K L w W).toMonoidHom
        x
theorem

localOrder_finitePlaceAdicCompletionMap

L82 ↗
Documentation

Local orders under the canonical completion map are multiplied by the ramification index.

Source context 7 commands

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

open scoped NumberField TensorProduct nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v w
variable
    (K : Type u) (L : Type v)
    [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 localOrder_finitePlaceAdicCompletionMap
    (w : HeightOneSpectrum (𝓞 K))
    (W : {W : HeightOneSpectrum (𝓞 L) //
      finitePlaceBelow (K := K) W = w})
    (x : (w.adicCompletion K)ˣ) :
    (FiniteIdeleGroup.localOrder W.1
      (Units.map
        (finitePlaceAdicCompletionMap K L w W).toMonoidHom
        x)).toAdd =
      (w.asIdeal.ramificationIdx' W.1.asIdeal : ℤ) *
        (FiniteIdeleGroup.localOrder w x).toAdd
def

extension

L111 ↗
FractionalIdealGroup.extension
Documentation

Extension of nonzero fractional ideals along the inclusion of number fields.

Source context 8 commands

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

open scoped NumberField TensorProduct nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace FractionalIdealGroup
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
def extension :
    FractionalIdealGroup K →* FractionalIdealGroup L
theorem

extension_prime_val

L119 ↗
FractionalIdealGroup.extension_prime_val
Documentation

On a prime fractional ideal, extension is the fractional ideal associated with the mapped integral ideal.

Source context 8 commands

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

open scoped NumberField TensorProduct nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace FractionalIdealGroup
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem extension_prime_val
    (w : HeightOneSpectrum (𝓞 K)) :
    ((extension K L (prime w) : FractionalIdealGroup L) :
      FractionalIdeal (nonZeroDivisors (𝓞 L)) L) =
      (w.asIdeal.map (algebraMap (𝓞 K) (𝓞 L)) :
        FractionalIdeal (nonZeroDivisors (𝓞 L)) L)
theorem

count_extension_prime

L135 ↗
FractionalIdealGroup.count_extension_prime
Documentation

At a place above w, the exponent of the extended prime is the ramification index.

Source context 8 commands

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

open scoped NumberField TensorProduct nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace FractionalIdealGroup
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem count_extension_prime
    (w : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 L))
    (hW : _root_.finitePlaceBelow (K := K) W = w) :
    FractionalIdeal.count L W
      ((extension K L (prime w) : FractionalIdealGroup L) :
        FractionalIdeal (nonZeroDivisors (𝓞 L)) L) =
      (w.asIdeal.ramificationIdx' W.asIdeal : ℤ)
theorem

count_extension_prime_ne

L163 ↗
FractionalIdealGroup.count_extension_prime_ne
Documentation

A prime below a different place has zero exponent after extension.

Source context 8 commands

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

open scoped NumberField TensorProduct nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace FractionalIdealGroup
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem count_extension_prime_ne
    (w : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 L))
    (hW : _root_.finitePlaceBelow (K := K) W ≠ w) :
    FractionalIdeal.count L W
      ((extension K L (prime w) : FractionalIdealGroup L) :
        FractionalIdeal (nonZeroDivisors (𝓞 L)) L) = 0
theorem

count_extension_factorization

L192 ↗
FractionalIdealGroup.count_extension_factorization
Documentation

The exponent formula for extension of a fractional ideal presented by its prime factorization.

Source context 8 commands

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

open scoped NumberField TensorProduct nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace FractionalIdealGroup
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem count_extension_factorization
    (exps : Multiplicative
      (HeightOneSpectrum (𝓞 K) →₀ ℤ))
    (W : HeightOneSpectrum (𝓞 L)) :
    FractionalIdeal.count L W
      ((extension K L
          (factorization exps) : FractionalIdealGroup L) :
        FractionalIdeal (nonZeroDivisors (𝓞 L)) L) =
      ((_root_.finitePlaceBelow
          (K := K) W).asIdeal.ramificationIdx' W.asIdeal : ℤ) *
        exps.toAdd
          (_root_.finitePlaceBelow (K := K) W)
theorem

count_extension

L259 ↗
FractionalIdealGroup.count_extension
Documentation

Extension multiplies the exponent at W by the ramification index over the place below W.

Source context 8 commands

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

open scoped NumberField TensorProduct nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace FractionalIdealGroup
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem count_extension
    (I : FractionalIdealGroup K)
    (W : HeightOneSpectrum (𝓞 L)) :
    FractionalIdeal.count L W
      ((extension K L I : FractionalIdealGroup L) :
        FractionalIdeal (nonZeroDivisors (𝓞 L)) L) =
      ((_root_.finitePlaceBelow
          (K := K) W).asIdeal.ramificationIdx' W.asIdeal : ℤ) *
        FractionalIdeal.count K
          (_root_.finitePlaceBelow (K := K) W)
          (I : FractionalIdeal
            (nonZeroDivisors (𝓞 K)) K)
theorem

classGroup_mk_extension_prime

L280 ↗
FractionalIdealGroup.classGroup_mk_extension_prime
Documentation

Extension of a prime fractional ideal commutes with passage to the ideal class group.

Source context 8 commands

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

open scoped NumberField TensorProduct nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace FractionalIdealGroup
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem classGroup_mk_extension_prime
    (w : HeightOneSpectrum (𝓞 K)) :
    ClassGroup.mk L (extension K L (prime w)) =
      ClassGroup.extendedHom (𝓞 K) (𝓞 L)
        (ClassGroup.mk K (prime w))
theorem

classGroup_mk_extension

L304 ↗
FractionalIdealGroup.classGroup_mk_extension
Documentation

Extension of arbitrary fractional ideals commutes with passage to the ideal class group.

Source context 8 commands

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

open scoped NumberField TensorProduct nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace FractionalIdealGroup
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem classGroup_mk_extension
    (I : FractionalIdealGroup K) :
    ClassGroup.mk L (extension K L I) =
      ClassGroup.extendedHom (𝓞 K) (𝓞 L)
        (ClassGroup.mk K I)
theorem

ideal_map_isPrincipal_of_extendedHom_eq_one

L334 ↗
ClassGroup.ideal_map_isPrincipal_of_extendedHom_eq_one
Documentation

If extension of ideal classes is trivial, then the extension of each integral ideal is principal.

Source context 9 commands

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

open scoped NumberField TensorProduct nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace ClassGroup
section ExtensionPrincipality
variable
    (A B : Type*) [CommRing A] [CommRing B]
    [Algebra A B] [Module.IsTorsionFree A B]
    [IsDedekindDomain A] [IsDedekindDomain B]
Lean source · statement
theorem ideal_map_isPrincipal_of_extendedHom_eq_one
    (h : extendedHom A B = 1)
    (I : Ideal A) :
    (I.map (algebraMap A B)).IsPrincipal
theorem

extendedHom_eq_one_iff_forall_ideal_map_isPrincipal

L355 ↗
ClassGroup.extendedHom_eq_one_iff_forall_ideal_map_isPrincipal
Documentation

Triviality of the class-group extension map is exactly the principalization of every integral ideal.

Source context 9 commands

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

open scoped NumberField TensorProduct nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace ClassGroup
section ExtensionPrincipality
variable
    (A B : Type*) [CommRing A] [CommRing B]
    [Algebra A B] [Module.IsTorsionFree A B]
    [IsDedekindDomain A] [IsDedekindDomain B]
Lean source · statement
theorem extendedHom_eq_one_iff_forall_ideal_map_isPrincipal :
    extendedHom A B = 1 ↔
      ∀ I : Ideal A,
        (I.map (algebraMap A B)).IsPrincipal
def

extension

L372 ↗
IdeleGroup.extension
Documentation

The usual extension map on ideles, constructed through the relative tensor-product presentation.

Source context 7 commands

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

open scoped NumberField TensorProduct nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace IdeleGroup
Lean source · statement
def extension :
    IdeleGroup K →* IdeleGroup L
theorem

extension_infiniteComponent

L378 ↗
IdeleGroup.extension_infiniteComponent
Source context 8 commands

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

open scoped NumberField TensorProduct nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace IdeleGroup
omit [IsGalois K L] in
Lean source · full declaration
theorem extension_infiniteComponent
    (a : IdeleGroup K)
    (W : InfinitePlace L) :
    infiniteComponent W (extension K L a) =
      letI : Algebra.IsIntegral K L :=
        Algebra.IsIntegral.of_finite K L
      let v :=
        _root_.infinitePlaceBelow (K := K) W
      letI : W.1.LiesOver v.1 := ⟨rfl⟩
      Units.map
        (NumberField.LiesOver.completionMap
          (v := v) (w := W))
        (infiniteComponent v a) := by
  let : Algebra.IsIntegral K L :=
    Algebra.IsIntegral.of_finite K L
  let : Algebra.IsSeparable K L :=
    Algebra.IsSeparable.of_integral K L
  let v :=
    _root_.infinitePlaceBelow (K := K) W
  let : W.1.LiesOver v.1 := ⟨rfl⟩
  apply Units.ext
  change
    (ContinuousMulEquiv.piUnits (extension K L a).1 W :
      W.Completion) = _
  change
    (ContinuousMulEquiv.piUnits
      (_root_.relativeIdeleBaseChangeMulEquiv
        (K := K) (L := L)
        (RelativeIdeleGroup.inclusion K L a)).1 W :
      W.Completion) = _
  rw [_root_.relativeIdeleBaseChangeMulEquiv_infinite]
  let f :=
    _root_.relativeInfiniteTensorPiMulEquiv
      (K := K) (L := L)
      ((_root_.relativeIdeleToLocalData
        (K := K) (L := L)
        (RelativeIdeleGroup.inclusion K L a)).infinite)
  change
    (ContinuousMulEquiv.piUnits
      (ContinuousMulEquiv.piUnits.symm f) W :
      W.Completion) = _
  rw [ContinuousMulEquiv.piUnits.apply_symm_apply]
  dsimp only [f]
  rw [_root_.relativeInfiniteTensorPiMulEquiv_apply]
  simp only [_root_.relativeIdeleToLocalData]
  rw [RelativeIdeleGroup.infiniteComponent_inclusion]
  rw [_root_.infinitePlaceTensorUnitsEquivAbove_apply]
  simp only [Units.coe_map]
  change
    _root_.infinitePlaceTensorRingEquivAbove
        (K := K) (L := L) v
        ((infiniteComponent v a : v.Completion) ⊗ₜ[K] (1 : L))
        ⟨W, rfl⟩ =
      NumberField.LiesOver.completionMap
        (v := v) (w := W)
        (infiniteComponent v a : v.Completion)
  simpa only [map_one, mul_one] using
    (_root_.infinitePlaceTensorRingEquivAbove_tmul
      (K := K) (L := L) v ⟨W, rfl⟩
      (infiniteComponent v a : v.Completion) (1 : L))
theorem

extension_finiteComponent

L443 ↗
IdeleGroup.extension_finiteComponent
Documentation

The finite component of an extended idele is the canonical local completion map applied to the component below it.

Source context 8 commands

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

open scoped NumberField TensorProduct nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace IdeleGroup
omit [IsGalois K L] in
Lean source · statement
theorem extension_finiteComponent
    (a : IdeleGroup K)
    (W : HeightOneSpectrum (𝓞 L)) :
    finiteComponent W (extension K L a) =
      Units.map
        (finitePlaceAdicCompletionMap K L
          (_root_.finitePlaceBelow (K := K) W)
          ⟨W, rfl⟩).toMonoidHom
        (finiteComponent
          (_root_.finitePlaceBelow (K := K) W) a)
theorem

extension_localOrder

L480 ↗
IdeleGroup.extension_localOrder
Documentation

The local order of an extended idele is multiplied by the ramification index at the chosen place above.

Source context 8 commands

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

open scoped NumberField TensorProduct nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace IdeleGroup
omit [IsGalois K L] in
Lean source · statement
theorem extension_localOrder
    (a : IdeleGroup K)
    (W : HeightOneSpectrum (𝓞 L)) :
    (FiniteIdeleGroup.localOrder W
      (finiteComponent W (extension K L a))).toAdd =
      ((_root_.finitePlaceBelow
          (K := K) W).asIdeal.ramificationIdx' W.asIdeal : ℤ) *
        (FiniteIdeleGroup.localOrder
          (_root_.finitePlaceBelow (K := K) W)
          (finiteComponent
            (_root_.finitePlaceBelow (K := K) W) a)).toAdd
theorem

fractionalIdeal_extension

L501 ↗
IdeleGroup.fractionalIdeal_extension
Documentation

The fractional ideal attached to an extended idele is the extension of the fractional ideal attached to the original idele.

Source context 8 commands

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

open scoped NumberField TensorProduct nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace IdeleGroup
omit [IsGalois K L] in
Lean source · statement
theorem fractionalIdeal_extension
    (a : IdeleGroup K) :
    fractionalIdeal (extension K L a) =
      FractionalIdealGroup.extension K L
        (fractionalIdeal a)
theorem

idealClass_extension

L532 ↗
IdeleGroup.idealClass_extension
Documentation

The ideal class attached to an extended idele is the extension of the ideal class attached to the original idele.

Source context 8 commands

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

open scoped NumberField TensorProduct nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace IdeleGroup
omit [IsGalois K L] in
Lean source · statement
theorem idealClass_extension
    (a : IdeleGroup K) :
    idealClass (extension K L a) =
      ClassGroup.extendedHom (𝓞 K) (𝓞 L)
        (idealClass a)
theorem

extension_mem_ordinaryIdealClassSubgroup

L548 ↗
IdeleGroup.extension_mem_ordinaryIdealClassSubgroup
Documentation

Extension sends the subgroup defining the ordinary ideal class quotient into the corresponding subgroup over the extension field.

Source context 8 commands

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

open scoped NumberField TensorProduct nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace IdeleGroup
omit [IsGalois K L] in
Lean source · statement
theorem extension_mem_ordinaryIdealClassSubgroup
    {a : IdeleGroup K}
    (ha : a ∈
      integralAtFinitePlaces (K := K) ⊔
        principalSubgroup K) :
    extension K L a ∈
      integralAtFinitePlaces (K := L) ⊔
        principalSubgroup L
theorem

extension_principalIdele

L566 ↗
IdeleGroup.extension_principalIdele
Documentation

Extension of a principal idele is the corresponding principal idele of the extension field.

Source context 8 commands

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

open scoped NumberField TensorProduct nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace IdeleGroup
omit [IsGalois K L] in
Lean source · statement
theorem extension_principalIdele (x : Kˣ) :
    extension K L (principalIdele K x) =
      principalIdele L
        (Units.map (algebraMap K L).toMonoidHom x)
theorem

extension_self

L624 ↗
IdeleGroup.extension_self
Documentation

Extension of ideles along the identity field extension is the identity homomorphism.

Source context 7 commands

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

open scoped NumberField TensorProduct nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace IdeleGroup
Lean source · statement
theorem extension_self :
    extension K K = MonoidHom.id (IdeleGroup K)
theorem

extension_comp

L698 ↗
IdeleGroup.extension_comp
Documentation

Extension of ideles is functorial in a tower of finite Galois extensions.

Source context 7 commands

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

open scoped NumberField TensorProduct nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace IdeleGroup
Lean source · statement
theorem extension_comp
    (M : Type w)
    [Field M] [NumberField M]
    [Algebra K M] [Algebra M L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L]
    [IsGalois K M] [IsGalois M L] :
    (extension M L).comp (extension K M) =
      extension K L
def

ideleClassExtension

L816 ↗
Documentation

The usual extension map on idele classes.

Source context 6 commands

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

open scoped NumberField TensorProduct nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def ideleClassExtension :
    IdeleClassGroup K →* IdeleClassGroup L
theorem

ideleClassExtension_mk

L830 ↗
Source context 7 commands

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

open scoped NumberField TensorProduct nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v w
variable
    (K : Type u) (L : Type v)
    [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 ideleClassExtension_mk (a : IdeleGroup K) :
    ideleClassExtension K L
        (QuotientGroup.mk'
          (IdeleGroup.principalSubgroup K) a) =
      QuotientGroup.mk'
        (IdeleGroup.principalSubgroup L)
        (IdeleGroup.extension K L a)
theorem

ideleClassExtension_self

L842 ↗
Documentation

Extension of idele classes along the identity field extension is the identity homomorphism.

Source context 6 commands

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

open scoped NumberField TensorProduct nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem ideleClassExtension_self :
    ideleClassExtension K K =
      MonoidHom.id (IdeleClassGroup K)
theorem

ideleClassExtension_comp

L861 ↗
Documentation

Extension of idele classes is functorial in a tower of finite Galois extensions.

Source context 6 commands

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

open scoped NumberField TensorProduct nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem ideleClassExtension_comp
    (M : Type w)
    [Field M] [NumberField M]
    [Algebra K M] [Algebra M L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L]
    [IsGalois K M] [IsGalois M L] :
    (ideleClassExtension M L).comp
        (ideleClassExtension K M) =
      ideleClassExtension K L

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