NYLL
Module

MvPowerSeries_isNoetherianRing_of_finite.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.MvPowerSeries_isNoetherianRing_of_finite
12 declarations indexed from sourceView source ↗

Module documentation

Mv Power Series is Noetherian Ring of finite

Imports5
  • Mathlib.RingTheory.PowerSeries.Ideal
  • Mathlib.RingTheory.MvPowerSeries.Rename
  • Mathlib.Data.Finsupp.Option
  • Mathlib.RingTheory.MvPowerSeries.Inverse
  • Mathlib.RingTheory.AdicCompletion.Noetherian
Imported by2

Declarations

def

optFun

L42 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_of_finite.M4cP1PS.optFun
Documentation

Regroup a power series in an optional variable as a power series in one variable with multivariable power-series coefficients.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace MvPowerSeries_isNoetherianRing_of_finite
universe u v w
noncomputable section
namespace M4cP1PS
open Finsupp Finset
section Equiv
variable {σ : Type*} {R : Type*} [CommSemiring R]
Lean source · statement
def optFun (φ : MvPowerSeries (Option σ) R) : PowerSeries (MvPowerSeries σ R)
def

optInv

L47 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_of_finite.M4cP1PS.optInv
Documentation

Recover a power series in an optional variable from its coefficients as a power series in one variable.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace MvPowerSeries_isNoetherianRing_of_finite
universe u v w
noncomputable section
namespace M4cP1PS
open Finsupp Finset
section Equiv
variable {σ : Type*} {R : Type*} [CommSemiring R]
Lean source · statement
def optInv (ψ : PowerSeries (MvPowerSeries σ R)) : MvPowerSeries (Option σ) R
theorem

coeff_coeff_optFun

L50 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_of_finite.M4cP1PS.coeff_coeff_optFun
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace MvPowerSeries_isNoetherianRing_of_finite
universe u v w
noncomputable section
namespace M4cP1PS
open Finsupp Finset
section Equiv
variable {σ : Type*} {R : Type*} [CommSemiring R]
Lean source · statement
theorem coeff_coeff_optFun (φ : MvPowerSeries (Option σ) R) (n : ℕ) (d : σ →₀ ℕ) :
    MvPowerSeries.coeff d (PowerSeries.coeff n (optFun φ)) = MvPowerSeries.coeff (d.optionElim n) φ
theorem

coeff_optInv

L57 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_of_finite.M4cP1PS.coeff_optInv
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace MvPowerSeries_isNoetherianRing_of_finite
universe u v w
noncomputable section
namespace M4cP1PS
open Finsupp Finset
section Equiv
variable {σ : Type*} {R : Type*} [CommSemiring R]
Lean source · statement
theorem coeff_optInv (ψ : PowerSeries (MvPowerSeries σ R)) (m : Option σ →₀ ℕ) :
    MvPowerSeries.coeff m (optInv ψ) = MvPowerSeries.coeff m.some (PowerSeries.coeff (m none) ψ)
theorem

optInv_optFun

L61 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_of_finite.M4cP1PS.optInv_optFun
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace MvPowerSeries_isNoetherianRing_of_finite
universe u v w
noncomputable section
namespace M4cP1PS
open Finsupp Finset
section Equiv
variable {σ : Type*} {R : Type*} [CommSemiring R]
Lean source · statement
theorem optInv_optFun (φ : MvPowerSeries (Option σ) R) : optInv (optFun φ) = φ
theorem

optFun_optInv

L65 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_of_finite.M4cP1PS.optFun_optInv
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace MvPowerSeries_isNoetherianRing_of_finite
universe u v w
noncomputable section
namespace M4cP1PS
open Finsupp Finset
section Equiv
variable {σ : Type*} {R : Type*} [CommSemiring R]
Lean source · statement
theorem optFun_optInv (ψ : PowerSeries (MvPowerSeries σ R)) : optFun (optInv ψ) = ψ
theorem

optFun_add

L69 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_of_finite.M4cP1PS.optFun_add
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace MvPowerSeries_isNoetherianRing_of_finite
universe u v w
noncomputable section
namespace M4cP1PS
open Finsupp Finset
section Equiv
variable {σ : Type*} {R : Type*} [CommSemiring R]
Lean source · statement
theorem optFun_add (φ ψ : MvPowerSeries (Option σ) R) : optFun (φ + ψ) = optFun φ + optFun ψ
theorem

optFun_mul

L73 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_of_finite.M4cP1PS.optFun_mul
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace MvPowerSeries_isNoetherianRing_of_finite
universe u v w
noncomputable section
namespace M4cP1PS
open Finsupp Finset
section Equiv
variable {σ : Type*} {R : Type*} [CommSemiring R]
Lean source · statement
theorem optFun_mul (φ ψ : MvPowerSeries (Option σ) R) : optFun (φ * ψ) = optFun φ * optFun ψ
def

optRingEquiv

L97 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_of_finite.M4cP1PS.optRingEquiv
Documentation

The ring equivalence between power series in an optional variable and iterated power series.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace MvPowerSeries_isNoetherianRing_of_finite
universe u v w
noncomputable section
namespace M4cP1PS
open Finsupp Finset
section Equiv
variable {σ : Type*} {R : Type*} [CommSemiring R]
Lean source · full declaration
def optRingEquiv : MvPowerSeries (Option σ) R ≃+* PowerSeries (MvPowerSeries σ R) where
  toFun := optFun
  invFun := optInv
  left_inv := optInv_optFun
  right_inv := optFun_optInv
  map_mul' := optFun_mul
  map_add' := optFun_add
theorem

isNoetherianRing_fin

L111 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_of_finite.M4cP1PS.isNoetherianRing_fin
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace MvPowerSeries_isNoetherianRing_of_finite
universe u v w
noncomputable section
namespace M4cP1PS
open Finsupp Finset
section Noetherian
variable (R : Type*) [CommRing R] [IsNoetherianRing R]
Lean source · full declaration
theorem isNoetherianRing_fin : ∀ n : ℕ, IsNoetherianRing (MvPowerSeries (Fin n) R)
  | 0 => isNoetherianRing_of_surjective R _ MvPowerSeries.C MvPowerSeries.C_surjective
  | n + 1 => by
    have := isNoetherianRing_fin n
    exact isNoetherianRing_of_ringEquiv (PowerSeries (MvPowerSeries (Fin n) R))
      (optRingEquiv.symm.trans (MvPowerSeries.renameEquiv R (finSuccEquiv n).symm).toRingEquiv)
theorem

isNoetherianRing_of_finite

L118 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isNoetherianRing_of_finite.M4cP1PS.isNoetherianRing_of_finite
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace MvPowerSeries_isNoetherianRing_of_finite
universe u v w
noncomputable section
namespace M4cP1PS
open Finsupp Finset
section Noetherian
variable (R : Type*) [CommRing R] [IsNoetherianRing R]
Lean source · statement
theorem isNoetherianRing_of_finite (σ : Type*) [Finite σ] : IsNoetherianRing (MvPowerSeries σ R)
theorem

isNoetherianRing_of_finite

L131 ↗
MvPowerSeries.isNoetherianRing_of_finite
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace MvPowerSeries_isNoetherianRing_of_finite
universe u v w
Lean source · statement
theorem _root_.MvPowerSeries.isNoetherianRing_of_finite {σ : Type u} {R : Type v} [Finite σ]
  [CommRing R]
    [IsNoetherianRing R] : IsNoetherianRing (MvPowerSeries σ R)

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