NYLL
Module

Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover
36 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules exists unique section of pullback Section closed Cover

Imports10
Imported by4

Declarations

lemma

map_app

L84 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.map_app
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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section General
variable {X Y : Scheme.{u}}
Lean source · statement
lemma map_app {M N : X.Modules} (φ : M ⟶ N) {U V : X.Opens} (i : V ⟶ U) (s : Γ(M, U)) :
    N.presheaf.map i.op (φ.app U s) = φ.app V (M.presheaf.map i.op s)
lemma

map_homOfLE_rfl

L89 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.map_homOfLE_rfl
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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section General
variable {X Y : Scheme.{u}}
Lean source · statement
lemma map_homOfLE_rfl {M : X.Modules} {U : X.Opens} (h : U ≤ U) (s : Γ(M, U)) :
    M.presheaf.map (homOfLE h).op s = s
lemma

map_map

L95 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.map_map
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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section General
variable {X Y : Scheme.{u}}
Lean source · statement
lemma map_map {M : X.Modules} {U V W : X.Opens} (i : V ⟶ U) (j : W ⟶ V) (s : Γ(M, U)) :
    M.presheaf.map j.op (M.presheaf.map i.op s) = M.presheaf.map (j ≫ i).op s
lemma

map_congr

L100 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.map_congr
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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section General
variable {X Y : Scheme.{u}}
Lean source · statement
lemma map_congr {M : X.Modules} {U V : X.Opens} (i j : V ⟶ U) (s : Γ(M, U)) :
    M.presheaf.map i.op s = M.presheaf.map j.op s
lemma

map_toUnitSection_one

L104 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.map_toUnitSection_one
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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section General
variable {X Y : Scheme.{u}}
Lean source · statement
lemma map_toUnitSection_one {U V : X.Opens} (i : V ⟶ U) :
    (𝟙_ X.Modules).presheaf.map i.op (toUnitSection U (1 : Γ(X, U))) = toUnitSection V 1
lemma

iso_inv_hom_app_apply

L109 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.iso_inv_hom_app_apply
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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section General
variable {X Y : Scheme.{u}}
Lean source · statement
lemma iso_inv_hom_app_apply {M N : X.Modules} (e : M ≅ N) (U : X.Opens) (x : Γ(N, U)) :
    e.hom.app U (e.inv.app U x) = x
lemma

iso_hom_inv_app_apply

L115 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.iso_hom_inv_app_apply
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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section General
variable {X Y : Scheme.{u}}
Lean source · statement
lemma iso_hom_inv_app_apply {M N : X.Modules} (e : M ≅ N) (U : X.Opens) (x : Γ(M, U)) :
    e.inv.app U (e.hom.app U x) = x
def

gsec

L122 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.gsec
Documentation

The global section obtained by evaluating a morphism from the unit module at one.

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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section General
variable {X Y : Scheme.{u}}
Lean source · statement
def gsec {M : X.Modules} (σ : 𝟙_ X.Modules ⟶ M) : Γ(M, ⊤)
lemma

gsec_def

L124 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.gsec_def
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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section General
variable {X Y : Scheme.{u}}
Lean source · statement
lemma gsec_def {M : X.Modules} (σ : 𝟙_ X.Modules ⟶ M) : gsec σ = σ.app ⊤ (toUnitSection ⊤ 1)
lemma

app_toUnitSection_one

L126 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.app_toUnitSection_one
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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section General
variable {X Y : Scheme.{u}}
Lean source · statement
lemma app_toUnitSection_one {M : X.Modules} (σ : 𝟙_ X.Modules ⟶ M) (U : X.Opens) :
    σ.app U (toUnitSection U 1) = M.presheaf.map (homOfLE (le_top : U ≤ ⊤)).op (gsec σ)
lemma

hom_ext_of_gsec_eq

L130 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.hom_ext_of_gsec_eq
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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section General
variable {X Y : Scheme.{u}}
Lean source · statement
lemma hom_ext_of_gsec_eq {M : X.Modules} {σ σ' : 𝟙_ X.Modules ⟶ M} (h : gsec σ = gsec σ') : σ = σ'
def

sectionsOfGsec

L139 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.sectionsOfGsec
Documentation

The compatible family of restrictions of a global section.

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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section General
variable {X Y : Scheme.{u}}
Lean source · full declaration
def sectionsOfGsec {M : X.Modules} (s : Γ(M, ⊤)) : (show SheafOfModules X.ringCatSheaf from
  M).sections :=
  PresheafOfModules.sectionsMk (M := M.val) (fun U => (M.presheaf.map (homOfLE (le_top : U.unop ≤
    ⊤)).op s :))
    (by
      intro U V f
      change M.presheaf.map f (M.presheaf.map (homOfLE (le_top : U.unop ≤ ⊤)).op s) =
        M.presheaf.map (homOfLE (le_top : V.unop ≤ ⊤)).op s
      rw [← CategoryTheory.comp_apply, ← M.presheaf.map_comp]
      rfl)
def

homOfGsec

L151 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.homOfGsec
Documentation

The morphism from the unit module corresponding to a global section.

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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section General
variable {X Y : Scheme.{u}}
Lean source · statement
def homOfGsec {M : X.Modules} (s : Γ(M, ⊤)) : 𝟙_ X.Modules ⟶ M
lemma

gsec_homOfGsec

L154 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.gsec_homOfGsec
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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section General
variable {X Y : Scheme.{u}}
Lean source · statement
lemma gsec_homOfGsec {M : X.Modules} (s : Γ(M, ⊤)) : gsec (homOfGsec s) = s
lemma

app_pullbackSection_toUnitSection_one

L160 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.app_pullbackSection_toUnitSection_one
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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section General
variable {X Y : Scheme.{u}}
Lean source · statement
lemma app_pullbackSection_toUnitSection_one (φ : X ⟶ Y) {L : Y.Modules} (σ : 𝟙_ Y.Modules ⟶ L)
    (U : Y.Opens) :
    (pullbackSection φ σ).app (φ ⁻¹ᵁ U) (toUnitSection (φ ⁻¹ᵁ U) 1) =
      pullbackLocalSection φ (σ.app U (toUnitSection U 1))
lemma

gsec_pullbackSection

L175 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.gsec_pullbackSection
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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section General
variable {X Y : Scheme.{u}}
Lean source · statement
lemma gsec_pullbackSection (φ : X ⟶ Y) {L : Y.Modules} (σ : 𝟙_ Y.Modules ⟶ L) :
    gsec (pullbackSection φ σ) = pullbackLocalSection φ (gsec σ)
lemma

pullbackComp_hom_app_app_pullbackLocalSection

L179 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.pullbackComp_hom_app_app_pullbackLocalSection
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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section General
variable {X Y : Scheme.{u}}
Lean source · statement
lemma pullbackComp_hom_app_app_pullbackLocalSection {Z : Scheme.{u}} (g : Z ⟶ Y) (f : Y ⟶ X) (M :
  X.Modules)
    (U : X.Opens) (s : Γ(M, U)) :
    ((pullbackComp g f).hom.app M).app (g ⁻¹ᵁ (f ⁻¹ᵁ U))
        (pullbackLocalSection g (pullbackLocalSection f s)) =
      pullbackLocalSection (g ≫ f) s
lemma

pullbackCongr_hom_app_app_pullbackLocalSection

L191 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.pullbackCongr_hom_app_app_pullbackLocalSection
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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section General
variable {X Y : Scheme.{u}}
Lean source · full declaration
lemma pullbackCongr_hom_app_app_pullbackLocalSection {f g : X ⟶ Y} (h : f = g) (M : Y.Modules)
    (U : Y.Opens) (s : Γ(M, U)) :
    ((pullbackCongr h).hom.app M).app (f ⁻¹ᵁ U) (pullbackLocalSection f s) =
      ((Modules.pullback g).obj M).presheaf.map
        (eqToHom (show f ⁻¹ᵁ U = g ⁻¹ᵁ U by rw [h])).op (pullbackLocalSection g s) := by
  subst h
  simp [pullbackCongr]
lemma

exists_isFrameOn

L199 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.exists_isFrameOn
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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section General
variable {X Y : Scheme.{u}}
Lean source · statement
lemma exists_isFrameOn {L : X.Modules} (hL : IsInvertible L) (x : X) :
    ∃ (U : X.Opens) (e : Γ(L, U)), x ∈ U ∧ IsFrameOn e U
lemma

map_id_apply

L205 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.map_id_apply
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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section General
variable {X Y : Scheme.{u}}
Lean source · statement
lemma map_id_apply {M : X.Modules} {U : X.Opens} (s : Γ(M, U)) : M.presheaf.map (𝟙 (op U)) s = s
def

res

L217 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.res
Documentation

Restriction of a global section of the pulled-back module to the preimage of an open.

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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section Side
variable {P Z X : Scheme.{u}} (φ : P ⟶ Z) (i : Z ⟶ X) {L : X.Modules}
Lean source · statement
def res (t : Γ((Modules.pullback i).obj L, ⊤)) (U : X.Opens) : Γ((Modules.pullback i).obj L, i ⁻¹ᵁ
  U)
lemma

res_top

L221 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.res_top
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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section Side
variable {P Z X : Scheme.{u}} (φ : P ⟶ Z) (i : Z ⟶ X) {L : X.Modules}
Lean source · statement
lemma res_top (t : Γ((Modules.pullback i).obj L, ⊤)) : res i t ⊤ = t
lemma

map_res

L224 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.map_res
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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section Side
variable {P Z X : Scheme.{u}} (φ : P ⟶ Z) (i : Z ⟶ X) {L : X.Modules}
Lean source · full declaration
lemma map_res (t : Γ((Modules.pullback i).obj L, ⊤)) {U V : X.Opens} (hVU : V ≤ U) :
    ((Modules.pullback i).obj L).presheaf.map
        (homOfLE (show i ⁻¹ᵁ V ≤ i ⁻¹ᵁ U from fun _ hx => hVU hx)).op (res i t U) = res i t V := by
  rw [res, map_map]
  rfl
abbrev

pbComp

L231 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.pbComp
Documentation

The local section pulled back along a composite morphism.

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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section Side
variable {P Z X : Scheme.{u}} (φ : P ⟶ Z) (i : Z ⟶ X) {L : X.Modules}
Lean source · statement
abbrev pbComp {U : X.Opens} (e : Γ(L, U)) : Γ((Modules.pullback (φ ≫ i)).obj L, φ ⁻¹ᵁ (i ⁻¹ᵁ U))
lemma

map_pullbackComp_app_pullbackLocalSection

L234 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.map_pullbackComp_app_pullbackLocalSection
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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section Side
variable {P Z X : Scheme.{u}} (φ : P ⟶ Z) (i : Z ⟶ X) {L : X.Modules}
Lean source · statement
lemma map_pullbackComp_app_pullbackLocalSection (t : Γ((Modules.pullback i).obj L, ⊤)) {U : X.Opens}
    (e : Γ(L, U)) (g : Γ(Z, i ⁻¹ᵁ U)) (hg : res i t U = g • pullbackLocalSection i e) :
    ((Modules.pullback (φ ≫ i)).obj L).presheaf.map (homOfLE (le_top : φ ⁻¹ᵁ (i ⁻¹ᵁ U) ≤ ⊤)).op
        (((pullbackComp φ i).hom.app L).app ⊤ (pullbackLocalSection φ t)) =
      φ.app (i ⁻¹ᵁ U) g • pbComp φ i e
lemma

pullbackCongr_hom_app_app_map_pullbackLocalSection

L258 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.pullbackCongr_hom_app_app_map_pullbackLocalSection
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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
Lean source · full declaration
lemma pullbackCongr_hom_app_app_map_pullbackLocalSection {P X : Scheme.{u}} {f g : P ⟶ X} (h : f =
  g)
    (M : X.Modules) (U : X.Opens) (s : Γ(M, U)) :
    ((pullbackCongr h).hom.app M).app (g ⁻¹ᵁ U)
        (((Modules.pullback f).obj M).presheaf.map (eqToHom (show g ⁻¹ᵁ U = f ⁻¹ᵁ U by rw [h])).op
          (pullbackLocalSection f s)) =
      pullbackLocalSection g s := by
  subst h
  simp only [pullbackCongr, eqToIso_refl, Iso.refl_hom, NatTrans.id_app, Scheme.Modules.Hom.id_app,
    eqToHom_refl, op_id, map_id_apply]
  rfl
lemma

map_app_eq_app_of_agree

L275 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.map_app_eq_app_of_agree
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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section Core
variable {X Z₁ Z₂ : Scheme.{u}} (i₁ : Z₁ ⟶ X) (i₂ : Z₂ ⟶ X)
  {L : X.Modules} (t₁ : Γ((Modules.pullback i₁).obj L, ⊤)) (t₂ : Γ((Modules.pullback i₂).obj L, ⊤))
Lean source · full declaration
lemma map_app_eq_app_of_agree {P : Scheme.{u}} (p₁ : P ⟶ Z₁) (p₂ : P ⟶ Z₂) (hc : p₁ ≫ i₁ = p₂ ≫ i₂)
    (hA : ((pullbackCongr hc).hom.app L).app ⊤
        (((pullbackComp p₁ i₁).hom.app L).app ⊤ (pullbackLocalSection p₁ t₁)) =
      ((pullbackComp p₂ i₂).hom.app L).app ⊤ (pullbackLocalSection p₂ t₂))
    {U : X.Opens} {e : Γ(L, U)} (he : IsFrameOn e U)
    (g₁ : Γ(Z₁, i₁ ⁻¹ᵁ U)) (g₂ : Γ(Z₂, i₂ ⁻¹ᵁ U))
    (hg₁ : res i₁ t₁ U = g₁ • pullbackLocalSection i₁ e) (hg₂ : res i₂ t₂ U = g₂ •
      pullbackLocalSection i₂ e) :
    P.presheaf.map (eqToHom (show p₂ ⁻¹ᵁ (i₂ ⁻¹ᵁ U) = p₁ ⁻¹ᵁ (i₁ ⁻¹ᵁ U) by
        rw [← Scheme.Hom.comp_preimage, ← Scheme.Hom.comp_preimage, hc])).op (p₁.app (i₁ ⁻¹ᵁ U) g₁)
          =
      p₂.app (i₂ ⁻¹ᵁ U) g₂ := by
  have hW : p₂ ⁻¹ᵁ (i₂ ⁻¹ᵁ U) = p₁ ⁻¹ᵁ (i₁ ⁻¹ᵁ U) := by
    rw [← Scheme.Hom.comp_preimage, ← Scheme.Hom.comp_preimage, hc]
  have hA' := congrArg (((Modules.pullback (p₂ ≫ i₂)).obj L).presheaf.map
    (homOfLE (le_top : p₂ ⁻¹ᵁ (i₂ ⁻¹ᵁ U) ≤ ⊤)).op) hA
  rw [map_pullbackComp_app_pullbackLocalSection p₂ i₂ t₂ e g₂ hg₂] at hA'
  have hfac : ((Modules.pullback (p₂ ≫ i₂)).obj L).presheaf.map
        (homOfLE (le_top : p₂ ⁻¹ᵁ (i₂ ⁻¹ᵁ U) ≤ ⊤)).op
        (((pullbackCongr hc).hom.app L).app ⊤
          (((pullbackComp p₁ i₁).hom.app L).app ⊤ (pullbackLocalSection p₁ t₁))) =
      ((pullbackCongr hc).hom.app L).app (p₂ ⁻¹ᵁ (i₂ ⁻¹ᵁ U))
        (((Modules.pullback (p₁ ≫ i₁)).obj L).presheaf.map (eqToHom hW).op
          (((Modules.pullback (p₁ ≫ i₁)).obj L).presheaf.map
            (homOfLE (le_top : p₁ ⁻¹ᵁ (i₁ ⁻¹ᵁ U) ≤ ⊤)).op
            (((pullbackComp p₁ i₁).hom.app L).app ⊤ (pullbackLocalSection p₁ t₁)))) := by
    rw [map_app, map_map]
    rfl
  rw [hfac, map_pullbackComp_app_pullbackLocalSection p₁ i₁ t₁ e g₁ hg₁, Scheme.Modules.map_smul,
    Scheme.Modules.Hom.app_smul] at hA'
  have hE : ((pullbackCongr hc).hom.app L).app (p₂ ⁻¹ᵁ (i₂ ⁻¹ᵁ U))
      (((Modules.pullback (p₁ ≫ i₁)).obj L).presheaf.map (eqToHom hW).op (pbComp p₁ i₁ e)) =
        pbComp p₂ i₂ e :=
    pullbackCongr_hom_app_app_map_pullbackLocalSection hc L U e
  rw [hE] at hA'
  have hfr := (he.pullbackLocalSection (p₂ ≫ i₂)).bijective le_rfl le_rfl
  simp only [map_homOfLE_rfl] at hfr
  exact hfr.1 hA'
def

Good

L315 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.Good
Documentation

A local section whose two pullbacks agree with the prescribed sections on the closed cover.

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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section Core
variable {X Z₁ Z₂ : Scheme.{u}} (i₁ : Z₁ ⟶ X) (i₂ : Z₂ ⟶ X)
  {L : X.Modules} (t₁ : Γ((Modules.pullback i₁).obj L, ⊤)) (t₂ : Γ((Modules.pullback i₂).obj L, ⊤))
Lean source · statement
def Good (U : X.Opens) (s : Γ(L, U)) : Prop
lemma

map

L320 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.Good.map
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section Core
variable {X Z₁ Z₂ : Scheme.{u}} (i₁ : Z₁ ⟶ X) (i₂ : Z₂ ⟶ X)
  {L : X.Modules} (t₁ : Γ((Modules.pullback i₁).obj L, ⊤)) (t₂ : Γ((Modules.pullback i₂).obj L, ⊤))
variable {i₁ i₂ t₁ t₂}
Lean source · statement
lemma Good.map {U V : X.Opens} (hVU : V ≤ U) {s : Γ(L, U)} (hs : Good i₁ i₂ t₁ t₂ U s) :
    Good i₁ i₂ t₁ t₂ V (L.presheaf.map (homOfLE hVU).op s)
lemma

unique

L326 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.Good.unique
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section Core
variable {X Z₁ Z₂ : Scheme.{u}} (i₁ : Z₁ ⟶ X) (i₂ : Z₂ ⟶ X)
  {L : X.Modules} (t₁ : Γ((Modules.pullback i₁).obj L, ⊤)) (t₂ : Γ((Modules.pullback i₂).obj L, ⊤))
variable {i₁ i₂ t₁ t₂}
Lean source · statement
lemma Good.unique [IsClosedImmersion i₁] [IsClosedImmersion i₂] [IsReduced X]
    (hcover : Set.range i₁.base ∪ Set.range i₂.base = Set.univ) {V : X.Opens} {e : Γ(L, V)} (he :
      IsFrameOn e V) {s s' : Γ(L, V)}
    (hs : Good i₁ i₂ t₁ t₂ V s) (hs' : Good i₁ i₂ t₁ t₂ V s') : s = s'
lemma

exists_of_isFrameOn

L349 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.Good.exists_of_isFrameOn
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section Core
variable {X Z₁ Z₂ : Scheme.{u}} (i₁ : Z₁ ⟶ X) (i₂ : Z₂ ⟶ X)
  {L : X.Modules} (t₁ : Γ((Modules.pullback i₁).obj L, ⊤)) (t₂ : Γ((Modules.pullback i₂).obj L, ⊤))
variable {i₁ i₂ t₁ t₂}
Lean source · full declaration
lemma Good.exists_of_isFrameOn {P : Scheme.{u}} (p₁ : P ⟶ Z₁) (p₂ : P ⟶ Z₂) (hc : p₁ ≫ i₁ = p₂ ≫ i₂)
    (hP : ∀ (U : X.Opens) (g₁ : Γ(Z₁, i₁ ⁻¹ᵁ U)) (g₂ : Γ(Z₂, i₂ ⁻¹ᵁ U)),
      P.presheaf.map (eqToHom (show p₂ ⁻¹ᵁ (i₂ ⁻¹ᵁ U) = p₁ ⁻¹ᵁ (i₁ ⁻¹ᵁ U) by
        rw [← Scheme.Hom.comp_preimage, ← Scheme.Hom.comp_preimage, hc])).op (p₁.app (i₁ ⁻¹ᵁ U) g₁)
          =
        p₂.app (i₂ ⁻¹ᵁ U) g₂ →
      ∃ f : Γ(X, U), i₁.app U f = g₁ ∧ i₂.app U f = g₂)
    (hA : ((pullbackCongr hc).hom.app L).app ⊤
        (((pullbackComp p₁ i₁).hom.app L).app ⊤ (pullbackLocalSection p₁ t₁)) =
      ((pullbackComp p₂ i₂).hom.app L).app ⊤ (pullbackLocalSection p₂ t₂))
    {U : X.Opens} {e : Γ(L, U)} (he : IsFrameOn e U) :
    ∃ s : Γ(L, U), Good i₁ i₂ t₁ t₂ U s := by
  obtain ⟨g₁, hg₁⟩ := ((he.pullbackLocalSection i₁).bijective le_rfl le_rfl).2 (res i₁ t₁ U)
  obtain ⟨g₂, hg₂⟩ := ((he.pullbackLocalSection i₂).bijective le_rfl le_rfl).2 (res i₂ t₂ U)
  change g₁ • _ = _ at hg₁
  change g₂ • _ = _ at hg₂
  rw [map_homOfLE_rfl] at hg₁ hg₂
  obtain ⟨f, hf₁, hf₂⟩ := hP U g₁ g₂
    (map_app_eq_app_of_agree i₁ i₂ t₁ t₂ p₁ p₂ hc hA he g₁ g₂ hg₁.symm hg₂.symm)
  refine ⟨f • e, ?_, ?_⟩
  · rw [pullbackLocalSection_smul, hf₁, hg₁]
  · rw [pullbackLocalSection_smul, hf₂, hg₂]
lemma

exists_glue

L376 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.exists_glue
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section Glue
Lean source · statement
lemma exists_glue {Y : Scheme.{u}} (M : Y.Modules) {ι : Type u} (U : ι → Y.Opens) (hU : (⊤ :
  Y.Opens) ≤ iSup U)
    (sf : ∀ a, Γ(M, U a))
    (h : ∀ a b, M.presheaf.map (homOfLE (inf_le_left : U a ⊓ U b ≤ U a)).op (sf a) =
      M.presheaf.map (homOfLE (inf_le_right : U a ⊓ U b ≤ U b)).op (sf b)) :
    ∃ s : Γ(M, ⊤), ∀ a, M.presheaf.map (homOfLE (le_top : U a ≤ ⊤)).op s = sf a
lemma

eq_of_locally_eq

L387 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.eq_of_locally_eq
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section Glue
Lean source · statement
lemma eq_of_locally_eq {Y : Scheme.{u}} (M : Y.Modules) {ι : Type u} (U : ι → Y.Opens) (V : Y.Opens)
    (hV : V ≤ iSup U) (iUV : ∀ a, U a ≤ V) {s t : Γ(M, V)}
    (h : ∀ a, M.presheaf.map (homOfLE (iUV a)).op s = M.presheaf.map (homOfLE (iUV a)).op t) : s =
      t
theorem

existsUnique_pullbackLocalSection_eq

L401 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.existsUnique_pullbackLocalSection_eq
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
section Glue
variable {X Z₁ Z₂ : Scheme.{u}} (i₁ : Z₁ ⟶ X) (i₂ : Z₂ ⟶ X) [IsClosedImmersion i₁]
  [IsClosedImmersion i₂]
  [IsReduced X] (hcover : Set.range i₁.base ∪ Set.range i₂.base = Set.univ)
  {L : X.Modules} (hL : IsInvertible L)
  (t₁ : Γ((Modules.pullback i₁).obj L, ⊤)) (t₂ : Γ((Modules.pullback i₂).obj L, ⊤))
include hcover hL in
Lean source · full declaration
theorem existsUnique_pullbackLocalSection_eq {P : Scheme.{u}} (p₁ : P ⟶ Z₁) (p₂ : P ⟶ Z₂)
    (hc : p₁ ≫ i₁ = p₂ ≫ i₂)
    (hP : ∀ (U : X.Opens) (g₁ : Γ(Z₁, i₁ ⁻¹ᵁ U)) (g₂ : Γ(Z₂, i₂ ⁻¹ᵁ U)),
      P.presheaf.map (eqToHom (show p₂ ⁻¹ᵁ (i₂ ⁻¹ᵁ U) = p₁ ⁻¹ᵁ (i₁ ⁻¹ᵁ U) by
        rw [← Scheme.Hom.comp_preimage, ← Scheme.Hom.comp_preimage, hc])).op (p₁.app (i₁ ⁻¹ᵁ U) g₁)
          =
        p₂.app (i₂ ⁻¹ᵁ U) g₂ →
      ∃ f : Γ(X, U), i₁.app U f = g₁ ∧ i₂.app U f = g₂)
    (hA : ((pullbackCongr hc).hom.app L).app ⊤
        (((pullbackComp p₁ i₁).hom.app L).app ⊤ (pullbackLocalSection p₁ t₁)) =
      ((pullbackComp p₂ i₂).hom.app L).app ⊤ (pullbackLocalSection p₂ t₂)) :
    ∃ s : Γ(L, ⊤), (pullbackLocalSection i₁ s = t₁ ∧ pullbackLocalSection i₂ s = t₂) ∧
      ∀ s' : Γ(L, ⊤), pullbackLocalSection i₁ s' = t₁ → pullbackLocalSection i₂ s' = t₂ → s' = s :=
        by
  choose U e hxU he using fun x : X => exists_isFrameOn hL x
  have hUtop : (⊤ : X.Opens) ≤ iSup U := fun x _ => Opens.mem_iSup.2 ⟨x, hxU x⟩
  choose sf hsf using fun x : X =>
    Good.exists_of_isFrameOn (i₁ := i₁) (i₂ := i₂) (t₁ := t₁) (t₂ := t₂) p₁ p₂ hc hP hA (he x)
  have hcompat : ∀ a b, L.presheaf.map (homOfLE (inf_le_left : U a ⊓ U b ≤ U a)).op (sf a) =
      L.presheaf.map (homOfLE (inf_le_right : U a ⊓ U b ≤ U b)).op (sf b) := fun a b =>
    Good.unique hcover (((he a).map (homOfLE inf_le_left)).mono inf_le_left)
      ((hsf a).map inf_le_left) ((hsf b).map inf_le_right)
  obtain ⟨s, hs⟩ := exists_glue L U hUtop sf hcompat
  have hGood_top : ∀ s' : Γ(L, ⊤),
      Good i₁ i₂ t₁ t₂ ⊤ s' ↔ (pullbackLocalSection i₁ s' = t₁ ∧ pullbackLocalSection i₂ s' = t₂)
        := by
    intro s'
    change (pullbackLocalSection i₁ s' = res i₁ t₁ ⊤ ∧ pullbackLocalSection i₂ s' = res i₂ t₂ ⊤) ↔ _
    rw [res_top, res_top]
  have hsGood : Good i₁ i₂ t₁ t₂ ⊤ s := by
    constructor
    · apply eq_of_locally_eq ((Modules.pullback i₁).obj L) (fun x => i₁ ⁻¹ᵁ U x) (i₁ ⁻¹ᵁ ⊤)
        (fun z _ => Opens.mem_iSup.2 ⟨i₁.base z, hxU (i₁.base z)⟩) (fun x => fun z _ =>
          Set.mem_univ _)
      intro x
      rw [map_homOfLE_pullbackLocalSection i₁ (le_top : U x ≤ ⊤) s, hs x, (hsf x).1,
        map_res i₁ t₁ (le_top : U x ≤ ⊤)]
    · apply eq_of_locally_eq ((Modules.pullback i₂).obj L) (fun x => i₂ ⁻¹ᵁ U x) (i₂ ⁻¹ᵁ ⊤)
        (fun z _ => Opens.mem_iSup.2 ⟨i₂.base z, hxU (i₂.base z)⟩) (fun x => fun z _ =>
          Set.mem_univ _)
      intro x
      rw [map_homOfLE_pullbackLocalSection i₂ (le_top : U x ≤ ⊤) s, hs x, (hsf x).2,
        map_res i₂ t₂ (le_top : U x ≤ ⊤)]
  refine ⟨s, (hGood_top s).1 hsGood, fun s' h₁ h₂ => ?_⟩
  have hs'Good : Good i₁ i₂ t₁ t₂ ⊤ s' := (hGood_top s').2 ⟨h₁, h₂⟩
  refine eq_of_locally_eq L U ⊤ hUtop (fun _ => le_top) fun x => ?_
  exact Good.unique hcover (he x) (hs'Good.map le_top) (hsGood.map le_top)
theorem

exists_unique_section_of_pullbackSection_closedCover

L451 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover.AlgebraicGeometry.Scheme.Modules.GlueSect.exists_unique_section_of_pullbackSection_closedCover
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_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace GlueSect
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
Lean source · statement
theorem exists_unique_section_of_pullbackSection_closedCover
    {X Z₁ Z₂ : Scheme.{u}} (i₁ : Z₁ ⟶ X) (i₂ : Z₂ ⟶ X) [IsClosedImmersion i₁] [IsClosedImmersion
      i₂] [IsReduced X]
    (hcover : Set.range i₁.base ∪ Set.range i₂.base = Set.univ)
    (L : X.Modules) (hL : Scheme.Modules.IsInvertible L)
    (σ₁ : 𝟙_ Z₁.Modules ⟶ (Scheme.Modules.pullback i₁).obj L) (σ₂ : 𝟙_ Z₂.Modules ⟶
      (Scheme.Modules.pullback i₂).obj L)
    (hagree : Scheme.Modules.pullbackSection (pullback.fst i₁ i₂) σ₁ ≫
        ((Scheme.Modules.pullbackComp (pullback.fst i₁ i₂) i₁).app L).hom ≫
          ((Scheme.Modules.pullbackCongr (pullback.condition (f := i₁) (g := i₂))).app L).hom =
      Scheme.Modules.pullbackSection (pullback.snd i₁ i₂) σ₂ ≫
        ((Scheme.Modules.pullbackComp (pullback.snd i₁ i₂) i₂).app L).hom) :
    ∃ σ : 𝟙_ X.Modules ⟶ L, Scheme.Modules.pullbackSection i₁ σ = σ₁ ∧
      Scheme.Modules.pullbackSection i₂ σ = σ₂ ∧
      ∀ σ' : 𝟙_ X.Modules ⟶ L, Scheme.Modules.pullbackSection i₁ σ' = σ₁ →
        Scheme.Modules.pullbackSection i₂ σ' = σ₂ → σ' = σ
theorem

exists_unique_section_of_pullbackSection_closedCover

L503 ↗
AlgebraicGeometry.Scheme.Modules.exists_unique_section_of_pullbackSection_closedCover
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits _root_.CategoryTheory.MonoidalCategory
  _root_.AlgebraicGeometry AlgebraicGeometry in
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.exists_unique_section_of_pullbackSection_closedCover
    {X Z₁ Z₂ : Scheme.{u}} (i₁ : Z₁ ⟶ X) (i₂ : Z₂ ⟶ X) [IsClosedImmersion i₁] [IsClosedImmersion
      i₂] [IsReduced X]
    (hcover : Set.range i₁.base ∪ Set.range i₂.base = Set.univ)
    (L : X.Modules) (hL : Scheme.Modules.IsInvertible L)
    (σ₁ : 𝟙_ Z₁.Modules ⟶ (Scheme.Modules.pullback i₁).obj L) (σ₂ : 𝟙_ Z₂.Modules ⟶
      (Scheme.Modules.pullback i₂).obj L)
    (hagree : Scheme.Modules.pullbackSection (pullback.fst i₁ i₂) σ₁ ≫
        ((Scheme.Modules.pullbackComp (pullback.fst i₁ i₂) i₁).app L).hom ≫
          ((Scheme.Modules.pullbackCongr (pullback.condition (f := i₁) (g := i₂))).app L).hom =
      Scheme.Modules.pullbackSection (pullback.snd i₁ i₂) σ₂ ≫
        ((Scheme.Modules.pullbackComp (pullback.snd i₁ i₂) i₂).app L).hom) :
    ∃ σ : 𝟙_ X.Modules ⟶ L, Scheme.Modules.pullbackSection i₁ σ = σ₁ ∧
      Scheme.Modules.pullbackSection i₂ σ = σ₂ ∧
      ∀ σ' : 𝟙_ X.Modules ⟶ L, Scheme.Modules.pullbackSection i₁ σ' = σ₁ →
        Scheme.Modules.pullbackSection i₂ σ' = σ₂ → σ' = σ

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