import Definitions.Def_AutomorphicForm_SiegelCoordinates

open NumberField IsDedekindDomain Matrix

noncomputable section

namespace AutomorphicForm

namespace SiegelReduction

open AutomorphicForm.WindowedSiegel AutomorphicForm.SiegelCoordinates NumberField.AdelicLevel
  NumberField.InfinitePlace

variable (F : Type) [Field F] [NumberField F]

theorem archComponent_globalPoints_apply (w : InfinitePlace F) (γ : GL (Fin 2) F) (i j : Fin 2) :
    ((archComponent F w (glArch (𝓞 F) F (globalPoints (𝓞 F) F γ)) : GL (Fin 2) w.Completion) :
        Matrix (Fin 2) (Fin 2) w.Completion) i j
      = ((γ : Matrix (Fin 2) (Fin 2) F) i j : w.Completion) := rfl

theorem glFin_globalPoints_apply (γ : GL (Fin 2) F) (i j : Fin 2) :
    ((glFin (𝓞 F) F (globalPoints (𝓞 F) F γ) : GL (Fin 2) (FiniteAdeleRing (𝓞 F) F)) :
        Matrix (Fin 2) (Fin 2) (FiniteAdeleRing (𝓞 F) F)) i j
      = algebraMap F (FiniteAdeleRing (𝓞 F) F) ((γ : Matrix (Fin 2) (Fin 2) F) i j) := rfl

omit [NumberField F] in

theorem norm_coe_completion (w : InfinitePlace F) (x : F) : ‖(x : w.Completion)‖ = w x := by
  rw [InfinitePlace.Completion.norm_coe]
  rfl

theorem det_archComponent_globalPoints (w : InfinitePlace F) (γ : GL (Fin 2) F) :
    ((archComponent F w (glArch (𝓞 F) F (globalPoints (𝓞 F) F γ)) : GL (Fin 2) w.Completion) :
        Matrix (Fin 2) (Fin 2) w.Completion).det
      = ((γ : Matrix (Fin 2) (Fin 2) F).det : w.Completion) := by
  rw [Matrix.det_fin_two, Matrix.det_fin_two]
  simp only [archComponent_globalPoints_apply, WithAbs.toAbs_sub, WithAbs.toAbs_mul,
    UniformSpace.Completion.coe_sub, UniformSpace.Completion.coe_mul]
  apply NumberField.InfinitePlace.Completion.ext
  rw [← NumberField.InfinitePlace.Completion.equiv_apply, map_sub, map_mul, map_mul]
  simp only [NumberField.InfinitePlace.Completion.equiv_apply]

theorem archHeight_globalPoints_mul_mul_archHeight_le (γ : GL (Fin 2) F)
    (hγ : (γ : Matrix (Fin 2) (Fin 2) F) 1 0 ≠ 0) (h : GL (Fin 2) (InfiniteAdeleRing F)) :
    archHeight F (glArch (𝓞 F) F (globalPoints (𝓞 F) F γ) * h) * archHeight F h
      ≤ |(Algebra.norm ℚ ((γ : Matrix (Fin 2) (Fin 2) F).det) : ℝ)|
          / |(Algebra.norm ℚ ((γ : Matrix (Fin 2) (Fin 2) F) 1 0) : ℝ)| ^ 2 := by
  have hplace : ∀ w : InfinitePlace F,
      localHeight (archComponent F w (glArch (𝓞 F) F (globalPoints (𝓞 F) F γ) * h))
          * localHeight (archComponent F w h)
        ≤ w ((γ : Matrix (Fin 2) (Fin 2) F).det) / w ((γ : Matrix (Fin 2) (Fin 2) F) 1 0) ^ 2 := by
    intro w
    have h10 : ((archComponent F w (glArch (𝓞 F) F (globalPoints (𝓞 F) F γ)) :
        GL (Fin 2) w.Completion) : Matrix (Fin 2) (Fin 2) w.Completion) 1 0 ≠ 0 := by
      rw [archComponent_globalPoints_apply, ← norm_pos_iff, norm_coe_completion]
      exact InfinitePlace.pos_iff.mpr hγ
    have hle := localHeight_mul_mul_localHeight_le
      (archComponent F w (glArch (𝓞 F) F (globalPoints (𝓞 F) F γ))) (archComponent F w h) h10
    rw [det_archComponent_globalPoints, archComponent_globalPoints_apply, norm_coe_completion,
      norm_coe_completion] at hle
    rwa [map_mul]
  have hnonneg : ∀ w : InfinitePlace F,
      0 ≤ localHeight (archComponent F w (glArch (𝓞 F) F (globalPoints (𝓞 F) F γ) * h))
        * localHeight (archComponent F w h) :=
    fun w => mul_nonneg (localHeight_pos _).le (localHeight_pos _).le
  unfold archHeight
  rw [← Finset.prod_mul_distrib]
  calc ∏ w : InfinitePlace F,
          localHeight (archComponent F w (glArch (𝓞 F) F (globalPoints (𝓞 F) F γ) * h)) ^ w.mult
            * localHeight (archComponent F w h) ^ w.mult
      = ∏ w : InfinitePlace F,
          (localHeight (archComponent F w (glArch (𝓞 F) F (globalPoints (𝓞 F) F γ) * h))
            * localHeight (archComponent F w h)) ^ w.mult := by
        refine Finset.prod_congr rfl fun w _ => ?_
        rw [mul_pow]
    _ ≤ ∏ w : InfinitePlace F,
          (w ((γ : Matrix (Fin 2) (Fin 2) F).det) / w ((γ : Matrix (Fin 2) (Fin 2) F) 1 0) ^ 2)
            ^ w.mult := by
        refine Finset.prod_le_prod (fun w _ => pow_nonneg (hnonneg w) _) fun w _ => ?_
        exact pow_le_pow_left₀ (hnonneg w) (hplace w) _
    _ = (∏ w : InfinitePlace F, w ((γ : Matrix (Fin 2) (Fin 2) F).det) ^ w.mult)
          / (∏ w : InfinitePlace F, w ((γ : Matrix (Fin 2) (Fin 2) F) 1 0) ^ w.mult) ^ 2 := by
        rw [← Finset.prod_pow, ← Finset.prod_div_distrib]
        refine Finset.prod_congr rfl fun w _ => ?_
        rw [div_pow, ← pow_mul, ← pow_mul, mul_comm 2]
    _ = |(Algebra.norm ℚ ((γ : Matrix (Fin 2) (Fin 2) F).det) : ℝ)|
          / |(Algebra.norm ℚ ((γ : Matrix (Fin 2) (Fin 2) F) 1 0) : ℝ)| ^ 2 := by
        rw [prod_eq_abs_norm, prod_eq_abs_norm, Rat.cast_abs, Rat.cast_abs]

theorem mem_range_of_coe_mem_integralFiniteAdeles {x : F}
    (hx : algebraMap F (FiniteAdeleRing (𝓞 F) F) x ∈ integralFiniteAdeles (𝓞 F) F) :
    x ∈ (algebraMap (𝓞 F) F).range := by
  refine HeightOneSpectrum.mem_integers_of_valuation_le_one F x fun v => ?_
  rw [← HeightOneSpectrum.valuedAdicCompletion_eq_valuation']
  exact valued_apply_le_one hx v

theorem mem_range_of_glFin_globalPoints_mem {γ : GL (Fin 2) F}
    (hγ : glFin (𝓞 F) F (globalPoints (𝓞 F) F γ) ∈ finiteIntegralGL2 (𝓞 F) F) (i j : Fin 2) :
    (γ : Matrix (Fin 2) (Fin 2) F) i j ∈ (algebraMap (𝓞 F) F).range ∧
      ((γ⁻¹ : GL (Fin 2) F) : Matrix (Fin 2) (Fin 2) F) i j ∈ (algebraMap (𝓞 F) F).range := by
  rw [mem_finiteIntegralGL2_iff] at hγ
  refine ⟨mem_range_of_coe_mem_integralFiniteAdeles F ?_,
    mem_range_of_coe_mem_integralFiniteAdeles F ?_⟩
  · rw [← glFin_globalPoints_apply]
    exact hγ.1 i j
  · rw [← glFin_globalPoints_apply, map_inv, map_inv]
    exact hγ.2 i j

theorem abs_norm_eq_one_of_mem_range {x : F} (hx : x ∈ (algebraMap (𝓞 F) F).range)
    (hx' : x⁻¹ ∈ (algebraMap (𝓞 F) F).range) (hx0 : x ≠ 0) : |Algebra.norm ℚ x| = 1 := by
  obtain ⟨a, rfl⟩ := hx
  obtain ⟨b, hb⟩ := hx'
  have hab : a * b = 1 := by
    apply IsFractionRing.injective (𝓞 F) F
    rw [map_mul, map_one, hb, mul_inv_cancel₀ hx0]
  have hu : IsUnit a := IsUnit.of_mul_eq_one b hab
  have h1 := NumberField.isUnit_iff_norm.mp hu
  rw [RingOfIntegers.coe_norm] at h1
  exact h1

theorem one_le_abs_norm_of_mem_range {x : F} (hx : x ∈ (algebraMap (𝓞 F) F).range) (hx0 : x ≠ 0) :
    (1 : ℝ) ≤ |(Algebra.norm ℚ x : ℝ)| := by
  obtain ⟨a, rfl⟩ := hx
  have ha : a ≠ 0 := fun h => hx0 (by rw [h, map_zero])
  have hz : Algebra.norm ℤ a ≠ 0 := Algebra.norm_ne_zero_iff.mpr ha
  have hq : (Algebra.norm ℚ (algebraMap (𝓞 F) F a) : ℝ) = ((Algebra.norm ℤ a : ℤ) : ℝ) := by
    rw [show (algebraMap (𝓞 F) F a) = ((a : 𝓞 F) : F) from rfl, ← Algebra.coe_norm_int]
    push_cast
    rfl
  rw [hq, ← Int.cast_abs]
  exact_mod_cast Int.one_le_abs hz

theorem archHeight_mul_mul_archHeight_le_one (γ : GL (Fin 2) F)
    (hγ : (γ : Matrix (Fin 2) (Fin 2) F) 1 0 ≠ 0) (g : AdelicGL2 (𝓞 F) F)
    (hg : glFin (𝓞 F) F g ∈ finiteIntegralGL2 (𝓞 F) F)
    (hγg : glFin (𝓞 F) F (globalPoints (𝓞 F) F γ * g) ∈ finiteIntegralGL2 (𝓞 F) F) :
    archHeight F (glArch (𝓞 F) F (globalPoints (𝓞 F) F γ * g)) * archHeight F (glArch (𝓞 F) F g)
      ≤ 1 := by
  have hγint : glFin (𝓞 F) F (globalPoints (𝓞 F) F γ) ∈ finiteIntegralGL2 (𝓞 F) F := by
    have h := Subgroup.mul_mem _ hγg (Subgroup.inv_mem _ hg)
    rwa [map_mul, mul_inv_cancel_right] at h
  have hdet : ((γ : Matrix (Fin 2) (Fin 2) F).det) ∈ (algebraMap (𝓞 F) F).range := by
    rw [Matrix.det_fin_two]
    exact Subring.sub_mem _
      (Subring.mul_mem _ (mem_range_of_glFin_globalPoints_mem F hγint 0 0).1
        (mem_range_of_glFin_globalPoints_mem F hγint 1 1).1)
      (Subring.mul_mem _ (mem_range_of_glFin_globalPoints_mem F hγint 0 1).1
        (mem_range_of_glFin_globalPoints_mem F hγint 1 0).1)
  have hdet' : ((γ : Matrix (Fin 2) (Fin 2) F).det)⁻¹ ∈ (algebraMap (𝓞 F) F).range := by
    have hinv : ((γ : Matrix (Fin 2) (Fin 2) F).det)⁻¹
        = ((γ⁻¹ : GL (Fin 2) F) : Matrix (Fin 2) (Fin 2) F).det := by
      rw [Matrix.coe_units_inv, Matrix.det_nonsing_inv, Ring.inverse_eq_inv']
    rw [hinv, Matrix.det_fin_two]
    exact Subring.sub_mem _
      (Subring.mul_mem _ (mem_range_of_glFin_globalPoints_mem F hγint 0 0).2
        (mem_range_of_glFin_globalPoints_mem F hγint 1 1).2)
      (Subring.mul_mem _ (mem_range_of_glFin_globalPoints_mem F hγint 0 1).2
        (mem_range_of_glFin_globalPoints_mem F hγint 1 0).2)
  have hdet0 : ((γ : Matrix (Fin 2) (Fin 2) F).det) ≠ 0 := (Matrix.isUnits_det_units γ).ne_zero
  have hN1 : |(Algebra.norm ℚ ((γ : Matrix (Fin 2) (Fin 2) F).det) : ℝ)| = 1 := by
    have h1 := abs_norm_eq_one_of_mem_range F hdet hdet' hdet0
    rw [← Rat.cast_abs, h1, Rat.cast_one]
  have hN2 : (1 : ℝ) ≤ |(Algebra.norm ℚ ((γ : Matrix (Fin 2) (Fin 2) F) 1 0) : ℝ)| :=
    one_le_abs_norm_of_mem_range F (mem_range_of_glFin_globalPoints_mem F hγint 1 0).1 hγ
  rw [map_mul]
  refine (archHeight_globalPoints_mul_mul_archHeight_le F γ hγ _).trans ?_
  rw [hN1, div_le_one (by positivity)]
  exact one_le_pow₀ hN2

end SiegelReduction

end AutomorphicForm