AlgebraicGeometry.RelPicard.RigidifiedLineBundle.subsingleton_iso_map_pullback_rigSection_comp_eq
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs
namespace RigidifiedLineBundle_subsingleton_iso_map_pullback_rigSection_comp_eq
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
NeronModelInfra
with_weak_namespace _root_.AlgebraicGeometry.RelPicard.RigidifiedLineBundleLean source · full declaration
theorem subsingleton_iso_map_pullback_rigSection_comp_eq
(R : Type u) [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
(ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
(hH0 : ∀ (A : Type u) [CommRing A] [Algebra R A],
let _ : Algebra A Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A), ⊤) :=
Scheme.TwoAffineOpenCover.algebraOfHom
(Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R A)) ⊤
Function.Bijective (algebraMap A Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R
A), ⊤)))
{T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (M M' : RigidifiedLineBundle c ε t)
(α : (Scheme.Modules.pullback (rigSection c t ε)).obj M.L ≅ SheafOfModules.unit T.ringCatSheaf)
(α' : (Scheme.Modules.pullback (rigSection c t ε)).obj M'.L ≅ SheafOfModules.unit
T.ringCatSheaf) :
Subsingleton {φ : M.L ≅ M'.L // (Scheme.Modules.pullback (rigSection c t ε)).mapIso φ ≪≫ α'
= α} :=
⟨fun a b => Subtype.ext
(AlgebraicGeometry.RelPicard.RigidifiedLineBundle.iso_eq_of_map_pullback_rigSection_comp_eq
R c ε hH0 t M M' α α' a.1 b.1 a.2 b.2)⟩