Scheme morphisms compatible with chosen structure morphisms form a subtype. This file constructs their identities, composition, and actions on points, and identifies them with morphisms in the over category. It also records existence and uniqueness over an isomorphism.
Scheme morphisms commuting with the specified structure morphisms to the base.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace NeronModelInfraabbrev SchemeHomOver {B Y X : Scheme.{u}} (g : Y ⟶ B) (f : X ⟶ B)The identity scheme morphism over the base.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace NeronModelInfra
variable {B Y X W : Scheme.{u}}def schemeHomOverId (f : X ⟶ B) : SchemeHomOver f fSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace NeronModelInfra
variable {B Y X W : Scheme.{u}}theorem schemeHomOverId_coe (f : X ⟶ B) : (schemeHomOverId f).1 = 𝟙 XComposition of two scheme morphisms over the base.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace NeronModelInfra
variable {B Y X W : Scheme.{u}}def schemeHomOverComp {g : Y ⟶ B} {f : X ⟶ B} {e : W ⟶ B}
(φ : SchemeHomOver g f) (ψ : SchemeHomOver f e) : SchemeHomOver g eSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace NeronModelInfra
variable {B Y X W : Scheme.{u}}theorem schemeHomOverComp_coe {g : Y ⟶ B} {f : X ⟶ B} {e : W ⟶ B}
(φ : SchemeHomOver g f) (ψ : SchemeHomOver f e) :
(schemeHomOverComp φ ψ).1 = φ.1 ≫ ψ.1Postcomposition of a base-valued point by a scheme morphism over the base.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace NeronModelInfra
variable {B Y X W : Scheme.{u}}def mapPt {T A A' : Scheme.{u}} {t : T ⟶ B} {f : A ⟶ B} {f' : A' ⟶ B}
(φ : A ⟶ A') (hφ : φ ≫ f' = f) (P : SchemeHomOver t f) : SchemeHomOver t f'Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace NeronModelInfra
variable {B Y X W : Scheme.{u}}theorem mapPt_coe {T A A' : Scheme.{u}} {t : T ⟶ B} {f : A ⟶ B} {f' : A' ⟶ B}
(φ : A ⟶ A') (hφ : φ ≫ f' = f) (P : SchemeHomOver t f) :
(mapPt φ hφ P).1 = P.1 ≫ φSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace NeronModelInfra
variable {B Y X W : Scheme.{u}}theorem schemeHomOverComp_assoc {V : Scheme.{u}} {g : Y ⟶ B} {f : X ⟶ B} {e : W ⟶ B}
{d : V ⟶ B} (φ : SchemeHomOver g f) (ψ : SchemeHomOver f e) (χ : SchemeHomOver e d) :
schemeHomOverComp (schemeHomOverComp φ ψ) χ =
schemeHomOverComp φ (schemeHomOverComp ψ χ)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace NeronModelInfra
variable {B Y X W : Scheme.{u}}theorem schemeHomOverComp_id_left {g : Y ⟶ B} {f : X ⟶ B} (φ : SchemeHomOver g f) :
schemeHomOverComp (schemeHomOverId g) φ = φSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace NeronModelInfra
variable {B Y X W : Scheme.{u}}theorem schemeHomOverComp_id_right {g : Y ⟶ B} {f : X ⟶ B} (φ : SchemeHomOver g f) :
schemeHomOverComp φ (schemeHomOverId f) = φThe over-category morphism associated to a scheme morphism over the base.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace NeronModelInfra
variable {B Y X W : Scheme.{u}}def schemeHomOverToOverHom {g : Y ⟶ B} {f : X ⟶ B}
(φ : SchemeHomOver g f) : Over.mk g ⟶ Over.mk fSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace NeronModelInfra
variable {B Y X W : Scheme.{u}}theorem schemeHomOverToOverHom_left {g : Y ⟶ B} {f : X ⟶ B}
(φ : SchemeHomOver g f) : (schemeHomOverToOverHom φ).left = φ.1The scheme morphism over the base underlying an over-category morphism.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace NeronModelInfra
variable {B Y X W : Scheme.{u}}def overHomToSchemeHomOver {g : Y ⟶ B} {f : X ⟶ B}
(h : Over.mk g ⟶ Over.mk f) : SchemeHomOver g fSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace NeronModelInfra
variable {B Y X W : Scheme.{u}}theorem overHomToSchemeHomOver_coe {g : Y ⟶ B} {f : X ⟶ B}
(h : Over.mk g ⟶ Over.mk f) : (overHomToSchemeHomOver h).1 = h.leftSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace NeronModelInfra
variable {B Y X W : Scheme.{u}}theorem overHomToSchemeHomOver_schemeHomOverToOverHom {g : Y ⟶ B} {f : X ⟶ B}
(φ : SchemeHomOver g f) : overHomToSchemeHomOver (schemeHomOverToOverHom φ) = φSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace NeronModelInfra
variable {B Y X W : Scheme.{u}}theorem schemeHomOverToOverHom_overHomToSchemeHomOver {g : Y ⟶ B} {f : X ⟶ B}
(h : Over.mk g ⟶ Over.mk f) : schemeHomOverToOverHom (overHomToSchemeHomOver h) = hThe equivalence between scheme morphisms over the base and over-category morphisms.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace NeronModelInfra
variable {B Y X W : Scheme.{u}}def schemeHomOverEquivOverHom (g : Y ⟶ B) (f : X ⟶ B) :
SchemeHomOver g f ≃ (Over.mk g ⟶ Over.mk f) where
toFun := schemeHomOverToOverHom
invFun := overHomToSchemeHomOver
left_inv := overHomToSchemeHomOver_schemeHomOverToOverHom
right_inv := schemeHomOverToOverHom_overHomToSchemeHomOverSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace NeronModelInfra
variable {B Y X W : Scheme.{u}}theorem schemeHomOverEquivOverHom_apply {g : Y ⟶ B} {f : X ⟶ B}
(φ : SchemeHomOver g f) : schemeHomOverEquivOverHom g f φ = schemeHomOverToOverHom φSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace NeronModelInfra
variable {B Y X W : Scheme.{u}}theorem schemeHomOverEquivOverHom_symm_apply {g : Y ⟶ B} {f : X ⟶ B}
(h : Over.mk g ⟶ Over.mk f) :
(schemeHomOverEquivOverHom g f).symm h = overHomToSchemeHomOver hSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace NeronModelInfra
variable {B Y X W : Scheme.{u}}theorem subsingleton_schemeHomOver_of_isIso (g : Y ⟶ B) (f : X ⟶ B)
[IsIso f] : Subsingleton (SchemeHomOver g f)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace NeronModelInfra
variable {B Y X W : Scheme.{u}}theorem nonempty_schemeHomOver_of_isIso (g : Y ⟶ B) (f : X ⟶ B)
[IsIso f] : Nonempty (SchemeHomOver g f)Precomposition of a base-valued point by a scheme morphism over the base.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace GoodReductionJacobian
open NeronModelInfradef schemeHomOverComp {B T' T A : Scheme.{u}} {t : T ⟶ B} {t' : T' ⟶ B} {f : A ⟶ B}
(ψ : T' ⟶ T) (hψ : ψ ≫ t = t') (x : SchemeHomOver t f) : SchemeHomOver t' fSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace GoodReductionJacobian
open NeronModelInfratheorem schemeHomOverComp_coe {B T' T A : Scheme.{u}} {t : T ⟶ B} {t' : T' ⟶ B} {f : A ⟶ B}
(ψ : T' ⟶ T) (hψ : ψ ≫ t = t') (x : SchemeHomOver t f) :
(schemeHomOverComp ψ hψ x).1 = ψ ≫ x.1