Module

Scheme_exists_iso_comp_eq_of_isOpenImmersion_of_isProper.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_iso_comp_eq_of_isOpenImmersion_of_isProper

8 declarations indexed from sourceView source ↗

Module documentation

Scheme exists iso comp eq of is Open Immersion of is Proper

Imports3

Imported by3

theorem

existence

L36 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_iso_comp_eq_of_isOpenImmersion_of_isProper.ProperCurveExtension.existence

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_iso_comp_eq_of_isOpenImmersion_of_isProper
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace ProperCurveExtension
variable {K : Type u} [Field K]

Lean source · statement

theorem existence {Y S : Scheme.{u}} (g : Y ⟶ S) [IsProper g] :
    ValuativeCriterion.Existence g

theorem

isSeparated_of_isSeparated_over

L42 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_iso_comp_eq_of_isOpenImmersion_of_isProper.ProperCurveExtension.isSeparated_of_isSeparated_over

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_iso_comp_eq_of_isOpenImmersion_of_isProper
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace ProperCurveExtension
variable {K : Type u} [Field K]

Lean source · statement

theorem isSeparated_of_isSeparated_over {Y : Scheme.{u}} (g : Y ⟶ Spec (.of K))
    [IsSeparated g] : Y.IsSeparated

theorem

isDominant_ι

L46 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_iso_comp_eq_of_isOpenImmersion_of_isProper.ProperCurveExtension.isDominant_ι

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_iso_comp_eq_of_isOpenImmersion_of_isProper
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace ProperCurveExtension
variable {K : Type u} [Field K]

Lean source · statement

theorem isDominant_ι {X : Scheme.{u}} [IrreducibleSpace X] (U : X.Opens)
    (hU : (U : Set X).Nonempty) : IsDominant U.ι

theorem

domain_eq_top

L57 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_iso_comp_eq_of_isOpenImmersion_of_isProper.ProperCurveExtension.domain_eq_top

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_iso_comp_eq_of_isOpenImmersion_of_isProper
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace ProperCurveExtension
variable {K : Type u} [Field K]
section Totalise
variable {X Y : Scheme.{u}} (sX : X ⟶ Spec (.of K)) (sY : Y ⟶ Spec (.of K))
  [IsIntegral X] [IsProper sY] (hval : ∀ x : X, ValuationRing (X.presheaf.stalk x))
  (f : X.PartialMap Y) (hf : f.hom ≫ sY = f.domain.ι ≫ sX)
include hval hf in

Lean source · statement

theorem domain_eq_top : f.toRationalMap.domain = ⊤

def

extend

L63 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_iso_comp_eq_of_isOpenImmersion_of_isProper.ProperCurveExtension.extend

Documentation

Extend a partial map to the whole source using its valuation-ring stalks.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_iso_comp_eq_of_isOpenImmersion_of_isProper
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace ProperCurveExtension
variable {K : Type u} [Field K]
section Totalise
variable {X Y : Scheme.{u}} (sX : X ⟶ Spec (.of K)) (sY : Y ⟶ Spec (.of K))
  [IsIntegral X] [IsProper sY] (hval : ∀ x : X, ValuationRing (X.presheaf.stalk x))
  (f : X.PartialMap Y) (hf : f.hom ≫ sY = f.domain.ι ≫ sX)

Lean source · statement

def extend : X ⟶ Y

theorem

ι_extend

L67 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_iso_comp_eq_of_isOpenImmersion_of_isProper.ProperCurveExtension.ι_extend

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_iso_comp_eq_of_isOpenImmersion_of_isProper
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace ProperCurveExtension
variable {K : Type u} [Field K]
section Totalise
variable {X Y : Scheme.{u}} (sX : X ⟶ Spec (.of K)) (sY : Y ⟶ Spec (.of K))
  [IsIntegral X] [IsProper sY] (hval : ∀ x : X, ValuationRing (X.presheaf.stalk x))
  (f : X.PartialMap Y) (hf : f.hom ≫ sY = f.domain.ι ≫ sX)

Lean source · statement

theorem ι_extend : f.domain.ι ≫ extend sX sY hval f hf = f.hom

theorem

extend_over

L83 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_iso_comp_eq_of_isOpenImmersion_of_isProper.ProperCurveExtension.extend_over

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_iso_comp_eq_of_isOpenImmersion_of_isProper
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace ProperCurveExtension
variable {K : Type u} [Field K]
section Totalise
variable {X Y : Scheme.{u}} (sX : X ⟶ Spec (.of K)) (sY : Y ⟶ Spec (.of K))
  [IsIntegral X] [IsProper sY] (hval : ∀ x : X, ValuationRing (X.presheaf.stalk x))
  (f : X.PartialMap Y) (hf : f.hom ≫ sY = f.domain.ι ≫ sX)

Lean source · statement

theorem extend_over : extend sX sY hval f hf ≫ sY = sX

theorem

exists_iso_comp_eq_of_isOpenImmersion_of_isProper

L93 ↗

AlgebraicGeometry.Scheme.exists_iso_comp_eq_of_isOpenImmersion_of_isProper

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_iso_comp_eq_of_isOpenImmersion_of_isProper
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
open ProperCurveExtension in

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.exists_iso_comp_eq_of_isOpenImmersion_of_isProper {K : Type
  u} [Field K] {C C' : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) (c' : C' ⟶ Spec (CommRingCat.of K))
    [IsIntegral C] [IsProper c] [SmoothOfRelativeDimension 1 c]
    [IsIntegral C'] [IsProper c'] [Smooth c']
    (U : C.Opens) (hU : (U : Set C).Nonempty)
    (j : (U : Scheme.{u}) ⟶ C') [IsOpenImmersion j] (hj : j ≫ c' = U.ι ≫ c) :
    ∃ e : C ≅ C', e.hom ≫ c' = c ∧ U.ι ≫ e.hom = j

Module documentation

Scheme exists iso comp eq of is Open Immersion of is Proper

Declarations