Hausdorff-ness for Noetherian rings

theorem IsHausdorff.of_le_jacobson {R : Type u} [CommRing R] (I : Ideal R) (M : Type u_1) [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] (h : I ≤ ⊥.jacobson) : IsHausdorff I M

theorem IsHausdorff.of_isLocalRing {R : Type u} [CommRing R] (I : Ideal R) (M : Type u_1) [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] [IsLocalRing R] (h : I ≠ ⊤) : IsHausdorff I M

instance instIsHausdorffMaximalIdeal {R : Type u} [CommRing R] (M : Type u_1) [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] [IsLocalRing R] : IsHausdorff (IsLocalRing.maximalIdeal R) M

theorem IsHausdorff.of_isTorsionFree {R : Type u} [CommRing R] (I : Ideal R) (M : Type u_1) [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] [IsDomain R] [Module.IsTorsionFree R M] (h : I ≠ ⊤) : IsHausdorff I M

theorem IsHausdorff.of_isDomain {R : Type u} [CommRing R] (I : Ideal R) [IsNoetherianRing R] [IsDomain R] (h : I ≠ ⊤) : IsHausdorff I R

@[instance 100]

instance instIsAdicCompleteMaximalIdealOfIsArtinianRing {A : Type u_1} [CommRing A] [IsArtinianRing A] [IsLocalRing A] : IsAdicComplete (IsLocalRing.maximalIdeal A) A

theorem tensorProduct_reesAlgebra_isNoetherian_of_fg {R : Type u} [CommRing R] (I : Ideal R) [IsNoetherianRing (R ⧸ I)] (fg : I.FG) : IsNoetherianRing (TensorProduct R (R ⧸ I) ↥(reesAlgebra I))

theorem reesAlgebra_quotient_isNoetherian {R : Type u} [CommRing R] (I : Ideal R) [IsNoetherianRing (R ⧸ I)] (fg : I.FG) : IsNoetherianRing (↥(reesAlgebra I) ⧸ Ideal.map (algebraMap R ↥(reesAlgebra I)) I)

theorem Polynomial.monomial_mem_reesAlgebra {R : Type u} [CommRing R] (I : Ideal R) (i : ℕ) {r : R} (mem : r ∈ I ^ i) : (monomial i) r ∈ reesAlgebra I

theorem mem_map_algebraMap_reesAlgebra_iff {R : Type u} [CommRing R] (I : Ideal R) (f : ↥(reesAlgebra I)) : f ∈ Ideal.map (algebraMap R ↥(reesAlgebra I)) I ↔ ∀ (n : ℕ), (↑f).coeff n ∈ I ^ (n + 1)

@[reducible, inline]

noncomputable abbrev reesAlgebraToAssociatedGraded {R : Type u} [CommRing R] (I : Ideal R) : ↥(reesAlgebra I) →+* ↥(reesAlgebra I) ⧸ Ideal.map (algebraMap R ↥(reesAlgebra I)) I

The canonical morphism from reesAlgebra to associated graded ring.

Equations

• reesAlgebraToAssociatedGraded I = Ideal.Quotient.mk (Ideal.map (algebraMap R ↥(reesAlgebra I)) I)

@[reducible, inline]

noncomputable abbrev Ideal.toAssociatedGraded {R : Type u} [CommRing R] (J I : Ideal R) : Ideal (↥(reesAlgebra I) ⧸ map (algebraMap R ↥(reesAlgebra I)) I)

The ideal ⨁ i, J ⊓ Iⁱ / J ⊓ Iⁱ⁺¹ corresponding to an ideal J of R.

Equations

• J.toAssociatedGraded I = Ideal.map (reesAlgebraToAssociatedGraded I) (Ideal.comap (reesAlgebra I).val (Ideal.map Polynomial.C J))

theorem exists_monomial_span_of_fg {R : Type u} [CommRing R] (I J : Ideal R) (fg : (J.toAssociatedGraded I).FG) : ∃ (ι : Type u) (f : ι → ↥(reesAlgebra I)) (deg : ι → ℕ) (coeff : ι → R), Finite ι ∧ (∀ (i : ι), ↑(f i) = (Polynomial.monomial (deg i)) (coeff i)) ∧ (∀ (i : ι), coeff i ∈ J) ∧ Ideal.map (reesAlgebraToAssociatedGraded I) (Ideal.span (Set.range f)) = J.toAssociatedGraded I

theorem exists_coeffs_sub_mem {R : Type u} [CommRing R] (I : Ideal R) (n : ℕ) (J : Ideal R) (ι : Type u) [Fintype ι] (f : ι → ↥(reesAlgebra I)) (deg : ι → ℕ) (coeff : ι → R) (eq : ∀ (i : ι), ↑(f i) = (Polynomial.monomial (deg i)) (coeff i)) (span_eq : Ideal.map (reesAlgebraToAssociatedGraded I) (Ideal.span (Set.range f)) = J.toAssociatedGraded I) (r : R) (rmem_J : r ∈ J) (rmem_pow : r ∈ I ^ n) : ∃ (coeff' : ι → R), (∀ (i : ι), coeff' i ∈ I ^ (n - deg i)) ∧ (∀ (i : ι), deg i > n → coeff' i = 0) ∧ r - ∑ x : ι, coeff' x * coeff x ∈ I ^ (n + 1)

theorem isNoetherianRing_of_isAdicComplete_of_fg {R : Type u} [CommRing R] (I : Ideal R) [IsNoetherianRing (R ⧸ I)] (fg : I.FG) (complete : IsAdicComplete I R) : IsNoetherianRing R

theorem AdicCompletion.isNoetherianRing_of_fg {R : Type u} [CommRing R] (I : Ideal R) [IsNoetherianRing (R ⧸ I)] (fg : I.FG) : IsNoetherianRing (AdicCompletion I R)

instance instIsNoetherianRingAdicCompletion {R : Type u} [CommRing R] (I : Ideal R) [IsNoetherianRing R] : IsNoetherianRing (AdicCompletion I R)

theorem AdicCompletion.ringKrullDim_eq {R : Type u} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] : ringKrullDim (AdicCompletion (IsLocalRing.maximalIdeal R) R) = ringKrullDim R