Module

TwoAffineOpenCover.lean

Nyll.SchemeTheory.Cohomology.Cech.TwoAffineOpenCover

21 declarations indexed from sourceView source ↗

Module documentation

Two affine charts with affine intersection, their section-ring cover and its scalar extension.

Imports4

Nyll.SchemeTheory.Cohomology.Cech.TwoChartCech
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.AlgebraicGeometry.Morphisms.Affine

Imported by272

structure

TwoAffineOpenCover

L31 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover

Documentation

A cover of X by two affine open subschemes whose intersection is also affine.

Source context 4 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite

Lean source · full declaration

structure Scheme.TwoAffineOpenCover (X : Scheme.{u}) where
  /-- The first open subset of the cover. -/
  U0 : X.Opens
  /-- The second open subset of the cover. -/
  U1 : X.Opens
  /-- The first open subset is affine. -/
  isAffineOpen_U0 : IsAffineOpen U0
  /-- The second open subset is affine. -/
  isAffineOpen_U1 : IsAffineOpen U1
  /-- The two open subsets cover the whole scheme. -/
  sup_eq_top : U0 ⊔ U1 = ⊤
  /-- The intersection of the two open subsets is affine. -/
  isAffineOpen_inf : IsAffineOpen (U0 ⊓ U1)

abbrev

specMap

L48 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.specMap

Documentation

The morphism of affine schemes induced by the R-algebra structure on A.

Source context 5 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace Scheme.TwoAffineOpenCover

Lean source · statement

abbrev specMap (R A : Type u) [CommRing R] [CommRing A] [Algebra R A] : Spec (.of A) ⟶ Spec (.of
    R)

def

algebraOfHom

L55 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.algebraOfHom

Documentation

The R-algebra structure on sections over U induced by the morphism c.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}

Lean source · statement

def algebraOfHom (c : X ⟶ Spec (.of R)) (U : X.Opens) : Algebra R Γ(X, U)

theorem

algebraMap_algebraOfHom

L58 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.algebraMap_algebraOfHom

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}

Lean source · statement

theorem algebraMap_algebraOfHom (c : X ⟶ Spec (.of R)) (U : X.Opens) (r : R) :
    (algebraOfHom c U).algebraMap r = (c.appLE ⊤ U le_top).hom ((Scheme.ΓSpecIso (.of
      R)).inv.hom r)

def

restrictAlgHom

L64 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.restrictAlgHom

Documentation

The restriction map on sections as an R-algebra homomorphism for the structures induced by c.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}

Lean source · full declaration

def restrictAlgHom (c : X ⟶ Spec (.of R)) {U V : X.Opens} (h : V ≤ U) :
    letI := algebraOfHom c U; letI := algebraOfHom c V
    Γ(X, U) →ₐ[R] Γ(X, V) :=
  letI := algebraOfHom c U; letI := algebraOfHom c V
  { (X.presheaf.map (homOfLE h).op).hom with
    commutes' := fun r => by
      change (c.appLE ⊤ U le_top ≫ X.presheaf.map (homOfLE h).op).hom _ = (c.appLE ⊤ V le_top).hom _
      exact congrArg
        (fun φ => φ.hom ((Scheme.ΓSpecIso (.of R)).inv.hom r))
        (Scheme.Hom.appLE_map c (by simp) (homOfLE h).op) }

def

cover

L79 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.cover

Documentation

The two-chart algebraic cover formed by the section rings of the affine opens and their intersection.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))

Lean source · statement

def cover : TwoChartCech.Cover.{u, u} R

theorem

cover_A0

L87 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.cover_A0

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))

Lean source · statement

theorem cover_A0 : (𝒱.cover c).A0 = Γ(X, 𝒱.U0)

theorem

cover_A1

L88 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.cover_A1

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))

Lean source · statement

theorem cover_A1 : (𝒱.cover c).A1 = Γ(X, 𝒱.U1)

theorem

cover_A01

L89 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.cover_A01

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))

Lean source · statement

theorem cover_A01 : (𝒱.cover c).A01 = Γ(X, 𝒱.U0 ⊓ 𝒱.U1)

theorem

cover_ρ0_apply

L90 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.cover_ρ0_apply

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))

Lean source · statement

theorem cover_ρ0_apply (x : (𝒱.cover c).A0) :
    (𝒱.cover c).ρ0 x = (X.presheaf.map (homOfLE (inf_le_left : 𝒱.U0 ⊓ 𝒱.U1 ≤ 𝒱.U0)).op).hom x

theorem

cover_ρ1_apply

L92 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.cover_ρ1_apply

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))

Lean source · statement

theorem cover_ρ1_apply (x : (𝒱.cover c).A1) :
    (𝒱.cover c).ρ1 x = (X.presheaf.map (homOfLE (inf_le_right : 𝒱.U0 ⊓ 𝒱.U1 ≤ 𝒱.U1)).op).hom x

abbrev

structureSheafSections

L97 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.structureSheafSections

Documentation

The two-chart section data of the structure sheaf.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))

Lean source · statement

abbrev structureSheafSections : TwoChartCech.Sections (𝒱.cover c)

abbrev

lineBundleSections

L100 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.lineBundleSections

Documentation

The two-chart section data for the line bundle glued by the unit t on the intersection.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))

Lean source · statement

abbrev lineBundleSections (t : (𝒱.cover c).A01ˣ) : TwoChartCech.Sections (𝒱.cover c)

theorem

res_res

L104 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.res_res

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
omit [CommRing R] in

Lean source · statement

theorem res_res {V₁ V₂ V₃ : X.Opens} (h₂₁ : V₂ ≤ V₁) (h₃₂ : V₃ ≤ V₂) (x : Γ(X, V₁)) :
    (X.presheaf.map (homOfLE h₃₂).op).hom ((X.presheaf.map (homOfLE h₂₁).op).hom x) =
      (X.presheaf.map (homOfLE (h₃₂.trans h₂₁)).op).hom x

theorem

restrict_mem_H0

L110 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.restrict_mem_H0

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))

Lean source · statement

theorem restrict_mem_H0 (s : Γ(X, ⊤)) :
    ((X.presheaf.map (homOfLE (le_top : 𝒱.U0 ≤ ⊤)).op).hom s,
      (X.presheaf.map (homOfLE (le_top : 𝒱.U1 ≤ ⊤)).op).hom s)
      ∈ (𝒱.structureSheafSections c).H0

def

toH0

L124 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.toH0

Documentation

The map sending a global section to its compatible pair of restrictions in degree-zero Cech cohomology.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))

Lean source · full declaration

def toH0 : letI := algebraOfHom c ⊤; Γ(X, ⊤) →ₗ[R] (𝒱.structureSheafSections c).H0 :=
  letI := algebraOfHom c ⊤; letI := algebraOfHom c 𝒱.U0; letI := algebraOfHom c 𝒱.U1
  LinearMap.codRestrict _
    (((restrictAlgHom c (le_top : 𝒱.U0 ≤ ⊤)).toLinearMap).prod
      ((restrictAlgHom c (le_top : 𝒱.U1 ≤ ⊤)).toLinearMap))
    (fun s => 𝒱.restrict_mem_H0 c s)

theorem

toH0_apply_coe

L131 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.toH0_apply_coe

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))

Lean source · full declaration

theorem toH0_apply_coe (s : Γ(X, ⊤)) :
    letI := algebraOfHom c ⊤
    ((𝒱.toH0 c s : (𝒱.structureSheafSections c).M0 × (𝒱.structureSheafSections c).M1)) =
      ((X.presheaf.map (homOfLE (le_top : 𝒱.U0 ≤ ⊤)).op).hom s,
        (X.presheaf.map (homOfLE (le_top : 𝒱.U1 ≤ ⊤)).op).hom s) := rfl

theorem

isAffineHom_fst

L141 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.isAffineHom_fst

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
section Pullback
variable (A : Type u) [CommRing A] [Algebra R A]

Lean source · statement

theorem isAffineHom_fst : IsAffineHom (Limits.pullback.fst c (specMap R A))

def

pullback

L148 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback

Documentation

The two-affine-open cover obtained by base change along the morphism from Spec A to Spec R.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
section Pullback
variable (A : Type u) [CommRing A] [Algebra R A]

Lean source · statement

def pullback : (Limits.pullback c (specMap R A)).TwoAffineOpenCover

theorem

pullback_U0

L157 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
section Pullback
variable (A : Type u) [CommRing A] [Algebra R A]

Lean source · statement

theorem pullback_U0 : (𝒱.pullback c A).U0 = (Limits.pullback.fst c (specMap R A)) ⁻¹ᵁ
    𝒱.U0

theorem

pullback_U1

L159 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
section Pullback
variable (A : Type u) [CommRing A] [Algebra R A]

Lean source · statement

theorem pullback_U1 : (𝒱.pullback c A).U1 = (Limits.pullback.fst c (specMap R A)) ⁻¹ᵁ
    𝒱.U1

Module documentation

Declarations