AlgebraicGeometry.Scheme.Modules.IsInvertible.nonempty_iso_pullback_pullback_of_rigidify_iso_unit
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicGeometry.Scheme.Modules.IsInvertible
universe u
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs in
open Scheme_Modules_IsInvertible_nonempty_iso_pullback_pullback_of_rigidify_iso_unit in
open _root_.CategoryTheory in
open _root_.CategoryTheory.MonoidalCategory in
open _root_.AlgebraicGeometry inLean source · statement
theorem nonempty_iso_pullback_pullback_of_rigidify_iso_unit
{T P : Scheme.{u}} (σ : T ⟶ P) (q : P ⟶ T) {L : P.Modules} (hL : Scheme.Modules.IsInvertible L)
(e : Nonempty (Scheme.Modules.rigidify σ q L ≅ SheafOfModules.unit P.ringCatSheaf)) :
Nonempty (L ≅ (Scheme.Modules.pullback q).obj ((Scheme.Modules.pullback σ).obj L))