AlgebraicGeometry.RelPicard.nonempty_thetaBundle_iso_of_iso
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Nonempty_thetaBundle_iso_of_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfraLean source · statement
theorem _root_.AlgebraicGeometry.RelPicard.nonempty_thetaBundle_iso_of_iso
{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))
(M M' : RigidifiedLineBundle c ε t) (e : M.L ≅ M'.L) (r n : ℕ) :
Nonempty (thetaBundle c ε t M r n ≅ thetaBundle c ε t M' r n)