Models over discrete valuation rings

This file packages a model of a scheme over the fraction field of a discrete valuation ring. A model includes its total space, a flat morphism of finite presentation to the spectrum of the ring, and an explicit identification of its generic fibre with the prescribed scheme. Thus a morphism of models is required to induce the identity on that prescribed generic fibre.

Models form a category. Properness is deliberately kept as an additional predicate: many constructions first produce a model and establish properness separately.

structure TauCeti.Model (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (C : AlgebraicGeometry.Scheme) (toK : C ⟶ AlgebraicGeometry.Spec ↧K) : Type (u + 1)

A flat finitely presented model over a discrete valuation ring, together with an explicit identification of its generic fibre with a fixed scheme over the fraction field.

Finite presentation is recorded by Mathlib's three constituent properties: LocallyOfFinitePresentation, QuasiCompact, and QuasiSeparated.

• total : AlgebraicGeometry.Scheme

  The total space of the model.

• toBase : self.total ⟶ AlgebraicGeometry.Spec ↧R

  The structure morphism of the model.

• flat : AlgebraicGeometry.Flat self.toBase

  The structure morphism is flat.

• locallyOfFinitePresentation : AlgebraicGeometry.LocallyOfFinitePresentation self.toBase

  The structure morphism is locally of finite presentation.

• quasiCompact : AlgebraicGeometry.QuasiCompact self.toBase

  The structure morphism is quasi-compact.

• quasiSeparated : AlgebraicGeometry.QuasiSeparated self.toBase

  The structure morphism is quasi-separated.

• genericFiberIso : genericFiber R K self.toBase ≅ CategoryTheory.Over.mk toK

  The chosen identification of the generic fibre with the prescribed scheme over K.

@[reducible, inline]

abbrev TauCeti.Model.IsProper {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} (M : Model R K C toK) : Prop

Properness of the structure morphism is an additional property of a model.

Equations

• M.IsProper = AlgebraicGeometry.IsProper M.toBase

noncomputable def TauCeti.Model.baseChangeHom {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} (M : Model R K C toK) {N : Model R K C toK} (f : M.total ⟶ N.total) (overBase : CategoryTheory.CategoryStruct.comp f N.toBase = M.toBase) : (genericFiber R K M.toBase).left ⟶ (genericFiber R K N.toBase).left

The morphism on generic fibres induced by a morphism over the base.

Equations

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

theorem TauCeti.Model.baseChangeHom_def {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} (M : Model R K C toK) {N : Model R K C toK} (f : M.total ⟶ N.total) (overBase : CategoryTheory.CategoryStruct.comp f N.toBase = M.toBase) : M.baseChangeHom f overBase = CategoryTheory.Over.Hom.left ((CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K)))).map (CategoryTheory.Over.homMk f overBase))

The generic-fibre map is the underlying map obtained by applying the pullback functor.

@[simp]

theorem TauCeti.Model.baseChangeHom_genericFiberι {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} (M : Model R K C toK) {N : Model R K C toK} (f : M.total ⟶ N.total) (overBase : CategoryTheory.CategoryStruct.comp f N.toBase = M.toBase) : CategoryTheory.CategoryStruct.comp (M.baseChangeHom f overBase) (genericFiberι R K N.toBase) = CategoryTheory.CategoryStruct.comp (genericFiberι R K M.toBase) f

The induced generic-fibre morphism commutes with the projections to the total spaces.

@[simp]

theorem TauCeti.Model.baseChangeHom_genericFiberι_assoc {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} (M : Model R K C toK) {N : Model R K C toK} (f : M.total ⟶ N.total) (overBase : CategoryTheory.CategoryStruct.comp f N.toBase = M.toBase) {Z : AlgebraicGeometry.Scheme} (h : N.total ⟶ Z) : CategoryTheory.CategoryStruct.comp (M.baseChangeHom f overBase) (CategoryTheory.CategoryStruct.comp (genericFiberι R K N.toBase) h) = CategoryTheory.CategoryStruct.comp (genericFiberι R K M.toBase) (CategoryTheory.CategoryStruct.comp f h)

The induced generic-fibre morphism commutes with the projections to the total spaces.

@[simp]

theorem TauCeti.Model.baseChangeHom_toSpec {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} (M : Model R K C toK) {N : Model R K C toK} (f : M.total ⟶ N.total) (overBase : CategoryTheory.CategoryStruct.comp f N.toBase = M.toBase) : CategoryTheory.CategoryStruct.comp (M.baseChangeHom f overBase) (CategoryTheory.Limits.pullback.snd N.toBase (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K)))) = CategoryTheory.Limits.pullback.snd M.toBase (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K)))

The induced generic-fibre morphism commutes with the structure maps to Spec K.

@[simp]

theorem TauCeti.Model.baseChangeHom_toSpec_assoc {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} (M : Model R K C toK) {N : Model R K C toK} (f : M.total ⟶ N.total) (overBase : CategoryTheory.CategoryStruct.comp f N.toBase = M.toBase) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧K ⟶ Z) : CategoryTheory.CategoryStruct.comp (M.baseChangeHom f overBase) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd N.toBase (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K)))) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd M.toBase (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K)))) h

The induced generic-fibre morphism commutes with the structure maps to Spec K.

structure TauCeti.Model.Hom {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} (M N : Model R K C toK) : Type u

A morphism of models is a morphism over the DVR that respects the chosen identification of the generic fibre.

• hom : M.total ⟶ N.total

  The morphism of total spaces.

• overBase : CategoryTheory.CategoryStruct.comp self.hom N.toBase = M.toBase

  The morphism commutes with the structure maps to the DVR.

• genericFiber : CategoryTheory.CategoryStruct.comp (M.baseChangeHom self.hom ⋯) (CategoryTheory.Over.Hom.left N.genericFiberIso.hom) = CategoryTheory.Over.Hom.left M.genericFiberIso.hom

  On generic fibres, the morphism respects the chosen identifications with C.

@[simp]

theorem TauCeti.Model.Hom.overBase_assoc {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} {M N : Model R K C toK} (self : M.Hom N) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) : CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp N.toBase h) = CategoryTheory.CategoryStruct.comp M.toBase h

The morphism commutes with the structure maps to the DVR.

@[simp]

theorem TauCeti.Model.Hom.genericFiber_assoc {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} {M N : Model R K C toK} (self : M.Hom N) {Z : AlgebraicGeometry.Scheme} (h : (CategoryTheory.Over.mk toK).left ⟶ Z) : CategoryTheory.CategoryStruct.comp (M.baseChangeHom self.hom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left N.genericFiberIso.hom) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left M.genericFiberIso.hom) h

On generic fibres, the morphism respects the chosen identifications with C.

theorem TauCeti.Model.Hom.ext {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} {M N : Model R K C toK} {f g : M.Hom N} (h : f.hom = g.hom) : f = g

Model morphisms are determined by their maps on total spaces.

theorem TauCeti.Model.Hom.ext_iff {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} {M N : Model R K C toK} {f g : M.Hom N} : f = g ↔ f.hom = g.hom

@[simp]

theorem TauCeti.Model.baseChangeHom_id {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} (M : Model R K C toK) : M.baseChangeHom (CategoryTheory.CategoryStruct.id M.total) ⋯ = CategoryTheory.CategoryStruct.id (genericFiber R K M.toBase).left

Base change carries the identity of a model's total space to the identity.

@[simp]

theorem TauCeti.Model.baseChangeHom_comp {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} {M N P : Model R K C toK} (f : M.total ⟶ N.total) (g : N.total ⟶ P.total) (hf : CategoryTheory.CategoryStruct.comp f N.toBase = M.toBase) (hg : CategoryTheory.CategoryStruct.comp g P.toBase = N.toBase) : M.baseChangeHom (CategoryTheory.CategoryStruct.comp f g) ⋯ = CategoryTheory.CategoryStruct.comp (M.baseChangeHom f hf) (N.baseChangeHom g hg)

Base change carries a composite of maps over the DVR to the composite of their base changes.

@[instance_reducible]

instance TauCeti.Model.instCategory {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} : CategoryTheory.Category.{u, u + 1} (Model R K C toK)

Models of a fixed scheme over the fraction field form a category.

Equations

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

@[simp]

theorem TauCeti.Model.id_hom {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} (M : Model R K C toK) : (CategoryTheory.CategoryStruct.id M).hom = CategoryTheory.CategoryStruct.id M.total

@[simp]

theorem TauCeti.Model.comp_hom {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} {M N P : Model R K C toK} (f : M ⟶ N) (g : N ⟶ P) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

def TauCeti.Model.forget {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} : CategoryTheory.Functor (Model R K C toK) AlgebraicGeometry.Scheme

The faithful functor sending a model to its total space.

Equations

• TauCeti.Model.forget = { obj := fun (M : TauCeti.Model R K C toK) => M.total, map := fun {X Y : TauCeti.Model R K C toK} (f : X ⟶ Y) => f.hom, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem TauCeti.Model.forget_obj {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} (M : Model R K C toK) : forget.obj M = M.total

@[simp]

theorem TauCeti.Model.forget_map {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} {M N : Model R K C toK} (f : M ⟶ N) : forget.map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.eqToHom ⋯))

The map of the total-space functor is the underlying scheme morphism, transported along the object-map equalities.

instance TauCeti.Model.instFaithfulSchemeForget {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} : forget.Faithful