Module

ProjectivePresentationFromFrames.lean

Nyll.SchemeTheory.Modules.ProjectivePresentationFromFrames

85 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules exists proj Presentation of i Sup eq top

Imports6

Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Mathlib.RingTheory.MvPolynomial.Homogeneous
Mathlib.Tactic.CategoryTheory.Reassoc
Mathlib.Tactic.Ring.RingNF
Nyll.SchemeTheory.Modules.ProjectivePresentation

Imported by9

abbrev

resTop

L50 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.resTop

Documentation

Restriction of a global module section to the specified open.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
variable {X : Scheme.{u}} (M : X.Modules)

Lean source · statement

abbrev resTop (s : Γ(M, ⊤)) (V : X.Opens) : Γ(M, V)

def

IsFrameOn

L54 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn

Documentation

The condition that a global section generates every section on each smaller open uniquely.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
variable {X : Scheme.{u}} (M : X.Modules)

Lean source · statement

def IsFrameOn (s : Γ(M, ⊤)) (V : X.Opens) : Prop

theorem

resTop_map'

L61 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.resTop_map'

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}

Lean source · statement

theorem resTop_map' {s : Γ(M, ⊤)} {V W : X.Opens} (ι : W ⟶ V) :
    M.presheaf.map ι.op (resTop M s V) = resTop M s W

theorem

resTop_map

L66 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.resTop_map

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
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

resTop_top

L71 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.resTop_top

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}

Lean source · statement

theorem resTop_top (s : Γ(M, ⊤)) : resTop M s ⊤ = s

theorem

mono

L81 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.mono

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
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

L84 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.bijective

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
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

L87 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.injective

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
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'

def

coef

L92 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.coef

Documentation

The scalar coordinate of a section with respect to the chosen frame.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
namespace IsFrameOn
variable {s t : Γ(M, ⊤)} {V W : X.Opens}

Lean source · statement

def coef (h : IsFrameOn M s V) (m : Γ(M, V)) : Γ(X, V)

theorem

coef_smul

L95 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.coef_smul

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
namespace IsFrameOn
variable {s t : Γ(M, ⊤)} {V W : X.Opens}

Lean source · statement

theorem coef_smul (h : IsFrameOn M s V) (m : Γ(M, V)) : h.coef m • resTop M s V = m

theorem

coef_eq_iff

L98 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.coef_eq_iff

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
namespace IsFrameOn
variable {s t : Γ(M, ⊤)} {V W : X.Opens}

Lean source · statement

theorem coef_eq_iff (h : IsFrameOn M s V) (m : Γ(M, V)) (g : Γ(X, V)) :
    h.coef m = g ↔ g • resTop M s V = m

theorem

coef_smul_resTop

L104 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.coef_smul_resTop

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
namespace IsFrameOn
variable {s t : Γ(M, ⊤)} {V W : X.Opens}

Lean source · statement

theorem coef_smul_resTop (h : IsFrameOn M s V) (g : Γ(X, V)) : h.coef (g • resTop M s V) = g

theorem

coef_resTop

L107 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.coef_resTop

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
namespace IsFrameOn
variable {s t : Γ(M, ⊤)} {V W : X.Opens}

Lean source · statement

theorem coef_resTop (h : IsFrameOn M s V) : h.coef (resTop M s V) = 1

theorem

map_coef'

L110 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.map_coef'

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
namespace IsFrameOn
variable {s t : Γ(M, ⊤)} {V W : X.Opens}

Lean source · statement

theorem map_coef' (h : IsFrameOn M s V) (ι : W ⟶ V) (m : Γ(M, V)) :
    X.presheaf.map ι.op (h.coef m) = (h.mono ι.le).coef (M.presheaf.map ι.op m)

theorem

map_coef

L115 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.map_coef

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
namespace IsFrameOn
variable {s t : Γ(M, ⊤)} {V W : X.Opens}

Lean source · statement

theorem map_coef (h : IsFrameOn M s V) (hWV : W ≤ V) (m : Γ(M, V)) :
    X.presheaf.map (homOfLE hWV).op (h.coef m) = (h.mono hWV).coef (M.presheaf.map (homOfLE
      hWV).op m)

theorem

coef_add

L120 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.coef_add

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
namespace IsFrameOn
variable {s t : Γ(M, ⊤)} {V W : X.Opens}

Lean source · statement

theorem coef_add (h : IsFrameOn M s V) (m m' : Γ(M, V)) : h.coef (m + m') = h.coef m + h.coef m'

theorem

coef_smul'

L124 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.coef_smul'

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
namespace IsFrameOn
variable {s t : Γ(M, ⊤)} {V W : X.Opens}

Lean source · statement

theorem coef_smul' (h : IsFrameOn M s V) (g : Γ(X, V)) (m : Γ(M, V)) : h.coef (g • m) = g * h.coef
  m

theorem

of_eq_unit_smul

L128 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.of_eq_unit_smul

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
namespace IsFrameOn
variable {s t : Γ(M, ⊤)} {V W : X.Opens}

Lean source · statement

theorem of_eq_unit_smul (hs : IsFrameOn M s V) (u : Γ(X, V)) (hu : IsUnit u)
    (ht : resTop M t V = u • resTop M s V) : IsFrameOn M t V

theorem

isUnit_of_eq_smul

L150 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.isUnit_of_eq_smul

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
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

theorem

of_forall_exists

L158 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.of_forall_exists

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
namespace IsFrameOn
variable {s t : Γ(M, ⊤)} {V W : X.Opens}

Lean source · statement

theorem of_forall_exists (V : X.Opens)
    (H : ∀ x ∈ V, ∃ W : X.Opens, W ≤ V ∧ x ∈ W ∧ IsFrameOn M s W) : IsFrameOn M s V

def

maxOpen

L195 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.maxOpen

Documentation

The largest open on which the global section is a frame.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
namespace IsFrameOn
variable {s t : Γ(M, ⊤)} {V W : X.Opens}

Lean source · statement

def maxOpen (M : X.Modules) (s : Γ(M, ⊤)) : X.Opens

theorem

le_maxOpen

L197 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.le_maxOpen

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
namespace IsFrameOn
variable {s t : Γ(M, ⊤)} {V W : X.Opens}

Lean source · statement

theorem le_maxOpen (h : IsFrameOn M s V) : V ≤ maxOpen M s

theorem

maxOpen_isFrameOn

L199 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.maxOpen_isFrameOn

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
namespace IsFrameOn
variable {s t : Γ(M, ⊤)} {V W : X.Opens}

Lean source · statement

theorem maxOpen_isFrameOn (s : Γ(M, ⊤)) : IsFrameOn M s (maxOpen M s)

def

algR

L240 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.algR

Documentation

The base-ring map to sections on an open induced by the structural morphism.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))

Lean source · statement

def algR (V : X.Opens) : R →+* Γ(X, V)

theorem

map_comp_algR

L243 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.map_comp_algR

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))

Lean source · statement

theorem map_comp_algR {V W : X.Opens} (ι : W ⟶ V) :
    (X.presheaf.map ι.op).hom.comp (algR f V) = algR f W

theorem

map_algR

L251 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.map_algR

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))

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

abbrev

trans

L262 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.trans

Documentation

The transition coefficient of a global section with respect to the chosen frame.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V W : X.Opens}

Lean source · statement

abbrev trans (hi : IsFrameOn M (σ i) V) (k : Fin (N + 1)) : Γ(X, V)

theorem

trans_smul

L264 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.trans_smul

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V W : X.Opens}

Lean source · statement

theorem trans_smul (hi : IsFrameOn M (σ i) V) (k : Fin (N + 1)) :
    hi.trans k • resTop M (σ i) V = resTop M (σ k) V

theorem

trans_self

L267 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.trans_self

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V W : X.Opens}

Lean source · statement

theorem trans_self (hi : IsFrameOn M (σ i) V) : hi.trans i = 1

theorem

map_trans

L269 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.map_trans

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V W : X.Opens}

Lean source · statement

theorem map_trans (hi : IsFrameOn M (σ i) V) (ι : W ⟶ V) (k : Fin (N + 1)) :
    X.presheaf.map ι.op (hi.trans k) = (hi.mono ι.le).trans k

theorem

trans_mul_trans

L273 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.trans_mul_trans

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V W : X.Opens}

Lean source · statement

theorem trans_mul_trans (hi : IsFrameOn M (σ i) V) (hj : IsFrameOn M (σ j) V) (k : Fin (N + 1)) :
    hi.trans k * hj.trans i = hj.trans k

theorem

trans_mul_trans_self

L278 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.trans_mul_trans_self

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V W : X.Opens}

Lean source · statement

theorem trans_mul_trans_self (hi : IsFrameOn M (σ i) V) (hj : IsFrameOn M (σ j) V) :
    hi.trans j * hj.trans i = 1

theorem

isUnit_trans

L282 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.isUnit_trans

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V W : X.Opens}

Lean source · statement

theorem isUnit_trans (hi : IsFrameOn M (σ i) V) (hj : IsFrameOn M (σ j) V) : IsUnit (hi.trans j)

def

evalHom

L286 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.evalHom

Documentation

Polynomial evaluation in the frame transition coefficients.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V W : X.Opens}

Lean source · statement

def evalHom (hi : IsFrameOn M (σ i) V) : MvPolynomial (Fin (N + 1)) R →+* Γ(X, V)

theorem

evalHom_X

L289 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.evalHom_X

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V W : X.Opens}

Lean source · statement

theorem evalHom_X (hi : IsFrameOn M (σ i) V) (k : Fin (N + 1)) :
    evalHom f hi (MvPolynomial.X k) = hi.trans k

theorem

evalHom_C

L293 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.evalHom_C

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V W : X.Opens}

Lean source · statement

theorem evalHom_C (hi : IsFrameOn M (σ i) V) (r : R) :
    evalHom f hi (MvPolynomial.C r) = algR f V r

theorem

evalHom_X_self

L297 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.evalHom_X_self

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V W : X.Opens}

Lean source · statement

theorem evalHom_X_self (hi : IsFrameOn M (σ i) V) : evalHom f hi (MvPolynomial.X i) = 1

theorem

isUnit_evalHom_X_self

L300 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.isUnit_evalHom_X_self

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V W : X.Opens}

Lean source · statement

theorem isUnit_evalHom_X_self (hi : IsFrameOn M (σ i) V) : IsUnit (evalHom f hi (MvPolynomial.X
  i))

theorem

map_comp_evalHom

L304 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.map_comp_evalHom

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V W : X.Opens}

Lean source · statement

theorem map_comp_evalHom (hi : IsFrameOn M (σ i) V) (ι : W ⟶ V) :
    (X.presheaf.map ι.op).hom.comp (evalHom f hi) = evalHom f (hi.mono ι.le)

def

chartHom

L315 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.chartHom

Documentation

The homomorphism on a standard projective chart supplied by its frame.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V W : X.Opens}

Lean source · statement

def chartHom (hi : IsFrameOn M (σ i) V) :
    Away (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R) (MvPolynomial.X i : MvPolynomial (Fin
      (N + 1)) R)
      →+* Γ(X, V)

theorem

chartHom_mk

L325 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.chartHom_mk

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V W : X.Opens}

Lean source · statement

theorem chartHom_mk (hi : IsFrameOn M (σ i) V) (d : ℕ) (a : MvPolynomial (Fin (N + 1)) R)
    (ha : a ∈ (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R) (d • 1)) :
    chartHom f hi (Away.mk _ (ProjSpace.X_mem_one R N i) d a ha) = evalHom f hi a

theorem

chartHom_ratio

L334 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.chartHom_ratio

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V W : X.Opens}

Lean source · statement

theorem chartHom_ratio (hi : IsFrameOn M (σ i) V) (k : Fin (N + 1)) :
    chartHom f hi (ProjSpace.ratio R N i k) = hi.trans k

theorem

chartHom_algebraMap

L338 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.chartHom_algebraMap

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V W : X.Opens}

Lean source · statement

theorem chartHom_algebraMap (hi : IsFrameOn M (σ i) V) (r : R) :
    chartHom f hi (algebraMap R _ r) = algR f V r

theorem

chartHom_comp_algebraMap

L346 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.chartHom_comp_algebraMap

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V W : X.Opens}

Lean source · statement

theorem chartHom_comp_algebraMap (hi : IsFrameOn M (σ i) V) :
    (chartHom f hi).comp (algebraMap R _) = algR f V

theorem

map_comp_chartHom

L350 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.map_comp_chartHom

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V W : X.Opens}

Lean source · statement

theorem map_comp_chartHom (hi : IsFrameOn M (σ i) V) (ι : W ⟶ V) :
    (X.presheaf.map ι.op).hom.comp (chartHom f hi) = chartHom f (hi.mono ι.le)

theorem

map_chartHom

L359 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.map_chartHom

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V W : X.Opens}

Lean source · statement

theorem map_chartHom (hi : IsFrameOn M (σ i) V) (ι : W ⟶ V) (z) :
    X.presheaf.map ι.op (chartHom f hi z) = chartHom f (hi.mono ι.le) z

def

chart

L364 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.chart

Documentation

The projective chart morphism defined by a frame.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V W : X.Opens}

Lean source · statement

def chart (hi : IsFrameOn M (σ i) V) :
    (V : Scheme.{u}) ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)

theorem

homOfLE_chart

L369 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.homOfLE_chart

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V W : X.Opens}

Lean source · statement

theorem homOfLE_chart (hi : IsFrameOn M (σ i) V) (h : W ≤ V) :
    X.homOfLE h ≫ chart f hi = chart f (hi.mono h)

theorem

chart_π

L378 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.chart_π

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V W : X.Opens}

Lean source · statement

theorem chart_π (hi : IsFrameOn M (σ i) V) : chart f hi ≫ ProjSpace.π R N = V.ι ≫ f

theorem

eval₂_mul_of_isHomogeneous

L415 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.eval₂_mul_of_isHomogeneous

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · full declaration

theorem eval₂_mul_of_isHomogeneous {R ι S : Type*} [CommRing R] [CommRing S] (φ : R →+* S) (g : ι
  → S) (c : S)
    {p : MvPolynomial ι R} {n : ℕ} (hp : p.IsHomogeneous n) :
    MvPolynomial.eval₂ φ (fun k => c * g k) p = c ^ n * MvPolynomial.eval₂ φ g p := by
  classical
  rw [MvPolynomial.eval₂_eq, MvPolynomial.eval₂_eq, Finset.mul_sum]
  refine Finset.sum_congr rfl fun d hd => ?_
  have hdeg : ∑ k ∈ d.support, d k = n := by
    have := hp (MvPolynomial.mem_support_iff.mp hd)
    simpa [Finsupp.weight_apply, Finsupp.sum] using this
  simp only [mul_pow, Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum, hdeg]
  ring

theorem

XX_mem_two

L435 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.XX_mem_two

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  {σ : Fin (N + 1) → Γ(M, ⊤)}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V : X.Opens}

Lean source · statement

theorem XX_mem_two (i j : Fin (N + 1)) :
    (MvPolynomial.X i * MvPolynomial.X j : MvPolynomial (Fin (N + 1)) R) ∈
      (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R) 2

theorem

XX_eq_left

L440 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.XX_eq_left

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  {σ : Fin (N + 1) → Γ(M, ⊤)}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V : X.Opens}

Lean source · statement

theorem XX_eq_left (i j : Fin (N + 1)) :
    (MvPolynomial.X i * MvPolynomial.X j : MvPolynomial (Fin (N + 1)) R) = MvPolynomial.X i *
      MvPolynomial.X j

theorem

XX_eq_right

L445 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.XX_eq_right

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  {σ : Fin (N + 1) → Γ(M, ⊤)}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V : X.Opens}

Lean source · statement

theorem XX_eq_right (i j : Fin (N + 1)) :
    (MvPolynomial.X i * MvPolynomial.X j : MvPolynomial (Fin (N + 1)) R) = MvPolynomial.X j *
      MvPolynomial.X i

theorem

evalHom_eq_mul_evalHom

L450 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.evalHom_eq_mul_evalHom

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  {σ : Fin (N + 1) → Γ(M, ⊤)}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V : X.Opens}

Lean source · statement

theorem evalHom_eq_mul_evalHom (hi : IsFrameOn M (σ i) V) (hj : IsFrameOn M (σ j) V)
    {a : MvPolynomial (Fin (N + 1)) R} {n : ℕ} (ha : a.IsHomogeneous n) :
    evalHom f hj a = hj.trans i ^ n * evalHom f hi a

def

chartHom₂

L459 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.chartHom₂

Documentation

The homomorphism on an overlap where both projective coordinates are invertible.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  {σ : Fin (N + 1) → Γ(M, ⊤)}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V : X.Opens}

Lean source · statement

def chartHom₂ {k : Fin (N + 1)} (hk : IsFrameOn M (σ k) V) (i j : Fin (N + 1))
    (hu : IsUnit (evalHom f hk (MvPolynomial.X i * MvPolynomial.X j))) :
    Away (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)
        (MvPolynomial.X i * MvPolynomial.X j : MvPolynomial (Fin (N + 1)) R) →+* Γ(X, V)

theorem

chartHom₂_mk_mul

L470 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.chartHom₂_mk_mul

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  {σ : Fin (N + 1) → Γ(M, ⊤)}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V : X.Opens}

Lean source · statement

theorem chartHom₂_mk_mul {k : Fin (N + 1)} (hk : IsFrameOn M (σ k) V) (i j : Fin (N + 1))
    (hu : IsUnit (evalHom f hk (MvPolynomial.X i * MvPolynomial.X j))) {e : ℕ}
    (hx2 : (MvPolynomial.X i * MvPolynomial.X j : MvPolynomial (Fin (N + 1)) R) ∈
      (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R) e)
    (d : ℕ) (a : MvPolynomial (Fin (N + 1)) R)
    (ha : a ∈ (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R) (d • e)) :
    chartHom₂ f hk i j hu (Away.mk _ hx2 d a ha) *
        evalHom f hk (MvPolynomial.X i * MvPolynomial.X j) ^ d = evalHom f hk a

theorem

isUnit_evalHom_XX_left

L489 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.isUnit_evalHom_XX_left

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  {σ : Fin (N + 1) → Γ(M, ⊤)}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V : X.Opens}

Lean source · statement

theorem isUnit_evalHom_XX_left (hi : IsFrameOn M (σ i) V) (hj : IsFrameOn M (σ j) V) :
    IsUnit (evalHom f hi (MvPolynomial.X i * MvPolynomial.X j))

theorem

isUnit_evalHom_XX_right

L494 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.isUnit_evalHom_XX_right

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  {σ : Fin (N + 1) → Γ(M, ⊤)}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V : X.Opens}

Lean source · statement

theorem isUnit_evalHom_XX_right (hi : IsFrameOn M (σ i) V) (hj : IsFrameOn M (σ j) V) :
    IsUnit (evalHom f hj (MvPolynomial.X i * MvPolynomial.X j))

theorem

chartHom₂_left_mk

L499 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.chartHom₂_left_mk

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  {σ : Fin (N + 1) → Γ(M, ⊤)}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V : X.Opens}

Lean source · statement

theorem chartHom₂_left_mk (hi : IsFrameOn M (σ i) V) (hj : IsFrameOn M (σ j) V) {e : ℕ}
    (hx2 : (MvPolynomial.X i * MvPolynomial.X j : MvPolynomial (Fin (N + 1)) R) ∈
      (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R) e)
    (d : ℕ) (a : MvPolynomial (Fin (N + 1)) R)
    (ha : a ∈ (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R) (d • e)) :
    chartHom₂ f hi i j (isUnit_evalHom_XX_left f hi hj) (Away.mk _ hx2 d a ha) =
      evalHom f hi a * hj.trans i ^ d

theorem

chartHom₂_right_mk

L512 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.chartHom₂_right_mk

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  {σ : Fin (N + 1) → Γ(M, ⊤)}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V : X.Opens}

Lean source · statement

theorem chartHom₂_right_mk (hi : IsFrameOn M (σ i) V) (hj : IsFrameOn M (σ j) V) {e : ℕ}
    (hx2 : (MvPolynomial.X i * MvPolynomial.X j : MvPolynomial (Fin (N + 1)) R) ∈
      (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R) e)
    (d : ℕ) (a : MvPolynomial (Fin (N + 1)) R)
    (ha : a ∈ (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R) (d • e)) :
    chartHom₂ f hj i j (isUnit_evalHom_XX_right f hi hj) (Away.mk _ hx2 d a ha) =
      evalHom f hj a * hi.trans j ^ d

theorem

chartHom₂_left_eq_right

L525 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.chartHom₂_left_eq_right

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  {σ : Fin (N + 1) → Γ(M, ⊤)}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V : X.Opens}

Lean source · statement

theorem chartHom₂_left_eq_right (hi : IsFrameOn M (σ i) V) (hj : IsFrameOn M (σ j) V) :
    chartHom₂ f hi i j (isUnit_evalHom_XX_left f hi hj) = chartHom₂ f hj i j
      (isUnit_evalHom_XX_right f hi hj)

theorem

chartHom₂_left_comp_awayMap

L541 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.chartHom₂_left_comp_awayMap

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  {σ : Fin (N + 1) → Γ(M, ⊤)}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V : X.Opens}

Lean source · statement

theorem chartHom₂_left_comp_awayMap (hi : IsFrameOn M (σ i) V) (hj : IsFrameOn M (σ j) V) :
    (chartHom₂ f hi i j (isUnit_evalHom_XX_left f hi hj)).comp
      (awayMap _ (ProjSpace.X_mem_one R N j) (XX_eq_left i j)) = chartHom f hi

theorem

chartHom₂_right_comp_awayMap

L551 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.chartHom₂_right_comp_awayMap

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  {σ : Fin (N + 1) → Γ(M, ⊤)}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V : X.Opens}

Lean source · statement

theorem chartHom₂_right_comp_awayMap (hi : IsFrameOn M (σ i) V) (hj : IsFrameOn M (σ j) V) :
    (chartHom₂ f hj i j (isUnit_evalHom_XX_right f hi hj)).comp
      (awayMap _ (ProjSpace.X_mem_one R N i) (XX_eq_right i j)) = chartHom f hj

theorem

chart_eq_chart

L561 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.IsFrameOn.chart_eq_chart

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  {σ : Fin (N + 1) → Γ(M, ⊤)}
namespace IsFrameOn
variable {i j : Fin (N + 1)} {V : X.Opens}

Lean source · statement

theorem chart_eq_chart (hi : IsFrameOn M (σ i) V) (hj : IsFrameOn M (σ j) V) : chart f hi = chart
  f hj

def

Umax

L602 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.Umax

Documentation

The maximal framing open for the specified global section.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))

Lean source · statement

def Umax (k : Fin (N + 1)) : X.Opens

theorem

isFrameOn_Umax

L604 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.isFrameOn_Umax

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))

Lean source · statement

theorem isFrameOn_Umax (k : Fin (N + 1)) : IsFrameOn M (σ k) (Umax σ k)

theorem

le_Umax

L608 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.le_Umax

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ} in

Lean source · statement

theorem le_Umax {k : Fin (N + 1)} {V : X.Opens} (h : IsFrameOn M (σ k) V) : V ≤ Umax σ k

abbrev

chartMax

L612 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.chartMax

Documentation

The projective chart on the maximal framing open.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ} in

Lean source · statement

abbrev chartMax (k : Fin (N + 1)) :
    (Umax σ k : Scheme.{u}) ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)

def

cover

L619 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.cover

Documentation

The open cover formed by the maximal framing opens.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ} in
variable (hcov : IsOpenCover (Umax (M := M) σ))

Lean source · statement

def cover : X.OpenCover

theorem

charts_compatible

L621 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.charts_compatible

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ} in
variable (hcov : IsOpenCover (Umax (M := M) σ))

Lean source · statement

theorem charts_compatible (k l : Fin (N + 1)) :
    pullback.fst ((Umax σ k).ι) ((Umax σ l).ι) ≫ chartMax f σ k =
      pullback.snd ((Umax σ k).ι) ((Umax σ l).ι) ≫ chartMax f σ l

def

toProj

L630 ↗

AlgebraicGeometry.Scheme.Modules.LinSys.toProj

Documentation

The projective morphism obtained by gluing the compatible frame charts.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ} in
variable (hcov : IsOpenCover (Umax (M := M) σ))

Lean source · statement

def _root_.AlgebraicGeometry.Scheme.Modules.LinSys.toProj : X ⟶ Proj
  (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)

theorem

ι_toProj

L634 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.ι_toProj

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ} in
variable (hcov : IsOpenCover (Umax (M := M) σ))

Lean source · statement

theorem ι_toProj (k : Fin (N + 1)) : (Umax σ k).ι ≫
  _root_.AlgebraicGeometry.Scheme.Modules.LinSys.toProj f σ hcov = chartMax f σ k

theorem

homOfLE_ι_toProj

L638 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.homOfLE_ι_toProj

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ} in
variable (hcov : IsOpenCover (Umax (M := M) σ))

Lean source · statement

theorem homOfLE_ι_toProj {k : Fin (N + 1)} {V : X.Opens} (h : IsFrameOn M (σ k) V) :
    V.ι ≫ _root_.AlgebraicGeometry.Scheme.Modules.LinSys.toProj f σ hcov = IsFrameOn.chart f h

theorem

toProj_π

L642 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.toProj_π

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
  (σ : Fin (N + 1) → Γ(M, ⊤))
variable {σ} in
variable (hcov : IsOpenCover (Umax (M := M) σ))

Lean source · statement

theorem toProj_π : _root_.AlgebraicGeometry.Scheme.Modules.LinSys.toProj f σ hcov ≫ ProjSpace.π R
  N = f

theorem

appLE_awayToSection_of_fac

L681 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.appLE_awayToSection_of_fac

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}

Lean source · statement

theorem appLE_awayToSection_of_fac {A τ : Type u} [CommRing A] [SetLike τ A] [AddSubgroupClass τ A]
    (𝒜 : ℕ → τ) [GradedRing 𝒜]
    {g : A} {m : ℕ} (g_deg : g ∈ 𝒜 m) (hm : 0 < m)
    (φ : X ⟶ Proj 𝒜) {V : X.Opens} (hV : IsAffineOpen V) (ψ : Away 𝒜 g →+* Γ(X, V))
    (hfac : V.ι ≫ φ = V.toSpecΓ ≫ Spec.map (CommRingCat.ofHom ψ) ≫ Proj.awayι 𝒜 g g_deg hm)
    (hle : V ≤ φ ⁻¹ᵁ Proj.basicOpen 𝒜 g) (z : Away 𝒜 g) :
    φ.appLE (Proj.basicOpen 𝒜 g) V hle (Proj.awayToSection 𝒜 g z) = ψ z

theorem

Umax_le_preimage

L710 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.Umax_le_preimage

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
variable (σ : Fin (N + 1) → Γ(M, ⊤)) (hcov : IsOpenCover (Umax (M := M) σ))

Lean source · statement

theorem Umax_le_preimage (k : Fin (N + 1)) :
    Umax σ k ≤ _root_.AlgebraicGeometry.Scheme.Modules.LinSys.toProj f σ hcov ⁻¹ᵁ
      Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R) (MvPolynomial.X k)

theorem

chart_preimage_basicOpen

L725 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.chart_preimage_basicOpen

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
variable (σ : Fin (N + 1) → Γ(M, ⊤)) (hcov : IsOpenCover (Umax (M := M) σ))
variable {σ} in

Lean source · statement

theorem chart_preimage_basicOpen {k : Fin (N + 1)} {V : X.Opens} (h : IsFrameOn M (σ k) V)
    (i : Fin (N + 1)) :
    IsFrameOn.chart f h ⁻¹ᵁ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)
      (MvPolynomial.X i) = V.ι ⁻¹ᵁ X.basicOpen (h.trans i)

theorem

preimage_le_Umax

L738 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.preimage_le_Umax

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
variable (σ : Fin (N + 1) → Γ(M, ⊤)) (hcov : IsOpenCover (Umax (M := M) σ))
variable {σ} in

Lean source · statement

theorem preimage_le_Umax (i : Fin (N + 1)) :
    _root_.AlgebraicGeometry.Scheme.Modules.LinSys.toProj f σ hcov ⁻¹ᵁ Proj.basicOpen
      (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R) (MvPolynomial.X i)
      ≤ Umax σ i

theorem

preimage_eq_Umax

L757 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.preimage_eq_Umax

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
variable (σ : Fin (N + 1) → Γ(M, ⊤)) (hcov : IsOpenCover (Umax (M := M) σ))
variable {σ} in

Lean source · statement

theorem preimage_eq_Umax (i : Fin (N + 1)) :
    _root_.AlgebraicGeometry.Scheme.Modules.LinSys.toProj f σ hcov ⁻¹ᵁ Proj.basicOpen
      (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R) (MvPolynomial.X i)
      = Umax σ i

theorem

isFrameOn_preimage

L763 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.isFrameOn_preimage

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
variable (σ : Fin (N + 1) → Γ(M, ⊤)) (hcov : IsOpenCover (Umax (M := M) σ))
variable {σ} in

Lean source · statement

theorem isFrameOn_preimage (i : Fin (N + 1)) :
    IsFrameOn M (σ i) (_root_.AlgebraicGeometry.Scheme.Modules.LinSys.toProj f σ hcov ⁻¹ᵁ
      Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R) (MvPolynomial.X i))

theorem

map_app_awayToSection_ratio

L768 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.map_app_awayToSection_ratio

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
variable (σ : Fin (N + 1) → Γ(M, ⊤)) (hcov : IsOpenCover (Umax (M := M) σ))
variable {σ} in

Lean source · statement

theorem map_app_awayToSection_ratio (i j : Fin (N + 1)) {V : X.Opens} (hVaff : IsAffineOpen V)
    (hV : V ≤ _root_.AlgebraicGeometry.Scheme.Modules.LinSys.toProj f σ hcov ⁻¹ᵁ
      Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R) (MvPolynomial.X i)) :
    X.presheaf.map (homOfLE hV).op
      ((_root_.AlgebraicGeometry.Scheme.Modules.LinSys.toProj f σ hcov).app (Proj.basicOpen
        (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)
        (MvPolynomial.X i)) (Proj.awayToSection _ (MvPolynomial.X i) (ProjSpace.ratio R N i j))) =
      ((isFrameOn_preimage f σ hcov i).mono hV).trans j

theorem

app_ratio_smul

L784 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.app_ratio_smul

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
variable (σ : Fin (N + 1) → Γ(M, ⊤)) (hcov : IsOpenCover (Umax (M := M) σ))
variable {σ} in

Lean source · statement

theorem app_ratio_smul (i j : Fin (N + 1)) :
    ((_root_.AlgebraicGeometry.Scheme.Modules.LinSys.toProj f σ hcov).app (Proj.basicOpen
      (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)
        (MvPolynomial.X i)) (Proj.awayToSection _ (MvPolynomial.X i) (ProjSpace.ratio R N i j))) •
      resTop M (σ i) (_root_.AlgebraicGeometry.Scheme.Modules.LinSys.toProj f σ hcov ⁻¹ᵁ
        Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R) (MvPolynomial.X i)) =
    resTop M (σ j) (_root_.AlgebraicGeometry.Scheme.Modules.LinSys.toProj f σ hcov ⁻¹ᵁ
        Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R) (MvPolynomial.X i))

def

projPresentation

L808 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.LinSys.projPresentation

Documentation

The projective presentation determined by the covering family of global frames.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace MvPolynomial
  HomogeneousLocalization
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
namespace LinSys
noncomputable section
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) {M : X.Modules} {N : ℕ}
variable (σ : Fin (N + 1) → Γ(M, ⊤)) (hcov : IsOpenCover (Umax (M := M) σ))
variable {σ} in

Lean source · full declaration

def projPresentation : M.ProjPresentation f N where
  σ := σ
  toProj := _root_.AlgebraicGeometry.Scheme.Modules.LinSys.toProj f σ hcov
  toProj_π := toProj_π f σ hcov
  frame := fun i V hV => isFrameOn_preimage f σ hcov i V hV
  app_ratio_smul := fun i j => app_ratio_smul f σ hcov i j

theorem

exists_projPresentation_of_iSup_eq_top'

L828 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.ProjectivePresentation.AlgebraicGeometry.Scheme.Modules.exists_projPresentation_of_iSup_eq_top'

Source context 9 commands

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

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

Lean source · full declaration

theorem Scheme.Modules.exists_projPresentation_of_iSup_eq_top'
    {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (M : X.Modules)
    (N : ℕ) (σ : Fin (N + 1) → Γ(M, ⊤))
    (U : Fin (N + 1) → X.Opens) (hU : iSup U = ⊤)
    (hframe : ∀ i (V : X.Opens), V ≤ U i →
       Function.Bijective fun g : Γ(X, V) => g • (M.presheaf.map (homOfLE (le_top : V ≤ ⊤)).op (σ
         i) : Γ(M, V))) :
    ∃ 𝔓 : M.ProjPresentation f N, 𝔓.σ = σ ∧ ∀ i, U i ≤ 𝔓.toProj ⁻¹ᵁ Proj.basicOpen _
      (MvPolynomial.X i) := by
  have hUle : ∀ i, U i ≤ Scheme.Modules.LinSys.Umax σ i := fun i =>
    Scheme.Modules.LinSys.le_Umax (hframe i)
  have hcov : IsOpenCover (Scheme.Modules.LinSys.Umax (M := M) σ) := by
    change iSup _ = ⊤
    exact top_le_iff.mp (hU ▸ iSup_mono hUle)
  exact ⟨Scheme.Modules.LinSys.projPresentation f σ hcov, rfl, fun i =>
    (hUle i).trans (Scheme.Modules.LinSys.Umax_le_preimage f σ hcov i)⟩

theorem

exists_projPresentation_of_iSup_eq_top

L852 ↗

AlgebraicGeometry.Scheme.Modules.exists_projPresentation_of_iSup_eq_top

Source context 7 commands

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

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

Lean source · full declaration

theorem _root_.AlgebraicGeometry.Scheme.Modules.exists_projPresentation_of_iSup_eq_top
    {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (M : X.Modules)
    (N : ℕ) (σ : Fin (N + 1) → Γ(M, ⊤))
    (U : Fin (N + 1) → X.Opens) (hU : iSup U = ⊤)
    (hframe : ∀ i (V : X.Opens), V ≤ U i →
       Function.Bijective fun g : Γ(X, V) => g • (M.presheaf.map (homOfLE (le_top : V ≤ ⊤)).op (σ
         i) : Γ(M, V))) :
    ∃ 𝔓 : M.ProjPresentation f N, 𝔓.σ = σ ∧ ∀ i, U i ≤ 𝔓.toProj ⁻¹ᵁ Proj.basicOpen _
      (MvPolynomial.X i) :=
  AlgebraicGeometry.Scheme.Modules.exists_projPresentation_of_iSup_eq_top' f M N σ U hU hframe

Module documentation

Scheme Modules exists proj Presentation of i Sup eq top

Declarations