NYLL
Module

LocalizationAtPrime.lean

Nyll.SchemeTheory.RingTheory.AdicCompletion.LocalizationAtPrime
18 declarations indexed from sourceView source ↗

Module documentation

Adic completion commutes with localization at a maximal ideal

For a maximal ideal Q of a commutative ring S, localization at Q identifies every finite quotient S ⧸ Q ^ n with the corresponding quotient of Localization.AtPrime Q by the n-th power of its maximal ideal. We prove that these finite-level equivalences commute with the power transition maps and lift them to an equivalence of adic completions.

Imports3
  • Mathlib.RingTheory.AdicCompletion.Algebra
  • Mathlib.RingTheory.Ideal.Quotient.Operations
  • Mathlib.RingTheory.Localization.AtPrime.Basic
Imported by2

Declarations

theorem

localizationAtPrimeQuotientPowEquiv_factorPow

L38 ↗
EtaleFundamentalGroups.localizationAtPrimeQuotientPowEquiv_factorPow
Documentation

The finite-level localization equivalences commute with the transition maps between powers of the maximal ideals.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uS
variable {S : Type uS} [CommRing S]
section AtPrime
variable (Q : Ideal S) [Q.IsMaximal]
local notation "S_Q" => Localization.AtPrime Q
local notation "m_Q" => IsLocalRing.maximalIdeal S_Q
Lean source · statement
theorem localizationAtPrimeQuotientPowEquiv_factorPow
    {m n : ℕ} (hmn : m ≤ n) (x : S ⧸ Q ^ n) :
    Ideal.Quotient.factorPow m_Q hmn
        (IsLocalization.AtPrime.equivQuotMaximalIdealPow Q S_Q n x) =
      IsLocalization.AtPrime.equivQuotMaximalIdealPow Q S_Q m
        (Ideal.Quotient.factorPow Q hmn x)
theorem

localizationAtPrimeQuotientPowEquiv_symm_factorPow

L57 ↗
EtaleFundamentalGroups.localizationAtPrimeQuotientPowEquiv_symm_factorPow
Documentation

Naturality of the inverse finite-level localization equivalences.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uS
variable {S : Type uS} [CommRing S]
section AtPrime
variable (Q : Ideal S) [Q.IsMaximal]
local notation "S_Q" => Localization.AtPrime Q
local notation "m_Q" => IsLocalRing.maximalIdeal S_Q
Lean source · statement
theorem localizationAtPrimeQuotientPowEquiv_symm_factorPow
    {m n : ℕ} (hmn : m ≤ n) (x : S_Q ⧸ m_Q ^ n) :
    Ideal.Quotient.factorPow Q hmn
        ((IsLocalization.AtPrime.equivQuotMaximalIdealPow Q S_Q n).symm x) =
      (IsLocalization.AtPrime.equivQuotMaximalIdealPow Q S_Q m).symm
        (Ideal.Quotient.factorPow m_Q hmn x)
theorem

factorPow_evalₐ

L69 ↗
EtaleFundamentalGroups.factorPow_evalₐ
Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uS
variable {S : Type uS} [CommRing S]
section AtPrime
variable (Q : Ideal S) [Q.IsMaximal]
local notation "S_Q" => Localization.AtPrime Q
local notation "m_Q" => IsLocalRing.maximalIdeal S_Q
Lean source · statement
theorem factorPow_evalₐ
    {R : Type*} [CommRing R] (I : Ideal R)
    {m n : ℕ} (hmn : m ≤ n) (x : AdicCompletion I R) :
    Ideal.Quotient.factorPow I hmn (AdicCompletion.evalₐ I n x) =
      AdicCompletion.evalₐ I m x
def

completionToAtPrimeQuotientRingHom

L98 ↗
EtaleFundamentalGroups.completionToAtPrimeQuotientRingHom
Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uS
variable {S : Type uS} [CommRing S]
section AtPrime
variable (Q : Ideal S) [Q.IsMaximal]
local notation "S_Q" => Localization.AtPrime Q
local notation "m_Q" => IsLocalRing.maximalIdeal S_Q
Lean source · statement
def completionToAtPrimeQuotientRingHom (n : ℕ) :
    AdicCompletion Q S →+* S_Q ⧸ m_Q ^ n
theorem

completionToAtPrimeQuotientRingHom_compatible

L103 ↗
EtaleFundamentalGroups.completionToAtPrimeQuotientRingHom_compatible
Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uS
variable {S : Type uS} [CommRing S]
section AtPrime
variable (Q : Ideal S) [Q.IsMaximal]
local notation "S_Q" => Localization.AtPrime Q
local notation "m_Q" => IsLocalRing.maximalIdeal S_Q
Lean source · statement
theorem completionToAtPrimeQuotientRingHom_compatible :
    ∀ {m n : ℕ} (hmn : m ≤ n),
      (Ideal.Quotient.factorPow m_Q hmn).comp
          (completionToAtPrimeQuotientRingHom Q n) =
        completionToAtPrimeQuotientRingHom Q m
def

completionToAtPrimeRingHom

L118 ↗
EtaleFundamentalGroups.completionToAtPrimeRingHom
Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uS
variable {S : Type uS} [CommRing S]
section AtPrime
variable (Q : Ideal S) [Q.IsMaximal]
local notation "S_Q" => Localization.AtPrime Q
local notation "m_Q" => IsLocalRing.maximalIdeal S_Q
Lean source · statement
def completionToAtPrimeRingHom :
    AdicCompletion Q S →+* AdicCompletion m_Q S_Q
theorem

evalₐ_completionToAtPrimeRingHom

L125 ↗
EtaleFundamentalGroups.evalₐ_completionToAtPrimeRingHom
Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uS
variable {S : Type uS} [CommRing S]
section AtPrime
variable (Q : Ideal S) [Q.IsMaximal]
local notation "S_Q" => Localization.AtPrime Q
local notation "m_Q" => IsLocalRing.maximalIdeal S_Q
Lean source · statement
theorem evalₐ_completionToAtPrimeRingHom
    (n : ℕ) (x : AdicCompletion Q S) :
    AdicCompletion.evalₐ m_Q n (completionToAtPrimeRingHom Q x) =
      IsLocalization.AtPrime.equivQuotMaximalIdealPow Q S_Q n
        (AdicCompletion.evalₐ Q n x)
def

atPrimeCompletionToQuotientRingHom

L134 ↗
EtaleFundamentalGroups.atPrimeCompletionToQuotientRingHom
Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uS
variable {S : Type uS} [CommRing S]
section AtPrime
variable (Q : Ideal S) [Q.IsMaximal]
local notation "S_Q" => Localization.AtPrime Q
local notation "m_Q" => IsLocalRing.maximalIdeal S_Q
Lean source · statement
def atPrimeCompletionToQuotientRingHom (n : ℕ) :
    AdicCompletion m_Q S_Q →+* S ⧸ Q ^ n
theorem

atPrimeCompletionToQuotientRingHom_compatible

L139 ↗
EtaleFundamentalGroups.atPrimeCompletionToQuotientRingHom_compatible
Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uS
variable {S : Type uS} [CommRing S]
section AtPrime
variable (Q : Ideal S) [Q.IsMaximal]
local notation "S_Q" => Localization.AtPrime Q
local notation "m_Q" => IsLocalRing.maximalIdeal S_Q
Lean source · statement
theorem atPrimeCompletionToQuotientRingHom_compatible :
    ∀ {m n : ℕ} (hmn : m ≤ n),
      (Ideal.Quotient.factorPow Q hmn).comp
          (atPrimeCompletionToQuotientRingHom Q n) =
        atPrimeCompletionToQuotientRingHom Q m
def

completionFromAtPrimeRingHom

L154 ↗
EtaleFundamentalGroups.completionFromAtPrimeRingHom
Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uS
variable {S : Type uS} [CommRing S]
section AtPrime
variable (Q : Ideal S) [Q.IsMaximal]
local notation "S_Q" => Localization.AtPrime Q
local notation "m_Q" => IsLocalRing.maximalIdeal S_Q
Lean source · statement
def completionFromAtPrimeRingHom :
    AdicCompletion m_Q S_Q →+* AdicCompletion Q S
theorem

evalₐ_completionFromAtPrimeRingHom

L161 ↗
EtaleFundamentalGroups.evalₐ_completionFromAtPrimeRingHom
Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uS
variable {S : Type uS} [CommRing S]
section AtPrime
variable (Q : Ideal S) [Q.IsMaximal]
local notation "S_Q" => Localization.AtPrime Q
local notation "m_Q" => IsLocalRing.maximalIdeal S_Q
Lean source · statement
theorem evalₐ_completionFromAtPrimeRingHom
    (n : ℕ) (x : AdicCompletion m_Q S_Q) :
    AdicCompletion.evalₐ Q n (completionFromAtPrimeRingHom Q x) =
      (IsLocalization.AtPrime.equivQuotMaximalIdealPow Q S_Q n).symm
        (AdicCompletion.evalₐ m_Q n x)
theorem

completionToAtPrime_comp_fromAtPrime

L170 ↗
EtaleFundamentalGroups.completionToAtPrime_comp_fromAtPrime
Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uS
variable {S : Type uS} [CommRing S]
section AtPrime
variable (Q : Ideal S) [Q.IsMaximal]
local notation "S_Q" => Localization.AtPrime Q
local notation "m_Q" => IsLocalRing.maximalIdeal S_Q
Lean source · statement
theorem completionToAtPrime_comp_fromAtPrime :
    (completionToAtPrimeRingHom Q).comp (completionFromAtPrimeRingHom Q) =
      RingHom.id (AdicCompletion m_Q S_Q)
theorem

completionFromAtPrime_comp_toAtPrime

L179 ↗
EtaleFundamentalGroups.completionFromAtPrime_comp_toAtPrime
Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uS
variable {S : Type uS} [CommRing S]
section AtPrime
variable (Q : Ideal S) [Q.IsMaximal]
local notation "S_Q" => Localization.AtPrime Q
local notation "m_Q" => IsLocalRing.maximalIdeal S_Q
Lean source · statement
theorem completionFromAtPrime_comp_toAtPrime :
    (completionFromAtPrimeRingHom Q).comp (completionToAtPrimeRingHom Q) =
      RingHom.id (AdicCompletion Q S)
def

adicCompletionLocalizationAtPrimeRingEquiv

L190 ↗
EtaleFundamentalGroups.adicCompletionLocalizationAtPrimeRingEquiv
Documentation

Completion at a maximal ideal is canonically equivalent, as a ring, to completion of its localization at the local maximal ideal.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uS
variable {S : Type uS} [CommRing S]
section AtPrime
variable (Q : Ideal S) [Q.IsMaximal]
local notation "S_Q" => Localization.AtPrime Q
local notation "m_Q" => IsLocalRing.maximalIdeal S_Q
Lean source · statement
def adicCompletionLocalizationAtPrimeRingEquiv :
    AdicCompletion Q S ≃+* AdicCompletion m_Q S_Q
theorem

evalₐ_adicCompletionLocalizationAtPrimeRingEquiv

L199 ↗
EtaleFundamentalGroups.evalₐ_adicCompletionLocalizationAtPrimeRingEquiv
Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uS
variable {S : Type uS} [CommRing S]
section AtPrime
variable (Q : Ideal S) [Q.IsMaximal]
local notation "S_Q" => Localization.AtPrime Q
local notation "m_Q" => IsLocalRing.maximalIdeal S_Q
Lean source · statement
theorem evalₐ_adicCompletionLocalizationAtPrimeRingEquiv
    (n : ℕ) (x : AdicCompletion Q S) :
    AdicCompletion.evalₐ m_Q n
        (adicCompletionLocalizationAtPrimeRingEquiv Q x) =
      IsLocalization.AtPrime.equivQuotMaximalIdealPow Q S_Q n
        (AdicCompletion.evalₐ Q n x)
theorem

evalₐ_adicCompletionLocalizationAtPrimeRingEquiv_symm

L208 ↗
EtaleFundamentalGroups.evalₐ_adicCompletionLocalizationAtPrimeRingEquiv_symm
Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uS
variable {S : Type uS} [CommRing S]
section AtPrime
variable (Q : Ideal S) [Q.IsMaximal]
local notation "S_Q" => Localization.AtPrime Q
local notation "m_Q" => IsLocalRing.maximalIdeal S_Q
Lean source · statement
theorem evalₐ_adicCompletionLocalizationAtPrimeRingEquiv_symm
    (n : ℕ) (x : AdicCompletion m_Q S_Q) :
    AdicCompletion.evalₐ Q n
        ((adicCompletionLocalizationAtPrimeRingEquiv Q).symm x) =
      (IsLocalization.AtPrime.equivQuotMaximalIdealPow Q S_Q n).symm
        (AdicCompletion.evalₐ m_Q n x)
def

adicCompletionLocalizationAtPrimeAlgEquiv

L218 ↗
EtaleFundamentalGroups.adicCompletionLocalizationAtPrimeAlgEquiv
Documentation

The canonical algebra equivalence over S: completion at Q agrees with completion of Localization.AtPrime Q at its maximal ideal.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uS
variable {S : Type uS} [CommRing S]
section AtPrime
variable (Q : Ideal S) [Q.IsMaximal]
local notation "S_Q" => Localization.AtPrime Q
local notation "m_Q" => IsLocalRing.maximalIdeal S_Q
Lean source · statement
def adicCompletionLocalizationAtPrimeAlgEquiv :
    AdicCompletion Q S ≃ₐ[S] AdicCompletion m_Q S_Q
theorem

evalₐ_adicCompletionLocalizationAtPrimeAlgEquiv

L227 ↗
EtaleFundamentalGroups.evalₐ_adicCompletionLocalizationAtPrimeAlgEquiv
Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uS
variable {S : Type uS} [CommRing S]
section AtPrime
variable (Q : Ideal S) [Q.IsMaximal]
local notation "S_Q" => Localization.AtPrime Q
local notation "m_Q" => IsLocalRing.maximalIdeal S_Q
Lean source · statement
theorem evalₐ_adicCompletionLocalizationAtPrimeAlgEquiv
    (n : ℕ) (x : AdicCompletion Q S) :
    AdicCompletion.evalₐ m_Q n
        (adicCompletionLocalizationAtPrimeAlgEquiv Q x) =
      IsLocalization.AtPrime.equivQuotMaximalIdealPow Q S_Q n
        (AdicCompletion.evalₐ Q n x)

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