Module

FiniteGeometricPoints.lean

Nyll.SchemeTheory.Etale.FiniteGeometricPoints

3 declarations indexed from sourceView source ↗

Module documentation

Geometric lifts through a finite morphism

An algebraically closed geometric fiber of a finite morphism is Artinian. The correspondence between rational points and closed points therefore constructs every geometric lift and proves that the set of lifts is finite. No étaleness or reducedness of the finite morphism is used.

Imports6

Mathlib.AlgebraicGeometry.AlgClosed.Basic
Mathlib.AlgebraicGeometry.Artinian
Mathlib.AlgebraicGeometry.Morphisms.Finite
Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Mathlib.AlgebraicGeometry.PullbackCarrier
Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Imported by4

def

geometricLiftEquivFiberSection

L35 ↗

AlgebraicGeometry.Scheme.Hom.geometricLiftEquivFiberSection

Documentation

Geometric lifts through a scheme morphism are sections of its geometric fiber.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
variable {X Y : Scheme.{u}} (q : Y ⟶ X)
  {Ω : Type u} [Field Ω] (t : Spec (CommRingCat.of Ω) ⟶ X)

Lean source · full declaration

def Scheme.Hom.geometricLiftEquivFiberSection :
    {s : Spec (CommRingCat.of Ω) ⟶ Y // s ≫ q = t} ≃
      {p : Spec (CommRingCat.of Ω) ⟶ pullback q t //
        p ≫ pullback.snd q t = 𝟙 _} where
  toFun s := ⟨pullback.lift s.val (𝟙 _) (s.property.trans (Category.id_comp t).symm),
    pullback.lift_snd _ _ _⟩
  invFun p := ⟨p.val ≫ pullback.fst q t, by
    rw [Category.assoc, pullback.condition, ← Category.assoc, p.property,
      Category.id_comp]⟩
  left_inv s := Subtype.ext (pullback.lift_fst _ _ _)
  right_inv p := by
    apply Subtype.ext
    apply pullback.hom_ext
    · exact pullback.lift_fst _ _ _
    · exact (pullback.lift_snd _ _ _).trans p.property.symm

theorem

exists_geometricLift_of_isFinite

L55 ↗

AlgebraicGeometry.Scheme.Hom.exists_geometricLift_of_isFinite

Documentation

Every point of the ordinary fiber is the image of an algebraically closed geometric lift.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
variable {X Y : Scheme.{u}} (q : Y ⟶ X)
  {Ω : Type u} [Field Ω] (t : Spec (CommRingCat.of Ω) ⟶ X)
variable [IsFinite q] [IsAlgClosed Ω]

Lean source · statement

theorem Scheme.Hom.exists_geometricLift_of_isFinite
    (y : Y) (hy : q y = t default) :
    ∃ s : Spec (CommRingCat.of Ω) ⟶ Y, s ≫ q = t ∧ s default = y

theorem

finite_geometricLifts_of_isFinite

L74 ↗

AlgebraicGeometry.Scheme.Hom.finite_geometricLifts_of_isFinite

Documentation

The lifts of an algebraically closed geometric point through a finite morphism form a finite type, including an empty fiber.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry
variable {X Y : Scheme.{u}} (q : Y ⟶ X)
  {Ω : Type u} [Field Ω] (t : Spec (CommRingCat.of Ω) ⟶ X)
variable [IsFinite q] [IsAlgClosed Ω]

Lean source · statement

theorem Scheme.Hom.finite_geometricLifts_of_isFinite :
    Finite {s : Spec (CommRingCat.of Ω) ⟶ Y // s ≫ q = t}

Module documentation

Geometric lifts through a finite morphism

Declarations

geometricLiftEquivFiberSection

exists_geometricLift_of_isFinite

finite_geometricLifts_of_isFinite