IdealNorm.lean

theorem exists_localHigherUnitGroup_le_norm_preimage
    (m : Modulus K)
    (W : HeightOneSpectrum (𝓞 L)) :
    let v := _root_.finitePlaceBelow (K := K) W
    letI : Algebra (v.adicCompletion K) (W.adicCompletion L) :=
      (_root_.finitePlaceAdicCompletionMap K L v ⟨W, rfl⟩).toAlgebra
    ∃ n : ℕ,
      localHigherUnitGroup W n ≤
        (localHigherUnitGroup v (m.finitePart v)).comap
          (LocalFieldTheory.normUnits
            (v.adicCompletion K) (W.adicCompletion L)) := by
  classical
  let v := _root_.finitePlaceBelow (K := K) W
  let : Algebra (v.adicCompletion K) (W.adicCompletion L) :=
    (_root_.finitePlaceAdicCompletionMap K L v ⟨W, rfl⟩).toAlgebra
  let : IsScalarTower
      K (v.adicCompletion K) (W.adicCompletion L) :=
    _root_.finitePlaceAdicCompletionMap_isScalarTower K L v ⟨W, rfl⟩
  let : ContinuousSMul
      (v.adicCompletion K) (W.adicCompletion L) :=
    continuousSMul_of_algebraMap _ _ (by
      change Continuous
        (_root_.finitePlaceAdicCompletionMap K L v ⟨W, rfl⟩)
      exact
        _root_.finitePlaceAdicCompletionMap_continuous
          K L v ⟨W, rfl⟩)
  let : FiniteDimensional
      (v.adicCompletion K) (W.adicCompletion L) :=
    inferInstance
  let : NontriviallyNormedField (v.adicCompletion K) :=
    NontriviallyNormedField.ofNormNeOne (by
      obtain ⟨ϖ, hϖ⟩ :=
        IsDiscreteValuationRing.exists_irreducible
          (v.adicCompletionIntegers K)
      refine ⟨(ϖ : v.adicCompletion K), ?_, ?_⟩
      · intro h
        exact hϖ.ne_zero (Subtype.ext h)
      · exact ne_of_lt (local_irreducible_norm_lt_one v hϖ))
  let U : Set (W.adicCompletion L)ˣ :=
    (LocalFieldTheory.normUnits
      (v.adicCompletion K) (W.adicCompletion L)) ⁻¹'
        (localHigherUnitGroup v (m.finitePart v) :
          Set (v.adicCompletion K)ˣ)
  have hTarget :
      (localHigherUnitGroup v (m.finitePart v) :
          Set (v.adicCompletion K)ˣ) ∈
        𝓝 (1 : (v.adicCompletion K)ˣ) :=
    (isOpen_localHigherUnitGroup v (m.finitePart v)).mem_nhds
      (localHigherUnitGroup v (m.finitePart v)).one_mem
  have hU : U ∈ 𝓝 (1 : (W.adicCompletion L)ˣ) := by
    have hcont :=
      LocalFieldTheory.normUnits_continuous_of_finiteDimensional
        (v.adicCompletion K) (W.adicCompletion L)
    have hTarget' :
        (localHigherUnitGroup v (m.finitePart v) :
          Set (v.adicCompletion K)ˣ) ∈
          𝓝 (LocalFieldTheory.normUnits
            (v.adicCompletion K) (W.adicCompletion L) 1) := by
      simpa using hTarget
    simpa [U] using hcont.continuousAt hTarget'
  obtain ⟨n, hn⟩ :=
    exists_localHigherUnitGroup_subset W hU
  refine ⟨n, ?_⟩
  intro x hx
  exact hn hx

def idealNormLiftedModulusExponent
    (m : Modulus K)
    (W : HeightOneSpectrum (𝓞 L)) : ℕ

theorem idealNormLiftedModulusExponent_pos
    (m : Modulus K)
    (W : HeightOneSpectrum (𝓞 L))
    (hW :
      _root_.finitePlaceBelow (K := K) W ∈ m.finitePart.support) :
    0 < idealNormLiftedModulusExponent
      (K := K) (L := L) m W

theorem localHigherUnitGroup_idealNormLiftedModulusExponent_le
    (m : Modulus K)
    (W : HeightOneSpectrum (𝓞 L))
    (hW :
      _root_.finitePlaceBelow (K := K) W ∈ m.finitePart.support) :
    let v := _root_.finitePlaceBelow (K := K) W
    letI : Algebra (v.adicCompletion K) (W.adicCompletion L) :=
      (_root_.finitePlaceAdicCompletionMap K L v ⟨W, rfl⟩).toAlgebra
    localHigherUnitGroup W
        (idealNormLiftedModulusExponent
          (K := K) (L := L) m W) ≤
      (localHigherUnitGroup v (m.finitePart v)).comap
        (LocalFieldTheory.normUnits
          (v.adicCompletion K) (W.adicCompletion L)) := by
  classical
  let v := _root_.finitePlaceBelow (K := K) W
  let : Algebra (v.adicCompletion K) (W.adicCompletion L) :=
    (_root_.finitePlaceAdicCompletionMap K L v ⟨W, rfl⟩).toAlgebra
  rw [idealNormLiftedModulusExponent, dite_eq_left hW]
  exact
    (localHigherUnitGroup_antitone W (Nat.le_succ _)).trans
      (Nat.find_spec
        (exists_localHigherUnitGroup_le_norm_preimage
          (K := K) (L := L) m W))

theorem idealNormLiftedModulusExponent_min
    (m : Modulus K)
    (W : HeightOneSpectrum (𝓞 L))
    (hW :
      _root_.finitePlaceBelow (K := K) W ∈ m.finitePart.support)
    (r : ℕ)
    (hr :
      let v := _root_.finitePlaceBelow (K := K) W
      letI : Algebra (v.adicCompletion K) (W.adicCompletion L) :=
        (_root_.finitePlaceAdicCompletionMap K L v ⟨W, rfl⟩).toAlgebra
      localHigherUnitGroup W r ≤
        (localHigherUnitGroup v (m.finitePart v)).comap
          (LocalFieldTheory.normUnits
            (v.adicCompletion K) (W.adicCompletion L))) :
    idealNormLiftedModulusExponent (K := K) (L := L) m W ≤ r + 1 := by
  classical
  let v := _root_.finitePlaceBelow (K := K) W
  let : Algebra (v.adicCompletion K) (W.adicCompletion L) :=
    (_root_.finitePlaceAdicCompletionMap K L v ⟨W, rfl⟩).toAlgebra
  rw [idealNormLiftedModulusExponent, dite_eq_left hW]
  exact Nat.add_le_add_right
    (Nat.find_min'
      (exists_localHigherUnitGroup_le_norm_preimage
        (K := K) (L := L) m W) hr) 1

theorem idealNormLiftedModulusExponent_eq_zero_of_not_mem
    (m : Modulus K)
    (W : HeightOneSpectrum (𝓞 L))
    (hW :
      _root_.finitePlaceBelow (K := K) W ∉ m.finitePart.support) :
    idealNormLiftedModulusExponent (K := K) (L := L) m W = 0

def idealNormLiftedSupport (m : Modulus K) :
    Set (HeightOneSpectrum (𝓞 L))

theorem idealNormLiftedSupport_finite (m : Modulus K) :
    (idealNormLiftedSupport (K := K) (L := L) m).Finite

def idealNormLiftedModulus
    (m : Modulus K) : Modulus L

theorem idealNormLiftedModulus_apply
    (m : Modulus K)
    (W : HeightOneSpectrum (𝓞 L)) :
    (idealNormLiftedModulus (K := K) (L := L) m).finitePart W =
      idealNormLiftedModulusExponent
        (K := K) (L := L) m W

theorem mem_idealNormLiftedModulus_support_iff
    (m : Modulus K)
    (W : HeightOneSpectrum (𝓞 L)) :
    W ∈ (idealNormLiftedModulus
        (K := K) (L := L) m).finitePart.support ↔
      _root_.finitePlaceBelow (K := K) W ∈ m.finitePart.support

def idealNormExponentMap :
    (HeightOneSpectrum (𝓞 L) →₀ ℤ) →+
      (HeightOneSpectrum (𝓞 K) →₀ ℤ)

theorem idealNormExponentMap_apply
    (e : HeightOneSpectrum (𝓞 L) →₀ ℤ)
    (v : HeightOneSpectrum (𝓞 K)) :
    idealNormExponentMap (K := K) (L := L) e v =
      e.sum fun W n =>
        if _root_.finitePlaceBelow (K := K) W = v then
          (W.asIdeal.inertiaDeg (𝓞 K) : ℤ) * n
        else
          0 := by
  classical
  simp [idealNormExponentMap, Finsupp.single_apply, eq_comm]

theorem idealNormExponentMap_apply_eq_sum_above
    (e : HeightOneSpectrum (𝓞 L) →₀ ℤ)
    (v : HeightOneSpectrum (𝓞 K))
    [Fintype {W : HeightOneSpectrum (𝓞 L) //
      _root_.finitePlaceBelow (K := K) W = v}] :
    idealNormExponentMap (K := K) (L := L) e v =
      ∑ W : {W : HeightOneSpectrum (𝓞 L) //
          _root_.finitePlaceBelow (K := K) W = v},
        (W.1.asIdeal.inertiaDeg (𝓞 K) : ℤ) * e W.1

theorem factorizationEquiv_symm_toAdd
    (I : FractionalIdealGroup L) :
    ((FractionalIdealGroup.factorizationEquiv
      (K := L)).symm I).toAdd =
        FractionalIdealGroup.countVector I

def fractionalIdealNorm :
    FractionalIdealGroup L →* FractionalIdealGroup K

theorem count_fractionalIdealNorm
    (I : FractionalIdealGroup L)
    (v : HeightOneSpectrum (𝓞 K)) :
    FractionalIdeal.count K v
        (fractionalIdealNorm (K := K) (L := L) I :
          FractionalIdeal (nonZeroDivisors (𝓞 K)) K) =
      idealNormExponentMap (K := K) (L := L)
        (FractionalIdealGroup.countVector I) v

theorem fractionalIdealNormPrimeBelow_eq_finitePlaceBelow
    (W : HeightOneSpectrum (𝓞 L)) :
    ClassFieldTheory.fractionalIdealNormPrimeBelow K L W =
      _root_.finitePlaceBelow (K := K) W

theorem idealNormExponentMap_eq_public :
    idealNormExponentMap (K := K) (L := L) =
      ClassFieldTheory.fractionalIdealNormExponentMap K L

theorem factorizationEquiv_eq_public
    (F : Type) [Field F] [NumberField F] :
    FractionalIdealGroup.factorizationEquiv (K := F) =
      ClassFieldTheory.NumberFieldFractionalIdealGroup.factorizationEquiv
        (K := F)

theorem fractionalIdealNorm_eq_public :
    fractionalIdealNorm (K := K) (L := L) =
      ClassFieldTheory.fractionalIdealNorm K L

theorem _root_.IdeleGroup.count_fractionalIdeal
    (a : IdeleGroup K)
    (v : HeightOneSpectrum (𝓞 K)) :
    FractionalIdeal.count K v
        (IdeleGroup.fractionalIdeal a :
          FractionalIdeal (nonZeroDivisors (𝓞 K)) K) =
      (FiniteIdeleGroup.localOrder v
        (IdeleGroup.finiteComponent v a)).toAdd

theorem _root_.IdeleGroup.fractionalIdeal_ideleNorm
    (a : IdeleGroup L) :
    IdeleGroup.fractionalIdeal (IdeleGroup.norm K L a) =
      fractionalIdealNorm (K := K) (L := L)
        (IdeleGroup.fractionalIdeal a)

theorem fractionalIdealNorm_mem_primeToModulusIdeals
    (m : Modulus K)
    (I : primeToModulusIdeals
      (idealNormLiftedModulus (K := K) (L := L) m)) :
    fractionalIdealNorm (K := K) (L := L)
        (I : FractionalIdealGroup L) ∈
      primeToModulusIdeals m

def primeToModulusIdealNorm
    (m : Modulus K) :
    primeToModulusIdeals
        (idealNormLiftedModulus (K := K) (L := L) m) →*
      primeToModulusIdeals m where
  toFun I :=
    ⟨fractionalIdealNorm (K := K) (L := L)
        (I : FractionalIdealGroup L),
      fractionalIdealNorm_mem_primeToModulusIdeals
        (K := K) (L := L) m I⟩
  map_one' := by
    apply Subtype.ext
    exact map_one _
  map_mul' I J := by
    apply Subtype.ext
    exact map_mul _ _ _

theorem primeToModulusIdealNorm_coe
    (m : Modulus K)
    (I : primeToModulusIdeals
      (idealNormLiftedModulus (K := K) (L := L) m)) :
    (primeToModulusIdealNorm
        (K := K) (L := L) m I :
      FractionalIdealGroup K) =
        fractionalIdealNorm (K := K) (L := L)
          (I : FractionalIdealGroup L)

theorem finite_norm_mem_finitePrimeToModulusSubgroup
    (m : Modulus K)
    (a : idelePrimeToModulusSubgroup
      (idealNormLiftedModulus (K := K) (L := L) m)) :
    (IdeleGroup.norm K L (a : IdeleGroup L)).2 ∈
      finitePrimeToModulusSubgroup m

def idealNormSubgroup
    (m : Modulus K) :
    Subgroup (primeToModulusIdeals m)