NYLL
Module

ProjSpace_exists_projPresentation_toProj_eq_and_locallyTrivial.lean

Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_projPresentation_toProj_eq_and_locallyTrivial
12 declarations indexed from sourceView source ↗

Module documentation

Proj Space exists proj Presentation to Proj eq and locally Trivial

Imports6
Imported by2

Declarations

def

U

L75 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_projPresentation_toProj_eq_and_locallyTrivial.AlgebraicGeometry.ProjSpace.PRES.U
Documentation

The pulled-back standard projective chart indexed by a universe-lifted coordinate.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_projPresentation_toProj_eq_and_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace PRES
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.Scheme.Modules.GlueOfCocycle
variable {A : Type u} [CommRing A] {n : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
def U (i : ULift.{u} (Fin (n + 1))) : X.Opens
def

fu

L78 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_projPresentation_toProj_eq_and_locallyTrivial.AlgebraicGeometry.ProjSpace.PRES.fu
Documentation

The transition unit between the two chosen frames on a pulled-back projective chart.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_projPresentation_toProj_eq_and_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace PRES
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.Scheme.Modules.GlueOfCocycle
variable {A : Type u} [CommRing A] {n : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
def fu (i j : ULift.{u} (Fin (n + 1))) : Γ(X, U φ i)
theorem

fu_self

L80 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_projPresentation_toProj_eq_and_locallyTrivial.AlgebraicGeometry.ProjSpace.PRES.fu_self
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_projPresentation_toProj_eq_and_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace PRES
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.Scheme.Modules.GlueOfCocycle
variable {A : Type u} [CommRing A] {n : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem fu_self (i : ULift.{u} (Fin (n + 1))) : fu φ i i = 1
theorem

fu_cocycle

L82 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_projPresentation_toProj_eq_and_locallyTrivial.AlgebraicGeometry.ProjSpace.PRES.fu_cocycle
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_projPresentation_toProj_eq_and_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace PRES
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.Scheme.Modules.GlueOfCocycle
variable {A : Type u} [CommRing A] {n : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem fu_cocycle (i j k : ULift.{u} (Fin (n + 1))) {W : X.Opens} (hi : W ≤ U φ i) (hj : W ≤ U φ
  j) :
    rO hi (fu φ i j) * rO hj (fu φ j k) = rO hi (fu φ i k)
def

cocycle

L94 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_projPresentation_toProj_eq_and_locallyTrivial.AlgebraicGeometry.ProjSpace.PRES.cocycle
Documentation

The unit cocycle formed by the projective transition units on chart intersections.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_projPresentation_toProj_eq_and_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace PRES
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.Scheme.Modules.GlueOfCocycle
variable {A : Type u} [CommRing A] {n : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · full declaration
def cocycle : UnitCocycle (U φ) where
  u i j := rO inf_le_left (fu φ i j)
  refl i := by rw [fu_self, map_one]
  cocycle i j k := by
    rw [rO_rO, rO_rO, rO_rO]
    exact fu_cocycle φ i j k _ _
def

σ

L105 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_projPresentation_toProj_eq_and_locallyTrivial.AlgebraicGeometry.ProjSpace.PRES.σ
Documentation

The global section of the glued line bundle obtained from the transition units for the chosen coordinate.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_projPresentation_toProj_eq_and_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace PRES
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.Scheme.Modules.GlueOfCocycle
variable {A : Type u} [CommRing A] {n : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
def σ (i : ULift.{u} (Fin (n + 1))) : Γ(glueOfCocycle (cocycle φ), ⊤)
theorem

map_σ

L111 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_projPresentation_toProj_eq_and_locallyTrivial.AlgebraicGeometry.ProjSpace.PRES.map_σ
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_projPresentation_toProj_eq_and_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace PRES
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.Scheme.Modules.GlueOfCocycle
variable {A : Type u} [CommRing A] {n : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem map_σ (i : ULift.{u} (Fin (n + 1))) :
    (glueOfCocycle (cocycle φ)).presheaf.map (homOfLE (le_top : U φ i ≤ ⊤)).op (σ φ i) = glueFrame
      (cocycle φ) i
theorem

map_σ_of_le

L120 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_projPresentation_toProj_eq_and_locallyTrivial.AlgebraicGeometry.ProjSpace.PRES.map_σ_of_le
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_projPresentation_toProj_eq_and_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace PRES
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.Scheme.Modules.GlueOfCocycle
variable {A : Type u} [CommRing A] {n : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem map_σ_of_le (i : ULift.{u} (Fin (n + 1))) {V : X.Opens} (hV : V ≤ U φ i) :
    (glueOfCocycle (cocycle φ)).presheaf.map (homOfLE (le_top : V ≤ ⊤)).op (σ φ i) =
      (glueOfCocycle (cocycle φ)).presheaf.map (homOfLE hV).op (glueFrame (cocycle φ) i)
theorem

fu_smul_map_σ

L126 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_projPresentation_toProj_eq_and_locallyTrivial.AlgebraicGeometry.ProjSpace.PRES.fu_smul_map_σ
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_projPresentation_toProj_eq_and_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace PRES
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.Scheme.Modules.GlueOfCocycle
variable {A : Type u} [CommRing A] {n : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem fu_smul_map_σ (i j : ULift.{u} (Fin (n + 1))) :
    fu φ i j • (glueOfCocycle (cocycle φ)).presheaf.map (homOfLE (le_top : U φ i ≤ ⊤)).op (σ φ i) =
      (glueOfCocycle (cocycle φ)).presheaf.map (homOfLE (le_top : U φ i ≤ ⊤)).op (σ φ j)
theorem

exists_mem_U

L137 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_projPresentation_toProj_eq_and_locallyTrivial.AlgebraicGeometry.ProjSpace.PRES.exists_mem_U
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_projPresentation_toProj_eq_and_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace PRES
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.Scheme.Modules.GlueOfCocycle
variable {A : Type u} [CommRing A] {n : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem exists_mem_U (x : X) : ∃ i, x ∈ U φ i
def

pres

L149 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_projPresentation_toProj_eq_and_locallyTrivial.AlgebraicGeometry.ProjSpace.PRES.pres
Documentation

The projective presentation of the glued line bundle using the given morphism and its coordinate sections.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_projPresentation_toProj_eq_and_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace PRES
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.Scheme.Modules.GlueOfCocycle
variable {A : Type u} [CommRing A] {n : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · full declaration
def pres : (glueOfCocycle (cocycle φ)).ProjPresentation (φ ≫ ProjSpace.π A n) n where
  σ i := σ φ ⟨i⟩
  toProj := φ
  toProj_π := rfl
  frame i V hV := by
    rw [map_σ_of_le φ ⟨i⟩ hV]
    exact isFrameOn_glueFrame (cocycle φ) ⟨i⟩ hV hV
  app_ratio_smul i j := fu_smul_map_σ φ ⟨i⟩ ⟨j⟩
theorem

exists_projPresentation_toProj_eq_and_locallyTrivial

L170 ↗
AlgebraicGeometry.ProjSpace.exists_projPresentation_toProj_eq_and_locallyTrivial
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_projPresentation_toProj_eq_and_locallyTrivial
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem _root_.AlgebraicGeometry.ProjSpace.exists_projPresentation_toProj_eq_and_locallyTrivial
    {A : Type u} [CommRing A] {n : ℕ} {X : Scheme.{u}}
    (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) :
    ∃ (L : X.Modules) (𝔓 : L.ProjPresentation (φ ≫ ProjSpace.π A n) n), 𝔓.toProj = φ ∧
      ∀ x : X, ∃ U : X.Opens, x ∈ U ∧
        Nonempty ((Scheme.Modules.pullback U.ι).obj L ≅ SheafOfModules.unit
          U.toScheme.ringCatSheaf)

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