NYLL
Module

Scheme_TwoAffineOpenCover_toH0_bijective.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_toH0_bijective
8 declarations indexed from sourceView source ↗

Module documentation

Global sections identify with degree-zero Cech cohomology for a two-affine open cover. The sheaf condition supplies a ring equivalence with the equalizer of chart restrictions.

Imports1
Imported by3

Declarations

abbrev

eqLocus

L46 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.SheafCondition.eqLocus
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_toH0_bijective
open CategoryTheory
noncomputable section
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace SheafCondition
variable (X : Scheme.{u}) (U V : X.Opens)
Lean source · statement
abbrev _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.SheafCondition.eqLocus
    : Subring (Γ(X, U) × Γ(X, V))
theorem

mem_eqLocus_iff

L53 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_toH0_bijective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.SheafCondition.mem_eqLocus_iff
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_toH0_bijective
open CategoryTheory
noncomputable section
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace SheafCondition
variable (X : Scheme.{u}) (U V : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.SheafCondition
Lean source · statement
theorem mem_eqLocus_iff (s : Γ(X, U) × Γ(X, V)) :
    s ∈ eqLocus X U V ↔
      (X.presheaf.map (homOfLE inf_le_left : U ⊓ V ⟶ U).op).hom s.1
        = (X.presheaf.map (homOfLE inf_le_right : U ⊓ V ⟶ V).op).hom s.2
def

gammaEquiv

L60 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_toH0_bijective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.SheafCondition.gammaEquiv
Documentation

Identify global sections with matching sections on the two opens of a cover.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_toH0_bijective
open CategoryTheory
noncomputable section
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace SheafCondition
variable (X : Scheme.{u}) (U V : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.SheafCondition
Lean source · statement
def gammaEquiv (h : U ⊔ V = ⊤) : Γ(X, ⊤) ≃+* eqLocus X U V
theorem

map_comp_apply

L64 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_toH0_bijective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.SheafCondition.map_comp_apply
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_toH0_bijective
open CategoryTheory
noncomputable section
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace SheafCondition
variable (X : Scheme.{u}) (U V : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.SheafCondition
Lean source · statement
theorem map_comp_apply {W₁ W₂ W₃ : X.Opens} (f : W₁ ⟶ W₂) (g : W₂ ⟶ W₃) (a : Γ(X, W₃)) :
    (X.presheaf.map f.op).hom ((X.presheaf.map g.op).hom a)
      = (X.presheaf.map (f ≫ g).op).hom a
theorem

gammaEquiv_apply_fst

L69 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_toH0_bijective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.SheafCondition.gammaEquiv_apply_fst
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_toH0_bijective
open CategoryTheory
noncomputable section
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace SheafCondition
variable (X : Scheme.{u}) (U V : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.SheafCondition
Lean source · statement
theorem gammaEquiv_apply_fst (h : U ⊔ V = ⊤) (a : Γ(X, ⊤)) :
    (gammaEquiv X U V h a).1.1 = (X.presheaf.map (homOfLE (le_top : U ≤ ⊤)).op).hom a
theorem

gammaEquiv_apply_snd

L79 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_toH0_bijective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.SheafCondition.gammaEquiv_apply_snd
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_toH0_bijective
open CategoryTheory
noncomputable section
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace SheafCondition
variable (X : Scheme.{u}) (U V : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.SheafCondition
Lean source · statement
theorem gammaEquiv_apply_snd (h : U ⊔ V = ⊤) (a : Γ(X, ⊤)) :
    (gammaEquiv X U V h a).1.2 = (X.presheaf.map (homOfLE (le_top : V ≤ ⊤)).op).hom a
theorem

toH0_bijective'

L96 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_toH0_bijective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.toH0_bijective'
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_toH0_bijective
open CategoryTheory
noncomputable section
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
open SheafCondition
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover)
    (c : X ⟶ Spec (.of R))
Lean source · full declaration
theorem toH0_bijective' : letI := algebraOfHom c ⊤; Function.Bijective (𝒱.toH0 c) := by
  let := algebraOfHom c ⊤
  have hpair : ∀ s : Γ(X, ⊤),
      ((𝒱.toH0 c s : (𝒱.structureSheafSections c).M0 × (𝒱.structureSheafSections c).M1))
        = (gammaEquiv X 𝒱.U0 𝒱.U1 𝒱.sup_eq_top s).1 := fun s => by
    rw [toH0_apply_coe]
    exact Prod.ext (gammaEquiv_apply_fst X _ _ _ s).symm (gammaEquiv_apply_snd X _ _ _ s).symm
  constructor
  · intro s s' hss'
    apply (gammaEquiv X 𝒱.U0 𝒱.U1 𝒱.sup_eq_top).injective
    apply Subtype.ext
    rw [← hpair, ← hpair, hss']
  · rintro ⟨p, hp⟩
    have hp' : p ∈ eqLocus X 𝒱.U0 𝒱.U1 :=
      (mem_eqLocus_iff X 𝒱.U0 𝒱.U1 p).mpr ((TwoChartCech.Cover.mem_H0_structureSheaf_iff _ p).mp hp)
    refine ⟨(gammaEquiv X 𝒱.U0 𝒱.U1 𝒱.sup_eq_top).symm ⟨p, hp'⟩, Subtype.ext ?_⟩
    rw [hpair, RingEquiv.apply_symm_apply]
theorem

toH0_bijective

L116 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.toH0_bijective
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_toH0_bijective
open CategoryTheory
noncomputable section
universe u
Lean source · full declaration
theorem _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.toH0_bijective
    {R : Type u} [CommRing R] {X : AlgebraicGeometry.Scheme.{u}}
    (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ AlgebraicGeometry.Spec (.of R)) :
    letI := AlgebraicGeometry.Scheme.TwoAffineOpenCover.algebraOfHom c ⊤
    Function.Bijective (𝒱.toH0 c) :=
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.toH0_bijective' 𝒱 c

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