ChartCompletion.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Completion coordinates for étale charts

Compatible infinitesimal isomorphisms identify an étale chart completion with a power-series ring. Expansion through a Noetherian local completion is faithfully flat.

theorem OAI.CartierSections.completion_eval_factor line 28

Source documentation

Evaluation of an adic completion commutes with reduction to a lower ideal power.

theorem completion_eval_factor (I : Ideal R) {m n : ℕ} (h : m ≤ n)
    (x : AdicCompletion I R) :
    Ideal.Quotient.factorₐ R (Ideal.pow_le_pow_right h) (AdicCompletion.evalₐ I n x) =
      AdicCompletion.evalₐ I m x := by
…

theorem OAI.CartierSections.quotientPowerMap_eval_compatible line 39

Source documentation

Evaluation on infinitesimal neighbourhoods is compatible with the maps induced by an algebra map.

theorem quotientPowerMap_eval_compatible (I : Ideal R) {m n : ℕ} (h : m ≤ n) :
    (Ideal.Quotient.factorₐ R
      (Ideal.pow_le_pow_right (I := I.map (algebraMap R A)) h)).comp
…

def OAI.CartierSections.chartCompletionMap line 50

Source documentation

The completion map induced by an algebra map.

noncomputable def chartCompletionMap (I : Ideal R) :
    AdicCompletion I R →ₐ[R] AdicCompletion (I.map (algebraMap R A)) A :=
…

theorem OAI.CartierSections.chartCompletionMap_eval line 56
theorem OAI.CartierSections.chartCompletionMap_bijective line 63
Source documentation
Étale charts with trivial residue extension have the same completion. This is derived from formal lifting and uniqueness at every order.
```
theorem chartCompletionMap_bijective [Algebra.FormallyEtale R A]
    (I : Ideal R) (hI : Function.Bijective (quotientBaseMap (A := A) I)) :
…
```
Mentions: OAI.CartierSections.quotientBaseMap
def OAI.CartierSections.chartCompletionEquiv line 104

def OAI.CartierSections.polynomialChartSeriesEquiv line 110

Source documentation

Formal coordinates on the completion of an étale polynomial chart.

noncomputable def polynomialChartSeriesEquiv
    {σ k A : Type*} [Finite σ] [CommRing k] [CommRing A]
    [Algebra (MvPolynomial σ k) A] [Algebra.FormallyEtale (MvPolynomial σ k) A]
    (hI : Function.Bijective
      (quotientBaseMap (A := A) (MvPolynomial.idealOfVars σ k))) :
…

Mentions: OAI.CartierSections.quotientBaseMap

theorem OAI.CartierSections.polynomialChartSeriesEquiv_coe line 120

def OAI.CartierSections.completionExpansion line 129

Source documentation

The expansion map attached to an isomorphism with the maximal-ideal completion.

noncomputable def completionExpansion
    {A S : Type*} [CommRing A] [IsLocalRing A] [CommRing S]
    (e : S ≃+* AdicCompletion (IsLocalRing.maximalIdeal A) A) : A →+* S :=
…

theorem OAI.CartierSections.completionExpansion_faithfullyFlat line 135

Source documentation

Formal expansion through a Noetherian completion is faithfully flat.

theorem completionExpansion_faithfullyFlat
    {A S : Type*} [CommRing A] [IsLocalRing A] [IsNoetherianRing A] [CommRing S]
    (e : S ≃+* AdicCompletion (IsLocalRing.maximalIdeal A) A) :
    letI : Algebra A S := (completionExpansion e).toAlgebra
…

Mentions: OAI.CartierSections.completionExpansion

theorem OAI.CartierSections.completionExpansion_isLocalHom line 148

Source documentation

A formal expansion through a Noetherian local completion reflects units.

theorem completionExpansion_isLocalHom
    {A S : Type*} [CommRing A] [IsLocalRing A] [IsNoetherianRing A] [CommRing S]
    (e : S ≃+* AdicCompletion (IsLocalRing.maximalIdeal A) A) :
    IsLocalHom (completionExpansion e) := by
…

Mentions: OAI.CartierSections.completionExpansion

def OAI.CartierSections.chartSeriesExpansion line 162

Source documentation

Expansion in completion coordinates as an algebra map over the coefficient ring.

noncomputable def chartSeriesExpansion
    (e : MvPowerSeries σ k ≃ₐ[MvPolynomial σ k]
      AdicCompletion (IsLocalRing.maximalIdeal A) A) : A →ₐ[k] MvPowerSeries σ k :=
…

theorem OAI.CartierSections.chartSeriesExpansion_toRingHom line 168
theorem OAI.CartierSections.chartSeriesExpansion_coordinate line 173