Module

IsLocalRing_isAdicComplete_map_maximalIdeal_quotient.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_isAdicComplete_map_maximalIdeal_quotient

4 declarations indexed from sourceView source ↗

Module documentation

Is Local Ring is Adic Complete map maximal Ideal quotient

Imports2

Mathlib.RingTheory.MvPowerSeries.Inverse
Mathlib.RingTheory.AdicCompletion.Noetherian

Imported by1

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.All

theorem

smodEq_pow_smul_top_iff

L35 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isAdicComplete_map_maximalIdeal_quotient.M4cP4PS.smodEq_pow_smul_top_iff

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isAdicComplete_map_maximalIdeal_quotient
universe u v w
namespace M4cP4PS
open IsLocalRing
section
variable {R : Type u} {S : Type v} [CommRing R] [CommRing S]

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

isAdicComplete_map_of_surjective

L39 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isAdicComplete_map_maximalIdeal_quotient.M4cP4PS.isAdicComplete_map_of_surjective

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isAdicComplete_map_maximalIdeal_quotient
universe u v w
namespace M4cP4PS
open IsLocalRing
section
variable {R : Type u} {S : Type v} [CommRing R] [CommRing S]

Lean source · statement

theorem isAdicComplete_map_of_surjective [IsNoetherianRing R] (I : Ideal R)
    [IsAdicComplete I R] (f : R →+* S)
    (hf : Function.Surjective f) : IsAdicComplete (I.map f) S

theorem

isAdicComplete_map_maximalIdeal_quotient

L87 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isAdicComplete_map_maximalIdeal_quotient.M4cP4PS.isAdicComplete_map_maximalIdeal_quotient

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isAdicComplete_map_maximalIdeal_quotient
universe u v w
namespace M4cP4PS
open IsLocalRing
section
variable {R : Type u} {S : Type v} [CommRing R] [CommRing S]

Lean source · statement

theorem isAdicComplete_map_maximalIdeal_quotient [IsLocalRing R] [IsNoetherianRing R]
    [IsAdicComplete (maximalIdeal R) R] (J : Ideal R) :
    IsAdicComplete ((maximalIdeal R).map (Ideal.Quotient.mk J)) (R ⧸ J)

theorem

isAdicComplete_map_maximalIdeal_quotient

L96 ↗

IsLocalRing.isAdicComplete_map_maximalIdeal_quotient

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isAdicComplete_map_maximalIdeal_quotient
universe u v w

Lean source · statement

theorem _root_.IsLocalRing.isAdicComplete_map_maximalIdeal_quotient {R : Type u} [CommRing R]
  [IsLocalRing R]
    [IsNoetherianRing R] [IsAdicComplete (IsLocalRing.maximalIdeal R) R] (J : Ideal R) :
    IsAdicComplete ((IsLocalRing.maximalIdeal R).map (Ideal.Quotient.mk J)) (R ⧸ J)

Module documentation

Is Local Ring is Adic Complete map maximal Ideal quotient

Declarations

smodEq_pow_smul_top_iff

isAdicComplete_map_of_surjective

isAdicComplete_map_maximalIdeal_quotient

isAdicComplete_map_maximalIdeal_quotient