Models by scheme-theoretic closure

Let R be a discrete valuation ring with fraction field K, let P be a quasi-compact scheme locally of finite type over R, and let C be a closed subscheme of the generic fibre P_K. The scheme-theoretic closure of C in P is a model of C over R: it is flat over R, because its local sections embed into sections over C, on which every nonzero element of R is invertible; it is of finite presentation, because R is noetherian; and its generic fibre is C again, because C is closed in the open subscheme P_K of P. When P is proper over R, for instance a projective space ℙᴺ_R in which C is embedded, the closure is a proper model of C. This is how a projective curve over K acquires a proper model over R.

Main definitions

• TauCeti.Model.closure: the scheme-theoretic closure of C in P, as a model of C.
• TauCeti.Model.closureι: its closed immersion into P.

Main results

• TauCeti.Model.ker_closureι: the closure is the scheme-theoretic image of C → P.
• TauCeti.Model.genericι_closureι: on generic fibres, the closure restricts to C ⟶ P_K.
• TauCeti.Model.isProper_closure: the closure in a proper scheme over R is a proper model.

References

• Q. Liu, Algebraic Geometry and Arithmetic Curves, Oxford University Press, 2002: flatness over Dedekind schemes in Section 4.3, and models of curves in Chapter 10.

noncomputable def TauCeti.Model.closure {R K : Type u} [CommRing R] [Field K] [Algebra R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} {P : AlgebraicGeometry.Scheme} {toR : P ⟶ AlgebraicGeometry.Spec ↧R} (i : C ⟶ (genericFiber R K toR).left) (hi : CategoryTheory.CategoryStruct.comp i (genericFiber R K toR).hom = toK) [IsDomain R] [IsDiscreteValuationRing R] [IsFractionRing R K] [AlgebraicGeometry.IsClosedImmersion i] [AlgebraicGeometry.LocallyOfFiniteType toR] [AlgebraicGeometry.QuasiCompact toR] : Model R K C toK

The scheme-theoretic closure in P of a closed subscheme C of the generic fibre of P → Spec R, as a model of C: its total space is the scheme-theoretic image of C → P, and its generic fibre is identified with C.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.Model.closureι {R K : Type u} [CommRing R] [Field K] [Algebra R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} {P : AlgebraicGeometry.Scheme} {toR : P ⟶ AlgebraicGeometry.Spec ↧R} (i : C ⟶ (genericFiber R K toR).left) (hi : CategoryTheory.CategoryStruct.comp i (genericFiber R K toR).hom = toK) [IsDomain R] [IsDiscreteValuationRing R] [IsFractionRing R K] [AlgebraicGeometry.IsClosedImmersion i] [AlgebraicGeometry.LocallyOfFiniteType toR] [AlgebraicGeometry.QuasiCompact toR] : (closure i hi).total ⟶ P

The closed immersion of the closure model into P.

Equations

• TauCeti.Model.closureι i hi = AlgebraicGeometry.Scheme.Hom.imageι (CategoryTheory.CategoryStruct.comp i (TauCeti.genericFiberι R K toR))

instance TauCeti.Model.instIsClosedImmersionClosureι {R K : Type u} [CommRing R] [Field K] [Algebra R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} {P : AlgebraicGeometry.Scheme} {toR : P ⟶ AlgebraicGeometry.Spec ↧R} (i : C ⟶ (genericFiber R K toR).left) (hi : CategoryTheory.CategoryStruct.comp i (genericFiber R K toR).hom = toK) [IsDomain R] [IsDiscreteValuationRing R] [IsFractionRing R K] [AlgebraicGeometry.IsClosedImmersion i] [AlgebraicGeometry.LocallyOfFiniteType toR] [AlgebraicGeometry.QuasiCompact toR] : AlgebraicGeometry.IsClosedImmersion (closureι i hi)

@[simp]

theorem TauCeti.Model.closureι_toBase {R K : Type u} [CommRing R] [Field K] [Algebra R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} {P : AlgebraicGeometry.Scheme} {toR : P ⟶ AlgebraicGeometry.Spec ↧R} (i : C ⟶ (genericFiber R K toR).left) (hi : CategoryTheory.CategoryStruct.comp i (genericFiber R K toR).hom = toK) [IsDomain R] [IsDiscreteValuationRing R] [IsFractionRing R K] [AlgebraicGeometry.IsClosedImmersion i] [AlgebraicGeometry.LocallyOfFiniteType toR] [AlgebraicGeometry.QuasiCompact toR] : CategoryTheory.CategoryStruct.comp (closureι i hi) toR = (closure i hi).toBase

The structure morphism of the closure model is the restriction of that of P.

@[simp]

theorem TauCeti.Model.closureι_toBase_assoc {R K : Type u} [CommRing R] [Field K] [Algebra R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} {P : AlgebraicGeometry.Scheme} {toR : P ⟶ AlgebraicGeometry.Spec ↧R} (i : C ⟶ (genericFiber R K toR).left) (hi : CategoryTheory.CategoryStruct.comp i (genericFiber R K toR).hom = toK) [IsDomain R] [IsDiscreteValuationRing R] [IsFractionRing R K] [AlgebraicGeometry.IsClosedImmersion i] [AlgebraicGeometry.LocallyOfFiniteType toR] [AlgebraicGeometry.QuasiCompact toR] {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) : CategoryTheory.CategoryStruct.comp (closureι i hi) (CategoryTheory.CategoryStruct.comp toR h) = CategoryTheory.CategoryStruct.comp (closure i hi).toBase h

The structure morphism of the closure model is the restriction of that of P.

@[simp]

theorem TauCeti.Model.ker_closureι {R K : Type u} [CommRing R] [Field K] [Algebra R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} {P : AlgebraicGeometry.Scheme} {toR : P ⟶ AlgebraicGeometry.Spec ↧R} (i : C ⟶ (genericFiber R K toR).left) (hi : CategoryTheory.CategoryStruct.comp i (genericFiber R K toR).hom = toK) [IsDomain R] [IsDiscreteValuationRing R] [IsFractionRing R K] [AlgebraicGeometry.IsClosedImmersion i] [AlgebraicGeometry.LocallyOfFiniteType toR] [AlgebraicGeometry.QuasiCompact toR] : AlgebraicGeometry.Scheme.Hom.ker (closureι i hi) = AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.CategoryStruct.comp i (genericFiberι R K toR))

The closure model is the scheme-theoretic image of C in P: its ideal sheaf in P is the kernel of C → P.

@[simp]

theorem TauCeti.Model.genericι_closureι {R K : Type u} [CommRing R] [Field K] [Algebra R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} {P : AlgebraicGeometry.Scheme} {toR : P ⟶ AlgebraicGeometry.Spec ↧R} (i : C ⟶ (genericFiber R K toR).left) (hi : CategoryTheory.CategoryStruct.comp i (genericFiber R K toR).hom = toK) [IsDomain R] [IsDiscreteValuationRing R] [IsFractionRing R K] [AlgebraicGeometry.IsClosedImmersion i] [AlgebraicGeometry.LocallyOfFiniteType toR] [AlgebraicGeometry.QuasiCompact toR] : CategoryTheory.CategoryStruct.comp (closure i hi).genericι (closureι i hi) = CategoryTheory.CategoryStruct.comp i (genericFiberι R K toR)

On generic fibres, the inclusion of the closure model into P restricts to the inclusion of C into the generic fibre of P.

@[simp]

theorem TauCeti.Model.genericι_closureι_assoc {R K : Type u} [CommRing R] [Field K] [Algebra R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} {P : AlgebraicGeometry.Scheme} {toR : P ⟶ AlgebraicGeometry.Spec ↧R} (i : C ⟶ (genericFiber R K toR).left) (hi : CategoryTheory.CategoryStruct.comp i (genericFiber R K toR).hom = toK) [IsDomain R] [IsDiscreteValuationRing R] [IsFractionRing R K] [AlgebraicGeometry.IsClosedImmersion i] [AlgebraicGeometry.LocallyOfFiniteType toR] [AlgebraicGeometry.QuasiCompact toR] {Z : AlgebraicGeometry.Scheme} (h : P ⟶ Z) : CategoryTheory.CategoryStruct.comp (closure i hi).genericι (CategoryTheory.CategoryStruct.comp (closureι i hi) h) = CategoryTheory.CategoryStruct.comp i (CategoryTheory.CategoryStruct.comp (genericFiberι R K toR) h)

On generic fibres, the inclusion of the closure model into P restricts to the inclusion of C into the generic fibre of P.

theorem TauCeti.Model.isProper_closure {R K : Type u} [CommRing R] [Field K] [Algebra R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} {P : AlgebraicGeometry.Scheme} {toR : P ⟶ AlgebraicGeometry.Spec ↧R} (i : C ⟶ (genericFiber R K toR).left) (hi : CategoryTheory.CategoryStruct.comp i (genericFiber R K toR).hom = toK) [IsDomain R] [IsDiscreteValuationRing R] [IsFractionRing R K] [AlgebraicGeometry.IsClosedImmersion i] [AlgebraicGeometry.IsProper toR] : (closure i hi).IsProper

The closure of C in a proper scheme over R is a proper model of C.