Module

AdicCompletion_isNoetherianRing_of_isNoetherianRing.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.AdicCompletion_isNoetherianRing_of_isNoetherianRing

16 declarations indexed from sourceView source ↗

Module documentation

Adic Completion is Noetherian Ring of is Noetherian Ring

Imports8

Mathlib.RingTheory.AdicCompletion.Algebra
Mathlib.RingTheory.MvPowerSeries.Equiv
Mathlib.RingTheory.MvPolynomial.Ideal
Mathlib.Algebra.BigOperators.Group.Finset.Basic
Mathlib.RingTheory.Noetherian.Basic
Mathlib.Tactic.Choose
Mathlib.Tactic.SplitIfs
Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.MvPowerSeries_isNoetherianRing_of_finite

Imported by3

abbrev

XI

L40 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.AdicCompletion_isNoetherianRing_of_isNoetherianRing.AdicCompletionNoetherian.XI

Documentation

The ideal generated by the finitely many polynomial variables.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace AdicCompletion_isNoetherianRing_of_isNoetherianRing
universe u
namespace AdicCompletionNoetherian
open MvPolynomial MvPowerSeries
variable {R : Type*} [CommRing R] (I : Ideal R) {n : ℕ} (f : Fin n → R)

Lean source · statement

abbrev XI : Ideal (MvPolynomial (Fin n) R)

abbrev

ev

L43 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.AdicCompletion_isNoetherianRing_of_isNoetherianRing.AdicCompletionNoetherian.ev

Documentation

Evaluation at the chosen generators of the ideal.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace AdicCompletion_isNoetherianRing_of_isNoetherianRing
universe u
namespace AdicCompletionNoetherian
open MvPolynomial MvPowerSeries
variable {R : Type*} [CommRing R] (I : Ideal R) {n : ℕ} (f : Fin n → R)

Lean source · statement

abbrev ev : MvPolynomial (Fin n) R →+* R

lemma

ev_C

L45 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.AdicCompletion_isNoetherianRing_of_isNoetherianRing.AdicCompletionNoetherian.ev_C

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace AdicCompletion_isNoetherianRing_of_isNoetherianRing
universe u
namespace AdicCompletionNoetherian
open MvPolynomial MvPowerSeries
variable {R : Type*} [CommRing R] (I : Ideal R) {n : ℕ} (f : Fin n → R)

Lean source · statement

lemma ev_C (r : R) : ev f (C r) = r

lemma

ev_surjective

L47 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.AdicCompletion_isNoetherianRing_of_isNoetherianRing.AdicCompletionNoetherian.ev_surjective

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace AdicCompletion_isNoetherianRing_of_isNoetherianRing
universe u
namespace AdicCompletionNoetherian
open MvPolynomial MvPowerSeries
variable {R : Type*} [CommRing R] (I : Ideal R) {n : ℕ} (f : Fin n → R)

Lean source · statement

lemma ev_surjective : Function.Surjective (ev f)

lemma

map_XI_eq

L49 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.AdicCompletion_isNoetherianRing_of_isNoetherianRing.AdicCompletionNoetherian.map_XI_eq

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace AdicCompletion_isNoetherianRing_of_isNoetherianRing
universe u
namespace AdicCompletionNoetherian
open MvPolynomial MvPowerSeries
variable {R : Type*} [CommRing R] (I : Ideal R) {n : ℕ} (f : Fin n → R)

Lean source · statement

lemma map_XI_eq : Ideal.map (ev f) (XI) = Ideal.span (Set.range f)

lemma

XI_le_comap

L58 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.AdicCompletion_isNoetherianRing_of_isNoetherianRing.AdicCompletionNoetherian.XI_le_comap

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace AdicCompletion_isNoetherianRing_of_isNoetherianRing
universe u
namespace AdicCompletionNoetherian
open MvPolynomial MvPowerSeries
variable {R : Type*} [CommRing R] (I : Ideal R) {n : ℕ} (f : Fin n → R)
variable (hf : Ideal.span (Set.range f) = I)
include hf

Lean source · statement

lemma XI_le_comap : (XI : Ideal (MvPolynomial (Fin n) R)) ≤ I.comap (ev f)

lemma

XI_pow_le_comap

L61 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.AdicCompletion_isNoetherianRing_of_isNoetherianRing.AdicCompletionNoetherian.XI_pow_le_comap

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace AdicCompletion_isNoetherianRing_of_isNoetherianRing
universe u
namespace AdicCompletionNoetherian
open MvPolynomial MvPowerSeries
variable {R : Type*} [CommRing R] (I : Ideal R) {n : ℕ} (f : Fin n → R)
variable (hf : Ideal.span (Set.range f) = I)
include hf

Lean source · statement

lemma XI_pow_le_comap (k : ℕ) :
    (XI : Ideal (MvPolynomial (Fin n) R)) ^ k ≤ (I ^ k).comap (ev f)

lemma

map_XI_pow_eq

L65 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.AdicCompletion_isNoetherianRing_of_isNoetherianRing.AdicCompletionNoetherian.map_XI_pow_eq

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace AdicCompletion_isNoetherianRing_of_isNoetherianRing
universe u
namespace AdicCompletionNoetherian
open MvPolynomial MvPowerSeries
variable {R : Type*} [CommRing R] (I : Ideal R) {n : ℕ} (f : Fin n → R)
variable (hf : Ideal.span (Set.range f) = I)
include hf

Lean source · statement

lemma map_XI_pow_eq (k : ℕ) : Ideal.map (ev f) (XI ^ k) = I ^ k

def

phi

L70 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.AdicCompletion_isNoetherianRing_of_isNoetherianRing.AdicCompletionNoetherian.phi

Documentation

The map to an ideal-power quotient obtained by truncating a power series and evaluating its variables.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace AdicCompletion_isNoetherianRing_of_isNoetherianRing
universe u
namespace AdicCompletionNoetherian
open MvPolynomial MvPowerSeries
variable {R : Type*} [CommRing R] (I : Ideal R) {n : ℕ} (f : Fin n → R)
variable (hf : Ideal.span (Set.range f) = I)
include hf

Lean source · statement

def phi (k : ℕ) : MvPowerSeries (Fin n) R →+* R ⧸ I ^ k

lemma

phi_apply

L74 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.AdicCompletion_isNoetherianRing_of_isNoetherianRing.AdicCompletionNoetherian.phi_apply

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace AdicCompletion_isNoetherianRing_of_isNoetherianRing
universe u
namespace AdicCompletionNoetherian
open MvPolynomial MvPowerSeries
variable {R : Type*} [CommRing R] (I : Ideal R) {n : ℕ} (f : Fin n → R)
variable (hf : Ideal.span (Set.range f) = I)
include hf

Lean source · statement

lemma phi_apply (k : ℕ) (p : MvPowerSeries (Fin n) R) :
    phi I f hf k p = Ideal.Quotient.mk (I ^ k) (ev f (truncTotal k p))

lemma

phi_eq_of_sub_mem

L78 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.AdicCompletion_isNoetherianRing_of_isNoetherianRing.AdicCompletionNoetherian.phi_eq_of_sub_mem

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace AdicCompletion_isNoetherianRing_of_isNoetherianRing
universe u
namespace AdicCompletionNoetherian
open MvPolynomial MvPowerSeries
variable {R : Type*} [CommRing R] (I : Ideal R) {n : ℕ} (f : Fin n → R)
variable (hf : Ideal.span (Set.range f) = I)
include hf

Lean source · statement

lemma phi_eq_of_sub_mem (k : ℕ) (p : MvPowerSeries (Fin n) R) (P : MvPolynomial (Fin n) R)
    (h : truncTotal k p - P ∈ (XI : Ideal (MvPolynomial (Fin n) R)) ^ k) :
    phi I f hf k p = Ideal.Quotient.mk (I ^ k) (ev f P)

lemma

phi_compat

L84 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.AdicCompletion_isNoetherianRing_of_isNoetherianRing.AdicCompletionNoetherian.phi_compat

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace AdicCompletion_isNoetherianRing_of_isNoetherianRing
universe u
namespace AdicCompletionNoetherian
open MvPolynomial MvPowerSeries
variable {R : Type*} [CommRing R] (I : Ideal R) {n : ℕ} (f : Fin n → R)
variable (hf : Ideal.span (Set.range f) = I)
include hf

Lean source · statement

lemma phi_compat {k l : ℕ} (hkl : k ≤ l) :
    (Ideal.Quotient.factorPow I hkl).comp (phi I f hf l) = phi I f hf k

def

Phi

L95 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.AdicCompletion_isNoetherianRing_of_isNoetherianRing.AdicCompletionNoetherian.Phi

Documentation

The map from the power-series ring to the adic completion induced by the compatible truncations.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace AdicCompletion_isNoetherianRing_of_isNoetherianRing
universe u
namespace AdicCompletionNoetherian
open MvPolynomial MvPowerSeries
variable {R : Type*} [CommRing R] (I : Ideal R) {n : ℕ} (f : Fin n → R)
variable (hf : Ideal.span (Set.range f) = I)
include hf

Lean source · statement

def Phi : MvPowerSeries (Fin n) R →+* AdicCompletion I R

lemma

evalₐ_Phi

L98 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.AdicCompletion_isNoetherianRing_of_isNoetherianRing.AdicCompletionNoetherian.evalₐ_Phi

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace AdicCompletion_isNoetherianRing_of_isNoetherianRing
universe u
namespace AdicCompletionNoetherian
open MvPolynomial MvPowerSeries
variable {R : Type*} [CommRing R] (I : Ideal R) {n : ℕ} (f : Fin n → R)
variable (hf : Ideal.span (Set.range f) = I)
include hf

Lean source · statement

lemma evalₐ_Phi (k : ℕ) (p : MvPowerSeries (Fin n) R) :
    AdicCompletion.evalₐ I k (Phi I f hf p) = phi I f hf k p

lemma

Phi_surjective

L102 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.AdicCompletion_isNoetherianRing_of_isNoetherianRing.AdicCompletionNoetherian.Phi_surjective

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace AdicCompletion_isNoetherianRing_of_isNoetherianRing
universe u
namespace AdicCompletionNoetherian
open MvPolynomial MvPowerSeries
variable {R : Type*} [CommRing R] (I : Ideal R) {n : ℕ} (f : Fin n → R)
variable (hf : Ideal.span (Set.range f) = I)
include hf

Lean source · statement

lemma Phi_surjective : Function.Surjective (Phi I f hf)

theorem

isNoetherianRing_of_isNoetherianRing

L151 ↗

AdicCompletion.isNoetherianRing_of_isNoetherianRing

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace AdicCompletion_isNoetherianRing_of_isNoetherianRing
universe u

Lean source · statement

theorem _root_.AdicCompletion.isNoetherianRing_of_isNoetherianRing {R : Type u} [CommRing R]
    [IsNoetherianRing R] (I : Ideal R) : IsNoetherianRing (AdicCompletion I R)

Module documentation

Adic Completion is Noetherian Ring of is Noetherian Ring

Declarations