OAI/AlgebraicGeometry/CartierSections/FieldRetraction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Monomial retractions on rational function fields

The closed étale chart retraction extends to the chart's fraction field.

  1. def OAI.CartierSections.closedChartFieldRetraction line 31

    Source documentation

    The retraction is a valuation of the chart's actual rational function field.

    noncomputable def closedChartFieldRetraction (w : σ → NNReal) : AddValuation K (WithTop ℝ) :=
…
  2. lemma OAI.CartierSections.closedChartFieldRetraction_regular line 35