Module

IsLocalRing_isAdicComplete_of_module_finite.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_isAdicComplete_of_module_finite

14 declarations indexed from sourceView source ↗

Module documentation

Is Local Ring is Adic Complete of module finite

Imports9

Mathlib.RingTheory.AdicCompletion.Functoriality
Mathlib.RingTheory.AdicCompletion.Exactness
Mathlib.RingTheory.AdicCompletion.Noetherian
Mathlib.RingTheory.Finiteness.Cardinality
Mathlib.RingTheory.LocalRing.Quotient
Mathlib.RingTheory.LocalRing.RingHom.Basic
Mathlib.RingTheory.Artinian.Module
Mathlib.RingTheory.Ideal.Over
Mathlib.RingTheory.MvPowerSeries.Inverse

Imported by2

theorem

smul_top_pow_le_of_le

L42 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isAdicComplete_of_module_finite.M4cP1X1.smul_top_pow_le_of_le

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isAdicComplete_of_module_finite
universe u v w
namespace M4cP1X1
open IsLocalRing
section Compare
variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M] {I J : Ideal R}

Lean source · statement

theorem smul_top_pow_le_of_le (hIJ : I ≤ J) (n : ℕ) :
    (I ^ n • ⊤ : Submodule R M) ≤ J ^ n • ⊤

theorem

smul_top_pow_mul_le_of_pow_le

L46 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isAdicComplete_of_module_finite.M4cP1X1.smul_top_pow_mul_le_of_pow_le

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isAdicComplete_of_module_finite
universe u v w
namespace M4cP1X1
open IsLocalRing
section Compare
variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M] {I J : Ideal R}

Lean source · statement

theorem smul_top_pow_mul_le_of_pow_le {N : ℕ} (hJI : J ^ N ≤ I) (n : ℕ) :
    (J ^ (N * n) • ⊤ : Submodule R M) ≤ I ^ n • ⊤

theorem

isHausdorff_of_le

L51 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isAdicComplete_of_module_finite.M4cP1X1.isHausdorff_of_le

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isAdicComplete_of_module_finite
universe u v w
namespace M4cP1X1
open IsLocalRing
section Compare
variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M] {I J : Ideal R}

Lean source · statement

theorem isHausdorff_of_le (hIJ : I ≤ J) [h : IsHausdorff J M] : IsHausdorff I M

theorem

isHausdorff_of_pow_le

L54 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isAdicComplete_of_module_finite.M4cP1X1.isHausdorff_of_pow_le

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isAdicComplete_of_module_finite
universe u v w
namespace M4cP1X1
open IsLocalRing
section Compare
variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M] {I J : Ideal R}

Lean source · statement

theorem isHausdorff_of_pow_le {N : ℕ} (hJI : J ^ N ≤ I) [h : IsHausdorff I M] :
    IsHausdorff J M

theorem

isPrecomplete_of_le_of_pow_le

L58 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isAdicComplete_of_module_finite.M4cP1X1.isPrecomplete_of_le_of_pow_le

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isAdicComplete_of_module_finite
universe u v w
namespace M4cP1X1
open IsLocalRing
section Compare
variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M] {I J : Ideal R}

Lean source · statement

theorem isPrecomplete_of_le_of_pow_le {N : ℕ} (hIJ : I ≤ J) (hJI : J ^ N ≤ I)
    [h : IsPrecomplete I M] : IsPrecomplete J M

theorem

isPrecomplete_of_pow_le_of_le

L69 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isAdicComplete_of_module_finite.M4cP1X1.isPrecomplete_of_pow_le_of_le

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isAdicComplete_of_module_finite
universe u v w
namespace M4cP1X1
open IsLocalRing
section Compare
variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M] {I J : Ideal R}

Lean source · statement

theorem isPrecomplete_of_pow_le_of_le {N : ℕ} (hIJ : I ≤ J) (hJI : J ^ N ≤ I)
    [h : IsPrecomplete J M] : IsPrecomplete I M

theorem

isAdicComplete_iff_of_le_of_pow_le

L80 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isAdicComplete_of_module_finite.M4cP1X1.isAdicComplete_iff_of_le_of_pow_le

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isAdicComplete_of_module_finite
universe u v w
namespace M4cP1X1
open IsLocalRing
section Compare
variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M] {I J : Ideal R}

Lean source · statement

theorem isAdicComplete_iff_of_le_of_pow_le {N : ℕ} (hIJ : I ≤ J) (hJI : J ^ N ≤ I) :
    IsAdicComplete I M ↔ IsAdicComplete J M

theorem

isPrecomplete_of_surjective

L101 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isAdicComplete_of_module_finite.M4cP1X1.isPrecomplete_of_surjective

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isAdicComplete_of_module_finite
universe u v w
namespace M4cP1X1
open IsLocalRing
section ModuleFinite
variable {R : Type*} [CommRing R] (I : Ideal R)
variable {M : Type*} [AddCommGroup M] [Module R M] {N : Type*} [AddCommGroup N] [Module R N]
open AdicCompletion

Lean source · statement

theorem isPrecomplete_of_surjective (f : M →ₗ[R] N) (hf : Function.Surjective f)
    [IsPrecomplete I M] : IsPrecomplete I N

theorem

isPrecomplete_pi

L109 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isAdicComplete_of_module_finite.M4cP1X1.isPrecomplete_pi

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isAdicComplete_of_module_finite
universe u v w
namespace M4cP1X1
open IsLocalRing
section ModuleFinite
variable {R : Type*} [CommRing R] (I : Ideal R)
variable {M : Type*} [AddCommGroup M] [Module R M] {N : Type*} [AddCommGroup N] [Module R N]
open AdicCompletion

Lean source · statement

theorem isPrecomplete_pi (ι : Type*) [Finite ι] [IsPrecomplete I R] :
    IsPrecomplete I (ι → R)

theorem

isPrecomplete_of_module_finite

L124 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isAdicComplete_of_module_finite.M4cP1X1.isPrecomplete_of_module_finite

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isAdicComplete_of_module_finite
universe u v w
namespace M4cP1X1
open IsLocalRing
section ModuleFinite
variable {R : Type*} [CommRing R] (I : Ideal R)
variable {M : Type*} [AddCommGroup M] [Module R M] {N : Type*} [AddCommGroup N] [Module R N]
open AdicCompletion

Lean source · statement

theorem isPrecomplete_of_module_finite [IsPrecomplete I R] [Module.Finite R M] :
    IsPrecomplete I M

theorem

isAdicComplete_of_module_finite

L130 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isAdicComplete_of_module_finite.M4cP1X1.isAdicComplete_of_module_finite

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isAdicComplete_of_module_finite
universe u v w
namespace M4cP1X1
open IsLocalRing
section ModuleFinite
variable {R : Type*} [CommRing R] (I : Ideal R)
variable {M : Type*} [AddCommGroup M] [Module R M] {N : Type*} [AddCommGroup N] [Module R N]
open AdicCompletion

Lean source · statement

theorem isAdicComplete_of_module_finite [IsNoetherianRing R] [IsAdicComplete I R]
    [Module.Finite R M] : IsAdicComplete I M

theorem

exists_maximalIdeal_pow_le_map

L143 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isAdicComplete_of_module_finite.M4cP1X1.exists_maximalIdeal_pow_le_map

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isAdicComplete_of_module_finite
universe u v w
namespace M4cP1X1
open IsLocalRing
section Local
variable {𝒪 : Type*} {T : Type*} [CommRing 𝒪] [IsLocalRing 𝒪] [CommRing T] [Algebra 𝒪 T]
  [Module.Finite 𝒪 T] [IsLocalRing T]

Lean source · statement

theorem exists_maximalIdeal_pow_le_map :
    ∃ N, maximalIdeal T ^ N ≤ (maximalIdeal 𝒪).map (algebraMap 𝒪 T)

theorem

isAdicComplete_maximalIdeal_of_module_finite

L152 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isAdicComplete_of_module_finite.M4cP1X1.isAdicComplete_maximalIdeal_of_module_finite

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isAdicComplete_of_module_finite
universe u v w
namespace M4cP1X1
open IsLocalRing
section Local
variable {𝒪 : Type*} {T : Type*} [CommRing 𝒪] [IsLocalRing 𝒪] [CommRing T] [Algebra 𝒪 T]
  [Module.Finite 𝒪 T] [IsLocalRing T]

Lean source · statement

theorem isAdicComplete_maximalIdeal_of_module_finite [IsNoetherianRing 𝒪]
    [IsAdicComplete (maximalIdeal 𝒪) 𝒪] [IsLocalHom (algebraMap 𝒪 T)] :
    IsAdicComplete (maximalIdeal T) T

theorem

isAdicComplete_of_module_finite

L165 ↗

IsLocalRing.isAdicComplete_of_module_finite

Source context 4 commands

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

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

Lean source · statement

theorem _root_.IsLocalRing.isAdicComplete_of_module_finite {𝒪 : Type u} {T : Type v} [CommRing 𝒪]
    [IsNoetherianRing 𝒪] [IsLocalRing 𝒪] [IsAdicComplete (IsLocalRing.maximalIdeal 𝒪) 𝒪]
    [CommRing T] [Algebra 𝒪 T] [Module.Finite 𝒪 T] [IsLocalRing T] [IsLocalHom (algebraMap 𝒪 T)] :
    IsAdicComplete (IsLocalRing.maximalIdeal T) T

Module documentation

Is Local Ring is Adic Complete of module finite

Declarations