SurfaceSmooth.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The normalized projective surface is smooth over ℂ.

lemma OAI.SourceSymmetry.homogeneousAway_toComplex line 11
lemma OAI.SourceSymmetry.projAway_toComplex line 25
lemma OAI.SourceSymmetry.projOpen_toComplex_smooth line 32
theorem OAI.SourceSymmetry.projectiveSurface_smooth line 52
Source documentation
The Proj of the normalized section algebra is smooth over ℂ.
```
theorem projectiveSurface_smooth : Smooth projectiveSurfaceToComplex := by
…
```
def OAI.SourceSymmetry.coefficientIota line 69
Source documentation
The coefficient charts are open immersions into the source Proj.
```
def coefficientIota (t : SectionIndex) (ht : Good t) :
    Spec (CommRingCat.of (coefficientChart t)) ⟶ projectiveSurface :=
…
```
Mentions: OAI.SourceSymmetry.SectionIndex, OAI.SourceSymmetry.Good, OAI.SourceSymmetry.coefficientChart
instance OAI.SourceSymmetry.coefficientIota_open line 73
lemma OAI.SourceSymmetry.coefficientIota_toComplex line 82
def OAI.SourceSymmetry.coefficientCotangentIso line 93
Source documentation
The intrinsic source cotangent sheaf on each good chart is the Kähler differential module already used in the canonical-frame calculation.
```
def coefficientCotangentIso (t : SectionIndex) (ht : Good t) :
    (ActualCotangent.sheaf projectiveSurfaceToComplex).restrict (coefficientIota t ht) ≅
      @tilde (CommRingCat.of (coefficientChart t))
        (ActualCotangent.affineModule (k := ℂ) (coefficientChart t)) :=
…
```
Mentions: OAI.SourceSymmetry.SectionIndex, OAI.SourceSymmetry.Good, OAI.ActualCotangent.sheaf, OAI.SourceSymmetry.coefficientIota, OAI.SourceSymmetry.coefficientChart, OAI.ActualCotangent.affineModule