NYLL
Module

Scheme_IdealSheafData_exists_comap_eq_of_openCover.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_exists_comap_eq_of_openCover
27 declarations indexed from sourceView source ↗

Module documentation

Gluing compatible ideal sheaves on an open cover

Ideal sheaves on the members of an open cover glue when their inverse images agree on common refinements. The ideal on each affine open is determined by its restrictions to transported affine opens in the cover.

Imports3
  • Mathlib.Algebra.Category.Ring.Basic
  • Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  • Mathlib.AlgebraicGeometry.Cover.Open
Imported by4

Declarations

lemma

appIso_of_comp_eq

L47 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover.AlgebraicGeometry.Scheme.IdealSheafData.Glue.appIso_of_comp_eq
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace Glue
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
lemma appIso_of_comp_eq {V U X : Scheme.{u}} (a : V ⟶ U) (f : U ⟶ X) (c : V ⟶ X)
    [IsOpenImmersion a] [IsOpenImmersion f] [IsOpenImmersion c] (hc : c = a ≫ f) (W : V.Opens)
    (e : f ''ᵁ a ''ᵁ W = c ''ᵁ W) :
    c.appIso W = X.presheaf.mapIso (eqToIso e).op ≪≫ f.appIso (a ''ᵁ W) ≪≫ a.appIso W
lemma

image_eq_of_comp_eq

L54 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover.AlgebraicGeometry.Scheme.IdealSheafData.Glue.image_eq_of_comp_eq
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace Glue
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
lemma image_eq_of_comp_eq {V U X : Scheme.{u}} (a : V ⟶ U) (f : U ⟶ X) (c : V ⟶ X)
    [IsOpenImmersion a] [IsOpenImmersion f] [IsOpenImmersion c] (hc : c = a ≫ f) (W : V.Opens) :
    f ''ᵁ a ''ᵁ W = c ''ᵁ W
lemma

mem_map_iff_of_bijective

L60 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover.AlgebraicGeometry.Scheme.IdealSheafData.Glue.mem_map_iff_of_bijective
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace Glue
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
lemma mem_map_iff_of_bijective {R S : Type*} [CommRing R] [CommRing S] (φ : R →+* S)
    (hφ : Function.Bijective φ) (K : Ideal R) (x : R) : φ x ∈ K.map φ ↔ x ∈ K
lemma

appIso_hom_naturality_apply

L65 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover.AlgebraicGeometry.Scheme.IdealSheafData.Glue.appIso_hom_naturality_apply
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace Glue
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
lemma appIso_hom_naturality_apply {Y' X' : Scheme.{u}} (g : Y' ⟶ X') [IsOpenImmersion g]
    {U V : Y'.Opens} (i : Opposite.op U ⟶ Opposite.op V) (y : Γ(X', g ''ᵁ U)) :
    (g.appIso V).hom (X'.presheaf.map (g.opensFunctor.op.map i) y) =
      Y'.presheaf.map i ((g.appIso U).hom y)
def

imA

L79 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover.AlgebraicGeometry.Scheme.IdealSheafData.Glue.imA
Documentation

The affine open obtained by mapping an affine open of a cover member into the scheme.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace Glue
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (𝒰 : X.OpenCover) (I : ∀ i, (𝒰.X i).IdealSheafData)
Lean source · statement
def imA (i : 𝒰.I₀) (W : (𝒰.X i).affineOpens) : X.affineOpens
lemma

coe_imA

L82 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover.AlgebraicGeometry.Scheme.IdealSheafData.Glue.coe_imA
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace Glue
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (𝒰 : X.OpenCover) (I : ∀ i, (𝒰.X i).IdealSheafData)
Lean source · statement
lemma coe_imA (i : 𝒰.I₀) (W : (𝒰.X i).affineOpens) :
    (imA 𝒰 i W : X.Opens) = 𝒰.f i ''ᵁ (W : (𝒰.X i).Opens)
def

T

L87 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover.AlgebraicGeometry.Scheme.IdealSheafData.Glue.T
Documentation

The ideal on a cover-image affine open transported by the inverse structure-sheaf isomorphism.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace Glue
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (𝒰 : X.OpenCover) (I : ∀ i, (𝒰.X i).IdealSheafData)
Lean source · statement
def T (i : 𝒰.I₀) (W : (𝒰.X i).affineOpens) : Ideal Γ(X, 𝒰.f i ''ᵁ (W : (𝒰.X i).Opens))
lemma

T_eq_comap

L91 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover.AlgebraicGeometry.Scheme.IdealSheafData.Glue.T_eq_comap
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace Glue
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (𝒰 : X.OpenCover) (I : ∀ i, (𝒰.X i).IdealSheafData)
Lean source · statement
lemma T_eq_comap (i : 𝒰.I₀) (W : (𝒰.X i).affineOpens) :
    T 𝒰 I i W = ((I i).ideal W).comap ((𝒰.f i).appIso W).hom.hom
lemma

T_map_of_le

L103 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover.AlgebraicGeometry.Scheme.IdealSheafData.Glue.T_map_of_le
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace Glue
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (𝒰 : X.OpenCover) (I : ∀ i, (𝒰.X i).IdealSheafData)
Lean source · statement
lemma T_map_of_le (i : 𝒰.I₀) {W W' : (𝒰.X i).affineOpens} (h : W' ≤ W) :
    (T 𝒰 I i W).map (X.presheaf.map (homOfLE ((𝒰.f i).image_mono h)).op).hom = T 𝒰 I i W'
def

J

L114 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover.AlgebraicGeometry.Scheme.IdealSheafData.Glue.J
Documentation

The ideal of sections whose restrictions lie in all transported cover-member ideals.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace Glue
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (𝒰 : X.OpenCover) (I : ∀ i, (𝒰.X i).IdealSheafData)
Lean source · statement
def J (V : X.affineOpens) : Ideal Γ(X, V)
lemma

mem_J_iff

L118 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover.AlgebraicGeometry.Scheme.IdealSheafData.Glue.mem_J_iff
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace Glue
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (𝒰 : X.OpenCover) (I : ∀ i, (𝒰.X i).IdealSheafData)
Lean source · statement
lemma mem_J_iff {V : X.affineOpens} (s : Γ(X, V)) :
    s ∈ J 𝒰 I V ↔ ∀ (i : 𝒰.I₀) (W : (𝒰.X i).affineOpens)
      (h : 𝒰.f i ''ᵁ (W : (𝒰.X i).Opens) ≤ (V : X.Opens)),
      X.presheaf.map (homOfLE h).op s ∈ T 𝒰 I i W
lemma

J_map_le

L124 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover.AlgebraicGeometry.Scheme.IdealSheafData.Glue.J_map_le
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace Glue
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (𝒰 : X.OpenCover) (I : ∀ i, (𝒰.X i).IdealSheafData)
Lean source · statement
lemma J_map_le {V V' : X.affineOpens} (h : V' ≤ V) :
    (J 𝒰 I V).map (X.presheaf.map (homOfLE h).op).hom ≤ J 𝒰 I V'
lemma

T_eq_of_image_eq

L136 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover.AlgebraicGeometry.Scheme.IdealSheafData.Glue.T_eq_of_image_eq
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace Glue
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (𝒰 : X.OpenCover) (I : ∀ i, (𝒰.X i).IdealSheafData)
Lean source · statement
lemma T_eq_of_image_eq
    (hI : ∀ ⦃i j : 𝒰.I₀⦄ ⦃V : Scheme.{u}⦄ (a : V ⟶ 𝒰.X i) (b : V ⟶ 𝒰.X j),
      a ≫ 𝒰.f i = b ≫ 𝒰.f j → (I i).comap a = (I j).comap b)
    {i j : 𝒰.I₀} (W₁ : (𝒰.X i).affineOpens) (W : (𝒰.X j).affineOpens)
    (e : 𝒰.f i ''ᵁ (W₁ : (𝒰.X i).Opens) = 𝒰.f j ''ᵁ (W : (𝒰.X j).Opens)) :
    T 𝒰 I i W₁ = (T 𝒰 I j W).map (X.presheaf.map (eqToHom e).op).hom
lemma

J_imA

L232 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover.AlgebraicGeometry.Scheme.IdealSheafData.Glue.J_imA
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace Glue
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (𝒰 : X.OpenCover) (I : ∀ i, (𝒰.X i).IdealSheafData)
Lean source · statement
lemma J_imA (i : 𝒰.I₀) (W : (𝒰.X i).affineOpens)
    (hI : ∀ ⦃i j : 𝒰.I₀⦄ ⦃V : Scheme.{u}⦄ (a : V ⟶ 𝒰.X i) (b : V ⟶ 𝒰.X j),
      a ≫ 𝒰.f i = b ≫ 𝒰.f j → (I i).comap a = (I j).comap b) :
    J 𝒰 I (imA 𝒰 i W) = T 𝒰 I i W
lemma

presheaf_map_eq

L275 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover.AlgebraicGeometry.Scheme.IdealSheafData.Glue.presheaf_map_eq
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace Glue
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (𝒰 : X.OpenCover) (I : ∀ i, (𝒰.X i).IdealSheafData)
section L3
omit 𝒰 in
Lean source · statement
lemma presheaf_map_eq {U V : X.Opens} (i j : Opposite.op U ⟶ Opposite.op V) :
    X.presheaf.map i = X.presheaf.map j
lemma

presheaf_map_map_apply

L280 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover.AlgebraicGeometry.Scheme.IdealSheafData.Glue.presheaf_map_map_apply
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace Glue
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (𝒰 : X.OpenCover) (I : ∀ i, (𝒰.X i).IdealSheafData)
section L3
omit 𝒰 in
Lean source · statement
lemma presheaf_map_map_apply {A B C : (X.Opens)ᵒᵖ} (i : A ⟶ B) (j : B ⟶ C) (k : A ⟶ C)
    (x : X.presheaf.obj A) :
    X.presheaf.map j (X.presheaf.map i x) = X.presheaf.map k x
lemma

mem_ideal_of_forall_basicOpen

L285 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover.AlgebraicGeometry.Scheme.IdealSheafData.Glue.mem_ideal_of_forall_basicOpen
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace Glue
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (𝒰 : X.OpenCover) (I : ∀ i, (𝒰.X i).IdealSheafData)
section L3
Lean source · statement
lemma mem_ideal_of_forall_basicOpen {Y : Scheme.{u}} (K : Y.IdealSheafData) (W : Y.affineOpens)
    (s : Set Γ(Y, W)) (hs : Ideal.span s = ⊤) (y : Γ(Y, W))
    (h : ∀ g ∈ s, Y.presheaf.map (homOfLE (Y.basicOpen_le g)).op y ∈ K.ideal (Y.affineBasicOpen g))
        :
    y ∈ K.ideal W
lemma

algebraMap_basicOpen_apply

L302 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover.AlgebraicGeometry.Scheme.IdealSheafData.Glue.algebraMap_basicOpen_apply
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace Glue
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (𝒰 : X.OpenCover) (I : ∀ i, (𝒰.X i).IdealSheafData)
section L3
omit I in
Lean source · statement
lemma algebraMap_basicOpen_apply {U : X.Opens} (f : Γ(X, U)) (x : Γ(X, U)) :
    algebraMap Γ(X, U) Γ(X, X.basicOpen f) x = X.presheaf.map (homOfLE (X.basicOpen_le f)).op x
lemma

J_map_congr

L306 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover.AlgebraicGeometry.Scheme.IdealSheafData.Glue.J_map_congr
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace Glue
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (𝒰 : X.OpenCover) (I : ∀ i, (𝒰.X i).IdealSheafData)
section L3
Lean source · statement
lemma J_map_congr {U₁ U₂ U₁' U₂' : X.affineOpens} (e : U₁ = U₂) (e' : U₁' = U₂')
    (h₁ : U₁' ≤ U₁) (h₂ : U₂' ≤ U₂)
    (H : J 𝒰 I U₁' = (J 𝒰 I U₁).map (X.presheaf.map (homOfLE h₁).op).hom) :
    J 𝒰 I U₂' = (J 𝒰 I U₂).map (X.presheaf.map (homOfLE h₂).op).hom
lemma

J_basicOpen_basicOpen

L313 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover.AlgebraicGeometry.Scheme.IdealSheafData.Glue.J_basicOpen_basicOpen
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace Glue
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (𝒰 : X.OpenCover) (I : ∀ i, (𝒰.X i).IdealSheafData)
section L3
Lean source · statement
lemma J_basicOpen_basicOpen
    (hJ : ∀ (i : 𝒰.I₀) (W : (𝒰.X i).affineOpens), J 𝒰 I (imA 𝒰 i W) = T 𝒰 I i W)
    {V : X.affineOpens} {g : Γ(X, V)} {i : 𝒰.I₀} {W : (𝒰.X i).affineOpens}
    (e : 𝒰.f i ''ᵁ (W : (𝒰.X i).Opens) = X.basicOpen g) (h' : Γ(X, X.basicOpen g)) :
    J 𝒰 I (X.affineBasicOpen (U := X.affineBasicOpen g) h') =
      (J 𝒰 I (X.affineBasicOpen g)).map (X.presheaf.map (homOfLE (X.basicOpen_le h')).op).hom
lemma

mem_J_of_forall_basicOpen

L340 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover.AlgebraicGeometry.Scheme.IdealSheafData.Glue.mem_J_of_forall_basicOpen
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace Glue
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (𝒰 : X.OpenCover) (I : ∀ i, (𝒰.X i).IdealSheafData)
section L3
Lean source · statement
lemma mem_J_of_forall_basicOpen {V : X.affineOpens} (x : Γ(X, V)) (s : Set Γ(X, V))
    (hs : Ideal.span s = ⊤)
    (hx : ∀ g ∈ s, X.presheaf.map (homOfLE (X.basicOpen_le g)).op x ∈ J 𝒰 I (X.affineBasicOpen g)) :
    x ∈ J 𝒰 I V
lemma

exists_good_cover

L378 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover.AlgebraicGeometry.Scheme.IdealSheafData.Glue.exists_good_cover
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace Glue
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (𝒰 : X.OpenCover) (I : ∀ i, (𝒰.X i).IdealSheafData)
section L3
omit I in
Lean source · statement
lemma exists_good_cover (V : X.affineOpens) :
    ∃ s : Finset Γ(X, V), Ideal.span (s : Set Γ(X, V)) = ⊤ ∧
      ∀ g ∈ s, ∃ (i : 𝒰.I₀) (W : (𝒰.X i).affineOpens),
        𝒰.f i ''ᵁ (W : (𝒰.X i).Opens) = X.basicOpen g
lemma

J_basicOpen_le'

L407 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover.AlgebraicGeometry.Scheme.IdealSheafData.Glue.J_basicOpen_le'
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace Glue
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (𝒰 : X.OpenCover) (I : ∀ i, (𝒰.X i).IdealSheafData)
section L3
Lean source · statement
lemma J_basicOpen_le'
    (hJ : ∀ (i : 𝒰.I₀) (W : (𝒰.X i).affineOpens), J 𝒰 I (imA 𝒰 i W) = T 𝒰 I i W)
    (V : X.affineOpens) (h : Γ(X, V)) :
    J 𝒰 I (X.affineBasicOpen h) ≤
      (J 𝒰 I V).map (X.presheaf.map (homOfLE (X.basicOpen_le h)).op).hom
lemma

J_basicOpen_le

L489 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover.AlgebraicGeometry.Scheme.IdealSheafData.Glue.J_basicOpen_le
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace Glue
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (𝒰 : X.OpenCover) (I : ∀ i, (𝒰.X i).IdealSheafData)
Lean source · statement
lemma J_basicOpen_le (V : X.affineOpens) (h : Γ(X, V))
    (hI : ∀ ⦃i j : 𝒰.I₀⦄ ⦃V : Scheme.{u}⦄ (a : V ⟶ 𝒰.X i) (b : V ⟶ 𝒰.X j),
      a ≫ 𝒰.f i = b ≫ 𝒰.f j → (I i).comap a = (I j).comap b) :
    J 𝒰 I (X.affineBasicOpen h) ≤
      (J 𝒰 I V).map (X.presheaf.map (homOfLE (X.basicOpen_le h)).op).hom
def

glued

L497 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover.AlgebraicGeometry.Scheme.IdealSheafData.Glue.glued
Documentation

The ideal sheaf glued from compatible ideal sheaves on the open cover.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace Glue
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (𝒰 : X.OpenCover) (I : ∀ i, (𝒰.X i).IdealSheafData)
Lean source · full declaration
def glued
    (hI : ∀ ⦃i j : 𝒰.I₀⦄ ⦃V : Scheme.{u}⦄ (a : V ⟶ 𝒰.X i) (b : V ⟶ 𝒰.X j),
      a ≫ 𝒰.f i = b ≫ 𝒰.f j → (I i).comap a = (I j).comap b) : X.IdealSheafData where
  ideal := J 𝒰 I
  map_ideal_basicOpen V h :=
    le_antisymm (J_map_le 𝒰 I (V := V) (V' := X.affineBasicOpen h) (X.basicOpen_le h))
      (J_basicOpen_le 𝒰 I V h hI)
theorem

comap_glued

L505 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover.AlgebraicGeometry.Scheme.IdealSheafData.Glue.comap_glued
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace Glue
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (𝒰 : X.OpenCover) (I : ∀ i, (𝒰.X i).IdealSheafData)
Lean source · statement
theorem comap_glued
    (hI : ∀ ⦃i j : 𝒰.I₀⦄ ⦃V : Scheme.{u}⦄ (a : V ⟶ 𝒰.X i) (b : V ⟶ 𝒰.X j),
      a ≫ 𝒰.f i = b ≫ 𝒰.f j → (I i).comap a = (I j).comap b) (i : 𝒰.I₀) :
    (glued 𝒰 I hI).comap (𝒰.f i) = I i
theorem

exists_comap_eq_of_openCover

L521 ↗
AlgebraicGeometry.Scheme.IdealSheafData.exists_comap_eq_of_openCover
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_exists_comap_eq_of_openCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.IdealSheafData.exists_comap_eq_of_openCover
    {X : Scheme.{u}} (𝒰 : X.OpenCover) (I : ∀ i, (𝒰.X i).IdealSheafData)
    (hI : ∀ ⦃i j : 𝒰.I₀⦄ ⦃V : Scheme.{u}⦄ (a : V ⟶ 𝒰.X i) (b : V ⟶ 𝒰.X j),
      a ≫ 𝒰.f i = b ≫ 𝒰.f j → (I i).comap a = (I j).comap b) :
    ∃ I₀ : X.IdealSheafData, ∀ i, I₀.comap (𝒰.f i) = I i

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