RetractionBounds.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Valuation inequalities for monomial retractions

In a closed étale chart, monomial retraction decreases the values of regular functions. The inequality passes to the valuation of the fraction field.

lemma OAI.CartierSections.closedChartRetraction_le line 32

Source documentation

Retraction decreases all regular-function values in a Noetherian closed étale chart, including boundary faces with zero weights.

lemma closedChartRetraction_le [CharZero k]
    (v : AddValuation A ENNReal) (B : Finset σ) (w : σ → ℝ≥0)
    (hwzero : ∀ i ∉ B, w i = 0)
    (hz : ∀ i ∈ B, v (algebraMap (MvPolynomial σ k) A (MvPolynomial.X i)) =
      (w i : ENNReal)) (f : A) : closedChartRetraction (σ := σ) (k := k) (A := A) (R := R) w f ≤ v f := by
…

Mentions: OAI.CartierSections.closedChartRetraction

lemma OAI.CartierSections.closedChartFieldRetraction_le line 82