SurfaceCharts.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Smoothness of the degree-zero homogeneous charts in the completed Cartier model.

lemma OAI.SourcePullbackChart.surfaceIota_toComplex line 11
instance OAI.SourcePullbackChart.surfaceChart_smooth line 17
Source documentation
Smoothness of the coefficient charts.
```
instance surfaceChart_smooth (i : Fin 3) : Algebra.Smooth ℂ (surfaceChart i) := by
…
```
Mentions: OAI.SourcePullbackChart.surfaceChart
instance OAI.SourcePullbackChart.surfaceChart_noetherian line 24
instance OAI.SourcePullbackChart.surfaceChart_regular line 27
lemma OAI.SourcePullbackChart.projectiveNormalization_toComplex line 38
Source documentation
The finite normalization map respects the very same complex structure used in the smoothness theorem.
```
lemma projectiveNormalization_toComplex :
    ExplicitCone.projectiveNormalization ≫ SourceZeroSections.planeScalar =
      ExplicitCone.projectiveSurfaceToComplex := by
…
```
Mentions: OAI.ExplicitCone.projectiveNormalization, OAI.SourceZeroSections.planeScalar, OAI.ExplicitCone.projectiveSurfaceToComplex
def OAI.SourcePullbackChart.completedSourcePrincipalQuotient line 71
instance OAI.SourcePullbackChart.completedSourcePrincipalQuotient_regular line 76
lemma OAI.SourcePullbackChart.completedSource_regular_at_fiber line 82
Source documentation
At every point of the exceptional fiber the ambient completed source local ring is regular.
```
lemma completedSource_regular_at_fiber (i : Fin 3) (p : Ideal (completedSourceChart i))
    [p.IsPrime] (hp : completedFiberParameter i ∈ p) :
    IsRegularLocalRing (Localization.AtPrime p) := by
…
```
Mentions: OAI.SourcePullbackChart.completedSourceChart, OAI.SourcePullbackChart.completedFiberParameter