NYLL
Module

SchemeHomOverBaseChange.lean

Nyll.AlgebraicCurves.Geometry.Schemes.SchemeHomOverBaseChange
14 declarations indexed from sourceView source ↗

Module documentation

Base change of morphisms over a scheme

Morphisms commuting with their structure maps induce morphisms of the base-changed schemes. Their projections, identities, compositions, and induced module comparisons are compatible.

Imports2
Imported by9

Declarations

def

fibreRestrictAlong

L35 ↗
NeronModelInfra.fibreRestrictAlong
Documentation

Restrict a morphism over B after an arbitrary base change C ⟶ B.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace NeronModelInfra
variable {B C X Y Z : Scheme.{u}}
Lean source · statement
def fibreRestrictAlong (c : C ⟶ B) (f : X ⟶ B) (g : Y ⟶ B)
    (φ : SchemeHomOver g f) :
    SchemeHomOver (pullback.snd g c) (pullback.snd f c)
theorem

fibreRestrictAlong_coe_comp_fst

L42 ↗
NeronModelInfra.fibreRestrictAlong_coe_comp_fst
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace NeronModelInfra
variable {B C X Y Z : Scheme.{u}}
Lean source · statement
theorem fibreRestrictAlong_coe_comp_fst (c : C ⟶ B) (f : X ⟶ B) (g : Y ⟶ B)
    (φ : SchemeHomOver g f) :
    (fibreRestrictAlong c f g φ).1 ≫ pullback.fst f c = pullback.fst g c ≫ φ.1
theorem

fibreRestrictAlong_coe_comp_snd

L47 ↗
NeronModelInfra.fibreRestrictAlong_coe_comp_snd
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace NeronModelInfra
variable {B C X Y Z : Scheme.{u}}
Lean source · statement
theorem fibreRestrictAlong_coe_comp_snd (c : C ⟶ B) (f : X ⟶ B) (g : Y ⟶ B)
    (φ : SchemeHomOver g f) :
    (fibreRestrictAlong c f g φ).1 ≫ pullback.snd f c = pullback.snd g c
theorem

fibreRestrictAlong_coe_eq_pullbackMap

L52 ↗
NeronModelInfra.fibreRestrictAlong_coe_eq_pullbackMap
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace NeronModelInfra
variable {B C X Y Z : Scheme.{u}}
Lean source · statement
theorem fibreRestrictAlong_coe_eq_pullbackMap (c : C ⟶ B) (f : X ⟶ B) (g : Y ⟶ B)
    (φ : SchemeHomOver g f)
    (eq₁ : g ≫ 𝟙 B = φ.1 ≫ f) (eq₂ : c ≫ 𝟙 B = 𝟙 C ≫ c) :
    (fibreRestrictAlong c f g φ).1 =
      pullback.map g c f c φ.1 (𝟙 C) (𝟙 B) eq₁ eq₂
theorem

fibreRestrictAlong_schemeHomOverId

L61 ↗
NeronModelInfra.fibreRestrictAlong_schemeHomOverId
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace NeronModelInfra
variable {B C X Y Z : Scheme.{u}}
Lean source · statement
theorem fibreRestrictAlong_schemeHomOverId (c : C ⟶ B) (f : X ⟶ B) :
    fibreRestrictAlong c f f (schemeHomOverId f) = schemeHomOverId (pullback.snd f c)
theorem

fibreRestrictAlong_schemeHomOverComp

L68 ↗
NeronModelInfra.fibreRestrictAlong_schemeHomOverComp
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace NeronModelInfra
variable {B C X Y Z : Scheme.{u}}
Lean source · statement
theorem fibreRestrictAlong_schemeHomOverComp (c : C ⟶ B) (f : X ⟶ B)
    (g : Y ⟶ B) (e : Z ⟶ B) (ψ : SchemeHomOver e g) (φ : SchemeHomOver g f) :
    fibreRestrictAlong c f e (schemeHomOverComp ψ φ) =
      schemeHomOverComp (fibreRestrictAlong c g e ψ) (fibreRestrictAlong c f g φ)
def

specGenericFibreInclusion

L79 ↗
NeronModelInfra.specGenericFibreInclusion
Documentation

The inclusion of the generic fibre induced by an algebra R → K.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace NeronModelInfra
variable {B C X Y Z : Scheme.{u}}
variable (R K : Type u) [CommRing R] [Field K] [Algebra R K]
Lean source · statement
def specGenericFibreInclusion : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of R)
theorem

specGenericFibreInclusion_eq

L82 ↗
NeronModelInfra.specGenericFibreInclusion_eq
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace NeronModelInfra
variable {B C X Y Z : Scheme.{u}}
variable (R K : Type u) [CommRing R] [Field K] [Algebra R K]
Lean source · statement
theorem specGenericFibreInclusion_eq :
    specGenericFibreInclusion R K = Spec.map (CommRingCat.ofHom (algebraMap R K))
def

genericFibreRestrict

L89 ↗
NeronModelInfra.genericFibreRestrict
Documentation

Restrict a morphism over Spec R to the generic fibre over K.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace NeronModelInfra
variable {B C X Y Z : Scheme.{u}}
variable (R K : Type u) [CommRing R] [Field K] [Algebra R K]
variable {X Y Z : Scheme.{u}}
Lean source · statement
def genericFibreRestrict (f : X ⟶ Spec (CommRingCat.of R))
    (g : Y ⟶ Spec (CommRingCat.of R)) (φ : SchemeHomOver g f) :
    SchemeHomOver (pullback.snd g (specGenericFibreInclusion R K))
      (pullback.snd f (specGenericFibreInclusion R K))
theorem

fibreRestrictAlong_specGenericFibreInclusion

L98 ↗
NeronModelInfra.fibreRestrictAlong_specGenericFibreInclusion
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace NeronModelInfra
variable {B C X Y Z : Scheme.{u}}
variable (R K : Type u) [CommRing R] [Field K] [Algebra R K]
variable {X Y Z : Scheme.{u}}
Lean source · statement
theorem fibreRestrictAlong_specGenericFibreInclusion
    (f : X ⟶ Spec (CommRingCat.of R)) (g : Y ⟶ Spec (CommRingCat.of R))
    (φ : SchemeHomOver g f) :
    fibreRestrictAlong (specGenericFibreInclusion R K) f g φ =
      genericFibreRestrict R K f g φ
theorem

genericFibreRestrict_coe_comp_snd

L105 ↗
NeronModelInfra.genericFibreRestrict_coe_comp_snd
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace NeronModelInfra
variable {B C X Y Z : Scheme.{u}}
variable (R K : Type u) [CommRing R] [Field K] [Algebra R K]
variable {X Y Z : Scheme.{u}}
Lean source · statement
theorem genericFibreRestrict_coe_comp_snd (f : X ⟶ Spec (CommRingCat.of R))
    (g : Y ⟶ Spec (CommRingCat.of R)) (φ : SchemeHomOver g f) :
    (genericFibreRestrict R K f g φ).1 ≫ pullback.snd f (specGenericFibreInclusion R K) =
      pullback.snd g (specGenericFibreInclusion R K)
theorem

genericFibreRestrict_coe_comp_fst

L111 ↗
NeronModelInfra.genericFibreRestrict_coe_comp_fst
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace NeronModelInfra
variable {B C X Y Z : Scheme.{u}}
variable (R K : Type u) [CommRing R] [Field K] [Algebra R K]
variable {X Y Z : Scheme.{u}}
Lean source · statement
theorem genericFibreRestrict_coe_comp_fst (f : X ⟶ Spec (CommRingCat.of R))
    (g : Y ⟶ Spec (CommRingCat.of R)) (φ : SchemeHomOver g f) :
    (genericFibreRestrict R K f g φ).1 ≫ pullback.fst f (specGenericFibreInclusion R K) =
      pullback.fst g (specGenericFibreInclusion R K) ≫ φ.1
theorem

genericFibreRestrict_schemeHomOverId

L117 ↗
NeronModelInfra.genericFibreRestrict_schemeHomOverId
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace NeronModelInfra
variable {B C X Y Z : Scheme.{u}}
variable (R K : Type u) [CommRing R] [Field K] [Algebra R K]
variable {X Y Z : Scheme.{u}}
Lean source · statement
theorem genericFibreRestrict_schemeHomOverId (f : X ⟶ Spec (CommRingCat.of R)) :
    genericFibreRestrict R K f f (schemeHomOverId f) =
      schemeHomOverId (pullback.snd f (specGenericFibreInclusion R K))
theorem

genericFibreRestrict_schemeHomOverComp

L122 ↗
NeronModelInfra.genericFibreRestrict_schemeHomOverComp
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace NeronModelInfra
variable {B C X Y Z : Scheme.{u}}
variable (R K : Type u) [CommRing R] [Field K] [Algebra R K]
variable {X Y Z : Scheme.{u}}
Lean source · statement
theorem genericFibreRestrict_schemeHomOverComp
    (f : X ⟶ Spec (CommRingCat.of R)) (g : Y ⟶ Spec (CommRingCat.of R))
    (e : Z ⟶ Spec (CommRingCat.of R)) (ψ : SchemeHomOver e g) (φ : SchemeHomOver g f) :
    genericFibreRestrict R K f e (schemeHomOverComp ψ φ) =
      schemeHomOverComp (genericFibreRestrict R K g e ψ)
        (genericFibreRestrict R K f g φ)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.