Module

NormConductor.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.NormConductor

36 declarations indexed from sourceView source ↗

Module documentation

Narrow finite conductors of actual idele-class norm subgroups

For a finite Galois extension of number fields, the image of the idele-class norm contains an explicitly constructed ray congruence subgroup. At a ramified finite place we choose a sufficiently deep higher-unit group inside the open local norm subgroup. Outside the finite ramification set, the full local unit group already consists of norms. The archimedean positive subgroup is always contained in the corresponding tensor-norm image.

This produces a defining modulus directly from the actual extension. In particular, the idele-class norm range is open, closed, and of finite index. Its narrow finite conductor can only be supported at ramified finite places. The full conductor, including an archimedean component, is deliberately not defined here.

Imports8

Imported by12

instance

normConductorIdeleClassGroupIsMulCommutative

L53 ↗

GlobalClassFieldTheory.GlobalClassFields.normConductorIdeleClassGroupIsMulCommutative

Documentation

Fix the canonical commutative idèle-class structure used by the norm quotients in this module.

Source context 6 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)

theorem

exists_localHigherUnitGroup_le_chosenFinitePlaceLocalNormSubgroup

L62 ↗

GlobalClassFieldTheory.GlobalClassFields.exists_localHigherUnitGroup_le_chosenFinitePlaceLocalNormSubgroup

Documentation

Every chosen finite-place norm subgroup contains a local higher-unit group. This is the local source used to construct an actual defining modulus.

Source context 8 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField L] in

Lean source · statement

theorem exists_localHigherUnitGroup_le_chosenFinitePlaceLocalNormSubgroup
    (v : HeightOneSpectrum (𝓞 K)) :
    ∃ n : ℕ,
      RayClass.localHigherUnitGroup v n ≤
        _root_.chosenFinitePlaceLocalNormSubgroup
          (K := K) (L := L) v

def

ideleClassNormLocalHigherUnitExponent

L88 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormLocalHigherUnitExponent

Documentation

The least higher-unit exponent whose group lies in the chosen finite-place norm subgroup.

Source context 8 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
open scoped Classical in

Lean source · statement

def ideleClassNormLocalHigherUnitExponent
    (v : HeightOneSpectrum (𝓞 K)) : ℕ

theorem

ideleClassNormLocalHigherUnitExponent_spec

L98 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormLocalHigherUnitExponent_spec

Documentation

The local higher-unit group at the selected exponent lies in the chosen local norm subgroup.

Source context 9 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField L] in
open scoped Classical in

Lean source · statement

theorem ideleClassNormLocalHigherUnitExponent_spec
    (v : HeightOneSpectrum (𝓞 K)) :
    RayClass.localHigherUnitGroup v
        (ideleClassNormLocalHigherUnitExponent
          (K := K) (L := L) v) ≤
      _root_.chosenFinitePlaceLocalNormSubgroup
        (K := K) (L := L) v

theorem

ideleClassNormLocalHigherUnitExponent_min

L114 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormLocalHigherUnitExponent_min

Documentation

The selected local higher-unit exponent is minimal among all exponents whose higher-unit group lies in the chosen local norm subgroup.

Source context 9 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField L] in
open scoped Classical in

Lean source · statement

theorem ideleClassNormLocalHigherUnitExponent_min
    (v : HeightOneSpectrum (𝓞 K))
    {n : ℕ}
    (hn :
      RayClass.localHigherUnitGroup v n ≤
        _root_.chosenFinitePlaceLocalNormSubgroup
          (K := K) (L := L) v) :
    ideleClassNormLocalHigherUnitExponent
        (K := K) (L := L) v ≤ n

theorem

ideleClassNormLocalHigherUnitExponent_eq_zero_iff

L132 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormLocalHigherUnitExponent_eq_zero_iff

Documentation

The selected local exponent is zero exactly when every integral unit of the finite-place completion is a norm from the chosen localized extension.

Source context 8 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField L] in

Lean source · statement

theorem ideleClassNormLocalHigherUnitExponent_eq_zero_iff
    (v : HeightOneSpectrum (𝓞 K)) :
    ideleClassNormLocalHigherUnitExponent
        (K := K) (L := L) v = 0 ↔
      (v.adicCompletionIntegers K).units ≤
        _root_.chosenFinitePlaceLocalNormSubgroup
          (K := K) (L := L) v

theorem

ideleClassNormLocalHigherUnitExponent_eq_zero_of_chosenUnramified

L154 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormLocalHigherUnitExponent_eq_zero_of_chosenUnramified

Documentation

At an unramified chosen completion, the selected local exponent is zero because the whole local integral-unit group consists of norms.

Source context 8 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField L] in

Lean source · statement

theorem ideleClassNormLocalHigherUnitExponent_eq_zero_of_chosenUnramified
    (v : HeightOneSpectrum (𝓞 K))
    (hunram :
      _root_.ChosenFinitePlaceIsUnramified
        (K := K) (L := L) v) :
    ideleClassNormLocalHigherUnitExponent
        (K := K) (L := L) v = 0

theorem

ideleClassNormLocalHigherUnitExponent_eq_zero_of_not_mem_ramified

L173 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormLocalHigherUnitExponent_eq_zero_of_not_mem_ramified

Documentation

Outside the finite set of ramified base places, the selected local higher-unit exponent is zero.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem ideleClassNormLocalHigherUnitExponent_eq_zero_of_not_mem_ramified
    (v : HeightOneSpectrum (𝓞 K))
    (hv :
      v ∉ _root_.ramifiedBaseFinitePlaces
        (K := K) (L := L)) :
    ideleClassNormLocalHigherUnitExponent
        (K := K) (L := L) v = 0

def

ideleClassNormDefiningModulus

L200 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormDefiningModulus

Documentation

A finite modulus built from the actual local norm subgroups. Its support is contained in the finite set of ramified base places.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

def ideleClassNormDefiningModulus :
    RayClass.FiniteModulus K

theorem

ideleClassNormDefiningModulus_apply

L216 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormDefiningModulus_apply

Documentation

Evaluation of the actual norm defining modulus is the selected local higher-unit exponent.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem ideleClassNormDefiningModulus_apply
    (v : HeightOneSpectrum (𝓞 K)) :
    ideleClassNormDefiningModulus (K := K) (L := L) v =
      ideleClassNormLocalHigherUnitExponent
        (K := K) (L := L) v

theorem

ideleClassNormDefiningModulus_local_spec

L225 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormDefiningModulus_local_spec

Documentation

The local higher-unit group prescribed by the actual norm defining modulus lies in the chosen local norm subgroup at every finite place.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem ideleClassNormDefiningModulus_local_spec
    (v : HeightOneSpectrum (𝓞 K)) :
    RayClass.localHigherUnitGroup v
        (ideleClassNormDefiningModulus (K := K) (L := L) v) ≤
      _root_.chosenFinitePlaceLocalNormSubgroup
        (K := K) (L := L) v

theorem

ideleClassNormDefiningModulus_le_of_localHigherUnitGroup_le

L238 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormDefiningModulus_le_of_localHigherUnitGroup_le

Documentation

The norm defining modulus is pointwise minimal among all moduli whose prescribed local higher-unit groups consist of chosen local norms.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem ideleClassNormDefiningModulus_le_of_localHigherUnitGroup_le
    (m : RayClass.FiniteModulus K)
    (hm :
      ∀ v : HeightOneSpectrum (𝓞 K),
        RayClass.localHigherUnitGroup v (m v) ≤
          _root_.chosenFinitePlaceLocalNormSubgroup
            (K := K) (L := L) v) :
    ideleClassNormDefiningModulus (K := K) (L := L) ≤ m

theorem

mem_ideleClassNormDefiningModulus_support_iff

L255 ↗

GlobalClassFieldTheory.GlobalClassFields.mem_ideleClassNormDefiningModulus_support_iff

Documentation

A finite place occurs in the constructed norm modulus exactly when some integral unit at that place is not a norm from the chosen localized extension.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem mem_ideleClassNormDefiningModulus_support_iff
    (v : HeightOneSpectrum (𝓞 K)) :
    v ∈
        (ideleClassNormDefiningModulus
          (K := K) (L := L)).support ↔
      ¬ (v.adicCompletionIntegers K).units ≤
        _root_.chosenFinitePlaceLocalNormSubgroup
          (K := K) (L := L) v

theorem

ideleClassNormDefiningModulus_support_subset_ramifiedBaseFinitePlaces

L272 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormDefiningModulus_support_subset_ramifiedBaseFinitePlaces

Documentation

The constructed defining modulus is supported only at ramified finite places of the base field.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem ideleClassNormDefiningModulus_support_subset_ramifiedBaseFinitePlaces :
    (ideleClassNormDefiningModulus
        (K := K) (L := L)).support ⊆
      _root_.ramifiedBaseFinitePlaces
        (K := K) (L := L)

theorem

ideleCongruenceSubgroup_normDefiningModulus_le_relativeIdeleNorm_range

L290 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleCongruenceSubgroup_normDefiningModulus_le_relativeIdeleNorm_range

Documentation

The raw idele congruence subgroup of the constructed modulus lies in the image of the actual relative-idele norm.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    ideleCongruenceSubgroup_normDefiningModulus_le_relativeIdeleNorm_range :
    (RayClass.Modulus.narrowOfFinite
        (ideleClassNormDefiningModulus
          (K := K) (L := L))).ideleCongruenceSubgroup ≤
      (RelativeIdeleGroup.norm K L).range

theorem

ideleClassNormDefiningModulus_isDefiningModulus

L322 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormDefiningModulus_isDefiningModulus

Documentation

The explicitly constructed modulus is a defining modulus for the actual idele-class norm subgroup.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem ideleClassNormDefiningModulus_isDefiningModulus :
    IsDefiningModulus
      ((_root_.ideleClassNorm K L).range)
      (RayClass.Modulus.narrowOfFinite
        (ideleClassNormDefiningModulus (K := K) (L := L)))

def

ideleClassNormConductorialSubgroup

L366 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormConductorialSubgroup

Documentation

The conductorial subgroup supplied by the actual idèle-class norm range and its explicitly constructed defining modulus.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

def ideleClassNormConductorialSubgroup :
    ConductorialSubgroup K

def

ideleClassNormNarrowFiniteConductor

L375 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormNarrowFiniteConductor

Documentation

The narrow finite conductor of the actual idèle-class norm range.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

def ideleClassNormNarrowFiniteConductor :
    RayClass.FiniteModulus K

theorem

ideleClassNorm_range_isOpen

L382 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNorm_range_isOpen

Documentation

The actual idele-class norm subgroup is open in the ordinary idele-class topology.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem ideleClassNorm_range_isOpen :
    IsOpen
      (((_root_.ideleClassNorm K L).range :
        Subgroup (IdeleClassGroup K)) :
        Set (IdeleClassGroup K))

theorem

ideleClassNorm_range_isClosed

L392 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNorm_range_isClosed

Documentation

The actual idele-class norm subgroup is closed.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem ideleClassNorm_range_isClosed :
    IsClosed
      (((_root_.ideleClassNorm K L).range :
        Subgroup (IdeleClassGroup K)) :
        Set (IdeleClassGroup K))

instance

ideleClassNorm_rangeFiniteIndex

L401 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNorm_rangeFiniteIndex

Documentation

The actual idele-class norm subgroup has finite index.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

instance ideleClassNorm_rangeFiniteIndex :
    ((_root_.ideleClassNorm K L).range).FiniteIndex

theorem

ideleClassNorm_narrowFiniteConductor_isDefiningModulus

L408 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNorm_narrowFiniteConductor_isDefiningModulus

Documentation

The narrow finite conductor itself is a defining modulus for the actual idele-class norm subgroup.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem ideleClassNorm_narrowFiniteConductor_isDefiningModulus :
    IsDefiningModulus
      ((_root_.ideleClassNorm K L).range)
      (RayClass.Modulus.narrowOfFinite
        (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))

def

narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient

L418 ↗

GlobalClassFieldTheory.GlobalClassFields.narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient

Documentation

The canonical quotient map from the ray class group at the actual narrow finite norm conductor onto the actual idèle-class norm quotient.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

def
    narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient :
    RayClass.RayClassGroup
        (RayClass.Modulus.narrowOfFinite
          (ideleClassNormNarrowFiniteConductor (K := K) (L := L))) →*
      IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range

theorem

narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient_mk

L438 ↗

GlobalClassFieldTheory.GlobalClassFields.narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient_mk

Documentation

The narrow finite conductor ray-class quotient map sends an idèle class to its class modulo the actual norm subgroup.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient_mk
    (x : IdeleClassGroup K) :
    narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient
        (K := K) (L := L)
        (QuotientGroup.mk'
          (RayClass.Modulus.congruenceSubgroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor
                (K := K) (L := L)))) x) =
      QuotientGroup.mk'
        ((_root_.ideleClassNorm K L).range) x

theorem

narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient_surjective

L453 ↗

GlobalClassFieldTheory.GlobalClassFields.narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient_surjective

Documentation

The canonical map from the conductor ray class group to the actual idele-class norm quotient is surjective.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient_surjective :
    Function.Surjective
      (narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient
        (K := K) (L := L))

theorem

narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient_ker

L472 ↗

GlobalClassFieldTheory.GlobalClassFields.narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient_ker

Documentation

The kernel of the conductor ray-class quotient map is the image of the actual norm subgroup modulo the conductor congruence subgroup.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient_ker :
    MonoidHom.ker
        (narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient
          (K := K) (L := L)) =
      Subgroup.map
        (QuotientGroup.mk'
          (RayClass.Modulus.congruenceSubgroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor
                (K := K) (L := L)))))
        ((_root_.ideleClassNorm K L).range)

def

narrowFiniteConductorRayClassNormSubgroupQuotientEquivIdeleClassNormQuotient

L503 ↗

GlobalClassFieldTheory.GlobalClassFields.narrowFiniteConductorRayClassNormSubgroupQuotientEquivIdeleClassNormQuotient

Documentation

Quotienting the conductor ray class group by the image of the actual norm subgroup recovers the actual idele-class norm quotient.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

def
    narrowFiniteConductorRayClassNormSubgroupQuotientEquivIdeleClassNormQuotient :
    (RayClass.RayClassGroup
          (RayClass.Modulus.narrowOfFinite
            (ideleClassNormNarrowFiniteConductor
              (K := K) (L := L))) ⧸
        Subgroup.map
          (QuotientGroup.mk'
            (RayClass.Modulus.congruenceSubgroup
              (RayClass.Modulus.narrowOfFinite
                (ideleClassNormNarrowFiniteConductor
                  (K := K) (L := L)))))
          ((_root_.ideleClassNorm K L).range)) ≃*
      IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range

theorem

narrowFiniteConductorRayClassGroup_card_eq_normSubgroupImage_card_mul_normQuotient_card

L530 ↗

GlobalClassFieldTheory.GlobalClassFields.narrowFiniteConductorRayClassGroup_card_eq_normSubgroupImage_card_mul_normQuotient_card

Documentation

The conductor ray class number factors as the order of the norm subgroup modulo conductor congruence times the order of the actual idele-class norm quotient.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    narrowFiniteConductorRayClassGroup_card_eq_normSubgroupImage_card_mul_normQuotient_card :
    Nat.card
        (RayClass.RayClassGroup
          (RayClass.Modulus.narrowOfFinite
            (ideleClassNormNarrowFiniteConductor
              (K := K) (L := L)))) =
      Nat.card
          (Subgroup.map
            (QuotientGroup.mk'
              (RayClass.Modulus.congruenceSubgroup
                (RayClass.Modulus.narrowOfFinite
                  (ideleClassNormNarrowFiniteConductor
                    (K := K) (L := L)))))
            ((_root_.ideleClassNorm K L).range)) *
        Nat.card
          (IdeleClassGroup K ⧸
            (_root_.ideleClassNorm K L).range)

theorem

ideleClassNormQuotient_card_dvd_narrowFiniteConductorRayClassGroup_card

L588 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormQuotient_card_dvd_narrowFiniteConductorRayClassGroup_card

Documentation

The order of the actual idèle-class norm quotient divides the order of the ray class group at its narrow finite conductor.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    ideleClassNormQuotient_card_dvd_narrowFiniteConductorRayClassGroup_card :
    Nat.card
        (IdeleClassGroup K ⧸
          (_root_.ideleClassNorm K L).range) ∣
      Nat.card
        (RayClass.RayClassGroup
          (RayClass.Modulus.narrowOfFinite
            (ideleClassNormNarrowFiniteConductor
              (K := K) (L := L))))

theorem

ideleClassNorm_narrowFiniteConductor_le_normDefiningModulus

L605 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNorm_narrowFiniteConductor_le_normDefiningModulus

Documentation

The narrow finite conductor of the actual norm subgroup is bounded by the modulus obtained from the chosen local norm subgroups.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem ideleClassNorm_narrowFiniteConductor_le_normDefiningModulus :
    ideleClassNormNarrowFiniteConductor (K := K) (L := L) ≤
      ideleClassNormDefiningModulus (K := K) (L := L)

theorem

ideleClassNorm_narrowFiniteConductor_apply_le_localHigherUnitExponent

L616 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNorm_narrowFiniteConductor_apply_le_localHigherUnitExponent

Documentation

At every finite place, the exponent of the narrow finite conductor of the actual norm subgroup is bounded by the least higher-unit depth already contained in the chosen local norm subgroup.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem ideleClassNorm_narrowFiniteConductor_apply_le_localHigherUnitExponent
    (v : HeightOneSpectrum (𝓞 K)) :
    ideleClassNormNarrowFiniteConductor (K := K) (L := L) v ≤
      ideleClassNormLocalHigherUnitExponent
        (K := K) (L := L) v

theorem

ideleClassNorm_narrowFiniteConductor_support_subset_normDefiningModulus_support

L633 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNorm_narrowFiniteConductor_support_subset_normDefiningModulus_support

Documentation

Every finite prime occurring in the narrow finite conductor of the actual norm subgroup already occurs in the modulus constructed from the chosen local norm subgroups.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    ideleClassNorm_narrowFiniteConductor_support_subset_normDefiningModulus_support :
    (ideleClassNormNarrowFiniteConductor
      (K := K) (L := L)).support ⊆
      (ideleClassNormDefiningModulus
        (K := K) (L := L)).support

theorem

not_mem_ideleClassNorm_narrowFiniteConductor_support_of_localHigherUnitClassSubgroup_zero_le

L654 ↗

GlobalClassFieldTheory.GlobalClassFields.not_mem_ideleClassNorm_narrowFiniteConductor_support_of_localHigherUnitClassSubgroup_zero_le

Documentation

If the zeroth one-place higher-unit class subgroup lies in the actual idèle-class norm range, then that finite place is absent from the narrow finite conductor support.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    not_mem_ideleClassNorm_narrowFiniteConductor_support_of_localHigherUnitClassSubgroup_zero_le
    (v : HeightOneSpectrum (𝓞 K))
    (hlocal :
      RayClass.localHigherUnitClassSubgroup v 0 ≤
        (_root_.ideleClassNorm K L).range) :
    v ∉
      (ideleClassNormNarrowFiniteConductor
        (K := K) (L := L)).support

theorem

not_mem_ideleClassNorm_narrowFiniteConductor_support_of_isUnramifiedAt

L677 ↗

GlobalClassFieldTheory.GlobalClassFields.not_mem_ideleClassNorm_narrowFiniteConductor_support_of_isUnramifiedAt

Documentation

If the chosen prime of L above v is algebraically unramified, then v does not occur in the conductor of the actual idele-class norm subgroup.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    not_mem_ideleClassNorm_narrowFiniteConductor_support_of_isUnramifiedAt
    (v : HeightOneSpectrum (𝓞 K))
    (hunram :
      Algebra.IsUnramifiedAt (𝓞 K)
        (_root_.finitePlaceExtensionCentre
          (K := K) (L := L) v
          (_root_.chosenFinitePlaceExtension (L := L) v)).asIdeal) :
    v ∉
      (ideleClassNormNarrowFiniteConductor
        (K := K) (L := L)).support

theorem

not_mem_ideleClassNorm_narrowFiniteConductor_support_of_splitsCompletely

L697 ↗

GlobalClassFieldTheory.GlobalClassFields.not_mem_ideleClassNorm_narrowFiniteConductor_support_of_splitsCompletely

Documentation

A finite place which splits completely does not occur in the narrow finite conductor of the actual idèle-class norm subgroup.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    not_mem_ideleClassNorm_narrowFiniteConductor_support_of_splitsCompletely
    (v : HeightOneSpectrum (𝓞 K))
    (hsplit :
      _root_.FinitePlaceSplitsCompletely
        (K := K) (L := L) v) :
    v ∉
      (ideleClassNormNarrowFiniteConductor
        (K := K) (L := L)).support

theorem

ideleClassNorm_narrowFiniteConductor_support_subset_ramifiedBaseFinitePlaces

L718 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNorm_narrowFiniteConductor_support_subset_ramifiedBaseFinitePlaces

Documentation

The narrow finite conductor of an actual finite Galois idèle-class norm subgroup is supported only at ramified finite places of the base field.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain Topology
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Fix the canonical commutative idèle-class structure used by the norm
quotients in this module. -/
local instance normConductorIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem ideleClassNorm_narrowFiniteConductor_support_subset_ramifiedBaseFinitePlaces :
    (ideleClassNormNarrowFiniteConductor
      (K := K) (L := L)).support ⊆
      _root_.ramifiedBaseFinitePlaces
        (K := K) (L := L)

Module documentation

Narrow finite conductors of actual idele-class norm subgroups

Declarations