AlgebraicGeometry.RelEffCartierDiv.nonempty_pullback_lineBundle_pullbackAlong_iso_of_supportedIn
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicGeometry.RelEffCartierDiv
universe u
open _root_.AlgebraicCurves.RelativeDivisors.Proofs in
open RelEffCartierDiv_nonempty_pullback_lineBundle_pullbackAlong_iso_of_supportedIn in
open _root_.CategoryTheory in
open _root_.CategoryTheory.Limits in
open _root_.AlgebraicGeometry in
open _root_.AlgebraicGeometry.RelPicard in
open _root_.NeronModelInfra in
open _root_.CategoryTheory.MonoidalCategory inLean source · statement
theorem nonempty_pullback_lineBundle_pullbackAlong_iso_of_supportedIn
(R : Type u) [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) [IsSeparated c]
(U : C.Opens) [SmoothOfRelativeDimension 1 (U.ι ≫ c)]
{ρ : ℕ} (E : RelEffCartierDiv c ρ (𝟙 (Spec (CommRingCat.of R)))) (hEU : E.SupportedIn U)
⦃T T' : Scheme.{u}⦄ {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)} (ψ :
SchemeHomOver t' t) :
Nonempty ((Scheme.Modules.pullback (baseChangeSnd c ψ)).obj (E.pullbackAlong t
(Category.comp_id t)).lineBundle ≅
(E.pullbackAlong t' (Category.comp_id t')).lineBundle)