Module

AdicCompletionInverseLimitRing.lean

Nyll.ValuedFieldTheory.Valuation.Topology.AdicCompletionInverseLimitRing

67 declarations indexed from sourceView source ↗

Module documentation

Adic completion and inverse limits

This file contains the algebraic and topological projective-limit descriptions of adically complete rings, complete discrete valuation rings, and their unit groups.

Imports6

Nyll.ValuedFieldTheory.Valuation.ValuedAdicComplete
Nyll.ValuedFieldTheory.Valuation.Topology.CompatibleInverseLimit
Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.Theory.Core
Nyll.ValuedFieldTheory.Valuation.Topology.Models
Mathlib.Algebra.Ring.TransferInstance
Mathlib.Topology.Homeomorph.TransferInstance

Imported by3

def

adicCompletion_coordinates_surjective

L62 ↗

LubinTate.Valuations.adicCompletion_coordinates_surjective

Documentation

The adic inverse-limit equivalence, projective-limit surjectivity in coordinates: every compatible adic-completion point is represented by a unique element of the original complete ring, and all finite coordinates agree with reduction modulo I ^ n.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

theorem adicCompletion_coordinates_surjective
    {R : Type*} [CommRing R] (I : Ideal R) [IsAdicComplete I R]
    (z : AdicCompletion I R) :
    ∃ x : R,
      adicCompletionAlgEquiv I x = z ∧
        ∀ n : ℕ,
          Ideal.Quotient.mk (I ^ n) x = AdicCompletion.evalₐ I n z

theorem

adicCompletion_coordinates_injective

L77 ↗

LubinTate.Valuations.adicCompletion_coordinates_injective

Documentation

The adic inverse-limit equivalence, uniqueness in coordinates: two elements with the same finite reductions modulo every I ^ n are equal.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

theorem adicCompletion_coordinates_injective
    {R : Type*} [CommRing R] (I : Ideal R) [IsAdicComplete I R]
    {x y : R}
    (h :
      ∀ n : ℕ,
        Ideal.Quotient.mk (I ^ n) x = Ideal.Quotient.mk (I ^ n) y) :
    x = y

structure

DiscreteAdicQuotient

L97 ↗

LubinTate.Valuations.DiscreteAdicQuotient

Documentation

A finite adic quotient with its discrete topology fixed in the type.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · full declaration

structure DiscreteAdicQuotient
    {R : Type*} [CommRing R] (I : Ideal R) (n : ℕ) where
  /-- The underlying residue class modulo `I ^ n`. -/
  val : R ⧸ I ^ n

def

equiv

L105 ↗

LubinTate.Valuations.DiscreteAdicQuotient.equiv

Documentation

Defines equiv.

Source context 8 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued
namespace DiscreteAdicQuotient

Lean source · full declaration

def equiv {R : Type*} [CommRing R] (I : Ideal R) (n : ℕ) :
    DiscreteAdicQuotient I n ≃ R ⧸ I ^ n where
  toFun := val
  invFun := fun x => ⟨x⟩
  left_inv := fun x => by cases x; rfl
  right_inv := fun _ => rfl

instance

(anonymous instance)

L113 ↗

Documentation

A discrete adic quotient inherits its commutative ring structure from the concrete quotient.

Source context 8 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued
namespace DiscreteAdicQuotient

Lean source · statement

instance {R : Type*} [CommRing R] (I : Ideal R) (n : ℕ) :
    CommRing (DiscreteAdicQuotient I n)

instance

(anonymous instance)

L118 ↗

Documentation

Each adic quotient is equipped with the discrete topology.

Source context 8 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued
namespace DiscreteAdicQuotient

Lean source · statement

instance {R : Type*} [CommRing R] (I : Ideal R) (n : ℕ) :
    TopologicalSpace (DiscreteAdicQuotient I n)

instance

(anonymous instance)

L122 ↗

Documentation

The selected topology on an adic quotient is discrete.

Source context 8 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued
namespace DiscreteAdicQuotient

Lean source · statement

instance {R : Type*} [CommRing R] (I : Ideal R) (n : ℕ) :
    DiscreteTopology (DiscreteAdicQuotient I n)

def

of

L127 ↗

LubinTate.Valuations.DiscreteAdicQuotient.of

Documentation

Defines of.

Source context 8 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued
namespace DiscreteAdicQuotient

Lean source · statement

def of {R : Type*} [CommRing R] (I : Ideal R) (n : ℕ)
    (x : R ⧸ I ^ n) : DiscreteAdicQuotient I n

theorem

val_of

L133 ↗

LubinTate.Valuations.DiscreteAdicQuotient.val_of

Documentation

Forgetting the discrete adic wrapper after insertion recovers the original quotient element.

Source context 8 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued
namespace DiscreteAdicQuotient

Lean source · statement

theorem val_of {R : Type*} [CommRing R] (I : Ideal R) (n : ℕ)
    (x : R ⧸ I ^ n) : (of I n x).val = x

def

homeomorph

L139 ↗

LubinTate.Valuations.DiscreteAdicQuotient.homeomorph

Documentation

The explicit boundary homeomorphism to the raw quotient equipped with the discrete topology.

Source context 8 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued
namespace DiscreteAdicQuotient

Lean source · statement

def homeomorph {R : Type*} [CommRing R] (I : Ideal R) (n : ℕ) :
    @Homeomorph (DiscreteAdicQuotient I n) (R ⧸ I ^ n)
      (inferInstance : TopologicalSpace (DiscreteAdicQuotient I n))
      (⊥ : TopologicalSpace (R ⧸ I ^ n))

theorem

homeomorph_apply

L152 ↗

LubinTate.Valuations.DiscreteAdicQuotient.homeomorph_apply

Documentation

The discrete adic homeomorphism evaluates as the underlying quotient equivalence.

Source context 8 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued
namespace DiscreteAdicQuotient

Lean source · statement

theorem homeomorph_apply {R : Type*} [CommRing R] (I : Ideal R) (n : ℕ)
    (x : DiscreteAdicQuotient I n) : homeomorph I n x = x.val

theorem

equiv_symm_apply

L158 ↗

LubinTate.Valuations.DiscreteAdicQuotient.equiv_symm_apply

Documentation

The inverse quotient equivalence inserts a concrete quotient into its discrete copy.

Source context 8 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued
namespace DiscreteAdicQuotient

Lean source · statement

theorem equiv_symm_apply {R : Type*} [CommRing R]
    (I : Ideal R) (n : ℕ) (x : R ⧸ I ^ n) :
    (equiv I n).symm x = of I n x

def

adicQuotientInverseLimit

L168 ↗

LubinTate.Valuations.adicQuotientInverseLimit

Documentation

The adic inverse-limit object lim_n R/I^n. This is an opaque public type; its compatible-family implementation is exposed only through the named equivalence and coordinate API below.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

def adicQuotientInverseLimit
    {R : Type*} [CommRing R] (I : Ideal R) : Type _

def

adicQuotientInverseLimitCompatibleFamiliesEquiv

L174 ↗

LubinTate.Valuations.adicQuotientInverseLimitCompatibleFamiliesEquiv

Documentation

The implementation representation of the all-level adic inverse limit.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · full declaration

def adicQuotientInverseLimitCompatibleFamiliesEquiv
    {R : Type*} [CommRing R] (I : Ideal R) :
    adicQuotientInverseLimit I ≃
      compatibleRingFamilies (fun n : ℕ => R ⧸ I ^ n)
        (fun {_ _} hmn => Ideal.Quotient.factorPow I hmn) := by
  unfold adicQuotientInverseLimit
  exact Equiv.refl _

instance

instCommRing

L183 ↗

LubinTate.Valuations.adicQuotientInverseLimit.instCommRing

Documentation

Compatible adic quotient families form a commutative ring coordinatewise.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

instance adicQuotientInverseLimit.instCommRing
    {R : Type*} [CommRing R] (I : Ideal R) :
    CommRing (adicQuotientInverseLimit I)

def

adicQuotientInverseLimitRepresentation

L190 ↗

LubinTate.Valuations.adicQuotientInverseLimitRepresentation

Documentation

The algebraic representation equivalence of the all-level adic inverse limit.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · full declaration

def adicQuotientInverseLimitRepresentation
    {R : Type*} [CommRing R] (I : Ideal R) :
    adicQuotientInverseLimit I ≃+*
      compatibleRingFamilies (fun n : ℕ => R ⧸ I ^ n)
        (fun {_ _} hmn => Ideal.Quotient.factorPow I hmn) :=
  (adicQuotientInverseLimitCompatibleFamiliesEquiv I).ringEquiv

def

adicQuotientInverseLimit_mk

L198 ↗

LubinTate.Valuations.adicQuotientInverseLimit_mk

Documentation

Build an all-level adic inverse-limit point from a compatible family.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

def adicQuotientInverseLimit_mk
    {R : Type*} [CommRing R] (I : Ideal R)
    (x : ∀ n : ℕ, R ⧸ I ^ n)
    (compatible : ∀ {m n : ℕ} (hmn : m ≤ n),
      Ideal.Quotient.factorPow I hmn (x n) = x m) :
    adicQuotientInverseLimit I

def

adicQuotientInverseLimit_eval

L208 ↗

LubinTate.Valuations.adicQuotientInverseLimit_eval

Documentation

Coordinate evaluation from the explicit projective limit.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · full declaration

def adicQuotientInverseLimit_eval
    {R : Type*} [CommRing R] (I : Ideal R) (n : ℕ) :
    adicQuotientInverseLimit I →+* R ⧸ I ^ n where
  toFun x := (adicQuotientInverseLimitCompatibleFamiliesEquiv I x).1 n
  map_one' := by rfl
  map_mul' _ _ := by rfl
  map_zero' := by rfl
  map_add' _ _ := by rfl

theorem

adicQuotientInverseLimit_eval_mk

L219 ↗

LubinTate.Valuations.adicQuotientInverseLimit_eval_mk

Documentation

Evaluation of an adic inverse-limit family returns its component at the selected level.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

theorem adicQuotientInverseLimit_eval_mk
    {R : Type*} [CommRing R] (I : Ideal R)
    (x : ∀ n : ℕ, R ⧸ I ^ n)
    (compatible : ∀ {m n : ℕ} (hmn : m ≤ n),
      Ideal.Quotient.factorPow I hmn (x n) = x m)
    (n : ℕ) :
    adicQuotientInverseLimit_eval I n
        (adicQuotientInverseLimit_mk I x compatible) = x n

theorem

adicQuotientInverseLimit_ext

L231 ↗

LubinTate.Valuations.adicQuotientInverseLimit_ext

Documentation

Adic inverse-limit elements are equal when all coordinate evaluations agree.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

theorem adicQuotientInverseLimit_ext
    {R : Type*} [CommRing R] (I : Ideal R)
    {x y : adicQuotientInverseLimit I}
    (h : ∀ n : ℕ, adicQuotientInverseLimit_eval I n x =
      adicQuotientInverseLimit_eval I n y) :
    x = y

theorem

adicQuotientInverseLimit_eval_factorPow

L244 ↗

LubinTate.Valuations.adicQuotientInverseLimit_eval_factorPow

Documentation

The explicit projective-limit coordinates are compatible with quotient transition maps.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

theorem adicQuotientInverseLimit_eval_factorPow
    {R : Type*} [CommRing R] (I : Ideal R)
    {m n : ℕ} (hmn : m ≤ n)
    (x : adicQuotientInverseLimit I) :
    Ideal.Quotient.factorPow I hmn
        (adicQuotientInverseLimit_eval I n x) =
      adicQuotientInverseLimit_eval I m x

instance

instTopologicalSpace

L256 ↗

LubinTate.Valuations.adicQuotientInverseLimit.instTopologicalSpace

Documentation

The canonical prodiscrete topology on the all-level inverse limit. The finite quotient stages are discrete inside this one representation boundary; their raw topology instances do not escape into public theorem statements.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

instance adicQuotientInverseLimit.instTopologicalSpace
    {R : Type*} [CommRing R] (I : Ideal R) :
    TopologicalSpace (adicQuotientInverseLimit I)

def

adicQuotientInverseLimitRepresentationHomeomorph

L262 ↗

LubinTate.Valuations.adicQuotientInverseLimitRepresentationHomeomorph

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · full declaration

def adicQuotientInverseLimitRepresentationHomeomorph
    {R : Type*} [CommRing R] (I : Ideal R) :
    letI : (n : ℕ) → TopologicalSpace (R ⧸ I ^ n) := fun _ => ⊥
    adicQuotientInverseLimit I ≃ₜ
      compatibleRingFamilies (fun n : ℕ => R ⧸ I ^ n)
        (fun {_ _} hmn => Ideal.Quotient.factorPow I hmn) := by
  letI : (n : ℕ) → TopologicalSpace (R ⧸ I ^ n) := fun _ => ⊥
  exact (adicQuotientInverseLimitCompatibleFamiliesEquiv I).homeomorph

def

adicQuotientInverseLimit_discreteEval

L273 ↗

LubinTate.Valuations.adicQuotientInverseLimit_discreteEval

Documentation

Coordinate evaluation into a type whose discreteness is recorded in the type itself.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

def adicQuotientInverseLimit_discreteEval
    {R : Type*} [CommRing R] (I : Ideal R) (n : ℕ) :
    adicQuotientInverseLimit I → DiscreteAdicQuotient I n

theorem

adicQuotientInverseLimit_discreteEval_continuous

L280 ↗

LubinTate.Valuations.adicQuotientInverseLimit_discreteEval_continuous

Documentation

Evaluation from the adic inverse limit to each discrete quotient is continuous.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

theorem adicQuotientInverseLimit_discreteEval_continuous
    {R : Type*} [CommRing R] (I : Ideal R) (n : ℕ) :
    Continuous (adicQuotientInverseLimit_discreteEval I n)

theorem

quotientEquivAlgOfEq_apply_symm

L298 ↗

LubinTate.Valuations.quotientEquivAlgOfEq_apply_symm

Documentation

The quotient algebra equivalence induced by equal ideals sends inverse representatives as expected.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

theorem quotientEquivAlgOfEq_apply_symm
    {R : Type*} [CommRing R] {I J : Ideal R}
    (h₁ h₂ : I = J) (y : R ⧸ J) :
    (Ideal.quotientEquivAlgOfEq R h₁)
      ((Ideal.quotientEquivAlgOfEq R h₂).symm y) = y

theorem

transitionMap_quotientEquivAlgOfEq

L313 ↗

LubinTate.Valuations.transitionMap_quotientEquivAlgOfEq

Documentation

Adic transition maps commute with quotient equivalences arising from equal powers.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

theorem transitionMap_quotientEquivAlgOfEq
    {R : Type*} [CommRing R] (I : Ideal R)
    {m n : ℕ} (hmn : m ≤ n)
    (hm : (I ^ m • ⊤ : Ideal R) = I ^ m)
    (hn : (I ^ n • ⊤ : Ideal R) = I ^ n)
    (y : R ⧸ I ^ n) :
    (Ideal.quotientEquivAlgOfEq R hm)
      (AdicCompletion.transitionMap I R hmn
        ((Ideal.quotientEquivAlgOfEq R hn).symm y)) =
      Ideal.Quotient.factorPow I hmn y

theorem

adicCompletion_eval_factorPow

L338 ↗

LubinTate.Valuations.adicCompletion_eval_factorPow

Documentation

The finite quotient coordinates of an adic-completion point are compatible under the transition maps.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

theorem adicCompletion_eval_factorPow
    {R : Type*} [CommRing R] (I : Ideal R)
    {m n : ℕ} (hmn : m ≤ n) (z : AdicCompletion I R) :
    Ideal.Quotient.factorPow I hmn (AdicCompletion.evalₐ I n z) =
      AdicCompletion.evalₐ I m z

def

adicCompletion_toQuotientInverseLimit

L349 ↗

LubinTate.Valuations.adicCompletion_toQuotientInverseLimit

Documentation

The map from the adic completion to the explicit projective limit lim_n R/I^n.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

def adicCompletion_toQuotientInverseLimit
    {R : Type*} [CommRing R] (I : Ideal R) :
    AdicCompletion I R → adicQuotientInverseLimit I

def

adicQuotientInverseLimit_toCompletion

L359 ↗

LubinTate.Valuations.adicQuotientInverseLimit_toCompletion

Documentation

The inverse map from the explicit projective limit lim_n R/I^n to the adic completion.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

def adicQuotientInverseLimit_toCompletion
    {R : Type*} [CommRing R] (I : Ideal R) :
    adicQuotientInverseLimit I → AdicCompletion I R

theorem

adicQuotientInverseLimit_toCompletion_eval

L378 ↗

LubinTate.Valuations.adicQuotientInverseLimit_toCompletion_eval

Documentation

The map from the adic inverse limit to the completion has the prescribed residue at every level.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

theorem adicQuotientInverseLimit_toCompletion_eval
    {R : Type*} [CommRing R] (I : Ideal R)
    (x : adicQuotientInverseLimit I) (n : ℕ) :
    AdicCompletion.evalₐ I n
        (adicQuotientInverseLimit_toCompletion I x) =
      adicQuotientInverseLimit_eval I n x

theorem

adicQuotientInverseLimit_left_inverse

L391 ↗

LubinTate.Valuations.adicQuotientInverseLimit_left_inverse

Documentation

Mapping an inverse-limit family to the completion and back recovers the family.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

theorem adicQuotientInverseLimit_left_inverse
    {R : Type*} [CommRing R] (I : Ideal R) (z : AdicCompletion I R) :
    adicQuotientInverseLimit_toCompletion I
        (adicCompletion_toQuotientInverseLimit I z) = z

theorem

adicQuotientInverseLimit_right_inverse

L401 ↗

LubinTate.Valuations.adicQuotientInverseLimit_right_inverse

Documentation

Mapping a completion element to its residue family and back recovers the element.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

theorem adicQuotientInverseLimit_right_inverse
    {R : Type*} [CommRing R] (I : Ideal R)
    (x : adicQuotientInverseLimit I) :
    adicCompletion_toQuotientInverseLimit I
        (adicQuotientInverseLimit_toCompletion I x) = x

def

adicCompletion_equiv_quotientInverseLimit

L414 ↗

LubinTate.Valuations.adicCompletion_equiv_quotientInverseLimit

Documentation

The adic inverse-limit equivalence, algebraic projective-limit form: the adic completion is canonically isomorphic to lim_n R/I^n.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · full declaration

def adicCompletion_equiv_quotientInverseLimit
    {R : Type*} [CommRing R] (I : Ideal R) :
    AdicCompletion I R ≃+* adicQuotientInverseLimit I where
  toFun := adicCompletion_toQuotientInverseLimit I
  invFun := adicQuotientInverseLimit_toCompletion I
  left_inv := adicQuotientInverseLimit_left_inverse I
  right_inv := adicQuotientInverseLimit_right_inverse I
  map_mul' x y := by
    ext n
    change AdicCompletion.evalₐ I n (x * y) =
      AdicCompletion.evalₐ I n x * AdicCompletion.evalₐ I n y
    simp
  map_add' x y := by
    ext n
    change AdicCompletion.evalₐ I n (x + y) =
      AdicCompletion.evalₐ I n x + AdicCompletion.evalₐ I n y
    simp

def

adicQuotientInverseLimit_canonicalMap

L434 ↗

LubinTate.Valuations.adicQuotientInverseLimit_canonicalMap

Documentation

The adic inverse-limit equivalence, canonical map from a ring to the explicit projective limit of its quotients.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · full declaration

def adicQuotientInverseLimit_canonicalMap
    {R : Type*} [CommRing R] (I : Ideal R) :
    R →+* adicQuotientInverseLimit I where
  toFun x := adicQuotientInverseLimit_mk I
    (fun n => Ideal.Quotient.mk (I ^ n) x)
    (fun _ => rfl)
  map_one' := by ext n; rfl
  map_mul' x y := by ext n; rfl
  map_zero' := by ext n; rfl
  map_add' x y := by ext n; rfl

def

adicQuotientInverseLimitEquiv

L447 ↗

LubinTate.Valuations.adicQuotientInverseLimitEquiv

Documentation

The adic inverse-limit equivalence, if R is complete for the I-adic topology, the canonical map R → lim_n R/I^n is a ring isomorphism.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

def adicQuotientInverseLimitEquiv
    {R : Type*} [CommRing R] (I : Ideal R) [IsAdicComplete I R] :
    R ≃+* adicQuotientInverseLimit I

theorem

adicQuotientInverseLimitEquiv_apply

L455 ↗

LubinTate.Valuations.adicQuotientInverseLimitEquiv_apply

Documentation

The complete-ring projective-limit isomorphism is induced by reduction modulo I^n in each coordinate.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

theorem adicQuotientInverseLimitEquiv_apply
    {R : Type*} [CommRing R] (I : Ideal R) [IsAdicComplete I R]
    (x : R) (n : ℕ) :
    adicQuotientInverseLimit_eval I n
        (adicQuotientInverseLimitEquiv I x) =
      Ideal.Quotient.mk (I ^ n) x

theorem

quotient_mk_continuous_adic_raw

L468 ↗

LubinTate.Valuations.quotient_mk_continuous_adic_raw

Documentation

Reduction modulo I^n is continuous from the I-adic topology to the discrete finite quotient topology.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

theorem quotient_mk_continuous_adic_raw
    {R : Type*} [CommRing R] (I : Ideal R) (n : ℕ) :
    @Continuous R (R ⧸ I ^ n) I.adicTopology
      (⊥ : TopologicalSpace (R ⧸ I ^ n))
      (Ideal.Quotient.mk (I ^ n))

theorem

quotient_mk_continuous_adic

L495 ↗

LubinTate.Valuations.quotient_mk_continuous_adic

Documentation

Reduction from the type-level adic ring to the named discrete quotient model is continuous.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · full declaration

theorem quotient_mk_continuous_adic
    {R : Type*} [CommRing R] (I : Ideal R) (n : ℕ) :
    Continuous fun x :
        WithTopology R I.adicTopology =>
      DiscreteAdicQuotient.of I n
        (Ideal.Quotient.mk (I ^ n) x.ofTopology) := by
  let : TopologicalSpace R := I.adicTopology
  let : TopologicalSpace (R ⧸ I ^ n) := ⊥
  let : DiscreteTopology (R ⧸ I ^ n) := ⟨rfl⟩
  have hraw := quotient_mk_continuous_adic_raw I n
  have hunderlying :
      Continuous fun x :
          WithTopology R I.adicTopology =>
        Ideal.Quotient.mk (I ^ n) x.ofTopology :=
    hraw.comp (WithTopology.continuous_ofTopology I.adicTopology)
  have hmodel :=
    (DiscreteAdicQuotient.homeomorph I n).symm.continuous.comp hunderlying
  convert hmodel using 1
  rfl

def

adicQuotientCompatibleFamiliesHomeomorph

L515 ↗

LubinTate.Valuations.adicQuotientCompatibleFamiliesHomeomorph

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · full declaration

def adicQuotientCompatibleFamiliesHomeomorph
    {R : Type*} [CommRing R] (I : Ideal R) [IsAdicComplete I R] :
    letI : TopologicalSpace R := I.adicTopology
    letI : (n : ℕ) → TopologicalSpace (R ⧸ I ^ n) := fun _ => ⊥
    R ≃ₜ compatibleRingFamilies (fun n : ℕ => R ⧸ I ^ n)
      (fun {_ _} hmn => Ideal.Quotient.factorPow I hmn) := by
  letI : TopologicalSpace R := I.adicTopology
  letI : (n : ℕ) → TopologicalSpace (R ⧸ I ^ n) := fun _ => ⊥
  letI : (n : ℕ) → DiscreteTopology (R ⧸ I ^ n) := fun _ => ⟨rfl⟩
  let e := (adicQuotientInverseLimitEquiv I).trans
    (adicQuotientInverseLimitRepresentation I)
  refine
    { toFun := e
      invFun := e.symm
      left_inv := e.left_inv
      right_inv := e.right_inv
      continuous_toFun := ?_
      continuous_invFun := ?_ }
  · exact Continuous.subtype_mk
      (continuous_pi fun n => by
        convert quotient_mk_continuous_adic_raw I n using 1
        funext x
        exact adicCompletion_eval_apply I n x)
      (fun x => by
        intro m n hmn
        exact adicCompletion_eval_factorPow I hmn
          ((adicCompletionAlgEquiv I) x))
  · rw [continuous_iff_continuousAt]
    intro q
    rw [ContinuousAt]
    rw [Filter.tendsto_def]
    intro s hs
    rcases (Ideal.hasBasis_nhds_adic I (e.symm q)).mem_iff.mp hs with
      ⟨n, _hn, hns⟩
    let cylinder : Set
        (compatibleRingFamilies (fun n : ℕ => R ⧸ I ^ n)
          (fun {_ _} hmn => Ideal.Quotient.factorPow I hmn)) :=
      {q' | q'.1 n = q.1 n}
    have hcont_coord :
        Continuous fun q' :
            compatibleRingFamilies (fun n : ℕ => R ⧸ I ^ n)
              (fun {_ _} hmn => Ideal.Quotient.factorPow I hmn) =>
          q'.1 n := by
      exact (continuous_apply n).comp continuous_subtype_val
    have hcyl_open : IsOpen cylinder := by
      exact (isOpen_discrete ({q.1 n} : Set (R ⧸ I ^ n))).preimage hcont_coord
    have hqmem : q ∈ cylinder := rfl
    exact mem_of_superset (hcyl_open.mem_nhds hqmem) (by
      intro q' hq'
      apply hns
      have hred' : Ideal.Quotient.mk (I ^ n) (e.symm q') = q'.1 n := by
        calc
          Ideal.Quotient.mk (I ^ n) (e.symm q') = (e (e.symm q')).1 n :=
            (adicQuotientInverseLimitEquiv_apply I (e.symm q') n).symm
          _ = q'.1 n := by
            simp [e.apply_symm_apply q']
      have hred : Ideal.Quotient.mk (I ^ n) (e.symm q) = q.1 n := by
        calc
          Ideal.Quotient.mk (I ^ n) (e.symm q) = (e (e.symm q)).1 n :=
            (adicQuotientInverseLimitEquiv_apply I (e.symm q) n).symm
          _ = q.1 n := by
            simp [e.apply_symm_apply q]
      have hmk : Ideal.Quotient.mk (I ^ n) (e.symm q') =
          Ideal.Quotient.mk (I ^ n) (e.symm q) := by
        rw [hred', hred, hq']
      have hmem : e.symm q' - e.symm q ∈ I ^ n := by
        exact (Ideal.Quotient.mk_eq_mk_iff_sub_mem
          (I := I ^ n) (x := e.symm q') (y := e.symm q)).1 hmk
      refine ⟨e.symm q' - e.symm q, hmem, ?_⟩
      ring)

def

adicQuotientInverseLimitHomeomorph

L588 ↗

LubinTate.Valuations.adicQuotientInverseLimitHomeomorph

Documentation

The canonical equivalence from an adically complete ring, represented by an adic type-level source and the opaque prodiscrete inverse-limit target.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

def adicQuotientInverseLimitHomeomorph
    {R : Type*} [CommRing R] (I : Ideal R) [IsAdicComplete I R] :
    WithTopology R I.adicTopology ≃ₜ
      adicQuotientInverseLimit I

def

adicPositiveQuotientInverseLimit

L602 ↗

LubinTate.Valuations.adicPositiveQuotientInverseLimit

Documentation

The opaque positive-indexed projective-limit object lim_n R/I^(n+1).

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

def adicPositiveQuotientInverseLimit
    {R : Type*} [CommRing R] (I : Ideal R) : Type _

def

adicPositiveQuotientInverseLimitCompatibleFamiliesEquiv

L609 ↗

LubinTate.Valuations.adicPositiveQuotientInverseLimitCompatibleFamiliesEquiv

Documentation

The implementation representation of the positive-indexed ring limit.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · full declaration

def adicPositiveQuotientInverseLimitCompatibleFamiliesEquiv
    {R : Type*} [CommRing R] (I : Ideal R) :
    adicPositiveQuotientInverseLimit I ≃
      compatibleRingFamilies (fun n : ℕ => R ⧸ I ^ (n + 1))
        (fun {_ _} hmn =>
          Ideal.Quotient.factorPow I (Nat.succ_le_succ hmn)) := by
  unfold adicPositiveQuotientInverseLimit
  exact Equiv.refl _

instance

instCommRing

L619 ↗

LubinTate.Valuations.adicPositiveQuotientInverseLimit.instCommRing

Documentation

Positive-level compatible adic quotient families form a commutative ring.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

instance adicPositiveQuotientInverseLimit.instCommRing
    {R : Type*} [CommRing R] (I : Ideal R) :
    CommRing (adicPositiveQuotientInverseLimit I)

def

adicPositiveQuotientInverseLimitRepresentation

L625 ↗

LubinTate.Valuations.adicPositiveQuotientInverseLimitRepresentation

Documentation

Defines adicPositiveQuotientInverseLimitRepresentation.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · full declaration

def adicPositiveQuotientInverseLimitRepresentation
    {R : Type*} [CommRing R] (I : Ideal R) :
    adicPositiveQuotientInverseLimit I ≃+*
      compatibleRingFamilies (fun n : ℕ => R ⧸ I ^ (n + 1))
        (fun {_ _} hmn =>
          Ideal.Quotient.factorPow I (Nat.succ_le_succ hmn)) :=
  (adicPositiveQuotientInverseLimitCompatibleFamiliesEquiv I).ringEquiv

def

adicPositiveQuotientInverseLimit_mk

L634 ↗

LubinTate.Valuations.adicPositiveQuotientInverseLimit_mk

Documentation

Defines adicPositiveQuotientInverseLimit_mk.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

def adicPositiveQuotientInverseLimit_mk
    {R : Type*} [CommRing R] (I : Ideal R)
    (x : ∀ n : ℕ, R ⧸ I ^ (n + 1))
    (compatible : ∀ {m n : ℕ} (hmn : m ≤ n),
      Ideal.Quotient.factorPow I (Nat.succ_le_succ hmn) (x n) = x m) :
    adicPositiveQuotientInverseLimit I

def

adicPositiveQuotientInverseLimit_eval

L644 ↗

LubinTate.Valuations.adicPositiveQuotientInverseLimit_eval

Documentation

Defines adicPositiveQuotientInverseLimit_eval.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · full declaration

def adicPositiveQuotientInverseLimit_eval
    {R : Type*} [CommRing R] (I : Ideal R) (n : ℕ) :
    adicPositiveQuotientInverseLimit I →+* R ⧸ I ^ (n + 1) where
  toFun x :=
    (adicPositiveQuotientInverseLimitCompatibleFamiliesEquiv I x).1 n
  map_one' := by rfl
  map_mul' _ _ := by rfl
  map_zero' := by rfl
  map_add' _ _ := by rfl

theorem

adicPositiveQuotientInverseLimit_eval_mk

L656 ↗

LubinTate.Valuations.adicPositiveQuotientInverseLimit_eval_mk

Documentation

Positive-level evaluation returns the selected adic quotient component.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

theorem adicPositiveQuotientInverseLimit_eval_mk
    {R : Type*} [CommRing R] (I : Ideal R)
    (x : ∀ n : ℕ, R ⧸ I ^ (n + 1))
    (compatible : ∀ {m n : ℕ} (hmn : m ≤ n),
      Ideal.Quotient.factorPow I (Nat.succ_le_succ hmn) (x n) = x m)
    (n : ℕ) :
    adicPositiveQuotientInverseLimit_eval I n
        (adicPositiveQuotientInverseLimit_mk I x compatible) = x n

theorem

adicPositiveQuotientInverseLimit_ext

L668 ↗

LubinTate.Valuations.adicPositiveQuotientInverseLimit_ext

Documentation

Positive adic inverse-limit elements are determined by all of their components.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

theorem adicPositiveQuotientInverseLimit_ext
    {R : Type*} [CommRing R] (I : Ideal R)
    {x y : adicPositiveQuotientInverseLimit I}
    (h : ∀ n : ℕ, adicPositiveQuotientInverseLimit_eval I n x =
      adicPositiveQuotientInverseLimit_eval I n y) :
    x = y

theorem

adicPositiveQuotientInverseLimit_eval_factorPow

L680 ↗

LubinTate.Valuations.adicPositiveQuotientInverseLimit_eval_factorPow

Documentation

Positive-level evaluation is compatible with the factor map between ideal powers.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

theorem adicPositiveQuotientInverseLimit_eval_factorPow
    {R : Type*} [CommRing R] (I : Ideal R)
    {m n : ℕ} (hmn : m ≤ n)
    (x : adicPositiveQuotientInverseLimit I) :
    Ideal.Quotient.factorPow I (Nat.succ_le_succ hmn)
        (adicPositiveQuotientInverseLimit_eval I n x) =
      adicPositiveQuotientInverseLimit_eval I m x

instance

instTopologicalSpace

L690 ↗

LubinTate.Valuations.adicPositiveQuotientInverseLimit.instTopologicalSpace

Documentation

The positive adic inverse limit carries the topology induced by its discrete coordinates.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

instance adicPositiveQuotientInverseLimit.instTopologicalSpace
    {R : Type*} [CommRing R] (I : Ideal R) :
    TopologicalSpace (adicPositiveQuotientInverseLimit I)

def

adicPositiveQuotientInverseLimitRepresentationHomeomorph

L697 ↗

LubinTate.Valuations.adicPositiveQuotientInverseLimitRepresentationHomeomorph

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · full declaration

def
    adicPositiveQuotientInverseLimitRepresentationHomeomorph
    {R : Type*} [CommRing R] (I : Ideal R) :
    letI : (n : ℕ) → TopologicalSpace (R ⧸ I ^ (n + 1)) := fun _ => ⊥
    adicPositiveQuotientInverseLimit I ≃ₜ
      compatibleRingFamilies (fun n : ℕ => R ⧸ I ^ (n + 1))
        (fun {_ _} hmn =>
          Ideal.Quotient.factorPow I (Nat.succ_le_succ hmn)) := by
  letI : (n : ℕ) → TopologicalSpace (R ⧸ I ^ (n + 1)) := fun _ => ⊥
  exact
    (adicPositiveQuotientInverseLimitCompatibleFamiliesEquiv I).homeomorph

def

adicPositiveQuotientInverseLimit_discreteEval

L710 ↗

LubinTate.Valuations.adicPositiveQuotientInverseLimit_discreteEval

Documentation

Defines adicPositiveQuotientInverseLimit_discreteEval.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

def adicPositiveQuotientInverseLimit_discreteEval
    {R : Type*} [CommRing R] (I : Ideal R) (n : ℕ) :
    adicPositiveQuotientInverseLimit I → DiscreteAdicQuotient I (n + 1)

theorem

adicPositiveQuotientInverseLimit_discreteEval_continuous

L717 ↗

LubinTate.Valuations.adicPositiveQuotientInverseLimit_discreteEval_continuous

Documentation

Every positive-level coordinate evaluation into a discrete adic quotient is continuous.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

theorem adicPositiveQuotientInverseLimit_discreteEval_continuous
    {R : Type*} [CommRing R] (I : Ideal R) (n : ℕ) :
    Continuous (adicPositiveQuotientInverseLimit_discreteEval I n)

def

adicQuotientInverseLimit_toPositive

L735 ↗

LubinTate.Valuations.adicQuotientInverseLimit_toPositive

Documentation

Defines adicQuotientInverseLimit_toPositive.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

def adicQuotientInverseLimit_toPositive
    {R : Type*} [CommRing R] (I : Ideal R) :
    adicQuotientInverseLimit I →
      adicPositiveQuotientInverseLimit I

def

adicPositiveQuotientInverseLimit_toAll

L747 ↗

LubinTate.Valuations.adicPositiveQuotientInverseLimit_toAll

Documentation

Defines adicPositiveQuotientInverseLimit_toAll.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

def adicPositiveQuotientInverseLimit_toAll
    {R : Type*} [CommRing R] (I : Ideal R) :
    adicPositiveQuotientInverseLimit I →
      adicQuotientInverseLimit I

theorem

adicPositiveQuotientInverseLimit_toPositive_toAll

L771 ↗

LubinTate.Valuations.adicPositiveQuotientInverseLimit_toPositive_toAll

Documentation

Restricting an all-level adic family to positive levels and extending back is the identity.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

theorem adicPositiveQuotientInverseLimit_toPositive_toAll
    {R : Type*} [CommRing R] (I : Ideal R)
    (x : adicPositiveQuotientInverseLimit I) :
    adicQuotientInverseLimit_toPositive I
        (adicPositiveQuotientInverseLimit_toAll I x) = x

theorem

adicQuotientInverseLimit_toAll_toPositive

L780 ↗

LubinTate.Valuations.adicQuotientInverseLimit_toAll_toPositive

Documentation

Extending a positive-level adic family and restricting again is the identity.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

theorem adicQuotientInverseLimit_toAll_toPositive
    {R : Type*} [CommRing R] (I : Ideal R)
    (x : adicQuotientInverseLimit I) :
    adicPositiveQuotientInverseLimit_toAll I
        (adicQuotientInverseLimit_toPositive I x) = x

def

adicQuotientInverseLimitEquivPositive

L797 ↗

LubinTate.Valuations.adicQuotientInverseLimitEquivPositive

Documentation

The all-level quotient inverse limit is equivalent to the canonical positive-indexed one.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · full declaration

def adicQuotientInverseLimitEquivPositive
    {R : Type*} [CommRing R] (I : Ideal R) :
    adicQuotientInverseLimit I ≃+*
      adicPositiveQuotientInverseLimit I where
  toFun := adicQuotientInverseLimit_toPositive I
  invFun := adicPositiveQuotientInverseLimit_toAll I
  left_inv := adicQuotientInverseLimit_toAll_toPositive I
  right_inv := adicPositiveQuotientInverseLimit_toPositive_toAll I
  map_mul' x y := by
    ext n
    rfl
  map_add' x y := by
    ext n
    rfl

def

adicPositiveQuotientInverseLimit_canonicalMap

L814 ↗

LubinTate.Valuations.adicPositiveQuotientInverseLimit_canonicalMap

Documentation

The adic inverse-limit equivalence, canonical map from a ring to the positive-indexed projective limit of its quotients.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · full declaration

def adicPositiveQuotientInverseLimit_canonicalMap
    {R : Type*} [CommRing R] (I : Ideal R) :
    R →+* adicPositiveQuotientInverseLimit I where
  toFun x := adicPositiveQuotientInverseLimit_mk I
    (fun n => Ideal.Quotient.mk (I ^ (n + 1)) x)
    (fun _ => rfl)
  map_one' := by ext n; rfl
  map_mul' x y := by ext n; rfl
  map_zero' := by ext n; rfl
  map_add' x y := by ext n; rfl

def

adicPositiveQuotientInverseLimitEquiv

L827 ↗

LubinTate.Valuations.adicPositiveQuotientInverseLimitEquiv

Documentation

The adic inverse-limit equivalence, if R is complete for the I-adic topology, the canonical map R → lim_n R/I^(n+1) is a ring isomorphism.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

def adicPositiveQuotientInverseLimitEquiv
    {R : Type*} [CommRing R] (I : Ideal R) [IsAdicComplete I R] :
    R ≃+* adicPositiveQuotientInverseLimit I

theorem

adicPositiveQuotientInverseLimitEquiv_apply

L835 ↗

LubinTate.Valuations.adicPositiveQuotientInverseLimitEquiv_apply

Documentation

The positive-indexed projective-limit isomorphism is induced by reduction modulo I^(n+1) in each coordinate.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

theorem adicPositiveQuotientInverseLimitEquiv_apply
    {R : Type*} [CommRing R] (I : Ideal R) [IsAdicComplete I R]
    (x : R) (n : ℕ) :
    adicPositiveQuotientInverseLimit_eval I n
        (adicPositiveQuotientInverseLimitEquiv I x) =
      Ideal.Quotient.mk (I ^ (n + 1)) x

def

adicPositiveQuotientCompatibleFamiliesHomeomorph

L843 ↗

LubinTate.Valuations.adicPositiveQuotientCompatibleFamiliesHomeomorph

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · full declaration

def adicPositiveQuotientCompatibleFamiliesHomeomorph
    {R : Type*} [CommRing R] (I : Ideal R) [IsAdicComplete I R] :
    letI : TopologicalSpace R := I.adicTopology
    letI : (n : ℕ) → TopologicalSpace (R ⧸ I ^ (n + 1)) := fun _ => ⊥
    R ≃ₜ compatibleRingFamilies (fun n : ℕ => R ⧸ I ^ (n + 1))
      (fun {_ _} hmn =>
        Ideal.Quotient.factorPow I (Nat.succ_le_succ hmn)) := by
  letI : TopologicalSpace R := I.adicTopology
  letI : (n : ℕ) → TopologicalSpace (R ⧸ I ^ (n + 1)) := fun _ => ⊥
  letI : (n : ℕ) → DiscreteTopology (R ⧸ I ^ (n + 1)) := fun _ => ⟨rfl⟩
  let e := (adicPositiveQuotientInverseLimitEquiv I).trans
    (adicPositiveQuotientInverseLimitRepresentation I)
  let c := (adicPositiveQuotientInverseLimitRepresentation I).toRingHom.comp
    (adicPositiveQuotientInverseLimit_canonicalMap I)
  refine
    { toFun := fun x => c x
      invFun := fun q => e.symm q
      left_inv := ?_
      right_inv := ?_
      continuous_toFun := ?_
      continuous_invFun := ?_ }
  · intro x
    have hc : c x = e x := by
      ext n
      exact (adicPositiveQuotientInverseLimitEquiv_apply I x n).symm
    change e.symm (c x) = x
    rw [hc]
    exact e.left_inv x
  · intro q
    ext n
    change Ideal.Quotient.mk (I ^ (n + 1)) (e.symm q) = q.1 n
    calc
      Ideal.Quotient.mk (I ^ (n + 1)) (e.symm q) = (e (e.symm q)).1 n :=
        (adicPositiveQuotientInverseLimitEquiv_apply I (e.symm q) n).symm
      _ = q.1 n := by simp [e.apply_symm_apply q]
  · change Continuous fun x : R => c x
    exact Continuous.subtype_mk
      (continuous_pi fun n => by
        simpa [c, adicPositiveQuotientInverseLimit_canonicalMap] using
          (quotient_mk_continuous_adic_raw I (n + 1)))
      (by
        intro x m n hmn
        rfl)
  · rw [continuous_iff_continuousAt]
    intro q
    rw [ContinuousAt, Filter.tendsto_def]
    intro s hs
    rcases (Ideal.hasBasis_nhds_adic I (e.symm q)).mem_iff.mp hs with
      ⟨n, _hn, hns⟩
    let cylinder : Set
        (compatibleRingFamilies (fun n : ℕ => R ⧸ I ^ (n + 1))
          (fun {_ _} hmn =>
            Ideal.Quotient.factorPow I (Nat.succ_le_succ hmn))) :=
      {q' | q'.1 n = q.1 n}
    have hcont_coord :
        Continuous fun q' : compatibleRingFamilies
            (fun n : ℕ => R ⧸ I ^ (n + 1))
            (fun {_ _} hmn =>
              Ideal.Quotient.factorPow I (Nat.succ_le_succ hmn)) =>
          q'.1 n := by
      exact (continuous_apply n).comp continuous_subtype_val
    have hcyl_open : IsOpen cylinder := by
      exact
        (isOpen_discrete ({q.1 n} : Set (R ⧸ I ^ (n + 1)))).preimage
          hcont_coord
    have hqmem : q ∈ cylinder := rfl
    exact mem_of_superset (hcyl_open.mem_nhds hqmem) (by
      intro q' hq'
      apply hns
      have hred' : Ideal.Quotient.mk (I ^ (n + 1)) (e.symm q') = q'.1 n := by
        calc
          Ideal.Quotient.mk (I ^ (n + 1)) (e.symm q') = (e (e.symm q')).1 n :=
            (adicPositiveQuotientInverseLimitEquiv_apply
              I (e.symm q') n).symm
          _ = q'.1 n := by simp [e.apply_symm_apply q']
      have hred : Ideal.Quotient.mk (I ^ (n + 1)) (e.symm q) = q.1 n := by
        calc
          Ideal.Quotient.mk (I ^ (n + 1)) (e.symm q) = (e (e.symm q)).1 n :=
            (adicPositiveQuotientInverseLimitEquiv_apply
              I (e.symm q) n).symm
          _ = q.1 n := by simp [e.apply_symm_apply q]
      have hmk : Ideal.Quotient.mk (I ^ (n + 1)) (e.symm q') =
          Ideal.Quotient.mk (I ^ (n + 1)) (e.symm q) := by
        rw [hred', hred, hq']
      have hmem_succ : e.symm q' - e.symm q ∈ I ^ (n + 1) := by
        exact (Ideal.Quotient.mk_eq_mk_iff_sub_mem
          (I := I ^ (n + 1)) (x := e.symm q') (y := e.symm q)).1 hmk
      have hmem : e.symm q' - e.symm q ∈ I ^ n :=
        Ideal.pow_le_pow_right (Nat.le_succ n) hmem_succ
      refine ⟨e.symm q' - e.symm q, hmem, ?_⟩
      ring)

def

adicPositiveQuotientInverseLimitHomeomorph

L937 ↗

LubinTate.Valuations.adicPositiveQuotientInverseLimitHomeomorph

Documentation

The positive-indexed topological inverse-limit equivalence with both topologies fixed by their types.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
open ValuationTheory.DiscreteValuationField
open ValuationTheory.Valuations
open Filter Set Topology
open scoped Valued

Lean source · statement

def adicPositiveQuotientInverseLimitHomeomorph
    {R : Type*} [CommRing R] (I : Ideal R) [IsAdicComplete I R] :
    WithTopology R I.adicTopology ≃ₜ
      adicPositiveQuotientInverseLimit I

Module documentation

Adic completion and inverse limits

Declarations