NYLL
Module

ProjSpace_exists_twistObj_top_forall_res_eq_of_mem_H0_twist.lean

Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_twistObj_top_forall_res_eq_of_mem_H0_twist
8 declarations indexed from sourceView source ↗

Module documentation

Proj Space exists twist Obj top forall res eq of mem H0 twist

Imports5
Imported by2

Declarations

def

single

L40 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_twistObj_top_forall_res_eq_of_mem_H0_twist.P2mWs6Glue.single
Documentation

The degree-zero index for a single chart of the pulled-back standard cover.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_twistObj_top_forall_res_eq_of_mem_H0_twist
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mWs6Glue
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
Lean source · statement
def single (a : Fin (n + 1)) : (ProjSpace.stdCoverPullback ι).Idx 0
theorem

eq_single

L43 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_twistObj_top_forall_res_eq_of_mem_H0_twist.P2mWs6Glue.eq_single
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_twistObj_top_forall_res_eq_of_mem_H0_twist
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mWs6Glue
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
Lean source · statement
theorem eq_single (s : (ProjSpace.stdCoverPullback ι).Idx 0) : s = single ι (s.1 0).down
theorem

inter_single

L50 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_twistObj_top_forall_res_eq_of_mem_H0_twist.P2mWs6Glue.inter_single
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_twistObj_top_forall_res_eq_of_mem_H0_twist
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mWs6Glue
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
Lean source · statement
theorem inter_single (a : Fin (n + 1)) :
    (ProjSpace.stdCoverPullback ι).inter (single ι a) = ProjSpace.pullbackChart ι a
def

pair

L59 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_twistObj_top_forall_res_eq_of_mem_H0_twist.P2mWs6Glue.pair
Documentation

The degree-one index for two strictly ordered charts of the pulled-back standard cover.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_twistObj_top_forall_res_eq_of_mem_H0_twist
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mWs6Glue
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
Lean source · statement
def pair (a b : Fin (n + 1)) (hab : a < b) : (ProjSpace.stdCoverPullback ι).Idx 1
theorem

face_pair_zero

L68 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_twistObj_top_forall_res_eq_of_mem_H0_twist.P2mWs6Glue.face_pair_zero
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_twistObj_top_forall_res_eq_of_mem_H0_twist
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mWs6Glue
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
Lean source · statement
theorem face_pair_zero (a b : Fin (n + 1)) (hab : a < b) :
    (ProjSpace.stdCoverPullback ι).face (pair ι a b hab) 0 = single ι b
theorem

face_pair_one

L74 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_twistObj_top_forall_res_eq_of_mem_H0_twist.P2mWs6Glue.face_pair_one
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_twistObj_top_forall_res_eq_of_mem_H0_twist
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mWs6Glue
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
Lean source · statement
theorem face_pair_one (a b : Fin (n + 1)) (hab : a < b) :
    (ProjSpace.stdCoverPullback ι).face (pair ι a b hab) 1 = single ι a
theorem

inter_single_inf_le_inter_pair

L80 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_twistObj_top_forall_res_eq_of_mem_H0_twist.P2mWs6Glue.inter_single_inf_le_inter_pair
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_twistObj_top_forall_res_eq_of_mem_H0_twist
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mWs6Glue
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
Lean source · statement
theorem inter_single_inf_le_inter_pair (a b : Fin (n + 1)) (hab : a < b) :
    (ProjSpace.stdCoverPullback ι).inter (single ι a) ⊓ (ProjSpace.stdCoverPullback ι).inter
      (single ι b)
      ≤ (ProjSpace.stdCoverPullback ι).inter (pair ι a b hab)
theorem

exists_twistObj_top_forall_res_eq_of_mem_H0_twist

L95 ↗
AlgebraicGeometry.ProjSpace.exists_twistObj_top_forall_res_eq_of_mem_H0_twist
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_twistObj_top_forall_res_eq_of_mem_H0_twist
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open P2mWs6Glue in
Lean source · statement
theorem _root_.AlgebraicGeometry.ProjSpace.exists_twistObj_top_forall_res_eq_of_mem_H0_twist
    {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
    (φ : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom φ] (m : ℕ)
    (c : (ProjSpace.twist (φ ≫ ProjSpace.π A n) φ m).cochain (ProjSpace.stdCoverPullback φ) 0)
    (hc : c ∈ (ProjSpace.twist (φ ≫ ProjSpace.π A n) φ m).H0 (ProjSpace.stdCoverPullback φ)) :
    ∃ g : ProjSpace.twistObj (φ ≫ ProjSpace.π A n) φ m ⊤,
      ∀ s : (ProjSpace.stdCoverPullback φ).Idx 0,
        (ProjSpace.twist (φ ≫ ProjSpace.π A n) φ m).res (le_top : (ProjSpace.stdCoverPullback
          φ).inter s ≤ ⊤) g = c s

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