ChartCompactness.lean`

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compactness of monomial retractions on a closed étale chart

Local algebra for uniform Cartier sections.

lemma OAI.CartierSections.continuous_closedChartFieldRetraction_evaluations line 38
Source documentation
Monomial retractions of a closed étale chart vary continuously with the weights.
```
lemma continuous_closedChartFieldRetraction_evaluations :
    Continuous (fun w : σ → NNReal => fun x : K =>
      closedChartFieldRetraction (σ := σ) (k := k) (R := R) (A := A) w x) :=
…
```
Mentions: OAI.CartierSections.closedChartFieldRetraction
lemma OAI.CartierSections.isCompact_closedChartFieldRetraction_cone line 47
Source documentation
The normalized monomial retractions on the fraction field of a closed étale chart form a compact set in the topology of pointwise evaluation.
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Field, IsAlgClosed, CommRing, IsLocalRing, IsNoetherianRing, IsDomain, Algebra, IsFractionRing, MvPolynomial, Finsupp, Nat, IsScalarTower, IsLocalization.AtPrime, MvPolynomial.idealOfVars, OAI.CartierSections.polynomialOrigin_isMaximal_topology, IsLocalHom, RingHom, Algebra.algebraMap, Algebra.FormallyUnramified and 12 more
Proof uses: IsCompact.image, OAI.CartierSections.isCompact_normalizedWeights, OAI.CartierSections.continuous_closedChartFieldRetraction_evaluations
85 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: ComparatorChallenges/CartierChartCompactnessSupport.lean:25 (same statement text; different proof or body). Qualify references as OAI.CartierSections.isCompact_closedChartFieldRetraction_cone@path.
```
lemma isCompact_closedChartFieldRetraction_cone
    (a : σ → NNReal) (ha : ∀ i, 0 < a i) :
    IsCompact ((fun w : σ → NNReal => fun x : K =>
      closedChartFieldRetraction (σ := σ) (k := k) (R := R) (A := A) w x) ''
…
```
Mentions: OAI.CartierSections.closedChartFieldRetraction