AlgebraicGeometry.RelPicard.RigidifiedLineBundle.exists_of_squareZero_of_twoAffineOpenCover
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs
namespace RigidifiedLineBundle_exists_of_squareZero_of_twoAffineOpenCover
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
NeronModelInfra TensorProduct
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover inLean source · statement
theorem
_root_.AlgebraicGeometry.RelPicard.RigidifiedLineBundle.exists_of_squareZero_of_twoAffineOpenCover
{R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
(ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (𝒱 : C.TwoAffineOpenCover)
{B : Type u} [CommRing B] [Algebra R B] (I : Ideal B) (hI : I ^ 2 = ⊥)
(ι : SchemeHomOver
(Spec.map (CommRingCat.ofHom (algebraMap R (B ⧸ I))))
(Spec.map (CommRingCat.ofHom (algebraMap R B))))
(hι : ι.1 = Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
(M : RigidifiedLineBundle c ε (Spec.map (CommRingCat.ofHom (algebraMap R (B ⧸ I))))) :
∃ M' : RigidifiedLineBundle c ε (Spec.map (CommRingCat.ofHom (algebraMap R B))),
Nonempty ((M'.pullbackAlong ι).L ≅ M.L)