SystemDomain.lean

theorem isDomain_of_prime_isSMulRegular
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    {p : R} (hp : Prime p) (hpreg : IsSMulRegular R p) : IsDomain R

theorem regularSystem_quotientHead
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    {p : R} {ps : List R}
    (hreg : IsRegular R (p :: ps))
    (hgen : Ideal.ofList (p :: ps) = maximalIdeal R) :
    let I : Ideal R := Ideal.span {p}
    let S := R ⧸ I
    IsRegular S (ps.map (Ideal.Quotient.mk I)) ∧
      Ideal.ofList (ps.map (Ideal.Quotient.mk I)) =
        (maximalIdeal R).map (Ideal.Quotient.mk I) := by
  dsimp only
  let I : Ideal R := Ideal.span {p}
  let S := R ⧸ I
  have hpMem : p ∈ maximalIdeal R := by
    rw [← hgen]
    exact Ideal.subset_span (by simp)
  have hIle : I ≤ maximalIdeal R := by
    apply Ideal.span_le.mpr
    intro z hz
    simp only [Set.mem_singleton_iff] at hz
    subst z
    change p ∈ maximalIdeal R
    exact hpMem
  have hIne : I ≠ ⊤ :=
    ne_top_of_le_ne_top (maximalIdeal.isMaximal R).ne_top hIle
  let : Nontrivial S := Ideal.Quotient.nontrivial_iff.mpr hIne
  let : IsLocalRing S :=
    IsLocalRing.of_surjective' (Ideal.Quotient.mk I)
      Ideal.Quotient.mk_surjective
  let : IsNoetherianRing S :=
    isNoetherianRing_of_surjective R S (Ideal.Quotient.mk I)
      Ideal.Quotient.mk_surjective
  have hregQ : IsRegular (QuotSMulTop p R)
      (ps.map (Ideal.Quotient.mk I)) :=
    ((isRegular_cons_iff' R p ps).mp hreg).2
  let e : QuotSMulTop p R ≃ₗ[S] S :=
    ((QuotSMulTop.equivQuotTensor p R).extendScalarsOfSurjective
      Ideal.Quotient.mk_surjective).trans
        ((TensorProduct.rid R S).extendScalarsOfSurjective
          Ideal.Quotient.mk_surjective)
  have hregS : IsRegular S (ps.map (Ideal.Quotient.mk I)) :=
    (e.isRegular_congr _).mp hregQ
  have hgenS : Ideal.ofList (ps.map (Ideal.Quotient.mk I)) =
      (maximalIdeal R).map (Ideal.Quotient.mk I) := by
    rw [← hgen, Ideal.map_ofList]
    simp [I]
  exact ⟨hregS, hgenS⟩

theorem regularSystem_quotientPrefix
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (xs ys : List R)
    (hreg : IsRegular R (xs ++ ys))
    (hgen : Ideal.ofList (xs ++ ys) = maximalIdeal R) :
    let I : Ideal R := Ideal.ofList xs
    let hI : I ≤ maximalIdeal R := by
      calc
        I ≤ Ideal.ofList (xs ++ ys) := by
          rw [Ideal.ofList_append]
          exact le_sup_left
        _ = maximalIdeal R := hgen
    let S := R ⧸ I
    letI : Nontrivial S :=
      Ideal.Quotient.nontrivial_iff.mpr
        (ne_top_of_le_ne_top (maximalIdeal.isMaximal R).ne_top hI)
    letI : IsLocalRing S :=
      IsLocalRing.of_surjective' (Ideal.Quotient.mk I)
        Ideal.Quotient.mk_surjective
    IsRegular S (ys.map (Ideal.Quotient.mk I)) ∧
      Ideal.ofList (ys.map (Ideal.Quotient.mk I)) = maximalIdeal S := by
  dsimp only
  let I : Ideal R := Ideal.ofList xs
  have hI : I ≤ maximalIdeal R := by
    calc
      I ≤ Ideal.ofList (xs ++ ys) := by
        rw [Ideal.ofList_append]
        exact le_sup_left
      _ = maximalIdeal R := hgen
  let S := R ⧸ I
  let q : R →+* S := Ideal.Quotient.mk I
  have hIne : I ≠ ⊤ :=
    ne_top_of_le_ne_top (maximalIdeal.isMaximal R).ne_top hI
  let : Nontrivial S := Ideal.Quotient.nontrivial_iff.mpr hIne
  let : IsLocalRing S :=
    IsLocalRing.of_surjective' q Ideal.Quotient.mk_surjective
  let : IsNoetherianRing S :=
    isNoetherianRing_of_surjective R S q Ideal.Quotient.mk_surjective
  have hweakQuotient :=
    ((isWeaklyRegular_append_iff' R xs ys).mp
      hreg.toIsWeaklyRegular).2
  have hsmulTop :
      Ideal.ofList xs • (⊤ : Ideal R) = I := by
    simp [I]
  let eAdd :
      (R ⧸ (Ideal.ofList xs • (⊤ : Ideal R))) ≃+ S :=
    (Submodule.quotEquivOfEq
      (Ideal.ofList xs • (⊤ : Ideal R)) I hsmulTop).toAddEquiv
  let e :
      (R ⧸ (Ideal.ofList xs • (⊤ : Ideal R))) ≃ₗ[S] S :=
    AddEquiv.toLinearEquiv (R := S) eAdd (by
      intro s z
      obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective s
      obtain ⟨a, rfl⟩ :=
        Submodule.mkQ_surjective
          (Ideal.ofList xs • (⊤ : Ideal R)) z
      rfl)
  have hweakS : IsWeaklyRegular S (ys.map q) := by
    exact (e.isWeaklyRegular_congr _).mp hweakQuotient
  have hgenMap :
      Ideal.ofList ((xs ++ ys).map q) =
        (maximalIdeal R).map q := by
    rw [← Ideal.map_ofList, hgen]
  have hmapXs : Ideal.ofList (xs.map q) = ⊥ := by
    rw [← Ideal.map_ofList]
    exact Ideal.map_quotient_self I
  have hgenS : Ideal.ofList (ys.map q) = maximalIdeal S := by
    calc
      Ideal.ofList (ys.map q) =
          Ideal.ofList (xs.map q) ⊔ Ideal.ofList (ys.map q) := by
        rw [hmapXs, bot_sup_eq]
      _ = Ideal.ofList ((xs ++ ys).map q) := by
        rw [List.map_append, Ideal.ofList_append]
      _ = (maximalIdeal R).map q := hgenMap
      _ = maximalIdeal S :=
        IsLocalRing.map_maximalIdeal_of_surjective
          q Ideal.Quotient.mk_surjective
  have hmem : ∀ r ∈ ys.map q, r ∈ maximalIdeal S := by
    intro r hr
    rw [← hgenS]
    exact Ideal.subset_span hr
  exact ⟨IsRegular.of_isWeaklyRegular_of_mem_maximalIdeal
      (L := S) hmem hweakS, hgenS⟩

theorem isDomain_of_regularSystem
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (ps : List R) (hreg : IsRegular R ps)
    (hgen : Ideal.ofList ps = maximalIdeal R) : IsDomain R

theorem isRegularLocalRing_of_regularSystem
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (ps : List R) (hreg : IsRegular R ps)
    (hgen : Ideal.ofList ps = maximalIdeal R) : IsRegularLocalRing R

theorem regularSystem_length_eq_ringKrullDim
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (ps : List R) (hreg : IsRegular R ps)
    (hgen : Ideal.ofList ps = maximalIdeal R) :
    ((ps.length : ℕ∞) : WithBot ℕ∞) = ringKrullDim R

theorem quotientPrefix_geometry_of_regularSystem
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (xs ys : List R)
    (hreg : IsRegular R (xs ++ ys))
    (hgen : Ideal.ofList (xs ++ ys) = maximalIdeal R) :
    IsDomain (R ⧸ Ideal.ofList xs) ∧
      IsRegularLocalRing (R ⧸ Ideal.ofList xs)

theorem quotientPrefix_ringKrullDim_eq_length_of_regularSystem
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (xs ys : List R)
    (hreg : IsRegular R (xs ++ ys))
    (hgen : Ideal.ofList (xs ++ ys) = maximalIdeal R) :
    ringKrullDim (R ⧸ Ideal.ofList xs) =
      ((ys.length : ℕ∞) : WithBot ℕ∞)

theorem quotientPrefix_geometry_dimension_two_of_regularSystem
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (xs : List R) (y z : R)
    (hreg : IsRegular R (xs ++ [y, z]))
    (hgen : Ideal.ofList (xs ++ [y, z]) = maximalIdeal R) :
    IsDomain (R ⧸ Ideal.ofList xs) ∧
      IsRegularLocalRing (R ⧸ Ideal.ofList xs) ∧
      ringKrullDim (R ⧸ Ideal.ofList xs) =
        ((2 : ℕ∞) : WithBot ℕ∞)

theorem prime_of_mem_regularSystem
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    {ps : List R} (hreg : IsRegular R ps)
    (hgen : Ideal.ofList ps = maximalIdeal R)
    {p : R} (hp : p ∈ ps) : Prime p

theorem quotient_geometry_of_mem_regularSystem
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    {ps : List R} (hreg : IsRegular R ps)
    (hgen : Ideal.ofList ps = maximalIdeal R)
    {p : R} (hp : p ∈ ps) :
    IsDomain (R ⧸ Ideal.span {p}) ∧
      IsRegularLocalRing (R ⧸ Ideal.span {p})