Documentation

TauCeti.NumberTheory.NumberField.Global.RayClass.Lattice

Greatest common divisors and least common multiples of moduli #

The divisibility order on number-field moduli is componentwise: the finite ideal divides in the usual ideal-theoretic sense, while the set of real places grows by inclusion. This file constructs the greatest common divisor and least common multiple for that order. On finite parts these are the sum and intersection of ideals, respectively; on infinite parts they are intersection and union.

The least common multiple combines congruence conditions: an element of the field is congruent to one modulo lcm 𝔪 𝔫 exactly when it is congruent to one modulo both 𝔪 and 𝔫. This is the form used when several ray conditions are replaced by one modulus. The support and exponent formulas record that finite prime exponents combine by min for gcd and by max for lcm.

Main definitions #

Main results #

References #

Definitions and universal properties #

source
noncomputable def TauCeti.GlobalNumberFields.Modulus.gcd {K : Type u_1} [Field K] [NumberField K] (m n : Modulus K) :
Modulus K

The greatest common divisor of two moduli. Its finite part is the sum of the two finite ideals and its infinite part contains the real places common to both moduli.

Instances For
    source
    noncomputable def TauCeti.GlobalNumberFields.Modulus.lcm {K : Type u_1} [Field K] [NumberField K] (m n : Modulus K) :
    Modulus K

    The least common multiple of two moduli. Its finite part is the intersection of the two finite ideals and its infinite part contains every real place occurring in either modulus.

    Instances For
      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.Modulus.gcd_finitePart {K : Type u_1} [Field K] [NumberField K] (m n : Modulus K) :
      (m.gcd n).finitePart = m.finitePart ⊔ n.finitePart
      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.Modulus.gcd_infinitePart {K : Type u_1} [Field K] [NumberField K] (m n : Modulus K) :
      (m.gcd n).infinitePart = m.infinitePart ∩ n.infinitePart
      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.Modulus.lcm_finitePart {K : Type u_1} [Field K] [NumberField K] (m n : Modulus K) :
      (m.lcm n).finitePart = m.finitePart ⊓ n.finitePart
      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.Modulus.lcm_infinitePart {K : Type u_1} [Field K] [NumberField K] (m n : Modulus K) :
      (m.lcm n).infinitePart = m.infinitePart ∪ n.infinitePart
      source
      theorem TauCeti.GlobalNumberFields.Modulus.gcd_dvd_left {K : Type u_1} [Field K] [NumberField K] (m n : Modulus K) :
      m.gcd n ∣ m

      The greatest common divisor divides its left argument.

      source
      theorem TauCeti.GlobalNumberFields.Modulus.gcd_dvd_right {K : Type u_1} [Field K] [NumberField K] (m n : Modulus K) :
      m.gcd n ∣ n

      The greatest common divisor divides its right argument.

      source
      theorem TauCeti.GlobalNumberFields.Modulus.dvd_gcd {K : Type u_1} [Field K] [NumberField K] {m n p : Modulus K} (hm : p ∣ m) (hn : p ∣ n) :
      p ∣ m.gcd n

      A modulus dividing both arguments divides their greatest common divisor.

      source
      theorem TauCeti.GlobalNumberFields.Modulus.dvd_gcd_iff {K : Type u_1} [Field K] [NumberField K] {m n p : Modulus K} :
      p ∣ m.gcd n ↔ p ∣ m ∧ p ∣ n

      A modulus divides a greatest common divisor exactly when it divides both arguments.

      source
      theorem TauCeti.GlobalNumberFields.Modulus.dvd_lcm_left {K : Type u_1} [Field K] [NumberField K] (m n : Modulus K) :
      m ∣ m.lcm n

      The least common multiple is divisible by its left argument.

      source
      theorem TauCeti.GlobalNumberFields.Modulus.dvd_lcm_right {K : Type u_1} [Field K] [NumberField K] (m n : Modulus K) :
      n ∣ m.lcm n

      The least common multiple is divisible by its right argument.

      source
      theorem TauCeti.GlobalNumberFields.Modulus.lcm_dvd {K : Type u_1} [Field K] [NumberField K] {m n p : Modulus K} (hm : m ∣ p) (hn : n ∣ p) :
      m.lcm n ∣ p

      The least common multiple divides every common multiple.

      source
      theorem TauCeti.GlobalNumberFields.Modulus.lcm_dvd_iff {K : Type u_1} [Field K] [NumberField K] {m n p : Modulus K} :
      m.lcm n ∣ p ↔ m ∣ p ∧ n ∣ p

      A least common multiple divides a modulus exactly when both arguments divide it.

      source
      theorem TauCeti.GlobalNumberFields.Modulus.gcd_comm {K : Type u_1} [Field K] [NumberField K] (m n : Modulus K) :
      m.gcd n = n.gcd m

      Greatest common divisors of moduli are commutative.

      source
      theorem TauCeti.GlobalNumberFields.Modulus.gcd_assoc {K : Type u_1} [Field K] [NumberField K] (m n p : Modulus K) :
      (m.gcd n).gcd p = m.gcd (n.gcd p)

      Greatest common divisors of moduli are associative.

      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.Modulus.gcd_self {K : Type u_1} [Field K] [NumberField K] (m : Modulus K) :
      m.gcd m = m

      A modulus is its own greatest common divisor.

      source
      theorem TauCeti.GlobalNumberFields.Modulus.lcm_comm {K : Type u_1} [Field K] [NumberField K] (m n : Modulus K) :
      m.lcm n = n.lcm m

      Least common multiples of moduli are commutative.

      source
      theorem TauCeti.GlobalNumberFields.Modulus.lcm_assoc {K : Type u_1} [Field K] [NumberField K] (m n p : Modulus K) :
      (m.lcm n).lcm p = m.lcm (n.lcm p)

      Least common multiples of moduli are associative.

      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.Modulus.lcm_self {K : Type u_1} [Field K] [NumberField K] (m : Modulus K) :
      m.lcm m = m

      A modulus is its own least common multiple.

      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.Modulus.gcd_one {K : Type u_1} [Field K] [NumberField K] (m : Modulus K) :
      m.gcd (one K) = one K

      The greatest common divisor with the trivial modulus is trivial.

      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.Modulus.one_gcd {K : Type u_1} [Field K] [NumberField K] (m : Modulus K) :
      (one K).gcd m = one K

      The greatest common divisor of the trivial modulus and any modulus is trivial.

      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.Modulus.lcm_one {K : Type u_1} [Field K] [NumberField K] (m : Modulus K) :
      m.lcm (one K) = m

      The least common multiple with the trivial modulus is the original modulus.

      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.Modulus.one_lcm {K : Type u_1} [Field K] [NumberField K] (m : Modulus K) :
      (one K).lcm m = m

      The least common multiple of the trivial modulus and any modulus is the original modulus.

      Primewise formulas #

      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.Modulus.support_gcd {K : Type u_1} [Field K] [NumberField K] (m n : Modulus K) :
      (m.gcd n).support = m.support ∩ n.support

      The finite support of a greatest common divisor is the intersection of the supports.

      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.Modulus.support_lcm {K : Type u_1} [Field K] [NumberField K] (m n : Modulus K) :
      (m.lcm n).support = m.support ∪ n.support

      The finite support of a least common multiple is the union of the supports.

      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.Modulus.exponent_gcd {K : Type u_1} [Field K] [NumberField K] (m n : Modulus K) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :
      (m.gcd n).exponent v = min (m.exponent v) (n.exponent v)

      At every finite place, the exponent in a greatest common divisor is the minimum of the two exponents.

      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.Modulus.exponent_lcm {K : Type u_1} [Field K] [NumberField K] (m n : Modulus K) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :
      (m.lcm n).exponent v = max (m.exponent v) (n.exponent v)

      At every finite place, the exponent in a least common multiple is the maximum of the two exponents.

      Combining congruence conditions #

      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.Modulus.isCongrOne_lcm_iff {K : Type u_1} [Field K] [NumberField K] {m n : Modulus K} {x : Kˣ} :
      IsCongrOne (m.lcm n) x ↔ IsCongrOne m x ∧ IsCongrOne n x

      Congruence to one modulo a least common multiple is equivalent to congruence modulo both arguments.

      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.congruenceSubgroup_lcm {K : Type u_1} [Field K] [NumberField K] (m n : Modulus K) :
      congruenceSubgroup (m.lcm n) = congruenceSubgroup m ⊓ congruenceSubgroup n

      The congruence subgroup of a least common multiple is the intersection of the two congruence subgroups.