NYLL
Module

Scheme_Modules_ProjPresentation_mem_preimage_basicOpen_iff.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_ProjPresentation_mem_preimage_basicOpen_iff
6 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Proj Presentation mem preimage basic Open iff

Imports2
Imported by3

Declarations

lemma

isUnit_germ_ratio_iff

L53 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_mem_preimage_basicOpen_iff.AlgebraicGeometry.Scheme.Modules.PresChart.isUnit_germ_ratio_iff
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_mem_preimage_basicOpen_iff
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
universe u
open Opposite TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresChart
section chart
variable (R : Type u) [CommRing R] (N : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
lemma isUnit_germ_ratio_iff (i j : Fin (N + 1)) (y : Proj 𝒜)
    (hy : y ∈ Proj.basicOpen 𝒜 (MvPolynomial.X j)) :
    IsUnit ((Proj 𝒜).presheaf.germ (Proj.basicOpen 𝒜 (MvPolynomial.X j)) y hy
      (Proj.awayToSection 𝒜 (MvPolynomial.X j) (ProjSpace.ratio R N j i))) ↔
      y ∈ Proj.basicOpen 𝒜 (MvPolynomial.X i)
lemma

exists_mem_basicOpen_X

L79 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_mem_preimage_basicOpen_iff.AlgebraicGeometry.Scheme.Modules.PresChart.exists_mem_basicOpen_X
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_mem_preimage_basicOpen_iff
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
universe u
open Opposite TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresChart
section chart
variable (R : Type u) [CommRing R] (N : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
lemma exists_mem_basicOpen_X (y : Proj 𝒜) : ∃ j : Fin (N + 1), y ∈ Proj.basicOpen 𝒜 (MvPolynomial.X
  j)
abbrev

resTop

L98 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_mem_preimage_basicOpen_iff.AlgebraicGeometry.Scheme.Modules.PresChart.resTop
Documentation

Restriction of a presenting global module section to an open subset.

Source context 22 commands

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

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

res_resTop

L102 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_mem_preimage_basicOpen_iff.AlgebraicGeometry.Scheme.Modules.PresChart.res_resTop
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_mem_preimage_basicOpen_iff
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
universe u
open Opposite TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresChart
section pres
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {M : X.Modules} {N : ℕ}
    (𝔓 : M.ProjPresentation f N)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
omit 𝔓 in
Lean source · statement
lemma res_resTop {V W : X.Opens} (h : W ≤ V) (s : Γ(M, ⊤)) :
    M.presheaf.map (homOfLE h).op (resTop V s) = resTop W s
theorem

main

L108 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_mem_preimage_basicOpen_iff.AlgebraicGeometry.Scheme.Modules.PresChart.main
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_mem_preimage_basicOpen_iff
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
universe u
open Opposite TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresChart
section pres
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {M : X.Modules} {N : ℕ}
    (𝔓 : M.ProjPresentation f N)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · full declaration
theorem main (i : Fin (N + 1)) (x : X) :
    x ∈ 𝔓.toProj ⁻¹ᵁ Proj.basicOpen 𝒜 (MvPolynomial.X i) ↔
      ∃ U : X.Opens, x ∈ U ∧ ∀ V : X.Opens, V ≤ U →
        Function.Bijective fun g : Γ(X, V) => g • resTop V (𝔓.σ i) := by
  constructor
  · intro hx
    exact ⟨_, hx, fun V hV => 𝔓.frame i V hV⟩
  · rintro ⟨U, hxU, hU⟩
    obtain ⟨j, hj⟩ := exists_mem_basicOpen_X R N (𝔓.toProj x)
    have hxW : x ∈ U ⊓ 𝔓.toProj ⁻¹ᵁ Proj.basicOpen 𝒜 (MvPolynomial.X j) := ⟨hxU, hj⟩
    have hWU : U ⊓ 𝔓.toProj ⁻¹ᵁ Proj.basicOpen 𝒜 (MvPolynomial.X j) ≤ U := inf_le_left
    have hWj : U ⊓ 𝔓.toProj ⁻¹ᵁ Proj.basicOpen 𝒜 (MvPolynomial.X j) ≤
        𝔓.toProj ⁻¹ᵁ Proj.basicOpen 𝒜 (MvPolynomial.X j) := inf_le_right
    have hρ : X.presheaf.map (homOfLE hWj).op
        (𝔓.toProj.app (Proj.basicOpen 𝒜 (MvPolynomial.X j))
          (Proj.awayToSection 𝒜 (MvPolynomial.X j) (ProjSpace.ratio R N j i))) •
        resTop (U ⊓ 𝔓.toProj ⁻¹ᵁ Proj.basicOpen 𝒜 (MvPolynomial.X j)) (𝔓.σ j) =
        resTop (U ⊓ 𝔓.toProj ⁻¹ᵁ Proj.basicOpen 𝒜 (MvPolynomial.X j)) (𝔓.σ i) := by
      have h := congrArg (M.presheaf.map (homOfLE hWj).op) (𝔓.app_ratio_smul j i)
      rw [Modules.map_smul, res_resTop, res_resTop] at h
      exact h
    obtain ⟨g, hg⟩ := (hU _ hWU).2 (resTop (U ⊓ 𝔓.toProj ⁻¹ᵁ Proj.basicOpen 𝒜 (MvPolynomial.X j))
      (𝔓.σ j))
    dsimp only at hg
    have h1 : (g * X.presheaf.map (homOfLE hWj).op
        (𝔓.toProj.app (Proj.basicOpen 𝒜 (MvPolynomial.X j))
          (Proj.awayToSection 𝒜 (MvPolynomial.X j) (ProjSpace.ratio R N j i)))) •
        resTop (U ⊓ 𝔓.toProj ⁻¹ᵁ Proj.basicOpen 𝒜 (MvPolynomial.X j)) (𝔓.σ j) =
        (1 : Γ(X, U ⊓ 𝔓.toProj ⁻¹ᵁ Proj.basicOpen 𝒜 (MvPolynomial.X j))) •
          resTop (U ⊓ 𝔓.toProj ⁻¹ᵁ Proj.basicOpen 𝒜 (MvPolynomial.X j)) (𝔓.σ j) := by
      rw [mul_smul, hρ, hg, one_smul]
    have hunit : IsUnit (X.presheaf.map (homOfLE hWj).op
        (𝔓.toProj.app (Proj.basicOpen 𝒜 (MvPolynomial.X j))
          (Proj.awayToSection 𝒜 (MvPolynomial.X j) (ProjSpace.ratio R N j i)))) := by
      refine isUnit_iff_exists_inv.mpr ⟨g, ?_⟩
      rw [mul_comm]
      exact (𝔓.frame j _ hWj).1 h1
    have hgerm : IsUnit (X.presheaf.germ _ x hxW (X.presheaf.map (homOfLE hWj).op
        (𝔓.toProj.app (Proj.basicOpen 𝒜 (MvPolynomial.X j))
          (Proj.awayToSection 𝒜 (MvPolynomial.X j) (ProjSpace.ratio R N j i))))) := hunit.map _
    rw [TopCat.Presheaf.germ_res_apply] at hgerm
    have hgerm' : IsUnit (X.presheaf.germ (𝔓.toProj ⁻¹ᵁ Proj.basicOpen 𝒜 (MvPolynomial.X j)) x hj
        (𝔓.toProj.app (Proj.basicOpen 𝒜 (MvPolynomial.X j))
          (Proj.awayToSection 𝒜 (MvPolynomial.X j) (ProjSpace.ratio R N j i)))) := hgerm
    rw [← Scheme.Hom.germ_stalkMap_apply] at hgerm'
    have : IsLocalHom (ConcreteCategory.hom (𝔓.toProj.stalkMap x)) :=
      inferInstanceAs (IsLocalHom (𝔓.toProj.stalkMap x).hom)
    rw [isUnit_map_iff] at hgerm'
    exact (isUnit_germ_ratio_iff R N i j _ hj).mp hgerm'
theorem

mem_preimage_basicOpen_iff

L164 ↗
AlgebraicGeometry.Scheme.Modules.ProjPresentation.mem_preimage_basicOpen_iff
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_mem_preimage_basicOpen_iff
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
universe u
open Opposite TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · full declaration
theorem _root_.AlgebraicGeometry.Scheme.Modules.ProjPresentation.mem_preimage_basicOpen_iff
    {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} {M : X.Modules} {N : ℕ}
    (𝔓 : M.ProjPresentation f N) (i : Fin (N + 1)) (x : X) :
    x ∈ 𝔓.toProj ⁻¹ᵁ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)
      (MvPolynomial.X i) ↔
      ∃ U : X.Opens, x ∈ U ∧ ∀ V : X.Opens, V ≤ U →
        Function.Bijective fun g : Γ(X, V) => g • (M.presheaf.map (homOfLE (le_top : V ≤ ⊤)).op
          (𝔓.σ i) : Γ(M, V)) :=
  AlgebraicGeometry.Scheme.Modules.PresChart.main 𝔓 i x

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