Module

ProjSpace_exists_isFG_hom_injective_saturated_twistGradedModule.lean

Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_isFG_hom_injective_saturated_twistGradedModule

136 declarations indexed from sourceView source ↗

Module documentation

Proj Space exists is FG hom injective saturated twist Graded Module

Imports3

Imported by3

theorem

proj_basicOpen_awayMk

L53 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.proj_basicOpen_awayMk

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
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

theorem proj_basicOpen_awayMk (j : Fin (N + 1)) {d : ℕ}
    {g : MvPolynomial (Fin (N + 1)) A} (hg : g ∈ 𝒜 d) :
    (Proj 𝒜).basicOpen ((Proj.awayToSection 𝒜 (MvPolynomial.X j)).hom
        (HomogeneousLocalization.Away.mk 𝒜 (ProjSpace.X_mem_one A N j) d g (by simpa using hg)))
      = Proj.basicOpen 𝒜 ((MvPolynomial.X j : MvPolynomial (Fin (N + 1)) A) * g) := by
  set z := HomogeneousLocalization.Away.mk 𝒜 (ProjSpace.X_mem_one A N j) d g
    (by simpa using hg) with hz
  have hkey : ∀ (x : Proj 𝒜) (hxj : x ∈ Proj.basicOpen 𝒜 (MvPolynomial.X j)),
      IsUnit ((Proj 𝒜).presheaf.germ _ x hxj ((Proj.awayToSection 𝒜 (MvPolynomial.X j)).hom z)) ↔ g
        ∉ x.asHomogeneousIdeal := by
    intro x hxj
    have : x.asHomogeneousIdeal.toIdeal.IsPrime := x.isPrime
    have hxj' : (MvPolynomial.X j : MvPolynomial (Fin (N + 1)) A) ∈
      x.asHomogeneousIdeal.toIdeal.primeCompl := hxj
    have hgerm := congrArg (fun ψ => CommRingCat.Hom.hom ψ z)
      (ProjectiveSpectrum.Proj.awayToSection_germ 𝒜 (MvPolynomial.X j) x hxj)
    simp only [CommRingCat.hom_comp, RingHom.comp_apply, CommRingCat.hom_ofHom] at hgerm
    erw [hgerm]
    have : IsLocalHom (Proj.stalkIso' 𝒜 x).toCommRingCatIso.inv.hom := isLocalHom_of_isIso _
    refine (isUnit_map_iff (Proj.stalkIso' 𝒜 x).toCommRingCatIso.inv.hom _).trans ?_
    rw [← HomogeneousLocalization.isUnit_iff_isUnit_val]
    have hval : (HomogeneousLocalization.mapId 𝒜 (Submonoid.powers_le.mpr hxj') z).val
        = Localization.mk g ⟨(MvPolynomial.X j : MvPolynomial (Fin (N + 1)) A) ^ d, pow_mem hxj' d⟩
          := by
      simp only [hz, HomogeneousLocalization.Away.mk, HomogeneousLocalization.mapId]
      rfl
    rw [show Submonoid.powers_le.mpr hxj = Submonoid.powers_le.mpr hxj' from rfl, hval,
      Localization.mk_eq_mk', IsLocalization.AtPrime.isUnit_mk'_iff]
    exact Iff.rfl
  ext x
  simp only [SetLike.mem_coe, Proj.basicOpen_mul, Proj.mem_basicOpen, Opens.mem_inf]
  refine ⟨fun hx => ?_, fun ⟨hxj, hxg⟩ => ?_⟩
  · have hxj : x ∈ Proj.basicOpen 𝒜 (MvPolynomial.X j) := Scheme.basicOpen_le _ _ hx
    exact ⟨hxj, (hkey x hxj).mp ((Scheme.mem_basicOpen _ _ x hxj).mp hx)⟩
  · exact (Scheme.mem_basicOpen _ _ x hxj).mpr ((hkey x hxj).mpr hxg)

theorem

pullbackOverlap_eq_basicOpen

L89 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.pullbackOverlap_eq_basicOpen

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
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 pullbackOverlap_eq_basicOpen (i j : Fin (N + 1)) :
    pullbackOverlap φ i j = X.basicOpen (frameUnit φ i j)

theorem

inf_pullbackChart_eq_basicOpen

L99 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.inf_pullbackChart_eq_basicOpen

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
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 inf_pullbackChart_eq_basicOpen (i j : Fin (N + 1)) :
    pullbackChart φ i ⊓ pullbackChart φ j = X.basicOpen (frameUnit φ i j)

theorem

restrictFun_injective_of_eq

L124 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.restrictFun_injective_of_eq

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)

Lean source · statement

theorem restrictFun_injective_of_eq {V W : X.Opens} (hVW : V = W) :
    Function.Injective (restrictFun (le_of_eq hVW) : Γ(X, W) → Γ(X, V))

theorem

frameUnit_cocycle_of_le

L130 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.frameUnit_cocycle_of_le

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)

Lean source · statement

theorem frameUnit_cocycle_of_le {W : X.Opens} (i i' j : Fin (N + 1)) (hi : W ≤ pullbackChart φ i)
  (hi' : W ≤ pullbackChart φ i') :
    restrictFun hi (frameUnit φ i i') * restrictFun hi' (frameUnit φ i' j) = restrictFun hi
      (frameUnit φ i j)

theorem

frameUnit_mul_swap_of_le

L139 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.frameUnit_mul_swap_of_le

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)

Lean source · statement

theorem frameUnit_mul_swap_of_le {W : X.Opens} (i i' : Fin (N + 1)) (hi : W ≤ pullbackChart φ i)
  (hi' : W ≤ pullbackChart φ i') :
    restrictFun hi (frameUnit φ i i') * restrictFun hi' (frameUnit φ i' i) = 1

theorem

twistObj_eq_of_val_eq

L149 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.twistObj_eq_of_val_eq

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Chart
variable {U : X.Opens} {i₀ : Fin (N + 1)} (hU : U ≤ pullbackChart φ i₀)
include hU

Lean source · statement

theorem twistObj_eq_of_val_eq {g g' : twistObj π φ m U} (h : g.val i₀ = g'.val i₀) : g = g'

def

frameFamily

L165 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.frameFamily

Documentation

A section family obtained by multiplying a chosen chart section by transition functions.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Chart
variable {U : X.Opens} {i₀ : Fin (N + 1)} (hU : U ≤ pullbackChart φ i₀)
include hU

Lean source · statement

def frameFamily (h : Γ(X, U ⊓ pullbackChart φ i₀)) : ∀ i : Fin (N + 1), Γ(X, U ⊓ pullbackChart φ i)

theorem

frameFamily_compat

L170 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.frameFamily_compat

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Chart
variable {U : X.Opens} {i₀ : Fin (N + 1)} (hU : U ≤ pullbackChart φ i₀)
include hU

Lean source · statement

theorem frameFamily_compat (h : Γ(X, U ⊓ pullbackChart φ i₀)) : TwistCompat φ m U (frameFamily φ m
  hU h)

def

twistObjOfFun

L183 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.twistObjOfFun

Documentation

The twisted section determined by a section on the chosen chart.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Chart
variable {U : X.Opens} {i₀ : Fin (N + 1)} (hU : U ≤ pullbackChart φ i₀)
include hU

Lean source · statement

def twistObjOfFun (h : Γ(X, U ⊓ pullbackChart φ i₀)) : twistObj π φ m U

theorem

twistObjOfFun_val_self

L186 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.twistObjOfFun_val_self

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Chart
variable {U : X.Opens} {i₀ : Fin (N + 1)} (hU : U ≤ pullbackChart φ i₀)
include hU

Lean source · statement

theorem twistObjOfFun_val_self (h : Γ(X, U ⊓ pullbackChart φ i₀)) : (twistObjOfFun φ π m hU h).val
  i₀ = h

theorem

twistObjOfFun_val

L191 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.twistObjOfFun_val

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Chart
variable {U : X.Opens} {i₀ : Fin (N + 1)} (hU : U ≤ pullbackChart φ i₀)
include hU

Lean source · statement

theorem twistObjOfFun_val (h : Γ(X, U ⊓ pullbackChart φ i₀)) (i : Fin (N + 1)) :
    (twistObjOfFun φ π m hU h).val i
      = restrictFun inf_le_right (frameUnit φ i i₀) ^ m * restrictFun (le_inf inf_le_left (le_trans
        inf_le_left hU)) h

theorem

twistObjOfFun_val_eq

L196 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.twistObjOfFun_val_eq

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Chart
variable {U : X.Opens} {i₀ : Fin (N + 1)} (hU : U ≤ pullbackChart φ i₀)
include hU

Lean source · statement

theorem twistObjOfFun_val_eq (g : twistObj π φ m U) : twistObjOfFun φ π m hU (g.val i₀) = g

theorem

val_self_injective

L199 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.val_self_injective

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Chart
variable {U : X.Opens} {i₀ : Fin (N + 1)} (hU : U ≤ pullbackChart φ i₀)
include hU

Lean source · full declaration

theorem val_self_injective : Function.Injective fun g : twistObj π φ m U => g.val i₀ :=
  fun _ _ h => twistObj_eq_of_val_eq φ π m hU h

theorem

val_self_surjective

L202 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.val_self_surjective

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Chart
variable {U : X.Opens} {i₀ : Fin (N + 1)} (hU : U ≤ pullbackChart φ i₀)
include hU

Lean source · full declaration

theorem val_self_surjective : Function.Surjective fun g : twistObj π φ m U => g.val i₀ :=
  fun h => ⟨twistObjOfFun φ π m hU h, twistObjOfFun_val_self φ π m hU h⟩

theorem

twistObjOfFun_add

L205 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.twistObjOfFun_add

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Chart
variable {U : X.Opens} {i₀ : Fin (N + 1)} (hU : U ≤ pullbackChart φ i₀)
include hU

Lean source · statement

theorem twistObjOfFun_add (h h' : Γ(X, U ⊓ pullbackChart φ i₀)) :
    twistObjOfFun φ π m hU (h + h') = twistObjOfFun φ π m hU h + twistObjOfFun φ π m hU h'

theorem

twistObjOfFun_smul

L211 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.twistObjOfFun_smul

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Chart
variable {U : X.Opens} {i₀ : Fin (N + 1)} (hU : U ≤ pullbackChart φ i₀)
include hU

Lean source · statement

theorem twistObjOfFun_smul (a : Γ(X, U)) (h : Γ(X, U ⊓ pullbackChart φ i₀)) :
    twistObjOfFun φ π m hU (restrictFun inf_le_left a * h) = a • twistObjOfFun φ π m hU h

def

interI

L240 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.interI

Documentation

The intersection of a finite family of projective charts.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
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 interI (I : Finset (Fin (N + 1))) : X.Opens

theorem

interI_le

L242 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.interI_le

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
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 interI_le {I : Finset (Fin (N + 1))} {i : Fin (N + 1)} (hi : i ∈ I) : interI φ I ≤
  pullbackChart φ i

theorem

interI_anti

L246 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.interI_anti

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
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 interI_anti {I J : Finset (Fin (N + 1))} (h : I ⊆ J) : interI φ J ≤ interI φ I

def

frameProd

L250 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.frameProd

Documentation

The product of transition functions on a chart.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
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 frameProd (I : Finset (Fin (N + 1))) (i₀ : Fin (N + 1)) : Γ(X, pullbackChart φ i₀)

theorem

pullbackChart_inf_interI_eq_basicOpen

L253 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.pullbackChart_inf_interI_eq_basicOpen

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
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_inf_interI_eq_basicOpen (K : Finset (Fin (N + 1))) (i₀ : Fin (N + 1)) :
    pullbackChart φ i₀ ⊓ interI φ K = X.basicOpen (frameProd φ K i₀)

theorem

interI_eq_basicOpen

L267 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.interI_eq_basicOpen

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
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 interI_eq_basicOpen {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I) :
    interI φ I = X.basicOpen (frameProd φ I i₀)

theorem

interI_le_basicOpen

L272 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.interI_le_basicOpen

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
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 interI_le_basicOpen {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I) :
    interI φ I ≤ X.basicOpen (frameProd φ I i₀)

theorem

basicOpen_le_interI

L275 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.basicOpen_le_interI

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
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 basicOpen_le_interI {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I) :
    X.basicOpen (frameProd φ I i₀) ≤ interI φ I

theorem

isAffineOpen_interI

L278 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.isAffineOpen_interI

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
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_interI [IsAffineHom φ] {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀
  ∈ I) :
    IsAffineOpen (interI φ I)

abbrev

uTop

L306 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.uTop

Documentation

The transition function restricted from the whole scheme.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))

Lean source · statement

abbrev uTop (i j : Fin (N + 1)) : Γ(X, (⊤ : X.Opens) ⊓ pullbackChart φ i)

theorem

D_xMul_apply

L309 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.D_xMul_apply

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))

Lean source · statement

theorem D_xMul_apply (j : Fin (N + 1)) (f : (twistGradedModule φ π).M) (d : ℤ) (i : Fin (N + 1)) :
    ((twistGradedModule φ π).xMul j f) d i = uTop φ i j * f (d - 1) i

theorem

twistXMul_pow_apply

L312 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.twistXMul_pow_apply

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))

Lean source · statement

theorem twistXMul_pow_apply (j : Fin (N + 1)) (k : ℕ) (f : (twistGradedModule φ π).M) (d : ℤ) (i :
  Fin (N + 1)) :
    (((twistGradedModule φ π).xMul j ^ k) f) d i = uTop φ i j ^ k * f (d - k) i

theorem

twistMonMul_apply

L322 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.twistMonMul_apply

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))

Lean source · statement

theorem twistMonMul_apply (b : Fin (N + 1) → ℕ) (f : (twistGradedModule φ π).M) (d : ℤ) (i : Fin (N
  + 1)) :
    (ProjSpaceCech.GradedModule.monMul (twistGradedModule φ π) b f) d i
      = (∏ j, uTop φ i j ^ b j) * f (d - ∑ j, (b j : ℤ)) i

theorem

twistMonMul_shift_apply

L367 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.twistMonMul_shift_apply

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)

Lean source · statement

theorem twistMonMul_shift_apply (k : ℤ) (b : Fin (N + 1) → ℕ) (f : ((twistGradedModule φ π).shift
  k).M) (d : ℤ) (i : Fin (N + 1)) :
    (ProjSpaceCech.GradedModule.monMul ((twistGradedModule φ π).shift k) b f) d i
      = (∏ j, uTop φ i j ^ b j) * f (d - ∑ j, (b j : ℤ)) i

abbrev

Wop

L378 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.Wop

Documentation

The intersection with the distinguished chart.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Psi
variable {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)

Lean source · statement

abbrev Wop (I : Finset (Fin (N + 1))) (i₀ : Fin (N + 1)) : X.Opens

theorem

Wop_le_top

L381 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.Wop_le_top

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Psi
variable {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)

Lean source · statement

theorem Wop_le_top : Wop φ I i₀ ≤ (⊤ : X.Opens) ⊓ pullbackChart φ i₀

theorem

Wop_le_self

L382 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.Wop_le_self

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Psi
variable {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)

Lean source · statement

theorem Wop_le_self : Wop φ I i₀ ≤ pullbackChart φ i₀

theorem

Wop_le_chart

L383 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.Wop_le_chart

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Psi
variable {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)

Lean source · statement

theorem Wop_le_chart {j : Fin (N + 1)} (hj : j ∈ I) : Wop φ I i₀ ≤ pullbackChart φ j

def

invProd

L387 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.invProd

Documentation

The product of inverse transition factors for a denominator.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Psi
variable {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)

Lean source · statement

def invProd (I : Finset (Fin (N + 1))) (i₀ : Fin (N + 1)) (a : Fin (N + 1) → ℕ) : Γ(X, Wop φ I i₀)

def

dirProd

L392 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.dirProd

Documentation

The product of direct transition factors for a denominator.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Psi
variable {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)

Lean source · statement

def dirProd (I : Finset (Fin (N + 1))) (i₀ : Fin (N + 1)) (a : Fin (N + 1) → ℕ) : Γ(X, Wop φ I i₀)

theorem

dirProd_mul_invProd

L396 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.dirProd_mul_invProd

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Psi
variable {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)

Lean source · statement

theorem dirProd_mul_invProd (a : Fin (N + 1) → ℕ) : dirProd φ I i₀ a * invProd φ I i₀ a = 1

theorem

invProd_add

L402 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.invProd_add

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Psi
variable {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)

Lean source · statement

theorem invProd_add (a b : Fin (N + 1) → ℕ) : invProd φ I i₀ (a + b) = invProd φ I i₀ a * invProd φ
  I i₀ b

theorem

dirProd_add

L408 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.dirProd_add

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Psi
variable {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)

Lean source · statement

theorem dirProd_add (a b : Fin (N + 1) → ℕ) : dirProd φ I i₀ (a + b) = dirProd φ I i₀ a * dirProd φ
  I i₀ b

theorem

restrictFun_prod_uTop

L414 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.restrictFun_prod_uTop

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Psi
variable {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)

Lean source · statement

theorem restrictFun_prod_uTop {a : Fin (N + 1) → ℕ} (ha : ∀ j ∉ I, a j = 0) :
    restrictFun (Wop_le_top φ) (∏ j, uTop φ i₀ j ^ a j) = dirProd φ I i₀ a

def

PsiNum

L427 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.PsiNum

Documentation

The local section associated to a homogeneous fraction.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Psi
variable {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)

Lean source · statement

def PsiNum (x : ProjSpaceCech.GradedModule.Frac ((twistGradedModule φ π).shift m) I) : Γ(X, Wop φ I
  i₀)

theorem

PsiNum_eq_of_rel

L431 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.PsiNum_eq_of_rel

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Psi
variable {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)

Lean source · statement

theorem PsiNum_eq_of_rel {x y : ProjSpaceCech.GradedModule.Frac ((twistGradedModule φ π).shift m) I}
    (h : ProjSpaceCech.GradedModule.Frac.Rel ((twistGradedModule φ π).shift m) I x y) :
    PsiNum φ π m (i₀ := i₀) x = PsiNum φ π m y

theorem

PsiNum_add_repr

L492 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.PsiNum_add_repr

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Psi
variable {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)}

Lean source · statement

theorem PsiNum_add_repr (x y : ProjSpaceCech.GradedModule.Frac ((twistGradedModule φ π).shift (m :
  ℤ)) I)
    (hnum : ProjSpaceCech.GradedModule.monMul ((twistGradedModule φ π).shift (m : ℤ)) y.denExp
      x.num + ProjSpaceCech.GradedModule.monMul ((twistGradedModule φ π).shift (m : ℤ)) x.denExp
      y.num
      ∈ ((twistGradedModule φ π).shift (m : ℤ)).grade (∑ j, ((x.denExp + y.denExp) j : ℤ))) :
    PsiNum φ π m (i₀ := i₀) ⟨x.denExp + y.denExp, ProjSpaceCech.GradedModule.Frac.supp_add I x.hden
      y.hden,
        ProjSpaceCech.GradedModule.monMul ((twistGradedModule φ π).shift (m : ℤ)) y.denExp x.num +
          ProjSpaceCech.GradedModule.monMul ((twistGradedModule φ π).shift (m : ℤ)) x.denExp y.num,
          hnum⟩
      = PsiNum φ π m x + PsiNum φ π m y

theorem

PsiNum_smul_repr

L540 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.PsiNum_smul_repr

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Psi
variable {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)}

Lean source · statement

theorem PsiNum_smul_repr (r : A) (x : ProjSpaceCech.GradedModule.Frac ((twistGradedModule φ
  π).shift (m : ℤ)) I) :
    PsiNum φ π m (i₀ := i₀) ⟨x.denExp, x.hden, r • x.num, Submodule.smul_mem _ r x.hnum⟩
      = (Scheme.TwoAffineOpenCover.algebraOfHom π (Wop φ I i₀)).algebraMap r * PsiNum φ π m x

def

PsiFun

L579 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.PsiFun

Documentation

Evaluation of a localized graded section on the distinguished chart.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Psi
variable {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)

Lean source · statement

def PsiFun : ProjSpaceCech.GradedModule.sec ((twistGradedModule φ π).shift (m : ℤ)) I → Γ(X, Wop φ
  I i₀)

theorem

PsiFun_mk

L583 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.PsiFun_mk

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Psi
variable {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)

Lean source · statement

theorem PsiFun_mk (x : ProjSpaceCech.GradedModule.Frac ((twistGradedModule φ π).shift (m : ℤ)) I) :
    PsiFun φ π m (i₀ := i₀) (ProjSpaceCech.GradedModule.sec.mk _ I x) = PsiNum φ π m x

theorem

PsiFun_add

L586 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.PsiFun_add

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Psi
variable {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)

Lean source · statement

theorem PsiFun_add (s t : ProjSpaceCech.GradedModule.sec ((twistGradedModule φ π).shift (m : ℤ)) I)
  :
    PsiFun φ π m (i₀ := i₀) (s + t) = PsiFun φ π m s + PsiFun φ π m t

theorem

PsiFun_smul

L594 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.PsiFun_smul

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Psi
variable {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)

Lean source · statement

theorem PsiFun_smul (r : A) (s : ProjSpaceCech.GradedModule.sec ((twistGradedModule φ π).shift (m :
  ℤ)) I) :
    PsiFun φ π m (i₀ := i₀) (r • s) = (Scheme.TwoAffineOpenCover.algebraOfHom π (Wop φ I
      i₀)).algebraMap r * PsiFun φ π m s

def

Psi

L603 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.Psi

Documentation

The linear comparison from localized graded sections to twisted sections.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Psi
variable {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)
include hi₀ in

Lean source · full declaration

def Psi : ProjSpaceCech.GradedModule.sec ((twistGradedModule φ π).shift (m : ℤ)) I →ₗ[A] twistObj π
  φ m (interI φ I) where
  toFun s := twistObjOfFun φ π m (interI_le φ hi₀) (PsiFun φ π m s)
  map_add' s t := by rw [PsiFun_add, twistObjOfFun_add]
  map_smul' r s := by
    rw [PsiFun_smul, RingHom.id_apply, twistObj.algebraMap_smul, ← twistObjOfFun_smul]
    congr 1
    rw [restrictFun_algebraMap' π]

theorem

Psi_val_self

L612 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.Psi_val_self

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Psi
variable {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)

Lean source · statement

theorem Psi_val_self (s : ProjSpaceCech.GradedModule.sec ((twistGradedModule φ π).shift (m : ℤ)) I)
  :
    (Psi φ π m hi₀ s).val i₀ = PsiFun φ π m s

theorem

Psi_mk_val_self

L617 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.Psi_mk_val_self

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Psi
variable {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)

Lean source · statement

theorem Psi_mk_val_self (x : ProjSpaceCech.GradedModule.Frac ((twistGradedModule φ π).shift (m :
  ℤ)) I) :
    (Psi φ π m hi₀ (ProjSpaceCech.GradedModule.sec.mk _ I x)).val i₀ = PsiNum φ π m x

theorem

exists_pow_mul_eq_zero_of_restrict_basicOpen

L645 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.exists_pow_mul_eq_zero_of_restrict_basicOpen

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)

Lean source · statement

theorem exists_pow_mul_eq_zero_of_restrict_basicOpen {V : X.Opens} (hV : IsAffineOpen V) (g s :
  Γ(X, V))
    (hs : restrictFun (X.basicOpen_le g) s = 0) : ∃ n : ℕ, g ^ n * s = 0

theorem

exists_pow_mul_eq_zero_of_restrict

L655 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.exists_pow_mul_eq_zero_of_restrict

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)

Lean source · statement

theorem exists_pow_mul_eq_zero_of_restrict {V O : X.Opens} (hV : IsAffineOpen V) (g s : Γ(X, V))
  (hOV : O ≤ V)
    (hgO : X.basicOpen g ≤ O) (hs : restrictFun hOV s = 0) : ∃ n : ℕ, g ^ n * s = 0

theorem

isAffineOpen_top_inf_pullbackChart

L662 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.isAffineOpen_top_inf_pullbackChart

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)

Lean source · statement

theorem isAffineOpen_top_inf_pullbackChart [IsAffineHom φ] (i : Fin (N + 1)) :
    IsAffineOpen ((⊤ : X.Opens) ⊓ pullbackChart φ i)

theorem

stepA

L671 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.stepA

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Inj
variable [IsAffineHom φ] {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)
include hi₀

Lean source · statement

theorem stepA (t : Γ(X, (⊤ : X.Opens) ⊓ pullbackChart φ i₀)) (ht : restrictFun (Wop_le_top φ (I :=
  I)) t = 0) :
    ∃ n : ℕ, restrictFun inf_le_right (frameProd φ I i₀) ^ n * t = 0

theorem

stepB_restrict

L684 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.stepB_restrict

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Inj
variable [IsAffineHom φ] {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)
include hi₀
omit [IsAffineHom φ] hi₀ in

Lean source · statement

theorem stepB_restrict (e : ℕ) (g : ∀ i, Γ(X, (⊤ : X.Opens) ⊓ pullbackChart φ i)) (hg : TwistCompat
  φ e ⊤ g)
    (n : ℕ) (i : Fin (N + 1)) :
    restrictFun (inf_le_left : ((⊤ : X.Opens) ⊓ pullbackChart φ i) ⊓ pullbackChart φ i₀ ≤ (⊤ :
      X.Opens) ⊓ pullbackChart φ i)
        ((∏ j ∈ I, uTop φ i j ^ n) * g i)
      = restrictFun (inf_le_left.trans inf_le_right : ((⊤ : X.Opens) ⊓ pullbackChart φ i) ⊓
        pullbackChart φ i₀ ≤ pullbackChart φ i)
          (frameUnit φ i i₀) ^ (n * I.card + e)
        * restrictFun (le_inf (inf_le_left.trans inf_le_left) inf_le_right :
            ((⊤ : X.Opens) ⊓ pullbackChart φ i) ⊓ pullbackChart φ i₀ ≤ (⊤ : X.Opens) ⊓
              pullbackChart φ i₀)
          (restrictFun inf_le_right (frameProd φ I i₀) ^ n * g i₀)

theorem

stepB

L712 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.stepB

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Inj
variable [IsAffineHom φ] {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)
include hi₀
omit hi₀ in

Lean source · statement

theorem stepB (e : ℕ) (g : ∀ i, Γ(X, (⊤ : X.Opens) ⊓ pullbackChart φ i)) (hg : TwistCompat φ e ⊤ g)
  (n : ℕ)
    (hkill : restrictFun inf_le_right (frameProd φ I i₀) ^ n * g i₀ = 0) (i : Fin (N + 1)) :
    ∃ k : ℕ, uTop φ i i₀ ^ k * ((∏ j ∈ I, uTop φ i j ^ n) * g i) = 0

theorem

stepC

L747 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.stepC

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Inj2
variable [IsAffineHom φ] {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)
include hi₀

Lean source · statement

theorem stepC (a : Fin (N + 1) → ℕ) (f : ((twistGradedModule φ π).shift (m : ℤ)).M)
    (hf : f ∈ ((twistGradedModule φ π).shift (m : ℤ)).grade (∑ j, (a j : ℤ)))
    (hW : restrictFun (Wop_le_top φ (I := I)) (f ((∑ j, (a j : ℤ)) + m) i₀) = 0) :
    ∃ c : Fin (N + 1) → ℕ, (∀ j ∉ I, c j = 0) ∧
      ProjSpaceCech.GradedModule.monMul ((twistGradedModule φ π).shift (m : ℤ)) c f = 0

theorem

Psi_injective

L781 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.Psi_injective

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Inj2
variable [IsAffineHom φ] {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)
include hi₀

Lean source · statement

theorem Psi_injective : Function.Injective (Psi φ π m hi₀ (I := I))

theorem

exists_extend_of_affine

L826 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.exists_extend_of_affine

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)

Lean source · statement

theorem exists_extend_of_affine {V O : X.Opens} (hV : IsAffineOpen V) (g : Γ(X, V)) (_hOV : O ≤ V)
  (hgO : X.basicOpen g ≤ O)
    (s : Γ(X, O)) : ∃ (n : ℕ) (t : Γ(X, V)),
      restrictFun (X.basicOpen_le g) t = restrictFun (X.basicOpen_le g) g ^ n * restrictFun hgO s

theorem

restrictFun_self

L838 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.restrictFun_self

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)

Lean source · statement

theorem restrictFun_self {W : X.Opens} (h : W ≤ W) (x : Γ(X, W)) : restrictFun h x = x

theorem

basicOpen_frameProd_le_Wop

L847 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.basicOpen_frameProd_le_Wop

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Surj
variable [IsAffineHom φ] {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)
include hi₀
omit [IsAffineHom φ] in

Lean source · statement

theorem basicOpen_frameProd_le_Wop :
    X.basicOpen (restrictFun (inf_le_right : (⊤ : X.Opens) ⊓ pullbackChart φ i₀ ≤ pullbackChart φ
      i₀) (frameProd φ I i₀)) ≤ Wop φ I i₀

theorem

Wop_le_basicOpen_frameProd

L858 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.Wop_le_basicOpen_frameProd

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Surj
variable [IsAffineHom φ] {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)
include hi₀
omit [IsAffineHom φ] in

Lean source · statement

theorem Wop_le_basicOpen_frameProd :
    Wop φ I i₀ ≤ X.basicOpen (restrictFun (inf_le_right : (⊤ : X.Opens) ⊓ pullbackChart φ i₀ ≤
      pullbackChart φ i₀) (frameProd φ I i₀))

theorem

surj_step1

L868 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.surj_step1

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Surj
variable [IsAffineHom φ] {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)
include hi₀

Lean source · statement

theorem surj_step1 (h : Γ(X, Wop φ I i₀)) : ∃ (n : ℕ) (t : Γ(X, (⊤ : X.Opens) ⊓ pullbackChart φ
  i₀)),
    restrictFun (Wop_le_top φ) t = restrictFun (Wop_le_top φ) (restrictFun inf_le_right (frameProd
      φ I i₀)) ^ n * h

theorem

surj_step2

L882 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.surj_step2

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Surj
variable [IsAffineHom φ] {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)
include hi₀
omit hi₀ in

Lean source · statement

theorem surj_step2 (e₁ : ℕ) (t : Γ(X, (⊤ : X.Opens) ⊓ pullbackChart φ i₀)) (i : Fin (N + 1)) :
    ∃ (k : ℕ) (f : Γ(X, (⊤ : X.Opens) ⊓ pullbackChart φ i)),
      restrictFun (inf_le_left : ((⊤ : X.Opens) ⊓ pullbackChart φ i) ⊓ pullbackChart φ i₀ ≤ (⊤ :
        X.Opens) ⊓ pullbackChart φ i) f
        = restrictFun (inf_le_left.trans inf_le_right : ((⊤ : X.Opens) ⊓ pullbackChart φ i) ⊓
          pullbackChart φ i₀ ≤ pullbackChart φ i)
            (frameUnit φ i i₀) ^ (k + e₁)
          * restrictFun (le_inf (inf_le_left.trans inf_le_left) inf_le_right :
              ((⊤ : X.Opens) ⊓ pullbackChart φ i) ⊓ pullbackChart φ i₀ ≤ (⊤ : X.Opens) ⊓
                pullbackChart φ i₀) t

theorem

isAffineOpen_topChart_inf

L936 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.isAffineOpen_topChart_inf

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)

Lean source · statement

theorem isAffineOpen_topChart_inf [IsAffineHom φ] (i j : Fin (N + 1)) :
    IsAffineOpen (((⊤ : X.Opens) ⊓ pullbackChart φ i) ⊓ pullbackChart φ j)

abbrev

Vt

L945 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.Vt

Documentation

The chart restricted from the whole scheme.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Surj3
variable {i₀ : Fin (N + 1)}

Lean source · statement

abbrev Vt (i : Fin (N + 1)) : X.Opens

abbrev

Ot

L947 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.Ot

Documentation

The overlap of two charts restricted from the whole scheme.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Surj3
variable {i₀ : Fin (N + 1)}

Lean source · statement

abbrev Ot (i i' : Fin (N + 1)) : X.Opens

theorem

Ot_le_Vt

L949 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.Ot_le_Vt

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Surj3
variable {i₀ : Fin (N + 1)}

Lean source · statement

theorem Ot_le_Vt (i i' : Fin (N + 1)) : Ot φ i i' ≤ Vt φ i

theorem

Ot_le_chart_left

L950 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.Ot_le_chart_left

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Surj3
variable {i₀ : Fin (N + 1)}

Lean source · statement

theorem Ot_le_chart_left (i i' : Fin (N + 1)) : Ot φ i i' ≤ pullbackChart φ i

theorem

Ot_le_chart_right

L952 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.Ot_le_chart_right

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Surj3
variable {i₀ : Fin (N + 1)}

Lean source · statement

theorem Ot_le_chart_right (i i' : Fin (N + 1)) : Ot φ i i' ≤ pullbackChart φ i'

theorem

Ot_le_Vt_right

L953 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.Ot_le_Vt_right

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Surj3
variable {i₀ : Fin (N + 1)}

Lean source · statement

theorem Ot_le_Vt_right (i i' : Fin (N + 1)) : Ot φ i i' ≤ Vt φ i'

theorem

surj_step3a

L956 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.surj_step3a

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Surj3
variable {i₀ : Fin (N + 1)}

Lean source · statement

theorem surj_step3a [IsAffineHom φ] (E : ℕ) (t : Γ(X, Vt φ i₀)) (F : ∀ i, Γ(X, Vt φ i))
    (hF : ∀ i, restrictFun (Ot_le_Vt φ i i₀) (F i)
      = restrictFun (Ot_le_chart_left φ i i₀) (frameUnit φ i i₀) ^ E * restrictFun (Ot_le_Vt_right
        φ i i₀) t)
    (i j : Fin (N + 1)) :
    ∃ r : ℕ, restrictFun (Ot_le_Vt φ i j) (uTop φ i i₀) ^ r
      * (restrictFun (Ot_le_Vt φ i j) (F i)
          - restrictFun (Ot_le_chart_left φ i j) (frameUnit φ i j) ^ E * restrictFun
            (Ot_le_Vt_right φ i j) (F j)) = 0

theorem

surj_step3b

L985 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.surj_step3b

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Surj3
variable {i₀ : Fin (N + 1)}

Lean source · full declaration

theorem surj_step3b [IsAffineHom φ] (E : ℕ) (t : Γ(X, Vt φ i₀)) (F : ∀ i, Γ(X, Vt φ i))
    (hF : ∀ i, restrictFun (Ot_le_Vt φ i i₀) (F i)
      = restrictFun (Ot_le_chart_left φ i i₀) (frameUnit φ i i₀) ^ E * restrictFun (Ot_le_Vt_right
        φ i i₀) t) :
    ∃ R : ℕ, TwistCompat φ (R + E) ⊤ (fun i => uTop φ i i₀ ^ R * F i) := by
  classical
  choose r hr using fun p : Fin (N + 1) × Fin (N + 1) => surj_step3a φ E t F hF p.1 p.2
  refine ⟨Finset.univ.sup r, fun i j => ?_⟩
  have hRij : r (i, j) ≤ Finset.univ.sup r := Finset.le_sup (f := r) (Finset.mem_univ (i, j))
  have key := hr (i, j)
  simp only at key
  have key' := congrArg (fun z => restrictFun (Ot_le_Vt φ i j) (uTop φ i i₀) ^ (Finset.univ.sup r -
    r (i, j)) * z) key
  simp only [mul_zero, ← mul_assoc, ← pow_add, Nat.sub_add_cancel hRij, mul_sub] at key'
  change restrictFun _ (uTop φ i i₀ ^ Finset.univ.sup r * F i)
    = restrictFun _ (frameUnit φ i j) ^ (Finset.univ.sup r + E) * restrictFun _ (uTop φ j i₀ ^
      Finset.univ.sup r * F j)
  rw [map_mul, map_pow, map_mul, map_pow]
  rw [sub_eq_zero] at key'
  rw [key', pow_add]
  have hc := frameUnit_cocycle_of_le φ i j i₀ (Ot_le_chart_left φ i j) (Ot_le_chart_right φ i j)
  have hu : restrictFun (Ot_le_Vt_right φ i j) (uTop φ j i₀) = restrictFun (Ot_le_chart_right φ i
    j) (frameUnit φ j i₀) := by
    simp only [uTop, restrictFun_restrictFun]
  have hu' : restrictFun (Ot_le_Vt φ i j) (uTop φ i i₀) = restrictFun (Ot_le_chart_left φ i j)
    (frameUnit φ i i₀) := by
    simp only [uTop, restrictFun_restrictFun]
  rw [hu, hu', ← hc]
  ring

theorem

invProd_single_self

L1038 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.invProd_single_self

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Surj4
variable [IsAffineHom φ] {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)
include hi₀
omit [IsAffineHom φ] hi₀ in

Lean source · statement

theorem invProd_single_self (M : ℕ) : invProd φ I i₀ (Pi.single i₀ M) = 1

theorem

restrictFun_frameProd_pow

L1049 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.restrictFun_frameProd_pow

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Surj4
variable [IsAffineHom φ] {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)
include hi₀
omit [IsAffineHom φ] hi₀ in

Lean source · full declaration

theorem restrictFun_frameProd_pow (n : ℕ) :
    restrictFun (Wop_le_top φ) (restrictFun (inf_le_right : (⊤ : X.Opens) ⊓ pullbackChart φ i₀ ≤
      pullbackChart φ i₀) (frameProd φ I i₀)) ^ n
      = dirProd φ I i₀ (fun j => if j ∈ I then n else 0) := by
  classical
  rw [restrictFun_restrictFun, frameProd, map_prod, ← Finset.prod_attach I, ← Finset.prod_pow,
    dirProd]
  refine Finset.prod_congr rfl fun j _ => ?_
  rw [ite_eq_left j.2]

theorem

PsiNum_surjective

L1059 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.PsiNum_surjective

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Surj4
variable [IsAffineHom φ] {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)
include hi₀

Lean source · statement

theorem PsiNum_surjective (h : Γ(X, Wop φ I i₀)) :
    ∃ x : ProjSpaceCech.GradedModule.Frac ((twistGradedModule φ π).shift (m : ℤ)) I, PsiNum φ π m
      (i₀ := i₀) x = h

theorem

Psi_surjective

L1118 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.Psi_surjective

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Surj4
variable [IsAffineHom φ] {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)
include hi₀

Lean source · statement

theorem Psi_surjective : Function.Surjective (Psi φ π m hi₀ (I := I))

theorem

Psi_bijective

L1125 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.Psi_bijective

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section Surj4
variable [IsAffineHom φ] {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)
include hi₀

Lean source · statement

theorem Psi_bijective : Function.Bijective (Psi φ π m hi₀ (I := I))

def

evalLin

L1148 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.ProjSpaceCech.GradedModule.evalLin

Documentation

Polynomial evaluation using the commuting graded multiplication operators.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
namespace GradedModule
open _root_.ProjSpaceCech.GradedModule
open _root_.ProjSpaceCech.GradedModule
open _root_.ProjSpaceCech
variable {R : Type u} [CommRing R] {n : ℕ} (D : GradedModule R n)

Lean source · statement

def evalLin (v : D.M) : MvPolynomial (Fin (n + 1)) R →ₗ[R] D.M

theorem

evalLin_monomial

L1152 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.ProjSpaceCech.GradedModule.evalLin_monomial

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
namespace GradedModule
open _root_.ProjSpaceCech.GradedModule
open _root_.ProjSpaceCech.GradedModule
open _root_.ProjSpaceCech
variable {R : Type u} [CommRing R] {n : ℕ} (D : GradedModule R n)

Lean source · statement

theorem evalLin_monomial (v : D.M) (e : Fin (n + 1) →₀ ℕ) (r : R) :
    evalLin D v (monomial e r) = r • GradedModule.monMul D (⇑e) v

theorem

evalLin_X_mul

L1159 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.ProjSpaceCech.GradedModule.evalLin_X_mul

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
namespace GradedModule
open _root_.ProjSpaceCech.GradedModule
open _root_.ProjSpaceCech.GradedModule
open _root_.ProjSpaceCech
variable {R : Type u} [CommRing R] {n : ℕ} (D : GradedModule R n)

Lean source · statement

theorem evalLin_X_mul (v : D.M) (j : Fin (n + 1)) (p : MvPolynomial (Fin (n + 1)) R) :
    evalLin D v (X j * p) = D.xMul j (evalLin D v p)

theorem

evalLin_mem_grade

L1175 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.ProjSpaceCech.GradedModule.evalLin_mem_grade

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
namespace GradedModule
open _root_.ProjSpaceCech.GradedModule
open _root_.ProjSpaceCech.GradedModule
open _root_.ProjSpaceCech
variable {R : Type u} [CommRing R] {n : ℕ} (D : GradedModule R n)

Lean source · statement

theorem evalLin_mem_grade {a : ℤ} {v : D.M} (hv : v ∈ D.grade a) {d : ℤ} {p : MvPolynomial (Fin (n
  + 1)) R}
    (hp : p ∈ (GradedModule.FD R n (-a)).grade d) : evalLin D v p ∈ D.grade d

def

evalHom

L1204 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.ProjSpaceCech.GradedModule.evalHom

Documentation

The graded morphism determined by a homogeneous element.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
namespace GradedModule
open _root_.ProjSpaceCech.GradedModule
open _root_.ProjSpaceCech.GradedModule
open _root_.ProjSpaceCech
variable {R : Type u} [CommRing R] {n : ℕ} (D : GradedModule R n)

Lean source · full declaration

def evalHom {a : ℤ} (v : D.M) (hv : v ∈ D.grade a) : GradedModule.Hom (GradedModule.FD R n (-a)) D
  where
  toLinearMap := evalLin D v
  mem_grade _d _p hp := evalLin_mem_grade D hv hp
  xMul_comm j := LinearMap.ext fun p => evalLin_X_mul D v j p

theorem

evalHom_one

L1210 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.ProjSpaceCech.GradedModule.evalHom_one

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
namespace GradedModule
open _root_.ProjSpaceCech.GradedModule
open _root_.ProjSpaceCech.GradedModule
open _root_.ProjSpaceCech
variable {R : Type u} [CommRing R] {n : ℕ} (D : GradedModule R n)

Lean source · statement

theorem evalHom_one {a : ℤ} (v : D.M) (hv : v ∈ D.grade a) :
    (evalHom D v hv).toLinearMap (1 : MvPolynomial (Fin (n + 1)) R) = v

def

monMulFrac

L1245 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.monMulFrac

Documentation

Multiplication of a homogeneous fraction by a monomial.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section MonMul
variable [IsAffineHom φ] {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)
include hi₀

Lean source · full declaration

def monMulFrac (c : Fin (N + 1) → ℕ) (x : ProjSpaceCech.GradedModule.Frac ((twistGradedModule φ
  π).shift (m : ℤ)) I) :
    ProjSpaceCech.GradedModule.Frac ((twistGradedModule φ π).shift (m : ℤ)) I where
  denExp := x.denExp + Pi.single i₀ (∑ l, c l)
  hden j hj := by
    have : j ≠ i₀ := fun h => hj (h ▸ hi₀)
    simp [Pi.add_apply, x.hden j hj, this]
  num := ProjSpaceCech.GradedModule.monMul ((twistGradedModule φ π).shift (m : ℤ)) c x.num
  hnum := by
    have h := ProjSpaceCech.GradedModule.monMul_mem_grade ((twistGradedModule φ π).shift (m : ℤ)) c
      _ x.num x.hnum
    convert h using 2
    have hsingle : (∑ j, ((Pi.single i₀ (∑ l, c l) : Fin (N + 1) → ℕ) j : ℤ)) = ∑ l, (c l : ℤ) := by
      rw [Finset.sum_eq_single i₀ (fun j _ hj =>
        by simp [hj]) (fun h => absurd (Finset.mem_univ _) h)]
      simp
    simp only [Pi.add_apply, Nat.cast_add, Finset.sum_add_distrib, hsingle]

theorem

PsiNum_monMulFrac

L1264 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.PsiNum_monMulFrac

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A)) (m : ℕ)
section MonMul
variable [IsAffineHom φ] {I : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)} (hi₀ : i₀ ∈ I)
include hi₀
omit [IsAffineHom φ] in

Lean source · statement

theorem PsiNum_monMulFrac (c : Fin (N + 1) → ℕ) (x : ProjSpaceCech.GradedModule.Frac
  ((twistGradedModule φ π).shift (m : ℤ)) I) :
    PsiNum φ π m (i₀ := i₀) (monMulFrac φ π m hi₀ c x)
      = restrictFun (Wop_le_top φ) (∏ l, uTop φ i₀ l ^ c l) * PsiNum φ π m x

theorem

prod_frameUnit_pow_eq

L1298 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.prod_frameUnit_pow_eq

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
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 prod_frameUnit_pow_eq (i₀ : Fin (N + 1)) (e : Fin (N + 1) →₀ ℕ) (d : ℕ) (hd : e.degree = d)
    (hm : MvPolynomial.monomial e (1 : A) ∈ (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A) (d
      • 1)) :
    (∏ l, frameUnit φ i₀ l ^ e l)
      = (φ.app (Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A) (MvPolynomial.X
        i₀))).hom
          ((Proj.awayToSection _ (MvPolynomial.X i₀)).hom
            (HomogeneousLocalization.Away.mk _ (X_mem_one A N i₀) d (MvPolynomial.monomial e (1 :
              A)) hm))

def

fracFun

L1336 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.fracFun

Documentation

The section obtained from a homogeneous polynomial fraction.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
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 fracFun (i : Fin (N + 1)) (k : ℕ) (p : MvPolynomial (Fin (N + 1)) A) (hp : p ∈ 𝒜 (k • 1)) :
  Γ(X, pullbackChart φ i)

theorem

exists_fracFun_eq

L1342 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.exists_fracFun_eq

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
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_fracFun_eq (i : Fin (N + 1)) (t : Γ(Proj 𝒜, Proj.basicOpen 𝒜 (MvPolynomial.X i))) :
    ∃ (k : ℕ) (p : MvPolynomial (Fin (N + 1)) A) (hp : p ∈ 𝒜 (k • 1)),
      (φ.app (Proj.basicOpen 𝒜 (MvPolynomial.X i))).hom t = fracFun φ i k p hp

theorem

exists_chart_generators

L1354 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.exists_chart_generators

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
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_chart_generators [IsFinite φ] (i : Fin (N + 1)) :
    ∃ (S : Finset Γ(X, pullbackChart φ i)), ∀ s : Γ(X, pullbackChart φ i),
      ∃ (k : Γ(X, pullbackChart φ i) → ℕ) (p : Γ(X, pullbackChart φ i) → MvPolynomial (Fin (N + 1))
        A)
        (hp : ∀ g, p g ∈ 𝒜 (k g • 1)),
        s = ∑ g ∈ S, fracFun φ i (k g) (p g) (hp g) * g

def

genSet

L1407 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.genSet

Documentation

A finite set of generators for the chart algebra.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Build
variable [IsFinite φ]

Lean source · statement

def genSet (i : Fin (N + 1)) : Finset Γ(X, pullbackChart φ i)

theorem

genSet_spec

L1410 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.genSet_spec

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Build
variable [IsFinite φ]

Lean source · statement

theorem genSet_spec (i : Fin (N + 1)) (s : Γ(X, pullbackChart φ i)) :
    ∃ (k : Γ(X, pullbackChart φ i) → ℕ) (p : Γ(X, pullbackChart φ i) → MvPolynomial (Fin (N + 1)) A)
      (hp : ∀ g, p g ∈ 𝒜 (k g • 1)), s = ∑ g ∈ genSet φ i, fracFun φ i (k g) (p g) (hp g) * g

def

Gens

L1416 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.Gens

Documentation

Chart generators together with their chart indices.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Build
variable [IsFinite φ]

Lean source · statement

def Gens : Type u

instance

(anonymous instance)

L1418 ↗

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Build
variable [IsFinite φ]

Lean source · statement

instance : Fintype (Gens φ)

theorem

mem_singleton_self'

L1420 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.mem_singleton_self'

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Build
variable [IsFinite φ]

Lean source · statement

theorem mem_singleton_self' (i : Fin (N + 1)) : i ∈ ({i} : Finset (Fin (N + 1)))

def

genTarget

L1424 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.genTarget

Documentation

The twisted section corresponding to a chart generator.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Build
variable [IsFinite φ]

Lean source · statement

def genTarget (i : Fin (N + 1)) (g : Γ(X, pullbackChart φ i)) : twistObj π φ 0 (interI φ {i})

def

genFrac

L1428 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.genFrac

Documentation

A homogeneous fraction representing a chart generator.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Build
variable [IsFinite φ]

Lean source · statement

def genFrac (t : Gens φ) : ProjSpaceCech.GradedModule.Frac ((twistGradedModule φ π).shift ((0 : ℕ)
  : ℤ)) {t.1}

theorem

Psi_genFrac

L1433 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.Psi_genFrac

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Build
variable [IsFinite φ]

Lean source · statement

theorem Psi_genFrac (t : Gens φ) :
    Psi φ π 0 (mem_singleton_self' t.1) (ProjSpaceCech.GradedModule.sec.mk _ _ (genFrac φ π t)) =
      genTarget φ π t.1 t.2

theorem

PsiNum_genFrac

L1442 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.PsiNum_genFrac

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Build
variable [IsFinite φ]

Lean source · statement

theorem PsiNum_genFrac (t : Gens φ) :
    PsiNum φ π 0 (i₀ := t.1) (genFrac φ π t) = restrictFun (Wop_le_self φ) (t.2 : Γ(X,
      pullbackChart φ t.1))

def

genDeg

L1449 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.genDeg

Documentation

The denominator degree of the fraction representing a generator.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Build
variable [IsFinite φ]

Lean source · statement

def genDeg (t : Gens φ) : ℤ

theorem

genFrac_num_mem

L1451 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.genFrac_num_mem

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Build
variable [IsFinite φ]

Lean source · statement

theorem genFrac_num_mem (t : Gens φ) : (genFrac φ π t).num ∈ (twistGradedModule φ π).grade (genDeg
  φ π t)

abbrev

GIdx

L1458 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.GIdx

Documentation

A finite index type for the chart generators.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Build
variable [IsFinite φ]

Lean source · statement

abbrev GIdx : Type

def

gen

L1461 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.gen

Documentation

The chart generator indexed by the finite index type.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Build
variable [IsFinite φ]

Lean source · statement

def gen (t : GIdx φ) : Gens φ

abbrev

Fgen

L1464 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.Fgen

Documentation

The finite free graded module on the chosen homogeneous generators.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Build
variable [IsFinite φ]

Lean source · statement

abbrev Fgen : ProjSpaceCech.GradedModule A N

def

psi0Lin

L1469 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.psi0Lin

Documentation

The linear map evaluating finite tuples at the chosen generators.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Build
variable [IsFinite φ]

Lean source · full declaration

def psi0Lin : (Fgen φ π).M →ₗ[A] (twistGradedModule φ π).M where
  toFun v := ∑ t : GIdx φ, ProjSpaceCech.GradedModule.evalLin (twistGradedModule φ π) (genFrac φ π
    (gen φ t)).num (v t)
  map_add' v w := by
    rw [← Finset.sum_add_distrib]
    exact Finset.sum_congr rfl fun t _ => by
      change ProjSpaceCech.GradedModule.evalLin _ _ (v t + w t) = _
      exact map_add _ _ _
  map_smul' r v := by
    rw [RingHom.id_apply, Finset.smul_sum]
    exact Finset.sum_congr rfl fun t _ => by
      change ProjSpaceCech.GradedModule.evalLin _ _ (r • v t) = _
      exact map_smul _ _ _

theorem

psi0Lin_apply

L1483 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.psi0Lin_apply

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Build
variable [IsFinite φ]

Lean source · statement

theorem psi0Lin_apply (v : (Fgen φ π).M) :
    psi0Lin φ π v = ∑ t : GIdx φ, ProjSpaceCech.GradedModule.evalLin (twistGradedModule φ π)
      (genFrac φ π (gen φ t)).num (v t)

def

psi0

L1488 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.psi0

Documentation

The graded morphism evaluating the chosen generators.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Build
variable [IsFinite φ]

Lean source · full declaration

def psi0 : ProjSpaceCech.GradedModule.Hom (Fgen φ π) (twistGradedModule φ π) where
  toLinearMap := psi0Lin φ π
  mem_grade d v hv := by
    rw [psi0Lin_apply]
    refine Submodule.sum_mem _ fun t _ => ?_
    exact ProjSpaceCech.GradedModule.evalLin_mem_grade _ (genFrac_num_mem φ π (gen φ t)) (hv t
      (Set.mem_univ t))
  xMul_comm j := by
    refine LinearMap.ext fun v => ?_
    rw [LinearMap.comp_apply, LinearMap.comp_apply, psi0Lin_apply, psi0Lin_apply, map_sum]
    refine Finset.sum_congr rfl fun t _ => ?_
    exact ProjSpaceCech.GradedModule.evalLin_X_mul _ _ j (v t)

theorem

psi0_single

L1501 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.psi0_single

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Build
variable [IsFinite φ]

Lean source · statement

theorem psi0_single (t : GIdx φ) (p : MvPolynomial (Fin (N + 1)) A) :
    (psi0 φ π).toLinearMap (Pi.single t p : (Fgen φ π).M)
      = ProjSpaceCech.GradedModule.evalLin (twistGradedModule φ π) (genFrac φ π (gen φ t)).num p

theorem

ker_psi0_stable

L1518 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.ker_psi0_stable

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Build
variable [IsFinite φ]

Lean source · statement

theorem ker_psi0_stable (j : Fin (N + 1)) : ∀ v ∈ LinearMap.ker (psi0 φ π).toLinearMap,
    (Fgen φ π).xMul j v ∈ LinearMap.ker (psi0 φ π).toLinearMap

abbrev

Mgen

L1525 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.Mgen

Documentation

The quotient by the kernel of evaluation at the generators.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Build
variable [IsFinite φ]

Lean source · statement

abbrev Mgen : ProjSpaceCech.GradedModule A N

theorem

mem_Mgen_grade_iff

L1529 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.mem_Mgen_grade_iff

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Build
variable [IsFinite φ]

Lean source · statement

theorem mem_Mgen_grade_iff (d : ℤ) (z : (Fgen φ π).M ⧸ LinearMap.ker (psi0 φ π).toLinearMap) :
    z ∈ (Mgen φ π).grade d ↔ z ∈ ((Fgen φ π).grade d).map (LinearMap.ker (psi0 φ
      π).toLinearMap).mkQ

def

mkQHom

L1534 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.mkQHom

Documentation

The graded quotient map onto the module generated by the chosen fractions.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Build
variable [IsFinite φ]

Lean source · full declaration

def mkQHom : ProjSpaceCech.GradedModule.Hom (Fgen φ π) (Mgen φ π) where
  toLinearMap := (LinearMap.ker (psi0 φ π).toLinearMap).mkQ
  mem_grade d _v hv := (mem_Mgen_grade_iff φ π d _).mpr (Submodule.mem_map_of_mem hv)
  xMul_comm _j := rfl

theorem

Mgen_isFG

L1539 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.Mgen_isFG

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Build
variable [IsFinite φ]

Lean source · statement

theorem Mgen_isFG : (Mgen φ π).IsFG

def

psi

L1546 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.psi

Documentation

The induced injective graded morphism into the twisted section module.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Build
variable [IsFinite φ]

Lean source · full declaration

def psi : ProjSpaceCech.GradedModule.Hom (Mgen φ π) (twistGradedModule φ π) where
  toLinearMap := (LinearMap.ker (psi0 φ π).toLinearMap).liftQ (psi0 φ π).toLinearMap le_rfl
  mem_grade d z hz := by
    obtain ⟨v, hv, rfl⟩ := Submodule.mem_map.mp ((mem_Mgen_grade_iff φ π d z).mp hz)
    exact (psi0 φ π).mem_grade d v hv
  xMul_comm j := by
    refine LinearMap.ext fun z => ?_
    obtain ⟨v, rfl⟩ := Submodule.mkQ_surjective _ z
    exact LinearMap.congr_fun ((psi0 φ π).xMul_comm j) v

theorem

psi_mkQ

L1556 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.psi_mkQ

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Build
variable [IsFinite φ]

Lean source · statement

theorem psi_mkQ (v : (Fgen φ π).M) :
    (psi φ π).toLinearMap ((LinearMap.ker (psi0 φ π).toLinearMap).mkQ v) = (psi0 φ π).toLinearMap v

theorem

psi_injective

L1560 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.psi_injective

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Build
variable [IsFinite φ]

Lean source · statement

theorem psi_injective : Function.Injective (psi φ π).toLinearMap

theorem

app_awayToSection_algebraMap

L1591 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.app_awayToSection_algebraMap

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
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 app_awayToSection_algebraMap (j : Fin (N + 1)) (r : A) :
    (φ.app (Proj.basicOpen 𝒜 (MvPolynomial.X j))).hom
        ((Proj.awayToSection 𝒜 (MvPolynomial.X j)).hom (algebraMap A (Away 𝒜 (MvPolynomial.X j)) r))
      = (Scheme.TwoAffineOpenCover.algebraOfHom (φ ≫ ProjSpace.π A N) (pullbackChart φ
        j)).algebraMap r

theorem

awayMk_eq_sum_monomial

L1634 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.awayMk_eq_sum_monomial

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
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 awayMk_eq_sum_monomial (j : Fin (N + 1)) (k : ℕ) (p : MvPolynomial (Fin (N + 1)) A) (hp : p
  ∈ 𝒜 (k • 1))
    (s : Finset (Fin (N + 1) →₀ ℕ)) (hsum : ∑ c ∈ s, MvPolynomial.monomial c (p.coeff c) = p)
    (hmono : ∀ c ∈ s, MvPolynomial.monomial c (1 : A) ∈ 𝒜 (k • 1)) :
    HomogeneousLocalization.Away.mk 𝒜 (X_mem_one A N j) k p hp
      = ∑ c ∈ s.attach, algebraMap A
          (Away 𝒜 (MvPolynomial.X j : MvPolynomial (Fin (N + 1)) A)) (p.coeff c.1)
          * HomogeneousLocalization.Away.mk 𝒜 (X_mem_one A N j) k
              (MvPolynomial.monomial c.1 (1 : A)) (hmono c.1 c.2)

theorem

fracFun_eq_sum

L1659 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.fracFun_eq_sum

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
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 fracFun_eq_sum (j : Fin (N + 1)) (k : ℕ) (p : MvPolynomial (Fin (N + 1)) A) (hp : p ∈ 𝒜 (k
  • 1)) :
    fracFun φ j k p hp
      = ∑ c ∈ p.support, (Scheme.TwoAffineOpenCover.algebraOfHom (φ ≫ ProjSpace.π A N)
        (pullbackChart φ j)).algebraMap (p.coeff c)
          * ∏ l, frameUnit φ j l ^ c l

theorem

twistObj_sum_val

L1706 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.twistObj_sum_val

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A

Lean source · statement

theorem twistObj_sum_val {m : ℕ} {U : X.Opens} {ι : Type*} (s : Finset ι) (f : ι → twistObj π φ m
  U) (i : Fin (N + 1)) :
    (∑ a ∈ s, f a).val i = ∑ a ∈ s, (f a).val i

theorem

eq_single_of_supp

L1715 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.eq_single_of_supp

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A

Lean source · statement

theorem eq_single_of_supp {j : Fin (N + 1)} (b : Fin (N + 1) → ℕ) (hb : ∀ l ∉ ({j} : Finset (Fin (N
  + 1))), b l = 0) :
    b = Pi.single j (b j)

theorem

sum_cast_eq_of_supp

L1723 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.sum_cast_eq_of_supp

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A

Lean source · statement

theorem sum_cast_eq_of_supp {j : Fin (N + 1)} (b : Fin (N + 1) → ℕ) (hb : ∀ l ∉ ({j} : Finset (Fin
  (N + 1))), b l = 0) :
    (∑ l, (b l : ℤ)) = b j

def

Good

L1734 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.Good

Documentation

The property of a localized section admitting a homogeneous generator presentation.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Sat
variable [IsFinite φ]

Lean source · statement

def Good (j : Fin (N + 1)) (z : ProjSpaceCech.GradedModule.sec ((twistGradedModule φ π).shift ((0 :
  ℕ) : ℤ)) {j}) : Prop

theorem

psi0_mem_shift_grade

L1743 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.psi0_mem_shift_grade

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Sat
variable [IsFinite φ]

Lean source · statement

theorem psi0_mem_shift_grade {d : ℤ} {v : (Fgen φ π).M} (hv : v ∈ (Fgen φ π).grade d) :
    (psi0 φ π).toLinearMap v ∈ ((twistGradedModule φ π).shift ((0 : ℕ) : ℤ)).grade d

theorem

monMul_shift_eq

L1750 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.monMul_shift_eq

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Sat
variable [IsFinite φ]
omit [IsFinite φ] in

Lean source · statement

theorem monMul_shift_eq (k : ℤ) (a : Fin (N + 1) → ℕ) :
    ProjSpaceCech.GradedModule.monMul ((twistGradedModule φ π).shift k) a =
      ProjSpaceCech.GradedModule.monMul (twistGradedModule φ π) a

theorem

good_zero

L1754 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.good_zero

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Sat
variable [IsFinite φ]

Lean source · statement

theorem good_zero (j : Fin (N + 1)) : Good φ π j 0

theorem

good_add

L1762 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.good_add

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Sat
variable [IsFinite φ]

Lean source · statement

theorem good_add (j : Fin (N + 1)) {z w : ProjSpaceCech.GradedModule.sec ((twistGradedModule φ
  π).shift ((0 : ℕ) : ℤ)) {j}}
    (hz : Good φ π j z) (hw : Good φ π j w) : Good φ π j (z + w)

theorem

good_smul_monMulFrac

L1786 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.good_smul_monMulFrac

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (π : X ⟶ Spec (.of A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
section Sat
variable [IsFinite φ]

Lean source · statement

theorem good_smul_monMulFrac (t : Gens φ) (r : A) (c : Fin (N + 1) → ℕ) :
    Good φ π t.1 (r • ProjSpaceCech.GradedModule.sec.mk _ {t.1} (monMulFrac φ π 0
      (mem_singleton_self' t.1) c (genFrac φ π t)))

theorem

good_sum

L1864 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.good_sum

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
section Sat2
variable [IsFinite φ]

Lean source · statement

theorem good_sum (π : X ⟶ Spec (.of A)) (j : Fin (N + 1)) {ι : Type*} (s : Finset ι)
    (f : ι → ProjSpaceCech.GradedModule.sec ((twistGradedModule φ π).shift ((0 : ℕ) : ℤ)) {j}) (hf
      : ∀ a ∈ s, Good φ π j (f a)) :
    Good φ π j (∑ a ∈ s, f a)

theorem

pullbackChart_le_Wop

L1871 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.pullbackChart_le_Wop

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
section Sat2
variable [IsFinite φ]
omit [IsFinite φ] in

Lean source · statement

theorem pullbackChart_le_Wop (j : Fin (N + 1)) : pullbackChart φ j ≤ Wop φ {j} j

theorem

restrictFun_prod_uTop'

L1875 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.restrictFun_prod_uTop'

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
section Sat2
variable [IsFinite φ]
omit [IsFinite φ] in

Lean source · statement

theorem restrictFun_prod_uTop' (j : Fin (N + 1)) (c : Fin (N + 1) → ℕ) :
    restrictFun (Wop_le_top φ (I := {j})) (∏ l, uTop φ j l ^ c l) = restrictFun (Wop_le_self φ) (∏
      l, frameUnit φ j l ^ c l)

theorem

psi_saturated

L1880 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.GMSec.psi_saturated

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace GMSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
section Sat2
variable [IsFinite φ]

Lean source · statement

theorem psi_saturated (π : X ⟶ Spec (.of A)) (hπ : φ ≫ ProjSpace.π A N = π) (j : Fin (N + 1)) (e :
  ℤ)
    (x : (twistGradedModule φ π).M) (hx : x ∈ (twistGradedModule φ π).grade e) :
    ∃ K : ℕ, ∃ x' ∈ (Mgen φ π).grade (e + K),
      (psi φ π).toLinearMap x' = ((twistGradedModule φ π).xMul j ^ K) x

theorem

exists_isFG_hom_injective_saturated_twistGradedModule'

L1986 ↗

AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist.AlgebraicGeometry.ProjSpace.exists_isFG_hom_injective_saturated_twistGradedModule'

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
open scoped AlgebraicGeometry _root_.AlgebraicGeometry.ProjSpace in

Lean source · statement

theorem AlgebraicGeometry.ProjSpace.exists_isFG_hom_injective_saturated_twistGradedModule'
    {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
    (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) [IsFinite φ]
    (π : X ⟶ Spec (.of A)) (hπ : φ ≫ ProjSpace.π A N = π) :
    ∃ (M' : ProjSpaceCech.GradedModule A N) (ψ : ProjSpaceCech.GradedModule.Hom M'
      (ProjSpace.twistGradedModule φ π)),
      M'.IsFG ∧ Function.Injective ψ.toLinearMap ∧
      ∀ (j : Fin (N + 1)) (e : ℤ), ∀ x ∈ (ProjSpace.twistGradedModule φ π).grade e,
        ∃ k : ℕ, ∃ x' ∈ M'.grade (e + k), ψ.toLinearMap x' = ((ProjSpace.twistGradedModule φ
          π).xMul j ^ k) x

theorem

exists_isFG_hom_injective_saturated_twistGradedModule

L2000 ↗

AlgebraicGeometry.ProjSpace.exists_isFG_hom_injective_saturated_twistGradedModule

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.SaturatedTwist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section

Lean source · statement

theorem _root_.AlgebraicGeometry.ProjSpace.exists_isFG_hom_injective_saturated_twistGradedModule
    {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
    (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) [IsFinite φ]
    (π : X ⟶ Spec (.of A)) (hπ : φ ≫ ProjSpace.π A N = π) :
    ∃ (M' : ProjSpaceCech.GradedModule A N) (ψ : ProjSpaceCech.GradedModule.Hom M'
      (ProjSpace.twistGradedModule φ π)),
      M'.IsFG ∧ Function.Injective ψ.toLinearMap ∧
      ∀ (j : Fin (N + 1)) (e : ℤ), ∀ x ∈ (ProjSpace.twistGradedModule φ π).grade e,
        ∃ k : ℕ, ∃ x' ∈ M'.grade (e + k), ψ.toLinearMap x' = ((ProjSpace.twistGradedModule φ
          π).xMul j ^ k) x

Module documentation

Proj Space exists is FG hom injective saturated twist Graded Module

Declarations