AlgebraicGeometry.RelPicard.IsAlgEquivZero.of_iso_pointsSubBasepoint
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsAlgEquivZero_of_iso_pointsSubBasepoint
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobianLean source · statement
theorem _root_.AlgebraicGeometry.RelPicard.IsAlgEquivZero.of_iso_pointsSubBasepoint
{k : Type u} [Field k] {A : Scheme.{u}} {a : A ⟶ Spec (CommRingCat.of k)}
[IsSeparated a] [SmoothOfRelativeDimension 1 a] [GeometricallyIntegral a]
[LocallyOfFiniteType a]
(ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) a) (Ps : List (SchemeHomOver (𝟙 (Spec
(CommRingCat.of k))) a))
{L : A.Modules}
(e : (Scheme.Modules.pullback (pullback.fst a (𝟙 _))).obj L ≅ pointsSubBasepointModule (a :=
a) ε Ps) :
IsAlgEquivZero a L