Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AlgebraicGeometry_ProjSpace.lean

definition module

Projective space over a ring, products, and Chow data

Fix a commutative ring R and n \in \mathbb{N}, and grade S = R[x_0,\dots,x_n] (Lean: MvPolynomial (Fin (n+1)) R) by total degree through MvPolynomial.homogeneousSubmodule. grad0Equiv is the ring isomorphism R \cong S_0 sending r to the constant C\,r, with inverse the constant coefficient, and π is the structure morphism \operatorname{Proj} S \to \operatorname{Spec} R, namely Proj.toSpecZero followed by Spec.map of that isomorphism; accompanying instances record that S is of finite type over S_0 (generated by the x_j) and that π is proper. irrelevant_le_span_X states S_+ \subseteq (x_0,\dots,x_n), and affineOpenCover is the resulting affine open cover of \operatorname{Proj} S whose j-th chart morphism is Proj.awayι at x_j (affineOpenCover_f). On the degree-zero localisation S_{(x_i)} (HomogeneousLocalization.Away) the instance algebraAway puts the R-algebra structure coming from R \cong S_0; awayι_comp_π identifies the chart followed by π with \operatorname{Spec} of R \to S_{(x_i)}; ratio R n i k is the element x_k/x_i, and the helper lemmas give x_i/x_i = 1, the value of \operatorname{algebraMap}, the expansion of a degree-d monomial over x_i^d as r\prod_j (x_j/x_i)^{e_j}, and S_{(x_i)} = R[x_k/x_i : k].

For e : \mathrm{Fin}\,m \to \mathbb{N}, prodOverAux builds by recursion on m a scheme with a morphism to \operatorname{Spec} R: the empty case is \operatorname{Spec} R with the identity, and the step takes the fibre product of \operatorname{Proj} of e_0+1 variables with the previous stage over \operatorname{Spec} R; prodOver, prodOverπ name the two components, which model \mathbb{P}^{e_0}_R \times_R \cdots \times_R \mathbb{P}^{e_{m-1}}_R over \operatorname{Spec} R, with properness, projections prodPr compatible with the structure maps, and a universal morphism prodLift out of any R-scheme equipped with a compatible family of morphisms to the factors (prodLiftAux packages the morphism together with its compatibility).

For an R-algebra A, mvMapGraded is the graded ring homomorphism induced by coefficient extension, irrelevant_le_map_mvMapGraded checks the hypothesis on irrelevant ideals, and map is the resulting morphism \operatorname{Proj} over A to \operatorname{Proj} over R.

Finally, relative to a morphism \pi : V \to \operatorname{Spec} R, the structure ChowDatum bundles: an arity m with dimensions e, a scheme V', a proper p : V' \to V, a closed immersion \iota : V' \to prodOver R e, the relation \iota followed by prodOverπ = p followed by \pi, and a dense open U \subseteq V over which p becomes an isomorphism (the second pullback projection of p along U \hookrightarrow V is an isomorphism). ChowDatumProj is the same data with the product replaced by a single \operatorname{Proj} of N_d+1 variables. Both carry their compatibility and properness assertions as fields.

Relation to Mathlib

Mathlib supplies \operatorname{Proj} of a graded ring together with Proj.toSpecZero, Proj.awayι, Proj.affineOpenCoverOfIrrelevantLESpan, Proj.map and homogeneous localisations; this module specialises them to the total-degree grading of a polynomial ring, thereby providing projective n-space over R and its standard charts. The iterated products and the ChowDatum/ChowDatumProj bundles are the project's own.

Where it is used

These definitions provide the projective-geometry vocabulary (projective space over a base ring, its standard affine charts, products of projective spaces, base change in the coefficients) used throughout the scheme-theoretic layer of the formalisation, and in particular the shape of the data produced by Chow's lemma.

References

  1. R. Hartshorne, Algebraic Geometry, Graduate Texts in Mathematics 52, Springer, 1977, II.2.5, II.4.8
  2. A. Grothendieck and J. Dieudonné, Éléments de géométrie algébrique II: Étude globale élémentaire de quelques classes de morphismes, Publ. Math. IHÉS 8 (1961), 2.4, 2.8.10, 5.6.1

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_AlgebraicGeometry_ProjSpace.lean

Imports

  • only Mathlib

Imported by

Declarations

Source

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

set_option autoImplicit false
set_option linter.unusedVariables false

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

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, if_neg (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 π : Proj 𝒜 ⟶ Spec (.of R) :=
  Proj.toSpecZero 𝒜 ≫ Spec.map (CommRingCat.ofHom (grad0Equiv R n).toRingHom)

instance finiteType_mvPolynomial :
    Algebra.FiniteType (𝒜 0) (MvPolynomial (Fin (n + 1)) R) := by
  classical
  refine ⟨⟨Finset.univ.image MvPolynomial.X, eq_top_iff.mpr fun p _ => ?_⟩⟩
  induction p using MvPolynomial.induction_on with
  | C r =>
    exact Subalgebra.algebraMap_mem _ (⟨C r, (mem_homogeneousSubmodule 0 _).mpr
      (isHomogeneous_C _ r)⟩ : 𝒜 0)
  | add p q hp hq => exact Subalgebra.add_mem _ (hp trivial) (hq trivial)
  | mul_X p j hp =>
    exact Subalgebra.mul_mem _ (hp trivial)
      (Algebra.subset_adjoin (Finset.mem_coe.mpr (Finset.mem_image_of_mem _ (Finset.mem_univ j))))

instance isProper_π : IsProper (π R n) := by
  unfold π
  haveI : IsProper (Proj.toSpecZero 𝒜) := inferInstance
  haveI : IsIso (CommRingCat.ofHom (grad0Equiv R n).toRingHom) :=
    (ConcreteCategory.isIso_iff_bijective _).mpr (grad0Equiv R n).bijective
  haveI : IsIso (Spec.map (CommRingCat.ofHom (grad0Equiv R n).toRingHom)) :=
    inferInstance
  infer_instance

end PnSetup

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

theorem irrelevant_le_span_X :
    (HomogeneousIdeal.irrelevant 𝒜).toIdeal
      ≤ Ideal.span (Set.range (MvPolynomial.X : Fin (n + 1) → MvPolynomial _ R)) := by
  rw [HomogeneousIdeal.toIdeal_irrelevant_le]
  intro i hi f hf
  have hf' : f.IsHomogeneous i := (MvPolynomial.mem_homogeneousSubmodule i f).mp hf
  show f ∈ MvPolynomial.idealOfVars (Fin (n + 1)) R
  rw [← pow_one (MvPolynomial.idealOfVars _ R), MvPolynomial.mem_pow_idealOfVars_iff]
  intro x hx
  rw [MvPolynomial.mem_support_iff] at hx
  have hdeg : Finsupp.degree x = i := by
    rw [Finsupp.degree_eq_weight_one]; exact hf' hx
  omega

end StdCover

section Setup

variable (R : Type u) [CommRing R] (n : ℕ)

local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R

theorem X_mem_one (j : Fin (n + 1)) :
    (MvPolynomial.X j : MvPolynomial (Fin (n + 1)) R) ∈ 𝒜 1 :=
  (mem_homogeneousSubmodule 1 _).mpr (isHomogeneous_X R j)

instance algebraAway (i : Fin (n + 1)) :
    Algebra R (Away 𝒜 (MvPolynomial.X i)) :=
  ((HomogeneousLocalization.fromZeroRingHom 𝒜 _).comp
    (grad0Equiv R n).toRingHom).toAlgebra

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)))) := by
  unfold π
  rw [← Category.assoc, Proj.awayι_toSpecZero, ← Spec.map_comp]
  rfl

def ratio (i k : Fin (n + 1)) : Away 𝒜 (MvPolynomial.X i) :=
  Away.mk 𝒜 (X_mem_one R n i) 1 (MvPolynomial.X k)
    (by simpa using X_mem_one R n k)

theorem ratio_self (i : Fin (n + 1)) :
    ratio R n i i = 1 := by
  apply HomogeneousLocalization.val_injective
  rw [ratio, Away.val_mk, HomogeneousLocalization.val_one,
    ← Localization.mk_one, Localization.mk_eq_mk_iff, Localization.r_iff_exists]
  exact ⟨1, by push_cast; ring⟩

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) := by
  rfl

end Setup

section StdCover

variable (R : Type u) [CommRing R] (n : ℕ)

local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R

def affineOpenCover : (Proj 𝒜).AffineOpenCover :=
  Proj.affineOpenCoverOfIrrelevantLESpan 𝒜 (fun j => MvPolynomial.X j)
    (fun j => X_mem_one R n j) (fun _ => one_pos)
    (irrelevant_le_span_X R n)

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 := rfl

end StdCover

section AdjoinRatio

variable (R : Type u) [CommRing R] (n : ℕ)

local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R

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) := by
  have hdsum : ∑ j, e j = d := by
    rw [← hd, Finsupp.degree]
    exact (Finset.sum_subset (Finset.subset_univ _)
      (fun j _ hj => Finsupp.notMem_support_iff.mp hj)).symm
  apply HomogeneousLocalization.val_injective
  have hval : (HomogeneousLocalization.val : Away 𝒜 (X i) → Localization.Away (X i))
      = (algebraMap (Away 𝒜 (X i)) (Localization.Away (X i))) := rfl
  rw [hval, map_mul, map_prod]
  simp only [map_pow, ratio, ← hval, Away.val_mk,
    val_algebraMap, Localization.mk_pow,
    ← Localization.mk_one_eq_algebraMap, Localization.mk_prod, Localization.mk_mul]
  congr 1
  · rw [MvPolynomial.monomial_eq, Finsupp.prod_pow]
  · refine Subtype.ext ?_
    push_cast
    simp only [Finset.prod_pow_eq_pow_sum, pow_one, one_mul, hdsum]

theorem adjoin_range_ratio (i : Fin (n + 1)) :
    Algebra.adjoin R (Set.range (ratio R n i)) = ⊤ := by
  rw [eq_top_iff]
  intro z _
  obtain ⟨d, a, ha, rfl⟩ := Away.mk_surjective 𝒜 (X_mem_one R n i) z
  have ha' : a.IsHomogeneous d := (mem_homogeneousSubmodule d a).mp (by simpa using ha)

  have hdeg : ∀ e ∈ a.support, (e : Fin (n + 1) →₀ ℕ).degree = d := fun e he => by
    rw [Finsupp.degree_eq_weight_one]; exact ha' (MvPolynomial.mem_support_iff.mp he)
  have hsum : Away.mk 𝒜 (X_mem_one R n i) d a ha
      = ∑ e ∈ a.support.attach,
          Away.mk 𝒜 (X_mem_one R n i) d
            (MvPolynomial.monomial e.1 (a.coeff e.1))
            ((mem_homogeneousSubmodule _ _).mpr
              (isHomogeneous_monomial _
                (by simp only [smul_eq_mul, mul_one]; exact hdeg e.1 e.2))) := by
    apply HomogeneousLocalization.val_injective
    have hval : (HomogeneousLocalization.val : Away 𝒜 (X i) → Localization.Away (X i))
        = (algebraMap (Away 𝒜 (X i)) (Localization.Away (X i))) := rfl
    rw [hval, map_sum]
    simp only [← hval, Away.val_mk]
    rw [Finset.sum_attach a.support
      (fun e => Localization.mk (monomial e (a.coeff e))
        (⟨(X i)^d, Away.val_mk._proof_1 d⟩ :
          Submonoid.powers (X i : MvPolynomial (Fin (n+1)) R))),
      ← Localization.mk_sum]
    congr 1
    exact MvPolynomial.as_sum a
  rw [hsum]
  refine Subalgebra.sum_mem _ fun e _ => ?_
  rw [awayMk_monomial R n i d e.1 (hdeg e.1 e.2) (a.coeff e.1)]
  exact Subalgebra.mul_mem _ (Subalgebra.algebraMap_mem _ _)
    (Subalgebra.prod_mem _ fun j _ =>
      Subalgebra.pow_mem _ (Algebra.subset_adjoin (Set.mem_range_self j)) _)

end AdjoinRatio

section ProdOver

variable (R : Type u) [CommRing R]

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 {m : ℕ} (e : Fin m → ℕ) : Scheme.{u} :=
  (prodOverAux R e).1

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

theorem isProper_prodOverπ {m : ℕ} (e : Fin m → ℕ) :
    IsProper (prodOverπ R e) := by
  induction m with
  | zero => exact inferInstanceAs (IsProper (𝟙 _))
  | succ m ih =>
    haveI := ih (e ∘ Fin.succ)
    change IsProper (pullback.fst _ _ ≫ π R (e 0))
    infer_instance

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

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_π {m : ℕ} (e : Fin m → ℕ) (k : Fin m) :
    prodPr R e k ≫ π R (e k) = prodOverπ R e := by
  induction m with
  | zero => exact k.elim0
  | succ m ih =>
    match k with
    | ⟨0, _⟩ => rfl
    | ⟨k + 1, hk⟩ =>
      have key := ih (e ∘ Fin.succ) ⟨k, Nat.succ_lt_succ_iff.mp hk⟩
      calc (pullback.snd _ _ ≫
            prodPr R (e ∘ Fin.succ) ⟨k, Nat.succ_lt_succ_iff.mp hk⟩)
              ≫ π R (e ⟨k + 1, hk⟩)
          = pullback.snd _ _ ≫ (prodPr R (e ∘ Fin.succ)
              ⟨k, Nat.succ_lt_succ_iff.mp hk⟩ ≫
              π R ((e ∘ Fin.succ) ⟨k, Nat.succ_lt_succ_iff.mp hk⟩)) :=
            Category.assoc _ _ _
        _ = pullback.snd _ _ ≫ prodOverπ R (e ∘ Fin.succ) := by rw [key]
        _ = prodOverπ R e := (pullback.condition).symm

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
      show pullback.lift (g 0) prev.1 _ ≫ pullback.fst _ _ ≫ π R (e 0) = s
      rw [← Category.assoc, pullback.lift_fst]; exact hg 0⟩

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 :=
  (prodLiftAux R s e g hg).1

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 := by
  exact (prodLiftAux R s e g hg).2

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 := by
  induction m with
  | zero => exact k.elim0
  | succ m ih =>
    match k with
    | ⟨0, _⟩ => exact pullback.lift_fst _ _ _
    | ⟨k + 1, hk⟩ =>
      show (pullback.lift _ _ _) ≫ (pullback.snd _ _ ≫
        prodPr R (e ∘ Fin.succ) ⟨k, Nat.succ_lt_succ_iff.mp hk⟩) = _
      rw [← Category.assoc, pullback.lift_snd]
      exact ih (e ∘ Fin.succ) (fun k => g k.succ) (fun k => hg k.succ)
        ⟨k, Nat.succ_lt_succ_iff.mp hk⟩

end ProdOver

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

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 (j : Fin (n + 1)) :
    (mvMapGraded R A n) (MvPolynomial.X j) = MvPolynomial.X j :=
  MvPolynomial.map_X _ j

theorem irrelevant_le_map_mvMapGraded :
    (HomogeneousIdeal.irrelevant 𝒜A)
      ≤ HomogeneousIdeal.map (mvMapGraded R A n)
          (HomogeneousIdeal.irrelevant 𝒜R) := by
  intro a ha
  show a ∈ (HomogeneousIdeal.map (mvMapGraded R A n)
    (HomogeneousIdeal.irrelevant _)).toIdeal
  rw [HomogeneousIdeal.toIdeal_map, MvPolynomial.as_sum a]
  refine Ideal.sum_mem _ fun d hd => ?_
  have hd0 : d ≠ 0 := by
    rintro rfl
    refine (MvPolynomial.mem_support_iff.mp hd) ?_
    rw [HomogeneousIdeal.mem_irrelevant_iff, GradedRing.proj_apply] at ha
    classical
    conv_lhs => rw [← DirectSum.sum_support_decompose (homogeneousSubmodule (Fin (n + 1)) A) a]
    rw [coeff_sum]
    refine Finset.sum_eq_zero fun i _ => ?_
    rcases eq_or_ne i 0 with rfl | hi0
    · rw [ha, coeff_zero]
    · exact ((mem_homogeneousSubmodule i _).mp
        (DirectSum.decompose (homogeneousSubmodule (Fin (n + 1)) A) a i).2).coeff_eq_zero
        (by simpa [Finsupp.degree] using hi0.symm)
  obtain ⟨j, hj⟩ := Finset.nonempty_iff_ne_empty.mpr (Finsupp.support_eq_empty.not.mpr hd0)
  obtain ⟨q, hq⟩ : (X j : MvPolynomial (Fin (n + 1)) A) ∣ monomial d (coeff d a) :=
    X_dvd_monomial.mpr (Or.inr (Finsupp.mem_support_iff.mp hj))
  rw [hq, show (X j : MvPolynomial (Fin (n + 1)) A)
      = (mvMapGraded R A n).toRingHom (X j) from (map_X _ j).symm]
  exact Ideal.mul_mem_right _ _ (Ideal.mem_map_of_mem _
    ((HomogeneousIdeal.mem_irrelevant_iff _ _).mpr (by
      rw [GradedRing.proj_apply, DirectSum.decompose_of_mem_ne _
        ((mem_homogeneousSubmodule 1 _).mpr (isHomogeneous_X R j)) one_ne_zero])))

def map : Proj 𝒜A ⟶ Proj 𝒜R :=
  Proj.map (mvMapGraded R A n) (irrelevant_le_map_mvMapGraded R A n)

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

end MapGraded

end ProjSpace

section Carrier

variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))

structure ChowDatum where

  m : ℕ

  e : Fin m → ℕ

  V' : Scheme.{u}

  p : V' ⟶ V

  ι : V' ⟶ ProjSpace.prodOver R e

  hp_proper : IsProper p

  hι_closed : IsClosedImmersion ι

  hover : ι ≫ ProjSpace.prodOverπ R e = p ≫ π

  U : V.Opens

  hU_dense : Dense (U : Set V)

  hp_isoU : IsIso (pullback.snd p U.ι)

attribute [instance] ChowDatum.hp_proper ChowDatum.hι_closed ChowDatum.hp_isoU

end Carrier

section CarrierProj

variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))

structure ChowDatumProj where

  Nd : ℕ

  V' : Scheme.{u}

  p : V' ⟶ V

  ιN : V' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (Nd + 1)) R)

  hp_proper : IsProper p

  hιN_closed : IsClosedImmersion ιN

  hoverN : ιN ≫ ProjSpace.π R Nd = p ≫ π

  U : V.Opens

  hU_dense : Dense (U : Set V)

  hp_isoU : IsIso (pullback.snd p U.ι)

attribute [instance] ChowDatumProj.hp_proper ChowDatumProj.hιN_closed
  ChowDatumProj.hp_isoU

end CarrierProj

end AlgebraicGeometry

end

Statements phrased using this module (225)

… and 75 more statements (search for the module name to find them).