NYLL
Module

MvPowerSeries_isNoetherianRing_fin.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.MvPowerSeries_isNoetherianRing_fin
39 declarations indexed from sourceView source ↗

Module documentation

Mv Power Series is Noetherian Ring fin

Imports24
  • Mathlib.Algebra.BigOperators.Group.Finset.Basic
  • Mathlib.Algebra.BigOperators.Group.Finset.Sigma
  • Mathlib.Algebra.Module.SpanRank
  • Mathlib.Data.Finsupp.Basic
  • Mathlib.Data.Finsupp.Antidiagonal
  • Mathlib.Data.Set.Card
  • Mathlib.RingTheory.MvPowerSeries.Basic
  • Mathlib.RingTheory.MvPowerSeries.Inverse
  • Mathlib.RingTheory.MvPowerSeries.Rename
  • Mathlib.RingTheory.PowerSeries.Basic
  • Mathlib.RingTheory.PowerSeries.Inverse
  • Mathlib.RingTheory.PowerSeries.Ideal
  • Mathlib.RingTheory.Ideal.Span
  • Mathlib.RingTheory.Ideal.Operations
  • Mathlib.RingTheory.Ideal.Maps
  • Mathlib.RingTheory.Ideal.Quotient.Defs
  • Mathlib.RingTheory.Ideal.Quotient.Operations
  • Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
  • Mathlib.RingTheory.Noetherian.Basic
  • Mathlib.RingTheory.KrullDimension.Basic
  • Mathlib.RingTheory.KrullDimension.Regular
  • Mathlib.RingTheory.RegularLocalRing.Defs
  • Mathlib.Tactic.Ext
  • Mathlib.Tactic.Ring.Basic
Imported by1

Declarations

theorem

sumElim_injective2

L59 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2MV.MvPowerSeries.Finsupp.sumElim_injective2
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
namespace W2MV
open MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
section IndexBijection
variable {α β : Type*}
Lean source · statement
theorem Finsupp.sumElim_injective2 :
    Function.Injective2 (Finsupp.sumElim : (α →₀ ℕ) → (β →₀ ℕ) → (α ⊕ β →₀ ℕ))
theorem

sumElim_eq_zero_iff

L68 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2MV.MvPowerSeries.Finsupp.sumElim_eq_zero_iff
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
namespace W2MV
open MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
section IndexBijection
variable {α β : Type*}
Lean source · statement
theorem Finsupp.sumElim_eq_zero_iff {a : α →₀ ℕ} {b : β →₀ ℕ} :
    a.sumElim b = 0 ↔ a = 0 ∧ b = 0
theorem

sumElim_eq_single_inl_iff

L77 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2MV.MvPowerSeries.Finsupp.sumElim_eq_single_inl_iff
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
namespace W2MV
open MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
section IndexBijection
variable {α β : Type*}
Lean source · statement
theorem Finsupp.sumElim_eq_single_inl_iff {a : α →₀ ℕ} {b : β →₀ ℕ} {s : α} {c : ℕ} :
    a.sumElim b = Finsupp.single (Sum.inl s) c ↔ a = Finsupp.single s c ∧ b = 0
theorem

sumElim_eq_single_inr_iff

L86 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2MV.MvPowerSeries.Finsupp.sumElim_eq_single_inr_iff
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
namespace W2MV
open MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
section IndexBijection
variable {α β : Type*}
Lean source · statement
theorem Finsupp.sumElim_eq_single_inr_iff {a : α →₀ ℕ} {b : β →₀ ℕ} {t : β} {c : ℕ} :
    a.sumElim b = Finsupp.single (Sum.inr t) c ↔ a = 0 ∧ b = Finsupp.single t c
def

sumToFun

L102 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2MV.MvPowerSeries.sumToFun
Documentation

Separate the variables of a power series indexed by a disjoint union.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
namespace W2MV
open MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
section SumRingEquiv
variable (α β : Type*) {R : Type*} [CommSemiring R]
Lean source · statement
def sumToFun (f : MvPowerSeries (α ⊕ β) R) : MvPowerSeries α (MvPowerSeries β R)
def

sumInvFun

L106 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2MV.MvPowerSeries.sumInvFun
Documentation

Combine the two sets of variables in an iterated power series.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
namespace W2MV
open MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
section SumRingEquiv
variable (α β : Type*) {R : Type*} [CommSemiring R]
Lean source · statement
def sumInvFun (g : MvPowerSeries α (MvPowerSeries β R)) : MvPowerSeries (α ⊕ β) R
theorem

coeff_sumToFun

L113 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2MV.MvPowerSeries.coeff_sumToFun
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
namespace W2MV
open MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
section SumRingEquiv
variable (α β : Type*) {R : Type*} [CommSemiring R]
variable {α β}
Lean source · statement
theorem coeff_sumToFun (f : MvPowerSeries (α ⊕ β) R) (a : α →₀ ℕ) (b : β →₀ ℕ) :
    coeff b (coeff a (sumToFun α β f)) = coeff (a.sumElim b) f
theorem

coeff_sumInvFun

L117 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2MV.MvPowerSeries.coeff_sumInvFun
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
namespace W2MV
open MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
section SumRingEquiv
variable (α β : Type*) {R : Type*} [CommSemiring R]
variable {α β}
Lean source · statement
theorem coeff_sumInvFun (g : MvPowerSeries α (MvPowerSeries β R)) (d : α ⊕ β →₀ ℕ) :
    coeff d (sumInvFun α β g) =
      coeff (d.comapDomain Sum.inr Sum.inr_injective.injOn)
        (coeff (d.comapDomain Sum.inl Sum.inl_injective.injOn) g)
theorem

coeff_mul_sumElim

L123 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2MV.MvPowerSeries.coeff_mul_sumElim
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
namespace W2MV
open MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
section SumRingEquiv
variable (α β : Type*) {R : Type*} [CommSemiring R]
variable {α β}
Lean source · statement
theorem coeff_mul_sumElim [DecidableEq α] [DecidableEq β]
    (f g : MvPowerSeries (α ⊕ β) R) (a : α →₀ ℕ) (b : β →₀ ℕ) :
    coeff (a.sumElim b) (f * g) =
      ∑ q ∈ antidiagonal a, ∑ r ∈ antidiagonal b,
        coeff (q.1.sumElim r.1) f * coeff (q.2.sumElim r.2) g
def

sumRingEquiv

L140 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2MV.MvPowerSeries.sumRingEquiv
Documentation

The ring equivalence separating variables indexed by a disjoint union.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
namespace W2MV
open MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
section SumRingEquiv
variable (α β : Type*) {R : Type*} [CommSemiring R]
variable {α β}
variable (α β) (R) in
Lean source · full declaration
def sumRingEquiv : MvPowerSeries (α ⊕ β) R ≃+* MvPowerSeries α (MvPowerSeries β R) where
  toFun := sumToFun α β
  invFun := sumInvFun α β
  left_inv f := by
    ext d
    rw [show coeff d (sumInvFun α β (sumToFun α β f)) =
        coeff ((d.comapDomain Sum.inl Sum.inl_injective.injOn).sumElim
          (d.comapDomain Sum.inr Sum.inr_injective.injOn)) f from rfl,
      Finsupp.comapDomain_sumElim_comapDomain]
  right_inv g := by
    ext a b
    rw [show coeff b (coeff a (sumToFun α β (sumInvFun α β g))) =
        coeff ((a.sumElim b).comapDomain Sum.inr Sum.inr_injective.injOn)
          (coeff ((a.sumElim b).comapDomain Sum.inl Sum.inl_injective.injOn) g) from rfl,
      Finsupp.comapDomain_inl_sumElim, Finsupp.comapDomain_inr_sumElim]
  map_add' f g := by
    ext a b
    simp only [map_add, coeff_sumToFun]
  map_mul' f g := by
    classical
    ext a b
    rw [coeff_sumToFun, coeff_mul_sumElim]
    rw [show coeff a (sumToFun α β f * sumToFun α β g) =
        ∑ q ∈ antidiagonal a, coeff q.1 (sumToFun α β f) * coeff q.2 (sumToFun α β g) from
      coeff_mul (φ := sumToFun α β f) (ψ := sumToFun α β g) (n := a), map_sum]
    refine Finset.sum_congr rfl fun q _ => ?_
    rw [show coeff b (coeff q.1 (sumToFun α β f) * coeff q.2 (sumToFun α β g)) =
        ∑ r ∈ antidiagonal b, coeff r.1 (coeff q.1 (sumToFun α β f)) *
          coeff r.2 (coeff q.2 (sumToFun α β g)) from coeff_mul ..]
    exact Finset.sum_congr rfl fun r _ => by rw [coeff_sumToFun, coeff_sumToFun]
theorem

coeff_sumRingEquiv

L171 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2MV.MvPowerSeries.coeff_sumRingEquiv
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
namespace W2MV
open MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
section SumRingEquiv
variable (α β : Type*) {R : Type*} [CommSemiring R]
variable {α β}
variable (α β) (R) in
Lean source · statement
theorem coeff_sumRingEquiv (f : MvPowerSeries (α ⊕ β) R) (a : α →₀ ℕ) (b : β →₀ ℕ) :
    coeff b (coeff a (sumRingEquiv α β R f)) = coeff (a.sumElim b) f
theorem

sumRingEquiv_X_inl

L175 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2MV.MvPowerSeries.sumRingEquiv_X_inl
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
namespace W2MV
open MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
section SumRingEquiv
variable (α β : Type*) {R : Type*} [CommSemiring R]
variable {α β}
variable (α β) (R) in
Lean source · statement
theorem sumRingEquiv_X_inl (s : α) :
    sumRingEquiv α β R (X (Sum.inl s)) = X s
theorem

sumRingEquiv_X_inr

L185 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2MV.MvPowerSeries.sumRingEquiv_X_inr
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
namespace W2MV
open MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
section SumRingEquiv
variable (α β : Type*) {R : Type*} [CommSemiring R]
variable {α β}
variable (α β) (R) in
Lean source · statement
theorem sumRingEquiv_X_inr (t : β) :
    sumRingEquiv α β R (X (Sum.inr t)) = C (X t)
theorem

sumRingEquiv_C

L194 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2MV.MvPowerSeries.sumRingEquiv_C
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
namespace W2MV
open MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
section SumRingEquiv
variable (α β : Type*) {R : Type*} [CommSemiring R]
variable {α β}
variable (α β) (R) in
Lean source · statement
theorem sumRingEquiv_C (r : R) :
    sumRingEquiv α β R (C r) = C (C r)
def

finSuccSumEquiv

L209 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2MV.MvPowerSeries.finSuccSumEquiv
Documentation

Separate the first finite index from the remaining indices.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
namespace W2MV
open MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
section FinSucc
variable {R : Type*} [CommSemiring R]
Lean source · full declaration
def finSuccSumEquiv (n : ℕ) : Fin (n + 1) ≃ Unit ⊕ Fin n where
  toFun := Fin.cases (Sum.inl ()) (fun i => Sum.inr i)
  invFun := Sum.elim (fun _ => 0) Fin.succ
  left_inv i := by
    induction i using Fin.cases <;> simp
  right_inv x := by
    rcases x with ⟨⟩ | i <;> simp
theorem

finSuccSumEquiv_zero

L217 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2MV.MvPowerSeries.finSuccSumEquiv_zero
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
namespace W2MV
open MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
section FinSucc
variable {R : Type*} [CommSemiring R]
Lean source · statement
theorem finSuccSumEquiv_zero (n : ℕ) : finSuccSumEquiv n 0 = Sum.inl ()
theorem

finSuccSumEquiv_succ

L219 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2MV.MvPowerSeries.finSuccSumEquiv_succ
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
namespace W2MV
open MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
section FinSucc
variable {R : Type*} [CommSemiring R]
Lean source · statement
theorem finSuccSumEquiv_succ (n : ℕ) (i : Fin n) :
    finSuccSumEquiv n i.succ = Sum.inr i
def

finSuccRingEquiv

L225 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2MV.MvPowerSeries.finSuccRingEquiv
Documentation

Express power series in finitely many variables as an iterated power series ring.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
namespace W2MV
open MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
section FinSucc
variable {R : Type*} [CommSemiring R]
variable (R) in
Lean source · statement
def finSuccRingEquiv (n : ℕ) :
    MvPowerSeries (Fin (n + 1)) R ≃+* PowerSeries (MvPowerSeries (Fin n) R)
theorem

finSuccRingEquiv_apply

L229 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2MV.MvPowerSeries.finSuccRingEquiv_apply
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
namespace W2MV
open MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
section FinSucc
variable {R : Type*} [CommSemiring R]
variable (R) in
Lean source · statement
theorem finSuccRingEquiv_apply (n : ℕ) (f : MvPowerSeries (Fin (n + 1)) R) :
    finSuccRingEquiv R n f =
      sumRingEquiv Unit (Fin n) R (rename (finSuccSumEquiv n) f)
theorem

finSuccRingEquiv_X_zero

L234 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2MV.MvPowerSeries.finSuccRingEquiv_X_zero
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
namespace W2MV
open MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
section FinSucc
variable {R : Type*} [CommSemiring R]
variable (R) in
Lean source · statement
theorem finSuccRingEquiv_X_zero (n : ℕ) :
    finSuccRingEquiv R n (X 0) = PowerSeries.X
theorem

finSuccRingEquiv_X_succ

L239 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2MV.MvPowerSeries.finSuccRingEquiv_X_succ
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
namespace W2MV
open MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
section FinSucc
variable {R : Type*} [CommSemiring R]
variable (R) in
Lean source · statement
theorem finSuccRingEquiv_X_succ (n : ℕ) (i : Fin n) :
    finSuccRingEquiv R n (X i.succ) = PowerSeries.C (X i)
theorem

finSuccRingEquiv_C

L244 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2MV.MvPowerSeries.finSuccRingEquiv_C
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
namespace W2MV
open MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
section FinSucc
variable {R : Type*} [CommSemiring R]
variable (R) in
Lean source · statement
theorem finSuccRingEquiv_C (n : ℕ) (r : R) :
    finSuccRingEquiv R n (C r) = PowerSeries.C (C r)
def

isEmptyRingEquiv

L256 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2MV.MvPowerSeries.isEmptyRingEquiv
Documentation

Power series with no variables form the coefficient ring.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
namespace W2MV
open MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
section IsEmpty
variable (σ : Type*) [IsEmpty σ] (R : Type*) [CommSemiring R]
Lean source · statement
def isEmptyRingEquiv : MvPowerSeries σ R ≃+* R
theorem

isEmptyRingEquiv_apply

L264 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2MV.MvPowerSeries.isEmptyRingEquiv_apply
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
namespace W2MV
open MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
section IsEmpty
variable (σ : Type*) [IsEmpty σ] (R : Type*) [CommSemiring R]
Lean source · statement
theorem isEmptyRingEquiv_apply (f : MvPowerSeries σ R) :
    isEmptyRingEquiv σ R f = constantCoeff f
theorem

isEmptyRingEquiv_symm_apply

L267 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2MV.MvPowerSeries.isEmptyRingEquiv_symm_apply
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
namespace W2MV
open MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
section IsEmpty
variable (σ : Type*) [IsEmpty σ] (R : Type*) [CommSemiring R]
Lean source · statement
theorem isEmptyRingEquiv_symm_apply (r : R) :
    (isEmptyRingEquiv σ R).symm r = C r
theorem

isNoetherianRing_fin

L274 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2MV.MvPowerSeries.isNoetherianRing_fin
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
namespace W2MV
open MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
section Noetherian
Lean source · statement
theorem isNoetherianRing_fin (R : Type*) [CommRing R] [IsNoetherianRing R] (n : ℕ) :
    IsNoetherianRing (MvPowerSeries (Fin n) R)
lemma

isSMulRegular_X

L300 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2PS.PowerSeries.isSMulRegular_X
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
open IsLocalRing PowerSeries RingTheory
open scoped Pointwise
universe u
namespace W2PS
namespace PowerSeries
variable {R : Type u} [CommRing R]
Lean source · statement
lemma isSMulRegular_X : IsSMulRegular R⟦X⟧ (X : R⟦X⟧)
lemma

ker_constantCoeff

L306 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2PS.PowerSeries.ker_constantCoeff
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
open IsLocalRing PowerSeries RingTheory
open scoped Pointwise
universe u
namespace W2PS
namespace PowerSeries
variable {R : Type u} [CommRing R]
Lean source · statement
lemma ker_constantCoeff : RingHom.ker (constantCoeff (R := R)) = Ideal.span {(X : R⟦X⟧)}
def

quotSpanXEquiv

L312 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2PS.PowerSeries.quotSpanXEquiv
Documentation

The ring equivalence evaluating a power series modulo its variable at its constant coefficient.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
open IsLocalRing PowerSeries RingTheory
open scoped Pointwise
universe u
namespace W2PS
namespace PowerSeries
variable {R : Type u} [CommRing R]
Lean source · statement
def quotSpanXEquiv : (R⟦X⟧ ⧸ Ideal.span {(X : R⟦X⟧)}) ≃+* R
lemma

quotSpanXEquiv_mk

L316 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2PS.PowerSeries.quotSpanXEquiv_mk
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
open IsLocalRing PowerSeries RingTheory
open scoped Pointwise
universe u
namespace W2PS
namespace PowerSeries
variable {R : Type u} [CommRing R]
Lean source · statement
lemma quotSpanXEquiv_mk (f : R⟦X⟧) :
    quotSpanXEquiv (Ideal.Quotient.mk _ f) = constantCoeff f
lemma

smul_top_eq_span_X

L321 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2PS.PowerSeries.smul_top_eq_span_X
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
open IsLocalRing PowerSeries RingTheory
open scoped Pointwise
universe u
namespace W2PS
namespace PowerSeries
variable {R : Type u} [CommRing R]
Lean source · statement
lemma smul_top_eq_span_X :
    (X : R⟦X⟧) • (⊤ : Ideal R⟦X⟧) = Ideal.span {(X : R⟦X⟧)}
lemma

mem_maximalIdeal_iff

L330 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2PS.PowerSeries.mem_maximalIdeal_iff
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
open IsLocalRing PowerSeries RingTheory
open scoped Pointwise
universe u
namespace W2PS
namespace PowerSeries
variable {R : Type u} [CommRing R]
section IsLocalRing
variable [IsLocalRing R]
Lean source · statement
lemma mem_maximalIdeal_iff {f : R⟦X⟧} :
    f ∈ maximalIdeal R⟦X⟧ ↔ constantCoeff f ∈ maximalIdeal R
lemma

X_mem_maximalIdeal

L335 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2PS.PowerSeries.X_mem_maximalIdeal
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
open IsLocalRing PowerSeries RingTheory
open scoped Pointwise
universe u
namespace W2PS
namespace PowerSeries
variable {R : Type u} [CommRing R]
section IsLocalRing
variable [IsLocalRing R]
Lean source · statement
lemma X_mem_maximalIdeal : (X : R⟦X⟧) ∈ maximalIdeal R⟦X⟧
lemma

C_mem_maximalIdeal

L339 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2PS.PowerSeries.C_mem_maximalIdeal
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
open IsLocalRing PowerSeries RingTheory
open scoped Pointwise
universe u
namespace W2PS
namespace PowerSeries
variable {R : Type u} [CommRing R]
section IsLocalRing
variable [IsLocalRing R]
Lean source · statement
lemma C_mem_maximalIdeal {r : R} (hr : r ∈ maximalIdeal R) :
    (C r : R⟦X⟧) ∈ maximalIdeal R⟦X⟧
lemma

ringKrullDim_powerSeries

L348 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2PS.PowerSeries.ringKrullDim_powerSeries
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
open IsLocalRing PowerSeries RingTheory
open scoped Pointwise
universe u
namespace W2PS
namespace PowerSeries
variable {R : Type u} [CommRing R]
section KrullDim
variable (R) [IsNoetherianRing R] [IsLocalRing R]
Lean source · statement
lemma ringKrullDim_powerSeries : ringKrullDim R⟦X⟧ = ringKrullDim R + 1
theorem

maximalIdeal_eq_span_image_union_X

L359 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2PS.PowerSeries.maximalIdeal_eq_span_image_union_X
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
open IsLocalRing PowerSeries RingTheory
open scoped Pointwise
universe u
namespace W2PS
namespace PowerSeries
variable {R : Type u} [CommRing R]
section MaximalIdealSpan
variable [IsLocalRing R]
Lean source · statement
theorem maximalIdeal_eq_span_image_union_X {S : Set R} (hS : maximalIdeal R = Ideal.span S) :
    maximalIdeal R⟦X⟧ = Ideal.span ((C : R →+* R⟦X⟧) '' S ∪ {(X : R⟦X⟧)})
theorem

spanFinrank_maximalIdeal_le_succ

L381 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2PS.PowerSeries.spanFinrank_maximalIdeal_le_succ
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
open IsLocalRing PowerSeries RingTheory
open scoped Pointwise
universe u
namespace W2PS
namespace PowerSeries
variable {R : Type u} [CommRing R]
section MaximalIdealSpan
variable [IsLocalRing R]
Lean source · statement
theorem spanFinrank_maximalIdeal_le_succ [IsNoetherianRing R] :
    (maximalIdeal R⟦X⟧).spanFinrank ≤ (maximalIdeal R).spanFinrank + 1
theorem

isRegularLocalRing_powerSeries

L399 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin.W2PS.PowerSeries.isRegularLocalRing_powerSeries
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
open IsLocalRing PowerSeries RingTheory
open scoped Pointwise
universe u
namespace W2PS
namespace PowerSeries
variable {R : Type u} [CommRing R]
Lean source · statement
theorem isRegularLocalRing_powerSeries (R : Type u) [CommRing R] [IsRegularLocalRing R] :
    IsRegularLocalRing R⟦X⟧
theorem

isNoetherianRing_fin

L410 ↗
MvPowerSeries.isNoetherianRing_fin
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_fin
open IsLocalRing PowerSeries RingTheory
open scoped Pointwise
universe u
open IsLocalRing
Lean source · statement
theorem _root_.MvPowerSeries.isNoetherianRing_fin (R : Type*) [CommRing R] [IsNoetherianRing R] (n
  : ℕ) :
    IsNoetherianRing (MvPowerSeries (Fin n) R)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.