AlgebraicGeometry.Scheme.existsUnique_germToFunctionField_eq_of_iSup_eq
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.GermGluing
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
universe uLean source · statement
theorem _root_.AlgebraicGeometry.Scheme.existsUnique_germToFunctionField_eq_of_iSup_eq
{X : Scheme.{u}} [IsIntegral X] {ι : Type u} (V : ι → X.Opens) (W : X.Opens) (hV : iSup V = W)
[hW : Nonempty W] [hVi : ∀ i, Nonempty (V i)]
(f : X.functionField) (s : ∀ i, Γ(X, V i)) (hs : ∀ i, X.germToFunctionField (V i) (s i) = f) :
∃! t : Γ(X, W), X.germToFunctionField W t = f ∧
∀ i, X.presheaf.map (homOfLE (hV ▸ le_iSup V i : V i ≤ W)).op t = s i