AbelianLocalConductorComparison.lean

theorem finitePlaceFieldPrincipalUnits_map_eq_localHigherUnitGroup
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ) :
    let vK := HeightOneSpectrum.adicAbv K v
    let hvKna : IsNonarchimedean (vK : K → ℝ) :=
      HeightOneSpectrum.isNonarchimedean_adicAbv K v
    letI : Valued vK.Completion ℝ≥0 :=
      _root_.GlobalClassFieldTheory.Reciprocity.finitePlaceArtinCompletionValued
        vK hvKna
    letI : ValuativeRel vK.Completion :=
      _root_.GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionValuativeRel v
    (LocalFieldTheory.fieldPrincipalUnits vK.Completion n).map
        (_root_.finitePlaceCompletionUnitsContinuousMulEquiv v).toMonoidHom =
      RayClass.localHigherUnitGroup v n := by
  let vK := HeightOneSpectrum.adicAbv K v
  let hvKna : IsNonarchimedean (vK : K → ℝ) :=
    HeightOneSpectrum.isNonarchimedean_adicAbv K v
  let : Valued vK.Completion ℝ≥0 :=
    _root_.GlobalClassFieldTheory.Reciprocity.finitePlaceArtinCompletionValued
      vK hvKna
  let : ValuativeRel vK.Completion :=
    _root_.GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionValuativeRel v
  let eField : vK.Completion ≃+* v.adicCompletion K :=
    _root_.finitePlaceCompletionRingEquiv v
  let eIntegers :
      𝒪[vK.Completion] ≃+* v.adicCompletionIntegers K :=
    _root_.finitePlaceCompletionIntegerRingEquiv v
  let eIntegralUnits :
      𝒪[vK.Completion]ˣ ≃*
        (v.adicCompletionIntegers K).units :=
    (Units.mapEquiv eIntegers.toMulEquiv).trans
      (v.adicCompletionIntegers K).toSubmonoid.unitsEquivUnitsType.symm
  let e :
      vK.Completionˣ ≃ₜ* (v.adicCompletion K)ˣ :=
    _root_.finitePlaceCompletionUnitsContinuousMulEquiv v
  have heField (u : 𝒪[vK.Completion]ˣ) :
      (eIntegralUnits u : (v.adicCompletion K)ˣ) =
        e (LocalFieldTheory.IsNonarchimedeanLocalField.integerUnitsToFieldUnits
          vK.Completion u) := by
    apply Units.ext
    change
      eField ((u : 𝒪[vK.Completion]) : vK.Completion) =
        eField ((u : 𝒪[vK.Completion]) : vK.Completion)
    rfl
  have hePrincipal (u : 𝒪[vK.Completion]ˣ) :
      RayClass.localHigherUnitMap v n (eIntegralUnits u) = 1 ↔
        u ∈ LocalFieldTheory.principalUnits vK.Completion n := by
    rw [RayClass.localHigherUnitMap_eq_one_iff,
      LocalFieldTheory.mem_principalUnits_iff]
    have hvalue :
        RayClass.localIntegralValue v (eIntegralUnits u) =
          eIntegers (u : 𝒪[vK.Completion]) := by
      change
        ((v.adicCompletionIntegers K).toSubmonoid.unitsEquivUnitsType
            (eIntegralUnits u) :
          (v.adicCompletionIntegers K)ˣ).1 =
            eIntegers (u : 𝒪[vK.Completion])
      simp [eIntegralUnits]
    rw [hvalue, ← eIntegers.map_one, ← eIntegers.map_sub]
    exact
      ValuationTheory.ringEquiv_mem_maximalIdeal_pow_iff
        eIntegers n ((u : 𝒪[vK.Completion]) - 1)
  ext x
  constructor
  · rintro ⟨z, ⟨u, hu, rfl⟩, rfl⟩
    apply (RayClass.mem_localHigherUnitGroup_iff v n _).2
    exact ⟨eIntegralUnits u, heField u, (hePrincipal u).2 hu⟩
  · intro hx
    obtain ⟨y, hyx, hy⟩ :=
      (RayClass.mem_localHigherUnitGroup_iff v n x).1 hx
    let u : 𝒪[vK.Completion]ˣ := eIntegralUnits.symm y
    have huy : eIntegralUnits u = y :=
      eIntegralUnits.apply_symm_apply y
    refine
      ⟨LocalFieldTheory.IsNonarchimedeanLocalField.integerUnitsToFieldUnits
          vK.Completion u,
        ⟨u, ?_, rfl⟩, ?_⟩
    · apply (hePrincipal u).1
      simpa only [huy] using hy
    · calc
        e (LocalFieldTheory.IsNonarchimedeanLocalField.integerUnitsToFieldUnits
              vK.Completion u) =
            (eIntegralUnits u : (v.adicCompletion K)ˣ) :=
          (heField u).symm
        _ = y := congrArg Subtype.val huy
        _ = x := hyx

theorem finitePlaceCompletion_valuationMap_eq_zero_of_mem_localHigherUnitGroup
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ)
    (x : (v.adicCompletion K)ˣ)
    (hx : x ∈ RayClass.localHigherUnitGroup v n) :
    let vK := HeightOneSpectrum.adicAbv K v
    letI : ValuativeRel vK.Completion :=
      _root_.GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionValuativeRel v
    letI : IsNonarchimedeanLocalField vK.Completion :=
      Reciprocity.finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
    IsNonarchimedeanLocalField.valuationMap vK.Completion
        (Additive.ofMul
          ((_root_.finitePlaceCompletionUnitsContinuousMulEquiv v).symm x)) =
      0 := by
  let vK := HeightOneSpectrum.adicAbv K v
  let : ValuativeRel vK.Completion :=
    _root_.GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionValuativeRel v
  let : IsNonarchimedeanLocalField vK.Completion :=
    Reciprocity.finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
  have hxMap :
      x ∈
        (LocalFieldTheory.fieldPrincipalUnits vK.Completion n).map
          (_root_.finitePlaceCompletionUnitsContinuousMulEquiv v).toMonoidHom := by
    dsimp only [vK]
    rw [finitePlaceFieldPrincipalUnits_map_eq_localHigherUnitGroup v n]
    exact hx
  have hxPrincipal :
      (_root_.finitePlaceCompletionUnitsContinuousMulEquiv v).symm x ∈
        LocalFieldTheory.fieldPrincipalUnits vK.Completion n :=
    (Subgroup.mem_map_equiv
      (f := (_root_.finitePlaceCompletionUnitsContinuousMulEquiv v).toMulEquiv)).mp
        hxMap
  change
    (_root_.finitePlaceCompletionUnitsContinuousMulEquiv v).symm x ∈
      (LocalFieldTheory.principalUnits vK.Completion n).map
        (IsNonarchimedeanLocalField.integerUnitsToFieldUnits
          vK.Completion) at hxPrincipal
  rcases hxPrincipal with ⟨u, _hu, hu⟩
  rw [← hu]
  dsimp only
  rw [IsNonarchimedeanLocalField.valuationMap_apply]
  exact
    IsNonarchimedeanLocalField.v_integerUnitsToFieldUnits
      vK.Completion u

theorem
    localHigherUnits_le_chosenNormSubgroup_iff_fieldPrincipalUnits_le_normSubgroup
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ) :
    let vK := HeightOneSpectrum.adicAbv K v
    let hvK : vK.IsNontrivial :=
      RayClass.adicAbv_isNontrivial v
    let hvKna : IsNonarchimedean (vK : K → ℝ) :=
      HeightOneSpectrum.isNonarchimedean_adicAbv K v
    let w := _root_.chosenFinitePlaceExtension (L := L) v
    letI hK :=
      AbsoluteValue.extensionCompletionAlgebra
        (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI : Algebra vK.Completion w.1.Completion :=
      AbsoluteValue.completionAlgebra vK w.1 w.2
    letI :=
      LocalClassFieldTheory.localizedCompletionGlobalAlgebra vK w
    letI :=
      LocalClassFieldTheory.localizedCompletionIsScalarTower vK w
    let E := AlgebraicNumberTheory.Valuations.LocalizedCompletion vK w
    letI : FiniteDimensional vK.Completion E :=
      AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite vK hvK w
    letI : Valued vK.Completion ℝ≥0 :=
      _root_.finitePlaceCompletionValued vK hvKna
    letI : ValuativeRel vK.Completion :=
      _root_.finitePlaceCompletionValuativeRel vK hvKna
    RayClass.localHigherUnitGroup v n ≤
        _root_.chosenFinitePlaceLocalNormSubgroup
          (K := K) (L := L) v ↔
      LocalFieldTheory.fieldPrincipalUnits vK.Completion n ≤
        LocalFieldTheory.localNormSubgroup vK.Completion E := by
  let vK := HeightOneSpectrum.adicAbv K v
  let hvK : vK.IsNontrivial :=
    RayClass.adicAbv_isNontrivial v
  let hvKna : IsNonarchimedean (vK : K → ℝ) :=
    HeightOneSpectrum.isNonarchimedean_adicAbv K v
  let w := _root_.chosenFinitePlaceExtension (L := L) v
  let hK :=
    AbsoluteValue.extensionCompletionAlgebra
      (K := K) w.1
  let : SMul K w.1.Completion := hK.toSMul
  let : Algebra vK.Completion w.1.Completion :=
    AbsoluteValue.completionAlgebra vK w.1 w.2
  let :=
    LocalClassFieldTheory.localizedCompletionGlobalAlgebra vK w
  let :=
    LocalClassFieldTheory.localizedCompletionIsScalarTower vK w
  let E := AlgebraicNumberTheory.Valuations.LocalizedCompletion vK w
  let : FiniteDimensional vK.Completion E :=
    AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite vK hvK w
  let : Valued vK.Completion ℝ≥0 :=
    _root_.finitePlaceCompletionValued vK hvKna
  let : ValuativeRel vK.Completion :=
    _root_.finitePlaceCompletionValuativeRel vK hvKna
  let e :
      vK.Completionˣ ≃ₜ* (v.adicCompletion K)ˣ :=
    _root_.finitePlaceCompletionUnitsContinuousMulEquiv v
  have hprincipal :
      (LocalFieldTheory.fieldPrincipalUnits vK.Completion n).map
          e.toMonoidHom =
        RayClass.localHigherUnitGroup v n := by
    simpa [vK, hvKna, e] using
      (finitePlaceFieldPrincipalUnits_map_eq_localHigherUnitGroup
        (K := K) v n)
  rw [← hprincipal]
  change
    (LocalFieldTheory.fieldPrincipalUnits vK.Completion n).map
          e.toMonoidHom ≤
        (LocalFieldTheory.localNormSubgroup
          vK.Completion E).map e.toMonoidHom ↔
      LocalFieldTheory.fieldPrincipalUnits vK.Completion n ≤
        LocalFieldTheory.localNormSubgroup vK.Completion E
  constructor
  · intro h x hx
    have hex :
        e x ∈
          (LocalFieldTheory.localNormSubgroup
            vK.Completion E).map e.toMonoidHom :=
      h ⟨x, hx, rfl⟩
    obtain ⟨y, hy, hyx⟩ := hex
    exact (e.injective hyx) ▸ hy
  · rintro h _ ⟨x, hx, rfl⟩
    exact ⟨x, h hx, rfl⟩

def ideleClassNormChosenFinitePlaceLocalConductorExponent
    (v : HeightOneSpectrum (𝓞 K)) : ℕ

theorem ideleClassNormLocalHigherUnitExponent_eq_localConductorExponent
    (v : HeightOneSpectrum (𝓞 K)) :
    ideleClassNormLocalHigherUnitExponent
        (K := K) (L := L) v =
      ideleClassNormChosenFinitePlaceLocalConductorExponent
        (K := K) (L := L) v