Base change of models over discrete valuation rings

A chosen finite extension of a discrete valuation ring carries a model to the pullback model over the chosen local ring. Its prescribed generic fibre is the scalar extension of the original curve to the extension field. The generic-fibre identification is the canonical comparison between the two ways of pulling the total space to that field.

This file constructs base change on both models and their morphisms and packages it as a functor. The construction retains the chosen generic-fibre identification, so it can be iterated when comparing models after a common finite extension.

noncomputable def TauCeti.Model.baseChange {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} (E : FiniteDVRExtension R K) (M : Model R K C toK) : Model E.localRing E.extensionField (genericFiber K E.extensionField toK).left (genericFiber K E.extensionField toK).hom

Base change of a model to the chosen local ring of a finite DVR extension.

Equations

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

@[simp]

theorem TauCeti.Model.baseChange_total {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} (E : FiniteDVRExtension R K) (M : Model R K C toK) : (baseChange E M).total = (genericFiber R E.localRing M.toBase).left

@[simp]

theorem TauCeti.Model.baseChange_toBase {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} (E : FiniteDVRExtension R K) (M : Model R K C toK) : (baseChange E M).toBase = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (genericFiber R E.localRing M.toBase).hom

noncomputable def TauCeti.Model.baseChangeGenericFiberIso {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} (E : FiniteDVRExtension R K) (M : Model R K C toK) : genericFiber E.localRing E.extensionField (baseChange E M).toBase ≅ genericFiber K E.extensionField toK

The canonical identification between the generic fibre of the pullback model and the scalar extension of the prescribed generic fibre.

Equations

• TauCeti.Model.baseChangeGenericFiberIso E M = id (TauCeti.Model.baseChangeGenericFiberIsoAux✝ E M)

@[simp]

theorem TauCeti.Model.baseChange_genericFiberIso {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} (E : FiniteDVRExtension R K) (M : Model R K C toK) : (baseChange E M).genericFiberIso = baseChangeGenericFiberIso E M

The chosen generic-fibre identification of a base-changed model is the canonical tower comparison.

noncomputable def TauCeti.Model.baseChangeMap {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} (E : FiniteDVRExtension R K) {M N : Model R K C toK} (f : M ⟶ N) : baseChange E M ⟶ baseChange E N

Base change of a morphism of models.

Equations

• TauCeti.Model.baseChangeMap E f = { hom := TauCeti.Model.baseChangeMapHom✝ E f, overBase := ⋯, genericFiber := ⋯ }

@[simp]

theorem TauCeti.Model.baseChangeMap_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} (E : FiniteDVRExtension R K) {M N : Model R K C toK} (f : M ⟶ N) : (baseChangeMap E f).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ((CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R E.localRing)))).map (CategoryTheory.Over.homMk f.hom ⋯))) (CategoryTheory.eqToHom ⋯))

The map on total spaces underlying base change of a model morphism is obtained by applying the pullback functor.

noncomputable def TauCeti.Model.baseChangeFunctor {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} (E : FiniteDVRExtension R K) : CategoryTheory.Functor (Model R K C toK) (Model E.localRing E.extensionField (genericFiber K E.extensionField toK).left (genericFiber K E.extensionField toK).hom)

Pullback to a chosen finite DVR extension defines a functor on models.

Equations

• TauCeti.Model.baseChangeFunctor E = { obj := TauCeti.Model.baseChange E, map := fun {X Y : TauCeti.Model R K C toK} => TauCeti.Model.baseChangeMap E, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem TauCeti.Model.baseChangeFunctor_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} (E : FiniteDVRExtension R K) (M : Model R K C toK) : (baseChangeFunctor E).obj M = baseChange E M

The object part of the model base-change functor is pullback of models.

@[simp]

theorem TauCeti.Model.baseChangeFunctor_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} (E : FiniteDVRExtension R K) {M N : Model R K C toK} (f : M ⟶ N) : (baseChangeFunctor E).map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (baseChangeMap E f) (CategoryTheory.eqToHom ⋯))

The morphism part of the model base-change functor is pullback of model morphisms.

theorem TauCeti.Model.isProper_baseChange {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} (E : FiniteDVRExtension R K) (M : Model R K C toK) (hM : M.IsProper) : (baseChange E M).IsProper

Proper models remain proper after base change to the chosen finite DVR extension.