import Mathlib.RingTheory.Ideal.Operations
import Mathlib.RingTheory.FiniteType
import Mathlib.Order.Height
import Mathlib.RingTheory.Polynomial.Quotient
import Mathlib.RingTheory.PrincipalIdealDomain
import Mathlib.RingTheory.DedekindDomain.Basic
import Mathlib.RingTheory.Ideal.Quotient
import Mathlib.RingTheory.Localization.AtPrime
import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
import Mathlib.Order.ConditionallyCompleteLattice.Basic
import CommAlg.krull

section AddToOrder

open List hiding le_antisymm
open OrderDual

universe u v

variable {α β : Type _}
variable [LT α] [LT β] (s t : Set α)

namespace Set

theorem append_mem_subchain_iff :
l ++ l' ∈ s.subchain ↔ l ∈ s.subchain ∧ l' ∈ s.subchain ∧ ∀ a ∈ l.getLast?, ∀ b ∈ l'.head?, a < b := by
  simp [subchain, chain'_append]
  aesop

end Set

namespace List
#check Option

theorem getLast?_map (l : List α) (f : α → β) :
  (l.map f).getLast? = Option.map f (l.getLast?) := by
  cases' l with a l
  . rfl
  induction' l with b l ih
  . rfl
  . simp [List.getLast?_cons_cons, ih]
  

end List
end AddToOrder

--trying and failing to prove ht p = dim R_p
section Localization

variable {R : Type _} [CommRing R] (I : PrimeSpectrum R)
variable {S : Type _} [CommRing S] [Algebra R S] [IsLocalization.AtPrime S I.asIdeal]

open Ideal
open LocalRing
open PrimeSpectrum

#check algebraMap R (Localization.AtPrime I.asIdeal)
#check PrimeSpectrum.comap (algebraMap R (Localization.AtPrime I.asIdeal))

#check krullDim
#check dim_eq_bot_iff
#check height_le_krullDim

variable (J₁ J₂ : PrimeSpectrum (Localization.AtPrime I.asIdeal))
example (h : J₁ ≤ J₂) : PrimeSpectrum.comap (algebraMap R (Localization.AtPrime I.asIdeal)) J₁ ≤
  PrimeSpectrum.comap (algebraMap R (Localization.AtPrime I.asIdeal)) J₂ := by
  intro x hx
  exact h hx

def gadslfasd' : Ideal S := (IsLocalization.AtPrime.localRing S I.asIdeal).maximalIdeal

-- instance gadslfasd : LocalRing S := IsLocalization.AtPrime.localRing S I.asIdeal

example (f : α → β) (hf : Function.Injective f) (h : a₁ ≠ a₂) : f a₁ ≠ f a₂ := by library_search

instance map_prime (J : PrimeSpectrum R) (hJ : J ≤ I) :
  (Ideal.map (algebraMap R S) J.asIdeal : Ideal S).IsPrime where
    ne_top' := by
      intro h
      rw [eq_top_iff_one, map, mem_span] at h
    mem_or_mem' := sorry

lemma comap_lt_of_lt (J₁ J₂ : PrimeSpectrum S) (J_lt : J₁ < J₂) : 
  PrimeSpectrum.comap (algebraMap R S) J₁ < PrimeSpectrum.comap (algebraMap R S) J₂ := by
  apply lt_of_le_of_ne
  apply comap_mono (le_of_lt J_lt)
  sorry

lemma lt_of_comap_lt (J₁ J₂ : PrimeSpectrum S)
(hJ : PrimeSpectrum.comap (algebraMap R S) J₁ < PrimeSpectrum.comap (algebraMap R S) J₂) :
J₁ < J₂ := by
  apply lt_of_le_of_ne
  sorry

/- If S = R_p, then height p = dim S -/
lemma height_eq_height_comap (J : PrimeSpectrum S) :
  height (PrimeSpectrum.comap (algebraMap R S) J) = height J := by
  simp [height]
  have H : {J_1 | J_1 < (PrimeSpectrum.comap (algebraMap R S)) J} = 
    (PrimeSpectrum.comap (algebraMap R S))'' {J_2 | J_2 < J}
  . sorry
  rw [H]
  apply Set.chainHeight_image
  intro x y
  constructor
  apply comap_lt_of_lt
  apply lt_of_comap_lt
  
lemma disjoint_primeCompl (I : PrimeSpectrum R) :
  { p | Disjoint (I.asIdeal.primeCompl : Set R) p.asIdeal} = {p | p ≤ I} := by
  ext p; apply Set.disjoint_compl_left_iff_subset

theorem localizationPrime_comap_range [Algebra R S] (I : PrimeSpectrum R) [IsLocalization.AtPrime S I.asIdeal] :
    Set.range (PrimeSpectrum.comap (algebraMap R S)) = { p | p ≤ I} := by
    rw [← disjoint_primeCompl]
    apply localization_comap_range


#check Set.chainHeight_image

lemma height_eq_dim_localization : height I = krullDim S := by
  --first show height I = height gadslfasd'
  simp [@krullDim_eq_height _ _ (IsLocalization.AtPrime.localRing S I.asIdeal)]
  simp [height]
  let f := (PrimeSpectrum.comap (algebraMap R S))
  have H : {J | J < I} = f '' {J | J < closedPoint S}
  
lemma height_eq_dim_localization' :
  height I = krullDim (Localization.AtPrime I.asIdeal) := Ideal.height_eq_dim_localization I

end Localization




section Polynomial

open Ideal Polynomial
variables {R : Type _} [CommRing R]
variable (J : Ideal R[X])
#check Ideal.comap C J

--given ideals I J, I ⊔ J is their sum
--given a in R, span {a} is the ideal generated by a
--the map R → R[X] is C →+*
--to show p[x] is prime, show p[x] is the kernel of the map R[x] → R → R/p
#check RingHom.ker_isPrime

def adj_x_map (I : Ideal R) : R[X] →+* R ⧸ I := (Ideal.Quotient.mk I).comp constantCoeff
--def adj_x_map' (I : Ideal R) : R[X] →+* R ⧸ I := (Ideal.Quotient.mk I).comp (evalRingHom 0)
def adjoin_x (I : Ideal R) : Ideal (Polynomial R) := RingHom.ker (adj_x_map I)
def adjoin_x' (I : PrimeSpectrum R) : PrimeSpectrum (Polynomial R) where
  asIdeal := adjoin_x I.asIdeal
  IsPrime := RingHom.ker_isPrime _

/- This somehow isn't in Mathlib? -/
@[simp]
theorem span_singleton_one : span ({0} : Set R) = ⊥ := by simp only [span_singleton_eq_bot]

theorem coeff_C_eq : RingHom.comp constantCoeff C = RingHom.id R := by ext; simp

variable (I : PrimeSpectrum R)
#check RingHom.ker (C.comp (Ideal.Quotient.mk I.asIdeal))
--#check Ideal.Quotient.mk I.asIdeal

def map_prime' (I : PrimeSpectrum R) : IsPrime (I.asIdeal.map C) := Ideal.isPrime_map_C_of_isPrime I.IsPrime

def map_prime'' (I : PrimeSpectrum R) : PrimeSpectrum R[X] := ⟨I.asIdeal.map C, map_prime' I⟩

@[simp]
lemma adj_x_comp_C (I : Ideal R) : RingHom.comp (adj_x_map I) C = Ideal.Quotient.mk I := by
  ext x; simp [adj_x_map]

-- ideal.mem_quotient_iff_mem_sup
lemma adjoin_x_eq (I : Ideal R) : adjoin_x I = I.map C ⊔ Ideal.span {X} := by
  apply le_antisymm
  . rintro p hp
    have h : ∃ q r, p = C r + X * q := ⟨p.divX, p.coeff 0, p.divX_mul_X_add.symm.trans $ by ring⟩
    obtain ⟨q, r, rfl⟩ := h
    suffices : r ∈ I
    . simp only [Submodule.mem_sup, Ideal.mem_span_singleton]
      refine' ⟨C r, Ideal.mem_map_of_mem C this, X * q, ⟨q, rfl⟩, rfl⟩
    rw [adjoin_x, adj_x_map, RingHom.mem_ker, RingHom.comp_apply] at hp
    rw [constantCoeff_apply, coeff_add, coeff_C_zero, coeff_X_mul_zero, add_zero] at hp
    rwa  [←RingHom.mem_ker, Ideal.mk_ker] at hp
  . rw [sup_le_iff]
    constructor
    . simp [adjoin_x, RingHom.ker, ←map_le_iff_le_comap, Ideal.map_map]
    . simp [span_le, adjoin_x, RingHom.mem_ker, adj_x_map]

lemma adjoin_x_inj {I J : Ideal R} (h : adjoin_x I = adjoin_x J) : I = J := by
  simp [adjoin_x_eq] at h
  have H : Ideal.map constantCoeff (Ideal.map C I ⊔ span {X}) =
          Ideal.map constantCoeff (Ideal.map C J ⊔ span {X}) := by rw [h]
  simp [Ideal.map_sup, Ideal.map_span, Ideal.map_map, coeff_C_eq] at H
  exact H


lemma map_lt_adjoin_x (I : PrimeSpectrum R) : map_prime'' I < adjoin_x' I := by
  simp [map_prime'', adjoin_x', adjoin_x_eq]
  show Ideal.map C I.asIdeal < Ideal.map C I.asIdeal ⊔ span {X}
  simp [Ideal.span_le, mem_map_C_iff]
  use 1
  simp
  intro h
  apply I.IsPrime.ne_top'
  rw [Ideal.eq_top_iff_one]
  exact h

lemma map_inj {I J : Ideal R} (h : I.map C = J.map C) : I = J := by
  have H : Ideal.map constantCoeff (Ideal.map C I) =
          Ideal.map constantCoeff (Ideal.map C J) := by rw [h]
  simp [Ideal.map_map, coeff_C_eq] at H
  exact H

lemma map_strictmono (I J : Ideal R) (h : I < J) : I.map C < J.map C := by
  rw [lt_iff_le_and_ne] at h ⊢
  constructor
  . apply map_mono h.1
  . intro H
    exact h.2 (map_inj H)

lemma adjoin_x_strictmono (I J : Ideal R) (h : I < J) : adjoin_x I < adjoin_x J := by
  rw [lt_iff_le_and_ne] at h ⊢
  constructor
  . rw [adjoin_x_eq, adjoin_x_eq]
    apply sup_le_sup_right
    apply map_mono h.1
  . intro H
    exact h.2 (adjoin_x_inj H)

example (n : ℕ∞) : n + 0 = n := by simp?

#eval List.Chain' (· < ·) [2,3]
example : [4,5] ++ [2] = [4,5,2] := rfl
#eval [2,4,5].map (λ n => n + n)

/- Given an ideal p in R, define the ideal p[x] in R[x] -/
lemma ht_adjoin_x_eq_ht_add_one [Nontrivial R] (I : PrimeSpectrum R) : height I + 1 ≤ height (adjoin_x' I) := by
  suffices H : height I + (1 : ℕ) ≤ height (adjoin_x' I) + (0 : ℕ)
  . norm_cast at H; rw [add_zero] at H; exact H
  rw [height, height, Set.chainHeight_add_le_chainHeight_add {J | J < I} _ 1 0]
  intro l hl
  use ((l.map map_prime'') ++ [map_prime'' I])
  constructor
  . simp [Set.append_mem_subchain_iff]
    refine' ⟨_,_,_⟩
    . show (List.map map_prime'' l).Chain' (· < ·) ∧ ∀ i ∈ _, i ∈ _
      constructor
      . apply List.chain'_map_of_chain' map_prime''
        intro a b hab
        apply map_strictmono a.asIdeal b.asIdeal
        exact hab
        exact hl.1
      . intro i hi
        rw [List.mem_map] at hi
        obtain ⟨a, ha, rfl⟩ := hi
        show map_prime'' a < adjoin_x' I
        calc map_prime'' a < map_prime'' I := by apply map_strictmono; apply hl.2; apply ha
          _ < adjoin_x' I := by apply map_lt_adjoin_x
    . apply map_lt_adjoin_x
    . intro a ha
      have H : ∃ b : PrimeSpectrum R, b ∈ l ∧ map_prime'' b = a
      . have H2 : l ≠ []
        . intro h
          rw [h] at ha
          tauto
        use l.getLast H2
        refine' ⟨List.getLast_mem H2, _⟩
        have H3 : l.map map_prime'' ≠ []
        . intro hl
          apply H2
          apply List.eq_nil_of_map_eq_nil hl
        rw [List.getLast?_eq_getLast _ H3, Option.some_inj] at ha
        simp [←ha, List.getLast_map _ H2]
      obtain ⟨b, hb, rfl⟩ := H
      apply map_strictmono
      apply hl.2
      exact hb
  . simp

lemma ne_bot_iff_exists' (n : WithBot ℕ∞) : n ≠ ⊥ ↔ ∃ m : ℕ∞, n = m := by
  convert WithBot.ne_bot_iff_exists using 3
  exact comm


lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
  krullDim R + (1 : ℕ∞) ≤ krullDim (Polynomial R) := by
  cases' krullDim_nonneg_of_nontrivial R with n hn
  rw [hn]
  change ↑(n + 1) ≤ krullDim R[X]
  have hn' := le_of_eq hn.symm
  rw [le_krullDim_iff'] at hn' ⊢
  cases' hn' with I hI
  use adjoin_x' I
  apply WithBot.coe_mono
  calc n + 1 ≤ height I + 1 := by
        apply add_le_add_right
        rw [WithBot.coe_le_coe] at hI
        exact hI
    _ ≤ height (adjoin_x' I) := ht_adjoin_x_eq_ht_add_one I
  

end Polynomial

open Ideal

variable {R : Type _} [CommRing R]

lemma height_le_top_iff_exists {I : PrimeSpectrum R} (hI : height I ≤ ⊤) :
  ∃ n : ℕ, true := by
  sorry

lemma eq_of_height_eq_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) (hJ : height J < ⊤)
  (ht_eq : height I = height J) : I = J := by
  by_cases h : I = J
  . exact h
  . have I_lt_J := lt_of_le_of_ne I_le_J h
    exfalso
    sorry

section Quotient

variables {R : Type _} [CommRing R] (I : Ideal R)

#check List.map <| PrimeSpectrum.comap <| Ideal.Quotient.mk I

lemma comap_chain {l : List (PrimeSpectrum (R ⧸ I))} (hl : l.Chain' (· < ·)) :
  List.Chain' (. < .) ((List.map <| PrimeSpectrum.comap <| Ideal.Quotient.mk I) l) := by


lemma dim_quotient_le_dim : krullDim (R ⧸ I) ≤ krullDim R := by

end Quotient