ValuationSubring_ringKrullDim_le_ringKrullDim_comap_add_trdeg.lean

lemma zpow_eq_one_imp {γ : Γ₀} (h1 : γ < 1) {m : ℤ} (hm : γ ^ m = 1) : m = 0

lemma exists_ne_map_eq_of_sum_eq_zero {R : Type*} [CommRing R] (v : Valuation R Γ₀)
    {ι : Type*} (s : Finset ι) (t : ι → R) (hs : s.Nonempty) (ht : ∀ i ∈ s, v (t i) ≠ 0)
    (hsum : ∑ i ∈ s, t i = 0) : ∃ i ∈ s, ∃ j ∈ s, i ≠ j ∧ v (t i) = v (t j)

def resHom : A.comap (algebraMap K L) →+* A

lemma coe_resHom_apply (c : A.comap (algebraMap K L)) :
    ((resHom K A c : A) : L) = algebraMap K L c

def ValIndep {b : ℕ} (x : Fin b → L) : Prop

lemma valuation_eq_one_of_le {S : ValuationSubring L} (h : A ≤ S) {y : L}
    (hy : A.valuation y = 1) : S.valuation y = 1

lemma dagger {P Q : Ideal A} [P.IsPrime] [Q.IsPrime]
    (hinv : Ideal.comap (resHom K A) P = Ideal.comap (resHom K A) Q) (c : K)
    (h0 : (ofPrime A P).valuation (algebraMap K L c) = 1) :
    (ofPrime A Q).valuation (algebraMap K L c) = 1

lemma valIndep_cons {P Q : Ideal A} [P.IsPrime] [Q.IsPrime] (hPQ : P ≤ Q)
    (hinv : Ideal.comap (resHom K A) P = Ideal.comap (resHom K A) Q)
    (f : A) (hfQ : f ∈ Q) (hfP : f ∉ P) {b : ℕ} (x : Fin b → A) (hx : ∀ k, x k ∉ Q)
    (hVI : ValIndep K A (fun k => (x k : L))) :
    ValIndep K A (Fin.cons (f : L) (fun k => (x k : L)) : Fin (b + 1) → L) := by
  intro c m hm
  set O₀ := ofPrime A P
  set O₁ := ofPrime A Q
  have hA0 : A ≤ O₀ := le_ofPrime A P
  have hA1 : A ≤ O₁ := le_ofPrime A Q
  rw [Fin.prod_univ_succ] at hm
  simp only [Fin.cons_zero, Fin.cons_succ] at hm
  have hf0 : O₀.valuation (f : L) = 1 :=
    (ofPrime_valuation_eq_one_iff_mem_primeCompl A P f).mpr hfP
  have hx0 : ∀ k, O₀.valuation (x k : L) = 1 := fun k =>
    (ofPrime_valuation_eq_one_iff_mem_primeCompl A P (x k)).mpr (fun h => hx k (hPQ h))
  have hx1 : ∀ k, O₁.valuation (x k : L) = 1 := fun k =>
    (ofPrime_valuation_eq_one_iff_mem_primeCompl A Q (x k)).mpr (hx k)
  have hf1 : O₁.valuation (f : L) < 1 := by
    have hle : O₁.valuation (f : L) ≤ 1 := (O₁.valuation_le_one_iff _).mpr (hA1 f.2)
    have hne : O₁.valuation (f : L) ≠ 1 := fun h =>
      (Ideal.mem_primeCompl_iff.mp
        ((ofPrime_valuation_eq_one_iff_mem_primeCompl A Q f).mp h)) hfQ
    exact lt_of_le_of_ne hle hne
  have h0 : O₀.valuation (algebraMap K L c) = 1 := by
    have h := valuation_eq_one_of_le hA0 hm
    rw [map_mul, map_mul, map_prod, map_zpow₀, hf0, one_zpow, one_mul] at h
    simp_rw [map_zpow₀, hx0, one_zpow, Finset.prod_const_one, mul_one] at h
    exact h
  have h1 : O₁.valuation (algebraMap K L c) = 1 := dagger hinv c h0
  have hm0 : m 0 = 0 := by
    have h := valuation_eq_one_of_le hA1 hm
    rw [map_mul, map_mul, map_prod, map_zpow₀, h1, one_mul] at h
    simp_rw [map_zpow₀, hx1, one_zpow, Finset.prod_const_one, mul_one] at h
    exact zpow_eq_one_imp hf1 h
  have hrest : (fun k : Fin b => m k.succ) = 0 := by
    apply hVI c
    rw [hm0, zpow_zero, one_mul] at hm
    exact hm
  funext i
  refine Fin.cases ?_ ?_ i
  · exact hm0
  · intro j; exact congr_fun hrest j

lemma extraction (s : LTSeries (PrimeSpectrum A)) :
    ∃ (s₀ : LTSeries (PrimeSpectrum (A.comap (algebraMap K L)))) (b : ℕ) (x : Fin b → A),
      s₀.head = PrimeSpectrum.comap (resHom K A) s.head ∧
      (∀ k, x k ∉ s.head.asIdeal) ∧
      ValIndep K A (fun k => (x k : L)) ∧
      s.length ≤ s₀.length + b := by
  induction s using RelSeries.inductionOn with
  | singleton P =>
    refine ⟨RelSeries.singleton _ (PrimeSpectrum.comap (resHom K A) P), 0, Fin.elim0, ?_, ?_, ?_,
      ?_⟩
    · simp
    · intro k; exact k.elim0
    · intro c m _; funext k; exact k.elim0
    · simp
  | cons p P hP ih =>
    obtain ⟨s₀, b, x, hhead, hx, hVI, hlen⟩ := ih
    have hlt : P < p.head := hP
    have hle : P.asIdeal ≤ p.head.asIdeal := (PrimeSpectrum.asIdeal_le_asIdeal _ _).mpr hlt.le
    have hcomap_le :
        PrimeSpectrum.comap (resHom K A) P ≤ PrimeSpectrum.comap (resHom K A) p.head :=
      (PrimeSpectrum.asIdeal_le_asIdeal _ _).mp (Ideal.comap_mono hle)
    by_cases hvis : PrimeSpectrum.comap (resHom K A) P < PrimeSpectrum.comap (resHom K A) p.head
    · have hrel : PrimeSpectrum.comap (resHom K A) P < s₀.head := by rwa [hhead]
      refine ⟨s₀.cons _ hrel, b, x, ?_, ?_, hVI, ?_⟩
      · simp only [RelSeries.head_cons]
      · intro k hk
        rw [RelSeries.head_cons] at hk
        exact hx k (hle hk)
      · simp only [RelSeries.cons_length]; omega
    · have heq : PrimeSpectrum.comap (resHom K A) P = PrimeSpectrum.comap (resHom K A) p.head :=
        eq_of_le_of_not_lt hcomap_le hvis
      have hne : P.asIdeal ≠ p.head.asIdeal := fun h => hlt.ne (PrimeSpectrum.ext h)
      obtain ⟨f, hfQ, hfP⟩ : ∃ f, f ∈ p.head.asIdeal ∧ f ∉ P.asIdeal :=
        IsConcreteLE.exists_of_lt (hle.lt_of_ne hne)
      have hinv : Ideal.comap (resHom K A) P.asIdeal = Ideal.comap (resHom K A) p.head.asIdeal := by
        have h := congrArg PrimeSpectrum.asIdeal heq
        simpa using h
      refine ⟨s₀, b + 1, Fin.cons f x, ?_, ?_, ?_, ?_⟩
      · rw [RelSeries.head_cons, heq]; exact hhead
      · intro k
        rw [RelSeries.head_cons]
        refine Fin.cases ?_ ?_ k
        · simpa using hfP
        · intro j; simp only [Fin.cons_succ]; exact fun h => hx j (hle h)
      · have h := valIndep_cons hle hinv f hfQ hfP x hx hVI
        have hfun : (fun k => ((Fin.cons f x : Fin (b + 1) → A) k : L)) =
            (Fin.cons (f : L) (fun k => (x k : L)) : Fin (b + 1) → L) := by
          funext k
          refine Fin.cases ?_ ?_ k
          · simp
          · intro j; simp
        rw [hfun]; exact h
      · simp only [RelSeries.cons_length]; omega

lemma algebraicIndependent_of_valIndep {b : ℕ} (x : Fin b → L) (hx0 : ∀ k, x k ≠ 0)
    (hVI : ValIndep K A x) : AlgebraicIndependent K x

theorem _root_.ValuationSubring.ringKrullDim_le_ringKrullDim_comap_add_trdeg
    {K L : Type*} [Field K] [Field L] [Algebra K L] (A : ValuationSubring L) :
    ringKrullDim A ≤ ringKrullDim (A.comap (algebraMap K L)) +
      (Cardinal.toENat (Algebra.trdeg K L) : WithBot ℕ∞)