Uniqueness of morphisms to separated models

Between two models with a fixed generic-fibre identification, there is at most one morphism if the target is separated over the DVR. In particular an isomorphism extending that identification, when it exists, is unique. This does not assert existence of an extension.

Flatness makes the generic fibre schematically dense, so the total spaces need not be reduced. Proper models are separated and hence satisfy the uniqueness statement. This is the separatedness argument for morphisms of models in Q. Liu, Algebraic Geometry and Arithmetic Curves, Chapter 10.

instance TauCeti.Model.subsingleton_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} [AlgebraicGeometry.IsSeparated N.toBase] : Subsingleton (M ⟶ N)

Morphisms between models with a fixed generic-fibre identification are unique when the target is separated over the DVR. No properness or reducedness assumption on the source is needed.

instance TauCeti.Model.subsingleton_iso {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} [AlgebraicGeometry.IsSeparated N.toBase] : Subsingleton (M ≅ N)

There is at most one isomorphism of models extending their fixed generic-fibre identification when the target is separated. Existence is a separate assertion.