AlgebraicGeometry.RelPicard.RigidifiedLineBundle.iso_eq_of_map_pullback_rigSection_comp_eq
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
NeronModelInfraLean source · full declaration
theorem
_root_.AlgebraicGeometry.RelPicard.RigidifiedLineBundle.iso_eq_of_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],
letI := 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)
(φ ψ : M.L ≅ M'.L)
(hφ : (Scheme.Modules.pullback (rigSection c t ε)).mapIso φ ≪≫ α' = α)
(hψ : (Scheme.Modules.pullback (rigSection c t ε)).mapIso ψ ≪≫ α' = α) :
φ = ψ :=
RigidifiedLineBundle.iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective R c ε t
(AlgebraicGeometry.bijective_appTop_pullback_snd_of_forall_bijective_algebraMap_sections R c
hH0 t).2 M M' α α' φ ψ hφ hψ