Module

BaseChangeFunctor.lean

Nyll.AlgebraicCurves.Geometry.Picard.BaseChangeFunctor

5 declarations indexed from sourceView source ↗

Module documentation

Base Change Functor

Imports2

Imported by1

Nyll.AlgebraicCurves.Geometry.Picard.All

def

baseChangeFunctor

L32 ↗

AlgebraicGeometry.RelPicard.baseChangeFunctor

Documentation

The native base-change functor used by the existing Picard construction. Its objects and maps share the one functorial pullback representation.

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R]

Lean source · statement

def baseChangeFunctor {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) :
    Over (Spec (CommRingCat.of R)) ⥤ Scheme.{u}

theorem

baseChangeFunctor_obj

L37 ↗

AlgebraicGeometry.RelPicard.baseChangeFunctor_obj

Documentation

The functor uses exactly the existing native pullback object.

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R]

Lean source · statement

theorem baseChangeFunctor_obj {C T : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    (t : T ⟶ Spec (CommRingCat.of R)) :
    (baseChangeFunctor c).obj (Over.mk t) = Limits.pullback c t

theorem

baseChangeFunctor_map

L42 ↗

AlgebraicGeometry.RelPicard.baseChangeFunctor_map

Documentation

The functor uses exactly the existing native base-change map.

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R]

Lean source · statement

theorem baseChangeFunctor_map {C T T' : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of R))
    {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
    (s : SchemeHomOver t' t) :
    (baseChangeFunctor c).map (schemeHomOverToOverHom s) = baseChangeSnd c s

theorem

baseChangeFunctor_map_postComp

L49 ↗

AlgebraicGeometry.RelPicard.baseChangeFunctor_map_postComp

Documentation

Composition is inherited from the same native object/map functor.

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R]

Lean source · statement

theorem baseChangeFunctor_map_postComp {C X X' T' : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of R))
    {x : X ⟶ Spec (CommRingCat.of R)} {x' : X' ⟶ Spec (CommRingCat.of R)}
    {t' : T' ⟶ Spec (CommRingCat.of R)} (φ : SchemeHomOver x x') (ψ : SchemeHomOver t' x) :
    (baseChangeFunctor c).map (schemeHomOverToOverHom ψ) ≫
        (baseChangeFunctor c).map (schemeHomOverToOverHom φ) =
      (baseChangeFunctor c).map (schemeHomOverToOverHom (postComp φ ψ))

theorem

rigSection_baseChangeFunctor

L60 ↗

AlgebraicGeometry.RelPicard.rigSection_baseChangeFunctor

Documentation

The existing rigidification square is the square of this native functor.

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R]

Lean source · statement

theorem rigSection_baseChangeFunctor {C T T' : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of R))
    {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (s : SchemeHomOver t' t) :
    rigSection c t' ε ≫ (baseChangeFunctor c).map (schemeHomOverToOverHom s) =
      s.1 ≫ rigSection c t ε

Module documentation

Base Change Functor

Declarations

baseChangeFunctor

baseChangeFunctor_obj

baseChangeFunctor_map

baseChangeFunctor_map_postComp

rigSection_baseChangeFunctor