NYLL
Module

PowerCofinality.lean

Nyll.EtaleFundamentalGroups.Completions.Adic.PowerCofinality
13 declarations indexed from sourceView source ↗

Module documentation

Cofinality of power-adic completions

For a positive integer e, the filtrations I ^ n and (I ^ e) ^ n are cofinal. This file realizes that cofinality at the finite quotient levels and produces the resulting canonical equivalence of adic completions.

Imports1
Imported by3

Declarations

def

powerQuotientEquiv

L28 ↗
EtaleFundamentalGroups.powerQuotientEquiv
Documentation

The quotient at level e * n for I is canonically the quotient at level n for I ^ e.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open LubinTate.Valuations
universe uR
Lean source · statement
def powerQuotientEquiv
    {R : Type uR} [CommRing R] (I : Ideal R) (e n : ℕ) :
    (R ⧸ I ^ (e * n)) ≃+* (R ⧸ (I ^ e) ^ n)
theorem

powerQuotientEquiv_mk

L34 ↗
EtaleFundamentalGroups.powerQuotientEquiv_mk
Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open LubinTate.Valuations
universe uR
Lean source · statement
theorem powerQuotientEquiv_mk
    {R : Type uR} [CommRing R] (I : Ideal R) (e n : ℕ) (r : R) :
    powerQuotientEquiv I e n (Ideal.Quotient.mk (I ^ (e * n)) r) =
      Ideal.Quotient.mk ((I ^ e) ^ n) r
theorem

powerQuotientEquiv_symm_mk

L41 ↗
EtaleFundamentalGroups.powerQuotientEquiv_symm_mk
Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open LubinTate.Valuations
universe uR
Lean source · statement
theorem powerQuotientEquiv_symm_mk
    {R : Type uR} [CommRing R] (I : Ideal R) (e n : ℕ) (r : R) :
    (powerQuotientEquiv I e n).symm
        (Ideal.Quotient.mk ((I ^ e) ^ n) r) =
      Ideal.Quotient.mk (I ^ (e * n)) r
theorem

factorPow_mk

L54 ↗
EtaleFundamentalGroups.factorPow_mk
Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open LubinTate.Valuations
universe uR
Lean source · statement
theorem factorPow_mk
    {R : Type uR} [CommRing R] (I : Ideal R)
    {m n : ℕ} (hmn : m ≤ n) (r : R) :
    Ideal.Quotient.factorPow I hmn
        (Ideal.Quotient.mk (I ^ n) r) =
      Ideal.Quotient.mk (I ^ m) r
theorem

powerQuotientEquiv_factorPow

L64 ↗
EtaleFundamentalGroups.powerQuotientEquiv_factorPow
Documentation

Reindexing quotient transition maps by n ↦ e * n commutes with the canonical quotient equivalences.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open LubinTate.Valuations
universe uR
Lean source · statement
theorem powerQuotientEquiv_factorPow
    {R : Type uR} [CommRing R] (I : Ideal R) (e : ℕ)
    {m n : ℕ} (hmn : m ≤ n)
    (x : R ⧸ I ^ (e * n)) :
    Ideal.Quotient.factorPow (I ^ e) hmn
        (powerQuotientEquiv I e n x) =
      powerQuotientEquiv I e m
        (Ideal.Quotient.factorPow I
          (Nat.mul_le_mul_left e hmn) x)
def

powerCofinalityRestrict

L86 ↗
EtaleFundamentalGroups.powerCofinalityRestrict
Documentation

Restrict an I-adic compatible family to the cofinal levels e * n.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open LubinTate.Valuations
universe uR
Lean source · full declaration
def powerCofinalityRestrict
    {R : Type uR} [CommRing R] (I : Ideal R) (e : ℕ) :
    adicQuotientInverseLimit I →+*
      adicQuotientInverseLimit (I ^ e) where
  toFun x :=
    adicQuotientInverseLimit_mk (I ^ e)
      (fun n => powerQuotientEquiv I e n
        (adicQuotientInverseLimit_eval I (e * n) x))
      (fun {m n} hmn => by
        rw [powerQuotientEquiv_factorPow I e hmn]
        rw [adicQuotientInverseLimit_eval_factorPow I
          (Nat.mul_le_mul_left e hmn) x])
  map_one' := by
    apply adicQuotientInverseLimit_ext (I ^ e)
    intro n
    simp only [map_one]
    rfl
  map_mul' x y := by
    apply adicQuotientInverseLimit_ext (I ^ e)
    intro n
    simp only [adicQuotientInverseLimit_eval_mk, map_mul]
    rfl
  map_zero' := by
    apply adicQuotientInverseLimit_ext (I ^ e)
    intro n
    simp only [map_zero]
    rfl
  map_add' x y := by
    apply adicQuotientInverseLimit_ext (I ^ e)
    intro n
    simp only [adicQuotientInverseLimit_eval_mk, map_add]
    rfl
def

powerCofinalityExtend

L122 ↗
EtaleFundamentalGroups.powerCofinalityExtend
Documentation

Extend a compatible family on the cofinal (I ^ e)-levels to all I-adic levels. At level n, reduce its level-n value from I ^ (e * n) to I ^ n.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open LubinTate.Valuations
universe uR
Lean source · full declaration
def powerCofinalityExtend
    {R : Type uR} [CommRing R] (I : Ideal R) (e : ℕ) (he : 0 < e) :
    adicQuotientInverseLimit (I ^ e) →+*
      adicQuotientInverseLimit I where
  toFun x :=
    adicQuotientInverseLimit_mk I
      (fun n => Ideal.Quotient.factorPow I
        (Nat.le_mul_of_pos_left n he)
        ((powerQuotientEquiv I e n).symm
          (adicQuotientInverseLimit_eval (I ^ e) n x)))
      (fun {m n} hmn => by
        rw [← adicQuotientInverseLimit_eval_factorPow (I ^ e) hmn x]
        refine Quotient.inductionOn'
          (adicQuotientInverseLimit_eval (I ^ e) n x) ?_
        intro r
        change
          Ideal.Quotient.factorPow I hmn
              (Ideal.Quotient.factorPow I (Nat.le_mul_of_pos_left n he)
                ((powerQuotientEquiv I e n).symm
                  (Ideal.Quotient.mk ((I ^ e) ^ n) r))) =
            Ideal.Quotient.factorPow I (Nat.le_mul_of_pos_left m he)
              ((powerQuotientEquiv I e m).symm
                (Ideal.Quotient.factorPow (I ^ e) hmn
                  (Ideal.Quotient.mk ((I ^ e) ^ n) r)))
        simp only [powerQuotientEquiv_symm_mk, factorPow_mk])
  map_one' := by
    apply adicQuotientInverseLimit_ext I
    intro n
    simp only [map_one]
    rfl
  map_mul' x y := by
    apply adicQuotientInverseLimit_ext I
    intro n
    simp only [adicQuotientInverseLimit_eval_mk, map_mul]
    rfl
  map_zero' := by
    apply adicQuotientInverseLimit_ext I
    intro n
    simp only [map_zero]
    rfl
  map_add' x y := by
    apply adicQuotientInverseLimit_ext I
    intro n
    simp only [adicQuotientInverseLimit_eval_mk, map_add]
    rfl
theorem

powerCofinalityExtend_restrict

L169 ↗
EtaleFundamentalGroups.powerCofinalityExtend_restrict
Documentation

Extending after restriction recovers every I-adic compatible family.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open LubinTate.Valuations
universe uR
Lean source · statement
theorem powerCofinalityExtend_restrict
    {R : Type uR} [CommRing R] (I : Ideal R) (e : ℕ) (he : 0 < e)
    (x : adicQuotientInverseLimit I) :
    powerCofinalityExtend I e he (powerCofinalityRestrict I e x) = x
theorem

powerCofinalityRestrict_extend

L187 ↗
EtaleFundamentalGroups.powerCofinalityRestrict_extend
Documentation

Restricting after extension recovers every (I ^ e)-adic compatible family; this is the finite-level cofinality argument.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open LubinTate.Valuations
universe uR
Lean source · statement
theorem powerCofinalityRestrict_extend
    {R : Type uR} [CommRing R] (I : Ideal R) (e : ℕ) (he : 0 < e)
    (x : adicQuotientInverseLimit (I ^ e)) :
    powerCofinalityRestrict I e (powerCofinalityExtend I e he x) = x
def

powerCofinalityInverseLimitEquiv

L219 ↗
EtaleFundamentalGroups.powerCofinalityInverseLimitEquiv
Documentation

The inverse limits of the I-adic and (I ^ e)-adic quotient systems are canonically ring-equivalent for e > 0.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open LubinTate.Valuations
universe uR
Lean source · full declaration
def powerCofinalityInverseLimitEquiv
    {R : Type uR} [CommRing R] (I : Ideal R) (e : ℕ) (he : 0 < e) :
    adicQuotientInverseLimit (I ^ e) ≃+*
      adicQuotientInverseLimit I where
  toFun := powerCofinalityExtend I e he
  invFun := powerCofinalityRestrict I e
  left_inv := powerCofinalityRestrict_extend I e he
  right_inv := powerCofinalityExtend_restrict I e he
  map_mul' := map_mul (powerCofinalityExtend I e he)
  map_add' := map_add (powerCofinalityExtend I e he)
def

adicCompletionPowerRingEquiv

L231 ↗
EtaleFundamentalGroups.adicCompletionPowerRingEquiv
Documentation

Power-adic cofinality for actual adic completions.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open LubinTate.Valuations
universe uR
Lean source · statement
def adicCompletionPowerRingEquiv
    {R : Type uR} [CommRing R] (I : Ideal R) (e : ℕ) (he : 0 < e) :
    AdicCompletion (I ^ e) R ≃+* AdicCompletion I R
theorem

adicCompletionPowerRingEquiv_eval

L241 ↗
EtaleFundamentalGroups.adicCompletionPowerRingEquiv_eval
Documentation

The power-cofinality equivalence has the expected finite quotient coordinate: level n is obtained by reducing from I ^ (e * n) to I ^ n.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open LubinTate.Valuations
universe uR
Lean source · statement
theorem adicCompletionPowerRingEquiv_eval
    {R : Type uR} [CommRing R] (I : Ideal R) (e : ℕ) (he : 0 < e)
    (x : AdicCompletion (I ^ e) R) (n : ℕ) :
    AdicCompletion.evalₐ I n (adicCompletionPowerRingEquiv I e he x) =
      Ideal.Quotient.factorPow I (Nat.le_mul_of_pos_left n he)
        ((powerQuotientEquiv I e n).symm
          (AdicCompletion.evalₐ (I ^ e) n x))
def

adicCompletionPowerAlgEquiv

L258 ↗
EtaleFundamentalGroups.adicCompletionPowerAlgEquiv
Documentation

The power-cofinality equivalence is an equivalence of R-algebras for the canonical maps into both adic completions.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open LubinTate.Valuations
universe uR
Lean source · statement
def adicCompletionPowerAlgEquiv
    {R : Type uR} [CommRing R] (I : Ideal R) (e : ℕ) (he : 0 < e) :
    AdicCompletion (I ^ e) R ≃ₐ[R] AdicCompletion I R

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