NYLL
Module

ChowDatumProj_nonempty_of.lean

Nyll.SchemeTheory.Morphisms.ChowDatumProj_nonempty_of
54 declarations indexed from sourceView source ↗

Module documentation

Segre embeddings and projective Chow data for proper schemes.

Imports10
  • Nyll.SchemeTheory.ProjectiveSpace.Basic
  • Nyll.SchemeTheory.Morphisms.ChowDatum_nonempty
  • Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  • Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
  • Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
  • Mathlib.AlgebraicGeometry.ZariskisMainTheorem
  • Mathlib.AlgebraicGeometry.Noetherian
  • Mathlib.AlgebraicGeometry.Birational.RationalMap
  • Mathlib.AlgebraicGeometry.Morphisms.Proper
  • Mathlib.RingTheory.TensorProduct.Basic
Imported by3

Declarations

abbrev

bigN

L54 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.bigN
Documentation

The dimension of the projective space containing the Segre embedding.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ChartHom
variable (R : Type u) [CommRing R] (n p : ℕ)
Lean source · statement
abbrev bigN : ℕ
theorem

bigN_succ

L56 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.bigN_succ
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ChartHom
variable (R : Type u) [CommRing R] (n p : ℕ)
Lean source · statement
theorem bigN_succ :
    (n + 1) * (p + 1) = bigN n p + 1
def

idx

L62 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.idx
Documentation

Identify pairs of homogeneous-coordinate indices with Segre-coordinate indices.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ChartHom
variable (R : Type u) [CommRing R] (n p : ℕ)
Lean source · statement
def idx : Fin (n + 1) × Fin (p + 1) ≃ Fin (bigN n p + 1)
abbrev

Tij

L73 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.Tij
Documentation

The coordinate ring of a product of two standard affine charts.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ChartHom
variable (R : Type u) [CommRing R] (n p : ℕ)
variable (i : Fin (n + 1)) (j : Fin (p + 1))
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
abbrev Tij : Type u
def

preSegre

L80 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.preSegre
Documentation

Send each Segre coordinate to the tensor product of the corresponding chart ratios.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ChartHom
variable (R : Type u) [CommRing R] (n p : ℕ)
variable (i : Fin (n + 1)) (j : Fin (p + 1))
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "Aˣ" => Away 𝒜ˣ (MvPolynomial.X i)
local notation "Aʸ" => Away 𝒜ʸ (MvPolynomial.X j)
Lean source · statement
def preSegre : MvPolynomial (Fin (N + 1)) R →ₐ[R] (Aˣ ⊗[R] Aʸ)
theorem

preSegre_apply

L85 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.preSegre_apply
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ChartHom
variable (R : Type u) [CommRing R] (n p : ℕ)
variable (i : Fin (n + 1)) (j : Fin (p + 1))
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "Aˣ" => Away 𝒜ˣ (MvPolynomial.X i)
local notation "Aʸ" => Away 𝒜ʸ (MvPolynomial.X j)
Lean source · statement
theorem preSegre_apply (k : Fin (n + 1)) (l : Fin (p + 1)) :
    preSegre R n p i j (MvPolynomial.X (idx n p (k, l)))
      = ((ProjSpace.ratio R n i k) ⊗ₜ[R] (ProjSpace.ratio R p j l) :
          Aˣ ⊗[R] Aʸ)
theorem

preSegre_unit

L92 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.preSegre_unit
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ChartHom
variable (R : Type u) [CommRing R] (n p : ℕ)
variable (i : Fin (n + 1)) (j : Fin (p + 1))
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "Aˣ" => Away 𝒜ˣ (MvPolynomial.X i)
local notation "Aʸ" => Away 𝒜ʸ (MvPolynomial.X j)
Lean source · statement
theorem preSegre_unit :
    (preSegre R n p i j).toRingHom
        (MvPolynomial.X (idx n p (i, j))) = 1
theorem

preSegre_mulone

L99 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.preSegre_mulone
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ChartHom
variable (R : Type u) [CommRing R] (n p : ℕ)
variable (i : Fin (n + 1)) (j : Fin (p + 1))
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "Aˣ" => Away 𝒜ˣ (MvPolynomial.X i)
local notation "Aʸ" => Away 𝒜ʸ (MvPolynomial.X j)
Lean source · statement
theorem preSegre_mulone :
    (preSegre R n p i j).toRingHom
        (X (idx n p (i, j))) * 1 = 1
def

segreLift

L105 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.segreLift
Documentation

Extend the Segre coordinate map to the chosen localized polynomial ring.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ChartHom
variable (R : Type u) [CommRing R] (n p : ℕ)
variable (i : Fin (n + 1)) (j : Fin (p + 1))
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "Aˣ" => Away 𝒜ˣ (MvPolynomial.X i)
local notation "Aʸ" => Away 𝒜ʸ (MvPolynomial.X j)
Lean source · statement
def segreLift :
    Localization.Away (X (idx n p (i, j)) :
      MvPolynomial (Fin (N + 1)) R) →+* Tij R n p i j
def

segreChart

L115 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.segreChart
Documentation

The ring map defining the Segre embedding on a standard affine chart.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ChartHom
variable (R : Type u) [CommRing R] (n p : ℕ)
variable (i : Fin (n + 1)) (j : Fin (p + 1))
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "Aˣ" => Away 𝒜ˣ (MvPolynomial.X i)
local notation "Aʸ" => Away 𝒜ʸ (MvPolynomial.X j)
Lean source · statement
def segreChart :
    Away 𝒜ᶻ (MvPolynomial.X (idx n p (i, j)))
      →+* Tij R n p i j
theorem

segreChart_ratio

L122 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.segreChart_ratio
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ChartHom
variable (R : Type u) [CommRing R] (n p : ℕ)
variable (i : Fin (n + 1)) (j : Fin (p + 1))
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "Aˣ" => Away 𝒜ˣ (MvPolynomial.X i)
local notation "Aʸ" => Away 𝒜ʸ (MvPolynomial.X j)
Lean source · statement
theorem segreChart_ratio (k : Fin (n + 1)) (l : Fin (p + 1)) :
    segreChart R n p i j
        (ProjSpace.ratio R N (idx n p (i, j))
          (idx n p (k, l)))
      = ((ProjSpace.ratio R n i k) ⊗ₜ[R] (ProjSpace.ratio R p j l) :
          Tij R n p i j)
theorem

segreChart_algebraMap

L134 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.segreChart_algebraMap
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ChartHom
variable (R : Type u) [CommRing R] (n p : ℕ)
variable (i : Fin (n + 1)) (j : Fin (p + 1))
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "Aˣ" => Away 𝒜ˣ (MvPolynomial.X i)
local notation "Aʸ" => Away 𝒜ʸ (MvPolynomial.X j)
Lean source · statement
theorem segreChart_algebraMap (r : R) :
    segreChart R n p i j
        (algebraMap R (Away 𝒜ᶻ (X (idx n p (i, j)))) r)
      = ((1 : Aˣ) ⊗ₜ[R] algebraMap R Aʸ r : Aˣ ⊗[R] Aʸ)
theorem

segreChart_surjective

L146 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.segreChart_surjective
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ChartHom
variable (R : Type u) [CommRing R] (n p : ℕ)
variable (i : Fin (n + 1)) (j : Fin (p + 1))
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "Aˣ" => Away 𝒜ˣ (MvPolynomial.X i)
local notation "Aʸ" => Away 𝒜ʸ (MvPolynomial.X j)
Lean source · statement
theorem segreChart_surjective :
    Function.Surjective (segreChart R n p i j)
theorem

comp_SpecMap_eq_iff

L201 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.comp_SpecMap_eq_iff
Documentation

Naturality of the global-sections description of maps to affine schemes, in both directions. The source scheme is arbitrary; the two affine targets and their maps may differ.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
Lean source · statement
theorem comp_SpecMap_eq_iff {W : Scheme.{u}} {A B C : Type u}
    [CommRing A] [CommRing B] [CommRing C]
    (f : W ⟶ Spec (.of B)) (g : W ⟶ Spec (.of C))
    (φ : A →+* B) (ψ : A →+* C) :
    f ≫ Spec.map (CommRingCat.ofHom φ) = g ≫ Spec.map (CommRingCat.ofHom ψ) ↔
      (((Scheme.ΓSpecIso (.of B)).inv ≫ f.appTop).hom).comp φ =
        (((Scheme.ΓSpecIso (.of C)).inv ≫ g.appTop).hom).comp ψ
def

prodCover

L235 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.prodCover
Documentation

The product affine cover induced by the standard covers of the two projective spaces.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ProductCover
variable (R : Type u) [CommRing R] (n p : ℕ)
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
def prodCover :
    (pullback (ProjSpace.π R n) (ProjSpace.π R p)).OpenCover
def

chartInclusion

L241 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.chartInclusion
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ProductCover
variable (R : Type u) [CommRing R] (n p : ℕ)
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
def chartInclusion (i : Fin (n + 1)) (j : Fin (p + 1)) :
    pullback
        (Proj.awayι 𝒜ˣ (X i) (ProjSpace.X_mem_one R n i) one_pos ≫ ProjSpace.π R n)
        (Proj.awayι 𝒜ʸ (X j) (ProjSpace.X_mem_one R p j) one_pos ≫ ProjSpace.π R p)
      ⟶ pullback (ProjSpace.π R n) (ProjSpace.π R p)
instance

chartInclusion_isOpenImmersion

L251 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.chartInclusion_isOpenImmersion
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ProductCover
variable (R : Type u) [CommRing R] (n p : ℕ)
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
instance chartInclusion_isOpenImmersion (i : Fin (n + 1)) (j : Fin (p + 1)) :
    IsOpenImmersion (chartInclusion R n p i j)
def

chartIso

L257 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.chartIso
Documentation

Identify a product chart with the spectrum of its tensor-product coordinate ring.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ProductCover
variable (R : Type u) [CommRing R] (n p : ℕ)
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
def chartIso (i : Fin (n + 1)) (j : Fin (p + 1)) :
    pullback ((Proj.awayι 𝒜ˣ (X i) (ProjSpace.X_mem_one R n i) one_pos) ≫ ProjSpace.π R n)
      ((Proj.awayι 𝒜ʸ (X j) (ProjSpace.X_mem_one R p j) one_pos) ≫ ProjSpace.π R p)
      ≅ Spec (.of <| (Away 𝒜ˣ (X i)) ⊗[R] (Away 𝒜ʸ (X j)))
def

chartMap

L265 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.chartMap
Documentation

The local Segre morphism on a product chart.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ProductCover
variable (R : Type u) [CommRing R] (n p : ℕ)
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
def chartMap (i : Fin (n + 1)) (j : Fin (p + 1)) :
    pullback ((Proj.awayι 𝒜ˣ (X i) (ProjSpace.X_mem_one R n i) one_pos) ≫ ProjSpace.π R n)
      ((Proj.awayι 𝒜ʸ (X j) (ProjSpace.X_mem_one R p j) one_pos) ≫ ProjSpace.π R p) ⟶ Proj 𝒜ᶻ
theorem

chartMap_over

L273 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.chartMap_over
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ProductCover
variable (R : Type u) [CommRing R] (n p : ℕ)
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
theorem chartMap_over (ij : Fin (n + 1) × Fin (p + 1)) :
    chartMap R n p ij.1 ij.2 ≫ ProjSpace.π R N
      = chartInclusion R n p ij.1 ij.2
          ≫ pullback.fst _ _ ≫ ProjSpace.π R n
theorem

prodCover_fst

L320 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.prodCover_fst
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ProductCover
variable (R : Type u) [CommRing R] (n p : ℕ)
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
theorem prodCover_fst (ij : Fin (n + 1) × Fin (p + 1)) :
    chartInclusion R n p ij.1 ij.2 ≫ pullback.fst _ _
      = (pullback.fst _ _ : pullback ((Proj.awayι 𝒜ˣ (X ij.1) (ProjSpace.X_mem_one R n ij.1)
          one_pos) ≫ ProjSpace.π R n)
      ((Proj.awayι 𝒜ʸ (X ij.2) (ProjSpace.X_mem_one R p ij.2) one_pos) ≫ ProjSpace.π R p) ⟶ _)
        ≫ Proj.awayι 𝒜ˣ (X ij.1) (ProjSpace.X_mem_one R n ij.1) one_pos
theorem

prodCover_snd

L330 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.prodCover_snd
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ProductCover
variable (R : Type u) [CommRing R] (n p : ℕ)
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
theorem prodCover_snd (ij : Fin (n + 1) × Fin (p + 1)) :
    chartInclusion R n p ij.1 ij.2 ≫ pullback.snd _ _
      = (pullback.snd _ _ : pullback ((Proj.awayι 𝒜ˣ (X ij.1) (ProjSpace.X_mem_one R n ij.1)
          one_pos) ≫ ProjSpace.π R n)
      ((Proj.awayι 𝒜ʸ (X ij.2) (ProjSpace.X_mem_one R p ij.2) one_pos) ≫ ProjSpace.π R p) ⟶ _)
        ≫ Proj.awayι 𝒜ʸ (X ij.2) (ProjSpace.X_mem_one R p ij.2) one_pos
theorem

chartIso_incL

L340 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.chartIso_incL
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ProductCover
variable (R : Type u) [CommRing R] (n p : ℕ)
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
theorem chartIso_incL (i : Fin (n + 1)) (j : Fin (p + 1)) :
    (chartIso R n p i j).hom
        ≫ Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.includeLeftRingHom
            (A := Away 𝒜ˣ (X i)) (B := Away 𝒜ʸ (X j))))
      = pullback.fst _ _
theorem

chartIso_incR

L351 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.chartIso_incR
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ProductCover
variable (R : Type u) [CommRing R] (n p : ℕ)
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
theorem chartIso_incR (i : Fin (n + 1)) (j : Fin (p + 1)) :
    (chartIso R n p i j).hom
        ≫ Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.includeRight
            (R := R) (A := Away 𝒜ˣ (X i)) (B := Away 𝒜ʸ (X j))).toRingHom)
      = pullback.snd _ _
theorem

isLocElem_ratio

L361 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.isLocElem_ratio
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ProductCover
variable (R : Type u) [CommRing R] (n p : ℕ)
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
theorem isLocElem_ratio (i k : Fin (n + 1)) :
    HomogeneousLocalization.Away.isLocalizationElem
        (ProjSpace.X_mem_one R n i) (ProjSpace.X_mem_one R n k)
      = ProjSpace.ratio R n i k
theorem

segreChart_preimage_ratio

L371 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.segreChart_preimage_ratio
Documentation

On an affine Segre chart, a coordinate basic open pulls back to the intersection of the corresponding basic opens in the two factors.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ProductCover
variable (R : Type u) [CommRing R] (n p : ℕ)
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
theorem segreChart_preimage_ratio (i k : Fin (n + 1)) (j l : Fin (p + 1)) :
    Spec.map (CommRingCat.ofHom (segreChart R n p i j))
        ⁻¹ᵁ PrimeSpectrum.basicOpen
          (ProjSpace.ratio R N (idx n p (i, j)) (idx n p (k, l)))
      = Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.includeLeftRingHom
          (R := R) (A := Away 𝒜ˣ (X i)) (B := Away 𝒜ʸ (X j))))
          ⁻¹ᵁ PrimeSpectrum.basicOpen (ProjSpace.ratio R n i k)
        ⊓ Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.includeRight
            (R := R) (A := Away 𝒜ˣ (X i)) (B := Away 𝒜ʸ (X j))).toRingHom)
          ⁻¹ᵁ PrimeSpectrum.basicOpen (ProjSpace.ratio R p j l)
theorem

range_SpecMap_awayMap

L403 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.range_SpecMap_awayMap
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ProductCover
variable (R : Type u) [CommRing R] (n p : ℕ)
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
theorem range_SpecMap_awayMap (i k : Fin (n + 1)) :
    Set.range (Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜ˣ
        (ProjSpace.X_mem_one R n k)
        (rfl : (X i * X k : MvPolynomial (Fin (n+1)) R) = X i * X k)))).base
      = (PrimeSpectrum.basicOpen (ProjSpace.ratio R n i k)
          : Set (PrimeSpectrum (Away 𝒜ˣ (X i))))
theorem

opensRange_prodCover_f

L416 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.opensRange_prodCover_f
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ProductCover
variable (R : Type u) [CommRing R] (n p : ℕ)
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
theorem opensRange_prodCover_f (α : Fin (n + 1) × Fin (p + 1)) :
    (chartInclusion R n p α.1 α.2).opensRange
      = pullback.fst (ProjSpace.π R n) (ProjSpace.π R p)
          ⁻¹ᵁ (Proj.awayι 𝒜ˣ (X α.1) (ProjSpace.X_mem_one R n α.1) one_pos).opensRange
        ⊓ pullback.snd (ProjSpace.π R n) (ProjSpace.π R p)
          ⁻¹ᵁ (Proj.awayι 𝒜ʸ (X α.2) (ProjSpace.X_mem_one R p α.2) one_pos).opensRange
theorem

awayMap_ratio_transition

L434 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.awayMap_ratio_transition
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ProductCover
variable (R : Type u) [CommRing R] (n p : ℕ)
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
theorem awayMap_ratio_transition (i k a : Fin (n + 1)) :
    (HomogeneousLocalization.awayMap 𝒜ˣ (ProjSpace.X_mem_one R n i)
        (mul_comm (X i) (X k) : (X i * X k : MvPolynomial (Fin (n+1)) R) = X k * X i))
      (ProjSpace.ratio R n k a)
    * (HomogeneousLocalization.awayMap 𝒜ˣ (ProjSpace.X_mem_one R n k)
        (rfl : (X i * X k : MvPolynomial (Fin (n+1)) R) = X i * X k))
      (ProjSpace.ratio R n i k)
    = (HomogeneousLocalization.awayMap 𝒜ˣ (ProjSpace.X_mem_one R n k)
        (rfl : (X i * X k : MvPolynomial (Fin (n+1)) R) = X i * X k))
      (ProjSpace.ratio R n i a)
theorem

segreChart_transition

L454 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.segreChart_transition
Documentation

The Segre formulas respect a change of affine coordinates in any commutative target ring. Agreement on the first chart and on base scalars, together with the two factor transitions, determines the homomorphism on the second chart.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ProductCover
variable (R : Type u) [CommRing R] (n p : ℕ)
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
theorem segreChart_transition {S : Type*} [CommRing S]
    (i k : Fin (n + 1)) (j l : Fin (p + 1))
    (ξ : Away 𝒜ᶻ (X (idx n p (i, j)) * X (idx n p (k, l))) →+* S)
    (τ : Tij R n p i j →+* S) (ρ : Tij R n p k l →+* S)
    (hξ : ∀ z : Away 𝒜ᶻ (X (idx n p (i, j))),
      ξ (HomogeneousLocalization.awayMap 𝒜ᶻ
      (ProjSpace.X_mem_one R N (idx n p (k, l))) rfl z)
        = τ (segreChart R n p i j z))
    (hX : ∀ a : Fin (n + 1),
      ρ (ProjSpace.ratio R n k a ⊗ₜ[R] (1 : Away 𝒜ʸ (X l)))
        * τ (ProjSpace.ratio R n i k ⊗ₜ[R] (1 : Away 𝒜ʸ (X j)))
        = τ (ProjSpace.ratio R n i a ⊗ₜ[R] (1 : Away 𝒜ʸ (X j))))
    (hY : ∀ b : Fin (p + 1),
      ρ ((1 : Away 𝒜ˣ (X k)) ⊗ₜ[R] ProjSpace.ratio R p l b)
        * τ ((1 : Away 𝒜ˣ (X i)) ⊗ₜ[R] ProjSpace.ratio R p j l)
        = τ ((1 : Away 𝒜ˣ (X i)) ⊗ₜ[R] ProjSpace.ratio R p j b))
    (hR : ∀ r : R,
      τ ((1 : Away 𝒜ˣ (X i)) ⊗ₜ[R] algebraMap R (Away 𝒜ʸ (X j)) r)
        = ρ ((1 : Away 𝒜ˣ (X k)) ⊗ₜ[R] algebraMap R (Away 𝒜ʸ (X l)) r))
    (z : Away 𝒜ᶻ (X (idx n p (k, l)))) :
    ξ (HomogeneousLocalization.awayMap 𝒜ᶻ
        (ProjSpace.X_mem_one R N (idx n p (i, j))) (mul_comm _ _) z)
      = ρ (segreChart R n p k l z)
theorem

overlap_fst_condition

L534 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.overlap_fst_condition
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ProductCover
variable (R : Type u) [CommRing R] (n p : ℕ)
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
theorem overlap_fst_condition (ij kl : Fin (n + 1) × Fin (p + 1)) :
    (pullback.fst (chartInclusion R n p ij.1 ij.2)
          (chartInclusion R n p kl.1 kl.2)
        ≫ (chartIso R n p ij.1 ij.2).hom
        ≫ Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom))
      ≫ Proj.awayι 𝒜ˣ (X ij.1) (ProjSpace.X_mem_one R n ij.1) one_pos
    = (pullback.snd _ _
        ≫ (chartIso R n p kl.1 kl.2).hom
        ≫ Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom))
      ≫ Proj.awayι 𝒜ˣ (X kl.1) (ProjSpace.X_mem_one R n kl.1) one_pos
theorem

overlap_snd_condition

L567 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.overlap_snd_condition
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ProductCover
variable (R : Type u) [CommRing R] (n p : ℕ)
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
theorem overlap_snd_condition (ij kl : Fin (n + 1) × Fin (p + 1)) :
    (pullback.fst (chartInclusion R n p ij.1 ij.2)
          (chartInclusion R n p kl.1 kl.2)
        ≫ (chartIso R n p ij.1 ij.2).hom
        ≫ Spec.map (CommRingCat.ofHom
            (Algebra.TensorProduct.includeRight (R := R)).toRingHom))
      ≫ Proj.awayι 𝒜ʸ (X ij.2) (ProjSpace.X_mem_one R p ij.2) one_pos
    = (pullback.snd _ _
        ≫ (chartIso R n p kl.1 kl.2).hom
        ≫ Spec.map (CommRingCat.ofHom
            (Algebra.TensorProduct.includeRight (R := R)).toRingHom))
      ≫ Proj.awayι 𝒜ʸ (X kl.2) (ProjSpace.X_mem_one R p kl.2) one_pos
theorem

chartMap_compat

L602 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.chartMap_compat
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ProductCover
variable (R : Type u) [CommRing R] (n p : ℕ)
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
theorem chartMap_compat (ij kl : Fin (n + 1) × Fin (p + 1)) :
    pullback.fst (chartInclusion R n p ij.1 ij.2)
        (chartInclusion R n p kl.1 kl.2)
      ≫ chartMap R n p ij.1 ij.2
    = pullback.snd _ _ ≫ chartMap R n p kl.1 kl.2
def

coverChartMap

L864 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.coverChartMap
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ProductCover
variable (R : Type u) [CommRing R] (n p : ℕ)
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
def coverChartMap (ij : (prodCover R n p).I₀) :
    (prodCover R n p).X ij ⟶ Proj 𝒜ᶻ
theorem

coverChartMap_compat

L868 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.coverChartMap_compat
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ProductCover
variable (R : Type u) [CommRing R] (n p : ℕ)
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
theorem coverChartMap_compat (ij kl : (prodCover R n p).I₀) :
    pullback.fst ((prodCover R n p).f ij) ((prodCover R n p).f kl) ≫
        coverChartMap R n p ij =
      pullback.snd _ _ ≫ coverChartMap R n p kl
def

segre2

L875 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.segre2
Documentation

The Segre morphism obtained by gluing its affine-chart descriptions.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ProductCover
variable (R : Type u) [CommRing R] (n p : ℕ)
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
def segre2 :
    pullback (ProjSpace.π R n) (ProjSpace.π R p) ⟶ Proj 𝒜ᶻ
theorem

chartInclusion_segre2

L879 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.chartInclusion_segre2
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ProductCover
variable (R : Type u) [CommRing R] (n p : ℕ)
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
theorem chartInclusion_segre2 (i : Fin (n + 1)) (j : Fin (p + 1)) :
    chartInclusion R n p i j ≫ segre2 R n p = chartMap R n p i j
theorem

segre2_over

L884 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.segre2_over
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ProductCover
variable (R : Type u) [CommRing R] (n p : ℕ)
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
theorem segre2_over :
    segre2 R n p ≫ ProjSpace.π R N
      = pullback.fst _ _ ≫ ProjSpace.π R n
theorem

segre2_preimage

L892 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.segre2_preimage
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ProductCover
variable (R : Type u) [CommRing R] (n p : ℕ)
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
theorem segre2_preimage (i : Fin (n + 1)) (j : Fin (p + 1)) :
    segre2 R n p
        ⁻¹ᵁ (Proj.awayι 𝒜ᶻ (X (idx n p (i, j)))
          (ProjSpace.X_mem_one R N _) one_pos).opensRange
      = (chartInclusion R n p i j).opensRange
theorem

segre2_closedImm

L940 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.segre2_closedImm
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section ProductCover
variable (R : Type u) [CommRing R] (n p : ℕ)
local notation "N" => bigN n p
local notation "𝒜ˣ" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜ʸ" => MvPolynomial.homogeneousSubmodule (Fin (p + 1)) R
local notation "𝒜ᶻ" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
Lean source · statement
theorem segre2_closedImm :
    IsClosedImmersion (segre2 R n p)
structure

SegreDatum

L991 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.SegreDatum
Documentation

A closed immersion of a finite product of projective spaces into projective space.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section Recursive
variable (R : Type u) [CommRing R]
Lean source · full declaration
structure SegreDatum {m : ℕ} (e : Fin m → ℕ) where

  /-- The dimension of the target projective space. -/
  Nd : ℕ

  /-- The Segre immersion into the target projective space. -/
  segσ : ProjSpace.prodOver R e
    ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (Nd + 1)) R)

  /-- The Segre morphism is a closed immersion. -/
  hσ_closed : IsClosedImmersion segσ

  /-- The Segre morphism commutes with the structure maps to the base. -/
  hσ_over : segσ ≫ ProjSpace.π R Nd = ProjSpace.prodOverπ R e
def

eval0

L1009 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.eval0
Documentation

Evaluate the sole homogeneous coordinate at one in the ring of global sections.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section Recursive
variable (R : Type u) [CommRing R]
attribute [scoped instance] SegreDatum.hσ_closed
Lean source · statement
def eval0 : MvPolynomial (Fin (0 + 1)) R →+* Γ(Spec (.of R), ⊤)
theorem

eval0_irrelevant

L1013 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.eval0_irrelevant
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section Recursive
variable (R : Type u) [CommRing R]
attribute [scoped instance] SegreDatum.hσ_closed
Lean source · statement
theorem eval0_irrelevant :
    (HomogeneousIdeal.irrelevant
      (homogeneousSubmodule (Fin (0 + 1)) R)).toIdeal.map (eval0 R) = ⊤
theorem

eval0_grad0

L1027 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.eval0_grad0
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section Recursive
variable (R : Type u) [CommRing R]
attribute [scoped instance] SegreDatum.hσ_closed
Lean source · statement
theorem eval0_grad0 :
    ((eval0 R).comp
        (algebraMap ((homogeneousSubmodule (Fin (0 + 1)) R) 0)
          (MvPolynomial (Fin (0 + 1)) R))).comp
      (ProjSpace.grad0Equiv R 0).toRingHom
      = (Scheme.ΓSpecIso (.of R)).inv.hom
theorem

segreAux0_section

L1041 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.segreAux0_section
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section Recursive
variable (R : Type u) [CommRing R]
attribute [scoped instance] SegreDatum.hσ_closed
Lean source · statement
theorem segreAux0_section :
    Proj.fromOfGlobalSections (homogeneousSubmodule (Fin (0 + 1)) R)
        (eval0 R) (eval0_irrelevant R)
      ≫ ProjSpace.π R 0 = 𝟙 (Spec (.of R))
def

segreAux0

L1051 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.segreAux0
Documentation

Segre data for the empty product of projective spaces.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section Recursive
variable (R : Type u) [CommRing R]
attribute [scoped instance] SegreDatum.hσ_closed
Lean source · full declaration
def segreAux0 : SegreDatum R (Fin.elim0 : Fin 0 → ℕ) where
  Nd := 0
  segσ := Proj.fromOfGlobalSections (homogeneousSubmodule (Fin (0 + 1)) R)
    (eval0 R) (eval0_irrelevant R)
  hσ_closed := by
    have hsep : IsSeparated (ProjSpace.π R 0) :=
      (ProjSpace.isProper_π R 0).toIsSeparated
    have hcomp : IsClosedImmersion (Proj.fromOfGlobalSections (homogeneousSubmodule (Fin (0 + 1)) R)
        (eval0 R) (eval0_irrelevant R)
        ≫ ProjSpace.π R 0) := by
      rw [segreAux0_section R]; infer_instance
    exact @IsClosedImmersion.of_comp _ _ _ _ (ProjSpace.π R 0) hcomp hsep
  hσ_over := by
    change _ = 𝟙 (Spec (.of R))
    exact segreAux0_section R
def

segreStep

L1067 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.segreStep
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section Recursive
variable (R : Type u) [CommRing R]
attribute [scoped instance] SegreDatum.hσ_closed
Lean source · statement
def segreStep {m : ℕ} (e : Fin (m + 1) → ℕ)
    (ih : SegreDatum R (e ∘ Fin.succ)) :
    ProjSpace.prodOver R e ⟶ pullback (ProjSpace.π R (e 0)) (ProjSpace.π R ih.Nd)
def

segreAuxSucc

L1076 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.segreAuxSucc
Documentation

Extend Segre data by one projective-space factor.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section Recursive
variable (R : Type u) [CommRing R]
attribute [scoped instance] SegreDatum.hσ_closed
Lean source · full declaration
def segreAuxSucc {m : ℕ} (e : Fin (m + 1) → ℕ)
    (ih : SegreDatum R (e ∘ Fin.succ)) : SegreDatum R e where
  Nd := bigN (e 0) ih.Nd
  segσ := segreStep R e ih ≫ segre2 R (e 0) ih.Nd
  hσ_closed := by
    have : IsClosedImmersion (segreStep R e ih) := by
      change IsClosedImmersion (pullback.map (ProjSpace.π R (e 0))
        (ProjSpace.prodOverπ R (e ∘ Fin.succ)) (ProjSpace.π R (e 0))
        (ProjSpace.π R ih.Nd) (𝟙 _) ih.segσ (𝟙 _)
        ((Category.comp_id _).trans (Category.id_comp _).symm)
        ((Category.comp_id _).trans ih.hσ_over.symm))
      refine MorphismProperty.IsStableUnderBaseChange.of_isPullback
        (P := @IsClosedImmersion)
        (f := pullback.snd (ProjSpace.π R (e 0)) (ProjSpace.π R ih.Nd))
        (f' := pullback.snd _ _) ?_ ih.hσ_closed
      refine (IsPullback.of_right ?_ (pullback.lift_snd _ _ _)
        (IsPullback.of_hasPullback (ProjSpace.π R (e 0)) (ProjSpace.π R ih.Nd))).flip
      rw [pullback.lift_fst, Category.comp_id, ih.hσ_over]
      exact IsPullback.of_hasPullback _ _
    have : IsClosedImmersion (segre2 R (e 0) ih.Nd) := segre2_closedImm R (e 0) ih.Nd
    exact IsClosedImmersion.comp (segreStep R e ih) (segre2 R (e 0) ih.Nd)
  hσ_over := by
    rw [Category.assoc, segre2_over, ← Category.assoc]
    have hfst : segreStep R e ih ≫
        pullback.fst (ProjSpace.π R (e 0)) (ProjSpace.π R ih.Nd) =
        pullback.fst (ProjSpace.π R (e 0)) (ProjSpace.prodOverπ R (e ∘ Fin.succ)) :=
      (pullback.lift_fst _ _ _).trans (Category.comp_id _)
    exact congrArg
      (fun f : ProjSpace.prodOver R e ⟶
        Proj (MvPolynomial.homogeneousSubmodule (Fin (e 0 + 1)) R) =>
          f ≫ ProjSpace.π R (e 0)) hfst
def

segreAux

L1109 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ProjSpace.Segre.segreAux
Documentation

Construct Segre data recursively for a finite product of projective spaces.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Segre
open _root_.AlgebraicGeometry.ProjSpace
section Recursive
variable (R : Type u) [CommRing R]
attribute [scoped instance] SegreDatum.hσ_closed
Lean source · full declaration
def segreAux : ∀ {_m : ℕ} (e : Fin _m → ℕ), SegreDatum R e
  | 0, e => (funext (fun k => k.elim0) : e = Fin.elim0) ▸ segreAux0 R
  | _m + 1, e => segreAuxSucc R e (segreAux (e ∘ Fin.succ))
def

toChowDatumProj

L1128 ↗
AlgebraicGeometry.ChowDatum.toChowDatumProj
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Converter
open ProjSpace.Segre
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
namespace ChowDatum
open scoped _root_.AlgebraicGeometry.ChowDatum in
Lean source · full declaration
def _root_.AlgebraicGeometry.ChowDatum.toChowDatumProj (D : ChowDatum π) : ChowDatumProj
    π where
  Nd := (segreAux R D.e).Nd
  V' := D.V'
  p := D.p
  ιN := D.ι ≫ (segreAux R D.e).segσ
  hp_proper := D.hp_proper
  hιN_closed := by
    have := D.hι_closed
    have := (segreAux R D.e).hσ_closed
    exact IsClosedImmersion.comp D.ι (segreAux R D.e).segσ
  hoverN := by
    rw [Category.assoc, (segreAux R D.e).hσ_over, D.hover]
  U := D.U
  hU_dense := D.hU_dense
  hp_isoU := D.hp_isoU
theorem

nonempty_chowDatumProj_of

L1148 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ChowDatum.nonempty_chowDatumProj_of
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Converter
open ProjSpace.Segre
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
open _root_.AlgebraicGeometry
open scoped _root_.AlgebraicGeometry.ChowDatum in
Lean source · statement
theorem ChowDatum.nonempty_chowDatumProj_of :
    Nonempty (ChowDatum π) → Nonempty (ChowDatumProj π)
theorem

exists_integral_chowDatumProj

L1155 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of.AlgebraicGeometry.ChowDatum.exists_integral_chowDatumProj
Documentation

The concrete Segre conversion preserves the integral source and the surjective modification map of the constructed Chow datum.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Converter
open ProjSpace.Segre
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
open _root_.AlgebraicGeometry
open scoped _root_.AlgebraicGeometry.ChowDatum in
Lean source · statement
theorem ChowDatum.exists_integral_chowDatumProj [IsProper π] [IsIntegral V] :
    ∃ D : ChowDatumProj π, IsIntegral D.V' ∧ Surjective D.p
theorem

exists_integral

L1166 ↗
AlgebraicGeometry.ChowDatumProj.exists_integral
Documentation

A proper integral scheme over any ring admits an integral projective proper cover, with the actual surjective morphism retained.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
Lean source · statement
theorem _root_.AlgebraicGeometry.ChowDatumProj.exists_integral {R : Type u} [CommRing R]
    {V : AlgebraicGeometry.Scheme.{u}}
    (π : V ⟶ AlgebraicGeometry.Spec (.of R)) [AlgebraicGeometry.IsProper π]
    [AlgebraicGeometry.IsIntegral V] :
    ∃ D : AlgebraicGeometry.ChowDatumProj π,
      AlgebraicGeometry.IsIntegral D.V' ∧ AlgebraicGeometry.Surjective D.p
theorem

nonempty_of

L1174 ↗
AlgebraicGeometry.ChowDatumProj.nonempty_of
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatumProj_nonempty_of
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
Lean source · statement
theorem _root_.AlgebraicGeometry.ChowDatumProj.nonempty_of {R : Type u} [CommRing R]
    {V : AlgebraicGeometry.Scheme.{u}}
    (π : V ⟶ AlgebraicGeometry.Spec (.of R)) :
    Nonempty (AlgebraicGeometry.ChowDatum π) → Nonempty (AlgebraicGeometry.ChowDatumProj π)

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