28.2 Constructible sets to 28.22 Locally projective modules

Section28.2 Constructible sets#

Section 28.2 of the Stacks Project, Tag 054B. 7 tags here are carried by 6 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 054C, a lemma

Tag 054C in the Stacks Project.

AlgebraicGeometry.isLocallyConstructible_iff_forall_affineOpens, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Constructible.lean, line 69. References: SGA 3 VIB (3.7), “(iii), special case”.

A subset of a scheme is locally constructible if and only if its restriction to every affine open subscheme is constructible.

public theorem isLocallyConstructible_iff_forall_affineOpens
    {X : Scheme.{u}} (E : Set X) :
    Topology.IsLocallyConstructible E ↔
      ∀ U : X.affineOpens, Topology.IsConstructible ((U.1 : Set X) ↓∩ E)
Tag 0AAW, a lemma

Tag 0AAW in the Stacks Project.

AlgebraicGeometry.compl_mem_nhds_of_isLocallyConstructible_of_mem_genericPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Constructible.lean, line 91. The attribute's comment: “neighborhood_disjoint”.

A generic point of an irreducible component which is not in a locally constructible subset has an open neighbourhood disjoint from that subset.

public theorem compl_mem_nhds_of_isLocallyConstructible_of_mem_genericPoints
    {X : Scheme.{u}} {E : Set X} {ξ : X} (hE : IsLocallyConstructible E)
    (hξ : ξ ∈ genericPoints X) (hξE : ξ ∉ E) :
    Eᶜ ∈ 𝓝 ξ

AlgebraicGeometry.mem_nhds_of_isLocallyConstructible_of_mem_genericPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Constructible.lean, line 123. The attribute's comment: “neighborhood_contained”.

A locally constructible set containing the generic point of an irreducible component contains an open neighbourhood of that point.

public theorem mem_nhds_of_isLocallyConstructible_of_mem_genericPoints
    {X : Scheme.{u}} {E : Set X} {ξ : X} (hE : IsLocallyConstructible E)
    (hξ : ξ ∈ genericPoints X) (hξE : ξ ∈ E) :
    E ∈ 𝓝 ξ
Tag 054D, a lemma

Tag 054D in the Stacks Project.

Declarations registered for the tag:

Tag 094L, a lemma

Tag 094L in the Stacks Project.

AlgebraicGeometry.spectralSpace_of_compactSpace_of_quasiSeparatedSpace, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Constructible.lean, line 137. References: SGA 4 IV (4.2.1), “special case”.

The underlying topological space of a quasi-compact and quasi-separated scheme is a spectral space: it is sober and quasi-compact, the quasi-compact opens form a basis, and any two of them meet in a quasi-compact open.

public instance spectralSpace_of_compactSpace_of_quasiSeparatedSpace (X : Scheme.{u})
    [CompactSpace X] [QuasiSeparatedSpace X] : SpectralSpace X
Tag 054E, a lemma

Tag 054E in the Stacks Project.

Declarations registered for the tag:

Tag 07ZL, a lemma

Tag 07ZL in the Stacks Project.

AlgebraicGeometry.isRetrocompact_iff_forall_affineOpens, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/ExtendFiniteType/RetrocompactOpen.lean, line 83. References: EGA IV (1.8.1), “retrocompact criterion”.

A subset of a scheme is retrocompact exactly when its intersection with every affine open is quasi-compact.

theorem isRetrocompact_iff_forall_affineOpens (E : Set X) :
    IsRetrocompact E ↔ ∀ W : X.affineOpens, IsCompact (E ∩ (W : Set X))
Tag 0F2M, a lemma

Tag 0F2M in the Stacks Project.

AlgebraicGeometry.locallyFinite_iff_parts_isLocallyConstructible, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/ConstructiblePartition.lean, line 154.

A partition of a scheme into retrocompact parts is locally finite if and only if all its parts are locally constructible.

public lemma locallyFinite_iff_parts_isLocallyConstructible
    {X : Scheme.{u}} {P : Set (Set X)} (hP : IsTopologicalPartition P)
    (hP_retrocompact : ∀ S ∈ P, IsRetrocompact S) :
    LocallyFinite (fun S : P ↦ (S : Set X)) ↔
      ∀ S ∈ P, Topology.IsLocallyConstructible S
Sources
LeanAlgebraicGeometry.isLocallyConstructible_iff_forall_affineOpens · AlgebraicGeometry.compl_mem_nhds_of_isLocallyConstructible_of_mem_genericPoints · AlgebraicGeometry.mem_nhds_of_isLocallyConstructible_of_mem_genericPoints · QuasiSeparatedSpace.inter_isCompact · IsCompact.isRetrocompact · AlgebraicGeometry.spectralSpace_of_compactSpace_of_quasiSeparatedSpace · Topology.IsLocallyConstructible.isConstructible · AlgebraicGeometry.isRetrocompact_iff_forall_affineOpens

Section28.3 Integral, irreducible, and reduced schemes#

Section 28.3 of the Stacks Project, Tag 01OJ. 4 tags here are carried by 1 declaration of the repository (in StacksFrontier) and 7 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01OK, a definition

Tag 01OK in the Stacks Project.

Declarations registered for the tag:

Tag 01OL, a lemma

Tag 01OL in the Stacks Project.

Declarations registered for the tag:

Tag 01OM, a lemma

Tag 01OM in the Stacks Project.

AlgebraicGeometry.Scheme.irreducibleSpace_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Irreducible.lean, line 115.

Stacks Project, Tag 01OM. A scheme is irreducible if and only if it has a nonempty affine open cover by irreducible opens whose members meet pairwise, if and only if it is nonempty and every nonempty affine open is irreducible.

theorem irreducibleSpace_tfae (X : Scheme.{u}) :
    List.TFAE [
      IrreducibleSpace X,
      ∃ (ι : Type u) (U : ι → X.Opens),
        Nonempty ι ∧
          IsOpenCover U ∧
          (∀ i, IsAffineOpen (U i)) ∧
          (∀ i, IrreducibleSpace (U i)) ∧
          ∀ i j, Set.Nonempty ((U i : Set X) ∩ (U j : Set X)),
      Nonempty X ∧
        ∀ U : X.Opens, IsAffineOpen U → Nonempty U → IrreducibleSpace U]
Tag 01ON, a lemma

Tag 01ON in the Stacks Project.

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.IsIntegral · AlgebraicGeometry.IsReduced.component_reduced · AlgebraicGeometry.isReduced_of_isReduced_stalk · AlgebraicGeometry.isReduced_stalk_of_isReduced · AlgebraicGeometry.IsReduced.of_openCover · AlgebraicGeometry.isReduced_of_isAffine_isReduced · AlgebraicGeometry.Scheme.irreducibleSpace_tfae · AlgebraicGeometry.isIntegral_iff_irreducibleSpace_and_isReduced

Section28.4 Types of schemes defined by properties of rings#

Section 28.4 of the Stacks Project, Tag 01OO. 5 tags here are carried by 10 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01OP, a definition

Tag 01OP in the Stacks Project.

CommRing.PropertyIsLocal, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/LocalRingProperty.lean, line 81.

A property of commutative rings is local if it is preserved by localization away from an element and descends from every finite family of such localizations whose elements generate the unit ideal.

structure PropertyIsLocal (P : ∀ (R : Type u) [CommRing R], Prop) : Prop
Tag 01OQ, a definition

Tag 01OQ in the Stacks Project.

AlgebraicGeometry.IsLocally, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/LocalRingProperty.lean, line 206.

A scheme is locally P if every point belongs to an affine open whose ring of sections satisfies P.

abbrev IsLocally (P : (R : Type u) → [CommRing R] → Prop) (X : Scheme.{u}) :
    Prop
Tag 01OR, a lemma

Tag 01OR in the Stacks Project.

AlgebraicGeometry.isLocally_iff_forall_affineOpens, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NagataNormalization/LocalProperty.lean, line 153. The attribute's comment: “part (1) iff part (2)”.

Stacks Project, Tag 01OR (part (1) iff part (2)). A scheme locally satisfies a local ring property precisely when the ring of sections over every affine open satisfies it.

theorem isLocally_iff_forall_affineOpens (hP : CommRing.PropertyIsLocal P) (X : Scheme.{u}) :
    IsLocally P X ↔ ∀ U : X.affineOpens, P Γ(X, U.1)

AlgebraicGeometry.isLocally_iff_exists_affineOpenCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NagataNormalization/LocalProperty.lean, line 163. The attribute's comment: “part (1) iff part (3)”.

Stacks Project, Tag 01OR (part (1) iff part (3)). A scheme locally satisfies a ring property precisely when it has an affine open cover on whose rings of sections the property holds.

theorem isLocally_iff_exists_affineOpenCover (P : (R : Type u) → [CommRing R] → Prop)
    (X : Scheme.{u}) :
    IsLocally P X ↔
      ∃ (ι : Type u) (U : ι → X.affineOpens),
        IsOpenCover (fun i ↦ (U i : X.Opens)) ∧ ∀ i, P Γ(X, (U i).1)

AlgebraicGeometry.isLocally_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NagataNormalization/LocalProperty.lean, line 176. The attribute's comment: “open subschemes”.

Stacks Project, Tag 01OR (open subschemes). Every open subscheme of a scheme locally satisfying a local ring property also locally satisfies that property.

theorem isLocally_open (hP : CommRing.PropertyIsLocal P) (X : Scheme.{u}) (hX : IsLocally P X)
    (U : X.Opens) : IsLocally P U.toScheme

AlgebraicGeometry.isLocally_iff_exists_openCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NagataNormalization/LocalProperty.lean, line 187. The attribute's comment: “part (1) iff part (4)”.

Stacks Project, Tag 01OR (part (1) iff part (4)). A scheme locally satisfies a local ring property precisely when it has an open cover by open subschemes locally satisfying the property.

theorem isLocally_iff_exists_openCover (hP : CommRing.PropertyIsLocal P) (X : Scheme.{u}) :
    IsLocally P X ↔
      ∃ (ι : Type u) (U : ι → X.Opens),
        IsOpenCover U ∧ ∀ i, IsLocally P (U i).toScheme
Tag 01OS, a lemma

Tag 01OS in the Stacks Project.

AlgebraicGeometry.isReduced_iff_isLocally_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/LocalRingProperty.lean, line 215. The attribute's comment: “Both directions, for an arbitrary scheme and with no further hypotheses: AlgebraicGeometry.IsReduced X is equivalent to IsLocally applied to reducedness of rings, which is locally reduced in the sense of Definition 01OQ.”.

A scheme is reduced exactly when it is locally reduced: every point has an affine open neighbourhood whose ring of sections is a reduced ring.

theorem isReduced_iff_isLocally_isReduced (X : Scheme.{u}) :
    IsReduced X ↔ IsLocally (fun (R : Type u) [CommRing R] => _root_.IsReduced R) X
Tag 01OT, a lemma

Tag 01OT in the Stacks Project.

CommRing.finiteType_int_isLocal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/LocalRingProperty.lean, line 97. The attribute's comment: “part (3) (absolutely Noetherian): being of finite type over ℤ is a local property”.

Being a finite-type algebra over the integers is a local property of commutative rings.

theorem finiteType_int_isLocal :
    PropertyIsLocal
      (fun (R : Type u) [CommRing R] => Algebra.FiniteType ℤ R)

CommRing.isNoetherianCohenMacaulayRing_propertyIsLocal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/LocalRingProperty.lean, line 158. The attribute's comment: “part (1) (Cohen-Macaulay): being Noetherian and Cohen-Macaulay is a local property”.

The property of a commutative ring of being Noetherian and Cohen–Macaulay is local.

public theorem isNoetherianCohenMacaulayRing_propertyIsLocal :
    PropertyIsLocal
      (fun (R : Type u) [hR : CommRing R] =>
        ∃ hN : IsNoetherianRing R, @IsCohenMacaulayRing R hR hN)

CommRing.isRegularRing_propertyIsLocal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/LocalRingProperty.lean, line 184. The attribute's comment: “part (2) (regular): being Noetherian and regular is a local property”.

Being a Noetherian regular ring is local on the spectrum.

theorem isRegularRing_propertyIsLocal :
    PropertyIsLocal (fun (R : Type u) [CommRing R] => IsRegularRing R)
Sources
LeanCommRing.PropertyIsLocal · AlgebraicGeometry.IsLocally · AlgebraicGeometry.isLocally_iff_forall_affineOpens · AlgebraicGeometry.isLocally_iff_exists_affineOpenCover · AlgebraicGeometry.isLocally_open · AlgebraicGeometry.isLocally_iff_exists_openCover · AlgebraicGeometry.isReduced_iff_isLocally_isReduced · CommRing.finiteType_int_isLocal

Section28.5 Noetherian schemes#

Section 28.5 of the Stacks Project, Tag 01OU. 10 tags here are carried by 15 declarations of the repository (all in StacksFrontier) and 8 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01OV, a definition

Tag 01OV in the Stacks Project.

Declarations registered for the tag:

Tag 01OW, a lemma

Tag 01OW in the Stacks Project.

Declarations registered for the tag:

Tag 01OX, a lemma

Tag 01OX in the Stacks Project.

AlgebraicGeometry.quasiCompact_of_isImmersion, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/NoetherianImmersion.lean, line 43. The attribute's comment: “all immersions”. References: SGA 3 VIB (1.4.2).

An immersion into a locally Noetherian scheme is quasi-compact.

instance (priority := 50) quasiCompact_of_isImmersion
    {X Z : Scheme.{u}} [IsLocallyNoetherian X]
    {f : Z ⟶ X} [IsImmersion f] : QuasiCompact f
Tag 01OZ, a lemma

Tag 01OZ in the Stacks Project.

AlgebraicGeometry.isLocallyNoetherianSpace_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Noetherian.lean, line 53. The attribute's comment: “the (locally) half: a locally Noetherian scheme has a locally Noetherian space”.

The underlying topological space of a locally Noetherian scheme is locally Noetherian.

theorem isLocallyNoetherianSpace_of_isLocallyNoetherian
    (X : Scheme) [IsLocallyNoetherian X] :
    IsLocallyNoetherianSpace X
Tag 02IK, a lemma

Tag 02IK in the Stacks Project.

AlgebraicGeometry.isLocallyNoetherian_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/NoetherianLocallyClosed.lean, line 55. The attribute's comment: “the locally Noetherian case, for the source of an arbitrary immersion”. References: EGA I (6.1.4).

A locally closed subscheme of a locally Noetherian scheme is locally Noetherian: the source of an immersion into a locally Noetherian scheme is locally Noetherian.

theorem isLocallyNoetherian_of_isImmersion [IsImmersion f] [IsLocallyNoetherian X] :
    IsLocallyNoetherian Z

AlgebraicGeometry.isNoetherian_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/NoetherianLocallyClosed.lean, line 69. The attribute's comment: “the Noetherian case, for the source of an arbitrary immersion”. References: EGA I (6.1.4).

A locally closed subscheme of a Noetherian scheme is Noetherian: the source of an immersion into a Noetherian scheme is Noetherian.

theorem isNoetherian_of_isImmersion [IsImmersion f] [IsNoetherian X] : IsNoetherian Z
Tag 02IL, a lemma

Tag 02IL in the Stacks Project.

AlgebraicGeometry.closedPoints_nonempty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/NoetherianClosedPoints.lean, line 96. The attribute's comment: “nonempty scheme”.

Every nonempty locally Noetherian scheme has a closed point.

theorem closedPoints_nonempty (X : Scheme.{u}) [IsLocallyNoetherian X] [Nonempty X] :
    (closedPoints X).Nonempty

AlgebraicGeometry.nonempty_inter_closedPoints_of_isClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/NoetherianClosedPoints.lean, line 253. The attribute's comment: “nonempty closed subset”. References: EGA IV (5.1.11).

Every nonempty closed subset of a locally Noetherian scheme contains a point that is closed in the ambient scheme.

theorem nonempty_inter_closedPoints_of_isClosed (X : Scheme.{u}) [IsLocallyNoetherian X]
    {Z : Set X} (hZ : Z.Nonempty) (hZ' : IsClosed Z) :
    (Z ∩ closedPoints X).Nonempty

AlgebraicGeometry.exists_specializes_closedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/NoetherianClosedPoints.lean, line 278. The attribute's comment: “closed specialization”.

Every point of a locally Noetherian scheme specializes to a closed point.

theorem exists_specializes_closedPoint (X : Scheme.{u}) [IsLocallyNoetherian X] (x : X) :
    ∃ y ∈ closedPoints X, Specializes x y
Tag 054F, a lemma

Tag 054F in the Stacks Project.

AlgebraicGeometry.exists_dvr_morphism_of_specializes_with_residueField_equiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/DiscreteValuation.lean, line 226. The attribute's comment: “part (2)”. References: EGA II (7.1.4), “special case”; EGA II (7.1.9), “more general”; EGA IV (15.5.2.2), “1°”; SGA 3 XV (3.3), “partial”.

Stacks Project, Tag 054F, part (2). For a strict specialization and a finitely generated extension K of the residue field at the generic point, the realizing discrete valuation ring can be chosen so that its generic residue field is isomorphic to K over that residue field.

theorem exists_dvr_morphism_of_specializes_with_residueField_equiv
    (X : Scheme.{u}) [IsLocallyNoetherian X] {x' x : X}
    (h : x' ⤳ x) (hne : x ≠ x')
    (K : Type u) [Field K] [Algebra (X.residueField x') K]
    [Algebra.EssFiniteType (X.residueField x') K] :
    ∃ (R : Type u) (_ : CommRing R) (_ : IsDomain R)
      (_ : IsDiscreteValuationRing R) (f : Spec (.of R) ⟶ X)
      (hη : f (genericPoint (Spec (.of R))) = x'),
      f (IsLocalRing.closedPoint R) = x ∧
        ∃ e : (Spec (.of R)).residueField (genericPoint (Spec (.of R))) ≃+* K,
          ∀ a : X.residueField x',
            e (f.residueFieldMap (genericPoint (Spec (.of R)))
              ((X.residueFieldCongr hη.symm).hom a)) =
              algebraMap (X.residueField x') K a

AlgebraicGeometry.exists_dvr_morphism_of_specializes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/DiscreteValuation.lean, line 309. The attribute's comment: “part (1)”.

Stacks Project, Tag 054F, part (1). A specialization of points on a locally Noetherian scheme is the image of the generic-to-closed specialization on the spectrum of a discrete valuation ring.

theorem exists_dvr_morphism_of_specializes (X : Scheme.{u}) [IsLocallyNoetherian X]
    {x' x : X} (h : x' ⤳ x) :
    ∃ (R : Type u) (_ : CommRing R) (_ : IsDomain R)
      (_ : IsDiscreteValuationRing R) (f : Spec (.of R) ⟶ X),
      f (genericPoint (Spec (.of R))) = x' ∧
        f (IsLocalRing.closedPoint R) = x
Tag 0CXG, a lemma

Tag 0CXG in the Stacks Project.

AlgebraicGeometry.exists_infinite_subset_pairwise_not_specializes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Specialization.lean, line 97.

An infinite set of points on a Noetherian scheme contains an infinite subset with no nontrivial specializations among its points.

theorem exists_infinite_subset_pairwise_not_specializes (S : Scheme.{u}) [IsNoetherian S]
    {T : Set S} (hT : T.Infinite) :
    ∃ T' : Set S, T' ⊆ T ∧ T'.Infinite ∧
      ∀ ⦃x y : S⦄, x ∈ T' → y ∈ T' → x ≠ y → ¬ x ⤳ y
Tag 0G2R, a lemma

Tag 0G2R in the Stacks Project.

maximalPoints, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/MaximalPoints.lean, line 56. The attribute's comment: “the set of maximal points”.

The points of T which admit no nontrivial generalization belonging to T.

def maximalPoints {X : Type u} [TopologicalSpace X] (T : Set X) : Set X

specialization_eq_of_mem_maximalPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/MaximalPoints.lean, line 61. The attribute's comment: “part (a)”.

There is no nontrivial specialization between maximal points of a subset.

theorem specialization_eq_of_mem_maximalPoints
    {X : Type u} [TopologicalSpace X] {T : Set X} {x y : X}
    (hx : x ∈ maximalPoints T) (hy : y ∈ maximalPoints T)
    (hxy : x ⤳ y) : x = y

AlgebraicGeometry.exists_maximalPoint_specializes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/MaximalPoints.lean, line 72. The attribute's comment: “part (b)”.

Every point of a subset of a Noetherian scheme is a specialization of a maximal point of that subset.

theorem exists_maximalPoint_specializes
    (X : Scheme.{u}) [IsNoetherian X] (T : Set X) {x : X} (hx : x ∈ T) :
    ∃ y ∈ maximalPoints T, y ⤳ x

AlgebraicGeometry.closure_maximalPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/MaximalPoints.lean, line 103. The attribute's comment: “part (c)”.

The maximal points of a subset of a Noetherian scheme have the same closure as the subset.

theorem closure_maximalPoints
    (X : Scheme.{u}) [IsNoetherian X] (T : Set X) :
    closure (maximalPoints T) = closure T
Tag 0G2F, a lemma

Tag 0G2F in the Stacks Project.

AlgebraicGeometry.exists_countable_dense_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/MaximalPoints.lean, line 290.

An infinite dense subset of a Noetherian scheme contains a countable dense subset.

theorem exists_countable_dense_subset (S : Scheme.{u}) [IsNoetherian S]
    (T : Set S) (_hT_infinite : T.Infinite) (hT_dense : Dense T) :
    ∃ E : Set S, E ⊆ T ∧ E.Countable ∧ Dense E
Sources
LeanAlgebraicGeometry.IsLocallyNoetherian · AlgebraicGeometry.isLocallyNoetherian_iff_of_iSup_eq_top · AlgebraicGeometry.IsNoetherian · AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover · AlgebraicGeometry.isLocallyNoetherian_iff_openCover · AlgebraicGeometry.isLocallyNoetherian_of_isOpenImmersion · AlgebraicGeometry.quasiCompact_of_isImmersion · AlgebraicGeometry.isLocallyNoetherianSpace_of_isLocallyNoetherian

Section28.6 Jacobson schemes#

Section 28.6 of the Stacks Project, Tag 01P1. 4 tags here are carried by 5 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01P2, a definition

Tag 01P2 in the Stacks Project.

Declarations registered for the tag:

Tag 01P3, a lemma

Tag 01P3 in the Stacks Project.

Declarations registered for the tag:

Tag 01P4, a lemma

Tag 01P4 in the Stacks Project.

AlgebraicGeometry.jacobsonSpace_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Jacobson.lean, line 99. The attribute's comment: “the equivalence of the five conditions (1)–(5)”. References: EGA IV (10.3.3), “sufficiency”; EGA IV (10.4.2).

For a scheme X the following are equivalent: X is a Jacobson space; X is locally Jacobson in the sense of Definition 01OQ; the ring of sections over every affine open of X is Jacobson; there is an affine open covering of X whose rings of sections are Jacobson; there is an open covering of X by Jacobson open subschemes.

theorem jacobsonSpace_tfae (X : Scheme.{u}) :
    List.TFAE [
      JacobsonSpace X,
      IsLocally (fun (R : Type u) [CommRing R] => IsJacobsonRing R) X,
      ∀ U : X.affineOpens, IsJacobsonRing Γ(X, (U : X.Opens)),
      ∃ (I : Type u) (U : I → X.affineOpens),
        IsOpenCover (fun i ↦ (U i : X.Opens)) ∧
          ∀ i, IsJacobsonRing Γ(X, (U i : X.Opens)),
      ∃ (I : Type u) (U : I → X.Opens),
        IsOpenCover U ∧ ∀ i, JacobsonSpace (U i).toScheme]

AlgebraicGeometry.jacobsonSpace_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Jacobson.lean, line 130. The attribute's comment: “the final assertion: every open subscheme of a Jacobson scheme is Jacobson”. References: EGA IV (10.4.3), “Open subpreschemes”.

Every open subscheme of a Jacobson scheme is Jacobson.

theorem jacobsonSpace_open {X : Scheme.{u}} (hX : JacobsonSpace X) (U : X.Opens) :
    JacobsonSpace U.toScheme

Declarations registered for the tag:

Tag 02IM, a lemma

Tag 02IM in the Stacks Project.

PrimeSpectrum.jacobsonSpace_compl_closedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/JacobsonPuncturedSpectrum/Basic.lean, line 93. The attribute's comment: “part (1)”. References: EGA IV (10.5.9), “Jacobson part”; EGA IV (10.5.7), “Noetherian local ring”; EGA IV (10.5.8), “local case”.

Stacks Project, Tag 02IM, part (1). The punctured spectrum of a Noetherian local ring is a Jacobson space.

theorem jacobsonSpace_compl_closedPoint
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] :
    JacobsonSpace ↥(({IsLocalRing.closedPoint R} : Set (PrimeSpectrum R))ᶜ)

PrimeSpectrum.jacobsonSpace_compl_zeroLocus_jacobson, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/JacobsonPuncturedSpectrum/Basic.lean, line 109. The attribute's comment: “part (2)”. References: EGA IV (10.5.8), “Spec(A)-V(R) Jacobson”; EGA IV (10.5.9), “Y is Jacobson”; EGA IV (10.5.7), “affine case”.

Stacks Project, Tag 02IM, part (2). The complement of the vanishing locus of the Jacobson radical of a Noetherian ring is a Jacobson space.

theorem jacobsonSpace_compl_zeroLocus_jacobson
    (R : Type u) [CommRing R] [IsNoetherianRing R] :
    JacobsonSpace
      ↥((PrimeSpectrum.zeroLocus (Ring.jacobson R : Set R))ᶜ)

PrimeSpectrum.jacobsonSpace_compl_zeroLocus_of_le_jacobson, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/JacobsonPuncturedSpectrum/Basic.lean, line 119. The attribute's comment: “part (3)”.

Stacks Project, Tag 02IM, part (3). If (R, I) is a Noetherian Zariski pair, that is if R is Noetherian and I is contained in the Jacobson radical of R, then Spec R \ V(I) is a Jacobson space.

theorem jacobsonSpace_compl_zeroLocus_of_le_jacobson
    (R : Type u) [CommRing R] [IsNoetherianRing R]
    (I : Ideal R) (hI : I ≤ Ring.jacobson R) :
    JacobsonSpace ↥((PrimeSpectrum.zeroLocus (I : Set R))ᶜ)
Sources
LeanJacobsonSpace · PrimeSpectrum.isJacobsonRing_iff_jacobsonSpace · AlgebraicGeometry.jacobsonSpace_tfae · AlgebraicGeometry.jacobsonSpace_open · JacobsonSpace.of_isOpenEmbedding · PrimeSpectrum.jacobsonSpace_compl_closedPoint · PrimeSpectrum.jacobsonSpace_compl_zeroLocus_jacobson · PrimeSpectrum.jacobsonSpace_compl_zeroLocus_of_le_jacobson

Section28.7 Normal schemes#

Section 28.7 of the Stacks Project, Tag 033H. 8 tags here are carried by 9 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 033I, a definition

Tag 033I in the Stacks Project.

AlgebraicGeometry.IsNormal, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Normal.lean, line 85.

A scheme is normal if each stalk of its structure sheaf is a normal domain.

class IsNormal (X : Scheme.{u}) : Prop
Tag 033J, a lemma

Tag 033J in the Stacks Project.

AlgebraicGeometry.isNormal_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Normal.lean, line 157. The attribute's comment: “equivalent conditions”.

Stacks Project, Tag 033J. Normality of a scheme is equivalent to normality of the section ring on every affine open, on one affine open covering, or to the existence of an open covering by normal open subschemes.

public theorem isNormal_tfae (X : Scheme.{u}) :
    List.TFAE [
      IsNormal X,
      ∀ U : X.affineOpens, IsNormalRing Γ(X, U),
      ∃ (I : Type u) (U : I → X.affineOpens),
        IsOpenCover (fun i ↦ (U i : X.Opens)) ∧
          ∀ i, IsNormalRing Γ(X, U i),
      ∃ (I : Type u) (U : I → X.Opens),
        IsOpenCover U ∧ ∀ i, IsNormal (U i).toScheme]

AlgebraicGeometry.isNormal_open, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Normal.lean, line 187. The attribute's comment: “open subschemes”.

Stacks Project, Tag 033J. Every open subscheme of a normal scheme is normal.

public instance isNormal_open {X : Scheme.{u}} [IsNormal X]
    (U : X.Opens) : IsNormal U.toScheme
Tag 033K, a lemma

Tag 033K in the Stacks Project.

AlgebraicGeometry.isReduced_of_isNormal, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Normal.lean, line 193. References: EGA II (7.3.7), “partial”; EGA IV (20.4.12), “partial”.

A normal scheme is reduced.

instance isReduced_of_isNormal (X : Scheme.{u}) [IsNormal X] : IsReduced X
Tag 033L, a lemma

Tag 033L in the Stacks Project.

AlgebraicGeometry.isNormal_iff_forall_affineOpen_normal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Normal.lean, line 199.

Stacks Project, Tag 033L. An integral scheme is normal if and only if the ring of sections on every nonempty affine open is a normal domain.

public theorem isNormal_iff_forall_affineOpen_normal (X : Scheme.{u}) [IsIntegral X] :
    IsNormal X ↔
      ∀ U : X.affineOpens, ∀ _hU : Nonempty U.1,
        letI : IsDomain Γ(X, U.1) := IsIntegral.component_integral U.1
        IsIntegrallyClosed Γ(X, U.1)
Tag 0357, a lemma

Tag 0357 in the Stacks Project.

AlgebraicGeometry.isNormal_iff_exists_iso_coproduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Normal.lean, line 357.

A scheme whose quasi-compact open subspaces have finitely many irreducible components is normal if and only if it is isomorphic to a coproduct of normal integral schemes.

public theorem isNormal_iff_exists_iso_coproduct
    {X : Scheme.{u}}
    (hX : ∀ (U : X.Opens), IsCompact (U : Set X) → (irreducibleComponents U).Finite) :
    IsNormal X ↔
      ∃ (ι : Type u) (Y : ι → Scheme.{u})
          (_ : ∀ i, IsNormal (Y i)) (_ : ∀ i, IsIntegral (Y i)),
        Nonempty (X ≅ ∐ Y)
Tag 033M, a lemma

Tag 033M in the Stacks Project.

AlgebraicGeometry.isNormal_iff_exists_iso_finite_coproduct_integral_normal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/NormalCoproduct.lean, line 55.

A Noetherian scheme is normal if and only if it is isomorphic to a finite coproduct of normal integral schemes.

public theorem isNormal_iff_exists_iso_finite_coproduct_integral_normal
    (X : Scheme.{u}) [IsNoetherian X] :
    IsNormal X ↔
      ∃ (ι : Type u) (_ : Finite ι) (Y : ι → Scheme.{u})
          (_ : ∀ i, IsNormal (Y i)) (_ : ∀ i, IsIntegral (Y i)),
        Nonempty (X ≅ ∐ Y)
Tag 033N, a lemma

Tag 033N in the Stacks Project.

AlgebraicGeometry.isNormal_iff_exists_iso_coproduct_integral_normal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/NormalCoproduct.lean, line 44.

A locally Noetherian scheme is normal if and only if it is isomorphic to a coproduct of normal integral schemes.

public theorem isNormal_iff_exists_iso_coproduct_integral_normal
    (X : Scheme.{u}) [IsLocallyNoetherian X] :
    IsNormal X ↔
      ∃ (ι : Type u) (Y : ι → Scheme.{u})
          (_ : ∀ i, IsNormal (Y i)) (_ : ∀ i, IsIntegral (Y i)),
        Nonempty (X ≅ ∐ Y)
Tag 0358, a lemma

Tag 0358 in the Stacks Project.

AlgebraicGeometry.normal_globalSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Normal.lean, line 241. References: EGA II (8.8.6.1).

The ring of global sections of an integral normal scheme is a normal domain.

theorem normal_globalSections (X : Scheme.{u}) [IsIntegral X] [IsNormal X] :
    IsIntegrallyClosed Γ(X, ⊤)
Sources
LeanAlgebraicGeometry.IsNormal · AlgebraicGeometry.isNormal_tfae · AlgebraicGeometry.isNormal_open · AlgebraicGeometry.isReduced_of_isNormal · AlgebraicGeometry.isNormal_iff_forall_affineOpen_normal · AlgebraicGeometry.isNormal_iff_exists_iso_coproduct · AlgebraicGeometry.isNormal_iff_exists_iso_finite_coproduct_integral_normal · AlgebraicGeometry.isNormal_iff_exists_iso_coproduct_integral_normal

Section28.8 Cohen-Macaulay schemes#

Section 28.8 of the Stacks Project, Tag 02IN. 3 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02IO, a definition

Tag 02IO in the Stacks Project.

AlgebraicGeometry.IsCohenMacaulay, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/CohenMacaulay.lean, line 47. References: EGA IV (5.7.1).

Cohen–Macaulay scheme. A scheme X is Cohen–Macaulay if every point belongs to an affine open U whose ring of sections Γ(X, U) is Noetherian and Cohen–Macaulay.

public def IsCohenMacaulay (X : Scheme.{u}) : Prop
Tag 02IP, a lemma

Tag 02IP in the Stacks Project.

AlgebraicGeometry.isCohenMacaulay_tfae_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/CohenMacaulayCharacterization.lean, line 185. References: EGA IV (5.7.1).

A scheme is Cohen–Macaulay if and only if it is locally Noetherian with Cohen–Macaulay local rings at every point, if and only if it is locally Noetherian with Cohen–Macaulay local rings at closed points.

theorem isCohenMacaulay_tfae_stalk (X : Scheme.{u}) :
    List.TFAE [
      IsCohenMacaulay X,
      IsLocallyNoetherian X ∧
        (∀ x : X, ∃ h : IsNoetherianRing (X.presheaf.stalk x),
          @IsCohenMacaulayLocalRing (X.presheaf.stalk x) _ h _),
      IsLocallyNoetherian X ∧
        (∀ x : X, x ∈ closedPoints X →
          ∃ h : IsNoetherianRing (X.presheaf.stalk x),
            @IsCohenMacaulayLocalRing (X.presheaf.stalk x) _ h _)]
Tag 02IQ, a lemma

Tag 02IQ in the Stacks Project.

AlgebraicGeometry.isCohenMacaulay_tfae_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/CohenMacaulayCharacterization.lean, line 413. The attribute's comment: “equivalent conditions”. References: EGA IV (5.7.1), “more general”.

Cohen–Macaulayness of a scheme is equivalent to the Noetherian Cohen–Macaulay condition on every affine coordinate ring, to that condition on one affine open covering, and to having an open covering by Cohen–Macaulay schemes.

theorem isCohenMacaulay_tfae_cover (X : Scheme.{u}) :
    List.TFAE [
      IsCohenMacaulay X,
      ∀ U : X.affineOpens, ∃ h : IsNoetherianRing Γ(X, U.val),
        @IsCohenMacaulayRing Γ(X, U.val) _ h,
      ∃ (I : Type u) (U : I → X.affineOpens),
        (⨆ i, (U i).val) = ⊤ ∧
          ∀ i, ∃ h : IsNoetherianRing Γ(X, (U i).val),
            @IsCohenMacaulayRing Γ(X, (U i).val) _ h,
      ∃ (I : Type u) (U : I → X.Opens),
        (⨆ i, U i) = ⊤ ∧ ∀ i, IsCohenMacaulay (U i).toScheme]

AlgebraicGeometry.IsCohenMacaulay.restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/CohenMacaulayCharacterization.lean, line 436. The attribute's comment: “open subschemes”.

Every open subscheme of a Cohen–Macaulay scheme is Cohen–Macaulay.

theorem IsCohenMacaulay.restrict {X : Scheme.{u}} (hX : IsCohenMacaulay X) (U : X.Opens) :
    IsCohenMacaulay U.toScheme
Sources
LeanAlgebraicGeometry.IsCohenMacaulay · AlgebraicGeometry.isCohenMacaulay_tfae_stalk · AlgebraicGeometry.isCohenMacaulay_tfae_cover · AlgebraicGeometry.IsCohenMacaulay.restrict

Section28.9 Regular schemes#

Section 28.9 of the Stacks Project, Tag 02IR. 4 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02IS, a definition

Tag 02IS in the Stacks Project.

AlgebraicGeometry.IsRegular, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Regular.lean, line 68. The attribute's comment: “the source's requirement on 𝒪_X(U), Noetherian and regular, is Mathlib's class IsRegularRing: it extends IsNoetherianRing, and its further field is that the localization at every prime is a regular local ring. Both halves of the requirement are therefore written into this definition, the Noetherian one recoverable as IsRegularRing.toIsNoetherian; see the module docstring”.

A scheme is regular, or nonsingular, if every point has an affine open neighbourhood whose ring of sections is Noetherian and regular.

public abbrev IsRegular (X : Scheme.{u}) : Prop
Tag 02IT, a lemma

Tag 02IT in the Stacks Project.

AlgebraicGeometry.isRegular_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/RegularCharacterization.lean, line 144.

A scheme is regular if and only if it is locally Noetherian with regular local rings at every point, if and only if it is locally Noetherian with regular local rings at closed points.

theorem isRegular_tfae (X : Scheme.{u}) :
    List.TFAE [
      IsRegular X,
      IsLocallyNoetherian X ∧ ∀ x : X, IsRegularLocalRing (X.presheaf.stalk x),
      IsLocallyNoetherian X ∧
        (∀ x : X, x ∈ closedPoints X → IsRegularLocalRing (X.presheaf.stalk x))]
Tag 02IU, a lemma

Tag 02IU in the Stacks Project.

AlgebraicGeometry.isRegular_tfae_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/RegularCharacterization.lean, line 255. The attribute's comment: “equivalent conditions”.

Stacks Project, Tag 02IU. A scheme is regular if and only if the ring of sections is regular on every affine open, if and only if it is regular on the members of one affine open covering, if and only if the scheme has an open covering by regular open subschemes.

theorem isRegular_tfae_cover (X : Scheme.{u}) :
    List.TFAE [
      IsRegular X,
      ∀ U : X.affineOpens, IsRegularRing Γ(X, U),
      ∃ (I : Type u) (U : I → X.affineOpens),
        (⨆ i, (U i).val) = ⊤ ∧ ∀ i, IsRegularRing Γ(X, U i),
      ∃ (I : Type u) (U : I → X.Opens),
        (⨆ i, U i) = ⊤ ∧ ∀ i, IsRegular (U i).toScheme]

AlgebraicGeometry.IsRegular.restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/RegularCharacterization.lean, line 276. The attribute's comment: “open subschemes”.

Stacks Project, Tag 02IU. Every open subscheme of a regular scheme is regular.

theorem IsRegular.restrict {X : Scheme.{u}} (hX : IsRegular X) (U : X.Opens) :
    IsRegular U.toScheme
Tag 0569, a lemma

Tag 0569 in the Stacks Project.

AlgebraicGeometry.isNormal_of_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Regular.lean, line 74. The attribute's comment: “a regular scheme is normal; the sole hypothesis is IsRegular of Tag 02IS, whose IsRegularRing already carries Noetherianness, so nothing beyond the source is assumed”.

Stacks Project, Tag 0569. Every regular scheme is normal.

public theorem isNormal_of_isRegular (X : Scheme.{u}) (hX : IsRegular X) :
    IsNormal X
Sources
LeanAlgebraicGeometry.IsRegular · AlgebraicGeometry.isRegular_tfae · AlgebraicGeometry.isRegular_tfae_cover · AlgebraicGeometry.IsRegular.restrict · AlgebraicGeometry.isNormal_of_isRegular

Section28.10 Dimension#

Section 28.10 of the Stacks Project, Tag 04MS. 6 tags here are carried by 9 declarations of the repository (all in StacksFrontier) and 4 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04MT, a definition

Tag 04MT in the Stacks Project.

Declarations registered for the tag:

Tag 04MU, a lemma

Tag 04MU in the Stacks Project.

AlgebraicGeometry.topologicalKrullDim_eq_iSup_krullDimOfRing_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Dimension.lean, line 78. The attribute's comment: “dimension_sup_local_rings”. References: EGA IV (5.1.4).

The dimension of a scheme is the supremum of the Krull dimensions of its local rings.

theorem topologicalKrullDim_eq_iSup_krullDimOfRing_stalk (X : Scheme.{u}) :
    topologicalKrullDim X = ⨆ x : X, ringKrullDim (X.presheaf.stalk x)

Declarations registered for the tag:

Tag 02IZ, a lemma

Tag 02IZ in the Stacks Project.

AlgebraicGeometry.codimension_eq_ringKrullDim_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/CodimensionLocalRing.lean, line 67. References: EGA IV (21.6.2), “partial”; EGA IV (5.1.2); EGA IV (5.1.3), “special case”.

Stacks 02IZ. Let X be a scheme, let Y ⊆ X be an irreducible closed subset and let ξ be the generic point of Y. Then the codimension of Y in X, in the sense of Stacks 02I3, is the Krull dimension of the local ring 𝒪_{X, ξ}.

theorem codimension_eq_ringKrullDim_stalk {X : Scheme.{u}} (Y : IrreducibleCloseds X) (ξ : X)
    (hξ : IsGenericPoint ξ (Y : Set X)) :
    (codimension Y : WithBot ℕ∞) = ringKrullDim (X.presheaf.stalk ξ)
Tag 0AAX, a lemma

Tag 0AAX in the Stacks Project.

AlgebraicGeometry.isArtinianRing_stalk_of_topologicalKrullDim_le_zero, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Dimension.lean, line 95. The attribute's comment: “the summands are spectra of Artinian local rings”.

The local rings of a locally Noetherian scheme of dimension at most zero are Artinian.

lemma isArtinianRing_stalk_of_topologicalKrullDim_le_zero
    (X : Scheme.{u}) [IsLocallyNoetherian X]
    (hX : topologicalKrullDim X ≤ 0) (x : X) :
    IsArtinianRing (X.presheaf.stalk x)

AlgebraicGeometry.isIso_sigmaFromSpecStalk_of_topologicalKrullDim_le_zero, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Dimension.lean, line 108. The attribute's comment: “the disjoint-union decomposition”.

A locally Noetherian scheme of dimension at most zero is the coproduct of the spectra of its local rings.

lemma isIso_sigmaFromSpecStalk_of_topologicalKrullDim_le_zero
    (X : Scheme.{u}) [IsLocallyNoetherian X]
    (hX : topologicalKrullDim X ≤ 0) :
    IsIso (sigmaFromSpecStalk X)
Tag 0CKV, a lemma

Tag 0CKV in the Stacks Project.

AlgebraicGeometry.separation_tfae_of_topologicalKrullDim_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/DimensionZero.lean, line 195. The attribute's comment: “separation_equivalences”.

Stacks Project, Tag 0CKV. For a scheme of dimension zero, quasi-separatedness, separatedness, Hausdorffness of the underlying space, and closedness of every affine open are equivalent.

theorem separation_tfae_of_topologicalKrullDim_eq_zero (X : Scheme.{u})
    (hX : topologicalKrullDim X = 0) :
    List.TFAE [
      QuasiSeparatedSpace X,
      X.IsSeparated,
      T2Space X,
      ∀ U : X.Opens, IsAffineOpen U → IsClosed (U : Set X)]

AlgebraicGeometry.connectedComponent_eq_singleton_of_topologicalKrullDim_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/DimensionZero.lean, line 257. The attribute's comment: “connected_components”.

Stacks Project, Tag 0CKV. The connected components of a quasi-separated zero-dimensional scheme are its points.

theorem connectedComponent_eq_singleton_of_topologicalKrullDim_eq_zero (X : Scheme.{u})
    [QuasiSeparatedSpace X] (hX : topologicalKrullDim X = 0) (x : X) :
    connectedComponent x = {x}

AlgebraicGeometry.isAffineOpen_of_isCompact_of_topologicalKrullDim_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/DimensionZero.lean, line 343. The attribute's comment: “quasicompact_open_affine”.

Stacks Project, Tag 0CKV. Every quasi-compact open subset of a quasi-separated scheme of dimension zero is affine.

theorem isAffineOpen_of_isCompact_of_topologicalKrullDim_eq_zero (X : Scheme.{u})
    [QuasiSeparatedSpace X] (hX : topologicalKrullDim X = 0) (U : X.Opens)
    (hU : IsCompact (U : Set X)) : IsAffineOpen U

AlgebraicGeometry.isAffine_of_topologicalKrullDim_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/DimensionZero.lean, line 352. The attribute's comment: “quasicompact_affine”.

Stacks Project, Tag 0CKV. A quasi-compact, quasi-separated scheme of dimension zero is affine.

theorem isAffine_of_topologicalKrullDim_eq_zero (X : Scheme.{u}) [CompactSpace X]
    [QuasiSeparatedSpace X] (hX : topologicalKrullDim X = 0) : IsAffine X
Tag 0H7C, a lemma

Tag 0H7C in the Stacks Project.

AlgebraicGeometry.topologicalKrullDimAt_eq_zero_iff_isIsolatedPoint, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Dimension.lean, line 181. References: EGA 0 (14.1.10), “loc. Noetherian scheme”.

A point of a locally Noetherian scheme has local dimension zero exactly when it is an isolated point.

public lemma topologicalKrullDimAt_eq_zero_iff_isIsolatedPoint
    (X : Scheme) [IsLocallyNoetherian X] (x : X) :
    topologicalKrullDimAt X x = 0 ↔ IsIsolatedPoint x
Sources
LeantopologicalKrullDim · topologicalKrullDimAt · AlgebraicGeometry.topologicalKrullDim_eq_iSup_krullDimOfRing_stalk · TopologicalSpace.topologicalKrullDim_eq_iSup_localKrullDim · TopologicalSpace.topologicalKrullDimAt_eq_localKrullDim · AlgebraicGeometry.codimension_eq_ringKrullDim_stalk · AlgebraicGeometry.isArtinianRing_stalk_of_topologicalKrullDim_le_zero · AlgebraicGeometry.isIso_sigmaFromSpecStalk_of_topologicalKrullDim_le_zero

Section28.11 Catenary schemes#

Section 28.11 of the Stacks Project, Tag 02IV. 4 tags here are carried by 4 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02IW, a definition

Tag 02IW in the Stacks Project.

Declarations registered for the tag:

Tag 02IX, a lemma

Tag 02IX in the Stacks Project.

AlgebraicGeometry.isCatenarySpace_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/SchemeTypesAndCatenary/Catenary.lean, line 186. The attribute's comment: “local criteria”.

A scheme is catenary exactly when this holds on an open covering, or when the rings of sections of every affine open (equivalently, of one affine open covering) are catenary.

public theorem isCatenarySpace_tfae (S : Scheme.{u}) :
    List.TFAE [
      IsCatenarySpace S,
      ∃ (ι : Type u) (U : ι → S.Opens),
        IsOpenCover U ∧ ∀ i, IsCatenarySpace (U i).toScheme,
      ∀ U : S.affineOpens, Ring.IsCatenary Γ(S, U),
      ∃ (ι : Type u) (U : ι → S.affineOpens),
        IsOpenCover (fun i ↦ (U i : S.Opens)) ∧
          ∀ i, Ring.IsCatenary Γ(S, U i)]

AlgebraicGeometry.IsCatenarySpace.of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/SchemeTypesAndCatenary/Catenary.lean, line 209. The attribute's comment: “locally closed subschemes”.

A locally closed subscheme of a catenary scheme is catenary.

public theorem IsCatenarySpace.of_isImmersion {S Z : Scheme.{u}} (i : Z ⟶ S)
    [IsImmersion i] (hS : IsCatenarySpace S) : IsCatenarySpace Z
Tag 02IY, a lemma

Tag 02IY in the Stacks Project.

AlgebraicGeometry.isCatenarySpace_iff_locally_dimensionFunction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Catenary.lean, line 51. References: SGA 6 X (1.6), “more general”.

A locally Noetherian scheme is catenary if and only if every point has an open neighbourhood admitting a dimension function.

public theorem isCatenarySpace_iff_locally_dimensionFunction
    (S : Scheme.{u}) [IsLocallyNoetherian S] :
    IrreducibleClosedsCodim.IsCatenarySpace S ↔
      ∀ x : S, ∃ U : Set S, IsOpen U ∧ x ∈ U ∧ Nonempty (DimensionFunction U)
Tag 02J0, a lemma

Tag 02J0 in the Stacks Project.

AlgebraicGeometry.isCatenarySpace_iff_stalk_isCatenary, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/SchemeTypesAndCatenary/Catenary.lean, line 308.

A scheme is catenary if and only if each of its local rings is catenary.

public theorem isCatenarySpace_iff_stalk_isCatenary (X : Scheme.{u}) :
    IrreducibleClosedsCodim.IsCatenarySpace X ↔
      ∀ x : X, Ring.IsCatenary (X.presheaf.stalk x)
Sources
LeanIrreducibleClosedsCodim.IsCatenarySpace · AlgebraicGeometry.isCatenarySpace_tfae · AlgebraicGeometry.IsCatenarySpace.of_isImmersion · AlgebraicGeometry.isCatenarySpace_iff_locally_dimensionFunction · AlgebraicGeometry.isCatenarySpace_iff_stalk_isCatenary

Section28.12 Serre's conditions#

Section 28.12 of the Stacks Project, Tag 033P. 7 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 033Q, a definition

Tag 033Q in the Stacks Project.

AlgebraicGeometry.IsRegularInCodimension, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Serre.lean, line 76. The attribute's comment: “property_rk”. References: EGA IV (5.8.2).

A scheme is regular in codimension k (has property (R_k)) if each of its local rings of Krull dimension at most k is regular.

public abbrev IsRegularInCodimension (X : Scheme) (k : ℕ) : Prop

AlgebraicGeometry.HasPropertySk, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Serre.lean, line 83. The attribute's comment: “property_sk”.

Serre's property (Sₖ) for a locally Noetherian scheme: at every point, the depth of the local ring is at least the minimum of k and the dimension of that local ring.

def HasPropertySk (X : Scheme.{u}) [IsLocallyNoetherian X] (k : ℕ) : Prop
Tag 0B3C, a lemma

Tag 0B3C in the Stacks Project.

AlgebraicGeometry.isRegular_iff_forall_isRegularInCodimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/RegularCharacterization.lean, line 288.

Stacks Project, Tag 0B3C. A locally Noetherian scheme is regular if and only if it is regular in codimension k for every nonnegative integer k.

theorem isRegular_iff_forall_isRegularInCodimension (X : Scheme.{u}) [IsLocallyNoetherian X] :
    IsRegular X ↔ ∀ k : ℕ, IsRegularInCodimension X k
Tag 0342, a lemma

Tag 0342 in the Stacks Project.

AlgebraicGeometry.isCohenMacaulay_iff_forall_hasPropertySk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/CohenMacaulayCharacterization.lean, line 498.

A locally Noetherian scheme is Cohen–Macaulay if and only if it satisfies Serre's condition (Sₖ) for every nonnegative integer k.

theorem isCohenMacaulay_iff_forall_hasPropertySk
    (X : Scheme.{u}) [IsLocallyNoetherian X] :
    IsCohenMacaulay X ↔ ∀ k : ℕ, HasPropertySk X k
Tag 0344, a lemma

Tag 0344 in the Stacks Project.

AlgebraicGeometry.isReduced_iff_hasPropertyS1_and_isRegularInCodimension_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Serre.lean, line 281. References: EGA IV (5.8.5); EGA IV (7.3.9).

A locally Noetherian scheme is reduced if and only if it satisfies Serre's conditions (S₁) and (R₀).

public theorem isReduced_iff_hasPropertyS1_and_isRegularInCodimension_zero
    (X : Scheme.{u}) [IsLocallyNoetherian X] :
    IsReduced X ↔
      HasPropertySk X 1 ∧ IsRegularInCodimension X 0
Tag 0345, a lemma

Tag 0345 in the Stacks Project.

AlgebraicGeometry.isNormal_iff_hasPropertySk_two_and_isRegularInCodimension_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Serre.lean, line 377. References: EGA II (7.3.7), “partial”; EGA IV (5.8.6); EGA IV (7.3.9).

Serre's criterion for normality, Stacks Project, Tag 0345. A locally Noetherian scheme is normal if and only if it satisfies Serre's condition (S₂) and is regular in codimension one.

public theorem isNormal_iff_hasPropertySk_two_and_isRegularInCodimension_one (X : Scheme.{u})
    [IsLocallyNoetherian X] :
    IsNormal X ↔ HasPropertySk X 2 ∧ IsRegularInCodimension X 1
Tag 0BX2, a lemma

Tag 0BX2 in the Stacks Project.

AlgebraicGeometry.isRegular_of_isNormal_of_topologicalKrullDim_le_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NormalRegular.lean, line 65. References: EGA IV (5.8.6), “(i), dim ≤ 1”.

A locally Noetherian normal scheme of dimension at most one is regular.

public theorem isRegular_of_isNormal_of_topologicalKrullDim_le_one (X : Scheme.{u})
    [IsLocallyNoetherian X] [IsNormal X] (hX : topologicalKrullDim X ≤ 1) :
    IsRegular X
Tag 0B3D, a lemma

Tag 0B3D in the Stacks Project.

AlgebraicGeometry.isCohenMacaulay_of_isNormal_of_topologicalKrullDim_le_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/CohenMacaulayCharacterization.lean, line 517. References: EGA IV (5.8.6), “(ii), dim ≤ 2”.

Stacks Project, Tag 0B3D. A locally Noetherian normal scheme of dimension at most two is Cohen–Macaulay.

theorem isCohenMacaulay_of_isNormal_of_topologicalKrullDim_le_two (X : Scheme.{u})
    [IsLocallyNoetherian X] [IsNormal X] (hX : topologicalKrullDim X ≤ 2) :
    IsCohenMacaulay X
Sources
LeanAlgebraicGeometry.IsRegularInCodimension · AlgebraicGeometry.HasPropertySk · AlgebraicGeometry.isRegular_iff_forall_isRegularInCodimension · AlgebraicGeometry.isCohenMacaulay_iff_forall_hasPropertySk · AlgebraicGeometry.isReduced_iff_hasPropertyS1_and_isRegularInCodimension_zero · AlgebraicGeometry.isNormal_iff_hasPropertySk_two_and_isRegularInCodimension_one · AlgebraicGeometry.isRegular_of_isNormal_of_topologicalKrullDim_le_one · AlgebraicGeometry.isCohenMacaulay_of_isNormal_of_topologicalKrullDim_le_two

Section28.13 Japanese and Nagata schemes#

Section 28.13 of the Stacks Project, Tag 033R. 7 tags here are carried by 9 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 033S, a definition

Tag 033S in the Stacks Project.

IsUniversallyJapaneseScheme, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Nagata.lean, line 60. The attribute's comment: “universally_japanese_scheme”. References: EGA IV (5.11.4); SGA 4 IX (2.14.2).

A scheme is universally Japanese if every point has an affine open neighbourhood whose ring of sections is universally Japanese.

public def IsUniversallyJapaneseScheme
    (X : Scheme.{u}) : Prop

Declarations registered for the tag:

Tag 033U, a lemma

Tag 033U in the Stacks Project.

isNagataScheme_iff_isLocallyNoetherian_and_isUniversallyJapaneseScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Nagata.lean, line 169. The attribute's comment: “the forward implication: a Nagata scheme is locally Noetherian”.

A scheme is Nagata if and only if it is locally Noetherian and universally Japanese.

public theorem isNagataScheme_iff_isLocallyNoetherian_and_isUniversallyJapaneseScheme
    (X : Scheme.{u}) :
    IsNagataScheme X ↔
      (IsLocallyNoetherian X ∧
        IsUniversallyJapaneseScheme X)
Tag 033V, a lemma

Tag 033V in the Stacks Project.

isJapaneseScheme_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Nagata.lean, line 87. The attribute's comment: “equivalent conditions”.

Stacks Project, Tag 033V. For an integral scheme, Japanese-ness is equivalent to Japanese-ness of the section ring of every nonempty affine open, to the existence of an affine open cover with Japanese section rings, and to the existence of an open cover by Japanese schemes.

public theorem isJapaneseScheme_tfae (X : Scheme.{u}) [IsIntegral X] :
    List.TFAE [
      IsJapaneseScheme X,
      ∀ U : X.affineOpens, ∀ _hU : Nonempty U.1,
        letI : IsDomain Γ(X, U.1) := IsIntegral.component_integral U.1
        IsJapaneseRing Γ(X, U.1),
      ∃ (I : Type u) (U : I → X.affineOpens),
        TopologicalSpace.IsOpenCover (fun i ↦ (U i).1) ∧
          ∀ i, ∃ _hU : Nonempty (U i).1,
            letI : IsDomain Γ(X, (U i).1) := IsIntegral.component_integral (U i).1
            IsJapaneseRing Γ(X, (U i).1),
      ∃ (I : Type u) (U : I → X.Opens),
        TopologicalSpace.IsOpenCover U ∧
        ∀ i, ∃ hU : IsIntegral (U i).toScheme,
            @IsJapaneseScheme (U i).toScheme hU]

isJapaneseScheme_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Nagata.lean, line 155. The attribute's comment: “open subschemes”.

Stacks Project, Tag 033V. Every nonempty open subscheme of a Japanese integral scheme is Japanese.

public theorem isJapaneseScheme_open (X : Scheme.{u}) [IsIntegral X] (hX : IsJapaneseScheme X)
    (U : X.Opens) [Nonempty U] :
    ∃ hU : IsIntegral U.toScheme, @IsJapaneseScheme U.toScheme hU
Tag 033W, a lemma

Tag 033W in the Stacks Project.

isUniversallyJapaneseScheme_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NagataNormalization/LocalProperty.lean, line 241. The attribute's comment: “equivalent conditions”. References: SGA 4 IX (2.14.2).

Stacks Project, Tag 033W. For a scheme X, being universally Japanese is equivalent to the section ring of every affine open being universally Japanese, to this holding on some affine open covering, and to admitting an open covering by universally Japanese open subschemes.

theorem isUniversallyJapaneseScheme_tfae (X : Scheme.{u}) :
    List.TFAE [
      IsUniversallyJapaneseScheme X,
      ∀ U : X.affineOpens, IsUniversallyJapaneseRing Γ(X, (U : X.Opens)),
      ∃ (I : Type u) (U : I → X.affineOpens),
        IsOpenCover (fun i ↦ (U i : X.Opens)) ∧
          ∀ i, IsUniversallyJapaneseRing Γ(X, (U i : X.Opens)),
      ∃ (I : Type u) (U : I → X.Opens),
        IsOpenCover U ∧ ∀ i, IsUniversallyJapaneseScheme (U i).toScheme]

isUniversallyJapaneseScheme_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NagataNormalization/LocalProperty.lean, line 262. The attribute's comment: “open subschemes”.

Stacks Project, Tag 033W. Every open subscheme of a universally Japanese scheme is universally Japanese.

theorem isUniversallyJapaneseScheme_open {X : Scheme.{u}} (hX : IsUniversallyJapaneseScheme X)
    (U : X.Opens) : IsUniversallyJapaneseScheme U.toScheme
Tag 033X, a lemma

Tag 033X in the Stacks Project.

isNagataScheme_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NagataNormalization/LocalProperty.lean, line 209. The attribute's comment: “equivalent conditions”.

Stacks Project, Tag 033X. For a scheme X, being Nagata is equivalent to the section ring of every affine open being Nagata, to this holding on some affine open covering, and to admitting an open covering by Nagata open subschemes.

theorem isNagataScheme_tfae (X : Scheme.{u}) :
    List.TFAE [
      IsNagataScheme X,
      ∀ U : X.affineOpens, IsNagataRing Γ(X, (U : X.Opens)),
      ∃ (I : Type u) (U : I → X.affineOpens),
        IsOpenCover (fun i ↦ (U i : X.Opens)) ∧
          ∀ i, IsNagataRing Γ(X, (U i : X.Opens)),
      ∃ (I : Type u) (U : I → X.Opens),
        IsOpenCover U ∧ ∀ i, IsNagataScheme (U i).toScheme]

isNagataScheme_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NagataNormalization/LocalProperty.lean, line 228. The attribute's comment: “open subschemes”.

Stacks Project, Tag 033X. Every open subscheme of a Nagata scheme is Nagata.

theorem isNagataScheme_open {X : Scheme.{u}} (hX : IsNagataScheme X) (U : X.Opens) :
    IsNagataScheme U.toScheme
Tag 033Y, a lemma

Tag 033Y in the Stacks Project.

Declarations registered for the tag:

Tag 033Z, a lemma

Tag 033Z in the Stacks Project.

isNagataScheme_iff_isLocallyNoetherian_and_isUniversallyJapaneseScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Nagata.lean, line 169.

A scheme is Nagata if and only if it is locally Noetherian and universally Japanese.

public theorem isNagataScheme_iff_isLocallyNoetherian_and_isUniversallyJapaneseScheme
    (X : Scheme.{u}) :
    IsNagataScheme X ↔
      (IsLocallyNoetherian X ∧
        IsUniversallyJapaneseScheme X)
Sources
LeanIsUniversallyJapaneseScheme · IsJapaneseScheme · IsNagataScheme · isNagataScheme_iff_isLocallyNoetherian_and_isUniversallyJapaneseScheme · isJapaneseScheme_tfae · isJapaneseScheme_open · isUniversallyJapaneseScheme_tfae · isUniversallyJapaneseScheme_open

Section28.15 The singular locus#

Section 28.15 of the Stacks Project, Tag 07R0. 1 tag here is carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07R1, a definition

Tag 07R1 in the Stacks Project.

AlgebraicGeometry.regularLocus, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Regular.lean, line 94. The attribute's comment: “regular locus”. References: EGA IV (6.12.1), “Reg(X)”; EGA IV (7.3.12), “special case”.

The regular locus of a scheme: the points at which its local ring is regular.

public abbrev regularLocus (X : Scheme.{u}) : Set X

AlgebraicGeometry.singularLocus, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Regular.lean, line 100. The attribute's comment: “singular locus”. References: EGA IV (6.12.1), “Sing(X)”.

The singular locus of a scheme, the complement of its regular locus.

public abbrev singularLocus (X : Scheme.{u}) : Set X
Sources
LeanAlgebraicGeometry.regularLocus · AlgebraicGeometry.singularLocus

Section28.16 Local irreducibility#

Section 28.16 of the Stacks Project, Tag 0BQ1. 6 tags here are carried by 12 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0BQ2, a definition

Tag 0BQ2 in the Stacks Project.

AlgebraicGeometry.IsUnibranchAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Unibranch.lean, line 284. The attribute's comment: “unibranch at a point”. References: EGA IV (6.15.1).

A scheme is unibranch at a point if its local ring there is unibranch.

public abbrev IsUnibranchAt
    (X : AlgebraicGeometry.Scheme.{u}) (x : X) : Prop

AlgebraicGeometry.IsGeometricallyUnibranchAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Unibranch.lean, line 292. The attribute's comment: “geometrically unibranch at a point”. References: EGA IV (6.15.1), “geom. unibranch at x”.

A scheme is geometrically unibranch at a point if its local ring there is geometrically unibranch.

public abbrev IsGeometricallyUnibranchAt
    (X : AlgebraicGeometry.Scheme.{u}) (x : X) : Prop

AlgebraicGeometry.IsUnibranch, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Unibranch.lean, line 300. The attribute's comment: “unibranch schemes”. References: EGA III (4.3.6), “unibranch point”; EGA IV (6.15.1), “unibranch, global”.

A scheme is unibranch if it is unibranch at every point.

public abbrev IsUnibranch
    (X : AlgebraicGeometry.Scheme.{u}) : Prop

AlgebraicGeometry.IsGeometricallyUnibranch, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Unibranch.lean, line 307. The attribute's comment: “geometrically unibranch schemes”. References: EGA IV (6.15.1), “geom. unibranch, global”; SGA 3 X (5.14.0).

A scheme is geometrically unibranch if it is geometrically unibranch at every point.

public abbrev IsGeometricallyUnibranch
    (X : AlgebraicGeometry.Scheme.{u}) : Prop
Tag 0BQ3, a lemma

Tag 0BQ3 in the Stacks Project.

AlgebraicGeometry.isGeometricallyUnibranch_of_isNormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Unibranch.lean, line 572. References: EGA III (4.3.6), “normal ⇒ unibranch”; EGA IV (6.15.6), “k' = k”; SGA 4 IX (2.14.1); SGA 4 XVII (6.2.6), “more general”.

A normal scheme is geometrically unibranch.

public theorem isGeometricallyUnibranch_of_isNormal {X : Scheme.{u}}
    [IsNormal X] : IsGeometricallyUnibranch X
Tag 0BQ4, a lemma

Tag 0BQ4 in the Stacks Project.

AlgebraicGeometry.isGeometricallyUnibranch_iff_isConnected_puncturedSpectrum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/UnibranchPuncturedSpectrum.lean, line 415.

A locally Noetherian scheme is geometrically unibranch exactly when, at every point which is not the generic point of an irreducible component, the punctured spectrum of a strict henselization of the local ring is connected.

theorem isGeometricallyUnibranch_iff_isConnected_puncturedSpectrum
    (X : Scheme.{u}) [IsLocallyNoetherian X] :
    IsGeometricallyUnibranch X ↔
      ∀ x : X, x ∉ genericPoints X →
        ∀ (κsep : Type u) [Field κsep] [Algebra (ResidueField (X.presheaf.stalk x)) κsep]
          [IsSepClosure (ResidueField (X.presheaf.stalk x)) κsep]
          (Ash : Type u) [CommRing Ash] [IsLocalRing Ash]
          [Algebra (X.presheaf.stalk x) Ash]
          [IsHenselization (X.presheaf.stalk x) κsep Ash],
          IsConnected ({closedPoint Ash}ᶜ : Set (PrimeSpectrum Ash))
Tag 0C38, a definition

Tag 0C38 in the Stacks Project.

AlgebraicGeometry.numberOfBranches, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Unibranch.lean, line 314. The attribute's comment: “number of branches”.

The number of branches of a scheme at a point is the number of branches of its local ring at that point.

public noncomputable abbrev numberOfBranches (X : AlgebraicGeometry.Scheme.{u}) (x : X) : ℕ∞

AlgebraicGeometry.numberOfGeometricBranches, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Unibranch.lean, line 320. The attribute's comment: “number of geometric branches”.

The number of geometric branches of a scheme at a point is the number of geometric branches of its local ring at that point.

public noncomputable abbrev numberOfGeometricBranches
    (X : AlgebraicGeometry.Scheme.{u}) (x : X) : ℕ∞
Tag 0E20, a lemma

Tag 0E20 in the Stacks Project.

AlgebraicGeometry.numberOfGeometricBranches_eq_iSup_sum_components, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/PrincipalOpens/GeometricBranches.lean, line 1042. The attribute's comment: “geometric_branches_sum”.

The geometric branches at a point are the geometric branches of its reduced irreducible components through that point, counted with multiplicity one per component.

public theorem numberOfGeometricBranches_eq_iSup_sum_components
    (X : Scheme.{u}) (x : X) :
    numberOfGeometricBranches X x =
      ⨆ s : Finset {Z : Set X // Z ∈ irreducibleComponents X ∧ x ∈ Z},
        ∑ Z ∈ s,
        let C : Closeds X :=
          ⟨Z.1, isClosed_of_mem_irreducibleComponents Z.1 Z.property.1⟩
        let I := Scheme.IdealSheafData.vanishingIdeal C
        numberOfGeometricBranches I.subscheme
          (⟨x, by
            change x ∈ ((Scheme.IdealSheafData.vanishingIdeal C).support : Set X)
            have h := Scheme.IdealSheafData.coe_support_vanishingIdeal C
            exact h.symm ▸ (show x ∈ (C : Set X) from Z.property.2)⟩ : I.subscheme)

AlgebraicGeometry.numberOfBranches_eq_iSup_sum_components, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/PrincipalOpens/GeometricBranches.lean, line 1093. The attribute's comment: “branches_sum”.

The branches at a point are the branches of its reduced irreducible components through that point, counted with multiplicity one per component.

public theorem numberOfBranches_eq_iSup_sum_components
    (X : Scheme.{u}) (x : X) :
    numberOfBranches X x =
      ⨆ s : Finset {Z : Set X // Z ∈ irreducibleComponents X ∧ x ∈ Z},
        ∑ Z ∈ s,
        let C : Closeds X :=
          ⟨Z.1, isClosed_of_mem_irreducibleComponents Z.1 Z.property.1⟩
        let I := Scheme.IdealSheafData.vanishingIdeal C
        numberOfBranches I.subscheme
          (⟨x, by
            change x ∈ ((Scheme.IdealSheafData.vanishingIdeal C).support : Set X)
            have h := Scheme.IdealSheafData.coe_support_vanishingIdeal C
            exact h.symm ▸ (show x ∈ (C : Set X) from Z.property.2)⟩ : I.subscheme)
Tag 0C39, a lemma

Tag 0C39 in the Stacks Project.

AlgebraicGeometry.numberOfBranches_eq_one_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Unibranch.lean, line 511. The attribute's comment: “part (1)”.

A scheme has exactly one branch at a point if and only if it is unibranch at that point.

public theorem numberOfBranches_eq_one_iff (X : Scheme.{u}) (x : X) :
    numberOfBranches X x = 1 ↔ IsUnibranchAt X x

AlgebraicGeometry.numberOfGeometricBranches_eq_one_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/Unibranch.lean, line 518. The attribute's comment: “part (2)”.

A scheme has exactly one geometric branch at a point if and only if it is geometrically unibranch at that point.

public theorem numberOfGeometricBranches_eq_one_iff (X : Scheme.{u}) (x : X) :
    numberOfGeometricBranches X x = 1 ↔ IsGeometricallyUnibranchAt X x
Sources
LeanAlgebraicGeometry.IsUnibranchAt · AlgebraicGeometry.IsGeometricallyUnibranchAt · AlgebraicGeometry.IsUnibranch · AlgebraicGeometry.IsGeometricallyUnibranch · AlgebraicGeometry.isGeometricallyUnibranch_of_isNormal · AlgebraicGeometry.isGeometricallyUnibranch_iff_isConnected_puncturedSpectrum · AlgebraicGeometry.numberOfBranches · AlgebraicGeometry.numberOfGeometricBranches

Section28.17 Characterizing modules of finite type and finite presentation#

Section 28.17 of the Stacks Project, Tag 01PA. 2 tags here are carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01PB, a lemma

Tag 01PB in the Stacks Project.

AlgebraicGeometry.tilde_isFiniteType_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Modules/TildeFiniteness.lean, line 142. References: EGA II (1.4.5), “affine base, B = O_Y”.

An associated sheaf on Spec R is of finite type precisely when its module of global sections is finite over R.

theorem tilde_isFiniteType_iff {R : CommRingCat.{u}} (M : ModuleCat.{u} R) :
    (tilde M).IsFiniteType ↔ Module.Finite R M
Tag 01PC, a lemma

Tag 01PC in the Stacks Project.

AlgebraicGeometry.tilde_isFinitePresentation_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Modules/TildeFiniteness.lean, line 200.

The quasi-coherent sheaf on Spec R associated to an R-module M is of finite presentation if and only if M is a finitely presented module.

theorem tilde_isFinitePresentation_iff {R : CommRingCat.{u}} (M : ModuleCat.{u} R) :
    (tilde M).IsFinitePresentation ↔ Module.FinitePresentation R M
Sources
LeanAlgebraicGeometry.tilde_isFiniteType_iff · AlgebraicGeometry.tilde_isFinitePresentation_iff

Section28.18 Sections over principal opens#

Section 28.18 of the Stacks Project, Tag 0B5K. 5 tags here are carried by 11 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01P7, a lemma

Tag 01P7 in the Stacks Project.

AlgebraicGeometry.isLocalizedModule_restriction_basicOpen_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/PrincipalOpens/Sections.lean, line 77. The attribute's comment: “quasi-coherent modules”. References: EGA III (1.4.5), “H⁰, L = 𝒪_X, qcqs”.

On a quasi-compact, quasi-separated open, restriction of sections of a quasi-coherent module to a principal open is localization at the defining function.

theorem isLocalizedModule_restriction_basicOpen_of_qcqs {X : Scheme.{u}} (M : X.Modules)
    [M.IsQuasicoherent] {U : X.Opens} (hU : IsCompact U.1) (hU' : IsQuasiSeparated U.1)
    (f : Γ(X, U)) :
    letI : Module Γ(X, U) Γ(M, X.basicOpen f) :=
      Module.compHom Γ(M, X.basicOpen f)
        (X.presheaf.map (homOfLE (X.basicOpen_le f)).op).hom
    IsLocalizedModule.Away f
      (Scheme.Modules.restrictionLinearMap M (homOfLE (X.basicOpen_le f)))

Declarations registered for the tag:

Tag 0B5L, an equation

Tag 0B5L in the Stacks Project.

Stacks.SheafOfModules.sectionLocalizationMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/NonvanishingSections/LocalizationMap.lean, line 1079.

The canonical map from degree-zero localized twisted sections to sections on X_s. It restricts a numerator to X_s and divides by the corresponding power of s. The section is invertible there, so this construction is independent of the fraction representative.

public noncomputable def sectionLocalizationMap (s : L.sections) :
    sectionAtNonvanishingOpen X L F s →+
      F.val.obj (op (nonvanishingOpen L s))

Stacks.SheafOfModules.sectionLocalizationMap_fraction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/NonvanishingSections/LocalizationMap.lean, line 1092. The attribute's comment: “homogeneous fraction formula”.

A homogeneous fraction m/sⁿ maps to the section t exactly when, on X_s, the restricted numerator is the tensor product of t with sⁿ. The local invertibility of sⁿ makes this condition a characterization.

public theorem sectionLocalizationMap_fraction (s : L.sections) (n : ℕ)
    (m : ((((Stacks.SheafOfModules.Tensor.sheafTensor ⟨(sectionSiteRing X),
      Presheaf.isSheaf_of_isSheaf_comp _ ((sectionSiteRing X)) (forget₂ CommRingCat RingCat)
      ((sectionSiteSheaf X))⟩).obj (F)).obj ((TensorPower.tensorPower (sectionSiteRing X)
      (sectionSiteSheaf X) L
        (n : ℤ))))).val.obj (op (⊤_ (Opens X.toRingedSpace.toPresheafedSpace))))
    (z : sectionAtNonvanishingOpen X L F s)
    (t : F.val.obj (op (nonvanishingOpen L s)))
    (hz : (z : LocalizedModule.Away
      (R := sectionRing (sectionSiteRing X) (sectionSiteSheaf X) L)
      (homogeneousSection X L s)
      (sectionModule (sectionSiteRing X) (sectionSiteSheaf X) L F)) =
        LocalizedModule.mk (S := Submonoid.powers (homogeneousSection X L s))
          (DirectSum.of _ (n : ℤ) m)
          ⟨(homogeneousSection X L s) ^ n, by exact ⟨n, rfl⟩⟩)
    (hdiv :
      ((((Stacks.SheafOfModules.Tensor.sheafTensor ⟨(sectionSiteRing X),
        Presheaf.isSheaf_of_isSheaf_comp _ ((sectionSiteRing X)) (forget₂ CommRingCat RingCat)
        ((sectionSiteSheaf X))⟩).obj (F)).obj ((TensorPower.tensorPower (sectionSiteRing X)
        (sectionSiteSheaf X) L
          (n : ℤ))))).val.map (terminal.from _).op m =
      tensorSectionAtOpen X L F
        (nonvanishingOpen L s) n t
        ((TensorPower.tensorPower (sectionSiteRing X) (sectionSiteSheaf X) L
          (n : ℤ)).val.map (terminal.from _).op (sectionPower X L s n))) :
    sectionLocalizationMap X L F s z = t

Stacks.SheafOfModules.sectionLocalizationMap_smul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/NonvanishingSections/LocalizationMap.lean, line 1131. The attribute's comment: “localized-ring linearity”.

The restriction-and-division map is linear over the induced map from the degree-zero homogeneous localization of the section ring to functions on X_s.

public theorem sectionLocalizationMap_smul (s : L.sections) :
    let U := nonvanishingOpen L s
    letI : Module
        ((TensorSheafification.structureSheaf (sectionSiteRing X)
          (sectionSiteSheaf X)).obj.obj (op U))
        (F.val.obj (op U)) := (F.val.obj (op U)).isModule
    ∃ φ : HomogeneousLocalization.Away
        (sectionRingGrading (sectionSiteRing X) (sectionSiteSheaf X) L)
        (homogeneousSection X L s) →+*
          (TensorSheafification.structureSheaf (sectionSiteRing X)
            (sectionSiteSheaf X)).obj.obj (op U),
      ∀ (a : HomogeneousLocalization.Away
          (sectionRingGrading (sectionSiteRing X) (sectionSiteSheaf X) L)
          (homogeneousSection X L s)) (z : sectionAtNonvanishingOpen X L F s),
        sectionLocalizationMap X L F s (a • z) =
          φ a • sectionLocalizationMap X L F s z
Tag 01PW, a lemma

Tag 01PW in the Stacks Project.

Stacks.SheafOfModules.sectionLocalizationMap_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/PrincipalOpens/GradedSectionInjective.lean, line 442. The attribute's comment: “part (1)”. References: EGA I (9.3.1), “(i)”.

[Stacks, Tag 01PW] part (1). Let X be a quasi-compact scheme, let L be an invertible 𝒪_X-module, let s be a global section of L and let ℱ be a quasi-coherent 𝒪_X-module. The comparison map of Tag 0B5L (⨁_n Γ(X, ℱ ⊗ L^{⊗ n}))_{(s)} ⟶ Γ(X_s, ℱ|_{X_s}) is injective.

theorem sectionLocalizationMap_injective [CompactSpace X] [F.IsQuasicoherent] (s : L.sections) :
    Function.Injective (sectionLocalizationMap X L F s)

Stacks.SheafOfModules.sectionLocalizationMap_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/PrincipalOpens/GradedSectionInjective.lean, line 1196. The attribute's comment: “part (2)”.

[Stacks, Tag 01PW] part (2). Let X be a quasi-compact and quasi-separated scheme, let L be an invertible 𝒪_X-module, let s be a global section of L and let ℱ be a quasi-coherent 𝒪_X-module. The comparison map of Tag 0B5L (⨁_n Γ(X, ℱ ⊗ L^{⊗ n}))_{(s)} ⟶ Γ(X_s, ℱ|_{X_s}) is bijective.

Both chart-local steps of the source's proof are theorems here, so the statement asks only for the quasi-coherence of ℱ and the quasi-compactness and quasi-separatedness of X: Stacks.SheafOfModules.hasTwistedChartExtension is Tag 01P7 on an affine chart trivializing L, and Stacks.SheafOfModules.hasTwistedCompactAnnihilation is part (1) over a quasi-compact open.

theorem sectionLocalizationMap_bijective [CompactSpace X] [QuasiSeparatedSpace X]
    [F.IsQuasicoherent] (s : L.sections) :
    Function.Bijective (sectionLocalizationMap X L F s)
Tag 0B5M, an equation

Tag 0B5M in the Stacks Project.

Stacks.SheafOfModules.homAtNonvanishingOpen, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/NonvanishingGradedHom.lean, line 842. The attribute's comment: “graded Hom localization”.

The degree-zero localization of the actual graded Hom module.

public noncomputable def homAtNonvanishingOpen (s : L.sections)

Stacks.SheafOfModules.homLocalizationMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/NonvanishingGradedHom.lean, line 1178.

Restrict a degree-zero localized graded morphism to the open where s trivializes L, dividing its degree-n numerator by sⁿ.

public noncomputable def homLocalizationMap (s : L.sections) :
    homAtNonvanishingOpen X L F G s →+
      (F.over (nonvanishingOpen L s) ⟶
        G.over (nonvanishingOpen L s))

Stacks.SheafOfModules.homLocalizationMap_fraction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/NonvanishingGradedHom.lean, line 1221. The attribute's comment: “homogeneous fraction formula”.

A homogeneous morphism f : F ⟶ G ⊗ Lⁿ, divided by sⁿ, restricts to the unique morphism on X_s whose tensor product with sⁿ is the restriction of f.

public theorem homLocalizationMap_fraction (s : L.sections) (n : ℕ)
    (f : F ⟶ (((Stacks.SheafOfModules.Tensor.sheafTensor
        ⟨(sectionSiteRing X), Presheaf.isSheaf_of_isSheaf_comp _ ((sectionSiteRing X))
        (forget₂ CommRingCat RingCat) ((sectionSiteSheaf X))⟩).obj (G)).obj
        ((TensorPower.tensorPower (sectionSiteRing X)
        (sectionSiteSheaf X) L (n : ℤ)))))
    (t : (sheafHomSpace X.toRingedSpace F G).val.obj
        (op (nonvanishingOpen L s)))
    (hdiv :
      ((((Stacks.SheafOfModules.Tensor.sheafTensor ⟨(sectionSiteRing X),
          Presheaf.isSheaf_of_isSheaf_comp _ ((sectionSiteRing X)) (forget₂ CommRingCat RingCat)
          ((sectionSiteSheaf X))⟩).obj ((sheafHomSpace X.toRingedSpace F G))).obj
          ((TensorPower.tensorPower (sectionSiteRing X)
          (sectionSiteSheaf X) L (n : ℤ))))).val.map
            (terminal.from _).op
              (homToTwistedSection X L F G n f) =
      tensorSectionAtOpen X L
        (sheafHomSpace X.toRingedSpace F G)
        (nonvanishingOpen L s) n t
        ((TensorPower.tensorPower (sectionSiteRing X)
          (sectionSiteSheaf X) L (n : ℤ)).val.map
            (terminal.from _).op (sectionPower X L s n))) :
    homLocalizationMap X L F G s (homFractionClass X L F G s n f) = ⟨t⟩
Tag 01XQ, a lemma

Tag 01XQ in the Stacks Project.

Stacks.SheafOfModules.homLocalizationMap_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/PrincipalOpens/GradedHomBijective.lean, line 108. The attribute's comment: “bijective”.

[Stacks, Tag 01XQ] part (2). Let X be a quasi-compact and quasi-separated scheme, let L be an invertible 𝒪_X-module, let s be a global section of L, let ℱ be an 𝒪_X-module of finite presentation and let 𝒢 be a quasi-coherent 𝒪_X-module. The comparison map of Tag 0B5M (⨁_n Hom(ℱ, 𝒢 ⊗ L^{⊗ n}))_{(s)} ⟶ Hom_{𝒪_{X_s}}(ℱ|_{X_s}, 𝒢|_{X_s}) is bijective.

The quasi-coherence of ℱ that the source assumes throughout the lemma is not carried separately: finite presentation implies it, and implies the finite type that part (1) of the tag asks for.

theorem homLocalizationMap_bijective [CompactSpace X] [QuasiSeparatedSpace X]
    [F.IsFinitePresentation] [G.IsQuasicoherent] (s : L.sections) :
    Function.Bijective (homLocalizationMap X L F G s)

Stacks.SheafOfModules.homLocalizationMap_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/PrincipalOpens/GradedHomInjective.lean, line 243. The attribute's comment: “injective”.

[Stacks, Tag 01XQ] part (1). Let X be a quasi-compact scheme, let L be an invertible 𝒪_X-module, let s be a global section of L and let ℱ, 𝒢 be quasi-coherent 𝒪_X-modules with ℱ of finite type. The comparison map of Tag 0B5M (⨁_n Hom(ℱ, 𝒢 ⊗ L^{⊗ n}))_{(s)} ⟶ Hom_{𝒪_{X_s}}(ℱ|_{X_s}, 𝒢|_{X_s}) is injective.

theorem homLocalizationMap_injective (X : Scheme.{u}) [CompactSpace X]
    (L : SheafOfModules.{u} (structureSheafRing X.toRingedSpace))
    [IsInvertible X.toRingedSpace.presheaf
      (structureSheafRing X.toRingedSpace).property L]
    (F G : X.Modules) [F.IsQuasicoherent] [G.IsQuasicoherent] [F.IsFiniteType]
    (s : L.sections) :
    Function.Injective (homLocalizationMap X L F G s)
Sources
LeanAlgebraicGeometry.isLocalizedModule_restriction_basicOpen_of_qcqs · AlgebraicGeometry.isLocalization_basicOpen_of_qcqs · Stacks.SheafOfModules.sectionLocalizationMap · Stacks.SheafOfModules.sectionLocalizationMap_fraction · Stacks.SheafOfModules.sectionLocalizationMap_smul · Stacks.SheafOfModules.sectionLocalizationMap_injective · Stacks.SheafOfModules.sectionLocalizationMap_bijective · Stacks.SheafOfModules.homAtNonvanishingOpen

Section28.19 Quasi-affine schemes#

Section 28.19 of the Stacks Project, Tag 01P5. 5 tags here are carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0EHM, a lemma

Tag 0EHM in the Stacks Project.

AlgebraicGeometry.isIso_pullback_fromTildeΓ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/PrincipalOpens/QuasiCompactOpen.lean, line 47.

For a quasi-coherent module F on a quasi-compact open U of an affine scheme, the canonical map to F from the restriction to U of the sheaf associated to the global sections of F is an isomorphism.

theorem isIso_pullback_fromTildeΓ
    (R : CommRingCat.{u}) (U : (Spec R).Opens)
    (hU : IsCompact (U : Set (Spec R)))
    (F : U.toScheme.Modules) [F.IsQuasicoherent] :
    IsIso ((Scheme.Modules.pullback U.ι).map
      (Scheme.Modules.fromTildeΓ ((Scheme.Modules.pushforward U.ι).obj F)) ≫
      (Scheme.Modules.pullbackPushforwardAdjunction U.ι).counit.app F)
Tag 01P8, a lemma

Tag 01P8 in the Stacks Project.

AlgebraicGeometry.isIso_toSpecΓ_restrict_basicOpen, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/QuasiAffine.lean, line 86.

Stacks Project, Tag 01P8. If X is quasi-compact and quasi-separated and its basic open defined by f is affine, then the canonical morphism to Spec Γ(X, ᵊ_X) restricts to an isomorphism from that basic open onto the standard open defined by f.

lemma isIso_toSpecΓ_restrict_basicOpen (X : Scheme.{u}) [CompactSpace X]
    [QuasiSeparatedSpace X] (f : Γ(X, ⊤)) (hf : IsAffineOpen (X.basicOpen f)) :
    IsIso (X.toSpecΓ ∣_ PrimeSpectrum.basicOpen f)
Tag 01P9, a lemma

Tag 01P9 in the Stacks Project.

AlgebraicGeometry.Scheme.isQuasiAffine_iff_quasiCompact_and_isOpenImmersion_toSpecΓ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/QuasiAffineToSpecGamma.lean, line 31.

Stacks 01P9. A scheme X is quasi-affine if and only if the canonical morphism X ⟶ Spec Γ(X, ⊤) is a quasi-compact open immersion.

theorem isQuasiAffine_iff_quasiCompact_and_isOpenImmersion_toSpecΓ (X : Scheme.{u}) :
    X.IsQuasiAffine ↔ QuasiCompact X.toSpecΓ ∧ IsOpenImmersion X.toSpecΓ
Tag 0ARY, a lemma

Tag 0ARY in the Stacks Project.

AlgebraicGeometry.isPullback_id_toSpecΓ_of_isOpenImmersion, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/QuasiAffine.lean, line 132.

Stacks Project, Tag 0ARY. For an open immersion U ⟶ V between quasi-affine schemes, the canonical morphism from U to the spectrum of its global sections is the base change of the induced morphism on spectra along the canonical morphism from V.

lemma isPullback_id_toSpecΓ_of_isOpenImmersion (U V : Scheme.{u}) (f : U ⟶ V)
    [IsOpenImmersion f]
    [U.IsQuasiAffine] [V.IsQuasiAffine] :
    IsPullback (𝟙 U) U.toSpecΓ (f ≫ V.toSpecΓ) (Spec.map f.appTop)
Tag 0F82, a lemma

Tag 0F82 in the Stacks Project.

AlgebraicGeometry.exists_affine_pullback_iso_affineSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/QuasiAffineAffineSpaceBundle.lean, line 391.

Stacks Project, Tag 0F82. A quasi-affine scheme X admits an integer n, an affine scheme T and a morphism T ⟶ X such that for every morphism X' ⟶ X with X' affine the fibre product X' ×_X T is isomorphic to affine n-space over X', as a scheme over X'.

theorem exists_affine_pullback_iso_affineSpace (X : Scheme.{u}) [X.IsQuasiAffine] :
    ∃ (n : ℕ) (T : Scheme.{u}), IsAffine T ∧
      ∃ f : T ⟶ X, ∀ (X' : Scheme.{u}) (_ : IsAffine X') (g : X' ⟶ X),
        Nonempty (Over.mk (pullback.fst g f) ≅
          Over.mk (AffineSpace.over (ULift.{u} (Fin n)) X').hom)

AlgebraicGeometry.exists_contains_affine_pullback_iso_affineSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiAffineAffineSpaceBundleInSite.lean, line 82. The attribute's comment: “the bundle chosen inside a big fppf site”.

For a quasi-affine scheme X satisfying the size cutoff of a big fppf site B, the affine-space bundle of Stacks 0F82 over X can be chosen with its total space satisfying the cutoff too, and its structure morphism is locally of finite type.

theorem exists_contains_affine_pullback_iso_affineSpace (B : BigFppfSite.{u})
    (X : Scheme.{u}) [X.IsQuasiAffine] (hX : B.Contains X) :
    ∃ (n : ℕ) (T : Scheme.{u}), IsAffine T ∧ B.Contains T ∧
      ∃ f : T ⟶ X, LocallyOfFiniteType f ∧
        ∀ (X' : Scheme.{u}) (_ : IsAffine X') (g : X' ⟶ X),
          Nonempty (Over.mk (pullback.fst g f) ≅
            Over.mk (AffineSpace.over (ULift.{u} (Fin n)) X').hom)
Sources
LeanAlgebraicGeometry.isIso_pullback_fromTildeΓ · AlgebraicGeometry.isIso_toSpecΓ_restrict_basicOpen · AlgebraicGeometry.Scheme.isQuasiAffine_iff_quasiCompact_and_isOpenImmersion_toSpecΓ · AlgebraicGeometry.isPullback_id_toSpecΓ_of_isOpenImmersion · AlgebraicGeometry.exists_affine_pullback_iso_affineSpace · AlgebraicGeometry.exists_contains_affine_pullback_iso_affineSpace

Section28.20 Flat modules#

Section 28.20 of the Stacks Project, Tag 05NZ. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05P0, a lemma

Tag 05P0 in the Stacks Project.

AlgebraicGeometry.isFlat_tilde_iff_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Modules/TildeFlat.lean, line 99. References: EGA III (1.4.15.5), “case A = B, φ = id”; EGA IV (2.1.2), “A = B, φ = id”.

Stacks Project, Tag 05P0. The sheaf associated to a module on an affine scheme is flat if and only if the module is flat.

theorem isFlat_tilde_iff_flat {R : CommRingCat.{u}} (M : ModuleCat.{u} R) :
    AlgebraicGeometry.SheafOfModules.IsFlat (tilde M) ↔ Module.Flat R M
Sources
LeanAlgebraicGeometry.isFlat_tilde_iff_flat

Section28.21 Locally free modules#

Section 28.21 of the Stacks Project, Tag 05P1. 3 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05JM, a lemma

Tag 05JM in the Stacks Project.

Stacks.Modules.tilde_isLocallyFree_iff_module, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/QuasiCoherent/LocallyFreeSite.lean, line 243. The attribute's comment: “locally free”.

The sheaf M̃ associated to an R-module M is a locally free 𝒪_X-module on X = Spec R, in the sense of Stacks Tag 01C6, if and only if M is a locally free R-module.

theorem tilde_isLocallyFree_iff_module :
    SheafOfModules.IsLocallyFree.{u, u, u}
        (tilde (R := CommRingCat.of R) (ModuleCat.of R M)) ↔ Module.IsLocallyFree R M

Stacks.Modules.tilde_isFiniteLocallyFree_iff_module, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/QuasiCoherent/LocallyFreeSite.lean, line 252. The attribute's comment: “finite locally free”.

The sheaf M̃ associated to an R-module M is a finite locally free 𝒪_X-module on X = Spec R, in the sense of Stacks Tag 01C6, if and only if M is a finite locally free R-module.

theorem tilde_isFiniteLocallyFree_iff_module :
    AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u}
        (tilde (R := CommRingCat.of R) (ModuleCat.of R M)) ↔ Module.IsFiniteLocallyFree R M

Stacks.Modules.tilde_isFiniteLocallyFreeOfRank_iff_module, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/QuasiCoherent/LocallyFreeSite.lean, line 262. The attribute's comment: “finite locally free of rank r”.

The sheaf M̃ associated to an R-module M is a finite locally free 𝒪_X-module of rank r on X = Spec R, in the sense of Stacks Tag 01C6, if and only if M is a finite locally free R-module of rank r.

theorem tilde_isFiniteLocallyFreeOfRank_iff_module (r : ℕ) :
    AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
        (tilde (R := CommRingCat.of R) (ModuleCat.of R M)) r ↔
      Module.IsFiniteLocallyFreeOfRank R M r

tilde_isLocallyFree_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/LocallyFree/SheafBridge.lean, line 1645.

Statement 1 (locally free case). M~ is a locally free O_X-module if and only if M is a locally free R-module.

PROOF (complete modulo the two helper lemmas): rewrite the sheaf side via isLocallyFree_iff_basicOpen, then: * (⇒) For each point x choose (by choose) a standard open D(g x) ∋ x on which the sheaf is free; the family (g x) covers Spec R (each x ∈ D(g x)), so Ideal.span (range g) = ⊤ by iSup_basicOpen_eq_top_iff, and by Helper 1 each M_{g x} is free — giving Module.IsLocallyFree R M with ι := PrimeSpectrum R. * (⇐) Given a covering family f : ι → R with span ⊤ and each M_{f i} free: for any x, the cover gives i with x ∈ D(f i), and Helper 1 makes the sheaf free on D(f i).

theorem tilde_isLocallyFree_iff (R : Type u) [CommRing R] (M : Type u)
    [AddCommGroup M] [Module R M] :
    (AlgebraicGeometry.tilde (R := CommRingCat.of R) (ModuleCat.of R M)).IsLocallyFree ↔
      Module.IsLocallyFree R M

tilde_isFiniteLocallyFree_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/LocallyFree/SheafBridge.lean, line 1671. References: EGA III (7.9.1), “M proj f.t. <=> M~ l.f.”.

Statement 2 (finite locally free case). M~ is a finite locally free O_X-module if and only if M is a finite locally free R-module.

PROOF (complete modulo isFiniteLocallyFree_iff_basicOpen and tilde_restrict_basicOpen_finiteFree_iff): same covering combinatorics as Statement 1, now carrying the finiteness witness Finite I through the helpers.

theorem tilde_isFiniteLocallyFree_iff (R : Type u) [CommRing R] (M : Type u)
    [AddCommGroup M] [Module R M] :
    (AlgebraicGeometry.tilde (R := CommRingCat.of R) (ModuleCat.of R M)).IsFiniteLocallyFree ↔
      Module.IsFiniteLocallyFree R M
Tag 05P2, a lemma

Tag 05P2 in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.flat_finitePresentation_locallyFree_fiberRank_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiberRank/LocallyFree.lean, line 303. References: EGA III (7.3.4); EGA 0 (5.4.1), “partial, special case”; EGA IV (19.7.4), “more general”; EGA IV (2.1.12), “special case”.

For a sheaf of modules F on a scheme X the following are equivalent: F is flat and of finite presentation; F is of finite presentation and all its stalks are free; F is locally free and of finite type; F is finite locally free; F is of finite type, all its stalks are free, and its fibre rank is locally constant.

Quasi-coherence is not assumed: it is implied by each of the five conditions.

theorem flat_finitePresentation_locallyFree_fiberRank_tfae {X : Scheme.{u}} (F : X.Modules) :
    List.TFAE [
      AlgebraicGeometry.SheafOfModules.IsFlat
          (C := TopologicalSpace.Opens X.toTopCat)
          (J := Opens.grothendieckTopology X.toTopCat) (O := X.sheaf) F ∧
        F.IsFinitePresentation,
      F.IsFinitePresentation ∧
        (∀ x : X,
          letI : Module (X.presheaf.stalk x) (F.presheaf.stalk x) :=
            PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
              (R := X.presheaf) F.val x
          Module.Free (X.presheaf.stalk x) (F.presheaf.stalk x)),
      _root_.SheafOfModules.IsLocallyFree.{u, u, u} F ∧
        _root_.SheafOfModules.IsFiniteType.{u, u, u} F,
      AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) F,
      _root_.SheafOfModules.IsFiniteType.{u, u, u} F ∧
        (∀ x : X,
          letI : Module (X.presheaf.stalk x) (F.presheaf.stalk x) :=
            PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
              (R := X.presheaf) F.val x
          Module.Free (X.presheaf.stalk x) (F.presheaf.stalk x)) ∧
        IsLocallyConstant (fiberRank F)]

Stacks.FiniteLocallyFree.ModuleTFAE.finiteLocallyFree_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Modules/FiniteLocallyFreeTFAE.lean, line 882. References: EGA III (7.3.4).

A quasi-coherent sheaf of modules on a scheme is finite locally free exactly when it satisfies any of the five equivalent flatness, presentation, stalk, or rank conditions.

AlgebraicGeometry.Scheme.Modules.flat_finitePresentation_locallyFree_fiberRank_tfae in StacksFrontier.AlgebraicGeometry.FiberRank.LocallyFree carries the tag too, and states the same list of five conditions without assuming quasi-coherence, so it implies this statement outright. Both carry the tag: a Stacks tag is registered once per clause or part of its statement, and more than one carrier is expected rather than a defect.

theorem finiteLocallyFree_tfae {X : Scheme.{u}} (F : X.Modules)
    [F.IsQuasicoherent] :
    List.TFAE [
      AlgebraicGeometry.SheafOfModules.IsFlat F ∧ F.IsFinitePresentation,
      F.IsFinitePresentation ∧
        (∀ x : X,
          letI : Module (X.presheaf.stalk x) (F.presheaf.stalk x) :=
            PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
              (R := X.presheaf) F.val x
          Module.Free (X.presheaf.stalk x) (F.presheaf.stalk x)),
      SheafOfModules.IsLocallyFree F ∧ F.IsFiniteType,
      AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree F,
      F.IsFiniteType ∧
        (∀ x : X,
          letI : Module (X.presheaf.stalk x) (F.presheaf.stalk x) :=
            PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
              (R := X.presheaf) F.val x
          Module.Free (X.presheaf.stalk x) (F.presheaf.stalk x)) ∧
        IsLocallyConstant (fiberRank F)]
Tag 0FWH, a lemma

Tag 0FWH in the Stacks Project.

Stacks.FiniteLocallyFree.Reduced.isFiniteLocallyFree_iff_isFiniteType_and_isLocallyConstant_fiberRank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Modules/ReducedFiniteLocallyFree.lean, line 416.

On a reduced scheme, a quasi-coherent sheaf is finite locally free exactly when it is of finite type and has locally constant fibre rank.

theorem isFiniteLocallyFree_iff_isFiniteType_and_isLocallyConstant_fiberRank
    {X : Scheme.{u}} [IsReduced X] (F : X.Modules) [F.IsQuasicoherent] :
    AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree F ↔
      (F.IsFiniteType ∧ IsLocallyConstant (fiberRank F))
Sources
LeanStacks.Modules.tilde_isLocallyFree_iff_module · Stacks.Modules.tilde_isFiniteLocallyFree_iff_module · Stacks.Modules.tilde_isFiniteLocallyFreeOfRank_iff_module · tilde_isLocallyFree_iff · tilde_isFiniteLocallyFree_iff · AlgebraicGeometry.Scheme.Modules.flat_finitePresentation_locallyFree_fiberRank_tfae · Stacks.FiniteLocallyFree.ModuleTFAE.finiteLocallyFree_tfae · Stacks.FiniteLocallyFree.Reduced.isFiniteLocallyFree_iff_isFiniteType_and_isLocallyConstant_fiberRank

Section28.22 Locally projective modules#

Section 28.22 of the Stacks Project, Tag 05JN. 3 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05JP, a definition

Tag 05JP in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.IsLocallyProjective, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/LocallyProjective.lean, line 45.

A sheaf of modules on a scheme is locally projective if its sections on every affine open are projective over the ring of functions on that open.

public abbrev IsLocallyProjective {X : Scheme.{u}}
    (M : SheafOfModules.{m} X.ringCatSheaf) : Prop
Tag 05JQ, a lemma

Tag 05JQ in the Stacks Project.

AlgebraicGeometry.isLocallyProjective_iff_exists_affineOpen_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/AmpleAndExtension/LocallyProjectiveCover.lean, line 162. The attribute's comment: “affine open cover characterization”. References: SGA 3 VIB (11.9.1), “(i) <=> (ii)”.

Stacks Project, Tag 05JQ. A quasi-coherent sheaf of modules is locally projective if and only if its sections are projective on every member of some affine open cover.

theorem isLocallyProjective_iff_exists_affineOpen_cover {X : Scheme.{u}} (M : X.Modules)
    [M.IsQuasicoherent] :
    Scheme.Modules.IsLocallyProjective M ↔
      ∃ (ι : Type u) (U : ι → X.Opens),
        IsOpenCover U ∧
          (∀ i, IsAffineOpen (U i)) ∧
          ∀ i, Module.Projective Γ(X, U i) Γ(M, U i)

AlgebraicGeometry.isLocallyProjective_tilde_iff_projective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/AmpleAndExtension/LocallyProjectiveCover.lean, line 192. The attribute's comment: “affine specialization”. References: SGA 3 VIB (11.9.1), “affine case”.

Stacks Project, Tag 05JQ. The sheaf associated to a module on an affine scheme is locally projective if and only if the original module is projective.

theorem isLocallyProjective_tilde_iff_projective (R : CommRingCat.{u})
    (M : ModuleCat.{u} R) :
    Scheme.Modules.IsLocallyProjective (tilde M) ↔ Module.Projective R M
Tag 060M, a lemma

Tag 060M in the Stacks Project.

AlgebraicGeometry.pullback_isLocallyProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/LocallyProjectivePullback.lean, line 65.

Stacks Project, Tag 060M. The pullback of a locally projective quasi-coherent module along a morphism of schemes is locally projective.

theorem pullback_isLocallyProjective {X Y : Scheme.{u}} (f : X ⟶ Y) (G : Y.Modules)
    [G.IsQuasicoherent] (hG : Scheme.Modules.IsLocallyProjective G) :
    Scheme.Modules.IsLocallyProjective ((Scheme.Modules.pullback f).obj G)
Sources
LeanAlgebraicGeometry.Scheme.Modules.IsLocallyProjective · AlgebraicGeometry.isLocallyProjective_iff_exists_affineOpen_cover · AlgebraicGeometry.isLocallyProjective_tilde_iff_projective · AlgebraicGeometry.pullback_isLocallyProjective

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.