Module

IsAdicComplete_of_module_finite.lean

Nyll.AlgebraicCurves.Foundations.Algebra.IsAdicComplete_of_module_finite

14 declarations indexed from sourceView source ↗

Module documentation

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

L41 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.IsAdicComplete_of_module_finite.M4cP1X1.smul_top_pow_le_of_le

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.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

L45 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.IsAdicComplete_of_module_finite.M4cP1X1.smul_top_pow_mul_le_of_pow_le

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.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

L50 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.IsAdicComplete_of_module_finite.M4cP1X1.isHausdorff_of_le

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.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

L53 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.IsAdicComplete_of_module_finite.M4cP1X1.isHausdorff_of_pow_le

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.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

L57 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.IsAdicComplete_of_module_finite.M4cP1X1.isPrecomplete_of_le_of_pow_le

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.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

L68 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.IsAdicComplete_of_module_finite.M4cP1X1.isPrecomplete_of_pow_le_of_le

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.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

L79 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.IsAdicComplete_of_module_finite.M4cP1X1.isAdicComplete_iff_of_le_of_pow_le

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.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

L100 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.IsAdicComplete_of_module_finite.M4cP1X1.isPrecomplete_of_surjective

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.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

L108 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.IsAdicComplete_of_module_finite.M4cP1X1.isPrecomplete_pi

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.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

L123 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.IsAdicComplete_of_module_finite.M4cP1X1.isPrecomplete_of_module_finite

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.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

L129 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.IsAdicComplete_of_module_finite.M4cP1X1.isAdicComplete_of_module_finite

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.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

L142 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.IsAdicComplete_of_module_finite.M4cP1X1.exists_maximalIdeal_pow_le_map

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.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

L151 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.IsAdicComplete_of_module_finite.M4cP1X1.isAdicComplete_maximalIdeal_of_module_finite

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.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

of_module_finite

L164 ↗

IsAdicComplete.of_module_finite

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.IsAdicComplete_of_module_finite
universe u v w

Lean source · statement

theorem _root_.IsAdicComplete.of_module_finite {R : Type u} [CommRing R] [IsNoetherianRing R]
    (I : Ideal R) [IsAdicComplete I R] (M : Type v) [AddCommGroup M] [Module R M]
    [Module.Finite R M] : IsAdicComplete I M

Module documentation

Is Adic Complete of module finite

Declarations