AlgebraicGeometry.RelPicard.RigidifiedLineBundle.fibrewiseAlgEquivZero_of_pullback_finite_faithfullyFlat
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FibrewiseDescent
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve NeronModelInfra
open scoped TensorProduct
with_weak_namespace _root_.AlgebraicGeometry.RelPicard.RigidifiedLineBundleLean source · statement
theorem fibrewiseAlgEquivZero_of_pullback_finite_faithfullyFlat
(R : Type u) [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
(ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
(R' : Type u) [CommRing R'] [Algebra R R'] [Module.Finite R R'] [Module.FaithfullyFlat R R']
{T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (M : RigidifiedLineBundle c ε t)
(h : FibrewiseAlgEquivZero (M.pullbackAlong
⟨pullback.fst t (specMap R R'), pullback.condition⟩)) :
FibrewiseAlgEquivZero M