Documentation

DerivedAlgGeo.AlgebraicGeometry.Numerical.Models.Surface.Comparison

Comparisons between rank-one numerical surface models #

The individual K3, abelian, and Enriques models depend only on their shared rank-one foundation. This downstream module owns declarations that mention more than one model.

source
noncomputable def AlgebraicGeometry.Numerical.Examples.k3AndAbelianPresentations (d : ℕ) :
NumericalVarietyData 2 SurfaceRing SurfaceNum × NumericalVarietyData 2 SurfaceRing SurfaceNum

Two numerical presentations on the same carriers coexist as ordinary data.

Equations
Instances For
    source
    noncomputable def AlgebraicGeometry.Numerical.Examples.k3EnriquesAbelianPresentations (d : ℕ) :
    NumericalVarietyData 2 SurfaceRing SurfaceNum × NumericalVarietyData 2 SurfaceRing SurfaceNum × NumericalVarietyData 2 SurfaceRing SurfaceNum

    Three numerical presentations on the same carriers coexist as ordinary data.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem AlgebraicGeometry.Numerical.Examples.chiStructureSheaf_enriques_ne_k3 (d : ℕ) (hd : d ≠ 0) :
      Surface.chiStructureSheaf (enriquesNumericalVariety d) ≠ Surface.chiStructureSheaf (k3NumericalVariety d)
      source
      theorem AlgebraicGeometry.Numerical.Examples.chiStructureSheaf_enriques_ne_abelian (d : ℕ) (hd : d ≠ 0) :
      Surface.chiStructureSheaf (enriquesNumericalVariety d) ≠ Surface.chiStructureSheaf (abelianNumericalVariety d)
      source
      theorem AlgebraicGeometry.Numerical.Examples.chiStructureSheaf_k3_ne_abelian (d : ℕ) (hd : d ≠ 0) :
      Surface.chiStructureSheaf (k3NumericalVariety d) ≠ Surface.chiStructureSheaf (abelianNumericalVariety d)