NYLL
Module

IsIsoOfBijectivePointsCharZero.lean

Nyll.AlgebraicCurves.Geometry.Curves.IsIsoOfBijectivePointsCharZero
6 declarations indexed from sourceView source ↗

Module documentation

Isomorphisms of proper smooth curves from rational points in characteristic zero

For a morphism from an integral proper smooth curve to an integral proper smooth scheme over an algebraically closed field of characteristic zero, bijectivity on rational points implies that the original morphism is an isomorphism.

The proof uses the actual diagonal and residue-field maps. After constructing the generic-stalk isomorphism, it uses the imported extension theorems for proper smooth curves. Those suppliers retain their Anthropic FLT upstream notices in their own source files.

Imports21
  • Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_isOpenImmersion_of_functionField_iso
  • Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_iso_comp_eq_of_isOpenImmersion_of_isProper
  • Mathlib.AlgebraicGeometry.AlgClosed.Basic
  • Mathlib.AlgebraicGeometry.FunctionField
  • Mathlib.AlgebraicGeometry.Morphisms.FiniteType
  • Mathlib.AlgebraicGeometry.Morphisms.Proper
  • Mathlib.AlgebraicGeometry.Morphisms.Separated
  • Mathlib.AlgebraicGeometry.Morphisms.Smooth
  • Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
  • Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
  • Mathlib.AlgebraicGeometry.Pullbacks
  • Mathlib.AlgebraicGeometry.ResidueField
  • Mathlib.AlgebraicGeometry.Stalk
  • Mathlib.Algebra.CharP.Algebra
  • Mathlib.CategoryTheory.Comma.Over.Basic
  • Mathlib.CategoryTheory.Limits.Shapes.Diagonal
  • Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  • Mathlib.FieldTheory.PurelyInseparable.Basic
  • Mathlib.FieldTheory.Separable
  • Mathlib.RingTheory.RingHom.PurelyInseparable
  • Mathlib.Topology.JacobsonSpace
Imported by2

Declarations

theorem

surjective_of_contains_closedPoints

L51 ↗
AlgebraicGeometry.surjective_of_contains_closedPoints
Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
namespace AlgebraicGeometry
universe u
Lean source · statement
theorem surjective_of_contains_closedPoints
    {X Y : Scheme.{u}} (f : X ⟶ Y) [UniversallyClosed f] [JacobsonSpace Y]
    (h : closedPoints Y ⊆ Set.range f) : Surjective f
theorem

surjective_of_surjective_rationalPoints

L62 ↗
AlgebraicGeometry.surjective_of_surjective_rationalPoints
Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
namespace AlgebraicGeometry
universe u
Lean source · full declaration
theorem surjective_of_surjective_rationalPoints
    {K : Type u} [Field K] [IsAlgClosed K] {X Y : Scheme.{u}}
    (c : X ⟶ Spec (CommRingCat.of K)) (d : Y ⟶ Spec (CommRingCat.of K))
    [IsProper c] [IsProper d] (f : Over.mk c ⟶ Over.mk d)
    (h : Function.Surjective
      (fun p : Over.mk (𝟙 (Spec (CommRingCat.of K))) ⟶ Over.mk c => p ≫ f)) :
    Surjective f.left := by
  let g : X ⟶ Y := f.left
  have hgbase : g ≫ d = c := f.w
  have : IsProper (g ≫ d) := by rw [hgbase]; infer_instance
  have : IsProper g := IsProper.of_comp g d
  have : JacobsonSpace Y := LocallyOfFiniteType.jacobsonSpace d
  change Surjective g
  apply surjective_of_contains_closedPoints (X := X) (Y := Y) g
  intro y hy
  let q : Over.mk (𝟙 (Spec (CommRingCat.of K))) ⟶ Over.mk d :=
    Over.homMk (pointOfClosedPoint d y hy) (pointOfClosedPoint_comp d y hy)
  obtain ⟨p, hp⟩ := h q
  refine ⟨p.left (IsLocalRing.closedPoint K), ?_⟩
  calc
    g (p.left (IsLocalRing.closedPoint K)) =
        (p ≫ f).left (IsLocalRing.closedPoint K) :=
      (Scheme.Hom.comp_apply p.left g (IsLocalRing.closedPoint K)).symm
    _ = q.left (IsLocalRing.closedPoint K) :=
      congrArg (fun r => r.left (IsLocalRing.closedPoint K)) hp
    _ = y := pointOfClosedPoint_apply d y hy (IsLocalRing.closedPoint K)
theorem

universallyInjective_of_injective_rationalPoints

L89 ↗
AlgebraicGeometry.universallyInjective_of_injective_rationalPoints
Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
namespace AlgebraicGeometry
universe u
Lean source · full declaration
theorem universallyInjective_of_injective_rationalPoints
    {K : Type u} [Field K] [IsAlgClosed K] {X Y : Scheme.{u}}
    (c : X ⟶ Spec (CommRingCat.of K)) (d : Y ⟶ Spec (CommRingCat.of K))
    [IsProper c] [IsProper d] (f : Over.mk c ⟶ Over.mk d)
    (h : Function.Injective
      (fun p : Over.mk (𝟙 (Spec (CommRingCat.of K))) ⟶ Over.mk c => p ≫ f)) :
    UniversallyInjective f.left := by
  let g : X ⟶ Y := f.left
  have hgbase : g ≫ d = c := f.w
  have : IsProper (g ≫ d) := by rw [hgbase]; infer_instance
  have : IsProper g := IsProper.of_comp g d
  let b : pullback g g ⟶ Spec (CommRingCat.of K) :=
    pullback.fst g g ≫ c
  have : LocallyOfFiniteType b := inferInstance
  have : JacobsonSpace ↥(pullback g g : Scheme.{u}) :=
    LocallyOfFiniteType.jacobsonSpace b
  rw [UniversallyInjective.iff_diagonal]
  apply surjective_of_contains_closedPoints (pullback.diagonal g)
  intro z hz
  let q : Spec (CommRingCat.of K) ⟶ pullback g g :=
    pointOfClosedPoint b z hz
  have hq : q ≫ b = 𝟙 _ := pointOfClosedPoint_comp b z hz
  have hbase : pullback.snd g g ≫ c = pullback.fst g g ≫ c := by
    calc
      pullback.snd g g ≫ c =
          (pullback.snd g g ≫ g) ≫ d := by rw [Category.assoc, hgbase]
      _ = (pullback.fst g g ≫ g) ≫ d :=
        congrArg (fun r => r ≫ d) (pullback.condition (f := g) (g := g)).symm
      _ = pullback.fst g g ≫ c := by rw [Category.assoc, hgbase]
  let p₁ : Over.mk (𝟙 (Spec (CommRingCat.of K))) ⟶ Over.mk c :=
    Over.homMk (q ≫ pullback.fst g g) (by
      rw [Category.assoc]
      exact hq)
  let p₂ : Over.mk (𝟙 (Spec (CommRingCat.of K))) ⟶ Over.mk c :=
    Over.homMk (q ≫ pullback.snd g g) (by
      change (q ≫ pullback.snd g g) ≫ c = 𝟙 _
      rw [Category.assoc, hbase]
      exact hq)
  have hp : p₁ ≫ f = p₂ ≫ f := by
    apply Over.OverMorphism.ext
    change (q ≫ pullback.fst g g) ≫ g =
      (q ≫ pullback.snd g g) ≫ g
    rw [Category.assoc, Category.assoc, pullback.condition]
  have heq : q ≫ pullback.fst g g = q ≫ pullback.snd g g :=
    congrArg Over.Hom.left (h hp)
  have hdiag : (q ≫ pullback.fst g g) ≫ pullback.diagonal g = q := by
    apply pullback.hom_ext
    · rw [Category.assoc, pullback.diagonal_fst, Category.comp_id]
    · rw [Category.assoc, pullback.diagonal_snd, Category.comp_id, heq]
  refine ⟨(q ≫ pullback.fst g g) (IsLocalRing.closedPoint K), ?_⟩
  calc
    pullback.diagonal g
        ((q ≫ pullback.fst g g) (IsLocalRing.closedPoint K)) =
        ((q ≫ pullback.fst g g) ≫ pullback.diagonal g)
          (IsLocalRing.closedPoint K) :=
      (Scheme.Hom.comp_apply (q ≫ pullback.fst g g) (pullback.diagonal g)
        (IsLocalRing.closedPoint K)).symm
    _ = q (IsLocalRing.closedPoint K) :=
      congrArg (fun r => r (IsLocalRing.closedPoint K)) hdiag
    _ = z := pointOfClosedPoint_apply b z hz (IsLocalRing.closedPoint K)
theorem

residueFieldMap_isIso_of_universallyInjective_charZero

L150 ↗
AlgebraicGeometry.residueFieldMap_isIso_of_universallyInjective_charZero
Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
namespace AlgebraicGeometry
universe u
Lean source · statement
theorem residueFieldMap_isIso_of_universallyInjective_charZero
    {K : Type u} [Field K] [CharZero K] {X Y : Scheme.{u}}
    (d : Y ⟶ Spec (CommRingCat.of K)) (f : X ⟶ Y) [UniversallyInjective f]
    (x : X) : IsIso (f.residueFieldMap x)
theorem

residue_genericPoint_isIso

L169 ↗
AlgebraicGeometry.residue_genericPoint_isIso
Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
namespace AlgebraicGeometry
universe u
Lean source · statement
theorem residue_genericPoint_isIso (X : Scheme.{u}) [IsIntegral X] :
    IsIso (X.residue (genericPoint X))
theorem

isIso_of_bijective_points_of_charZero

L177 ↗
AlgebraicGeometry.Scheme.Hom.isIso_of_bijective_points_of_charZero
Documentation

A morphism from an integral proper smooth curve to an integral proper smooth scheme over an algebraically closed field of characteristic zero is an isomorphism if its actual map on rational points is bijective.

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
namespace AlgebraicGeometry
universe u
Lean source · full declaration
theorem Scheme.Hom.isIso_of_bijective_points_of_charZero
    {K : Type u} [Field K] [IsAlgClosed K] [CharZero K] {X Y : Scheme.{u}}
    (c : X ⟶ Spec (CommRingCat.of K)) (d : Y ⟶ Spec (CommRingCat.of K))
    [IsIntegral X] [IsProper c] [SmoothOfRelativeDimension 1 c]
    [IsIntegral Y] [IsProper d] [Smooth d] (f : Over.mk c ⟶ Over.mk d)
    (h : Function.Bijective
      (fun p : Over.mk (𝟙 (Spec (CommRingCat.of K))) ⟶ Over.mk c => p ≫ f)) :
    IsIso f.left := by
  let g : X ⟶ Y := f.left
  have hgbase : g ≫ d = c := f.w
  have : Surjective g := surjective_of_surjective_rationalPoints c d f h.2
  have : UniversallyInjective g := universallyInjective_of_injective_rationalPoints c d f h.1
  have hη : g (genericPoint X) = genericPoint Y := by
    apply IsGenericPoint.eq _ (genericPoint_spec Y)
    have hg := (genericPoint_spec X).image g.continuous
    rw [Set.image_univ, g.surjective.range_eq, closure_univ] at hg
    exact hg
  have : IsIso (X.residue (genericPoint X)) := residue_genericPoint_isIso X
  have : IsIso (Y.residue (g (genericPoint X))) := by
    rw [hη]
    exact residue_genericPoint_isIso Y
  have : IsIso (g.residueFieldMap (genericPoint X)) :=
    residueFieldMap_isIso_of_universallyInjective_charZero d g (genericPoint X)
  have hcomp : IsIso (g.stalkMap (genericPoint X) ≫ X.residue (genericPoint X)) := by
    rw [← Scheme.residue_residueFieldMap]
    infer_instance
  have : IsIso (g.stalkMap (genericPoint X)) :=
    (isIso_comp_right_iff (g.stalkMap (genericPoint X))
      (X.residue (genericPoint X))).mp hcomp
  let eη : Y.presheaf.stalk (g (genericPoint X)) ≅ Y.functionField :=
    Y.presheaf.stalkCongr (Inseparable.of_eq hη)
  let ψ : X.functionField ≅ Y.functionField :=
    (asIso (g.stalkMap (genericPoint X))).symm ≪≫ eη
  have hgeneric : Spec.map ψ.inv ≫ Y.fromSpecStalk (genericPoint Y) =
      X.fromSpecStalk (genericPoint X) ≫ g := by
    change Spec.map (eη.inv ≫ g.stalkMap (genericPoint X)) ≫
      Y.fromSpecStalk (genericPoint Y) = _
    rw [Spec.map_comp, Category.assoc]
    change Spec.map (g.stalkMap (genericPoint X)) ≫
      Spec.map (Y.presheaf.stalkSpecializes (Inseparable.of_eq hη).specializes) ≫
        Y.fromSpecStalk (genericPoint Y) = _
    rw [Scheme.SpecMap_stalkSpecializes_fromSpecStalk, Scheme.SpecMap_stalkMap_fromSpecStalk]
  have hψ : Spec.map ψ.inv ≫ Y.fromSpecStalk (genericPoint Y) ≫ d =
      X.fromSpecStalk (genericPoint X) ≫ c := by
    rw [← Category.assoc, hgeneric, Category.assoc, hgbase]
  obtain ⟨U, hU, j, hjopen, hjbase, hjgeneric⟩ :=
    Scheme.exists_isOpenImmersion_of_functionField_iso c d ψ hψ
  have : IsOpenImmersion j := hjopen
  obtain ⟨e, hebase, heU⟩ :=
    Scheme.exists_iso_comp_eq_of_isOpenImmersion_of_isProper c d U ⟨genericPoint X, hU⟩ j hjbase
  have hegeneric : X.fromSpecStalk (genericPoint X) ≫ e.hom =
      X.fromSpecStalk (genericPoint X) ≫ g := by
    calc
      X.fromSpecStalk (genericPoint X) ≫ e.hom =
          (U.fromSpecStalkOfMem (genericPoint X) hU ≫ U.ι) ≫ e.hom :=
        congrArg (fun r => r ≫ e.hom)
          (U.fromSpecStalkOfMem_ι (genericPoint X) hU).symm
      _ = U.fromSpecStalkOfMem (genericPoint X) hU ≫ j := by rw [Category.assoc, heU]
      _ = Spec.map ψ.inv ≫ Y.fromSpecStalk (genericPoint Y) := hjgeneric
      _ = X.fromSpecStalk (genericPoint X) ≫ g := hgeneric
  have : IsDominant (X.fromSpecStalk (genericPoint X)) := by
    have hd : Dense ({genericPoint X} : Set X) :=
      dense_iff_closure_eq.mpr (genericPoint_spec X).def
    refine ⟨hd.mono (Set.singleton_subset_iff.mpr ?_)⟩
    exact ⟨IsLocalRing.closedPoint X.functionField, Scheme.fromSpecStalk_closedPoint⟩
  have he : e.hom = g :=
    ext_of_isDominant_of_isSeparated d (hebase.trans hgbase.symm)
      (X.fromSpecStalk (genericPoint X)) hegeneric
  change IsIso g
  rw [← he]
  infer_instance

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.