NYLL
Module

Scheme_Modules_FiniteBySections_isFinite_of_unit.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_FiniteBySections_isFinite_of_unit
42 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Finite By Sections is Finite of unit

Imports1
Imported by2

Declarations

abbrev

resTop

L53 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.resTop
Documentation

Restriction of a global module section to an open subset.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Frames
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
abbrev resTop (s : Γ(M, ⊤)) (V : X.Opens) : Γ(M, V)
def

IsFrameOn

L57 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.IsFrameOn
Documentation

A global section gives unique scalar coordinates on the given open subset.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Frames
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
def IsFrameOn (s : Γ(M, ⊤)) (V : X.Opens) : Prop
theorem

resTop_map

L64 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.resTop_map
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Frames
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
Lean source · statement
theorem resTop_map {s : Γ(M, ⊤)} {V W : X.Opens} (h : W ≤ V) :
    M.presheaf.map (homOfLE h).op (resTop M s V) = resTop M s W
theorem

mono

L73 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.IsFrameOn.mono
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Frames
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
namespace IsFrameOn
variable {s t : Γ(M, ⊤)} {V W : X.Opens}
Lean source · statement
theorem mono (h : IsFrameOn M s V) (hWV : W ≤ V) : IsFrameOn M s W
theorem

bijective

L76 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.IsFrameOn.bijective
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Frames
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
namespace IsFrameOn
variable {s t : Γ(M, ⊤)} {V W : X.Opens}
Lean source · full declaration
theorem bijective (h : IsFrameOn M s V) :
    Function.Bijective fun g : Γ(X, V) => g • resTop M s V := h V le_rfl
theorem

injective

L79 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.IsFrameOn.injective
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Frames
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
namespace IsFrameOn
variable {s t : Γ(M, ⊤)} {V W : X.Opens}
Lean source · statement
theorem injective (h : IsFrameOn M s V) {g g' : Γ(X, V)}
    (hg : g • resTop M s V = g' • resTop M s V) : g = g'
theorem

isUnit_of_eq_smul

L83 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.IsFrameOn.isUnit_of_eq_smul
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Frames
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
namespace IsFrameOn
variable {s t : Γ(M, ⊤)} {V W : X.Opens}
Lean source · statement
theorem isUnit_of_eq_smul (hs : IsFrameOn M s V) (ht : IsFrameOn M t V) (g : Γ(X, V))
    (hg : resTop M t V = g • resTop M s V) : IsUnit g
def

algR

L103 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.algR
Documentation

The coefficient ring acting on sections through the structure morphism.

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Chart
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {N : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "ℙ" => Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)
Lean source · statement
def algR (V : X.Opens) : R →+* Γ(X, V)
theorem

map_algR

L106 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.map_algR
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Chart
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {N : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "ℙ" => Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)
Lean source · statement
theorem map_algR {V W : X.Opens} (ι : W ⟶ V) (r : R) :
    X.presheaf.map ι.op (algR f V r) = algR f W r
theorem

algR_top

L114 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.algR_top
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Chart
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {N : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "ℙ" => Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)
Lean source · statement
theorem algR_top (r : R) : algR f ⊤ r = f.appTop ((Scheme.ΓSpecIso (.of R)).inv r)
def

chartRing

L125 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.chartRing
Documentation

The ring of sections on the preimage of a standard projective chart.

Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Chart
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {N : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "ℙ" => Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)
section ChartDefs
variable (t : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)) (i : Fin (N + 1))
  (V : X.Opens) (hle : V ≤ t ⁻¹ᵁ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)
    (MvPolynomial.X i))
Lean source · statement
def chartRing (t : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)) (i : Fin (N + 1))
    (V : X.Opens) (hle : V ≤ t ⁻¹ᵁ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (N + 1))
      R) (MvPolynomial.X i)) : Away 𝒜 (MvPolynomial.X i : MvPolynomial (Fin (N + 1)) R) →+* Γ(X, V)
theorem

chartRing_apply

L132 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.chartRing_apply
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Chart
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {N : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "ℙ" => Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)
section ChartDefs
variable (t : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)) (i : Fin (N + 1))
  (V : X.Opens) (hle : V ≤ t ⁻¹ᵁ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)
    (MvPolynomial.X i))
Lean source · statement
theorem chartRing_apply (z : Away 𝒜 (MvPolynomial.X i : MvPolynomial (Fin (N + 1)) R)) :
    chartRing t i V hle z = t.appLE (Proj.basicOpen 𝒜 (MvPolynomial.X i)) V hle (Proj.awayToSection
      𝒜 (MvPolynomial.X i) z)
theorem

map_app_awayToSection

L136 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.map_app_awayToSection
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Chart
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {N : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "ℙ" => Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)
section ChartDefs
variable (t : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)) (i : Fin (N + 1))
  (V : X.Opens) (hle : V ≤ t ⁻¹ᵁ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)
    (MvPolynomial.X i))
Lean source · statement
theorem map_app_awayToSection (z : Away 𝒜 (MvPolynomial.X i : MvPolynomial (Fin (N + 1)) R)) :
    X.presheaf.map (homOfLE hle).op (t.app (Proj.basicOpen 𝒜 (MvPolynomial.X i))
      (Proj.awayToSection 𝒜 (MvPolynomial.X i) z))
      = chartRing t i V hle z
theorem

map_chartRing

L142 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.map_chartRing
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Chart
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {N : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "ℙ" => Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)
section ChartDefs
variable (t : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)) (i : Fin (N + 1))
  (V : X.Opens) (hle : V ≤ t ⁻¹ᵁ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)
    (MvPolynomial.X i))
Lean source · statement
theorem map_chartRing {W : X.Opens} (h : W ≤ V) (z : Away 𝒜 (MvPolynomial.X i : MvPolynomial (Fin
  (N + 1)) R)) :
    X.presheaf.map (homOfLE h).op (chartRing t i V hle z) = chartRing t i W (h.trans hle) z
theorem

fac

L148 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.fac
Source context 29 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Chart
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {N : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "ℙ" => Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)
section ChartDefs
variable (t : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)) (i : Fin (N + 1))
  (V : X.Opens) (hle : V ≤ t ⁻¹ᵁ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)
    (MvPolynomial.X i))
include hle in
Lean source · statement
theorem fac : V.ι ≫ t = V.toSpecΓ ≫ Spec.map (CommRingCat.ofHom (chartRing t i V hle)) ≫
    Proj.awayι 𝒜 (MvPolynomial.X i) (ProjSpace.X_mem_one R N i) one_pos
theorem

chartRing_comp_algebraMap

L161 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.chartRing_comp_algebraMap
Source context 29 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Chart
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {N : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "ℙ" => Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)
section ChartDefs
variable (t : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)) (i : Fin (N + 1))
  (V : X.Opens) (hle : V ≤ t ⁻¹ᵁ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)
    (MvPolynomial.X i))
include hle in
Lean source · statement
theorem chartRing_comp_algebraMap (hV : IsAffineOpen V) (ht : t ≫ ProjSpace.π R N = f) :
    (chartRing t i V hle).comp (algebraMap R _) = algR f V
theorem

chartRing_algebraMap

L178 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.chartRing_algebraMap
Source context 29 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Chart
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {N : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "ℙ" => Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)
section ChartDefs
variable (t : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)) (i : Fin (N + 1))
  (V : X.Opens) (hle : V ≤ t ⁻¹ᵁ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)
    (MvPolynomial.X i))
include hle in
Lean source · statement
theorem chartRing_algebraMap (hV : IsAffineOpen V) (ht : t ≫ ProjSpace.π R N = f) (r : R) :
    chartRing t i V hle (algebraMap R _ r) = algR f V r
theorem

isFrameOn

L194 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.isFrameOn
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Pres
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {M : X.Modules} {N : ℕ}
  (𝔓 : M.ProjPresentation f N) (i : Fin (N + 1)) (V : X.Opens)
  (hle : V ≤ 𝔓.toProj ⁻¹ᵁ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)
    (MvPolynomial.X i))
include hle in
Lean source · statement
theorem isFrameOn : IsFrameOn M (𝔓.σ i) V
theorem

chartRing_ratio_smul

L196 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.chartRing_ratio_smul
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Pres
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {M : X.Modules} {N : ℕ}
  (𝔓 : M.ProjPresentation f N) (i : Fin (N + 1)) (V : X.Opens)
  (hle : V ≤ 𝔓.toProj ⁻¹ᵁ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)
    (MvPolynomial.X i))
Lean source · statement
theorem chartRing_ratio_smul (l : Fin (N + 1)) :
    chartRing 𝔓.toProj i V hle (ProjSpace.ratio R N i l) • resTop M (𝔓.σ i) V = resTop M (𝔓.σ l) V
def

fn

L216 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.fn
Documentation

The regular functions given by the presenting sections of the unit module.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Unit
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {N : ℕ}
  (𝔓 : Scheme.Modules.ProjPresentation (SheafOfModules.unit X.ringCatSheaf : X.Modules) f N)
Lean source · statement
def fn (i : Fin (N + 1)) : Γ(X, ⊤)
def

U

L219 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.U
Documentation

The standard projective chart pulled back along the presentation morphism.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Unit
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {N : ℕ}
  (𝔓 : Scheme.Modules.ProjPresentation (SheafOfModules.unit X.ringCatSheaf : X.Modules) f N)
Lean source · statement
def U (i : Fin (N + 1)) : X.Opens
theorem

resTop_unit

L222 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.resTop_unit
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Unit
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {N : ℕ}
  (𝔓 : Scheme.Modules.ProjPresentation (SheafOfModules.unit X.ringCatSheaf : X.Modules) f N)
Lean source · full declaration
theorem resTop_unit (i : Fin (N + 1)) (V : X.Opens) :
    (show Γ(X, V) from resTop (SheafOfModules.unit X.ringCatSheaf : X.Modules) (𝔓.σ i) V)
      = X.presheaf.map (homOfLE (le_top : V ≤ ⊤)).op (fn 𝔓 i) := rfl
instance

unitProjFiniteSectionModule

L228 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.unitProjFiniteSectionModule
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Unit
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {N : ℕ}
  (𝔓 : Scheme.Modules.ProjPresentation (SheafOfModules.unit X.ringCatSheaf : X.Modules) f N)
section UnitScalar
Lean source · statement
instance unitProjFiniteSectionModule (V : X.Opens) :
    Module Γ(X, V) Γ((SheafOfModules.unit X.ringCatSheaf : X.Modules), V)
theorem

unit_smul

L232 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.unit_smul
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Unit
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {N : ℕ}
  (𝔓 : Scheme.Modules.ProjPresentation (SheafOfModules.unit X.ringCatSheaf : X.Modules) f N)
section UnitScalar
local instance unitProjFiniteSectionModule (V : X.Opens) :
    Module Γ(X, V) Γ((SheafOfModules.unit X.ringCatSheaf : X.Modules), V) :=
  ((SheafOfModules.unit X.ringCatSheaf : X.Modules).val.obj (op V)).isModule
Lean source · full declaration
theorem unit_smul (V : X.Opens) (a : Γ(X, V)) (m : Γ((SheafOfModules.unit X.ringCatSheaf :
  X.Modules), V)) :
    (show Γ(X, V) from (a • m)) = a * (show Γ(X, V) from m) := rfl
theorem

isUnit_res

L238 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.isUnit_res
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Unit
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {N : ℕ}
  (𝔓 : Scheme.Modules.ProjPresentation (SheafOfModules.unit X.ringCatSheaf : X.Modules) f N)
Lean source · statement
theorem isUnit_res (i : Fin (N + 1)) : IsUnit (X.presheaf.map (homOfLE (le_top : U 𝔓 i ≤ ⊤)).op (fn
  𝔓 i))
theorem

U_le_basicOpen

L245 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.U_le_basicOpen
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Unit
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {N : ℕ}
  (𝔓 : Scheme.Modules.ProjPresentation (SheafOfModules.unit X.ringCatSheaf : X.Modules) f N)
Lean source · statement
theorem U_le_basicOpen (i : Fin (N + 1)) : U 𝔓 i ≤ X.basicOpen (fn 𝔓 i)
theorem

iSup_U

L250 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.iSup_U
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Unit
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {N : ℕ}
  (𝔓 : Scheme.Modules.ProjPresentation (SheafOfModules.unit X.ringCatSheaf : X.Modules) f N)
Lean source · statement
theorem iSup_U : (⨆ i, U 𝔓 i) = ⊤
theorem

isLocalizationElem_eq

L261 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.isLocalizationElem_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_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Unit
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {N : ℕ}
  (𝔓 : Scheme.Modules.ProjPresentation (SheafOfModules.unit X.ringCatSheaf : X.Modules) f N)
Lean source · statement
theorem isLocalizationElem_eq (j i : Fin (N + 1)) :
    HomogeneousLocalization.Away.isLocalizationElem (𝒜 := MvPolynomial.homogeneousSubmodule (Fin (N
      + 1)) R)
      (ProjSpace.X_mem_one R N j) (ProjSpace.X_mem_one R N i) = ProjSpace.ratio R N j i
theorem

ι_preimage_U

L268 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.ι_preimage_U
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Unit
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {N : ℕ}
  (𝔓 : Scheme.Modules.ProjPresentation (SheafOfModules.unit X.ringCatSheaf : X.Modules) f N)
Lean source · statement
theorem ι_preimage_U (j i : Fin (N + 1)) :
    (U 𝔓 j).ι ⁻¹ᵁ U 𝔓 i = (U 𝔓 j).ι ⁻¹ᵁ X.basicOpen (chartRing 𝔓.toProj j (U 𝔓 j) le_rfl
      (ProjSpace.ratio R N j i))
theorem

mem_U_of_mem

L281 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.mem_U_of_mem
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Unit
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {N : ℕ}
  (𝔓 : Scheme.Modules.ProjPresentation (SheafOfModules.unit X.ringCatSheaf : X.Modules) f N)
Lean source · statement
theorem mem_U_of_mem (j i : Fin (N + 1)) (x : X) (hxj : x ∈ U 𝔓 j)
    (hx : x ∈ X.basicOpen (chartRing 𝔓.toProj j (U 𝔓 j) le_rfl (ProjSpace.ratio R N j i))) : x ∈ U
      𝔓 i
theorem

basicOpen_eq_U

L290 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.basicOpen_eq_U
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Unit
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {N : ℕ}
  (𝔓 : Scheme.Modules.ProjPresentation (SheafOfModules.unit X.ringCatSheaf : X.Modules) f N)
Lean source · statement
theorem basicOpen_eq_U (i : Fin (N + 1)) : X.basicOpen (fn 𝔓 i) = U 𝔓 i
theorem

isAffineOpen_U

L307 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.isAffineOpen_U
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Unit
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {N : ℕ}
  (𝔓 : Scheme.Modules.ProjPresentation (SheafOfModules.unit X.ringCatSheaf : X.Modules) f N)
Lean source · statement
theorem isAffineOpen_U [IsAffineHom 𝔓.toProj] (i : Fin (N + 1)) : IsAffineOpen (U 𝔓 i)
def

θ

L319 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.θ
Documentation

Evaluation of polynomial coordinates at the presenting regular functions.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Affine
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {N : ℕ}
  (𝔓 : Scheme.Modules.ProjPresentation (SheafOfModules.unit X.ringCatSheaf : X.Modules) f N)
Lean source · statement
def θ : MvPolynomial (Fin (N + 1)) R →+* Γ(X, ⊤)
theorem

θ_X

L322 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.θ_X
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Affine
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {N : ℕ}
  (𝔓 : Scheme.Modules.ProjPresentation (SheafOfModules.unit X.ringCatSheaf : X.Modules) f N)
Lean source · statement
theorem θ_X (i : Fin (N + 1)) : θ 𝔓 (MvPolynomial.X i) = fn 𝔓 i
theorem

θ_comp_C

L324 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.θ_comp_C
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Affine
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {N : ℕ}
  (𝔓 : Scheme.Modules.ProjPresentation (SheafOfModules.unit X.ringCatSheaf : X.Modules) f N)
Lean source · statement
theorem θ_comp_C : (θ 𝔓).comp MvPolynomial.C = ((Scheme.ΓSpecIso (.of R)).inv ≫ f.appTop).hom
def

ψ

L328 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.ψ
Documentation

The affine morphism induced by the presenting regular functions.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Affine
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {N : ℕ}
  (𝔓 : Scheme.Modules.ProjPresentation (SheafOfModules.unit X.ringCatSheaf : X.Modules) f N)
Lean source · statement
def ψ : X ⟶ Spec (.of (MvPolynomial (Fin (N + 1)) R))
theorem

ψ_comp

L331 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.ψ_comp
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Affine
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {N : ℕ}
  (𝔓 : Scheme.Modules.ProjPresentation (SheafOfModules.unit X.ringCatSheaf : X.Modules) f N)
Lean source · statement
theorem ψ_comp : ψ 𝔓 ≫ Spec.map (CommRingCat.ofHom (MvPolynomial.C : R →+* MvPolynomial (Fin (N +
  1)) R)) = f
theorem

ψ_preimage_basicOpen

L337 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.ψ_preimage_basicOpen
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Affine
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {N : ℕ}
  (𝔓 : Scheme.Modules.ProjPresentation (SheafOfModules.unit X.ringCatSheaf : X.Modules) f N)
Lean source · statement
theorem ψ_preimage_basicOpen (b : MvPolynomial (Fin (N + 1)) R) :
    ψ 𝔓 ⁻¹ᵁ PrimeSpectrum.basicOpen b = X.basicOpen (θ 𝔓 b)
theorem

mem_basicOpen_iff

L343 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.mem_basicOpen_iff
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Affine
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {N : ℕ}
  (𝔓 : Scheme.Modules.ProjPresentation (SheafOfModules.unit X.ringCatSheaf : X.Modules) f N)
Lean source · statement
theorem mem_basicOpen_iff (x : X) (b : MvPolynomial (Fin (N + 1)) R) :
    b ∉ (ψ 𝔓 x).asIdeal ↔ x ∈ X.basicOpen (θ 𝔓 b)
theorem

span_eq_top

L349 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.span_eq_top
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Affine
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {N : ℕ}
  (𝔓 : Scheme.Modules.ProjPresentation (SheafOfModules.unit X.ringCatSheaf : X.Modules) f N)
include 𝔓 in
Lean source · statement
theorem span_eq_top [IsFinite 𝔓.toProj] : Ideal.span (Set.range (fn 𝔓)) = ⊤
theorem

isFinite

L396 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit.AlgebraicGeometry.Scheme.Modules.FBSUnit.isFinite
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FBSUnit
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
section Affine
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {N : ℕ}
  (𝔓 : Scheme.Modules.ProjPresentation (SheafOfModules.unit X.ringCatSheaf : X.Modules) f N)
include 𝔓 in
Lean source · statement
theorem isFinite [IsFinite 𝔓.toProj] : IsFinite f
theorem

isFinite_of_unit

L410 ↗
AlgebraicGeometry.Scheme.Modules.FiniteBySections.isFinite_of_unit
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_isFinite_of_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.FiniteBySections.isFinite_of_unit
    {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R))
    (h𝒪 : Scheme.Modules.FiniteBySections (SheafOfModules.unit X.ringCatSheaf : X.Modules) f) :
    IsFinite f

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