Module

StageHom.lean

Nyll.AlgebraicCurves.Geometry.Picard.StageHom

6 declarations indexed from sourceView source ↗

Module documentation

Morphisms between affine scalar-extension stages and their pullback-chart preimages.

Imports2

Imported by23

def

stageHom

L31 ↗

AlgebraicGeometry.RelPicard.LFP.stageHom

Documentation

The relative spectrum morphism induced contravariantly by an R-algebra homomorphism.

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace AlgebraicGeometry.RelPicard.LFP
open Scheme.TwoAffineOpenCover
variable (R : Type u) [CommRing R]

Lean source · statement

def stageHom {A₀ A' : Type u} [CommRing A₀] [CommRing A']
    [Algebra R A₀] [Algebra R A']
    (f : A₀ →ₐ[R] A') : SchemeHomOver (specMap R A') (specMap R A₀)

theorem

stageHom_val

L42 ↗

AlgebraicGeometry.RelPicard.LFP.stageHom_val

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace AlgebraicGeometry.RelPicard.LFP
open Scheme.TwoAffineOpenCover
variable (R : Type u) [CommRing R]

Lean source · statement

theorem stageHom_val {A₀ A' : Type u} [CommRing A₀] [CommRing A']
    [Algebra R A₀] [Algebra R A']
    (f : A₀ →ₐ[R] A') : (stageHom R f).1 = Spec.map (CommRingCat.ofHom f.toRingHom)

theorem

baseChangeSnd_fst

L55 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.baseChangeSnd_fst

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover)
    (c : C ⟶ Spec (.of R))
    {A₀ A' : Type u} [CommRing A₀] [CommRing A'] [Algebra R A₀] [Algebra R A']
    (ψ : SchemeHomOver (specMap R A') (specMap R A₀))

Lean source · statement

theorem baseChangeSnd_fst :
    RelPicard.baseChangeSnd c ψ ≫ Limits.pullback.fst c (specMap R A₀) =
      Limits.pullback.fst c (specMap R A')

theorem

baseChangeSnd_preimage_U0

L60 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.baseChangeSnd_preimage_U0

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover)
    (c : C ⟶ Spec (.of R))
    {A₀ A' : Type u} [CommRing A₀] [CommRing A'] [Algebra R A₀] [Algebra R A']
    (ψ : SchemeHomOver (specMap R A') (specMap R A₀))

Lean source · statement

theorem baseChangeSnd_preimage_U0 :
    RelPicard.baseChangeSnd c ψ ⁻¹ᵁ (𝒱.pullback c A₀).U0 = (𝒱.pullback c A').U0

theorem

baseChangeSnd_preimage_U1

L64 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.baseChangeSnd_preimage_U1

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover)
    (c : C ⟶ Spec (.of R))
    {A₀ A' : Type u} [CommRing A₀] [CommRing A'] [Algebra R A₀] [Algebra R A']
    (ψ : SchemeHomOver (specMap R A') (specMap R A₀))

Lean source · statement

theorem baseChangeSnd_preimage_U1 :
    RelPicard.baseChangeSnd c ψ ⁻¹ᵁ (𝒱.pullback c A₀).U1 = (𝒱.pullback c A').U1

theorem

baseChangeSnd_preimage_inf

L68 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.baseChangeSnd_preimage_inf

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover)
    (c : C ⟶ Spec (.of R))
    {A₀ A' : Type u} [CommRing A₀] [CommRing A'] [Algebra R A₀] [Algebra R A']
    (ψ : SchemeHomOver (specMap R A') (specMap R A₀))

Lean source · statement

theorem baseChangeSnd_preimage_inf :
    RelPicard.baseChangeSnd c ψ ⁻¹ᵁ ((𝒱.pullback c A₀).U0 ⊓ (𝒱.pullback c A₀).U1) =
      (𝒱.pullback c A').U0 ⊓ (𝒱.pullback c A').U1

Module documentation

Declarations

stageHom

stageHom_val

baseChangeSnd_fst

baseChangeSnd_preimage_U0

baseChangeSnd_preimage_U1

baseChangeSnd_preimage_inf