NYLL
Module

ProjTwistDatum.lean

Nyll.AlgebraicCurves.Geometry.Projective.ProjTwistDatum
68 declarations indexed from sourceView source ↗

Module documentation

Proj Twist Datum

Imports2
Imported by41

Declarations

theorem

val_awayMap_ratio

L35 ↗
AlgebraicGeometry.ProjSpace.val_awayMap_ratio
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable (A : Type u) [CommRing A] (N : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
local notation "S" => MvPolynomial (Fin (N + 1)) A
Lean source · statement
theorem val_awayMap_ratio (i i' _k : Fin (N + 1)) {f g : S} (hg : g ∈ 𝒜 1) (hx : X i * X i' = f * g)
    (r : Away 𝒜 f) (a : S)
    (hr : r.val = Localization.mk a (⟨f ^ 1, ⟨1, rfl⟩⟩ : Submonoid.powers f)) :
    (awayMap 𝒜 hg hx r).val
      = Localization.mk (a * g) (⟨(X i * X i' : S) ^ 1, ⟨1, rfl⟩⟩ : Submonoid.powers (X i * X i' :
        S))
theorem

awayMap_ratio_mul

L52 ↗
AlgebraicGeometry.ProjSpace.awayMap_ratio_mul
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable (A : Type u) [CommRing A] (N : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
local notation "S" => MvPolynomial (Fin (N + 1)) A
Lean source · statement
theorem awayMap_ratio_mul (i i' j : Fin (N + 1)) :
    awayMap 𝒜 (X_mem_one A N i') rfl (ratio A N i i')
        * awayMap 𝒜 (X_mem_one A N i) (mul_comm (X i) (X i') : (X i * X i' : S) = X i' * X i)
          (ratio A N i' j)
      = awayMap 𝒜 (X_mem_one A N i') rfl (ratio A N i j)
theorem

awayMap_ratio_mul_swap

L68 ↗
AlgebraicGeometry.ProjSpace.awayMap_ratio_mul_swap
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable (A : Type u) [CommRing A] (N : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
local notation "S" => MvPolynomial (Fin (N + 1)) A
Lean source · statement
theorem awayMap_ratio_mul_swap (i i' : Fin (N + 1)) :
    awayMap 𝒜 (X_mem_one A N i') rfl (ratio A N i i')
        * awayMap 𝒜 (X_mem_one A N i) (mul_comm (X i) (X i') : (X i * X i' : S) = X i' * X i)
          (ratio A N i' i)
      = 1
def

pullbackChart

L87 ↗
AlgebraicGeometry.ProjSpace.pullbackChart
Documentation

The inverse image of a standard affine chart of projective space.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
def pullbackChart (i : Fin (N + 1)) : X.Opens
theorem

pullbackChart_eq

L90 ↗
AlgebraicGeometry.ProjSpace.pullbackChart_eq
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem pullbackChart_eq (i : Fin (N + 1)) :
    pullbackChart φ i = φ ⁻¹ᵁ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)
      (MvPolynomial.X i)
def

frameUnit

L95 ↗
AlgebraicGeometry.ProjSpace.frameUnit
Documentation

The pulled-back coordinate ratio relating the two standard chart frames.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
def frameUnit (i j : Fin (N + 1)) : Γ(X, pullbackChart φ i)
abbrev

restrictFun

L101 ↗
AlgebraicGeometry.ProjSpace.restrictFun
Documentation

The ring homomorphism restricting functions to a smaller open.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
abbrev restrictFun {U U' : X.Opens} (h : U ≤ U') : Γ(X, U') →+* Γ(X, U)
def

TwistCompat

L105 ↗
AlgebraicGeometry.ProjSpace.TwistCompat
Documentation

The transition relation for local sections of the specified projective twist.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
def TwistCompat (m : ℕ) (U : X.Opens) (g : ∀ i : Fin (N + 1), Γ(X, U ⊓ pullbackChart φ i)) : Prop
def

twistSections

L115 ↗
AlgebraicGeometry.ProjSpace.twistSections
Documentation

The additive subgroup of local families satisfying the twist transition relation.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · full declaration
def twistSections (m : ℕ) (U : X.Opens) : AddSubgroup (∀ i : Fin (N + 1), Γ(X, U ⊓ pullbackChart φ
  i)) where
  carrier := {g | TwistCompat φ m U g}
  zero_mem' := fun i j => by simp
  add_mem' := by
    intro g g' hg hg' i j
    simp only [Pi.add_apply, map_add, hg i j, hg' i j, mul_add]
  neg_mem' := by
    intro g hg i j
    simp only [Pi.neg_apply, map_neg, hg i j, mul_neg]
theorem

mem_twistSections

L126 ↗
AlgebraicGeometry.ProjSpace.mem_twistSections
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem mem_twistSections {m : ℕ} {U : X.Opens} (g : ∀ i : Fin (N + 1), Γ(X, U ⊓ pullbackChart φ
  i)) :
    g ∈ twistSections φ m U ↔ TwistCompat φ m U g
theorem

smul_mem_twistSections

L130 ↗
AlgebraicGeometry.ProjSpace.smul_mem_twistSections
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · full declaration
theorem smul_mem_twistSections {m : ℕ} {U : X.Opens} (a : Γ(X, U)) {g : ∀ i, Γ(X, U ⊓
  pullbackChart φ i)}
    (hg : g ∈ twistSections φ m U) :
    (fun i => restrictFun (inf_le_left : U ⊓ pullbackChart φ i ≤ U) a * g i) ∈ twistSections φ m U
      := by
  intro i j
  simp only [map_mul, hg i j]
  have h1 : restrictFun (inf_le_left : (U ⊓ pullbackChart φ i) ⊓ pullbackChart φ j ≤ U ⊓
    pullbackChart φ i) (restrictFun (inf_le_left : U ⊓ pullbackChart φ i ≤ U) a)
      = restrictFun (le_inf (le_trans inf_le_left inf_le_left) inf_le_right : (U ⊓ pullbackChart φ
        i) ⊓ pullbackChart φ j ≤ U ⊓ pullbackChart φ j)
          (restrictFun (inf_le_left : U ⊓ pullbackChart φ j ≤ U) a) := by
    change (X.presheaf.map _ ≫ X.presheaf.map _).hom a = (X.presheaf.map _ ≫ X.presheaf.map _).hom a
    rw [← X.presheaf.map_comp, ← X.presheaf.map_comp]
    rfl
  rw [h1]
  ring
theorem

res_mem_twistSections

L148 ↗
AlgebraicGeometry.ProjSpace.res_mem_twistSections
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · full declaration
theorem res_mem_twistSections {m : ℕ} {U U' : X.Opens} (h : U ≤ U') {g : ∀ i, Γ(X, U' ⊓
  pullbackChart φ i)}
    (hg : g ∈ twistSections φ m U') :
    (fun i => restrictFun (inf_le_inf_right (pullbackChart φ i) h) (g i)) ∈ twistSections φ m U
      := by
  intro i j
  have key := congrArg (restrictFun (inf_le_inf_right (pullbackChart φ j) (inf_le_inf_right
    (pullbackChart φ i) h))) (hg i j)
  simp only [map_mul, map_pow] at key
  have e1 : ∀ (W₁ W₂ W₃ : X.Opens) (h₁ : W₁ ≤ W₂) (h₂ : W₂ ≤ W₃) (x : Γ(X, W₃)),
      restrictFun h₁ (restrictFun h₂ x) = restrictFun (h₁.trans h₂) x := by
    intro W₁ W₂ W₃ h₁ h₂ x
    change (X.presheaf.map _ ≫ X.presheaf.map _).hom x = _
    rw [← X.presheaf.map_comp]
    rfl
  rw [e1, e1, e1] at key
  rw [e1, e1]
  convert key using 2
theorem

restrictFun_restrictFun

L178 ↗
AlgebraicGeometry.ProjSpace.restrictFun_restrictFun
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
namespace ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
Lean source · statement
theorem restrictFun_restrictFun {W₁ W₂ W₃ : X.Opens} (h₁ : W₁ ≤ W₂) (h₂ : W₂ ≤ W₃) (x : Γ(X, W₃)) :
    restrictFun h₁ (restrictFun h₂ x) = restrictFun (h₁.trans h₂) x
theorem

restrictFun_irrel

L184 ↗
AlgebraicGeometry.ProjSpace.restrictFun_irrel
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
namespace ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
Lean source · statement
theorem restrictFun_irrel {W₁ W₂ : X.Opens} (h₁ h₂ : W₁ ≤ W₂) (x : Γ(X, W₂)) : restrictFun h₁ x =
  restrictFun h₂ x
theorem

restrictFun_refl

L187 ↗
AlgebraicGeometry.ProjSpace.restrictFun_refl
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
namespace ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
Lean source · statement
theorem restrictFun_refl {W : X.Opens} (x : Γ(X, W)) : restrictFun (le_refl W) x = x
theorem

restrictFun_algebraMap

L192 ↗
AlgebraicGeometry.ProjSpace.restrictFun_algebraMap
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
namespace ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
Lean source · full declaration
theorem restrictFun_algebraMap (π : X ⟶ Spec (.of A)) {U U' : X.Opens} (h : U ≤ U') (r : A) :
    letI := Scheme.TwoAffineOpenCover.algebraOfHom π U
    letI := Scheme.TwoAffineOpenCover.algebraOfHom π U'
    restrictFun h (algebraMap A (Γ(X, U') : Type u) r) = algebraMap A (Γ(X, U) : Type u) r := by
  let := Scheme.TwoAffineOpenCover.algebraOfHom π U
  let := Scheme.TwoAffineOpenCover.algebraOfHom π U'
  exact (Scheme.TwoAffineOpenCover.restrictAlgHom π h).commutes r
theorem

restrictFun_algebraMap'

L200 ↗
AlgebraicGeometry.ProjSpace.restrictFun_algebraMap'
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
namespace ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
Lean source · statement
theorem restrictFun_algebraMap' (π : X ⟶ Spec (.of A)) {U U' : X.Opens} (h : U ≤ U') (r : A) :
    restrictFun h ((Scheme.TwoAffineOpenCover.algebraOfHom π U').algebraMap r)
      = (Scheme.TwoAffineOpenCover.algebraOfHom π U).algebraMap r
structure

twistObj

L206 ↗
AlgebraicGeometry.ProjSpace.twistObj
Documentation

Local section families equipped with the twist transition relation.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
namespace ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
Lean source · full declaration
structure twistObj (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule
  (Fin (N + 1)) A)) (m : ℕ) (U : X.Opens) : Type u where
  /-- The local section on each pulled-back standard chart. -/
  val : ∀ i : Fin (N + 1), Γ(X, U ⊓ pullbackChart φ i)
  /-- Compatibility of the local sections with the twist transition functions. -/
  compat : TwistCompat φ m U val
def

equivSections

L214 ↗
AlgebraicGeometry.ProjSpace.twistObj.equivSections
Documentation

The equivalence between bundled twist families and compatible section families.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
namespace ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
Lean source · full declaration
def twistObj.equivSections (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule
  (Fin (N + 1)) A)) (m : ℕ) (U : X.Opens) :
    twistObj π φ m U ≃ twistSections φ m U where
  toFun g := ⟨g.val, g.compat⟩
  invFun s := ⟨s.1, s.2⟩
  left_inv _ := rfl
  right_inv _ := rfl
instance

addCommGroup

L222 ↗
AlgebraicGeometry.ProjSpace.twistObj.addCommGroup
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
namespace ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
Lean source · statement
instance twistObj.addCommGroup (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj
  (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ) (U : X.Opens) : AddCommGroup
  (twistObj π φ m U)
theorem

val_injective

L227 ↗
AlgebraicGeometry.ProjSpace.twistObj.val_injective
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
namespace ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
Lean source · statement
theorem twistObj.val_injective {π : X ⟶ Spec (.of A)} {φ : X ⟶ Proj
  (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)} {m : ℕ} {U : X.Opens} :
    Function.Injective (twistObj.val (π := π) (φ := φ) (m := m) (U := U))
instance

moduleSections

L232 ↗
AlgebraicGeometry.ProjSpace.twistObj.moduleSections
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
namespace ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
Lean source · full declaration
instance twistObj.moduleSections (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj
  (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ) (U : X.Opens) : Module Γ(X, U)
  (twistObj π φ m U) where
  smul a g := ⟨fun i => restrictFun inf_le_left a * g.val i, smul_mem_twistSections φ a g.compat⟩
  one_smul g := by
    refine twistObj.ext (_root_.funext fun i => ?_)
    change restrictFun _ 1 * g.val i = g.val i
    rw [map_one, one_mul]
  mul_smul a b g := by
    refine twistObj.ext (_root_.funext fun i => ?_)
    change restrictFun _ (a * b) * g.val i = restrictFun _ a * (restrictFun _ b * g.val i)
    rw [map_mul, mul_assoc]
  smul_zero a := by
    refine twistObj.ext (_root_.funext fun i => ?_)
    change restrictFun _ a * (0 : Γ(X, U ⊓ pullbackChart φ i)) = 0
    rw [mul_zero]
  smul_add a g g' := by
    refine twistObj.ext (_root_.funext fun i => ?_)
    change restrictFun _ a * (g.val i + g'.val i) = restrictFun _ a * g.val i + restrictFun _ a *
      g'.val i
    rw [mul_add]
  add_smul a b g := by
    refine twistObj.ext (_root_.funext fun i => ?_)
    change restrictFun _ (a + b) * g.val i = restrictFun _ a * g.val i + restrictFun _ b * g.val i
    rw [map_add, add_mul]
  zero_smul g := by
    refine twistObj.ext (_root_.funext fun i => ?_)
    change restrictFun _ 0 * g.val i = 0
    rw [map_zero, zero_mul]
theorem

smul_val

L262 ↗
AlgebraicGeometry.ProjSpace.twistObj.smul_val
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
namespace ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
Lean source · statement
theorem twistObj.smul_val {π : X ⟶ Spec (.of A)} {φ : X ⟶ Proj
  (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)} {m : ℕ} {U : X.Opens} (a : Γ(X, U)) (g :
  twistObj π φ m U) (i : Fin (N + 1)) :
    (a • g).val i = restrictFun inf_le_left a * g.val i
instance

module

L267 ↗
AlgebraicGeometry.ProjSpace.twistObj.module
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
namespace ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
Lean source · statement
instance twistObj.module (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule
  (Fin (N + 1)) A)) (m : ℕ) (U : X.Opens) : Module A (twistObj π φ m U)
theorem

algebraMap_smul

L272 ↗
AlgebraicGeometry.ProjSpace.twistObj.algebraMap_smul
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
namespace ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
Lean source · full declaration
theorem twistObj.algebraMap_smul {π : X ⟶ Spec (.of A)} {φ : X ⟶ Proj
  (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)} {m : ℕ} {U : X.Opens} (r : A) (g : twistObj
  π φ m U) :
    letI := Scheme.TwoAffineOpenCover.algebraOfHom π U
    r • g = algebraMap A (Γ(X, U) : Type u) r • g := by rfl
def

twistRes

L279 ↗
AlgebraicGeometry.ProjSpace.twistRes
Documentation

The linear restriction map on compatible twist families.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
namespace ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
Lean source · statement
def twistRes (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1))
  A)) (m : ℕ) {U U' : X.Opens} (h : U ≤ U') : twistObj π φ m U' →ₗ[A] twistObj π φ m U
theorem

twistRes_val

L296 ↗
AlgebraicGeometry.ProjSpace.twistRes_val
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
namespace ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
Lean source · statement
theorem twistRes_val (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin
  (N + 1)) A)) (m : ℕ) {U U' : X.Opens} (h : U ≤ U') (g : twistObj π φ m U') (i : Fin (N + 1)) :
    (twistRes π φ m h g).val i = restrictFun (inf_le_inf_right (pullbackChart φ i) h) (g.val i)
def

twist

L302 ↗
AlgebraicGeometry.ProjSpace.twist
Documentation

The module presheaf of compatible local sections of the projective twist.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
namespace ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
Lean source · full declaration
def twist (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1))
  A)) (m : ℕ) : OModulePresheaf π where
  obj U := twistObj π φ m U
  addCommGroup _ := inferInstance
  module U := twistObj.module π φ m U
  moduleSections U := twistObj.moduleSections π φ m U
  isScalarTower U := by
    let := Scheme.TwoAffineOpenCover.algebraOfHom π U
    exact ⟨fun r a g => by
      change (r • a) • g = algebraMap A (Γ(X, U) : Type u) r • (a • g)
      rw [Algebra.smul_def, mul_smul]⟩
  res h := twistRes π φ m h
  res_smul h a g := by
    change twistRes π φ m h (a • g) = restrictFun h a • twistRes π φ m h g
    refine twistObj.ext (_root_.funext fun i => ?_)
    change restrictFun _ (restrictFun _ a * g.val i) = restrictFun _ (restrictFun _ a) *
      restrictFun _ (g.val i)
    rw [map_mul, restrictFun_restrictFun, restrictFun_restrictFun]
  res_refl U := by
    refine LinearMap.ext fun g => twistObj.ext (_root_.funext fun i => ?_)
    change restrictFun _ (g.val i) = g.val i
    exact restrictFun_refl _
  res_comp h h' := by
    refine LinearMap.ext fun g => twistObj.ext (_root_.funext fun i => ?_)
    change restrictFun _ (g.val i) = restrictFun _ (restrictFun _ (g.val i))
    rw [restrictFun_restrictFun]
theorem

twist_obj

L329 ↗
AlgebraicGeometry.ProjSpace.twist_obj
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
namespace ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
Lean source · statement
theorem twist_obj (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N
  + 1)) A)) (m : ℕ) (U : X.Opens) : (twist π φ m).obj U = twistObj π φ m U
def

pullbackOverlap

L343 ↗
AlgebraicGeometry.ProjSpace.pullbackOverlap
Documentation

The inverse image of the overlap of two standard projective charts.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
def pullbackOverlap (i i' : Fin (N + 1)) : X.Opens
theorem

pullbackOverlap_eq_inf

L347 ↗
AlgebraicGeometry.ProjSpace.pullbackOverlap_eq_inf
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem pullbackOverlap_eq_inf (i i' : Fin (N + 1)) : pullbackOverlap φ i i' = pullbackChart φ i ⊓
  pullbackChart φ i'
theorem

pullbackOverlap_le_left

L351 ↗
AlgebraicGeometry.ProjSpace.pullbackOverlap_le_left
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem pullbackOverlap_le_left (i i' : Fin (N + 1)) : pullbackOverlap φ i i' ≤ pullbackChart φ i
theorem

pullbackOverlap_le_right

L355 ↗
AlgebraicGeometry.ProjSpace.pullbackOverlap_le_right
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem pullbackOverlap_le_right (i i' : Fin (N + 1)) : pullbackOverlap φ i i' ≤ pullbackChart φ
  i'
theorem

restrictFun_frameUnit_left

L359 ↗
AlgebraicGeometry.ProjSpace.restrictFun_frameUnit_left
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem restrictFun_frameUnit_left (i i' k : Fin (N + 1)) :
    restrictFun (pullbackOverlap_le_left φ i i') (frameUnit φ i k)
      = (φ.app (Proj.basicOpen _ (MvPolynomial.X i * MvPolynomial.X i'))).hom
          ((Proj.awayToSection _ (MvPolynomial.X i * MvPolynomial.X i')).hom
            (awayMap _ (X_mem_one A N i') rfl (ratio A N i k)))
theorem

restrictFun_frameUnit_right

L382 ↗
AlgebraicGeometry.ProjSpace.restrictFun_frameUnit_right
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem restrictFun_frameUnit_right (i i' k : Fin (N + 1)) :
    restrictFun (pullbackOverlap_le_right φ i i') (frameUnit φ i' k)
      = (φ.app (Proj.basicOpen _ (MvPolynomial.X i * MvPolynomial.X i'))).hom
          ((Proj.awayToSection _ (MvPolynomial.X i * MvPolynomial.X i')).hom
            (awayMap _ (X_mem_one A N i) (mul_comm (MvPolynomial.X i) (MvPolynomial.X i') :
              (MvPolynomial.X i * MvPolynomial.X i' : MvPolynomial (Fin (N + 1)) A) =
                MvPolynomial.X i' * MvPolynomial.X i)
              (ratio A N i' k)))
theorem

frameUnit_cocycle

L409 ↗
AlgebraicGeometry.ProjSpace.frameUnit_cocycle
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem frameUnit_cocycle (i i' j : Fin (N + 1)) :
    restrictFun (pullbackOverlap_le_left φ i i') (frameUnit φ i i') * restrictFun
      (pullbackOverlap_le_right φ i i') (frameUnit φ i' j)
      = restrictFun (pullbackOverlap_le_left φ i i') (frameUnit φ i j)
theorem

frameUnit_self

L417 ↗
AlgebraicGeometry.ProjSpace.frameUnit_self
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem frameUnit_self (i : Fin (N + 1)) : frameUnit φ i i = 1
theorem

frameUnit_mul_swap

L421 ↗
AlgebraicGeometry.ProjSpace.frameUnit_mul_swap
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem frameUnit_mul_swap (i i' : Fin (N + 1)) :
    restrictFun (pullbackOverlap_le_left φ i i') (frameUnit φ i i') * restrictFun
      (pullbackOverlap_le_right φ i i') (frameUnit φ i' i) = 1
theorem

add_val

L434 ↗
AlgebraicGeometry.ProjSpace.twistObj.add_val
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
Lean source · statement
theorem twistObj.add_val {π : X ⟶ Spec (.of A)} {φ : X ⟶ Proj
  (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)} {m : ℕ} {U : X.Opens}
    (g g' : twistObj π φ m U) : (g + g').val = g.val + g'.val
theorem

zero_val

L438 ↗
AlgebraicGeometry.ProjSpace.twistObj.zero_val
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
Lean source · statement
theorem twistObj.zero_val {π : X ⟶ Spec (.of A)} {φ : X ⟶ Proj
  (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)} {m : ℕ} {U : X.Opens} :
    (0 : twistObj π φ m U).val = 0
theorem

twist_res_val

L442 ↗
AlgebraicGeometry.ProjSpace.twist_res_val
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
Lean source · statement
theorem twist_res_val {π : X ⟶ Spec (.of A)} {φ : X ⟶ Proj
  (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)} {m : ℕ}
    {U U' : X.Opens} (h : U ≤ U') (g : twistObj π φ m U') (i : Fin (N + 1)) :
    ((twist π φ m).res h g).val i = restrictFun (inf_le_inf_right (pullbackChart φ i) h) (g.val i)
theorem

twist_smul_val

L448 ↗
AlgebraicGeometry.ProjSpace.twist_smul_val
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
Lean source · statement
theorem twist_smul_val {π : X ⟶ Spec (.of A)} {φ : X ⟶ Proj
  (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)} {m : ℕ}
    {U : X.Opens} (a : Γ(X, U)) (g : (twist π φ m).obj U) (i : Fin (N + 1)) :
    (a • g : twistObj π φ m U).val i = restrictFun inf_le_left a * (g : twistObj π φ m U).val i
theorem

twist_algebraMap_smul_val

L454 ↗
AlgebraicGeometry.ProjSpace.twist_algebraMap_smul_val
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
Lean source · full declaration
theorem twist_algebraMap_smul_val {π : X ⟶ Spec (.of A)} {φ : X ⟶ Proj
  (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)} {m : ℕ}
    {U : X.Opens} (r : A) (g : (twist π φ m).obj U) (i : Fin (N + 1)) :
    letI := Scheme.TwoAffineOpenCover.algebraOfHom π U
    (r • g : twistObj π φ m U).val i = restrictFun inf_le_left (algebraMap A (Γ(X, U) : Type u) r)
      * (g : twistObj π φ m U).val i :=
  rfl
def

twistFam

L475 ↗
AlgebraicGeometry.ProjSpace.twistFam
Documentation

Families of chart sections indexed by integral degree.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
section GradedModuleOfTwist
variable (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
def twistFam (_π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N +
  1)) A)) : Type u
instance

addCommGroup

L478 ↗
AlgebraicGeometry.ProjSpace.twistFam.addCommGroup
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
section GradedModuleOfTwist
variable (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
instance twistFam.addCommGroup (π : X ⟶ Spec (.of A)) : AddCommGroup (twistFam π φ)
def

moduleOfHom

L482 ↗
AlgebraicGeometry.ProjSpace.moduleOfHom
Documentation

The base-ring module structure on local functions induced by the structure morphism.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
section GradedModuleOfTwist
variable (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
def moduleOfHom (π : X ⟶ Spec (.of A)) (W : X.Opens) : Module A (Γ(X, W) : Type u)
instance

module

L485 ↗
AlgebraicGeometry.ProjSpace.twistFam.module
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
section GradedModuleOfTwist
variable (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
instance twistFam.module (π : X ⟶ Spec (.of A)) : Module A (twistFam π φ)
theorem

smul_apply

L490 ↗
AlgebraicGeometry.ProjSpace.twistFam.smul_apply
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
section GradedModuleOfTwist
variable (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem twistFam.smul_apply (π : X ⟶ Spec (.of A)) (r : A) (f : twistFam π φ) (d : ℤ) (i : Fin (N
  + 1)) :
    (r • f) d i = (Scheme.TwoAffineOpenCover.algebraOfHom π ((⊤ : X.Opens) ⊓ pullbackChart φ
      i)).algebraMap r * f d i
def

twistGrade

L496 ↗
AlgebraicGeometry.ProjSpace.twistGrade
Documentation

Families supported in one degree and satisfying the corresponding twist relation.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
section GradedModuleOfTwist
variable (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · full declaration
def twistGrade (π : X ⟶ Spec (.of A)) (d : ℤ) : Submodule A (twistFam π φ) where
  carrier := {f | (∀ d', d' ≠ d → f d' = 0) ∧ (d < 0 → f d = 0) ∧ (0 ≤ d → TwistCompat φ d.toNat ⊤
    (f d))}
  zero_mem' := ⟨fun _ _ => rfl, fun _ => rfl, fun _ => (twistSections φ d.toNat ⊤).zero_mem⟩
  add_mem' := by
    rintro f g ⟨hf1, hf2, hf3⟩ ⟨hg1, hg2, hg3⟩
    refine ⟨fun d' hd' => ?_, fun hd => ?_, fun hd => (twistSections φ d.toNat ⊤).add_mem (hf3 hd)
      (hg3 hd)⟩
    · change f d' + g d' = 0
      rw [hf1 d' hd', hg1 d' hd', add_zero]
    · change f d + g d = 0
      rw [hf2 hd, hg2 hd, add_zero]
  smul_mem' := by
    rintro r f ⟨hf1, hf2, hf3⟩
    refine ⟨fun d' hd' => ?_, fun hd => ?_, fun hd => ?_⟩
    · funext i
      change _ * f d' i = 0
      rw [hf1 d' hd']
      exact mul_zero _
    · funext i
      change _ * f d i = 0
      rw [hf2 hd]
      exact mul_zero _
    · intro i j
      have hc := hf3 hd i j
      have hi := restrictFun_algebraMap' π
        (inf_le_left : ((⊤ : X.Opens) ⊓ pullbackChart φ i) ⊓ pullbackChart φ j ≤ (⊤ : X.Opens) ⊓
          pullbackChart φ i) r
      have hj := restrictFun_algebraMap' π
        (le_inf (le_trans inf_le_left inf_le_left) inf_le_right :
          ((⊤ : X.Opens) ⊓ pullbackChart φ i) ⊓ pullbackChart φ j ≤ (⊤ : X.Opens) ⊓ pullbackChart
            φ j) r
      change restrictFun _ ((Scheme.TwoAffineOpenCover.algebraOfHom π _).algebraMap r * f d i)
        = _ * restrictFun _ ((Scheme.TwoAffineOpenCover.algebraOfHom π _).algebraMap r * f d j)
      rw [map_mul, map_mul, hc, hi, hj]
      ring
def

twistXMul

L534 ↗
AlgebraicGeometry.ProjSpace.twistXMul
Documentation

The linear operator on graded section families induced by a projective coordinate.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
section GradedModuleOfTwist
variable (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · full declaration
def twistXMul (π : X ⟶ Spec (.of A)) (j : Fin (N + 1)) : twistFam π φ →ₗ[A] twistFam π φ where
  toFun f := fun d i => restrictFun inf_le_right (frameUnit φ i j) * f (d - 1) i
  map_add' f g := by
    funext d i
    change restrictFun _ (frameUnit φ i j) * (f (d - 1) i + g (d - 1) i) = _ * _ + _ * _
    rw [mul_add]
  map_smul' r f := by
    funext d i
    let := Scheme.TwoAffineOpenCover.algebraOfHom π ((⊤ : X.Opens) ⊓ pullbackChart φ i)
    change restrictFun _ (frameUnit φ i j) * (algebraMap A (Γ(X, (⊤ : X.Opens) ⊓ pullbackChart φ
      i) : Type u) r * f (d - 1) i)
      = algebraMap A (Γ(X, (⊤ : X.Opens) ⊓ pullbackChart φ i) : Type u) r * (restrictFun _
        (frameUnit φ i j) * f (d - 1) i)
    ring
theorem

twistXMul_apply

L549 ↗
AlgebraicGeometry.ProjSpace.twistXMul_apply
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
section GradedModuleOfTwist
variable (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem twistXMul_apply (π : X ⟶ Spec (.of A)) (j : Fin (N + 1)) (f : twistFam π φ) (d : ℤ) (i :
  Fin (N + 1)) :
    twistXMul φ π j f d i = restrictFun inf_le_right (frameUnit φ i j) * f (d - 1) i
theorem

frameUnit_cocycle_top

L553 ↗
AlgebraicGeometry.ProjSpace.frameUnit_cocycle_top
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
section GradedModuleOfTwist
variable (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem frameUnit_cocycle_top (i i' j : Fin (N + 1)) :
    restrictFun (inf_le_left : ((⊤ : X.Opens) ⊓ pullbackChart φ i) ⊓ pullbackChart φ i' ≤ (⊤ :
      X.Opens) ⊓ pullbackChart φ i)
        (restrictFun inf_le_right (frameUnit φ i j))
      = restrictFun (le_trans inf_le_left inf_le_right : ((⊤ : X.Opens) ⊓ pullbackChart φ i) ⊓
        pullbackChart φ i' ≤ pullbackChart φ i) (frameUnit φ i i')
        * restrictFun (le_inf (le_trans inf_le_left inf_le_left) inf_le_right :
            ((⊤ : X.Opens) ⊓ pullbackChart φ i) ⊓ pullbackChart φ i' ≤ (⊤ : X.Opens) ⊓
              pullbackChart φ i')
          (restrictFun inf_le_right (frameUnit φ i' j))
theorem

twistXMul_mem

L569 ↗
AlgebraicGeometry.ProjSpace.twistXMul_mem
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
section GradedModuleOfTwist
variable (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem twistXMul_mem (π : X ⟶ Spec (.of A)) (j : Fin (N + 1)) (d : ℤ) (f : twistFam π φ) (hf : f
  ∈ twistGrade φ π d) :
    twistXMul φ π j f ∈ twistGrade φ π (d + 1)
theorem

twistXMul_comm

L601 ↗
AlgebraicGeometry.ProjSpace.twistXMul_comm
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem twistXMul_comm (π : X ⟶ Spec (.of A)) (j k : Fin (N + 1)) : twistXMul φ π j ∘ₗ twistXMul φ
  π k = twistXMul φ π k ∘ₗ twistXMul φ π j
def

twistGradedModule

L610 ↗
AlgebraicGeometry.ProjSpace.twistGradedModule
Documentation

The graded module of compatible projective-twist section families.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · full declaration
def twistGradedModule (π : X ⟶ Spec (.of A)) : ProjSpaceCech.GradedModule A N where
  M := twistFam π φ
  grade := twistGrade φ π
  xMul := twistXMul φ π
  xMul_mem_grade j d f hf := twistXMul_mem φ π j d f hf
  xMul_comm j k := twistXMul_comm φ π j k
theorem

twistGradedModule_M

L617 ↗
AlgebraicGeometry.ProjSpace.twistGradedModule_M
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem twistGradedModule_M (π : X ⟶ Spec (.of A)) : (twistGradedModule φ π).M = twistFam π φ
theorem

twistGradedModule_grade

L618 ↗
AlgebraicGeometry.ProjSpace.twistGradedModule_grade
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem twistGradedModule_grade (π : X ⟶ Spec (.of A)) (d : ℤ) : (twistGradedModule φ π).grade d =
  twistGrade φ π d
theorem

twistGradedModule_xMul

L620 ↗
AlgebraicGeometry.ProjSpace.twistGradedModule_xMul
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem twistGradedModule_xMul (π : X ⟶ Spec (.of A)) (j : Fin (N + 1)) : (twistGradedModule φ
  π).xMul j = twistXMul φ π j
def

twistGradeToObj

L624 ↗
AlgebraicGeometry.ProjSpace.twistGradeToObj
Documentation

The twist section obtained by evaluating a nonnegative homogeneous family.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
def twistGradeToObj (π : X ⟶ Spec (.of A)) {d : ℤ} (hd : 0 ≤ d) (f : twistFam π φ) (hf : f ∈
  twistGrade φ π d) : twistObj π φ d.toNat ⊤
theorem

twistGradeToObj_val

L628 ↗
AlgebraicGeometry.ProjSpace.twistGradeToObj_val
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem twistGradeToObj_val (π : X ⟶ Spec (.of A)) {d : ℤ} (hd : 0 ≤ d) (f : twistFam π φ)
  (hf : f ∈ twistGrade φ π d) :
    (twistGradeToObj φ π hd f hf).val = f d
def

objToTwistFam

L633 ↗
AlgebraicGeometry.ProjSpace.objToTwistFam
Documentation

The graded family supported in the degree of the given twist section.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
def objToTwistFam (π : X ⟶ Spec (.of A)) (m : ℕ) (g : twistObj π φ m ⊤) : twistFam π φ
theorem

objToTwistFam_mem

L636 ↗
AlgebraicGeometry.ProjSpace.objToTwistFam_mem
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem objToTwistFam_mem (π : X ⟶ Spec (.of A)) (m : ℕ) (g : twistObj π φ m ⊤) : objToTwistFam φ
  π m g ∈ twistGrade φ π m
theorem

isUnit_restrictFun_frameUnit

L651 ↗
AlgebraicGeometry.ProjSpace.isUnit_restrictFun_frameUnit
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem isUnit_restrictFun_frameUnit (i i' : Fin (N + 1)) :
    IsUnit (restrictFun (pullbackOverlap_le_left φ i i') (frameUnit φ i i'))
theorem

pullbackChart_eq_stdCoverPullback_U

L655 ↗
AlgebraicGeometry.ProjSpace.pullbackChart_eq_stdCoverPullback_U
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem pullbackChart_eq_stdCoverPullback_U [IsAffineHom φ] (i : Fin (N + 1)) :
    pullbackChart φ i = (ProjSpace.stdCoverPullback φ).U ⟨i⟩
theorem

isAffineOpen_pullbackChart

L658 ↗
AlgebraicGeometry.ProjSpace.isAffineOpen_pullbackChart
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem isAffineOpen_pullbackChart [IsAffineHom φ] (i : Fin (N + 1)) : IsAffineOpen (pullbackChart
  φ i)
theorem

isAffineOpen_pullbackOverlap

L662 ↗
AlgebraicGeometry.ProjSpace.isAffineOpen_pullbackOverlap
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem isAffineOpen_pullbackOverlap [IsAffineHom φ] (i i' : Fin (N + 1)) : IsAffineOpen
  (pullbackOverlap φ i i')
def

twistGradeEquiv

L677 ↗
AlgebraicGeometry.ProjSpace.twistGradeEquiv
Documentation

The linear equivalence between a nonnegative graded piece and twist sections.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · full declaration
def twistGradeEquiv (π : X ⟶ Spec (.of A)) {d : ℤ} (hd : 0 ≤ d) :
    twistGrade φ π d ≃ₗ[A] twistObj π φ d.toNat ⊤ where
  toFun f := twistGradeToObj φ π hd f.1 f.2
  invFun g := ⟨objToTwistFam φ π d.toNat g, by
    have h := objToTwistFam_mem φ π d.toNat g
    rwa [Int.toNat_of_nonneg hd] at h⟩
  map_add' f g := rfl
  map_smul' r f := by
    refine twistObj.ext (_root_.funext fun i => ?_)
    change (Scheme.TwoAffineOpenCover.algebraOfHom π ((⊤ : X.Opens) ⊓ pullbackChart φ
      i)).algebraMap r * f.1 d i
      = restrictFun inf_le_left ((Scheme.TwoAffineOpenCover.algebraOfHom π (⊤ :
        X.Opens)).algebraMap r) * f.1 d i
    rw [restrictFun_algebraMap' π]
  left_inv f := by
    apply Subtype.ext
    funext d'
    change (if d' = ((d.toNat : ℕ) : ℤ) then f.1 d else 0) = f.1 d'
    rw [Int.toNat_of_nonneg hd]
    split_ifs with h
    · rw [h]
    · exact (f.2.1 d' h).symm
  right_inv g := by
    refine twistObj.ext ?_
    change (if d = ((d.toNat : ℕ) : ℤ) then g.val else 0) = g.val
    rw [Int.toNat_of_nonneg hd, ite_eq_left rfl]
theorem

twistGradeEquiv_apply_val

L704 ↗
AlgebraicGeometry.ProjSpace.twistGradeEquiv_apply_val
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem twistGradeEquiv_apply_val (π : X ⟶ Spec (.of A)) {d : ℤ} (hd : 0 ≤ d) (f :
  twistGrade φ π d) :
    (twistGradeEquiv φ π hd f).val = f.1 d

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