Documentation

TauCeti.AlgebraicGeometry.Curves.StableReduction.Fibers

Generic fibres of models over a discrete valuation ring #

This file defines the canonical inclusion of a model's chosen generic fibre into its total space. It records compatibility with the structure morphism and proves that the inclusion is open. When the model is a family of curves, so is its generic fibre.

source
noncomputable def TauCeti.Model.genericι {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) :
C ⟶ M.total

The chosen generic fibre of a model, included into its total space.

Equations
Instances For
    source
    theorem TauCeti.Model.genericι_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) :
    M.genericι = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left M.genericFiberIso.inv) (genericFiberι R K M.toBase)

    The chosen generic-fibre inclusion is the pullback projection transported along the model's prescribed generic-fibre identification.

    source
    @[simp]
    theorem TauCeti.Model.genericι_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} (f : M ⟶ N) :
    CategoryTheory.CategoryStruct.comp M.genericι f.hom = N.genericι

    A morphism of models restricts to the prescribed identification on the generic fibre.

    source
    @[simp]
    theorem TauCeti.Model.genericι_hom_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} (f : M ⟶ N) {Z : AlgebraicGeometry.Scheme} (h : N.total ⟶ Z) :
    CategoryTheory.CategoryStruct.comp M.genericι (CategoryTheory.CategoryStruct.comp f.hom h) = CategoryTheory.CategoryStruct.comp N.genericι h

    A morphism of models restricts to the prescribed identification on the generic fibre.

    source
    @[simp]
    theorem TauCeti.Model.genericFiberIso_hom_left_genericι {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.comp (CategoryTheory.Over.Hom.left M.genericFiberIso.hom) M.genericι = genericFiberι R K M.toBase

    Precomposed with the chosen identification of the generic fibre with C, the inclusion of a model's chosen generic fibre is the canonical inclusion of the generic fibre.

    source
    @[simp]
    theorem TauCeti.Model.genericFiberIso_hom_left_genericι_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) {Z : AlgebraicGeometry.Scheme} (h : M.total ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left M.genericFiberIso.hom) (CategoryTheory.CategoryStruct.comp M.genericι h) = CategoryTheory.CategoryStruct.comp (genericFiberι R K M.toBase) h

    Precomposed with the chosen identification of the generic fibre with C, the inclusion of a model's chosen generic fibre is the canonical inclusion of the generic fibre.

    source
    @[simp]
    theorem TauCeti.Model.genericι_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} (M : Model R K C toK) :
    CategoryTheory.CategoryStruct.comp M.genericι M.toBase = CategoryTheory.CategoryStruct.comp toK (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K)))

    The inclusion of a model's chosen generic fibre lies over the fraction-field morphism.

    source
    @[simp]
    theorem TauCeti.Model.genericι_toBase_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) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) :
    CategoryTheory.CategoryStruct.comp M.genericι (CategoryTheory.CategoryStruct.comp M.toBase h) = CategoryTheory.CategoryStruct.comp toK (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K))) h)

    The inclusion of a model's chosen generic fibre lies over the fraction-field morphism.

    source
    theorem TauCeti.Model.isPullback_genericι {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.IsPullback M.genericι toK M.toBase (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K)))

    The square defining a model's chosen generic fibre is a pullback.

    source
    theorem TauCeti.Model.isOpenImmersion_genericι {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) :
    AlgebraicGeometry.IsOpenImmersion M.genericι

    A model's chosen generic fibre is an open subscheme of its total space.

    source
    theorem TauCeti.Model.familyOfCurves_toK {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) [AlgebraicGeometry.FamilyOfCurves M.toBase] :
    AlgebraicGeometry.FamilyOfCurves toK

    If a model is a family of curves, then so is its chosen generic fibre over the fraction field.