NYLL
Module

Scheme_Modules_ProjPresentation_exists_projPresentation_pullback_sigma_eq_toProj_eq.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_ProjPresentation_exists_projPresentation_pullback_sigma_eq_toProj_eq
12 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Proj Presentation exists proj Presentation pullback sigma eq to Proj eq

Imports3
Imported by2

Declarations

lemma

preimage_chart

L68 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_projPresentation_pullback_sigma_eq_toProj_eq.AlgebraicGeometry.Scheme.Modules.PresPre.preimage_chart
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_projPresentation_pullback_sigma_eq_toProj_eq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresPre
variable {R : Type u} [CommRing R] {X X' : Scheme.{u}} {f : X ⟶ Spec (.of R)} (p : X' ⟶ X)
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
lemma preimage_chart (i : Fin (N + 1)) :
    (p ≫ 𝔓.toProj) ⁻¹ᵁ Proj.basicOpen 𝒜R (MvPolynomial.X i) =
      p ⁻¹ᵁ (𝔓.toProj ⁻¹ᵁ Proj.basicOpen 𝒜R (MvPolynomial.X i))
abbrev

σ'

L74 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_projPresentation_pullback_sigma_eq_toProj_eq.AlgebraicGeometry.Scheme.Modules.PresPre.σ'
Documentation

The presenting sections pulled back through the adjunction unit.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_projPresentation_pullback_sigma_eq_toProj_eq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresPre
variable {R : Type u} [CommRing R] {X X' : Scheme.{u}} {f : X ⟶ Spec (.of R)} (p : X' ⟶ X)
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
abbrev σ' (i : Fin (N + 1)) : Γ((Modules.pullback p).obj M, ⊤)
lemma

presheaf_map_congr

L77 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_projPresentation_pullback_sigma_eq_toProj_eq.AlgebraicGeometry.Scheme.Modules.PresPre.presheaf_map_congr
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_projPresentation_pullback_sigma_eq_toProj_eq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresPre
variable {R : Type u} [CommRing R] {X X' : Scheme.{u}} {f : X ⟶ Spec (.of R)} (p : X' ⟶ X)
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
omit 𝔓 in
Lean source · statement
lemma presheaf_map_congr {Z : Scheme.{u}} (G : TopCat.Presheaf Ab Z) {U V : Z.Opens}
    (k₁ k₂ : op U ⟶ op V) (z : G.obj (op U)) : G.map k₁ z = G.map k₂ z
def

eta

L82 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_projPresentation_pullback_sigma_eq_toProj_eq.AlgebraicGeometry.Scheme.Modules.PresPre.eta
Documentation

The pullback of a module section through the adjunction unit.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_projPresentation_pullback_sigma_eq_toProj_eq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresPre
variable {R : Type u} [CommRing R] {X X' : Scheme.{u}} {f : X ⟶ Spec (.of R)} (p : X' ⟶ X)
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
def eta (U : X.Opens) (m : Γ(M, U)) : Γ((Modules.pullback p).obj M, p ⁻¹ᵁ U)
lemma

eta_smul

L85 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_projPresentation_pullback_sigma_eq_toProj_eq.AlgebraicGeometry.Scheme.Modules.PresPre.eta_smul
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_projPresentation_pullback_sigma_eq_toProj_eq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresPre
variable {R : Type u} [CommRing R] {X X' : Scheme.{u}} {f : X ⟶ Spec (.of R)} (p : X' ⟶ X)
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
omit 𝔓 f in
Lean source · statement
lemma eta_smul (U : X.Opens) (r : Γ(X, U)) (m : Γ(M, U)) :
    eta p (M := M) U (r • m) = p.app U r • eta p (M := M) U m
lemma

eta_resTop

L89 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_projPresentation_pullback_sigma_eq_toProj_eq.AlgebraicGeometry.Scheme.Modules.PresPre.eta_resTop
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_projPresentation_pullback_sigma_eq_toProj_eq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresPre
variable {R : Type u} [CommRing R] {X X' : Scheme.{u}} {f : X ⟶ Spec (.of R)} (p : X' ⟶ X)
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
omit 𝔓 f in
Lean source · statement
lemma eta_resTop (U : X.Opens) (m : Γ(M, ⊤)) :
    eta p (M := M) U (M.presheaf.map (homOfLE (le_top : U ≤ ⊤)).op m) =
      ((Modules.pullback p).obj M).presheaf.map (homOfLE (le_top : p ⁻¹ᵁ U ≤ ⊤)).op (eta p (M := M)
        ⊤ m)
lemma

ratio_pulled

L100 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_projPresentation_pullback_sigma_eq_toProj_eq.AlgebraicGeometry.Scheme.Modules.PresPre.ratio_pulled
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_projPresentation_pullback_sigma_eq_toProj_eq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresPre
variable {R : Type u} [CommRing R] {X X' : Scheme.{u}} {f : X ⟶ Spec (.of R)} (p : X' ⟶ X)
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
lemma ratio_pulled (i j : Fin (N + 1)) :
    (p.app (𝔓.toProj ⁻¹ᵁ Proj.basicOpen 𝒜R (MvPolynomial.X i))
        (𝔓.toProj.app (Proj.basicOpen 𝒜R (MvPolynomial.X i))
          (Proj.awayToSection _ (MvPolynomial.X i) (ProjSpace.ratio R N i j)))) •
      ((Modules.pullback p).obj M).presheaf.map
        (homOfLE (le_top : p ⁻¹ᵁ (𝔓.toProj ⁻¹ᵁ Proj.basicOpen 𝒜R (MvPolynomial.X i)) ≤ ⊤)).op (σ' p
          𝔓 i) =
      ((Modules.pullback p).obj M).presheaf.map
        (homOfLE (le_top : p ⁻¹ᵁ (𝔓.toProj ⁻¹ᵁ Proj.basicOpen 𝒜R (MvPolynomial.X i)) ≤ ⊤)).op (σ' p
          𝔓 j)
lemma

comp_app_ratio

L116 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_projPresentation_pullback_sigma_eq_toProj_eq.AlgebraicGeometry.Scheme.Modules.PresPre.comp_app_ratio
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_projPresentation_pullback_sigma_eq_toProj_eq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresPre
variable {R : Type u} [CommRing R] {X X' : Scheme.{u}} {f : X ⟶ Spec (.of R)} (p : X' ⟶ X)
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
lemma comp_app_ratio (i j : Fin (N + 1)) :
    (p ≫ 𝔓.toProj).app (Proj.basicOpen 𝒜R (MvPolynomial.X i))
        (Proj.awayToSection 𝒜R (MvPolynomial.X i) (ProjSpace.ratio R N i j)) =
      p.app (𝔓.toProj ⁻¹ᵁ Proj.basicOpen 𝒜R (MvPolynomial.X i))
        (𝔓.toProj.app (Proj.basicOpen 𝒜R (MvPolynomial.X i))
          (Proj.awayToSection 𝒜R (MvPolynomial.X i) (ProjSpace.ratio R N i j)))
def

precomp

L131 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_projPresentation_pullback_sigma_eq_toProj_eq.AlgebraicGeometry.Scheme.Modules.PresPre.precomp
Documentation

The projective presentation obtained by pulling back the module and precomposing its projective map.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_projPresentation_pullback_sigma_eq_toProj_eq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresPre
variable {R : Type u} [CommRing R] {X X' : Scheme.{u}} {f : X ⟶ Spec (.of R)} (p : X' ⟶ X)
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · full declaration
def precomp : ((Modules.pullback p).obj M).ProjPresentation (p ≫ f) N where
  σ := σ' p 𝔓
  toProj := p ≫ 𝔓.toProj
  toProj_π := by rw [Category.assoc, 𝔓.toProj_π]
  frame := fun i V hV =>
    bijective_smul_unit_app_of_bijective_smul p M (𝔓.σ i)
      (V := 𝔓.toProj ⁻¹ᵁ Proj.basicOpen 𝒜R (MvPolynomial.X i)) (𝔓.frame i) V
      (hV.trans (preimage_chart p 𝔓 i).le)
  app_ratio_smul := fun i j => by
    have key := ratio_pulled p 𝔓 i j
    have hc := comp_app_ratio p 𝔓 i j
    rw [hc]
    exact key
lemma

precomp_σ

L145 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_projPresentation_pullback_sigma_eq_toProj_eq.AlgebraicGeometry.Scheme.Modules.PresPre.precomp_σ
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_projPresentation_pullback_sigma_eq_toProj_eq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresPre
variable {R : Type u} [CommRing R] {X X' : Scheme.{u}} {f : X ⟶ Spec (.of R)} (p : X' ⟶ X)
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
lemma precomp_σ (i : Fin (N + 1)) :
    (precomp p 𝔓).σ i = ((pullbackPushforwardAdjunction p).unit.app M).app ⊤ (𝔓.σ i)
lemma

precomp_toProj

L148 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_projPresentation_pullback_sigma_eq_toProj_eq.AlgebraicGeometry.Scheme.Modules.PresPre.precomp_toProj
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_projPresentation_pullback_sigma_eq_toProj_eq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresPre
variable {R : Type u} [CommRing R] {X X' : Scheme.{u}} {f : X ⟶ Spec (.of R)} (p : X' ⟶ X)
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
lemma precomp_toProj : (precomp p 𝔓).toProj = p ≫ 𝔓.toProj
theorem

exists_projPresentation_pullback_sigma_eq_toProj_eq

L168 ↗
AlgebraicGeometry.Scheme.Modules.ProjPresentation.exists_projPresentation_pullback_sigma_eq_toProj_eq
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicGeometry
universe u
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs in
open Scheme_Modules_ProjPresentation_exists_projPresentation_pullback_sigma_eq_toProj_eq in
open AlgebraicGeometry.Scheme.Modules.PresPre in
Lean source · statement
theorem Scheme.Modules.ProjPresentation.exists_projPresentation_pullback_sigma_eq_toProj_eq
    {R : Type u} [CommRing R] {X X' : Scheme.{u}} {f : X ⟶ Spec (.of R)} (p : X' ⟶ X)
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N) :
    ∃ 𝔓' : ((Scheme.Modules.pullback p).obj M).ProjPresentation (p ≫ f) N,
      (∀ i, 𝔓'.σ i = (((Scheme.Modules.pullbackPushforwardAdjunction p).unit.app M).app ⊤) (𝔓.σ i))
        ∧
      𝔓'.toProj = p ≫ 𝔓.toProj

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