AlgebraicGeometry.Scheme.Modules.eq_of_forall_map_homOfLE_eq_and_exists_of_compatible
Sections of a scheme module satisfy separatedness and gluing on an open cover.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.ModulesLean source · statement
theorem eq_of_forall_map_homOfLE_eq_and_exists_of_compatible
{X : Scheme.{u}} (M : X.Modules) {ι : Type u} (U : ι → X.Opens) (V : X.Opens)
(hUV : ∀ i, U i ≤ V) (hV : V ≤ ⨆ i, U i) :
(∀ s t : Γ(M, V),
(∀ i, M.presheaf.map (homOfLE (hUV i)).op s =
M.presheaf.map (homOfLE (hUV i)).op t) → s = t) ∧
(∀ v : ∀ i, Γ(M, U i),
(∀ i j, M.presheaf.map (homOfLE (inf_le_left : U i ⊓ U j ≤ U i)).op (v i) =
M.presheaf.map (homOfLE (inf_le_right : U i ⊓ U j ≤ U j)).op (v j)) →
∃ s : Γ(M, V), ∀ i, M.presheaf.map (homOfLE (hUV i)).op s = v i)