NYLL
Module

Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial
21 declarations indexed from sourceView source ↗

Module documentation

Global sections and pushforward of locally trivial modules

For a scheme with a two-affine-open cover, the pushforward of a locally trivial module is the sheaf associated to its module of global sections on the affine base.

Imports3
Imported by5

Declarations

abbrev

res

L49 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.res
Documentation

Restrict a module section to a smaller open.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
abbrev res {W W' : X.Opens} (h : W' ≤ W) : Γ(M, W) → Γ(M, W')
abbrev

rres

L53 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.rres
Documentation

Restrict a regular function to a smaller open.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
abbrev rres (X : Scheme.{u}) {W W' : X.Opens} (h : W' ≤ W) : Γ(X, W) → Γ(X, W')
lemma

map_eq_res

L58 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.map_eq_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_isIso_fromTildeGamma_pushforward_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
Lean source · statement
lemma map_eq_res {W W' : X.Opens} (i : W' ⟶ W) (s : Γ(M, W)) : M.presheaf.map i.op s = res M i.le s
lemma

res_res

L62 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.res_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_isIso_fromTildeGamma_pushforward_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
Lean source · statement
lemma res_res {W W' W'' : X.Opens} (h : W' ≤ W) (h' : W'' ≤ W') (s : Γ(M, W)) :
    res M h' (res M h s) = res M (h'.trans h) s
lemma

rres_rres

L68 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.rres_rres
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
Lean source · statement
lemma rres_rres {W W' W'' : X.Opens} (h : W' ≤ W) (h' : W'' ≤ W') (t : Γ(X, W)) :
    rres X h' (rres X h t) = rres X (h'.trans h) t
lemma

res_smul

L74 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.res_smul
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
Lean source · statement
lemma res_smul {W W' : X.Opens} (h : W' ≤ W) (t : Γ(X, W)) (s : Γ(M, W)) :
    res M h (t • s) = rres X h t • res M h s
lemma

res_add

L78 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.res_add
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
Lean source · statement
lemma res_add {W W' : X.Opens} (h : W' ≤ W) (s s' : Γ(M, W)) : res M h (s + s') = res M h s + res M
  h s'
lemma

res_sub

L82 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.res_sub
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
Lean source · statement
lemma res_sub {W W' : X.Opens} (h : W' ≤ W) (s s' : Γ(M, W)) : res M h (s - s') = res M h s - res M
  h s'
lemma

res_zero

L86 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.res_zero
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
Lean source · statement
lemma res_zero {W W' : X.Opens} (h : W' ≤ W) : res M h (0 : Γ(M, W)) = 0
lemma

rres_pow

L88 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.rres_pow
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
Lean source · statement
lemma rres_pow {W W' : X.Opens} (h : W' ≤ W) (t : Γ(X, W)) (n : ℕ) : rres X h (t ^ n) = rres X h t ^
  n
lemma

rres_refl

L92 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.rres_refl
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
Lean source · statement
lemma rres_refl {W : X.Opens} (h : W ≤ W) (t : Γ(X, W)) : rres X h t = t
theorem

exists_pow_smul_eq_zero_of_res_basicOpen_eq_zero

L97 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.exists_pow_smul_eq_zero_of_res_basicOpen_eq_zero
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
Lean source · statement
theorem exists_pow_smul_eq_zero_of_res_basicOpen_eq_zero
    (U0 U1 : X.Opens) (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hsup : U0 ⊔ U1 = ⊤)
    (htriv : ∀ x : X, ∃ (V : X.Opens), x ∈ V ∧
      Nonempty ((Scheme.Modules.pullback V.ι).obj M ≅ SheafOfModules.unit V.toScheme.ringCatSheaf))
    (t : Γ(X, ⊤)) (V : X.Opens) (hV : V = X.basicOpen t) (s : Γ(M, ⊤))
    (hs : res M (le_top (a := V)) s = 0) :
    ∃ n : ℕ, t ^ n • s = 0
theorem

exists_glue₂

L131 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.exists_glue₂
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
Lean source · statement
theorem exists_glue₂ (U0 U1 : X.Opens) (hsup : U0 ⊔ U1 = ⊤) (z0 : Γ(M, U0)) (z1 : Γ(M, U1))
    (h : res M (inf_le_left : U0 ⊓ U1 ≤ U0) z0 = res M (inf_le_right : U0 ⊓ U1 ≤ U1) z1) :
    ∃ s : Γ(M, ⊤), res M le_top s = z0 ∧ res M le_top s = z1
theorem

exists_res_eq_pow_smul

L154 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.exists_res_eq_pow_smul
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
Lean source · statement
theorem exists_res_eq_pow_smul
    (U0 U1 : X.Opens) (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hsup : U0 ⊔ U1 = ⊤)
    (hinf : IsAffineOpen (U0 ⊓ U1))
    (htriv : ∀ x : X, ∃ (V : X.Opens), x ∈ V ∧
      Nonempty ((Scheme.Modules.pullback V.ι).obj M ≅ SheafOfModules.unit V.toScheme.ringCatSheaf))
    (t : Γ(X, ⊤)) (V : X.Opens) (hV : V = X.basicOpen t) (y : Γ(M, V)) :
    ∃ (n : ℕ) (s : Γ(M, ⊤)), res M (le_top (a := V)) s = rres X (le_top (a := V)) t ^ n • y
def

toSecRingHom

L227 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.toSecRingHom
Documentation

The homomorphism from the base ring to sections over a preimage open.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
section pushforward
variable {A : Type u} [CommRing A] (π : X ⟶ Spec (.of A))
Lean source · statement
def toSecRingHom (U : (Spec (CommRingCat.of A)).Opens) : A →+* Γ(X, π ⁻¹ᵁ U)
lemma

smul_pushforward_eq

L232 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.smul_pushforward_eq
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
section pushforward
variable {A : Type u} [CommRing A] (π : X ⟶ Spec (.of A))
Lean source · full declaration
lemma smul_pushforward_eq (U : (Spec (CommRingCat.of A)).Opens) (a : A)
    (s : ((modulesSpecToSheaf (R := .of A)).obj ((Scheme.Modules.pushforward π).obj M)).1.obj (op
        U)) :
    a • s = (toSecRingHom π U a) • (show Γ(M, π ⁻¹ᵁ U) from s) := rfl
def

secTop

L238 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.secTop
Documentation

The global section obtained by pulling back a base ring element.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
section pushforward
variable {A : Type u} [CommRing A] (π : X ⟶ Spec (.of A))
Lean source · statement
def secTop (a : A) : Γ(X, ⊤)
lemma

toSecRingHom_eq

L240 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.toSecRingHom_eq
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
section pushforward
variable {A : Type u} [CommRing A] (π : X ⟶ Spec (.of A))
Lean source · statement
lemma toSecRingHom_eq (U : (Spec (CommRingCat.of A)).Opens) (a : A) :
    toSecRingHom π U a = rres X (le_top (a := π ⁻¹ᵁ U)) (secTop π a)
lemma

preimage_basicOpen_eq

L251 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.preimage_basicOpen_eq
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
section pushforward
variable {A : Type u} [CommRing A] (π : X ⟶ Spec (.of A))
Lean source · statement
lemma preimage_basicOpen_eq (f : A) : π ⁻¹ᵁ PrimeSpectrum.basicOpen f = X.basicOpen (secTop π f)
theorem

isIso_fromTildeGamma_pushforward

L258 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.isIso_fromTildeGamma_pushforward
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
section pushforward
variable {A : Type u} [CommRing A] (π : X ⟶ Spec (.of A))
Lean source · statement
theorem isIso_fromTildeGamma_pushforward
    (U0 U1 : X.Opens) (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hsup : U0 ⊔ U1 = ⊤)
    (hinf : IsAffineOpen (U0 ⊓ U1))
    (htriv : ∀ x : X, ∃ (V : X.Opens), x ∈ V ∧
      Nonempty ((Scheme.Modules.pullback V.ι).obj M ≅ SheafOfModules.unit V.toScheme.ringCatSheaf))
          :
    IsIso (Scheme.Modules.fromTildeΓ (R := .of A) ((Scheme.Modules.pushforward π).obj M))
theorem

isIso_fromTildeGamma_pushforward_of_locallyTrivial

L325 ↗
AlgebraicGeometry.Scheme.Modules.isIso_fromTildeGamma_pushforward_of_locallyTrivial
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_pushforward_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.Scheme.Modules in
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.isIso_fromTildeGamma_pushforward_of_locallyTrivial
    {A : Type u} [CommRing A] {X : Scheme.{u}} (π : X ⟶ Spec (.of A)) (𝒱 : X.TwoAffineOpenCover)
    (M : X.Modules)
    (htriv : ∀ x : X, ∃ (V : X.Opens), x ∈ V ∧
      Nonempty ((Scheme.Modules.pullback V.ι).obj M ≅ SheafOfModules.unit V.toScheme.ringCatSheaf))
          :
    IsIso (Scheme.Modules.fromTildeΓ (R := .of A) ((Scheme.Modules.pushforward π).obj M))

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