Module

IsPullback_baseChangeSnd.lean

Nyll.AlgebraicCurves.Geometry.Picard.IsPullback_baseChangeSnd

1 declaration indexed from sourceView source ↗

Module documentation

The pullback square associated with baseChangeSnd along a relative scheme morphism.

Imports2

Imported by4

theorem

isPullback_baseChangeSnd

L30 ↗

AlgebraicGeometry.RelPicard.isPullback_baseChangeSnd

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs.IsPullback_baseChangeSnd
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra

Lean source · statement

theorem _root_.AlgebraicGeometry.RelPicard.isPullback_baseChangeSnd
    {R : Type u} [CommRing R] {C T T' : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)} (ψ : SchemeHomOver t' t) :
    IsPullback (baseChangeSnd c ψ) (pullback.snd c t') (pullback.snd c t) ψ.1

Module documentation

Declarations

isPullback_baseChangeSnd