theorem
L29 ↗exists_isUnit_smul_eq
AlgebraicGeometry.Scheme.Modules.IsFrameOn.exists_isUnit_smul_eq
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isUnit_smul_eq
universe u v
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometryLean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.IsFrameOn.exists_isUnit_smul_eq
{X : Scheme.{u}} {M : X.Modules} {U : X.Opens} {s s' : Γ(M, U)} {V : X.Opens}
(hs : Scheme.Modules.IsFrameOn s V) (hs' : Scheme.Modules.IsFrameOn s' V)
{W : X.Opens} (hWU : W ≤ U) (hWV : W ≤ V) :
∃ u : Γ(X, W), IsUnit u ∧
u • M.presheaf.map (homOfLE hWU).op s = M.presheaf.map (homOfLE hWU).op s'