NYLL
Module

Scheme_Modules_projective_sections_of_locallyTrivial.lean

Nyll.AlgebraicCurves.Geometry.Projective.Scheme_Modules_projective_sections_of_locallyTrivial
38 declarations indexed from sourceView source ↗

Module documentation

Projectivity of sections of locally trivial scheme modules on affine open subsets.

Imports4
Imported by25

Declarations

abbrev

rM

L50 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.rM
Documentation

Restriction of module sections to a smaller open.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
abbrev rM {V W : X.Opens} (h : V ≤ W) : Γ(M, W) → Γ(M, V)
abbrev

rO

L54 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.rO
Documentation

Restriction of structure sheaf sections to a smaller open.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
abbrev rO {V W : X.Opens} (h : V ≤ W) : Γ(X, W) → Γ(X, V)
theorem

rM_rM

L57 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.rM_rM
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
theorem rM_rM {V₁ V₂ V₃ : X.Opens} (h₂₁ : V₂ ≤ V₁) (h₃₂ : V₃ ≤ V₂) (y : Γ(M, V₁)) :
    rM M h₃₂ (rM M h₂₁ y) = rM M (h₃₂.trans h₂₁) y
theorem

rO_rO

L63 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.rO_rO
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
omit M in
Lean source · statement
theorem rO_rO {V₁ V₂ V₃ : X.Opens} (h₂₁ : V₂ ≤ V₁) (h₃₂ : V₃ ≤ V₂) (g : Γ(X, V₁)) :
    rO h₃₂ (rO h₂₁ g) = rO (h₃₂.trans h₂₁) g
theorem

rM_self

L68 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.rM_self
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
theorem rM_self {V : X.Opens} (h : V ≤ V) (y : Γ(M, V)) : rM M h y = y
theorem

rO_self

L73 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.rO_self
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
omit M in
Lean source · statement
theorem rO_self {V : X.Opens} (h : V ≤ V) (g : Γ(X, V)) : rO h g = g
theorem

rM_smul

L77 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.rM_smul
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
theorem rM_smul {V W : X.Opens} (h : V ≤ W) (g : Γ(X, W)) (y : Γ(M, W)) :
    rM M h (g • y) = rO h g • rM M h y
theorem

hat_eq

L84 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.hat_eq
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
section Transport
variable (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
Lean source · statement
theorem hat_eq {W : X.Opens} (hWV : W ≤ V) : V.ι ''ᵁ V.ι ⁻¹ᵁ W = W
theorem

le_hat

L87 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.le_hat
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
section Transport
variable (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
Lean source · statement
theorem le_hat {W : X.Opens} (hWV : W ≤ V) : W ≤ V.ι ''ᵁ V.ι ⁻¹ᵁ W
theorem

hat_le

L88 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.hat_le
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
section Transport
variable (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
Lean source · statement
theorem hat_le {W : X.Opens} (hWV : W ≤ V) : V.ι ''ᵁ V.ι ⁻¹ᵁ W ≤ W
def

eApp

L91 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.eApp
Documentation

The local trivialization applied to module sections over the image open.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
section Transport
variable (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
Lean source · statement
def eApp (W : X.Opens) (m : Γ(M, V.ι ''ᵁ V.ι ⁻¹ᵁ W)) : Γ(X, V.ι ''ᵁ V.ι ⁻¹ᵁ W)
def

eInv

L95 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.eInv
Documentation

The inverse local trivialization applied to structure sheaf sections over the image open.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
section Transport
variable (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
Lean source · statement
def eInv (W : X.Opens) (a : Γ(X, V.ι ''ᵁ V.ι ⁻¹ᵁ W)) : Γ(M, V.ι ''ᵁ V.ι ⁻¹ᵁ W)
theorem

eInv_eApp

L98 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.eInv_eApp
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
section Transport
variable (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
Lean source · statement
theorem eInv_eApp (W : X.Opens) (m : Γ(M, V.ι ''ᵁ V.ι ⁻¹ᵁ W)) : eInv M V e W (eApp M V e W m) =
    m
theorem

eApp_eInv

L106 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.eApp_eInv
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
section Transport
variable (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
Lean source · statement
theorem eApp_eInv (W : X.Opens) (a : Γ(X, V.ι ''ᵁ V.ι ⁻¹ᵁ W)) : eApp M V e W (eInv M V e W a) =
    a
theorem

eApp_zero

L116 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.eApp_zero
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
section Transport
variable (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
Lean source · statement
theorem eApp_zero (W : X.Opens) : eApp M V e W 0 = 0
theorem

eApp_injective

L118 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.eApp_injective
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
section Transport
variable (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
Lean source · statement
theorem eApp_injective (W : X.Opens) : Function.Injective (eApp M V e W)
theorem

restrict_smul_eq

L121 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.restrict_smul_eq
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
section Transport
variable (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
Lean source · statement
theorem restrict_smul_eq (W' : V.toScheme.Opens) (b : Γ(V.toScheme, W')) (m : Γ(M.restrict V.ι,
    W')) :
    (HSMul.hSMul (α := Γ(V.toScheme, W')) (β := Γ(M.restrict V.ι, W')) b m : Γ(M, V.ι ''ᵁ W'))
      = HSMul.hSMul (α := Γ(X, V.ι ''ᵁ W')) (β := Γ(M, V.ι ''ᵁ W')) ((Scheme.Hom.appIso V.ι
        W').inv b) m
theorem

eApp_smul

L127 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.eApp_smul
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
section Transport
variable (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
Lean source · statement
theorem eApp_smul (W : X.Opens) (a : Γ(X, V.ι ''ᵁ V.ι ⁻¹ᵁ W)) (m : Γ(M, V.ι ''ᵁ V.ι ⁻¹ᵁ W)) :
    eApp M V e W (a • m) = a * eApp M V e W m
theorem

unit_map_eq

L139 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.unit_map_eq
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
section Transport
variable (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
omit M e in
Lean source · statement
theorem unit_map_eq {W₁' W₂' : V.toScheme.Opens} (i : W₂' ⟶ W₁') (a : Γ(X, V.ι ''ᵁ W₁')) :
    ((Scheme.Modules.presheaf (SheafOfModules.unit V.toScheme.ringCatSheaf)).map i.op) a
      = (X.presheaf.map ((Scheme.Hom.opensFunctor V.ι).map i).op).hom a
theorem

eApp_res

L143 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.eApp_res
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
section Transport
variable (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
Lean source · statement
theorem eApp_res {W₁ W₂ : X.Opens} (h : W₂ ≤ W₁) (m : Γ(M, V.ι ''ᵁ V.ι ⁻¹ᵁ W₁)) :
    eApp M V e W₂ (rM M (Scheme.Hom.image_mono V.ι (Scheme.Hom.preimage_mono V.ι h)) m)
      = rO (Scheme.Hom.image_mono V.ι (Scheme.Hom.preimage_mono V.ι h)) (eApp M V e W₁ m)
def

ψ

L161 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.ψ
Documentation

The local trivialization transported to an open contained in its domain.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
section StepA
variable (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
Lean source · statement
def ψ {W : X.Opens} (hWV : W ≤ V) (m : Γ(M, W)) : Γ(X, W)
def

ψinv

L165 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.ψinv
Documentation

The inverse trivialization transported to an open contained in its domain.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
section StepA
variable (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
Lean source · statement
def ψinv {W : X.Opens} (hWV : W ≤ V) (a : Γ(X, W)) : Γ(M, W)
theorem

rM_roundtrip

L168 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.rM_roundtrip
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
section StepA
variable (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
Lean source · statement
theorem rM_roundtrip {W : X.Opens} (hWV : W ≤ V) (m : Γ(M, W)) : rM M (le_hat V hWV) (rM M
    (hat_le V hWV) m) = m
theorem

rM_roundtrip'

L171 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.rM_roundtrip'
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
section StepA
variable (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
Lean source · statement
theorem rM_roundtrip' {W : X.Opens} (hWV : W ≤ V) (m : Γ(M, V.ι ''ᵁ V.ι ⁻¹ᵁ W)) :
    rM M (hat_le V hWV) (rM M (le_hat V hWV) m) = m
theorem

rO_roundtrip

L175 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.rO_roundtrip
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
section StepA
variable (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
omit M e in
Lean source · statement
theorem rO_roundtrip {W : X.Opens} (hWV : W ≤ V) (a : Γ(X, W)) : rO (le_hat V hWV) (rO (hat_le V
    hWV) a) = a
theorem

rO_roundtrip'

L179 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.rO_roundtrip'
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
section StepA
variable (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
omit M e in
Lean source · statement
theorem rO_roundtrip' {W : X.Opens} (hWV : W ≤ V) (a : Γ(X, V.ι ''ᵁ V.ι ⁻¹ᵁ W)) :
    rO (hat_le V hWV) (rO (le_hat V hWV) a) = a
theorem

ψ_ψinv

L183 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.ψ_ψinv
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
section StepA
variable (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
Lean source · statement
theorem ψ_ψinv {W : X.Opens} (hWV : W ≤ V) (a : Γ(X, W)) : ψ M V e hWV (ψinv M V e hWV a) = a
theorem

ψinv_ψ

L187 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.ψinv_ψ
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
section StepA
variable (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
Lean source · statement
theorem ψinv_ψ {W : X.Opens} (hWV : W ≤ V) (m : Γ(M, W)) : ψinv M V e hWV (ψ M V e hWV m) = m
theorem

ψ_injective

L191 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.ψ_injective
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
section StepA
variable (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
Lean source · statement
theorem ψ_injective {W : X.Opens} (hWV : W ≤ V) : Function.Injective (ψ M V e hWV)
theorem

ψ_zero

L194 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.ψ_zero
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
section StepA
variable (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
Lean source · statement
theorem ψ_zero {W : X.Opens} (hWV : W ≤ V) : ψ M V e hWV 0 = 0
theorem

ψ_smul

L199 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.ψ_smul
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
section StepA
variable (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
Lean source · statement
theorem ψ_smul {W : X.Opens} (hWV : W ≤ V) (a : Γ(X, W)) (m : Γ(M, W)) :
    ψ M V e hWV (a • m) = a * ψ M V e hWV m
theorem

ψ_res

L208 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.LocTriv.ψ_res
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace LocTriv
variable {X : Scheme.{u}} (M : X.Modules)
section StepA
variable (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
Lean source · statement
theorem ψ_res {W₁ W₂ : X.Opens} (h₁ : W₁ ≤ V) (h : W₂ ≤ W₁) (m : Γ(M, W₁)) :
    ψ M V e (h.trans h₁) (rM M h m) = rO h (ψ M V e h₁ m)
theorem

ψ_add

L229 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.ψ_add
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Loc
open LocTriv
variable {X : Scheme.{u}} (M : X.Modules) (U : X.affineOpens) (f : Γ(X, U.1))
  (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
  (hfV : X.basicOpen f ≤ V)
Lean source · statement
theorem ψ_add {W : X.Opens} (hWV : W ≤ V) (m m' : Γ(M, W)) :
    ψ M V e hWV (m + m') = ψ M V e hWV m + ψ M V e hWV m'
def

gψ

L237 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.gψ
Documentation

The linear map to basic open sections obtained by restriction and local trivialization.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Loc
open LocTriv
variable {X : Scheme.{u}} (M : X.Modules) (U : X.affineOpens) (f : Γ(X, U.1))
  (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
  (hfV : X.basicOpen f ≤ V)
Lean source · full declaration
def gψ : Γ(M, U.1) →ₗ[Γ(X, U.1)] Γ(X, X.basicOpen f) where
  toFun m := ψ M V e hfV (rM M (X.basicOpen_le f) m)
  map_add' m m' := by
    simp only [rM, map_add]
    exact ψ_add M V e hfV _ _
  map_smul' a m := by
    rw [rM_smul, ψ_smul, Algebra.smul_def]
    rfl
theorem

gψ_apply

L246 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.gψ_apply
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Loc
open LocTriv
variable {X : Scheme.{u}} (M : X.Modules) (U : X.affineOpens) (f : Γ(X, U.1))
  (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
  (hfV : X.basicOpen f ≤ V)
Lean source · statement
theorem gψ_apply (m : Γ(M, U.1)) : gψ M U f V e hfV m = ψ M V e hfV (rM M (X.basicOpen_le f) m)
theorem

isLocalizedModule_gψ

L250 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.isLocalizedModule_gψ
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Loc
open LocTriv
variable {X : Scheme.{u}} (M : X.Modules) (U : X.affineOpens) (f : Γ(X, U.1))
  (V : X.Opens) (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
  (hfV : X.basicOpen f ≤ V)
include hfV in
Lean source · full declaration
theorem isLocalizedModule_gψ
    (htriv : ∀ x : X, ∃ (V : X.Opens), x ∈ V ∧
      Nonempty ((Scheme.Modules.pullback V.ι).obj M ≅ SheafOfModules.unit
        V.toScheme.ringCatSheaf)) :
    IsLocalizedModule (Submonoid.powers f) (gψ M U f V e hfV) where
  map_units s := by
    have := U.2.isLocalization_basicOpen f
    exact IsLocalizedModule.map_units (Algebra.linearMap Γ(X, U.1) Γ(X, X.basicOpen f)) s
  surj b := by
    obtain ⟨n, y, hy⟩ := (isLocalization_basicOpen_of_locallyTrivial M htriv U f).1 (ψinv M V e
      hfV b)
    refine ⟨(y, ⟨f ^ n, n, rfl⟩), ?_⟩
    change (f ^ n : Γ(X, U.1)) • b = ψ M V e hfV (rM M (X.basicOpen_le f) y)
    change (f ^ n : Γ(X, U.1)) • b = ψ M V e hfV (M.presheaf.map (homOfLE (X.basicOpen_le f)).op y)
    rw [hy, ψ_smul, ψ_ψinv, Algebra.smul_def]
    rfl
  exists_of_eq {m m'} h := by
    have h' : rM M (X.basicOpen_le f) m = rM M (X.basicOpen_le f) m' := ψ_injective M V e hfV h
    have h0 : M.presheaf.map (homOfLE (X.basicOpen_le f)).op (m - m') = 0 := by
      rw [map_sub]; exact sub_eq_zero.mpr h'
    obtain ⟨n, hn⟩ := (isLocalization_basicOpen_of_locallyTrivial M htriv U f).2 _ h0
    refine ⟨⟨f ^ n, n, rfl⟩, ?_⟩
    rw [smul_sub, sub_eq_zero] at hn
    exact hn
theorem

projective_sections

L278 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_Modules_projective_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.SectProj.projective_sections
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace SectProj
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open LocTriv in
Lean source · statement
theorem projective_sections
    {X : Scheme.{u}} (M : X.Modules)
    (htriv : ∀ x : X, ∃ (V : X.Opens), x ∈ V ∧
      Nonempty ((Scheme.Modules.pullback V.ι).obj M ≅ SheafOfModules.unit V.toScheme.ringCatSheaf))
    (U : X.affineOpens) :
    Module.Projective Γ(X, U.1) Γ(M, U.1)
theorem

projective_sections_of_locallyTrivial

L329 ↗
AlgebraicGeometry.Scheme.Modules.projective_sections_of_locallyTrivial
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_projective_sections_of_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.projective_sections_of_locallyTrivial
    {X : Scheme.{u}} (M : X.Modules)
    (htriv : ∀ x : X, ∃ (V : X.Opens), x ∈ V ∧
      Nonempty ((Scheme.Modules.pullback V.ι).obj M ≅ SheafOfModules.unit V.toScheme.ringCatSheaf))
    (U : X.affineOpens) :
    Module.Projective Γ(X, U.1) Γ(M, U.1)

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