AlgebraicGeometry.Scheme.Modules.nonempty_pullback_iso_of_bijective_app_of_le_opensRange
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_iso_of_bijective_app_of_le_opensRange
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
AlgebraicGeometry.Scheme.ModulesLean source · statement
theorem
_root_.AlgebraicGeometry.Scheme.Modules.nonempty_pullback_iso_of_bijective_app_of_le_opensRange
{X Y : Scheme.{u}} (f : Y ⟶ X) [IsOpenImmersion f] (M : Y.Modules) (L : X.Modules)
(π : L ⟶ (Scheme.Modules.pushforward f).obj M)
(hπ : ∀ U : X.Opens, U ≤ f.opensRange → Function.Bijective (π.app U)) :
Nonempty ((Scheme.Modules.pullback f).obj L ≅ M)