NYLL
Module

Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2
14 declarations indexed from sourceView source ↗

Module documentation

Local frames from a pullback trivialization

An isomorphism from the pullback to an open subscheme to its unit module supplies a frame on that open subset, compatible with further restriction.

Imports3
Imported by2

Declarations

structure

TrivializationBelow

L62 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2.PresheafOfModules.FrameBridge.TrivializationBelow
Documentation

A compatible choice of generators trivializing a presheaf below an object.

Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
noncomputable section
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace FrameBridge
open Opposite
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))
Lean source · full declaration
structure TrivializationBelow (X₀ : Cᵒᵖ) where
  /-- The generator assigned to each restriction of the fixed object. -/
  gen : ∀ {Y : Cᵒᵖ} (_ : X₀ ⟶ Y), F.obj Y
  /-- Restriction maps carry each chosen generator to the next one. -/
  compat : ∀ {Y Z : Cᵒᵖ} (f : X₀ ⟶ Y) (g : Y ⟶ Z), F.map g (gen f) = gen (f ≫ g)
  /-- Multiplication by each generator is a bijection. -/
  bij : ∀ {Y : Cᵒᵖ} (f : X₀ ⟶ Y), Function.Bijective (fun a : R.obj Y => a • gen f)
def

restrictRingCatSheafHom

L106 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameBridge.restrictRingCatSheafHom
Documentation

The structure-sheaf map used to restrict modules to an open subscheme.

Source context 22 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameBridge
open TopologicalSpace Opposite PresheafOfModules.FrameBridge
variable {X : Scheme.{u}}
variable (U : X.Opens)
Lean source · statement
def restrictRingCatSheafHom : (U : Scheme.{u}).ringCatSheaf ⟶
    (U.ι.opensFunctor.sheafPushforwardContinuous RingCat.{u}
      (Opens.grothendieckTopology (U : Scheme.{u})) (Opens.grothendieckTopology X)).obj
        X.ringCatSheaf
def

restrictFunctor'

L113 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameBridge.restrictFunctor'
Documentation

Restriction of modules using the inclusion of an open subscheme.

Source context 22 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameBridge
open TopologicalSpace Opposite PresheafOfModules.FrameBridge
variable {X : Scheme.{u}}
variable (U : X.Opens)
Lean source · statement
def restrictFunctor' : X.Modules ⥤ (U : Scheme.{u}).Modules
lemma

restrictFunctor'_eq

L116 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameBridge.restrictFunctor'_eq
Source context 22 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameBridge
open TopologicalSpace Opposite PresheafOfModules.FrameBridge
variable {X : Scheme.{u}}
variable (U : X.Opens)
Lean source · statement
lemma restrictFunctor'_eq : restrictFunctor' U = Modules.restrictFunctor U.ι
def

restrictFunctor'IsoPullback

L125 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameBridge.restrictFunctor'IsoPullback
Documentation

Restriction to an open subscheme identifies with pullback.

Source context 22 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameBridge
open TopologicalSpace Opposite PresheafOfModules.FrameBridge
variable {X : Scheme.{u}}
variable (U : X.Opens)
Lean source · statement
def restrictFunctor'IsoPullback : restrictFunctor' U ≅ Modules.pullback U.ι
lemma

image_preimage_of_le

L130 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameBridge.image_preimage_of_le
Source context 23 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameBridge
open TopologicalSpace Opposite PresheafOfModules.FrameBridge
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
Lean source · statement
lemma image_preimage_of_le {V : X.Opens} (h : V ≤ U) : U.ι ''ᵁ (U.ι ⁻¹ᵁ V) = V
def

gen₀

L139 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameBridge.gen₀
Documentation

The local generator obtained by transporting the unit section.

Source context 25 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameBridge
open TopologicalSpace Opposite PresheafOfModules.FrameBridge
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
section
variable (e : (restrictFunctor' U).obj L ≅ SheafOfModules.unit (U : Scheme.{u}).ringCatSheaf)
Lean source · statement
def gen₀ (W : (U : Scheme.{u}).Opens) : Γ(L, U.ι ''ᵁ W)
lemma

gen₀_spec

L142 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameBridge.gen₀_spec
Source context 25 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameBridge
open TopologicalSpace Opposite PresheafOfModules.FrameBridge
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
section
variable (e : (restrictFunctor' U).obj L ≅ SheafOfModules.unit (U : Scheme.{u}).ringCatSheaf)
Lean source · statement
lemma gen₀_spec (W : (U : Scheme.{u}).Opens) (b : Γ(X, U.ι ''ᵁ W)) :
    (e.inv.val.app (op W)).hom b = b • gen₀ L e W
lemma

gen₀_bijective

L149 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameBridge.gen₀_bijective
Source context 25 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameBridge
open TopologicalSpace Opposite PresheafOfModules.FrameBridge
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
section
variable (e : (restrictFunctor' U).obj L ≅ SheafOfModules.unit (U : Scheme.{u}).ringCatSheaf)
Lean source · full declaration
lemma gen₀_bijective (W : (U : Scheme.{u}).Opens) :
    Function.Bijective (fun b : Γ(X, U.ι ''ᵁ W) => b • gen₀ L e W) := by
  have h : Function.Bijective ((e.inv.val.app (op W)).hom) := by
    refine Function.bijective_iff_has_inverse.2 ⟨(e.hom.val.app (op W)).hom, fun b => ?_, fun m =>
      ?_⟩
    · exact congr($(e.inv_hom_id).val.app (op W) |>.hom b)
    · exact congr($(e.hom_inv_id).val.app (op W) |>.hom m)
  exact (funext (gen₀_spec L e W) ▸ h :)
lemma

gen₀_map

L158 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameBridge.gen₀_map
Source context 25 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameBridge
open TopologicalSpace Opposite PresheafOfModules.FrameBridge
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
section
variable (e : (restrictFunctor' U).obj L ≅ SheafOfModules.unit (U : Scheme.{u}).ringCatSheaf)
Lean source · statement
lemma gen₀_map {W W' : (U : Scheme.{u}).Opens} (i : W' ⟶ W) :
    L.val.map (U.ι.opensFunctor.map i).op (gen₀ L e W) = gen₀ L e W'
lemma

bijective_smul_map_eqToHom

L166 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameBridge.bijective_smul_map_eqToHom
Source context 26 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameBridge
open TopologicalSpace Opposite PresheafOfModules.FrameBridge
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
section
variable (e : (restrictFunctor' U).obj L ≅ SheafOfModules.unit (U : Scheme.{u}).ringCatSheaf)
omit e in
Lean source · full declaration
lemma bijective_smul_map_eqToHom {A B : X.Opens} (q : A = B) (t : Γ(L, A))
    (h : Function.Bijective (fun b : Γ(X, A) => b • t)) :
    Function.Bijective (fun a : Γ(X, B) =>
      a • (show Γ(L, B) from L.val.map (eqToHom q.symm : B ⟶ A).op t)) := by
  subst q
  have e1 : L.val.map (eqToHom (rfl : A = A) : A ⟶ A).op t = t := by
    rw [eqToHom_refl, op_id]
    exact PresheafOfModules.InternalHom.map_id_apply (R := X.sheaf.obj) L.val _ _
  simpa only [e1] using h
def

trivializationBelow

L177 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameBridge.trivializationBelow
Documentation

The compatible generators induced by a trivialization on an open subscheme.

Source context 25 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameBridge
open TopologicalSpace Opposite PresheafOfModules.FrameBridge
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
section
variable (e : (restrictFunctor' U).obj L ≅ SheafOfModules.unit (U : Scheme.{u}).ringCatSheaf)
Lean source · full declaration
def trivializationBelow : TrivializationBelow L.val (op U) where
  gen {Y} f := L.val.map (eqToHom (image_preimage_of_le (U := U) f.unop.le).symm :
      Y.unop ⟶ U.ι ''ᵁ (U.ι ⁻¹ᵁ Y.unop)).op (gen₀ L e (U.ι ⁻¹ᵁ Y.unop))
  compat {Y Z} f g := by
    have hle : U.ι ⁻¹ᵁ Z.unop ≤ U.ι ⁻¹ᵁ Y.unop := fun x hx => g.unop.le hx
    dsimp only
    rw [← gen₀_map L e (homOfLE hle)]
    erw [← PresheafOfModules.map_comp_apply, ← PresheafOfModules.map_comp_apply]
    exact congrFun (congrArg
      (fun φ : (op (U.ι ''ᵁ (U.ι ⁻¹ᵁ Y.unop)) ⟶ Z) =>
        ((L.val.map φ).hom : L.val.obj (op (U.ι ''ᵁ (U.ι ⁻¹ᵁ Y.unop))) → L.val.obj Z))
      (Subsingleton.elim _ _)) _
  bij {Y} f := bijective_smul_map_eqToHom L (image_preimage_of_le (U := U) f.unop.le) _
    (gen₀_bijective L e _)
theorem

exists_isFrameOn_of_pullback_iso_unit

L197 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2.AlgebraicGeometry.Scheme.Modules.exists_isFrameOn_of_pullback_iso_unit
Source context 19 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open FrameBridge in
Lean source · statement
theorem exists_isFrameOn_of_pullback_iso_unit {X : Scheme.{u}} {M : X.Modules} (U : X.Opens)
    (eU : (Modules.pullback U.ι).obj M ≅ SheafOfModules.unit (U : Scheme.{u}).ringCatSheaf) :
    ∃ s : Γ(M, U), IsFrameOn s U
theorem

exists_isFrameOn_of_pullback_iso_unit_monoidalV2

L218 ↗
AlgebraicGeometry.Scheme.Modules.exists_isFrameOn_of_pullback_iso_unit_monoidalV2
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
open _root_.AlgebraicGeometry in
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.exists_isFrameOn_of_pullback_iso_unit_monoidalV2
  {X : Scheme.{u}} {M : X.Modules} (U : X.Opens)
    (eU : (Scheme.Modules.pullback U.ι).obj M ≅ SheafOfModules.unit (U : Scheme.{u}).ringCatSheaf)
      :
    ∃ s : Γ(M, U), Scheme.Modules.IsFrameOn s U

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.