NYLL
Module

MvPowerSeries_isAdicComplete_maximalIdeal.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.MvPowerSeries_isAdicComplete_maximalIdeal
14 declarations indexed from sourceView source ↗

Module documentation

Mv Power Series is Adic Complete maximal Ideal

Imports3
  • Mathlib.RingTheory.MvPowerSeries.Inverse
  • Mathlib.RingTheory.AdicCompletion.Noetherian
  • Mathlib.RingTheory.MvPowerSeries.Trunc
Imported by1

Declarations

theorem

smodEq_pow_smul_top_iff

L34 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isAdicComplete_maximalIdeal.M4cP4PS.smodEq_pow_smul_top_iff
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace MvPowerSeries_isAdicComplete_maximalIdeal
universe u v w
namespace M4cP4PS
open MvPowerSeries IsLocalRing Finsupp
variable {σ : Type u} {R : Type v} [CommRing R]
Lean source · statement
theorem smodEq_pow_smul_top_iff (I : Ideal R) (n : ℕ) (x y : R) :
    x ≡ y [SMOD (I ^ n • ⊤ : Submodule R R)] ↔ x - y ∈ I ^ n
theorem

maximalIdeal_eq_comap

L38 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isAdicComplete_maximalIdeal.M4cP4PS.maximalIdeal_eq_comap
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace MvPowerSeries_isAdicComplete_maximalIdeal
universe u v w
namespace M4cP4PS
open MvPowerSeries IsLocalRing Finsupp
variable {σ : Type u} {R : Type v} [CommRing R]
Lean source · statement
theorem maximalIdeal_eq_comap [IsLocalRing R] :
    maximalIdeal (MvPowerSeries σ R) = (maximalIdeal R).comap (constantCoeff (σ := σ) (R := R))
def

dropVar

L46 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isAdicComplete_maximalIdeal.M4cP4PS.dropVar
Documentation

Retain exactly the terms whose exponent in the chosen variable is zero.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace MvPowerSeries_isAdicComplete_maximalIdeal
universe u v w
namespace M4cP4PS
open MvPowerSeries IsLocalRing Finsupp
variable {σ : Type u} {R : Type v} [CommRing R]
Lean source · statement
def dropVar (i : σ) (φ : MvPowerSeries σ R) : MvPowerSeries σ R
theorem

coeff_dropVar

L49 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isAdicComplete_maximalIdeal.M4cP4PS.coeff_dropVar
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace MvPowerSeries_isAdicComplete_maximalIdeal
universe u v w
namespace M4cP4PS
open MvPowerSeries IsLocalRing Finsupp
variable {σ : Type u} {R : Type v} [CommRing R]
Lean source · full declaration
theorem coeff_dropVar (i : σ) (φ : MvPowerSeries σ R) (m : σ →₀ ℕ) :
    coeff m (dropVar i φ) = if m i = 0 then coeff m φ else 0 := rfl
theorem

mem_pow_span_X_of_coeff_eq_zero

L52 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isAdicComplete_maximalIdeal.M4cP4PS.mem_pow_span_X_of_coeff_eq_zero
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace MvPowerSeries_isAdicComplete_maximalIdeal
universe u v w
namespace M4cP4PS
open MvPowerSeries IsLocalRing Finsupp
variable {σ : Type u} {R : Type v} [CommRing R]
Lean source · statement
theorem mem_pow_span_X_of_coeff_eq_zero [Finite σ] (k : ℕ) (φ : MvPowerSeries σ R)
    (hφ : ∀ m : σ →₀ ℕ, m.degree < k → coeff m φ = 0) :
    φ ∈ Ideal.span (Set.range (X : σ → MvPowerSeries σ R)) ^ k
theorem

sub_truncTotal_mem_pow_span_X

L114 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isAdicComplete_maximalIdeal.M4cP4PS.sub_truncTotal_mem_pow_span_X
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace MvPowerSeries_isAdicComplete_maximalIdeal
universe u v w
namespace M4cP4PS
open MvPowerSeries IsLocalRing Finsupp
variable {σ : Type u} {R : Type v} [CommRing R]
Lean source · statement
theorem sub_truncTotal_mem_pow_span_X [Finite σ] (k : ℕ) (φ : MvPowerSeries σ R) :
    φ - (truncTotal k φ : MvPolynomial σ R) ∈ Ideal.span (Set.range (X : σ → MvPowerSeries σ R)) ^
      k
theorem

coeff_mem_pow_of_mem_pow

L127 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isAdicComplete_maximalIdeal.M4cP4PS.coeff_mem_pow_of_mem_pow
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace MvPowerSeries_isAdicComplete_maximalIdeal
universe u v w
namespace M4cP4PS
open MvPowerSeries IsLocalRing Finsupp
variable {σ : Type u} {R : Type v} [CommRing R]
section LocalCoeff
variable [IsLocalRing R]
local notation "𝔐" => maximalIdeal (MvPowerSeries σ R)
local notation "𝔪" => maximalIdeal R
Lean source · statement
theorem coeff_mem_pow_of_mem_pow (n : ℕ) (x : MvPowerSeries σ R) (hx : x ∈ 𝔐 ^ n) (m : σ →₀ ℕ) :
    coeff m x ∈ 𝔪 ^ (n - m.degree)
theorem

C_mem_pow

L161 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isAdicComplete_maximalIdeal.M4cP4PS.C_mem_pow
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace MvPowerSeries_isAdicComplete_maximalIdeal
universe u v w
namespace M4cP4PS
open MvPowerSeries IsLocalRing Finsupp
variable {σ : Type u} {R : Type v} [CommRing R]
section LocalCoeff
variable [IsLocalRing R]
local notation "𝔐" => maximalIdeal (MvPowerSeries σ R)
local notation "𝔪" => maximalIdeal R
Lean source · statement
theorem C_mem_pow (k : ℕ) (c : R) (hc : c ∈ 𝔪 ^ k) : (C c : MvPowerSeries σ R) ∈ 𝔐 ^ k
theorem

span_X_le

L171 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isAdicComplete_maximalIdeal.M4cP4PS.span_X_le
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace MvPowerSeries_isAdicComplete_maximalIdeal
universe u v w
namespace M4cP4PS
open MvPowerSeries IsLocalRing Finsupp
variable {σ : Type u} {R : Type v} [CommRing R]
section LocalCoeff
variable [IsLocalRing R]
local notation "𝔐" => maximalIdeal (MvPowerSeries σ R)
local notation "𝔪" => maximalIdeal R
Lean source · statement
theorem span_X_le : Ideal.span (Set.range (X : σ → MvPowerSeries σ R)) ≤ 𝔐
theorem

monomial_one_mem_pow

L179 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isAdicComplete_maximalIdeal.M4cP4PS.monomial_one_mem_pow
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace MvPowerSeries_isAdicComplete_maximalIdeal
universe u v w
namespace M4cP4PS
open MvPowerSeries IsLocalRing Finsupp
variable {σ : Type u} {R : Type v} [CommRing R]
section LocalCoeff
variable [IsLocalRing R]
local notation "𝔐" => maximalIdeal (MvPowerSeries σ R)
local notation "𝔪" => maximalIdeal R
variable [Finite σ]
Lean source · statement
theorem monomial_one_mem_pow (m : σ →₀ ℕ) : (monomial m (1 : R) : MvPowerSeries σ R) ∈ 𝔐 ^ m.degree
theorem

monomial_mem_pow

L188 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isAdicComplete_maximalIdeal.M4cP4PS.monomial_mem_pow
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace MvPowerSeries_isAdicComplete_maximalIdeal
universe u v w
namespace M4cP4PS
open MvPowerSeries IsLocalRing Finsupp
variable {σ : Type u} {R : Type v} [CommRing R]
section LocalCoeff
variable [IsLocalRing R]
local notation "𝔐" => maximalIdeal (MvPowerSeries σ R)
local notation "𝔪" => maximalIdeal R
variable [Finite σ]
Lean source · statement
theorem monomial_mem_pow (n : ℕ) (m : σ →₀ ℕ) (c : R) (hc : c ∈ 𝔪 ^ (n - m.degree)) :
    (monomial m c : MvPowerSeries σ R) ∈ 𝔐 ^ n
theorem

mem_pow_of_coeff_mem_pow

L198 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isAdicComplete_maximalIdeal.M4cP4PS.mem_pow_of_coeff_mem_pow
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace MvPowerSeries_isAdicComplete_maximalIdeal
universe u v w
namespace M4cP4PS
open MvPowerSeries IsLocalRing Finsupp
variable {σ : Type u} {R : Type v} [CommRing R]
section LocalCoeff
variable [IsLocalRing R]
local notation "𝔐" => maximalIdeal (MvPowerSeries σ R)
local notation "𝔪" => maximalIdeal R
variable [Finite σ]
Lean source · statement
theorem mem_pow_of_coeff_mem_pow (n : ℕ) (x : MvPowerSeries σ R)
    (hx : ∀ m : σ →₀ ℕ, m.degree < n → coeff m x ∈ 𝔪 ^ (n - m.degree)) : x ∈ 𝔐 ^ n
theorem

isAdicComplete_maximalIdeal

L213 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.MvPowerSeries_isAdicComplete_maximalIdeal.M4cP4PS.isAdicComplete_maximalIdeal
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace MvPowerSeries_isAdicComplete_maximalIdeal
universe u v w
namespace M4cP4PS
open MvPowerSeries IsLocalRing Finsupp
variable {σ : Type u} {R : Type v} [CommRing R]
section LocalCoeff
variable [IsLocalRing R]
local notation "𝔐" => maximalIdeal (MvPowerSeries σ R)
local notation "𝔪" => maximalIdeal R
variable [Finite σ]
Lean source · statement
theorem isAdicComplete_maximalIdeal [IsAdicComplete (maximalIdeal R) R] :
    IsAdicComplete 𝔐 (MvPowerSeries σ R)
theorem

isAdicComplete_maximalIdeal

L254 ↗
MvPowerSeries.isAdicComplete_maximalIdeal
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace MvPowerSeries_isAdicComplete_maximalIdeal
universe u v w
Lean source · statement
theorem _root_.MvPowerSeries.isAdicComplete_maximalIdeal {σ : Type u} {R : Type v} [Finite σ]
  [CommRing R]
    [IsLocalRing R] [IsAdicComplete (IsLocalRing.maximalIdeal R) R] :
    IsAdicComplete (IsLocalRing.maximalIdeal (MvPowerSeries σ R)) (MvPowerSeries σ R)

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