Isomorphisms of models #
This file identifies the categorical isomorphisms between models with the isomorphisms of their
total spaces. The generic-fibre condition in Model.Hom is preserved by the inverse because
base change is functorial; consequently model isomorphisms are exactly the morphisms whose total
maps are isomorphisms. This is the categorical form needed when comparing models with a fixed
generic-fibre identification.
theorem
TauCeti.Model.isIso_iff_isIso_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)
:
A morphism of models is an isomorphism exactly when its total-space map is one.
instance
TauCeti.Model.isIso_of_isIso_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.IsIso f.hom]
:
A model morphism is an isomorphism whenever its map on total spaces is one.
instance
TauCeti.Model.isIso_hom_of_isIso
{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.IsIso f]
: