Equality of sections on `Scheme.OpenCover`

Stream: Is there code for X?

[Christian Merten]

Do we have something like:

import Mathlib

open AlgebraicGeometry

lemma eq_of_eq_cover {X : Scheme.{u}} (f g : Scheme.Γ.obj (op X)) (𝒰 : X.OpenCover)
    (h : ∀ i : 𝒰.J, Scheme.Γ.map (𝒰.map i).op f = Scheme.Γ.map (𝒰.map i).op g) : f = g :=
  sorry

I have tried to use docs#TopCat.Sheaf.eq_of_locally_eq', but this does not apply cleanly, because 𝒰.J is not in the right universe.

[Christian Merten]

(Sidenote: this times out at isDefEq if the explicit universe annotation is dropped)

[Adam Topaz]

I assume you need to use the sheaf condition for the structure sheaf

[Adam Topaz]

It should be fairly direct

[Adam Topaz]

You may need to restrict the universe of J as it appears in the Zariski topology

[Adam Topaz]

Namely X.OpenCover.{u}

[Adam Topaz]

We could also develop some api to convert an open cover with arbitrary universes to one with the same universes as X.

[Adam Topaz]

Alternatively you could view f and g as morphisms to A1 (do we have a way to do this yet?) and use the gluing API

[Andrew Yang]

import Mathlib

open AlgebraicGeometry Opposite CategoryTheory

universe u

noncomputable
def IsOpenImmersion.ΓIso {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] :
    Scheme.Γ.obj (op X) ≅ Y.presheaf.obj (op (Scheme.Hom.opensRange f)) :=
  Scheme.Γ.mapIso (IsOpenImmersion.isoOfRangeEq
      (Scheme.ιOpens (Scheme.Hom.opensRange f)) _ Subtype.range_val).op ≪≫
    Y.presheaf.mapIso (eqToIso (TopologicalSpace.Opens.openEmbedding_obj_top _).symm).op

lemma IsOpenImmersion.map_ΓIso_inv
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] :
  Y.presheaf.map (homOfLE le_top).op ≫ (IsOpenImmersion.ΓIso f).inv = Scheme.Γ.map f.op := by
  conv_rhs => rw [← IsOpenImmersion.isoOfRangeEq_inv_fac
      (Scheme.ιOpens (Scheme.Hom.opensRange f)) _ Subtype.range_val]
  rw [IsOpenImmersion.ΓIso]
  dsimp
  rw [← Functor.map_comp_assoc]
  rfl

lemma eq_of_eq_cover {X : Scheme.{u}} (f g : Scheme.Γ.obj (op X)) (𝒰 : X.OpenCover)
    (h : ∀ i : 𝒰.J, Scheme.Γ.map (𝒰.map i).op f = Scheme.Γ.map (𝒰.map i).op g) : f = g := by
  fapply TopCat.Sheaf.eq_of_locally_eq' X.sheaf
    (fun i ↦ Scheme.Hom.opensRange (𝒰.map (𝒰.f i))) _ (fun _ ↦ homOfLE le_top)
  · rintro x -; simpa using ⟨_, 𝒰.Covers x⟩
  · intro x;
    replace h := h (𝒰.f x)
    rw [← IsOpenImmersion.map_ΓIso_inv] at h
    exact (IsOpenImmersion.ΓIso (𝒰.map (𝒰.f x))).commRingCatIsoToRingEquiv.symm.injective h

[Christian Merten]

Andrew Yang said:

import Mathlib

open AlgebraicGeometry Opposite CategoryTheory

universe u

noncomputable
def IsOpenImmersion.ΓIso {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] :
    Scheme.Γ.obj (op X) ≅ Y.presheaf.obj (op (Scheme.Hom.opensRange f)) :=
  Scheme.Γ.mapIso (IsOpenImmersion.isoOfRangeEq
      (Scheme.ιOpens (Scheme.Hom.opensRange f)) _ Subtype.range_val).op ≪≫
    Y.presheaf.mapIso (eqToIso (TopologicalSpace.Opens.openEmbedding_obj_top _).symm).op

lemma IsOpenImmersion.map_ΓIso_inv
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] :
  Y.presheaf.map (homOfLE le_top).op ≫ (IsOpenImmersion.ΓIso f).inv = Scheme.Γ.map f.op := by
  conv_rhs => rw [← IsOpenImmersion.isoOfRangeEq_inv_fac
      (Scheme.ιOpens (Scheme.Hom.opensRange f)) _ Subtype.range_val]
  rw [IsOpenImmersion.ΓIso]
  dsimp
  rw [← Functor.map_comp_assoc]
  rfl

lemma eq_of_eq_cover {X : Scheme.{u}} (f g : Scheme.Γ.obj (op X)) (𝒰 : X.OpenCover)
    (h : ∀ i : 𝒰.J, Scheme.Γ.map (𝒰.map i).op f = Scheme.Γ.map (𝒰.map i).op g) : f = g := by
  fapply TopCat.Sheaf.eq_of_locally_eq' X.sheaf
    (fun i ↦ Scheme.Hom.opensRange (𝒰.map (𝒰.f i))) _ (fun _ ↦ homOfLE le_top)
  · rintro x -; simpa using ⟨_, 𝒰.Covers x⟩
  · intro x;
    replace h := h (𝒰.f x)
    rw [← IsOpenImmersion.map_ΓIso_inv] at h
    exact (IsOpenImmersion.ΓIso (𝒰.map (𝒰.f x))).commRingCatIsoToRingEquiv.symm.injective h

Thanks a lot!

[Christian Merten]

Ah, so the trick is to use X.carrier as the indexing type and then use 𝒰.f :light_bulb: