Module

Basic.lean

Nyll.SchemeTheory.ProjectiveSpace.Basic

33 declarations indexed from sourceView source ↗

Module documentation

Projective space and its standard charts

Projective space is constructed from graded polynomial rings together with its standard affine charts, maps and fibre products. Chow data records the resulting projective compactification constructions.

Imports5

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.RingTheory.MvPolynomial.Homogeneous
Mathlib.RingTheory.MvPolynomial.Ideal

Imported by92

def

grad0Equiv

L46 ↗

AlgebraicGeometry.ProjSpace.grad0Equiv

Documentation

The identification of the degree zero homogeneous polynomials with the coefficient ring.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section PnSetup
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R

Lean source · full declaration

def grad0Equiv : R ≃+* (𝒜 0) where
  toFun r := ⟨C r, (mem_homogeneousSubmodule 0 _).mpr (isHomogeneous_C _ r)⟩
  invFun p := MvPolynomial.constantCoeff p.1
  left_inv r := by simp
  right_inv p := by
    ext : 1
    have hp : p.1.IsHomogeneous 0 := (mem_homogeneousSubmodule 0 _).mp p.2
    ext d
    rcases eq_or_ne d 0 with rfl | hd
    · simp [MvPolynomial.constantCoeff]
    · rw [MvPolynomial.coeff_C, ite_eq_right (Ne.symm hd)]
      by_contra h
      refine hd (Finsupp.ext fun i => ?_)
      have hdeg : (Finsupp.weight (1 : Fin (n + 1) → ℕ)) d = 0 := hp (fun h0 => h h0.symm)
      simp only [Finsupp.weight_apply, Pi.one_apply, smul_eq_mul, mul_one,
        Finsupp.sum] at hdeg
      by_cases hi : i ∈ d.support
      · exact (Finset.sum_eq_zero_iff_of_nonneg (fun _ _ => Nat.zero_le _)).mp hdeg i hi
      · exact Finsupp.notMem_support_iff.mp hi
  map_mul' a b := by ext : 1; simp
  map_add' a b := by ext : 1; simp

def

π

L69 ↗

AlgebraicGeometry.ProjSpace.π

Documentation

The structure morphism of projective space to the coefficient spectrum.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section PnSetup
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R

Lean source · statement

def π : Proj 𝒜 ⟶ Spec (.of R)

instance

finiteType_mvPolynomial

L72 ↗

AlgebraicGeometry.ProjSpace.finiteType_mvPolynomial

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section PnSetup
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R

Lean source · statement

instance finiteType_mvPolynomial :
    Algebra.FiniteType (𝒜 0) (MvPolynomial (Fin (n + 1)) R)

instance

isProper_π

L85 ↗

AlgebraicGeometry.ProjSpace.isProper_π

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section PnSetup
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R

Lean source · statement

instance isProper_π : IsProper (π R n)

theorem

irrelevant_le_span_X

L106 ↗

AlgebraicGeometry.ProjSpace.irrelevant_le_span_X

Source context 11 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section StdCover
open MvPolynomial AlgebraicGeometry.Proj
variable (R : Type u) [CommRing R] (n : ℕ)
attribute [local instance] MvPolynomial.gradedAlgebra
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R

Lean source · statement

theorem irrelevant_le_span_X :
    (HomogeneousIdeal.irrelevant 𝒜).toIdeal
      ≤ Ideal.span (Set.range (MvPolynomial.X : Fin (n + 1) → MvPolynomial _ R))

theorem

X_mem_one

L128 ↗

AlgebraicGeometry.ProjSpace.X_mem_one

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section Setup
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R

Lean source · statement

theorem X_mem_one (j : Fin (n + 1)) :
    (MvPolynomial.X j : MvPolynomial (Fin (n + 1)) R) ∈ 𝒜 1

instance

algebraAway

L132 ↗

AlgebraicGeometry.ProjSpace.algebraAway

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section Setup
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R

Lean source · statement

instance algebraAway (i : Fin (n + 1)) :
    Algebra R (Away 𝒜 (MvPolynomial.X i))

theorem

awayι_comp_π

L137 ↗

AlgebraicGeometry.ProjSpace.awayι_comp_π

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section Setup
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R

Lean source · statement

theorem awayι_comp_π (i : Fin (n + 1)) :
    Proj.awayι 𝒜 (MvPolynomial.X i) (X_mem_one R n i) one_pos
      ≫ π R n
      = Spec.map (CommRingCat.ofHom (algebraMap R (Away 𝒜 (MvPolynomial.X i))))

def

ratio

L146 ↗

AlgebraicGeometry.ProjSpace.ratio

Documentation

The ratio of two homogeneous coordinate variables on the standard affine chart.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section Setup
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R

Lean source · statement

def ratio (i k : Fin (n + 1)) : Away 𝒜 (MvPolynomial.X i)

theorem

ratio_self

L150 ↗

AlgebraicGeometry.ProjSpace.ratio_self

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section Setup
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R

Lean source · statement

theorem ratio_self (i : Fin (n + 1)) :
    ratio R n i i = 1

theorem

val_algebraMap

L157 ↗

AlgebraicGeometry.ProjSpace.val_algebraMap

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section Setup
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R

Lean source · statement

theorem val_algebraMap (i : Fin (n + 1)) (r : R) :
    (algebraMap R (Away 𝒜 (MvPolynomial.X i)) r).val
      = algebraMap (MvPolynomial (Fin (n + 1)) R) _ (MvPolynomial.C r)

def

affineOpenCover

L171 ↗

AlgebraicGeometry.ProjSpace.affineOpenCover

Documentation

The standard affine cover of projective space by its homogeneous coordinate charts.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section StdCover
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R

Lean source · statement

def affineOpenCover : (Proj 𝒜).AffineOpenCover

theorem

affineOpenCover_f

L176 ↗

AlgebraicGeometry.ProjSpace.affineOpenCover_f

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section StdCover
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R

Lean source · statement

theorem affineOpenCover_f (j : Fin (n + 1)) :
    (affineOpenCover R n).openCover.f j
      = Proj.awayι 𝒜 (MvPolynomial.X j) (X_mem_one R n j) one_pos

theorem

awayMk_monomial

L188 ↗

AlgebraicGeometry.ProjSpace.awayMk_monomial

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section AdjoinRatio
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R

Lean source · statement

theorem awayMk_monomial (i : Fin (n + 1)) (d : ℕ)
    (e : Fin (n + 1) →₀ ℕ) (hd : e.degree = d) (r : R)
    (hm : MvPolynomial.monomial e r ∈ 𝒜 (d • 1)) :
    Away.mk 𝒜 (X_mem_one R n i) d (MvPolynomial.monomial e r) hm
      = algebraMap R _ r * ∏ j, (ratio R n i j) ^ (e j)

theorem

adjoin_range_ratio

L210 ↗

AlgebraicGeometry.ProjSpace.adjoin_range_ratio

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section AdjoinRatio
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R

Lean source · statement

theorem adjoin_range_ratio (i : Fin (n + 1)) :
    Algebra.adjoin R (Set.range (ratio R n i)) = ⊤

def

prodOverAux

L252 ↗

AlgebraicGeometry.ProjSpace.prodOverAux

Documentation

The recursively constructed product of projective spaces together with its structure morphism.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section ProdOver
variable (R : Type u) [CommRing R]

Lean source · full declaration

def prodOverAux :
    ∀ {m : ℕ}, (Fin m → ℕ) → Σ (P : Scheme.{u}), P ⟶ Spec (.of R)
  | 0, _ => ⟨Spec (.of R), 𝟙 _⟩
  | m + 1, e =>
    let prev := @prodOverAux m (e ∘ Fin.succ)
    ⟨pullback (π R (e 0)) prev.2,
     pullback.fst _ _ ≫ π R (e 0)⟩

abbrev

prodOver

L261 ↗

AlgebraicGeometry.ProjSpace.prodOver

Documentation

The product over the coefficient spectrum of the indexed projective spaces.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section ProdOver
variable (R : Type u) [CommRing R]

Lean source · statement

abbrev prodOver {m : ℕ} (e : Fin m → ℕ) : Scheme.{u}

abbrev

prodOverπ

L265 ↗

AlgebraicGeometry.ProjSpace.prodOverπ

Documentation

The structure morphism of the indexed product of projective spaces.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section ProdOver
variable (R : Type u) [CommRing R]

Lean source · statement

abbrev prodOverπ {m : ℕ} (e : Fin m → ℕ) :
    prodOver R e ⟶ Spec (.of R)

theorem

isProper_prodOverπ

L269 ↗

AlgebraicGeometry.ProjSpace.isProper_prodOverπ

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section ProdOver
variable (R : Type u) [CommRing R]

Lean source · statement

theorem isProper_prodOverπ {m : ℕ} (e : Fin m → ℕ) :
    IsProper (prodOverπ R e)

instance

instIsProperProdOverπ

L278 ↗

AlgebraicGeometry.ProjSpace.instIsProperProdOverπ

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section ProdOver
variable (R : Type u) [CommRing R]

Lean source · statement

instance instIsProperProdOverπ {m : ℕ} (e : Fin m → ℕ) : IsProper (prodOverπ R e)

def

prodPr

L282 ↗

AlgebraicGeometry.ProjSpace.prodPr

Documentation

The projection from the indexed product to the indicated projective space.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section ProdOver
variable (R : Type u) [CommRing R]

Lean source · full declaration

def prodPr :
    ∀ {m : ℕ} (e : Fin m → ℕ) (k : Fin m),
      prodOver R e ⟶
        Proj (MvPolynomial.homogeneousSubmodule (Fin (e k + 1)) R)
  | _m + 1, _e, ⟨0, _⟩ => pullback.fst _ _
  | _m + 1, e, ⟨k + 1, hk⟩ =>
    pullback.snd _ _ ≫ prodPr (e ∘ Fin.succ) ⟨k, Nat.succ_lt_succ_iff.mp hk⟩

theorem

prodPr_comp_π

L290 ↗

AlgebraicGeometry.ProjSpace.prodPr_comp_π

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section ProdOver
variable (R : Type u) [CommRing R]

Lean source · statement

theorem prodPr_comp_π {m : ℕ} (e : Fin m → ℕ) (k : Fin m) :
    prodPr R e k ≫ π R (e k) = prodOverπ R e

def

prodLiftAux

L310 ↗

AlgebraicGeometry.ProjSpace.prodLiftAux

Documentation

The recursively constructed product lift together with its compatibility with the base morphism.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section ProdOver
variable (R : Type u) [CommRing R]

Lean source · full declaration

def prodLiftAux {X : Scheme.{u}} (s : X ⟶ Spec (.of R)) :
    ∀ {m : ℕ} (e : Fin m → ℕ)
      (g : ∀ k, X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (e k + 1)) R))
      (_ : ∀ k, g k ≫ π R (e k) = s),
      Σ' (l : X ⟶ prodOver R e), l ≫ prodOverπ R e = s
  | 0, _, _, _ => ⟨s, Category.comp_id s⟩
  | m + 1, e, g, hg =>
    let prev := @prodLiftAux X s m (e ∘ Fin.succ)
      (fun k => g k.succ) (fun k => hg k.succ)
    ⟨pullback.lift (g 0) prev.1 (by rw [hg 0, prev.2]),
     by
      change pullback.lift (g 0) prev.1 _ ≫ pullback.fst _ _ ≫ π R (e 0) = s
      rw [← Category.assoc, pullback.lift_fst]; exact hg 0⟩

def

prodLift

L325 ↗

AlgebraicGeometry.ProjSpace.prodLift

Documentation

The product lift determined by morphisms to each projective factor over the same base.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section ProdOver
variable (R : Type u) [CommRing R]

Lean source · statement

def prodLift {X : Scheme.{u}} (s : X ⟶ Spec (.of R)) {m : ℕ} (e : Fin m → ℕ)
    (g : ∀ k, X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (e k + 1)) R))
    (hg : ∀ k, g k ≫ π R (e k) = s) :
    X ⟶ prodOver R e

theorem

prodLift_comp_prodOverπ

L331 ↗

AlgebraicGeometry.ProjSpace.prodLift_comp_prodOverπ

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section ProdOver
variable (R : Type u) [CommRing R]

Lean source · statement

theorem prodLift_comp_prodOverπ {X : Scheme.{u}} (s : X ⟶ Spec (.of R))
    {m : ℕ} (e : Fin m → ℕ)
    (g : ∀ k, X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (e k + 1)) R))
    (hg : ∀ k, g k ≫ π R (e k) = s) :
    prodLift R s e g hg ≫ prodOverπ R e = s

theorem

prodLift_comp_prodPr

L338 ↗

AlgebraicGeometry.ProjSpace.prodLift_comp_prodPr

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section ProdOver
variable (R : Type u) [CommRing R]

Lean source · statement

theorem prodLift_comp_prodPr {X : Scheme.{u}} (s : X ⟶ Spec (.of R))
    {m : ℕ} (e : Fin m → ℕ)
    (g : ∀ k, X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (e k + 1)) R))
    (hg : ∀ k, g k ≫ π R (e k) = s) (k : Fin m) :
    prodLift R s e g hg ≫ prodPr R e k = g k

def

mvMapGraded

L365 ↗

AlgebraicGeometry.ProjSpace.mvMapGraded

Documentation

The graded polynomial homomorphism induced by extending the coefficient ring.

Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section MapGraded
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · full declaration

def mvMapGraded : 𝒜R →+*ᵍ 𝒜A where
  toRingHom := MvPolynomial.map (algebraMap R A)
  map_mem hx := (mem_homogeneousSubmodule _ _).mpr (((mem_homogeneousSubmodule _ _).mp hx).map _)

theorem

mvMapGraded_X

L369 ↗

AlgebraicGeometry.ProjSpace.mvMapGraded_X

Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section MapGraded
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · statement

theorem mvMapGraded_X (j : Fin (n + 1)) :
    (mvMapGraded R A n) (MvPolynomial.X j) = MvPolynomial.X j

theorem

irrelevant_le_map_mvMapGraded

L373 ↗

AlgebraicGeometry.ProjSpace.irrelevant_le_map_mvMapGraded

Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section MapGraded
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · statement

theorem irrelevant_le_map_mvMapGraded :
    (HomogeneousIdeal.irrelevant 𝒜A)
      ≤ HomogeneousIdeal.map (mvMapGraded R A n)
          (HomogeneousIdeal.irrelevant 𝒜R)

def

map

L407 ↗

AlgebraicGeometry.ProjSpace.map

Documentation

The morphism of projective spaces induced by extending the coefficient ring.

Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section MapGraded
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · statement

def map : Proj 𝒜A ⟶ Proj 𝒜R

theorem

map_eq

L410 ↗

AlgebraicGeometry.ProjSpace.map_eq

Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section MapGraded
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · statement

theorem map_eq : map R A n = Proj.map (mvMapGraded R A n) (irrelevant_le_map_mvMapGraded R A n)

structure

ChowDatum

L423 ↗

AlgebraicGeometry.ChowDatum

Documentation

A proper modification with a closed immersion into a product of projective spaces and a dense open where the modification is an isomorphism.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Carrier
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))

Lean source · full declaration

structure ChowDatum where
  /-- The number of projective space factors. -/
  m : ℕ
  /-- The dimension of each projective space factor. -/
  e : Fin m → ℕ
  /-- The modifying scheme. -/
  V' : Scheme.{u}
  /-- The modification morphism to the original scheme. -/
  p : V' ⟶ V
  /-- The immersion into the product of projective spaces. -/
  ι : V' ⟶ ProjSpace.prodOver R e
  /-- The modification morphism is proper. -/
  hp_proper : IsProper p
  /-- The product immersion is closed. -/
  hι_closed : IsClosedImmersion ι
  /-- The product immersion and modification commute with the base morphisms. -/
  hover : ι ≫ ProjSpace.prodOverπ R e = p ≫ π
  /-- The open subset where the modification is an isomorphism. -/
  U : V.Opens
  /-- The selected open subset is dense. -/
  hU_dense : Dense (U : Set V)
  /-- The modification restricted over the selected open is an isomorphism. -/
  hp_isoU : IsIso (pullback.snd p U.ι)

structure

ChowDatumProj

L457 ↗

AlgebraicGeometry.ChowDatumProj

Documentation

A proper modification with a closed immersion into one projective space and a dense open where the modification is an isomorphism.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section CarrierProj
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))

Lean source · full declaration

structure ChowDatumProj where
  /-- The dimension of the projective space. -/
  Nd : ℕ
  /-- The modifying scheme. -/
  V' : Scheme.{u}
  /-- The modification morphism to the original scheme. -/
  p : V' ⟶ V
  /-- The immersion into projective space. -/
  ιN : V' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (Nd + 1)) R)
  /-- The modification morphism is proper. -/
  hp_proper : IsProper p
  /-- The projective space immersion is closed. -/
  hιN_closed : IsClosedImmersion ιN
  /-- The projective space immersion and modification commute with the base morphisms. -/
  hoverN : ιN ≫ ProjSpace.π R Nd = p ≫ π
  /-- The open subset where the modification is an isomorphism. -/
  U : V.Opens
  /-- The selected open subset is dense. -/
  hU_dense : Dense (U : Set V)
  /-- The modification restricted over the selected open is an isomorphism. -/
  hp_isoU : IsIso (pullback.snd p U.ι)

Module documentation

Projective space and its standard charts

Declarations