Module

AdicCompletionLocalRing.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.AdicCompletionLocalRing

27 declarations indexed from sourceView source ↗

Module documentation

Adic Completion Local Ring

Imports5

Mathlib.RingTheory.AdicCompletion.Completeness
Mathlib.RingTheory.AdicCompletion.LocalRing
Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.RingTheory.Noetherian.Defs

Imported by3

theorem

evalₐ_algebraMap

L33 ↗

AdicCompletion.evalₐ_algebraMap

Source context 5 commands

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

open IsLocalRing
namespace AdicCompletion
variable {A : Type*} [CommRing A]
section Kernel
variable (I : Ideal A)

Lean source · statement

theorem evalₐ_algebraMap (n : ℕ) (a : A) :
    evalₐ I n (algebraMap A (AdicCompletion I A) a) = Ideal.Quotient.mk _ a

theorem

mem_ker_evalₐ_iff

L37 ↗

AdicCompletion.mem_ker_evalₐ_iff

Source context 5 commands

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

open IsLocalRing
namespace AdicCompletion
variable {A : Type*} [CommRing A]
section Kernel
variable (I : Ideal A)

Lean source · statement

theorem mem_ker_evalₐ_iff (n : ℕ) (x : AdicCompletion I A) :
    x ∈ RingHom.ker (evalₐ I n) ↔ x ∈ LinearMap.ker (eval I A n)

theorem

ker_evalₐ_eq_map_pow

L45 ↗

AdicCompletion.ker_evalₐ_eq_map_pow

Source context 5 commands

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

open IsLocalRing
namespace AdicCompletion
variable {A : Type*} [CommRing A]
section Kernel
variable (I : Ideal A)

Lean source · statement

theorem ker_evalₐ_eq_map_pow (hI : I.FG) (n : ℕ) :
    RingHom.ker (evalₐ I n) = (I ^ n).map (algebraMap A (AdicCompletion I A))

theorem

exists_eq_algebraMap_add

L51 ↗

AdicCompletion.exists_eq_algebraMap_add

Source context 5 commands

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

open IsLocalRing
namespace AdicCompletion
variable {A : Type*} [CommRing A]
section Kernel
variable (I : Ideal A)

Lean source · statement

theorem exists_eq_algebraMap_add (hI : I.FG) (n : ℕ) (x : AdicCompletion I A) :
    ∃ a : A, ∃ y ∈ (I ^ n).map (algebraMap A (AdicCompletion I A)),
      x = algebraMap A (AdicCompletion I A) a + y

theorem

isUnit_one_add_of_mem_map

L58 ↗

AdicCompletion.isUnit_one_add_of_mem_map

Source context 5 commands

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

open IsLocalRing
namespace AdicCompletion
variable {A : Type*} [CommRing A]
section Kernel
variable (I : Ideal A)

Lean source · statement

theorem isUnit_one_add_of_mem_map (hI : I.FG) {x : AdicCompletion I A}
    (hx : x ∈ I.map (algebraMap A (AdicCompletion I A))) : IsUnit (1 + x)

theorem

isUnit_add_of_mem_map

L65 ↗

AdicCompletion.isUnit_add_of_mem_map

Source context 5 commands

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

open IsLocalRing
namespace AdicCompletion
variable {A : Type*} [CommRing A]
section Kernel
variable (I : Ideal A)

Lean source · statement

theorem isUnit_add_of_mem_map (hI : I.FG) {u x : AdicCompletion I A} (hu : IsUnit u)
    (hx : x ∈ I.map (algebraMap A (AdicCompletion I A))) : IsUnit (u + x)

theorem

isUnit_of_isUnit_algebraMap

L78 ↗

AdicCompletion.isUnit_of_isUnit_algebraMap

Source context 5 commands

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

open IsLocalRing
namespace AdicCompletion
variable {A : Type*} [CommRing A]
section Local
variable [IsLocalRing A]

Lean source · statement

theorem isUnit_of_isUnit_algebraMap {a : A}
    (h : IsUnit (algebraMap A (AdicCompletion (maximalIdeal A) A) a)) : IsUnit a

theorem

isUnit_one_add_of_mem_map_maximalIdeal

L88 ↗

AdicCompletion.isUnit_one_add_of_mem_map_maximalIdeal

Source context 5 commands

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

open IsLocalRing
namespace AdicCompletion
variable {A : Type*} [CommRing A]
section Local
variable [IsLocalRing A]

Lean source · statement

theorem isUnit_one_add_of_mem_map_maximalIdeal (h𝔪 : (maximalIdeal A).FG)
    {x : AdicCompletion (maximalIdeal A) A}
    (hx : x ∈ (maximalIdeal A).map (algebraMap A (AdicCompletion (maximalIdeal A) A))) :
    IsUnit (1 + x)

theorem

maximalIdeal_fg

L96 ↗

AdicCompletion.maximalIdeal_fg

Source context 6 commands

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

open IsLocalRing
namespace AdicCompletion
variable {A : Type*} [CommRing A]
section Local
variable [IsLocalRing A]
variable [IsNoetherianRing A]

Lean source · statement

theorem maximalIdeal_fg : (maximalIdeal A).FG

instance

instIsLocalRingMaximalIdeal

L98 ↗

AdicCompletion.instIsLocalRingMaximalIdeal

Source context 6 commands

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

open IsLocalRing
namespace AdicCompletion
variable {A : Type*} [CommRing A]
section Local
variable [IsLocalRing A]
variable [IsNoetherianRing A]

Lean source · statement

instance instIsLocalRingMaximalIdeal : IsLocalRing (AdicCompletion (maximalIdeal A) A)

theorem

maximalIdeal_pow_eq_ker_evalₐ

L101 ↗

AdicCompletion.maximalIdeal_pow_eq_ker_evalₐ

Source context 6 commands

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

open IsLocalRing
namespace AdicCompletion
variable {A : Type*} [CommRing A]
section Local
variable [IsLocalRing A]
variable [IsNoetherianRing A]

Lean source · statement

theorem maximalIdeal_pow_eq_ker_evalₐ (n : ℕ) :
    maximalIdeal (AdicCompletion (maximalIdeal A) A) ^ n = RingHom.ker (evalₐ (maximalIdeal A) n)

theorem

maximalIdeal_eq_ker_evalₐ_one

L106 ↗

AdicCompletion.maximalIdeal_eq_ker_evalₐ_one

Source context 6 commands

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

open IsLocalRing
namespace AdicCompletion
variable {A : Type*} [CommRing A]
section Local
variable [IsLocalRing A]
variable [IsNoetherianRing A]

Lean source · statement

theorem maximalIdeal_eq_ker_evalₐ_one :
    maximalIdeal (AdicCompletion (maximalIdeal A) A) = RingHom.ker (evalₐ (maximalIdeal A) 1)

theorem

mem_maximalIdeal_iff

L110 ↗

AdicCompletion.mem_maximalIdeal_iff

Source context 6 commands

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

open IsLocalRing
namespace AdicCompletion
variable {A : Type*} [CommRing A]
section Local
variable [IsLocalRing A]
variable [IsNoetherianRing A]

Lean source · statement

theorem mem_maximalIdeal_iff (x : AdicCompletion (maximalIdeal A) A) :
    x ∈ maximalIdeal (AdicCompletion (maximalIdeal A) A) ↔ evalₐ (maximalIdeal A) 1 x = 0

def

quotientMaximalIdealPowAlgHom

L120 ↗

AdicCompletion.quotientMaximalIdealPowAlgHom

Documentation

The map from the completion modulo a maximal-ideal power to the corresponding quotient of the ring.

Source context 8 commands

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

open IsLocalRing
namespace AdicCompletion
variable {A : Type*} [CommRing A]
section Local
variable [IsLocalRing A]
variable [IsNoetherianRing A]
section Scalars
variable (k : Type*) [CommRing k] [Algebra k A]

Lean source · statement

def quotientMaximalIdealPowAlgHom (n : ℕ) :
    (AdicCompletion (maximalIdeal A) A ⧸ maximalIdeal (AdicCompletion (maximalIdeal A) A) ^ n)
      →ₐ[k] A ⧸ maximalIdeal A ^ n

theorem

quotientMaximalIdealPowAlgHom_mk

L126 ↗

AdicCompletion.quotientMaximalIdealPowAlgHom_mk

Source context 8 commands

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

open IsLocalRing
namespace AdicCompletion
variable {A : Type*} [CommRing A]
section Local
variable [IsLocalRing A]
variable [IsNoetherianRing A]
section Scalars
variable (k : Type*) [CommRing k] [Algebra k A]

Lean source · statement

theorem quotientMaximalIdealPowAlgHom_mk (n : ℕ) (x : AdicCompletion (maximalIdeal A) A) :
    quotientMaximalIdealPowAlgHom k n (Ideal.Quotient.mk _ x) = evalₐ (maximalIdeal A) n x

theorem

quotientMaximalIdealPowAlgHom_bijective

L130 ↗

AdicCompletion.quotientMaximalIdealPowAlgHom_bijective

Source context 8 commands

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

open IsLocalRing
namespace AdicCompletion
variable {A : Type*} [CommRing A]
section Local
variable [IsLocalRing A]
variable [IsNoetherianRing A]
section Scalars
variable (k : Type*) [CommRing k] [Algebra k A]

Lean source · statement

theorem quotientMaximalIdealPowAlgHom_bijective (n : ℕ) :
    Function.Bijective (quotientMaximalIdealPowAlgHom (A := A) k n)

def

quotientMaximalIdealPowAlgEquiv

L145 ↗

AdicCompletion.quotientMaximalIdealPowAlgEquiv

Documentation

The equivalence between the completion and the original ring modulo the same maximal-ideal power.

Source context 8 commands

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

open IsLocalRing
namespace AdicCompletion
variable {A : Type*} [CommRing A]
section Local
variable [IsLocalRing A]
variable [IsNoetherianRing A]
section Scalars
variable (k : Type*) [CommRing k] [Algebra k A]

Lean source · statement

def quotientMaximalIdealPowAlgEquiv (n : ℕ) :
    (AdicCompletion (maximalIdeal A) A ⧸ maximalIdeal (AdicCompletion (maximalIdeal A) A) ^ n)
      ≃ₐ[k] A ⧸ maximalIdeal A ^ n

theorem

quotientMaximalIdealPowAlgEquiv_mk

L150 ↗

AdicCompletion.quotientMaximalIdealPowAlgEquiv_mk

Source context 8 commands

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

open IsLocalRing
namespace AdicCompletion
variable {A : Type*} [CommRing A]
section Local
variable [IsLocalRing A]
variable [IsNoetherianRing A]
section Scalars
variable (k : Type*) [CommRing k] [Algebra k A]

Lean source · statement

theorem quotientMaximalIdealPowAlgEquiv_mk (n : ℕ) (x : AdicCompletion (maximalIdeal A) A) :
    quotientMaximalIdealPowAlgEquiv k n (Ideal.Quotient.mk _ x) = evalₐ (maximalIdeal A) n x

theorem

quotientMaximalIdealPowAlgEquiv_mk_algebraMap

L154 ↗

AdicCompletion.quotientMaximalIdealPowAlgEquiv_mk_algebraMap

Source context 8 commands

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

open IsLocalRing
namespace AdicCompletion
variable {A : Type*} [CommRing A]
section Local
variable [IsLocalRing A]
variable [IsNoetherianRing A]
section Scalars
variable (k : Type*) [CommRing k] [Algebra k A]

Lean source · statement

theorem quotientMaximalIdealPowAlgEquiv_mk_algebraMap (n : ℕ) (a : A) :
    quotientMaximalIdealPowAlgEquiv k n (Ideal.Quotient.mk _ (algebraMap A _ a))
      = Ideal.Quotient.mk _ a

theorem

isUnit_algEquiv_iff

L171 ↗

AdicCompletion.isUnit_algEquiv_iff

Source context 8 commands

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

open IsLocalRing
namespace AdicCompletion
variable {A : Type*} [CommRing A]
section Transport
variable [IsLocalRing A] [IsNoetherianRing A]
variable {k : Type*} [CommRing k] [Algebra k A] {B : Type*} [CommRing B] [IsLocalRing B] [Algebra k
  B]
variable (Φ : AdicCompletion (maximalIdeal A) A ≃ₐ[k] B)
omit [IsNoetherianRing A] [IsLocalRing B] in

Lean source · statement

theorem isUnit_algEquiv_iff (x : AdicCompletion (maximalIdeal A) A) : IsUnit (Φ x) ↔ IsUnit x

theorem

comap_maximalIdeal_algEquiv

L174 ↗

AdicCompletion.comap_maximalIdeal_algEquiv

Source context 7 commands

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

open IsLocalRing
namespace AdicCompletion
variable {A : Type*} [CommRing A]
section Transport
variable [IsLocalRing A] [IsNoetherianRing A]
variable {k : Type*} [CommRing k] [Algebra k A] {B : Type*} [CommRing B] [IsLocalRing B] [Algebra k
  B]
variable (Φ : AdicCompletion (maximalIdeal A) A ≃ₐ[k] B)

Lean source · statement

theorem comap_maximalIdeal_algEquiv :
    (maximalIdeal B).comap (Φ : AdicCompletion (maximalIdeal A) A →+* B)
      = maximalIdeal (AdicCompletion (maximalIdeal A) A)

theorem

map_maximalIdeal_algEquiv

L181 ↗

AdicCompletion.map_maximalIdeal_algEquiv

Source context 7 commands

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

open IsLocalRing
namespace AdicCompletion
variable {A : Type*} [CommRing A]
section Transport
variable [IsLocalRing A] [IsNoetherianRing A]
variable {k : Type*} [CommRing k] [Algebra k A] {B : Type*} [CommRing B] [IsLocalRing B] [Algebra k
  B]
variable (Φ : AdicCompletion (maximalIdeal A) A ≃ₐ[k] B)

Lean source · statement

theorem map_maximalIdeal_algEquiv :
    (maximalIdeal (AdicCompletion (maximalIdeal A) A)).map
        (Φ : AdicCompletion (maximalIdeal A) A →+* B) = maximalIdeal B

theorem

maximalIdeal_eq_map_algEquiv

L187 ↗

AdicCompletion.maximalIdeal_eq_map_algEquiv

Source context 7 commands

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

open IsLocalRing
namespace AdicCompletion
variable {A : Type*} [CommRing A]
section Transport
variable [IsLocalRing A] [IsNoetherianRing A]
variable {k : Type*} [CommRing k] [Algebra k A] {B : Type*} [CommRing B] [IsLocalRing B] [Algebra k
  B]
variable (Φ : AdicCompletion (maximalIdeal A) A ≃ₐ[k] B)

Lean source · statement

theorem maximalIdeal_eq_map_algEquiv :
    maximalIdeal B = (maximalIdeal A).map
      ((Φ : AdicCompletion (maximalIdeal A) A →+* B).comp
        (algebraMap A (AdicCompletion (maximalIdeal A) A)))

theorem

maximalIdeal_pow_eq_map_algEquiv

L193 ↗

AdicCompletion.maximalIdeal_pow_eq_map_algEquiv

Source context 7 commands

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

open IsLocalRing
namespace AdicCompletion
variable {A : Type*} [CommRing A]
section Transport
variable [IsLocalRing A] [IsNoetherianRing A]
variable {k : Type*} [CommRing k] [Algebra k A] {B : Type*} [CommRing B] [IsLocalRing B] [Algebra k
  B]
variable (Φ : AdicCompletion (maximalIdeal A) A ≃ₐ[k] B)

Lean source · statement

theorem maximalIdeal_pow_eq_map_algEquiv (n : ℕ) :
    maximalIdeal B ^ n = (maximalIdeal A ^ n).map
      ((Φ : AdicCompletion (maximalIdeal A) A →+* B).comp
        (algebraMap A (AdicCompletion (maximalIdeal A) A)))

theorem

algEquiv_algebraMap_mem_maximalIdeal

L199 ↗

AdicCompletion.algEquiv_algebraMap_mem_maximalIdeal

Source context 7 commands

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

open IsLocalRing
namespace AdicCompletion
variable {A : Type*} [CommRing A]
section Transport
variable [IsLocalRing A] [IsNoetherianRing A]
variable {k : Type*} [CommRing k] [Algebra k A] {B : Type*} [CommRing B] [IsLocalRing B] [Algebra k
  B]
variable (Φ : AdicCompletion (maximalIdeal A) A ≃ₐ[k] B)

Lean source · statement

theorem algEquiv_algebraMap_mem_maximalIdeal {a : A} (ha : a ∈ maximalIdeal A) :
    Φ (algebraMap A _ a) ∈ maximalIdeal B

def

quotientMaximalIdealPowAlgEquivOfAlgEquiv

L206 ↗

AdicCompletion.quotientMaximalIdealPowAlgEquivOfAlgEquiv

Documentation

The quotient equivalence induced by an algebra equivalence with the maximal-ideal completion.

Source context 7 commands

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

open IsLocalRing
namespace AdicCompletion
variable {A : Type*} [CommRing A]
section Transport
variable [IsLocalRing A] [IsNoetherianRing A]
variable {k : Type*} [CommRing k] [Algebra k A] {B : Type*} [CommRing B] [IsLocalRing B] [Algebra k
  B]
variable (Φ : AdicCompletion (maximalIdeal A) A ≃ₐ[k] B)

Lean source · statement

def quotientMaximalIdealPowAlgEquivOfAlgEquiv (n : ℕ) :
    (B ⧸ maximalIdeal B ^ n) ≃ₐ[k] A ⧸ maximalIdeal A ^ n

theorem

quotientMaximalIdealPowAlgEquivOfAlgEquiv_mk

L213 ↗

AdicCompletion.quotientMaximalIdealPowAlgEquivOfAlgEquiv_mk

Source context 7 commands

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

open IsLocalRing
namespace AdicCompletion
variable {A : Type*} [CommRing A]
section Transport
variable [IsLocalRing A] [IsNoetherianRing A]
variable {k : Type*} [CommRing k] [Algebra k A] {B : Type*} [CommRing B] [IsLocalRing B] [Algebra k
  B]
variable (Φ : AdicCompletion (maximalIdeal A) A ≃ₐ[k] B)

Lean source · statement

theorem quotientMaximalIdealPowAlgEquivOfAlgEquiv_mk (n : ℕ) (a : A) :
    quotientMaximalIdealPowAlgEquivOfAlgEquiv Φ n (Ideal.Quotient.mk _ (Φ (algebraMap A _ a)))
      = Ideal.Quotient.mk _ a

Module documentation

Adic Completion Local Ring

Declarations