PrincipalNorm.lean

theorem archimedeanNorm_principalIdele (x : Kˣ) :
    ((archimedeanNorm
        (IdeleGroup.principalIdele K x).1 : ℝ≥0ˣ) : ℝ≥0) =
      ⟨|(Algebra.norm ℚ) (x : K)|, abs_nonneg _⟩

def absoluteNorm :
    FractionalIdealGroup K →* ℝ≥0ˣ where
  toFun I :=
    Units.mk0
      ⟨(FractionalIdeal.absNorm
          (I : FractionalIdeal (nonZeroDivisors (𝓞 K)) K) : ℝ),
        Rat.cast_nonneg.mpr
          (FractionalIdeal.absNorm_nonneg
            (I : FractionalIdeal (nonZeroDivisors (𝓞 K)) K))⟩
      (by
        intro h
        have hr := congrArg (fun z : ℝ≥0 => z.1) h
        change
          ((FractionalIdeal.absNorm
            (I : FractionalIdeal
              (nonZeroDivisors (𝓞 K)) K) : ℚ) : ℝ) = 0 at hr
        have hq : FractionalIdeal.absNorm
            (I : FractionalIdeal
              (nonZeroDivisors (𝓞 K)) K) = 0 := by
          exact_mod_cast hr
        exact Units.ne_zero I
          (FractionalIdeal.absNorm_eq_zero_iff.mp hq))
  map_one' := by
    apply Units.ext
    apply NNReal.eq
    change
      ((FractionalIdeal.absNorm
        (1 : FractionalIdeal
          (nonZeroDivisors (𝓞 K)) K) : ℚ) : ℝ) = 1
    rw [FractionalIdeal.absNorm_one]
    norm_num
  map_mul' I J := by
    apply Units.ext
    change
      (⟨(FractionalIdeal.absNorm
          ((I * J : FractionalIdealGroup K) :
            FractionalIdeal (nonZeroDivisors (𝓞 K)) K) : ℝ),
        Rat.cast_nonneg.mpr
          (FractionalIdeal.absNorm_nonneg
            ((I * J : FractionalIdealGroup K) :
              FractionalIdeal (nonZeroDivisors (𝓞 K)) K))⟩ : ℝ≥0) =
      ⟨(FractionalIdeal.absNorm
          (I : FractionalIdeal
            (nonZeroDivisors (𝓞 K)) K) : ℝ),
        Rat.cast_nonneg.mpr
          (FractionalIdeal.absNorm_nonneg
            (I : FractionalIdeal
              (nonZeroDivisors (𝓞 K)) K))⟩ *
      ⟨(FractionalIdeal.absNorm
          (J : FractionalIdeal
            (nonZeroDivisors (𝓞 K)) K) : ℝ),
        Rat.cast_nonneg.mpr
          (FractionalIdeal.absNorm_nonneg
            (J : FractionalIdeal
              (nonZeroDivisors (𝓞 K)) K))⟩
    apply NNReal.eq
    change
      ((FractionalIdeal.absNorm
        ((I * J : FractionalIdealGroup K) :
          FractionalIdeal (nonZeroDivisors (𝓞 K)) K) : ℚ) : ℝ) =
      ((FractionalIdeal.absNorm
        (I : FractionalIdeal
          (nonZeroDivisors (𝓞 K)) K) : ℚ) : ℝ) *
      ((FractionalIdeal.absNorm
        (J : FractionalIdeal
          (nonZeroDivisors (𝓞 K)) K) : ℚ) : ℝ)
    norm_cast
    simpa only [Units.val_mul] using
      (map_mul FractionalIdeal.absNorm
        (I : FractionalIdeal (nonZeroDivisors (𝓞 K)) K)
        (J : FractionalIdeal (nonZeroDivisors (𝓞 K)) K))

theorem absoluteNorm_prime (v : HeightOneSpectrum (𝓞 K)) :
    absoluteNorm (prime v) = FiniteIdeleGroup.primeNorm v

theorem absoluteNorm_factorization
    (e : Multiplicative
      (HeightOneSpectrum (𝓞 K) →₀ ℤ)) :
    absoluteNorm (factorization e) =
      FiniteIdeleGroup.divisorNorm e

theorem absoluteNorm_toPrincipalIdeal (x : Kˣ) :
    ((absoluteNorm
      (toPrincipalIdeal (𝓞 K) K x) : ℝ≥0ˣ) : ℝ≥0) =
      ⟨|((Algebra.norm ℚ) (x : K) : ℝ)|, abs_nonneg _⟩

theorem absoluteNorm_eq_fractionalIdealAbsoluteNorm
    (a : FiniteIdeleGroup K) :
    absoluteNorm a =
      FractionalIdealGroup.absoluteNorm (fractionalIdeal a)

theorem absoluteNorm_principalIdele (x : Kˣ) :
    ((absoluteNorm
      (IdeleGroup.principalIdele K x).2 : ℝ≥0ˣ) : ℝ≥0) =
      ⟨|((Algebra.norm ℚ) (x : K) : ℝ)|, abs_nonneg _⟩

theorem finite_absoluteNorm_eq_archimedeanNorm_principalIdele
    (x : Kˣ) :
    FiniteIdeleGroup.absoluteNorm (principalIdele K x).2 =
      InfiniteIdeleGroup.archimedeanNorm
        (principalIdele K x).1

theorem absoluteNorm_principalIdele (x : Kˣ) :
    absoluteNorm (principalIdele K x) = 1

theorem principalSubgroup_le_normOneSubgroup :
    principalSubgroup K ≤ normOneSubgroup (K := K)

def absoluteNorm :
    IdeleClassGroup K →* ℝ≥0ˣ

theorem absoluteNorm_mk (a : IdeleGroup K) :
    absoluteNorm
      (QuotientGroup.mk' (IdeleGroup.principalSubgroup K) a) =
        IdeleGroup.absoluteNorm a

def normOneSubgroup : Subgroup (IdeleClassGroup K)

theorem comap_normOneSubgroup :
    Subgroup.comap
      (QuotientGroup.mk' (IdeleGroup.principalSubgroup K))
      (normOneSubgroup (K := K)) =
        IdeleGroup.normOneSubgroup (K := K)

theorem mk_mem_normOneSubgroup_iff (a : IdeleGroup K) :
    QuotientGroup.mk' (IdeleGroup.principalSubgroup K) a ∈
        normOneSubgroup (K := K) ↔
      a ∈ IdeleGroup.normOneSubgroup (K := K)