Documentation

MazurTorsion.NumberTheory.CyclotomicOrbitCoprimeNormalization

Galois-orbit coprime normalization of cyclotomic pseudo-units #

This file strengthens the denominator-avoidance part of pseudo-unit normalization. Given a nonzero integral denominator ideal, we apply the existing normalization theorem to the product of all of its cyclotomic Galois conjugates. The resulting numerator is therefore outside every Galois conjugate of every finite prime dividing the denominator.

This is an ideal-theoretic normalization statement. It does not use or assert any reciprocity law.

source
noncomputable def NumberTheory.CyclotomicCharacter.InverseExtension.galoisOrbitIdealProduct {p : ℕ} (I : Ideal (NumberField.RingOfIntegers (PrimeCyclotomicField p))) :
Ideal (NumberField.RingOfIntegers (PrimeCyclotomicField p))

The product of all cyclotomic Galois conjugates of an integral ideal.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem NumberTheory.CyclotomicCharacter.InverseExtension.galoisOrbitIdealProduct_ne_bot {p : ℕ} (I : Ideal (NumberField.RingOfIntegers (PrimeCyclotomicField p))) (hI : I ≠ ⊥) :
    galoisOrbitIdealProduct I ≠ ⊥

    The Galois-orbit product of a nonzero ideal is nonzero.

    source
    theorem NumberTheory.CyclotomicCharacter.InverseExtension.not_mem_mapFinitePrime_of_coprime_galoisOrbitIdealProduct {p : ℕ} (I : Ideal (NumberField.RingOfIntegers (PrimeCyclotomicField p))) (eta : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (hcoprime : IsCoprime (Ideal.span {eta}) (galoisOrbitIdealProduct I)) (sigma : Gal(PrimeCyclotomicField p/ℚ)) (v : FinitePrime (PrimeCyclotomicField p)) (hvI : v.asIdeal ∣ I) :
    eta ∉ ((mapFinitePrime sigma) v).asIdeal

    Coprimality with the full orbit product keeps an element outside every conjugate of every finite prime dividing the original ideal.

    source
    theorem NumberTheory.CyclotomicCharacter.InverseExtension.exists_galoisOrbit_coprime_integral_pseudoUnit_normalization {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (E : InverseExtension p L) (hdiv : ∀ (v : FinitePrime (PrimeCyclotomicField p)), ↑p ∣ FractionalIdeal.count (PrimeCyclotomicField p) v (FractionalIdeal.spanSingleton (nonZeroDivisors (NumberField.RingOfIntegers (PrimeCyclotomicField p))) E.kummerPresentation.radicand)) (I : Ideal (NumberField.RingOfIntegers (PrimeCyclotomicField p))) (hI : I ≠ ⊥) :
    ∃ (c : (PrimeCyclotomicField p)ˣ) (eta : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (B : Ideal (NumberField.RingOfIntegers (PrimeCyclotomicField p))), eta ≠ 0 ∧ (algebraMap (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) eta = E.kummerPresentation.radicand * ↑c ^ p ∧ Ideal.span {eta} = B ^ p ∧ IsCoprime (Ideal.span {eta}) (galoisOrbitIdealProduct I) ∧ IsCoprime (Ideal.span {eta}) (cyclotomicPrime p).asIdeal ∧ ∀ (sigma : Gal(PrimeCyclotomicField p/ℚ)) (v : FinitePrime (PrimeCyclotomicField p)), v.asIdeal ∣ I → eta ∉ ((mapFinitePrime sigma) v).asIdeal

    A pseudo-unit radicand can be normalized so that its integral numerator is coprime to the full Galois-orbit product of a prescribed nonzero denominator ideal. In particular, the numerator lies outside every conjugate of every finite prime dividing that denominator.