Module

Scheme_Modules_finite_sections_of_locallyTrivial.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_finite_sections_of_locallyTrivial

36 declarations indexed from sourceView source ↗

Module documentation

Finite section modules of locally trivial sheaves

Local trivializations on basic opens and a finite affine cover provide finite generation of module sections over an affine open.

Imports6

Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.RingTheory.Finiteness.Defs
Mathlib.RingTheory.Finiteness.Basic
Mathlib.RingTheory.Ideal.Span
Nyll.SchemeTheory.Modules.LocallyTrivialSectionsLocalization

Imported by10

def

LocProp

L49 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocProp

Documentation

The surjectivity and torsion conditions for restricting sections to a basic open.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry

Lean source · statement

def LocProp {X : Scheme.{u}} (M : X.Modules) (V : X.Opens) (g : Γ(X, V)) : Prop

abbrev

rM

L61 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.rM

Documentation

Restriction of module sections along an inclusion of opens.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

L65 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.rO

Documentation

Restriction of ring sections along an inclusion of opens.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

L68 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.rM_rM

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

L74 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.rO_rO

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

L79 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.rM_self

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

L84 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.rO_self

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

L88 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.rM_smul

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

L95 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.hat_eq

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

L98 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.le_hat

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

L99 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.hat_le

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

L102 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.eApp

Documentation

The section map induced by the chosen local trivialization.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

L106 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.eInv

Documentation

The inverse section map induced by the chosen local trivialization.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

L109 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.eInv_eApp

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

L120 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.eApp_eInv

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

L134 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.eApp_zero

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

L136 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.eApp_injective

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

L139 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.restrict_smul_eq

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

L145 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.eApp_smul

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

L157 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.unit_map_eq

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

L161 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.eApp_res

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

ψ

L179 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.ψ

Documentation

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

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

L183 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.ψinv

Documentation

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

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

L186 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.rM_roundtrip

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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'

L189 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.rM_roundtrip'

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

L193 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.rO_roundtrip

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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'

L197 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.rO_roundtrip'

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

L201 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.ψ_ψinv

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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_ψ

L205 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.ψinv_ψ

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

L209 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.ψ_injective

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

L212 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.ψ_zero

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

L217 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.ψ_smul

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

L226 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.ψ_res

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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

locProp

L236 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.LocTriv.locProp

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
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)
include V e in

Lean source · statement

theorem locProp {W : X.Opens} (hW : IsAffineOpen W) (hWV : W ≤ V) (g : Γ(X, W)) : LocProp M W g

theorem

finite_sections_of_locallyTrivial'

L265 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_sections_of_locallyTrivial.AlgebraicGeometry.Scheme.Modules.finite_sections_of_locallyTrivial'

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open LocTriv in

Lean source · statement

theorem finite_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.Finite Γ(X, U.1) Γ(M, U.1)

theorem

finite_sections_of_locallyTrivial

L365 ↗

AlgebraicGeometry.Scheme.Modules.finite_sections_of_locallyTrivial

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_finite_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.finite_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.Finite Γ(X, U.1) Γ(M, U.1)

Module documentation

Finite section modules of locally trivial sheaves

Declarations