Module

Scheme_Modules_FiniteBySections_of_isFinite.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_FiniteBySections_of_isFinite

36 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Finite By Sections of is Finite

Imports4

Imported by4

abbrev

rM

L52 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.rM

Documentation

Restriction of module sections along an inclusion of opens.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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

L56 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.rO

Documentation

Restriction of regular functions along an inclusion of opens.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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

L59 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.rM_rM

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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

L64 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.rO_rO

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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

L69 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.rM_self

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.rO_self

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.rM_smul

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.hat_eq

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.le_hat

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.hat_le

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.eApp

Documentation

The chosen trivialisation evaluated on a preimage open.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.eInv

Documentation

The inverse trivialisation evaluated on a preimage open.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.eInv_eApp

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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

L103 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.eApp_eInv

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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

L108 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.eApp_zero

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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

L110 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.eApp_injective

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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

L113 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.restrict_smul_eq

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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

L119 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.eApp_smul

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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

L130 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.unit_map_eq

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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

L134 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.eApp_res

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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

ψ

L153 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.ψ

Documentation

Coordinates of a module section under the chosen local trivialisation.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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

L157 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.ψinv

Documentation

A module section reconstructed from its local coordinate.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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

L160 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.rM_roundtrip

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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'

L163 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.rM_roundtrip'

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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

L167 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.rO_roundtrip

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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'

L171 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.rO_roundtrip'

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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

L175 ↗

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

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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_ψ

L179 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.ψinv_ψ

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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

L183 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.ψ_injective

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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

L186 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.ψ_zero

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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

L191 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.ψ_smul

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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

L200 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.LocTriv.ψ_res

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
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

eq_of_le_bot

L220 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.eq_of_le_bot

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Frames
open LocTriv
variable {X : Scheme.{u}} (M : X.Modules) (V : X.Opens)
  (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)

Lean source · statement

theorem eq_of_le_bot {W : X.Opens} (hW : W ≤ ⊥) (s t : Γ(M, W)) : s = t

theorem

frame_of_eq_unit_smul

L224 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.frame_of_eq_unit_smul

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Frames
open LocTriv
variable {X : Scheme.{u}} (M : X.Modules) (V : X.Opens)
  (e : M.restrict V.ι ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)

Lean source · full declaration

theorem frame_of_eq_unit_smul {W : X.Opens} (hWV : W ≤ V) (y : Γ(M, ⊤)) (c : Γ(X, W)) (hc : IsUnit
  c)
    (hy : rM M (le_top : W ≤ ⊤) y = c • ψinv M V e hWV 1) (V' : X.Opens) (hV' : V' ≤ W) :
    Function.Bijective fun a : Γ(X, V') => a • (M.presheaf.map (homOfLE (le_top : V' ≤ ⊤)).op y)
      := by
  have hcu : IsUnit (rO hV' c) := hc.map _
  have h1 : rM M hV' (ψinv M V e hWV 1) = ψinv M V e (hV'.trans hWV) 1 := by
    apply ψ_injective M V e (hV'.trans hWV)
    rw [ψ_res M V e hWV hV', ψ_ψinv, ψ_ψinv]
    exact map_one _
  have hres : M.presheaf.map (homOfLE (le_top : V' ≤ ⊤)).op y = rO hV' c • ψinv M V e (hV'.trans
    hWV) 1 := by
    change rM M le_top y = _
    rw [← rM_rM M (le_top : W ≤ ⊤) hV', hy, rM_smul, h1]
  have key : (fun a : Γ(X, V') => a • (M.presheaf.map (homOfLE (le_top : V' ≤ ⊤)).op y))
      = (ψinv M V e (hV'.trans hWV)) ∘ (fun a => a * rO hV' c) := by
    funext a
    simp only [Function.comp_apply]
    rw [hres, ← mul_smul]
    apply ψ_injective M V e (hV'.trans hWV)
    rw [ψ_smul, ψ_ψinv, ψ_ψinv, mul_one]
  rw [key]
  refine Function.Bijective.comp ?_ ?_
  · exact Function.bijective_iff_has_inverse.mpr ⟨ψ M V e _, ψ_ψinv M V e _, ψinv_ψ M V e _⟩
  · exact (Units.mulRight hcu.unit).bijective

theorem

main

L253 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite.AlgebraicGeometry.Scheme.Modules.FBSFinite.main

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSFinite
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open LocTriv in

Lean source · statement

theorem main {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) [IsFinite f]
    (M : X.Modules) (hM : Scheme.Modules.IsInvertible M) :
    Scheme.Modules.FiniteBySections M f

theorem

of_isFinite

L312 ↗

AlgebraicGeometry.Scheme.Modules.FiniteBySections.of_isFinite

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.FiniteBySections.of_isFinite {R : Type u}
  [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) [IsFinite f]
    (M : X.Modules) (hM : Scheme.Modules.IsInvertible M) :
    Scheme.Modules.FiniteBySections M f

Module documentation

Scheme Modules Finite By Sections of is Finite

Declarations