Module

ProjSpace_exists_sec_shift_twistGradedModule_equiv.lean

Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_sec_shift_twistGradedModule_equiv

88 declarations indexed from sourceView source ↗

Module documentation

Sections of shifts of the projective twisting module

Local homogeneous fractions identify shifted graded sections with twisting-module sections.

Imports3

Imported by2

theorem

proj_basicOpen_awayMk

L57 ↗

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

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L93 ↗

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

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L103 ↗

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

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L128 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L134 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L143 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L153 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L169 ↗

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

Documentation

The local family generated by a section using the transition units.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L174 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L187 ↗

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

Documentation

The compatible twisting section generated on a chart.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L190 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L195 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L200 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L203 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L206 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L209 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L215 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L244 ↗

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

Documentation

The intersection of the charts indexed by a finite set.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L246 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L250 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L254 ↗

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

Documentation

The product of transition units on a chart.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L257 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L271 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L276 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L279 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L282 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L310 ↗

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

Documentation

The transition unit restricted to the top-chart intersection.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L313 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L316 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L326 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L371 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L382 ↗

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

Documentation

The intersection of the finite chart intersection with the distinguished chart.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L385 ↗

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

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L386 ↗

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

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L387 ↗

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

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L391 ↗

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

Documentation

The product of inverse transition factors for the denominator exponents.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L396 ↗

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

Documentation

The product of direct transition factors for the denominator exponents.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L400 ↗

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

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L406 ↗

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

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L412 ↗

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

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L418 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_sec_shift_twistGradedModule_equiv.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
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L431 ↗

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

Documentation

The section represented by a homogeneous numerator and its denominator factors.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L435 ↗

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

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L496 ↗

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

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L544 ↗

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

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L583 ↗

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

Documentation

The map from fraction classes to sections on the distinguished intersection.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L587 ↗

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

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L590 ↗

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

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L598 ↗

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

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L607 ↗

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

Documentation

The linear map from graded fraction sections to twisting sections.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L616 ↗

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

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L621 ↗

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

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L649 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L659 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L666 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L675 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L688 ↗

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

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L716 ↗

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

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L751 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L785 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L830 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L842 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L851 ↗

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

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L862 ↗

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

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L872 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L886 ↗

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

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L940 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L949 ↗

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

Documentation

A chart expressed as its intersection with the top open.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L951 ↗

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

Documentation

The overlap of two charts expressed under the top open.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L953 ↗

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

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L954 ↗

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

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L956 ↗

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

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L957 ↗

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

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L960 ↗

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

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L989 ↗

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

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L1042 ↗

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

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L1053 ↗

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

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L1063 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L1122 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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

L1129 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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))

theorem

invProd_eq_prod_dite

L1159 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_sec_shift_twistGradedModule_equiv.AlgebraicGeometry.ProjSpace.GMSec.invProd_eq_prod_dite

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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 Nat
variable {I J : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)}

Lean source · full declaration

theorem invProd_eq_prod_dite {K : Finset (Fin (N + 1))} (hIK : I ⊆ K) (a : Fin (N + 1) → ℕ) (ha : ∀
  j ∉ I, a j = 0) :
    invProd φ K i₀ a = ∏ j, (if hj : j ∈ I then restrictFun (Wop_le_chart φ (i₀ := i₀) (hIK hj))
      (frameUnit φ j i₀) ^ a j else 1) := by
  classical
  unfold invProd
  have h1 : (∏ j ∈ K.attach, restrictFun (Wop_le_chart φ (i₀ := i₀) j.2) (frameUnit φ j i₀) ^ a j)
      = ∏ j ∈ K.attach, (fun j : Fin (N + 1) =>
          if hj : j ∈ K then restrictFun (Wop_le_chart φ (i₀ := i₀) hj) (frameUnit φ j i₀) ^ a j
            else 1) j := by
    refine Finset.prod_congr rfl fun j _ => ?_
    simp only [dite_eq_left j.2]
  rw [h1, Finset.prod_attach K (fun j : Fin (N + 1) =>
      if hj : j ∈ K then restrictFun (Wop_le_chart φ (i₀ := i₀) hj) (frameUnit φ j i₀) ^ a j else
        1)]
  rw [Finset.prod_subset (Finset.subset_univ K)
    (f := fun j : Fin (N + 1) => if hj : j ∈ K then restrictFun (Wop_le_chart φ (i₀ := i₀) hj)
      (frameUnit φ j i₀) ^ a j else 1)
    (fun j _ hj => by simp only [dite_eq_right hj])]
  refine Finset.prod_congr rfl fun j _ => ?_
  by_cases hjI : j ∈ I
  · rw [dite_eq_left (hIK hjI), dite_eq_left hjI]
  · rw [dite_eq_right hjI]
    by_cases hjK : j ∈ K
    · rw [dite_eq_left hjK, ha j hjI, pow_zero]
    · rw [dite_eq_right hjK]

theorem

restrictFun_invProd

L1186 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_sec_shift_twistGradedModule_equiv.AlgebraicGeometry.ProjSpace.GMSec.restrictFun_invProd

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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 Nat
variable {I J : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)}

Lean source · statement

theorem restrictFun_invProd (hIJ : I ⊆ J) (a : Fin (N + 1) → ℕ) (ha : ∀ j ∉ I, a j = 0) :
    restrictFun (inf_le_inf_right (pullbackChart φ i₀) (interI_anti φ hIJ) : Wop φ J i₀ ≤ Wop φ I
      i₀) (invProd φ I i₀ a)
      = invProd φ J i₀ a

theorem

secIncl_mk

L1197 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_sec_shift_twistGradedModule_equiv.AlgebraicGeometry.ProjSpace.GMSec.secIncl_mk

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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 Nat
variable {I J : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)}

Lean source · full declaration

theorem secIncl_mk (hIJ : I ⊆ J) (x : ProjSpaceCech.GradedModule.Frac ((twistGradedModule φ
  π).shift (m : ℤ)) I) :
    ProjSpaceCech.GradedModule.secIncl ((twistGradedModule φ π).shift (m : ℤ)) hIJ
      (ProjSpaceCech.GradedModule.sec.mk _ I x)
      = ProjSpaceCech.GradedModule.sec.mk _ J ⟨x.denExp, fun j hj => x.hden j (fun h => hj (hIJ
        h)), x.num, x.hnum⟩ := rfl

theorem

Psi_secIncl

L1204 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_sec_shift_twistGradedModule_equiv.AlgebraicGeometry.ProjSpace.GMSec.Psi_secIncl

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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 Nat
variable {I J : Finset (Fin (N + 1))} {i₀ : Fin (N + 1)}

Lean source · statement

theorem Psi_secIncl (hi₀ : i₀ ∈ I) (hIJ : I ⊆ J)
    (s : ProjSpaceCech.GradedModule.sec ((twistGradedModule φ π).shift (m : ℤ)) I) :
    Psi φ π m (hIJ hi₀) (ProjSpaceCech.GradedModule.secIncl _ hIJ s)
      = (twist π φ m).res (interI_anti φ hIJ) (Psi φ π m hi₀ s)

theorem

invProd_change

L1241 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_sec_shift_twistGradedModule_equiv.AlgebraicGeometry.ProjSpace.GMSec.invProd_change

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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 Indep
variable {I : Finset (Fin (N + 1))} {i₀ i₁ : Fin (N + 1)} (hi₀ : i₀ ∈ I) (hi₁ : i₁ ∈ I)
include hi₀ hi₁
omit hi₀ hi₁ in

Lean source · statement

theorem invProd_change (a : Fin (N + 1) → ℕ) (ha : ∀ j ∉ I, a j = 0) :
    restrictFun (inf_le_left : interI φ I ⊓ pullbackChart φ i₀ ⊓ pullbackChart φ i₁ ≤ Wop φ I i₀)
      (invProd φ I i₀ a)
      = restrictFun (le_inf (inf_le_left.trans inf_le_left) inf_le_right :
          interI φ I ⊓ pullbackChart φ i₀ ⊓ pullbackChart φ i₁ ≤ Wop φ I i₁) (invProd φ I i₁ a)
        * restrictFun (inf_le_right : interI φ I ⊓ pullbackChart φ i₀ ⊓ pullbackChart φ i₁ ≤
          pullbackChart φ i₁)
            (frameUnit φ i₁ i₀) ^ (∑ j, a j)

theorem

Psi_eq_of_mem

L1260 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_sec_shift_twistGradedModule_equiv.AlgebraicGeometry.ProjSpace.GMSec.Psi_eq_of_mem

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_sec_shift_twistGradedModule_equiv
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 Indep
variable {I : Finset (Fin (N + 1))} {i₀ i₁ : Fin (N + 1)} (hi₀ : i₀ ∈ I) (hi₁ : i₁ ∈ I)
include hi₀ hi₁

Lean source · statement

theorem Psi_eq_of_mem : Psi φ π m hi₀ (I := I) = Psi φ π m hi₁

theorem

exists_sec_shift_twistGradedModule_equiv'

L1320 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_sec_shift_twistGradedModule_equiv.AlgebraicGeometry.ProjSpace.exists_sec_shift_twistGradedModule_equiv'

Source context 15 commands

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

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

Lean source · full declaration

theorem exists_sec_shift_twistGradedModule_equiv'
    {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
    (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) [IsAffineHom φ]
    (π : X ⟶ Spec (.of A)) (m : ℕ) :
    ∃ e : ∀ (I : Finset (Fin (N + 1))), I.Nonempty →
        (ProjSpaceCech.GradedModule.sec ((ProjSpace.twistGradedModule φ π).shift (m : ℤ)) I
          ≃ₗ[A] ProjSpace.twistObj π φ m (⨅ i ∈ I, ProjSpace.pullbackChart φ i)),
      ∀ (I J : Finset (Fin (N + 1))) (hI : I.Nonempty) (hIJ : I ⊆ J)
        (x : ProjSpaceCech.GradedModule.sec ((ProjSpace.twistGradedModule φ π).shift (m : ℤ)) I),
        e J (hI.mono hIJ) (ProjSpaceCech.GradedModule.secIncl _ hIJ x)
          = ProjSpace.twistRes π φ m
              (le_iInf fun i => le_iInf fun hi => (iInf_le _ i).trans (iInf_le _ (hIJ hi)) :
                (⨅ i ∈ J, ProjSpace.pullbackChart φ i) ≤ ⨅ i ∈ I, ProjSpace.pullbackChart φ i)
              (e I hI x) := by
  classical
  refine ⟨fun I hI => LinearEquiv.ofBijective (GMSec.Psi φ π m hI.choose_spec) (GMSec.Psi_bijective
    φ π m hI.choose_spec), ?_⟩
  intro I J hI hIJ x
  change GMSec.Psi φ π m (hI.mono hIJ).choose_spec (ProjSpaceCech.GradedModule.secIncl _ hIJ x)
    = ProjSpace.twistRes π φ m _ (GMSec.Psi φ π m hI.choose_spec x)
  rw [GMSec.Psi_eq_of_mem φ π m (hI.mono hIJ).choose_spec (hIJ hI.choose_spec), GMSec.Psi_secIncl]
  rfl

theorem

exists_sec_shift_twistGradedModule_equiv

L1345 ↗

AlgebraicGeometry.ProjSpace.exists_sec_shift_twistGradedModule_equiv

Source context 8 commands

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

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

Lean source · full declaration

theorem _root_.AlgebraicGeometry.ProjSpace.exists_sec_shift_twistGradedModule_equiv
    {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
    (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) [IsAffineHom φ]
    (π : X ⟶ Spec (.of A)) (m : ℕ) :
    ∃ e : ∀ (I : Finset (Fin (N + 1))), I.Nonempty →
        (ProjSpaceCech.GradedModule.sec ((ProjSpace.twistGradedModule φ π).shift (m : ℤ)) I
          ≃ₗ[A] ProjSpace.twistObj π φ m (⨅ i ∈ I, ProjSpace.pullbackChart φ i)),
      ∀ (I J : Finset (Fin (N + 1))) (hI : I.Nonempty) (hIJ : I ⊆ J)
        (x : ProjSpaceCech.GradedModule.sec ((ProjSpace.twistGradedModule φ π).shift (m : ℤ)) I),
        e J (hI.mono hIJ) (ProjSpaceCech.GradedModule.secIncl _ hIJ x)
          = ProjSpace.twistRes π φ m
              (le_iInf fun i => le_iInf fun hi => (iInf_le _ i).trans (iInf_le _ (hIJ hi)) :
                (⨅ i ∈ J, ProjSpace.pullbackChart φ i) ≤ ⨅ i ∈ I, ProjSpace.pullbackChart φ i)
              (e I hI x) :=
  AlgebraicGeometry.ProjSpace.exists_sec_shift_twistGradedModule_equiv' φ π m

Module documentation

Sections of shifts of the projective twisting module

Declarations