Module

RayClassModulus.lean

Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.RayClassModulus

11 declarations indexed from sourceView source ↗

Module documentation

Ray class moduli

A modulus consists of finite-prime exponents and a finite set of real places.

Imports5

Mathlib.Algebra.FiniteSupport.Defs
Mathlib.Order.Preorder.Finsupp
Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Mathlib.RingTheory.DedekindDomain.Factorization

Imported by8

abbrev

RayClassRealPlace

L31 ↗

ClassFieldTheory.RayClassRealPlace

Documentation

A real infinite place of a number field.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u

Lean source · statement

abbrev RayClassRealPlace
    (K : Type u) [Field K] [NumberField K]

structure

RayClassModulus

L37 ↗

ClassFieldTheory.RayClassModulus

Documentation

A ray modulus: finite prime exponents together with the real places at which positivity is imposed.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u

Lean source · full declaration

structure RayClassModulus
    (K : Type u) [Field K] [NumberField K] where
  /-- The finite prime-power part. -/
  finitePart : HeightOneSpectrum (𝓞 K) →₀ ℕ
  /-- The selected real places. -/
  infinitePart : Finset (RayClassRealPlace K)

theorem

ext

L47 ↗

ClassFieldTheory.RayClassModulus.ext

Documentation

Ray moduli are equal when their finite exponents and real-place sets agree.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
namespace RayClassModulus

Lean source · statement

theorem ext
    {K : Type u} [Field K] [NumberField K]
    {m n : RayClassModulus K}
    (hfinite : m.finitePart = n.finitePart)
    (hinfinite : m.infinitePart = n.infinitePart) : m = n

instance

(anonymous instance)

L58 ↗

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
namespace RayClassModulus

Lean source · full declaration

instance {K : Type u} [Field K] [NumberField K] : LE (RayClassModulus K) where
  le m n :=
    m.finitePart ≤ n.finitePart ∧ m.infinitePart ⊆ n.infinitePart

instance

(anonymous instance)

L62 ↗

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
namespace RayClassModulus

Lean source · full declaration

instance {K : Type u} [Field K] [NumberField K] :
    PartialOrder (RayClassModulus K) where
  le_refl m := ⟨le_rfl, fun _ hx => hx⟩
  le_trans _ _ _ hmn hnp :=
    ⟨hmn.1.trans hnp.1, fun _ hx => hnp.2 (hmn.2 hx)⟩
  le_antisymm m n hmn hnm := by
    cases m with
    | mk mfinite minfinite =>
      cases n with
      | mk nfinite ninfinite =>
        have hfinite : mfinite = nfinite :=
          le_antisymm hmn.1 hnm.1
        have hinfinite : minfinite = ninfinite := by
          apply Finset.ext
          intro x
          exact ⟨fun hx => hmn.2 hx, fun hx => hnm.2 hx⟩
        cases hfinite
        cases hinfinite
        rfl

theorem

le_iff

L84 ↗

ClassFieldTheory.RayClassModulus.le_iff

Documentation

Modulus divisibility is exponentwise at finite primes and inclusion at real places.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
namespace RayClassModulus

Lean source · statement

theorem le_iff
    {K : Type u} [Field K] [NumberField K]
    (m n : RayClassModulus K) :
    m ≤ n ↔
      (∀ v, m.finitePart v ≤ n.finitePart v) ∧
        m.infinitePart ⊆ n.infinitePart

instance

(anonymous instance)

L94 ↗

Documentation

Meet takes the minimum finite-prime exponent and intersects the real places; join takes the maximum exponent and unions the real places.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
namespace RayClassModulus

Lean source · statement

instance {K : Type u} [Field K] [NumberField K] :
    Lattice (RayClassModulus K)

theorem

finitePart_inf

L112 ↗

ClassFieldTheory.RayClassModulus.finitePart_inf

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
namespace RayClassModulus

Lean source · statement

theorem finitePart_inf
    {K : Type u} [Field K] [NumberField K]
    (m n : RayClassModulus K) :
    (m ⊓ n).finitePart = m.finitePart ⊓ n.finitePart

theorem

mem_infinitePart_inf

L117 ↗

ClassFieldTheory.RayClassModulus.mem_infinitePart_inf

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
namespace RayClassModulus

Lean source · statement

theorem mem_infinitePart_inf
    {K : Type u} [Field K] [NumberField K]
    (m n : RayClassModulus K) (v : RayClassRealPlace K) :
    v ∈ (m ⊓ n).infinitePart ↔
      v ∈ m.infinitePart ∧ v ∈ n.infinitePart

theorem

finitePart_sup

L126 ↗

ClassFieldTheory.RayClassModulus.finitePart_sup

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
namespace RayClassModulus

Lean source · statement

theorem finitePart_sup
    {K : Type u} [Field K] [NumberField K]
    (m n : RayClassModulus K) :
    (m ⊔ n).finitePart = m.finitePart ⊔ n.finitePart

theorem

mem_infinitePart_sup

L131 ↗

ClassFieldTheory.RayClassModulus.mem_infinitePart_sup

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
namespace RayClassModulus

Lean source · statement

theorem mem_infinitePart_sup
    {K : Type u} [Field K] [NumberField K]
    (m n : RayClassModulus K) (v : RayClassRealPlace K) :
    v ∈ (m ⊔ n).infinitePart ↔
      v ∈ m.infinitePart ∨ v ∈ n.infinitePart

Module documentation

Ray class moduli

Declarations