AlgebraicGeometry.RelPicard.RigidifiedLineBundle.fibrewiseAlgEquivZero_of_pullbackAlong_openCover
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs
namespace RigidifiedLineBundle_fibrewiseAlgEquivZero_of_pullbackAlong_openCover
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
NeronModelInfra
with_weak_namespace _root_.AlgebraicGeometry.RelPicard.RigidifiedLineBundleLean source · statement
theorem fibrewiseAlgEquivZero_of_pullbackAlong_openCover
(R : Type u) [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
(ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
{T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
{ι : Type u} {U : ι → Scheme.{u}} (u : ∀ i, U i ⟶ Spec (CommRingCat.of R))
(f : ∀ i, SchemeHomOver (u i) t) [∀ i, IsOpenImmersion (f i).1]
(hf : ∀ x : T, ∃ i, x ∈ Set.range (f i).1.base)
(M : RigidifiedLineBundle c ε t) (h : ∀ i, FibrewiseAlgEquivZero (M.pullbackAlong (f i))) :
FibrewiseAlgEquivZero M