Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AlgebraicGeometry_ProjSpaceCover.lean

definition module

Standard ordered affine cover of projective space

Throughout, R (resp. A) is a commutative ring, n a natural number, and \mathcal{A} denotes the graded ring R[x_0,\dots,x_n] presented as MvPolynomial.homogeneousSubmodule (Fin (n+1)) R, the grading by total degree, so that Proj 𝒜 is \mathbb{P}^n_R. Recall that a Scheme.OrderedAffineCover of a scheme V consists of a finite linearly ordered index type, a family of opens of V indexed by it, a proof that each member is an affine open, and a proof that the supremum of the family is \top; the linear order is part of the data, since it is what makes the alternating Čech complex attached to the cover well defined.

The first definition, ProjSpace.stdCover R n, is the ordered affine cover of Proj 𝒜 with index type ULift (Fin (n+1)) carrying its inherited finiteness and order, and with j-th member the basic open D_+(x_j), i.e. Proj.basicOpen 𝒜 (MvPolynomial.X j.down). That these opens are affine is the standard statement for the basic open attached to a homogeneous element of positive degree, applied to x_j, homogeneous of degree 1; that they cover \mathbb{P}^n_R follows from the inclusion of the irrelevant ideal in the ideal generated by x_0,\dots,x_n (the lemma irrelevant_le_span_X), after identifying the supremum over ULift (Fin (n+1)) with the supremum over Fin (n+1).

The second definition, ProjSpace.stdCoverPullback ι, takes a scheme W and a morphism \iota : W \to \mathbb{P}^n_A which is affine (IsAffineHom), and forms the ordered affine cover of W with the same index type whose j-th member is the preimage open \iota^{-1}D_+(x_j): affineness of each member is affineness of the preimage of an affine open under an affine morphism, and the covering property is preserved under taking preimages. Two auxiliary lemmas record the members of the two covers, (\mathrm{stdCover}\ R\ n).U\ j = D_+(x_j) and (\mathrm{stdCoverPullback}\ \iota).U\ j = \iota^{-1}D_+(x_j).

Relation to Mathlib

The graded ring Proj, Proj.basicOpen, affineness of basic opens and preservation of affine opens under affine morphisms are Mathlib's; Scheme.OrderedAffineCover is the project's variant of Mathlib's Scheme.AffineOpenCover, with a finite linearly ordered index type and no chosen affine scheme presentations. The same charts also occur as a Mathlib-style Scheme.AffineOpenCover under the name ProjSpace.affineOpenCover.

Where it is used

These covers are the ones on which the project's alternating Čech complexes of module presheaves (OModulePresheaf.cochain and its differential) are formed: stdCover for \mathbb{P}^n_R itself, and stdCoverPullback ι for a scheme affine over \mathbb{P}^n_A, for instance a closed subscheme, which is the setting in which finiteness of coherent cohomology is obtained.

References

  1. R. Hartshorne, Algebraic Geometry, Graduate Texts in Mathematics 52, Springer, 1977, II.2.5 and III.4
  2. A. Grothendieck and J. Dieudonné, Éléments de géométrie algébrique II, Publ. Math. IHÉS 8 (1961), §2

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_ProjSpaceCover.lean

Imports

Imported by

Declarations

Source

import Definitions.Def_AlgebraicGeometry_ProjSpace
import Definitions.Def_AlgebraicGeometry_OrderedAffineCoverCech
import Mathlib.AlgebraicGeometry.Morphisms.Affine ↗

set_option autoImplicit false

noncomputable section

universe u

open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial

namespace AlgebraicGeometry

attribute [local instance] MvPolynomial.gradedAlgebra

namespace ProjSpace

section StdCover

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

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

def stdCover : Scheme.OrderedAffineCover.{u} (Proj 𝒜) where
  ι := ULift.{u} (Fin (n + 1))
  U j := AlgebraicGeometry.Proj.basicOpen 𝒜 (MvPolynomial.X j.down)
  isAffineOpen j := AlgebraicGeometry.Proj.isAffineOpen_basicOpen 𝒜 (MvPolynomial.X j.down)
    ((MvPolynomial.mem_homogeneousSubmodule 1 _).mpr (MvPolynomial.isHomogeneous_X R j.down))
    one_pos
  iSup_eq_top := by
    have key : (⨆ j : ULift.{u} (Fin (n + 1)),
        AlgebraicGeometry.Proj.basicOpen 𝒜 (MvPolynomial.X j.down))
        = ⨆ j : Fin (n + 1), AlgebraicGeometry.Proj.basicOpen 𝒜 (MvPolynomial.X j) := by
      refine le_antisymm (iSup_le fun j => ?_) (iSup_le fun j => ?_)
      · exact le_iSup (fun j' : Fin (n + 1) => AlgebraicGeometry.Proj.basicOpen 𝒜 (X j')) j.down
      · exact le_iSup (fun j' : ULift.{u} (Fin (n + 1)) =>
          AlgebraicGeometry.Proj.basicOpen 𝒜 (X j'.down)) (ULift.up j)
    rw [key]
    exact AlgebraicGeometry.Proj.iSup_basicOpen_eq_top 𝒜 _
      (irrelevant_le_span_X R n)

theorem stdCover_U (j : ULift.{u} (Fin (n + 1))) :
    (stdCover R n).U j = AlgebraicGeometry.Proj.basicOpen 𝒜 (MvPolynomial.X j.down) := rfl

end StdCover

section StdCoverPullback

variable {A : Type u} [CommRing A] {n : ℕ}
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]

def stdCoverPullback : Scheme.OrderedAffineCover.{u} W :=
  let f := ι
  { ι := ULift.{u} (Fin (n + 1))
    U := fun j => f ⁻¹ᵁ ((stdCover A n).U j)
    isAffineOpen := fun j => ((stdCover A n).isAffineOpen j).preimage f
    iSup_eq_top := Scheme.Hom.iSup_preimage_eq_top f (stdCover A n).iSup_eq_top }

theorem stdCoverPullback_U (j : ULift.{u} (Fin (n + 1))) :
    (stdCoverPullback ι).U j = ι ⁻¹ᵁ (stdCover A n).U j := rfl

end StdCoverPullback

end ProjSpace

end AlgebraicGeometry

end

Statements phrased using this module (36)