OAI/AlgebraicGeometry/CartierSections/ChartRetraction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Monomial retractions on closed étale charts

The completed local coordinate isomorphism defines a faithful formal expansion. Its monomial valuation allows boundary faces with zero weights.

  1. def OAI.CartierSections.completionIdealCongr line 17

    Source documentation

    Equal ideals have canonically isomorphic completions.

    noncomputable def completionIdealCongr {P A : Type*} [CommRing P] [CommRing A]
    [Algebra P A] (I J : Ideal A) (h : I = J) :
    AdicCompletion I A ≃ₐ[P] AdicCompletion J A := by
…
  2. def OAI.CartierSections.closedChartEquiv line 38

    Source documentation

    The completed coordinate isomorphism at a closed étale point.

    noncomputable def closedChartEquiv : MvPowerSeries σ k ≃ₐ[MvPolynomial σ k]
    AdicCompletion (IsLocalRing.maximalIdeal A) A := by
…
  3. def OAI.CartierSections.closedChartExpansion line 45
  4. lemma OAI.CartierSections.closedChartExpansion_coordinate line 49
  5. def OAI.CartierSections.closedChartRetraction line 55

    Source documentation

    The monomial valuation pulled back by the formal coordinate expansion.

    noncomputable def closedChartRetraction (w : σ → ℝ≥0) : AddValuation A ENNReal :=
…
  6. lemma OAI.CartierSections.closedChartExpansion_injective line 58
  7. lemma OAI.CartierSections.closedChartRetraction_finite line 66