ClosedCharts.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Closed étale coordinate charts

Over an algebraically closed coefficient field, a closed unramified chart has no residue extension, and its coordinate functions generate its maximal ideal.

theorem OAI.CartierSections.local_unramified_base_bijective line 23

Source documentation

A local essentially finite type unramified chart over an algebraically closed residue field induces an isomorphism on residue rings.

theorem local_unramified_base_bijective
    {R A : Type*} [CommRing R] [CommRing A] [Algebra R A]
    [IsLocalRing R] [IsLocalRing A] [IsLocalHom (algebraMap R A)]
    [Algebra.FormallyUnramified R A] [Algebra.EssFiniteType R A]
    [IsAlgClosed (IsLocalRing.ResidueField R)] :
    Function.Bijective (quotientBaseMap (A := A) (IsLocalRing.maximalIdeal R)) := by
…

Mentions: OAI.CartierSections.quotientBaseMap

theorem OAI.CartierSections.idealOfVars_eq_ker_constantCoeff line 48

Source documentation

The coordinate-origin ideal is the literal kernel of the constant coefficient map.

theorem idealOfVars_eq_ker_constantCoeff {σ k : Type*} [CommRing k] :
    MvPolynomial.idealOfVars σ k = RingHom.ker (MvPolynomial.constantCoeff (σ := σ) (R := k)) := by
…

def OAI.CartierSections.polynomialOriginResidueEquiv line 60
theorem OAI.CartierSections.polynomialOriginResidueEquiv_mk line 66
theorem OAI.CartierSections.polynomialOrigin_isMaximal line 71

theorem OAI.CartierSections.closed_chart_maximalIdeal line 92

Source documentation

Closed étale coordinate functions generate the maximal ideal.

theorem closed_chart_maximalIdeal :
    (MvPolynomial.idealOfVars σ k).map (algebraMap (MvPolynomial σ k) A) =
      IsLocalRing.maximalIdeal A := by
…

theorem OAI.CartierSections.closed_chart_base_bijective line 104
Source documentation
The residue premise for the completion equivalence follows from a closed unramified chart over the algebraically closed coefficient field.
```
theorem closed_chart_base_bijective :
    Function.Bijective (quotientBaseMap (A := A) (MvPolynomial.idealOfVars σ k)) := by
…
```
Mentions: OAI.CartierSections.quotientBaseMap