AlgebraicGeometry.Scheme.Modules.nonempty_pullback_preimage_iso_unit_of_pullback_iso_unit
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.PreimageTriviality
universe u
open CategoryTheory AlgebraicGeometryLean source · statement
theorem
_root_.AlgebraicGeometry.Scheme.Modules.nonempty_pullback_preimage_iso_unit_of_pullback_iso_unit
{X Y : Scheme.{u}} (g : Y ⟶ X) {L : X.Modules} {U : X.Opens}
(e : (Scheme.Modules.pullback U.ι).obj L ≅ SheafOfModules.unit U.toScheme.ringCatSheaf) :
Nonempty ((Scheme.Modules.pullback (g ⁻¹ᵁ U).ι).obj ((Scheme.Modules.pullback g).obj L) ≅
SheafOfModules.unit (g ⁻¹ᵁ U).toScheme.ringCatSheaf)