NYLL
Module

Scheme_Modules_FiniteBySections_tensor.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_FiniteBySections_tensor
37 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Finite By Sections tensor

Imports6
Imported by2

Declarations

theorem

map_homOfLE_refl

L47 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.map_homOfLE_refl
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section Frame
variable {X : Scheme.{u}} {M : X.Modules} {W : X.Opens}
Lean source · statement
theorem map_homOfLE_refl (s : Γ(M, W)) : M.presheaf.map (homOfLE (le_refl W)).op s = s
theorem

smul_left_injective_of_isFrameOn

L52 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.smul_left_injective_of_isFrameOn
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section Frame
variable {X : Scheme.{u}} {M : X.Modules} {W : X.Opens}
Lean source · full declaration
theorem smul_left_injective_of_isFrameOn {s : Γ(M, W)} (hs : Scheme.Modules.IsFrameOn s W) :
    Function.Injective fun g : Γ(X, W) => g • s := by
  have h := (hs (le_refl W) (le_refl W)).1
  simpa only [map_homOfLE_refl] using h
theorem

smul_left_surjective_of_isFrameOn

L57 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.smul_left_surjective_of_isFrameOn
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section Frame
variable {X : Scheme.{u}} {M : X.Modules} {W : X.Opens}
Lean source · full declaration
theorem smul_left_surjective_of_isFrameOn {s : Γ(M, W)} (hs : Scheme.Modules.IsFrameOn s W) :
    Function.Surjective fun g : Γ(X, W) => g • s := by
  have h := (hs (le_refl W) (le_refl W)).2
  simpa only [map_homOfLE_refl] using h
theorem

isUnit_of_smul_frame_eq_frame

L62 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.isUnit_of_smul_frame_eq_frame
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section Frame
variable {X : Scheme.{u}} {M : X.Modules} {W : X.Opens}
Lean source · statement
theorem isUnit_of_smul_frame_eq_frame {s t : Γ(M, W)} (hs : Scheme.Modules.IsFrameOn s W)
    (ht : Scheme.Modules.IsFrameOn t W) {c : Γ(X, W)} (hc : c • s = t) : IsUnit c
theorem

isFrameOn_map

L70 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.isFrameOn_map
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section Frame
variable {X : Scheme.{u}} {M : X.Modules} {W : X.Opens}
Lean source · statement
theorem isFrameOn_map {U V : X.Opens} {s : Γ(M, U)} (hs : Scheme.Modules.IsFrameOn s V)
    (hWU : W ≤ U) (hWV : W ≤ V) :
    Scheme.Modules.IsFrameOn (M.presheaf.map (homOfLE hWU).op s) W
abbrev

PP

L83 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.PP
Documentation

Projective space over the coefficient ring.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section OnePresentation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
  {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
Lean source · statement
abbrev PP (R : Type u) [CommRing R] (N : ℕ) : Scheme.{u}
abbrev

DD

L87 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.DD
Documentation

The standard affine chart of projective space.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section OnePresentation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
  {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
Lean source · statement
abbrev DD (R : Type u) [CommRing R] (N : ℕ) (i : Fin (N + 1)) : (PP R N).Opens
abbrev

chart

L91 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.chart
Documentation

The preimage of a standard chart under the chosen projective presentation.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section OnePresentation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
  {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
Lean source · statement
abbrev chart (i : Fin (N + 1)) : X.Opens
theorem

iSup_DD

L93 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.iSup_DD
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section OnePresentation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
  {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
Lean source · statement
theorem iSup_DD : ⨆ i, DD R N i = ⊤
theorem

iSup_chart

L96 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.iSup_chart
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section OnePresentation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
  {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
Lean source · statement
theorem iSup_chart : ⨆ i, chart 𝔓 i = ⊤
theorem

exists_mem_chart

L100 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.exists_mem_chart
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section OnePresentation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
  {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
Lean source · statement
theorem exists_mem_chart (x : X) : ∃ i, x ∈ chart 𝔓 i
theorem

isFrameOn_σ

L104 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.isFrameOn_σ
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section OnePresentation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
  {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
Lean source · statement
theorem isFrameOn_σ (i : Fin (N + 1)) : Scheme.Modules.IsFrameOn (𝔓.σ i) (chart 𝔓 i)
def

rfun

L108 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.rfun
Documentation

The pullback of a homogeneous coordinate ratio to a presentation chart.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section OnePresentation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
  {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
Lean source · statement
def rfun (i j : Fin (N + 1)) : Γ(X, chart 𝔓 i)
theorem

rfun_smul

L111 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.rfun_smul
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section OnePresentation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
  {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
Lean source · statement
theorem rfun_smul (i j : Fin (N + 1)) :
    rfun 𝔓 i j • M.presheaf.map (homOfLE (le_top : chart 𝔓 i ≤ ⊤)).op (𝔓.σ i) =
      M.presheaf.map (homOfLE (le_top : chart 𝔓 i ≤ ⊤)).op (𝔓.σ j)
theorem

mem_DD_of_isUnit_germ

L122 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.mem_DD_of_isUnit_germ
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section ProjRatio
variable (R : Type u) [CommRing R] (N : ℕ)
Lean source · statement
theorem mem_DD_of_isUnit_germ (i j : Fin (N + 1)) (p : PP R N) (hp : p ∈ DD R N i)
    (hu : IsUnit ((PP R N).presheaf.germ (DD R N i) p hp
      (Proj.awayToSection _ (MvPolynomial.X i) (ProjSpace.ratio R N i j)))) :
    p ∈ DD R N j
theorem

mem_chart_of_isUnit_rfun

L159 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.mem_chart_of_isUnit_rfun
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section OnePresentation2
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
  {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
Lean source · statement
theorem mem_chart_of_isUnit_rfun {i j : Fin (N + 1)} {O : X.Opens} (hO : O ≤ chart 𝔓 i) {x : X}
    (hx : x ∈ O) (hu : IsUnit (X.presheaf.map (homOfLE hO).op (rfun 𝔓 i j))) : x ∈ chart 𝔓 j
theorem

modMap_map

L180 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.modMap_map
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section Restrict
variable {X : Scheme.{u}} {M : X.Modules} {U V W : X.Opens}
Lean source · statement
theorem modMap_map (h₁ : V ≤ U) (h₂ : W ≤ V) (s : Γ(M, U)) :
    M.presheaf.map (homOfLE h₂).op (M.presheaf.map (homOfLE h₁).op s) =
      M.presheaf.map (homOfLE (h₂.trans h₁)).op s
theorem

ringMap_map

L186 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.ringMap_map
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section Restrict
variable {X : Scheme.{u}} {M : X.Modules} {U V W : X.Opens}
Lean source · statement
theorem ringMap_map (h₁ : V ≤ U) (h₂ : W ≤ V) (g : Γ(X, U)) :
    X.presheaf.map (homOfLE h₂).op (X.presheaf.map (homOfLE h₁).op g) =
      X.presheaf.map (homOfLE (h₂.trans h₁)).op g
theorem

restrict_smul_eq

L192 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.restrict_smul_eq
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section Restrict
variable {X : Scheme.{u}} {M : X.Modules} {U V W : X.Opens}
Lean source · statement
theorem restrict_smul_eq (h₁ : V ≤ U) (h₂ : W ≤ V) {g : Γ(X, V)} {s t : Γ(M, U)}
    (h : g • M.presheaf.map (homOfLE h₁).op s = M.presheaf.map (homOfLE h₁).op t) :
    X.presheaf.map (homOfLE h₂).op g • M.presheaf.map (homOfLE (h₂.trans h₁)).op s =
      M.presheaf.map (homOfLE (h₂.trans h₁)).op t
abbrev

KK

L208 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.KK
Documentation

The dimension of the projective space used for the Segre presentation.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section Two
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
  {L M : X.Modules} {N N' : ℕ} (𝔓 : L.ProjPresentation f N) (𝔔 : M.ProjPresentation f N')
Lean source · statement
abbrev KK (N N' : ℕ) : ℕ
theorem

KK_succ

L210 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.KK_succ
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section Two
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
  {L M : X.Modules} {N N' : ℕ} (𝔓 : L.ProjPresentation f N) (𝔔 : M.ProjPresentation f N')
Lean source · statement
theorem KK_succ (N N' : ℕ) : (N + 1) * (N' + 1) = KK N N' + 1
def

idx

L214 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.idx
Documentation

The correspondence between Segre coordinates and pairs of original coordinates.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section Two
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
  {L M : X.Modules} {N N' : ℕ} (𝔓 : L.ProjPresentation f N) (𝔔 : M.ProjPresentation f N')
Lean source · statement
def idx (N N' : ℕ) : Fin (KK N N' + 1) ≃ Fin (N + 1) × Fin (N' + 1)
def

ρ

L218 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.ρ
Documentation

The tensor products of the two families of presenting sections.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section Two
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
  {L M : X.Modules} {N N' : ℕ} (𝔓 : L.ProjPresentation f N) (𝔔 : M.ProjPresentation f N')
Lean source · statement
def ρ (k : Fin (KK N N' + 1)) : Γ(L ⊗ M, ⊤)
abbrev

WW

L222 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.WW
Documentation

The intersection of the two presentation charts indexed by a Segre coordinate.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section Two
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
  {L M : X.Modules} {N N' : ℕ} (𝔓 : L.ProjPresentation f N) (𝔔 : M.ProjPresentation f N')
Lean source · statement
abbrev WW (k : Fin (KK N N' + 1)) : X.Opens
theorem

iSup_WW

L224 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.iSup_WW
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section Two
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
  {L M : X.Modules} {N N' : ℕ} (𝔓 : L.ProjPresentation f N) (𝔔 : M.ProjPresentation f N')
Lean source · statement
theorem iSup_WW : ⨆ k, WW 𝔓 𝔔 k = ⊤
theorem

exists_mem_WW

L234 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.exists_mem_WW
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section Two
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
  {L M : X.Modules} {N N' : ℕ} (𝔓 : L.ProjPresentation f N) (𝔔 : M.ProjPresentation f N')
Lean source · statement
theorem exists_mem_WW (x : X) : ∃ k, x ∈ WW 𝔓 𝔔 k
theorem

isFrameOn_ρ

L238 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.isFrameOn_ρ
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section Two
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
  {L M : X.Modules} {N N' : ℕ} (𝔓 : L.ProjPresentation f N) (𝔔 : M.ProjPresentation f N')
Lean source · statement
theorem isFrameOn_ρ (k : Fin (KK N N' + 1)) : Scheme.Modules.IsFrameOn (ρ 𝔓 𝔔 k) (WW 𝔓 𝔔 k)
theorem

exists_segre

L242 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.exists_segre
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section Two
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
  {L M : X.Modules} {N N' : ℕ} (𝔓 : L.ProjPresentation f N) (𝔔 : M.ProjPresentation f N')
Lean source · statement
theorem exists_segre :
    ∃ 𝔖 : (L ⊗ M).ProjPresentation f (KK N N'), 𝔖.σ = ρ 𝔓 𝔔 ∧ ∀ k, WW 𝔓 𝔔 k ≤ chart 𝔖 k
theorem

map_ρ

L247 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.map_ρ
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section Two
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
  {L M : X.Modules} {N N' : ℕ} (𝔓 : L.ProjPresentation f N) (𝔔 : M.ProjPresentation f N')
Lean source · statement
theorem map_ρ (k : Fin (KK N N' + 1)) (O : X.Opens) :
    (L ⊗ M).presheaf.map (homOfLE (le_top : O ≤ ⊤)).op (ρ 𝔓 𝔔 k) =
      Scheme.Modules.tensorSections (L.presheaf.map (homOfLE (le_top : O ≤ ⊤)).op (𝔓.σ (idx N N'
        k).1))
        (M.presheaf.map (homOfLE (le_top : O ≤ ⊤)).op (𝔔.σ (idx N N' k).2))
theorem

chart_segre_le

L256 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.chart_segre_le
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section Two
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
  {L M : X.Modules} {N N' : ℕ} (𝔓 : L.ProjPresentation f N) (𝔔 : M.ProjPresentation f N')
variable {𝔓 𝔔}
Lean source · statement
theorem chart_segre_le (𝔖 : (L ⊗ M).ProjPresentation f (KK N N')) (hσ : 𝔖.σ = ρ 𝔓 𝔔)
    (hW : ∀ k, WW 𝔓 𝔔 k ≤ chart 𝔖 k) (k : Fin (KK N N' + 1)) : chart 𝔖 k ≤ WW 𝔓 𝔔 k
theorem

isSeparated_of_isFinite

L312 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.isSeparated_of_isFinite
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section Two
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
  {L M : X.Modules} {N N' : ℕ} (𝔓 : L.ProjPresentation f N) (𝔔 : M.ProjPresentation f N')
variable {𝔓 𝔔}
variable (𝔓 𝔔)
Lean source · statement
theorem isSeparated_of_isFinite (hφ : IsFinite 𝔓.toProj) : IsSeparated f
theorem

isProper_of_isFinite

L316 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.isProper_of_isFinite
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section Two
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
  {L M : X.Modules} {N N' : ℕ} (𝔓 : L.ProjPresentation f N) (𝔔 : M.ProjPresentation f N')
variable {𝔓 𝔔}
variable (𝔓 𝔔)
Lean source · statement
theorem isProper_of_isFinite (hφ : IsFinite 𝔓.toProj) : IsProper f
theorem

isAffineOpen_inf

L320 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.isAffineOpen_inf
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section Two
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
  {L M : X.Modules} {N N' : ℕ} (𝔓 : L.ProjPresentation f N) (𝔔 : M.ProjPresentation f N')
variable {𝔓 𝔔}
variable (𝔓 𝔔)
Lean source · statement
theorem isAffineOpen_inf (hφ : IsFinite 𝔓.toProj) {U V : X.Opens} (hU : IsAffineOpen U) (hV :
  IsAffineOpen V) :
    IsAffineOpen (U ⊓ V)
theorem

isAffineOpen_DD

L327 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.isAffineOpen_DD
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section Two
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
  {L M : X.Modules} {N N' : ℕ} (𝔓 : L.ProjPresentation f N) (𝔔 : M.ProjPresentation f N')
variable {𝔓 𝔔}
variable (𝔓 𝔔)
Lean source · statement
theorem isAffineOpen_DD (R : Type u) [CommRing R] (N : ℕ) (i : Fin (N + 1)) : IsAffineOpen (DD R N
  i)
theorem

isAffineOpen_chart

L331 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.isAffineOpen_chart
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section Two
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
  {L M : X.Modules} {N N' : ℕ} (𝔓 : L.ProjPresentation f N) (𝔔 : M.ProjPresentation f N')
variable {𝔓 𝔔}
variable (𝔓 𝔔)
Lean source · statement
theorem isAffineOpen_chart (hφ : IsFinite 𝔓.toProj) (i : Fin (N + 1)) : IsAffineOpen (chart 𝔓 i)
theorem

finiteBySections_tensor

L334 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor.P2mSegre.finiteBySections_tensor
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
noncomputable section
namespace P2mSegre
section Two
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
  {L M : X.Modules} {N N' : ℕ} (𝔓 : L.ProjPresentation f N) (𝔔 : M.ProjPresentation f N')
variable {𝔓 𝔔}
variable (𝔓 𝔔)
Lean source · statement
theorem finiteBySections_tensor (hφ : IsFinite 𝔓.toProj) (hψ : IsFinite 𝔔.toProj) :
    (L ⊗ M).FiniteBySections f
theorem

tensor

L362 ↗
AlgebraicGeometry.Scheme.Modules.FiniteBySections.tensor
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensor
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.FiniteBySections.tensor
    {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)}
    {L M : X.Modules} (hL : L.FiniteBySections f) (hM : M.FiniteBySections f) :
    (L ⊗ M).FiniteBySections f

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