import Mathlib
import Definitions.Def_AlgebraicCurve_DivisorPushPull

set_option autoImplicit false

noncomputable section

namespace AlgebraicCurve

section Forget

variable {K K' F' : Type*} [Field K] [Field K'] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']

namespace Place

def forgetConstants (w : Place K' F') : Place K F' where
  toValuationSubring := w.toValuationSubring
  algebraMap_mem' a := by
    rw [IsScalarTower.algebraMap_apply K K' F']
    exact w.algebraMap_mem' (algebraMap K K' a)
  ne_top' := w.ne_top'
  isPrincipalIdealRing' := w.isPrincipalIdealRing'

@[simp]
theorem forgetConstants_toValuationSubring (w : Place K' F') :
    (forgetConstants (K := K) w).toValuationSubring = w.toValuationSubring :=
  rfl

theorem forgetConstants_injective :
    Function.Injective (forgetConstants (K := K) (K' := K') (F' := F')) := by
  intro v w h
  exact Place.ext (congrArg (fun p : Place K F' => p.toValuationSubring) h)

@[simp]
theorem ord_forgetConstants (w : Place K' F') (f : F') :
    (forgetConstants (K := K) w).ord f = w.ord f :=
  rfl

end Place

end Forget

section Extend

variable {K K' F' : Type*} [Field K] [Field K'] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']

namespace Place

variable (K') in

theorem algebraMap_mem_of_isIntegral [Algebra.IsIntegral K K'] (v : Place K F') (a : K') :
    algebraMap K' F' a ∈ v.toValuationSubring := by

  have hint : IsIntegral K (algebraMap K' F' a) :=
    (Algebra.IsIntegral.isIntegral (R := K) a).map (IsScalarTower.toAlgHom K K' F')

  have hint' : IsIntegral v.toValuationSubring (algebraMap K' F' a) := hint.tower_top

  obtain ⟨y, hy⟩ := IsIntegrallyClosed.isIntegral_iff.mp hint'
  rw [← hy]
  exact y.2

variable (K') in

def extendConstants [Algebra.IsIntegral K K'] (v : Place K F') : Place K' F' where
  toValuationSubring := v.toValuationSubring
  algebraMap_mem' := v.algebraMap_mem_of_isIntegral K'
  ne_top' := v.ne_top'
  isPrincipalIdealRing' := v.isPrincipalIdealRing'

@[simp]
theorem extendConstants_toValuationSubring [Algebra.IsIntegral K K'] (v : Place K F') :
    (extendConstants K' v).toValuationSubring = v.toValuationSubring :=
  rfl

variable (K K') in

def constantFieldEquiv [Algebra.IsIntegral K K'] : Place K F' ≃ Place K' F' where
  toFun := extendConstants K'
  invFun := forgetConstants
  left_inv _ := Place.ext rfl
  right_inv _ := Place.ext rfl

@[simp]
theorem constantFieldEquiv_apply_toValuationSubring [Algebra.IsIntegral K K']
    (v : Place K F') :
    (constantFieldEquiv K K' v).toValuationSubring = v.toValuationSubring :=
  rfl

@[simp]
theorem constantFieldEquiv_symm_apply [Algebra.IsIntegral K K'] (w : Place K' F') :
    (constantFieldEquiv K K' (F' := F')).symm w = forgetConstants w :=
  rfl

end Place

end Extend

section Pullback

variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']

namespace Place

variable (F) in

def restrictConstants (w : Place K' F') : Place K F :=
  (forgetConstants (K := K) w).restrict F

@[simp]
theorem restrictConstants_toValuationSubring (w : Place K' F') :
    (restrictConstants F (K := K) w).toValuationSubring
      = w.toValuationSubring.comap (algebraMap F F') :=
  rfl

theorem ord_restrictConstants (w : Place K' F') (f : F) :
    w.ord (algebraMap F F' f)
      = ramificationIndex (F := F) (forgetConstants (K := K) w)
          * (restrictConstants F (K := K) w).ord f :=
  (forgetConstants (K := K) w).ord_restrict f

variable (K') in

theorem restrictConstants_fiber_finite [HasPrincipalDivisors K' F'] (v : Place K F) :
    {w : Place K' F' | restrictConstants F (K := K) w = v}.Finite := by
  obtain ⟨f, hf0, hford⟩ : ∃ f : F, f ≠ 0 ∧ 0 < v.ord f := by
    obtain ⟨π, hπ⟩ := IsDiscreteValuationRing.exists_irreducible v.toValuationSubring
    refine ⟨(π : F), ?_, ?_⟩
    · simpa [ne_eq, ZeroMemClass.coe_eq_zero] using hπ.ne_zero
    · rw [v.ord_coe_irreducible hπ]
      exact one_pos
  have hf0' : algebraMap F F' f ≠ 0 := fun h =>
    hf0 ((map_eq_zero_iff _ (algebraMap F F').injective).mp h)
  obtain ⟨D, hD, -⟩ := HasPrincipalDivisors.exists_divisor (K := K') (algebraMap F F' f) hf0'
  apply Set.Finite.subset D.support.finite_toSet
  intro w hw
  simp only [Set.mem_setOf_eq] at hw
  simp only [Finset.mem_coe, Finsupp.mem_support_iff, hD w]
  have := (forgetConstants (K := K) w).ord_algebraMap_ne_zero_of_restrict_eq
    (v := v) (f := f) (by omega) hw
  exact this

variable (K' F') in

def fiberConstants [HasPrincipalDivisors K' F'] (v : Place K F) : Finset (Place K' F') :=
  (restrictConstants_fiber_finite K' v).toFinset

@[simp]
theorem mem_fiberConstants [HasPrincipalDivisors K' F'] {v : Place K F} {w : Place K' F'} :
    w ∈ fiberConstants K' F' v ↔ restrictConstants F (K := K) w = v := by
  simp only [fiberConstants, Set.Finite.mem_toFinset, Set.mem_setOf_eq]

end Place

namespace Divisor

variable [HasPrincipalDivisors K' F']

variable (K' F') in

def pullbackConstantsSingleHom (v : Place K F) : ℤ →+ Divisor K' F' where
  toFun n := ∑ w ∈ Place.fiberConstants K' F' v,
    Finsupp.single w (n * (Place.forgetConstants (K := K) w).ramificationIndex F)
  map_zero' := by simp
  map_add' m n := by
    rw [← Finset.sum_add_distrib]
    exact Finset.sum_congr rfl fun w _ => by rw [add_mul, Finsupp.single_add]

variable (K' F') in

def pullbackConstants : Divisor K F →+ Divisor K' F' :=
  Finsupp.liftAddHom (pullbackConstantsSingleHom K' F')

theorem pullbackConstants_single (v : Place K F) (n : ℤ) :
    pullbackConstants K' F' (Finsupp.single v n)
      = ∑ w ∈ Place.fiberConstants K' F' v,
          Finsupp.single w (n * (Place.forgetConstants (K := K) w).ramificationIndex F) :=
  Finsupp.liftAddHom_apply_single _ _ _

theorem pullbackConstants_single_apply_of_restrict_eq {v : Place K F} {w : Place K' F'}
    (hw : Place.restrictConstants F (K := K) w = v) (n : ℤ) :
    pullbackConstants K' F' (Finsupp.single v n) w
      = n * (Place.forgetConstants (K := K) w).ramificationIndex F := by
  rw [pullbackConstants_single, Finset.sum_apply']
  refine (Finset.sum_eq_single_of_mem w (Place.mem_fiberConstants.mpr hw) ?_).trans
    (by rw [Finsupp.single_eq_same])
  intro b _ hb
  exact Finsupp.single_eq_of_ne hb.symm

theorem pullbackConstants_single_apply_of_restrict_ne {v : Place K F} {w : Place K' F'}
    (hw : Place.restrictConstants F (K := K) w ≠ v) (n : ℤ) :
    pullbackConstants K' F' (Finsupp.single v n) w = 0 := by
  rw [pullbackConstants_single, Finset.sum_apply']
  refine Finset.sum_eq_zero fun b hb => ?_
  refine Finsupp.single_eq_of_ne fun h => hw ?_
  exact h ▸ Place.mem_fiberConstants.mp hb

theorem pullbackConstants_apply (D : Divisor K F) (w : Place K' F') :
    pullbackConstants K' F' D w
      = (Place.forgetConstants (K := K) w).ramificationIndex F
          * D (Place.restrictConstants F (K := K) w) := by
  induction D using Finsupp.induction with
  | zero => simp
  | single_add v n D _ _ ih =>
    rw [map_add, Finsupp.add_apply, ih, Finsupp.add_apply, mul_add]
    congr 1
    rcases eq_or_ne (Place.restrictConstants F (K := K) w) v with hw | hw
    · rw [pullbackConstants_single_apply_of_restrict_eq hw, hw, Finsupp.single_eq_same,
        mul_comm]
    · rw [pullbackConstants_single_apply_of_restrict_ne hw, Finsupp.single_eq_of_ne hw,
        mul_zero]

theorem pullbackConstants_apply_eq_ord {f : F} {D : Divisor K F}
    (hD : ∀ v : Place K F, D v = v.ord f) (w : Place K' F') :
    pullbackConstants K' F' D w = w.ord (algebraMap F F' f) := by
  rw [pullbackConstants_apply, hD, Place.ord_restrictConstants (K := K) w f]

theorem isPrincipal_pullbackConstants {D : Divisor K F} (hD : D.IsPrincipal) :
    (pullbackConstants K' F' D).IsPrincipal := by
  obtain ⟨f, hf, hDf⟩ := hD
  exact ⟨algebraMap F F' f,
    fun h => hf ((map_eq_zero_iff _ (algebraMap F F').injective).mp h),
    fun w => pullbackConstants_apply_eq_ord hDf w⟩

theorem pullbackConstants_mem_principal {D : Divisor K F}
    (hD : D ∈ principal (K := K) (F := F)) :
    pullbackConstants K' F' D ∈ principal (K := K') (F := F') :=
  isPrincipal_pullbackConstants hD

end Divisor

end Pullback

section ClassGroup

variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K' F']

variable (K K' F F') in

def Pic.baseChange : Pic K F →+ Pic K' F' :=
  QuotientAddGroup.map _ _ (Divisor.pullbackConstants K' F')
    fun _ hD => Divisor.pullbackConstants_mem_principal hD

@[simp]
theorem Pic.baseChange_mk (D : Divisor K F) :
    Pic.baseChange K K' F F' (QuotientAddGroup.mk D)
      = QuotientAddGroup.mk (Divisor.pullbackConstants K' F' D) :=
  rfl

variable (K K' F F') in

class ConstantFieldDegreeFormula : Prop where
  degree_pullbackConstants : ∀ D : Divisor K F,
    Divisor.degree (Divisor.pullbackConstants K' F' D) = Divisor.degree D

theorem Divisor.pullbackConstants_mem_degZero [ConstantFieldDegreeFormula K K' F F']
    {D : Divisor K F} (hD : D ∈ Divisor.degZero (K := K) (F := F)) :
    Divisor.pullbackConstants K' F' D ∈ Divisor.degZero (K := K') (F := F') := by
  rw [Divisor.mem_degZero] at hD ⊢
  rw [ConstantFieldDegreeFormula.degree_pullbackConstants (K := K) (F := F) D, hD]

end ClassGroup

end AlgebraicCurve