Module

ProjectivePresentationIso.lean

Nyll.SchemeTheory.Modules.ProjectivePresentationIso

4 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Proj Presentation exists of iso

Imports2

Imported by3

theorem

map_app

L36 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_of_iso.PresIso.map_app

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_of_iso
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite
namespace PresIso
variable {X : Scheme.{u}} {M M' : X.Modules}

Lean source · statement

theorem map_app (φ : M ⟶ M') {U V : X.Opens} (i : V ⟶ U) (s : Γ(M, U)) :
    M'.presheaf.map i.op (φ.app U s) = φ.app V (M.presheaf.map i.op s)

theorem

app_bijective

L42 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_of_iso.PresIso.app_bijective

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_of_iso
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite
namespace PresIso
variable {X : Scheme.{u}} {M M' : X.Modules}

Lean source · statement

theorem app_bijective (e : M ≅ M') (U : X.Opens) : Function.Bijective (e.hom.app U)

def

transport

L47 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_of_iso.PresIso.transport

Documentation

Transport a projective presentation across e, retaining its projective-space morphism and mapping its global sections by e.hom.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_of_iso
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite
namespace PresIso
variable {X : Scheme.{u}} {M M' : X.Modules}

Lean source · full declaration

def transport {R : Type u} [CommRing R] {f : X ⟶ Spec (.of R)} {N : ℕ}
    (𝔓 : M.ProjPresentation f N) (e : M ≅ M') : M'.ProjPresentation f N where
  σ := fun i => e.hom.app ⊤ (𝔓.σ i)
  toProj := 𝔓.toProj
  toProj_π := 𝔓.toProj_π
  frame := fun i V hV => by
    have key : (fun g : Γ(X, V) => g • M'.presheaf.map (homOfLE (le_top : V ≤ ⊤)).op (e.hom.app ⊤
      (𝔓.σ i)))
        = (e.hom.app V) ∘ (fun g : Γ(X, V) => g • M.presheaf.map (homOfLE (le_top : V ≤ ⊤)).op (𝔓.σ
          i)) := by
      funext g
      simp only [Function.comp_apply, map_app, Scheme.Modules.Hom.app_smul]
    rw [key]
    exact (app_bijective e V).comp (𝔓.frame i V hV)
  app_ratio_smul := fun i j => by
    rw [map_app, map_app, ← Scheme.Modules.Hom.app_smul, 𝔓.app_ratio_smul i j]

theorem

exists_of_iso

L66 ↗

AlgebraicGeometry.Scheme.Modules.ProjPresentation.exists_of_iso

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_of_iso
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.ProjPresentation.exists_of_iso
    {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {M M' : X.Modules} {N : ℕ}
    (𝔓 : M.ProjPresentation f N) (e : M ≅ M') :
    ∃ 𝔓' : M'.ProjPresentation f N, 𝔓'.toProj = 𝔓.toProj ∧ ∀ i, 𝔓'.σ i = (e.hom.app ⊤) (𝔓.σ i)

Module documentation

Scheme Modules Proj Presentation exists of iso

Declarations

map_app

app_bijective

transport

exists_of_iso