AlgebraicGeometry.RelPicard.RigidifiedLineBundle.nonempty_iso_unit_pullback_rigSection_of_squareZero_of_pullback_iso
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_unit_pullback_rigSection_of_squareZero_of_pullback_iso
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
NeronModelInfra TensorProduct
open RigidifiedLineBundle_nonempty_iso_unit_pullback_rigSection_of_squareZero_of_pullback_iso in
with_weak_namespace _root_.AlgebraicGeometry.RelPicard.RigidifiedLineBundleLean source · statement
theorem nonempty_iso_unit_pullback_rigSection_of_squareZero_of_pullback_iso
{R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
(ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
{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)))))
(L' : (pullback c (Spec.map (CommRingCat.ofHom (algebraMap R B)))).Modules)
(hL' : Scheme.Modules.IsInvertible L')
(isoL : Nonempty ((Scheme.Modules.pullback (baseChangeSnd c ι)).obj L' ≅ M.L)) :
Nonempty
((Scheme.Modules.pullback (rigSection c (Spec.map (CommRingCat.ofHom
(algebraMap R B))) ε)).obj L'
≅ SheafOfModules.unit (Spec (CommRingCat.of B)).ringCatSheaf)