NYLL
Module

LocalRepresentabilityULift.lean

Nyll.SchemeTheory.LocalGeometry.LocalRepresentabilityULift
24 declarations indexed from sourceView source ↗

Module documentation

Gluing schemes from locally representable open charts

Representable open charts for a sheaf determine scheme gluing data. The glued scheme represents the sheaf through the universe-lifted Yoneda functor, with the chart maps giving the local comparison and the induced Yoneda morphism an isomorphism.

Imports9
  • Mathlib.CategoryTheory.MorphismProperty.Representable
  • Mathlib.AlgebraicGeometry.GluingOneHypercover
  • Mathlib.CategoryTheory.Sites.LocallyBijective
  • Mathlib.CategoryTheory.Limits.Shapes.Products
  • Mathlib.Tactic.Simps.Basic
  • Mathlib.Tactic.CategoryTheory.Reassoc
  • Mathlib.Tactic.DSimpPercent
  • Mathlib.Tactic.Conv
  • Mathlib.CategoryTheory.Category.Basic
Imported by16

Declarations

abbrev

presheafULift

L46 ↗
CategoryTheory.MorphismProperty.presheafULift
Documentation

The relative morphism property on presheaves defined using the universe-lifted Yoneda functor.

Source context 4 commands

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

universe w v u
open CategoryTheory Category Limits Opposite
namespace CategoryTheory.MorphismProperty
variable {C : Type u} [Category.{v} C] (P : MorphismProperty C)
Lean source · statement
abbrev presheafULift : MorphismProperty (Cᵒᵖ ⥤ Type (max w v))
lemma

presheafULift_monomorphisms_le_monomorphisms

L50 ↗
CategoryTheory.MorphismProperty.presheafULift_monomorphisms_le_monomorphisms
Source context 5 commands

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

universe w v u
open CategoryTheory Category Limits Opposite
namespace CategoryTheory.MorphismProperty
variable {C : Type u} [Category.{v} C] (P : MorphismProperty C)
variable {P}
Lean source · statement
lemma presheafULift_monomorphisms_le_monomorphisms :
    presheafULift.{w} (monomorphisms C) ≤ monomorphisms _
lemma

presheafULift_mono_of_le

L63 ↗
CategoryTheory.MorphismProperty.presheafULift_mono_of_le
Source context 6 commands

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

universe w v u
open CategoryTheory Category Limits Opposite
namespace CategoryTheory.MorphismProperty
variable {C : Type u} [Category.{v} C] (P : MorphismProperty C)
variable {P}
variable {G : Cᵒᵖ ⥤ Type (max w v)}
Lean source · statement
lemma presheafULift_mono_of_le (hP : P ≤ MorphismProperty.monomorphisms C)
    {X : C} {f : uliftYoneda.{w}.obj X ⟶ G} (hf : P.presheafULift f) : Mono f
lemma

fst'_self_eq_snd_ULift

L68 ↗
CategoryTheory.MorphismProperty.fst'_self_eq_snd_ULift
Source context 6 commands

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

universe w v u
open CategoryTheory Category Limits Opposite
namespace CategoryTheory.MorphismProperty
variable {C : Type u} [Category.{v} C] (P : MorphismProperty C)
variable {P}
variable {G : Cᵒᵖ ⥤ Type (max w v)}
Lean source · statement
lemma fst'_self_eq_snd_ULift (hP : P ≤ MorphismProperty.monomorphisms C)
    {X : C} {f : uliftYoneda.{w}.obj X ⟶ G} (hf : P.presheafULift f) :
    hf.rep.fst' f = hf.rep.snd f
lemma

isIso_fst'_self_ULift

L75 ↗
CategoryTheory.MorphismProperty.isIso_fst'_self_ULift
Source context 6 commands

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

universe w v u
open CategoryTheory Category Limits Opposite
namespace CategoryTheory.MorphismProperty
variable {C : Type u} [Category.{v} C] (P : MorphismProperty C)
variable {P}
variable {G : Cᵒᵖ ⥤ Type (max w v)}
Lean source · statement
lemma isIso_fst'_self_ULift (hP : P ≤ MorphismProperty.monomorphisms C)
    {X : C} {f : uliftYoneda.{w}.obj X ⟶ G} (hf : P.presheafULift f) : IsIso (hf.rep.fst' f)
def

tripleRotation

L98 ↗
AlgebraicGeometry.Scheme.LocalRepresentabilityULift.tripleRotation
Source context 8 commands

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

universe w v u
open CategoryTheory Category Limits Opposite
namespace AlgebraicGeometry
namespace Scheme
variable (F : Sheaf Scheme.zariskiTopology.{u} (Type (max w u)))
  {ι : Type u} {X : ι → Scheme.{u}}
  (f : (i : ι) → uliftYoneda.{w}.obj (X i) ⟶ F.obj)
  (hf : ∀ i, MorphismProperty.presheafULift.{w} @IsOpenImmersion (f i))
namespace LocalRepresentabilityULift
variable {F f} (i j k : ι)
open Functor.relativelyRepresentable
Lean source · statement
def tripleRotation :
    pullback₃ (hf i).rep (f j) (f k) ⟶ pullback₃ (hf j).rep (f k) (f i)
lemma

tripleRotation_p₁

L109 ↗
AlgebraicGeometry.Scheme.LocalRepresentabilityULift.tripleRotation_p₁
Source context 8 commands

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

universe w v u
open CategoryTheory Category Limits Opposite
namespace AlgebraicGeometry
namespace Scheme
variable (F : Sheaf Scheme.zariskiTopology.{u} (Type (max w u)))
  {ι : Type u} {X : ι → Scheme.{u}}
  (f : (i : ι) → uliftYoneda.{w}.obj (X i) ⟶ F.obj)
  (hf : ∀ i, MorphismProperty.presheafULift.{w} @IsOpenImmersion (f i))
namespace LocalRepresentabilityULift
variable {F f} (i j k : ι)
open Functor.relativelyRepresentable
Lean source · statement
lemma tripleRotation_p₁ :
    tripleRotation hf i j k ≫ pullback₃.p₁ (hf j).rep (f k) (f i) =
      pullback₃.p₂ (hf i).rep (f j) (f k)
lemma

tripleRotation_p₂

L115 ↗
AlgebraicGeometry.Scheme.LocalRepresentabilityULift.tripleRotation_p₂
Source context 8 commands

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

universe w v u
open CategoryTheory Category Limits Opposite
namespace AlgebraicGeometry
namespace Scheme
variable (F : Sheaf Scheme.zariskiTopology.{u} (Type (max w u)))
  {ι : Type u} {X : ι → Scheme.{u}}
  (f : (i : ι) → uliftYoneda.{w}.obj (X i) ⟶ F.obj)
  (hf : ∀ i, MorphismProperty.presheafULift.{w} @IsOpenImmersion (f i))
namespace LocalRepresentabilityULift
variable {F f} (i j k : ι)
open Functor.relativelyRepresentable
Lean source · statement
lemma tripleRotation_p₂ :
    tripleRotation hf i j k ≫ pullback₃.p₂ (hf j).rep (f k) (f i) =
      pullback₃.p₃ (hf i).rep (f j) (f k)
lemma

tripleRotation_p₃

L121 ↗
AlgebraicGeometry.Scheme.LocalRepresentabilityULift.tripleRotation_p₃
Source context 8 commands

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

universe w v u
open CategoryTheory Category Limits Opposite
namespace AlgebraicGeometry
namespace Scheme
variable (F : Sheaf Scheme.zariskiTopology.{u} (Type (max w u)))
  {ι : Type u} {X : ι → Scheme.{u}}
  (f : (i : ι) → uliftYoneda.{w}.obj (X i) ⟶ F.obj)
  (hf : ∀ i, MorphismProperty.presheafULift.{w} @IsOpenImmersion (f i))
namespace LocalRepresentabilityULift
variable {F f} (i j k : ι)
open Functor.relativelyRepresentable
Lean source · statement
lemma tripleRotation_p₃ :
    tripleRotation hf i j k ≫ pullback₃.p₃ (hf j).rep (f k) (f i) =
      pullback₃.p₁ (hf i).rep (f j) (f k)
def

glueData

L130 ↗
AlgebraicGeometry.Scheme.LocalRepresentabilityULift.glueData
Documentation

The scheme gluing data obtained from the locally representable open charts and their pairwise pullbacks.

Source context 8 commands

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

universe w v u
open CategoryTheory Category Limits Opposite
namespace AlgebraicGeometry
namespace Scheme
variable (F : Sheaf Scheme.zariskiTopology.{u} (Type (max w u)))
  {ι : Type u} {X : ι → Scheme.{u}}
  (f : (i : ι) → uliftYoneda.{w}.obj (X i) ⟶ F.obj)
  (hf : ∀ i, MorphismProperty.presheafULift.{w} @IsOpenImmersion (f i))
namespace LocalRepresentabilityULift
variable {F f} (i j k : ι)
open Functor.relativelyRepresentable
Lean source · full declaration
def glueData : GlueData where
  J := ι
  U := X
  V := fun (i, j) ↦ (hf i).rep.pullback (f j)
  f i j := (hf i).rep.fst' (f j)
  f_mono i j :=
    have := (hf j).property _ _ _ ((hf i).1.isPullback' (f j)).flip
    IsOpenImmersion.mono _
  f_id i := MorphismProperty.isIso_fst'_self_ULift IsOpenImmersion.le_monomorphisms (hf i)
  t i j := (hf i).rep.symmetry (hf j).rep
  t_id i := by apply (hf i).rep.hom_ext' <;>
    simp [MorphismProperty.fst'_self_eq_snd_ULift IsOpenImmersion.le_monomorphisms (hf i)]
  t' i j k := tripleRotation hf i j k
  t_fac i j k := (hf j).rep.hom_ext'
    (by
      exact (Category.assoc _ _ _).trans
        ((congrArg (fun a : pullback₃ (hf j).rep (f k) (f i) ⟶ X j =>
            tripleRotation hf i j k ≫ a)
          (pullback₃.snd_fst'_eq_p₁ (hf j).rep (f k) (f i))).trans
          ((tripleRotation_p₁ hf i j k).trans
            (congrArg (fun a : (hf i).rep.pullback (f j) ⟶ X j =>
                pullback.fst ((hf i).rep.fst' (f j)) ((hf i).rep.fst' (f k)) ≫ a)
              ((hf i).rep.symmetry_fst (hf j).rep).symm))))
    (by
      exact (Category.assoc _ _ _).trans
        ((tripleRotation_p₃ hf i j k).trans
          (congrArg (fun a : (hf i).rep.pullback (f j) ⟶ X i =>
              pullback.fst ((hf i).rep.fst' (f j)) ((hf i).rep.fst' (f k)) ≫ a)
            ((hf i).rep.symmetry_snd (hf j).rep).symm)))
  cocycle i j k := by
    change tripleRotation hf i j k ≫ tripleRotation hf j k i ≫
      tripleRotation hf k i j = 𝟙 (pullback₃ (hf i).rep (f j) (f k))
    apply pullback₃.hom_ext
    · rw [Category.assoc, Category.assoc, tripleRotation_p₁,
        tripleRotation_p₂, tripleRotation_p₃, Category.id_comp]
    · rw [Category.assoc, Category.assoc, tripleRotation_p₂,
        tripleRotation_p₃, tripleRotation_p₁, Category.id_comp]
    · rw [Category.assoc, Category.assoc, tripleRotation_p₃,
        tripleRotation_p₁, tripleRotation_p₂, Category.id_comp]
  f_open i j := (hf j).property _ _ _ ((hf i).1.isPullback' (f j)).flip
def

toGlued

L172 ↗
AlgebraicGeometry.Scheme.LocalRepresentabilityULift.toGlued
Documentation

The canonical open immersion from a chart into the scheme obtained by gluing.

Source context 8 commands

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

universe w v u
open CategoryTheory Category Limits Opposite
namespace AlgebraicGeometry
namespace Scheme
variable (F : Sheaf Scheme.zariskiTopology.{u} (Type (max w u)))
  {ι : Type u} {X : ι → Scheme.{u}}
  (f : (i : ι) → uliftYoneda.{w}.obj (X i) ⟶ F.obj)
  (hf : ∀ i, MorphismProperty.presheafULift.{w} @IsOpenImmersion (f i))
namespace LocalRepresentabilityULift
variable {F f} (i j k : ι)
open Functor.relativelyRepresentable
Lean source · statement
def toGlued (i : ι) : X i ⟶ (glueData hf).glued
instance

(anonymous instance)

L175 ↗
Source context 8 commands

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

universe w v u
open CategoryTheory Category Limits Opposite
namespace AlgebraicGeometry
namespace Scheme
variable (F : Sheaf Scheme.zariskiTopology.{u} (Type (max w u)))
  {ι : Type u} {X : ι → Scheme.{u}}
  (f : (i : ι) → uliftYoneda.{w}.obj (X i) ⟶ F.obj)
  (hf : ∀ i, MorphismProperty.presheafULift.{w} @IsOpenImmersion (f i))
namespace LocalRepresentabilityULift
variable {F f} (i j k : ι)
open Functor.relativelyRepresentable
Lean source · statement
instance : IsOpenImmersion (toGlued hf i)
def

uliftYonedaGluedToSheaf

L181 ↗
AlgebraicGeometry.Scheme.LocalRepresentabilityULift.uliftYonedaGluedToSheaf
Documentation

The morphism from the universe-lifted Yoneda sheaf of the glued scheme, defined by gluing the given local chart sections.

Source context 8 commands

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

universe w v u
open CategoryTheory Category Limits Opposite
namespace AlgebraicGeometry
namespace Scheme
variable (F : Sheaf Scheme.zariskiTopology.{u} (Type (max w u)))
  {ι : Type u} {X : ι → Scheme.{u}}
  (f : (i : ι) → uliftYoneda.{w}.obj (X i) ⟶ F.obj)
  (hf : ∀ i, MorphismProperty.presheafULift.{w} @IsOpenImmersion (f i))
namespace LocalRepresentabilityULift
variable {F f} (i j k : ι)
open Functor.relativelyRepresentable
Lean source · full declaration
def uliftYonedaGluedToSheaf :
    (GrothendieckTopology.uliftYoneda.{w} zariskiTopology).obj (glueData hf).glued ⟶ F where
  hom := uliftYonedaEquiv.symm
    ((glueData hf).sheafValGluedMk (fun i ↦ uliftYonedaEquiv (f i)) (by
      intro (i : ι) (j : ι)
      change F.obj.map ((hf i).rep.fst' (f j)).op (uliftYonedaEquiv (f i)) =
        F.obj.map (((hf j).rep.fst' (f i)).op ≫
          ((hf i).rep.symmetry (hf j).rep).op) (uliftYonedaEquiv (f j))
      rw [uliftYonedaEquiv_naturality, uliftYonedaEquiv_naturality]
      congr 1
      rw [← op_comp, Quiver.Hom.unop_op, Quiver.Hom.unop_op]
      erw [Functor.relativelyRepresentable.symmetry_fst, ((hf i).rep.isPullback' (f j)).w]))
lemma

uliftYoneda_toGlued_uliftYonedaGluedToSheaf

L195 ↗
AlgebraicGeometry.Scheme.LocalRepresentabilityULift.uliftYoneda_toGlued_uliftYonedaGluedToSheaf
Source context 8 commands

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

universe w v u
open CategoryTheory Category Limits Opposite
namespace AlgebraicGeometry
namespace Scheme
variable (F : Sheaf Scheme.zariskiTopology.{u} (Type (max w u)))
  {ι : Type u} {X : ι → Scheme.{u}}
  (f : (i : ι) → uliftYoneda.{w}.obj (X i) ⟶ F.obj)
  (hf : ∀ i, MorphismProperty.presheafULift.{w} @IsOpenImmersion (f i))
namespace LocalRepresentabilityULift
variable {F f} (i j k : ι)
open Functor.relativelyRepresentable
Lean source · statement
lemma uliftYoneda_toGlued_uliftYonedaGluedToSheaf (i : ι) :
    uliftYoneda.{w}.map (toGlued hf i) ≫ (uliftYonedaGluedToSheaf hf).hom = f i
lemma

uliftYonedaGluedToSheaf_app_toGlued

L205 ↗
AlgebraicGeometry.Scheme.LocalRepresentabilityULift.uliftYonedaGluedToSheaf_app_toGlued
Source context 8 commands

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

universe w v u
open CategoryTheory Category Limits Opposite
namespace AlgebraicGeometry
namespace Scheme
variable (F : Sheaf Scheme.zariskiTopology.{u} (Type (max w u)))
  {ι : Type u} {X : ι → Scheme.{u}}
  (f : (i : ι) → uliftYoneda.{w}.obj (X i) ⟶ F.obj)
  (hf : ∀ i, MorphismProperty.presheafULift.{w} @IsOpenImmersion (f i))
namespace LocalRepresentabilityULift
variable {F f} (i j k : ι)
open Functor.relativelyRepresentable
Lean source · statement
lemma uliftYonedaGluedToSheaf_app_toGlued {i : ι} :
    dsimp% (uliftYonedaGluedToSheaf hf).hom.app (op (X i)) ⟨toGlued hf i⟩ =
      uliftYonedaEquiv (f i)
lemma

uliftYonedaGluedToSheaf_app_comp

L217 ↗
AlgebraicGeometry.Scheme.LocalRepresentabilityULift.uliftYonedaGluedToSheaf_app_comp
Source context 8 commands

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

universe w v u
open CategoryTheory Category Limits Opposite
namespace AlgebraicGeometry
namespace Scheme
variable (F : Sheaf Scheme.zariskiTopology.{u} (Type (max w u)))
  {ι : Type u} {X : ι → Scheme.{u}}
  (f : (i : ι) → uliftYoneda.{w}.obj (X i) ⟶ F.obj)
  (hf : ∀ i, MorphismProperty.presheafULift.{w} @IsOpenImmersion (f i))
namespace LocalRepresentabilityULift
variable {F f} (i j k : ι)
open Functor.relativelyRepresentable
Lean source · statement
lemma uliftYonedaGluedToSheaf_app_comp {V U : Scheme.{u}} (γ : V ⟶ U)
    (α : U ⟶ (glueData hf).glued) :
    dsimp% (uliftYonedaGluedToSheaf hf).hom.app (op V) ⟨γ ≫ α⟩ =
      F.obj.map γ.op ((uliftYonedaGluedToSheaf hf).hom.app (op U) ⟨α⟩)
instance

instIsLocallySurjectiveUliftYonedaGluedToSheaf

L224 ↗
AlgebraicGeometry.Scheme.LocalRepresentabilityULift.instIsLocallySurjectiveUliftYonedaGluedToSheaf
Documentation

The map from the glued scheme is locally surjective when the original charts cover the sheaf.

Source context 8 commands

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

universe w v u
open CategoryTheory Category Limits Opposite
namespace AlgebraicGeometry
namespace Scheme
variable (F : Sheaf Scheme.zariskiTopology.{u} (Type (max w u)))
  {ι : Type u} {X : ι → Scheme.{u}}
  (f : (i : ι) → uliftYoneda.{w}.obj (X i) ⟶ F.obj)
  (hf : ∀ i, MorphismProperty.presheafULift.{w} @IsOpenImmersion (f i))
namespace LocalRepresentabilityULift
variable {F f} (i j k : ι)
open Functor.relativelyRepresentable
Lean source · statement
instance instIsLocallySurjectiveUliftYonedaGluedToSheaf
    [Presheaf.IsLocallySurjective Scheme.zariskiTopology (Sigma.desc f)] :
    Sheaf.IsLocallySurjective (uliftYonedaGluedToSheaf hf)
lemma

comp_toGlued_eq

L240 ↗
AlgebraicGeometry.Scheme.LocalRepresentabilityULift.comp_toGlued_eq
Source context 8 commands

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

universe w v u
open CategoryTheory Category Limits Opposite
namespace AlgebraicGeometry
namespace Scheme
variable (F : Sheaf Scheme.zariskiTopology.{u} (Type (max w u)))
  {ι : Type u} {X : ι → Scheme.{u}}
  (f : (i : ι) → uliftYoneda.{w}.obj (X i) ⟶ F.obj)
  (hf : ∀ i, MorphismProperty.presheafULift.{w} @IsOpenImmersion (f i))
namespace LocalRepresentabilityULift
variable {F f} (i j k : ι)
open Functor.relativelyRepresentable
Lean source · statement
lemma comp_toGlued_eq {U : Scheme.{u}} {i j : ι} (a : U ⟶ X i) (b : U ⟶ X j)
    (h : uliftYoneda.{w}.map a ≫ f i = uliftYoneda.{w}.map b ≫ f j) :
    a ≫ toGlued hf i = b ≫ toGlued hf j
lemma

glueData_openCover_map

L254 ↗
AlgebraicGeometry.Scheme.LocalRepresentabilityULift.glueData_openCover_map
Source context 8 commands

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

universe w v u
open CategoryTheory Category Limits Opposite
namespace AlgebraicGeometry
namespace Scheme
variable (F : Sheaf Scheme.zariskiTopology.{u} (Type (max w u)))
  {ι : Type u} {X : ι → Scheme.{u}}
  (f : (i : ι) → uliftYoneda.{w}.obj (X i) ⟶ F.obj)
  (hf : ∀ i, MorphismProperty.presheafULift.{w} @IsOpenImmersion (f i))
namespace LocalRepresentabilityULift
variable {F f} (i j k : ι)
open Functor.relativelyRepresentable
Lean source · statement
lemma glueData_openCover_map : (glueData hf).openCover.f j = toGlued hf j
instance

(anonymous instance)

L256 ↗
Source context 8 commands

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

universe w v u
open CategoryTheory Category Limits Opposite
namespace AlgebraicGeometry
namespace Scheme
variable (F : Sheaf Scheme.zariskiTopology.{u} (Type (max w u)))
  {ι : Type u} {X : ι → Scheme.{u}}
  (f : (i : ι) → uliftYoneda.{w}.obj (X i) ⟶ F.obj)
  (hf : ∀ i, MorphismProperty.presheafULift.{w} @IsOpenImmersion (f i))
namespace LocalRepresentabilityULift
variable {F f} (i j k : ι)
open Functor.relativelyRepresentable
Lean source · full declaration
instance : Sheaf.IsLocallyInjective (uliftYonedaGluedToSheaf hf) where
  equalizerSieve_mem := by
    rintro ⟨U⟩ ⟨α⟩ ⟨β⟩ h
    replace h : (uliftYonedaGluedToSheaf hf).hom.app _ ⟨α⟩ =
        (uliftYonedaGluedToSheaf hf).hom.app _ ⟨β⟩ := h
    have mem := (glueData hf).openCover.mem_grothendieckTopology
    refine GrothendieckTopology.superset_covering _ ?_
      (zariskiTopology.intersection_covering (zariskiTopology.pullback_stable α mem)
        (zariskiTopology.pullback_stable β mem))
    rintro V (γ : _ ⟶ U) ⟨⟨W₁, a, _, ⟨i⟩, fac₁⟩, ⟨W₂, b, _, ⟨j⟩, fac₂⟩⟩
    change V ⟶ X i at a
    change V ⟶ X j at b
    change a ≫ toGlued hf i = γ ≫ α at fac₁
    change b ≫ toGlued hf j = γ ≫ β at fac₂
    change ULift.up (γ ≫ α) = ULift.up (γ ≫ β)
    replace h : (uliftYonedaGluedToSheaf hf).hom.app _ ⟨γ ≫ α⟩ =
        (uliftYonedaGluedToSheaf hf).hom.app _ ⟨γ ≫ β⟩ := by
      dsimp at h; simp [h]
    rw [← fac₁, ← fac₂] at h ⊢
    apply congrArg ULift.up
    apply comp_toGlued_eq
    have hi := (uliftYonedaGluedToSheaf_app_comp hf a (toGlued hf i)).trans
      (congrArg (fun t => F.obj.map a.op t)
        (uliftYonedaGluedToSheaf_app_toGlued hf (i := i)))
    have hj := (uliftYonedaGluedToSheaf_app_comp hf b (toGlued hf j)).trans
      (congrArg (fun t => F.obj.map b.op t)
        (uliftYonedaGluedToSheaf_app_toGlued hf (i := j)))
    have hmap := hi.symm.trans (h.trans hj)
    apply uliftYonedaEquiv.{w}.injective
    have ha := uliftYonedaEquiv_naturality (X := op (X i)) (f i) a.op
    have hb := uliftYonedaEquiv_naturality (X := op (X j)) (f j) b.op
    exact ha.symm.trans (hmap.trans hb)
instance

(anonymous instance)

L291 ↗
Source context 9 commands

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

universe w v u
open CategoryTheory Category Limits Opposite
namespace AlgebraicGeometry
namespace Scheme
variable (F : Sheaf Scheme.zariskiTopology.{u} (Type (max w u)))
  {ι : Type u} {X : ι → Scheme.{u}}
  (f : (i : ι) → uliftYoneda.{w}.obj (X i) ⟶ F.obj)
  (hf : ∀ i, MorphismProperty.presheafULift.{w} @IsOpenImmersion (f i))
namespace LocalRepresentabilityULift
variable {F f} (i j k : ι)
open Functor.relativelyRepresentable
variable [Presheaf.IsLocallySurjective Scheme.zariskiTopology (Sigma.desc f)]
Lean source · statement
instance : IsIso (uliftYonedaGluedToSheaf hf)
def

uliftYonedaIsoSheaf

L297 ↗
AlgebraicGeometry.Scheme.LocalRepresentabilityULift.uliftYonedaIsoSheaf
Documentation

The isomorphism identifying the given sheaf with the universe-lifted Yoneda sheaf of the glued scheme.

Source context 9 commands

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

universe w v u
open CategoryTheory Category Limits Opposite
namespace AlgebraicGeometry
namespace Scheme
variable (F : Sheaf Scheme.zariskiTopology.{u} (Type (max w u)))
  {ι : Type u} {X : ι → Scheme.{u}}
  (f : (i : ι) → uliftYoneda.{w}.obj (X i) ⟶ F.obj)
  (hf : ∀ i, MorphismProperty.presheafULift.{w} @IsOpenImmersion (f i))
namespace LocalRepresentabilityULift
variable {F f} (i j k : ι)
open Functor.relativelyRepresentable
variable [Presheaf.IsLocallySurjective Scheme.zariskiTopology (Sigma.desc f)]
Lean source · statement
def uliftYonedaIsoSheaf :
    (GrothendieckTopology.uliftYoneda.{w} zariskiTopology).obj (glueData hf).glued ≅ F
def

representableBy

L303 ↗
AlgebraicGeometry.Scheme.LocalRepresentabilityULift.representableBy
Documentation

The representation of the underlying presheaf by the scheme obtained by gluing its open charts.

Source context 9 commands

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

universe w v u
open CategoryTheory Category Limits Opposite
namespace AlgebraicGeometry
namespace Scheme
variable (F : Sheaf Scheme.zariskiTopology.{u} (Type (max w u)))
  {ι : Type u} {X : ι → Scheme.{u}}
  (f : (i : ι) → uliftYoneda.{w}.obj (X i) ⟶ F.obj)
  (hf : ∀ i, MorphismProperty.presheafULift.{w} @IsOpenImmersion (f i))
namespace LocalRepresentabilityULift
variable {F f} (i j k : ι)
open Functor.relativelyRepresentable
variable [Presheaf.IsLocallySurjective Scheme.zariskiTopology (Sigma.desc f)]
Lean source · statement
def representableBy : F.obj.RepresentableBy (glueData hf).glued
theorem

isRepresentable

L308 ↗
AlgebraicGeometry.Scheme.LocalRepresentabilityULift.isRepresentable
Source context 10 commands

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

universe w v u
open CategoryTheory Category Limits Opposite
namespace AlgebraicGeometry
namespace Scheme
variable (F : Sheaf Scheme.zariskiTopology.{u} (Type (max w u)))
  {ι : Type u} {X : ι → Scheme.{u}}
  (f : (i : ι) → uliftYoneda.{w}.obj (X i) ⟶ F.obj)
  (hf : ∀ i, MorphismProperty.presheafULift.{w} @IsOpenImmersion (f i))
namespace LocalRepresentabilityULift
variable {F f} (i j k : ι)
open Functor.relativelyRepresentable
variable [Presheaf.IsLocallySurjective Scheme.zariskiTopology (Sigma.desc f)]
include hf in
Lean source · statement
theorem isRepresentable : F.obj.IsRepresentable

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