NormalBasisInfiniteProduct.lean

theorem chosenBaseUniformizerPow_integerRingFieldSubmodule_exists_mem_maximalIdeal_pow
    (m : Nat) {x : L}
    (hx : x ∈ chosenBaseUniformizerPowSubmodule K L m
      (integerRingFieldSubmodule K L)) :
    ∃ a : 𝒪[L], a ∈ (𝓂[L] ^ m : Ideal 𝒪[L]) ∧ (a : L) = x

theorem chosenNormalBasisPrincipalUnitSet_mem_principalUnits_succ_of_lattice_bound
    {b n i : Nat}
    (hb : chosenBaseUniformizerPowSubmodule K L b
        (chosenNormalBasisIntegerLattice K L) ≤
      integerRingFieldSubmodule K L)
    (hbn : b + 1 ≤ n) {z : 𝒪[L]ˣ}
    (hz : z ∈ chosenNormalBasisPrincipalUnitSet K L (n + i)) :
    z ∈ principalUnits L (1 + i)

theorem tendsto_chosenNormalBasisPrincipalUnitSequence_one_of_lattice_bound
    [UniformSpace L] [IsUniformAddGroup L] [IsNonarchimedeanLocalField L]
    {b n : Nat}
    (hb : chosenBaseUniformizerPowSubmodule K L b
        (chosenNormalBasisIntegerLattice K L) ≤
      integerRingFieldSubmodule K L)
    (hbn : b + 1 ≤ n) (z : Nat → 𝒪[L]ˣ)
    (hz : ∀ i : Nat, z i ∈ chosenNormalBasisPrincipalUnitSet K L (n + i)) :
    Tendsto (fun i : Nat => ((z i : 𝒪[L]ˣ) : 𝒪[L])) atTop
      (nhds (1 : 𝒪[L])) := by
  have hsub : Tendsto
      (fun i : Nat => ((z i : 𝒪[L]ˣ) : 𝒪[L]) - 1) atTop
      (nhds (0 : 𝒪[L])) := by
    rw [tendsto_def]
    intro s hs
    rcases eventually_maximalIdeal_pow_subset_nhds_zero L s hs with ⟨N, hN⟩
    filter_upwards [eventually_ge_atTop N] with i hi
    apply hN (1 + i)
    · exact le_trans hi (Nat.le_add_left i 1)
    · exact (mem_principalUnits_iff L (z i) (1 + i)).1
        (chosenNormalBasisPrincipalUnitSet_mem_principalUnits_succ_of_lattice_bound
          (K := K) (L := L) hb hbn (hz i))
  simpa using hsub.const_add (1 : 𝒪[L])

theorem continuous_integerRingEquiv_of_isNonarchimedeanLocalField
    [UniformSpace L] [IsUniformAddGroup L] [IsNonarchimedeanLocalField L]
    (e : 𝒪[L] ≃+* 𝒪[L]) : Continuous e

theorem tendsto_galoisGroupIntegerUnits_tateNorm_of_tendsto
    [UniformSpace L] [IsUniformAddGroup L] [IsNonarchimedeanLocalField L]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (f : Nat → 𝒪[L]ˣ) (x : 𝒪[L]ˣ)
    (hf : Tendsto (fun d : Nat => ((f d : 𝒪[L]ˣ) : 𝒪[L])) atTop
      (nhds ((x : 𝒪[L]ˣ) : 𝒪[L]))) :
    letI := galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure K L
    Tendsto
      (fun d : Nat =>
        ((tateNorm (Gal(L / K)) 𝒪[L]ˣ (f d) : 𝒪[L]ˣ) : 𝒪[L]))
      atTop
      (nhds ((tateNorm (Gal(L / K)) 𝒪[L]ˣ x : 𝒪[L]ˣ) : 𝒪[L])) := by
  let := galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure K L
  have hσ (sigma : Gal(L / K)) : Tendsto
      (fun d : Nat => ((sigma • f d : 𝒪[L]ˣ) : 𝒪[L])) atTop
      (nhds ((sigma • x : 𝒪[L]ˣ) : 𝒪[L])) := by
    have he :=
      (continuous_integerRingEquiv_of_isNonarchimedeanLocalField L
        (galoisGroupIntegerRingEquivOfIsIntegralClosure K L sigma)).tendsto
          ((x : 𝒪[L]ˣ) : 𝒪[L]) |>.comp hf
    rw [show
      (⇑(galoisGroupIntegerRingEquivOfIsIntegralClosure K L sigma) ∘
          fun d : Nat => ((f d : 𝒪[L]ˣ) : 𝒪[L])) =
        (fun d : Nat =>
          (galoisGroupIntegerRingEquivOfIsIntegralClosure K L sigma)
            ((f d : 𝒪[L]ˣ) : 𝒪[L])) by
      funext d
      rfl] at he
    simpa [
      galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure_smul] using he
  have hprod := tendsto_finsetProd
    (Finset.univ : Finset (Gal(L / K))) (fun sigma _ => hσ sigma)
  convert hprod using 1 <;> simp [tateNorm]

theorem tendsto_galoisGroupIntegerUnits_sigmaMinusOne_of_tendsto
    [UniformSpace L] [IsUniformAddGroup L] [IsNonarchimedeanLocalField L]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (g : Gal(L/K)) (f : Nat → 𝒪[L]ˣ) (x : 𝒪[L]ˣ)
    (hf : Tendsto (fun d : Nat => ((f d : 𝒪[L]ˣ) : 𝒪[L])) atTop
      (nhds ((x : 𝒪[L]ˣ) : 𝒪[L]))) :
    letI := galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure K L
    Tendsto
      (fun d : Nat =>
        ((sigmaMinusOne (Gal(L / K)) 𝒪[L]ˣ g (f d) : 𝒪[L]ˣ) : 𝒪[L]))
      atTop
      (nhds ((sigmaMinusOne (Gal(L / K)) 𝒪[L]ˣ g x : 𝒪[L]ˣ) : 𝒪[L])) := by
  let := galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure K L
  have hgO : Tendsto
      (fun d : Nat => ((g • f d : 𝒪[L]ˣ) : 𝒪[L])) atTop
      (nhds ((g • x : 𝒪[L]ˣ) : 𝒪[L])) := by
    have he :=
      (continuous_integerRingEquiv_of_isNonarchimedeanLocalField L
        (galoisGroupIntegerRingEquivOfIsIntegralClosure K L g)).tendsto
          ((x : 𝒪[L]ˣ) : 𝒪[L]) |>.comp hf
    rw [show
      (⇑(galoisGroupIntegerRingEquivOfIsIntegralClosure K L g) ∘
          fun d : Nat => ((f d : 𝒪[L]ˣ) : 𝒪[L])) =
        (fun d : Nat =>
          (galoisGroupIntegerRingEquivOfIsIntegralClosure K L g)
            ((f d : 𝒪[L]ˣ) : 𝒪[L])) by
      funext d
      rfl] at he
    simpa [
      galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure_smul] using he
  have hfL : Tendsto
      (fun d : Nat => (((f d : 𝒪[L]ˣ) : 𝒪[L]) : L)) atTop
      (nhds (((x : 𝒪[L]ˣ) : 𝒪[L]) : L)) :=
    continuous_subtype_val.tendsto ((x : 𝒪[L]ˣ) : 𝒪[L]) |>.comp hf
  have hgL : Tendsto
      (fun d : Nat => (((g • f d : 𝒪[L]ˣ) : 𝒪[L]) : L)) atTop
      (nhds (((g • x : 𝒪[L]ˣ) : 𝒪[L]) : L)) :=
    continuous_subtype_val.tendsto ((g • x : 𝒪[L]ˣ) : 𝒪[L]) |>.comp hgO
  have hinv_coe (u : 𝒪[L]ˣ) :
      ((((u⁻¹ : 𝒪[L]ˣ) : 𝒪[L])) : L) =
        ((((u : 𝒪[L]ˣ) : 𝒪[L])) : L)⁻¹ := by
    apply eq_inv_of_mul_eq_one_right
    exact congrArg (fun y : 𝒪[L] => (y : L)) u.val_inv
  apply tendsto_subtype_rng.2
  have h := hgL.mul (hfL.inv₀ (by
    intro hx0
    apply Units.ne_zero x
    apply Subtype.ext
    exact hx0))
  convert h using 1 <;> simp [sigmaMinusOne, hinv_coe]

def chosenNormalBasisPrincipalUnitSequenceAsPrincipalUnits
    {b n : Nat}
    (hb : chosenBaseUniformizerPowSubmodule K L b
        (chosenNormalBasisIntegerLattice K L) ≤
      integerRingFieldSubmodule K L)
    (hbn : b + 1 ≤ n) (z : Nat → 𝒪[L]ˣ)
    (hz : ∀ i : Nat, z i ∈ chosenNormalBasisPrincipalUnitSet K L (n + i))
    (i : Nat) : principalUnits L (1 + i)

theorem chosenNormalBasisPrincipalUnitSequenceAsPrincipalUnits_val
    {b n : Nat}
    (hb : chosenBaseUniformizerPowSubmodule K L b
        (chosenNormalBasisIntegerLattice K L) ≤
      integerRingFieldSubmodule K L)
    (hbn : b + 1 ≤ n) (z : Nat → 𝒪[L]ˣ)
    (hz : ∀ i : Nat, z i ∈ chosenNormalBasisPrincipalUnitSet K L (n + i))
    (i : Nat) :
    (chosenNormalBasisPrincipalUnitSequenceAsPrincipalUnits K L hb hbn z hz i : 𝒪[L]ˣ) = z i

def chosenNormalBasisPrincipalUnitCorrectionProduct (z : Nat → 𝒪[L]ˣ) :
    Nat → 𝒪[L]ˣ
  | 0 => 1
  | d + 1 => chosenNormalBasisPrincipalUnitCorrectionProduct z d * z d

theorem chosenNormalBasisPrincipalUnitCorrectionProduct_zero (z : Nat → 𝒪[L]ˣ) :
    chosenNormalBasisPrincipalUnitCorrectionProduct (L := L) z 0 = 1

theorem chosenNormalBasisPrincipalUnitCorrectionProduct_succ
    (z : Nat → 𝒪[L]ˣ) (d : Nat) :
    chosenNormalBasisPrincipalUnitCorrectionProduct (L := L) z (d + 1) =
      chosenNormalBasisPrincipalUnitCorrectionProduct (L := L) z d * z d

theorem chosenNormalBasisPrincipalUnitCorrectionProduct_eq_principalUnitsCorrectionProduct
    {b n : Nat}
    (hb : chosenBaseUniformizerPowSubmodule K L b
        (chosenNormalBasisIntegerLattice K L) ≤
      integerRingFieldSubmodule K L)
    (hbn : b + 1 ≤ n) (z : Nat → 𝒪[L]ˣ)
    (hz : ∀ i : Nat, z i ∈ chosenNormalBasisPrincipalUnitSet K L (n + i))
    (d : Nat) :
    chosenNormalBasisPrincipalUnitCorrectionProduct (L := L) z d =
      principalUnitsCorrectionProduct L 1
        (chosenNormalBasisPrincipalUnitSequenceAsPrincipalUnits K L hb hbn z hz) d

theorem chosenNormalBasisPrincipalUnitCorrectionProduct_mem
    {n : Nat}
    (hmul : ∀ u : 𝒪[L]ˣ, u ∈ chosenNormalBasisPrincipalUnitSet K L n →
      ∀ v : 𝒪[L]ˣ, v ∈ chosenNormalBasisPrincipalUnitSet K L n →
        u * v ∈ chosenNormalBasisPrincipalUnitSet K L n)
    (z : Nat → 𝒪[L]ˣ)
    (hz : ∀ i : Nat, z i ∈ chosenNormalBasisPrincipalUnitSet K L (n + i))
    (d : Nat) :
    chosenNormalBasisPrincipalUnitCorrectionProduct (L := L) z d ∈
      chosenNormalBasisPrincipalUnitSet K L n

theorem chosenNormalBasisPrincipalUnitCorrectionProduct_div_mem
    {n : Nat}
    (hmul : ∀ k : Nat, n ≤ k →
      ∀ u : 𝒪[L]ˣ, u ∈ chosenNormalBasisPrincipalUnitSet K L k →
        ∀ v : 𝒪[L]ˣ, v ∈ chosenNormalBasisPrincipalUnitSet K L k →
          u * v ∈ chosenNormalBasisPrincipalUnitSet K L k)
    (z : Nat → 𝒪[L]ˣ)
    (hz : ∀ i : Nat, z i ∈ chosenNormalBasisPrincipalUnitSet K L (n + i))
    (m d : Nat) :
    chosenNormalBasisPrincipalUnitCorrectionProduct (L := L) z (m + d) /
        chosenNormalBasisPrincipalUnitCorrectionProduct (L := L) z m ∈
      chosenNormalBasisPrincipalUnitSet K L (n + m)

theorem exists_tendsto_chosenNormalBasisPrincipalUnitCorrectionProduct_principalUnit
    [UniformSpace L] [IsUniformAddGroup L] [IsNonarchimedeanLocalField L]
    {b n : Nat}
    (hb : chosenBaseUniformizerPowSubmodule K L b
        (chosenNormalBasisIntegerLattice K L) ≤
      integerRingFieldSubmodule K L)
    (hbn : b + 1 ≤ n) (z : Nat → 𝒪[L]ˣ)
    (hz : ∀ i : Nat, z i ∈ chosenNormalBasisPrincipalUnitSet K L (n + i)) :
    ∃ x : principalUnits L 1,
      Tendsto
        (fun d : Nat =>
          ((chosenNormalBasisPrincipalUnitCorrectionProduct (L := L) z d : 𝒪[L]ˣ) :
            𝒪[L]))
        atTop (nhds (((x : principalUnits L 1) : 𝒪[L]ˣ) : 𝒪[L])) := by
  let zU : ∀ i : Nat, principalUnits L (1 + i) :=
    chosenNormalBasisPrincipalUnitSequenceAsPrincipalUnits K L hb hbn z hz
  rcases exists_tendsto_principalUnitsCorrectionProduct_principalUnit
      L 1 (by rfl) zU with ⟨x, hx⟩
  refine ⟨x, hx.congr' (Eventually.of_forall ?_)⟩
  intro d
  exact congrArg (fun q : 𝒪[L]ˣ => (q : 𝒪[L]))
    (chosenNormalBasisPrincipalUnitCorrectionProduct_eq_principalUnitsCorrectionProduct
      (K := K) (L := L) hb hbn z hz d).symm

theorem chosenNormalBasisPrincipalUnitCorrectionProduct_limit_mem
    [UniformSpace L] [IsUniformAddGroup L] [IsNonarchimedeanLocalField L]
    {n : Nat}
    (hclosed : IsClosed
      ((chosenBaseUniformizerPowSubmodule K L n
        (chosenNormalBasisIntegerLattice K L) : Set L)))
    (hmul : ∀ u : 𝒪[L]ˣ, u ∈ chosenNormalBasisPrincipalUnitSet K L n →
      ∀ v : 𝒪[L]ˣ, v ∈ chosenNormalBasisPrincipalUnitSet K L n →
        u * v ∈ chosenNormalBasisPrincipalUnitSet K L n)
    (z : Nat → 𝒪[L]ˣ)
    (hz : ∀ i : Nat, z i ∈ chosenNormalBasisPrincipalUnitSet K L (n + i))
    (x : 𝒪[L]ˣ)
    (hx : Tendsto
      (fun d : Nat =>
        ((chosenNormalBasisPrincipalUnitCorrectionProduct (L := L) z d : 𝒪[L]ˣ) :
          𝒪[L]))
      atTop (nhds ((x : 𝒪[L]ˣ) : 𝒪[L]))) :
    x ∈ chosenNormalBasisPrincipalUnitSet K L n := by
  have hxL : Tendsto
      (fun d : Nat =>
        (((chosenNormalBasisPrincipalUnitCorrectionProduct (L := L) z d : 𝒪[L]ˣ) :
          𝒪[L]) : L))
      atTop (nhds ((((x : 𝒪[L]ˣ) : 𝒪[L])) : L)) :=
    (continuous_subtype_val.tendsto ((x : 𝒪[L]ˣ) : 𝒪[L])).comp hx
  have hsub : Tendsto
      (fun d : Nat =>
        (((((chosenNormalBasisPrincipalUnitCorrectionProduct (L := L) z d : 𝒪[L]ˣ) :
          𝒪[L]) - 1 : 𝒪[L]) : L)))
      atTop (nhds (((((x : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L))) := by
    simpa using hxL.sub (tendsto_const_nhds (x := (1 : L)))
  rw [mem_chosenNormalBasisPrincipalUnitSet_iff]
  exact submodule_mem_of_tendsto_of_forall_mem_of_closed
    (K := K) (L := L) hclosed hsub
    (fun d => chosenNormalBasisPrincipalUnitCorrectionProduct_mem
      (K := K) (L := L) hmul z hz d)

theorem exists_tendsto_chosenNormalBasisPrincipalUnitCorrectionProduct
    [UniformSpace L] [IsUniformAddGroup L] [IsNonarchimedeanLocalField L]
    [Module.Finite 𝒪[K] 𝒪[L]] :
    ∃ c : Nat, ∀ n : Nat, c ≤ n →
      ∀ z : Nat → 𝒪[L]ˣ,
        (∀ i : Nat, z i ∈ chosenNormalBasisPrincipalUnitSet K L (n + i)) →
          ∃ x : 𝒪[L]ˣ,
            Tendsto
                (fun d : Nat =>
                  ((chosenNormalBasisPrincipalUnitCorrectionProduct (L := L) z d :
                    𝒪[L]ˣ) : 𝒪[L]))
                atTop (nhds ((x : 𝒪[L]ˣ) : 𝒪[L])) ∧
              x ∈ chosenNormalBasisPrincipalUnitSet K L n := by
  rcases
    exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_le_integerRingFieldSubmodule
      (K := K) (L := L) with ⟨b, hb⟩
  rcases exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_mul_mul_mem_self
      (K := K) (L := L) with ⟨cMul, hcMul⟩
  rcases exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_isClosed
      (K := K) (L := L) with ⟨cClosed, hcClosed⟩
  refine ⟨max (b + 1) (max cMul cClosed), ?_⟩
  intro n hn z hz
  have hbn : b + 1 ≤ n :=
    le_trans (le_max_left (b + 1) (max cMul cClosed)) hn
  have hrest : max cMul cClosed ≤ max (b + 1) (max cMul cClosed) :=
    le_max_right (b + 1) (max cMul cClosed)
  have hcMuln : cMul ≤ n :=
    le_trans (le_trans (le_max_left cMul cClosed) hrest) hn
  have hcClosedn : cClosed ≤ n :=
    le_trans (le_trans (le_max_right cMul cClosed) hrest) hn
  let hmulLattice := hcMul n hcMuln
  have hmul : ∀ u : 𝒪[L]ˣ, u ∈ chosenNormalBasisPrincipalUnitSet K L n →
      ∀ v : 𝒪[L]ˣ, v ∈ chosenNormalBasisPrincipalUnitSet K L n →
        u * v ∈ chosenNormalBasisPrincipalUnitSet K L n := by
    intro u hu v hv
    exact chosenNormalBasisPrincipalUnitSet_mul_mem
      (K := K) (L := L) hmulLattice hu hv
  rcases exists_tendsto_chosenNormalBasisPrincipalUnitCorrectionProduct_principalUnit
      (K := K) (L := L) hb hbn z hz with ⟨x, hx⟩
  let xu : 𝒪[L]ˣ := (x : principalUnits L 1)
  refine ⟨xu, ?_, ?_⟩
  · exact hx
  · exact chosenNormalBasisPrincipalUnitCorrectionProduct_limit_mem
      (K := K) (L := L) (hcClosed n hcClosedn) hmul z hz xu hx