29.2 Closed immersions to 29.22 Morphisms of finite…

Section29.2 Closed immersions#

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

Tag 01QO, a lemma

Tag 01QO in the Stacks Project.

Stacks.AlgebraicGeometry.ClosedImmersionTFAE.closedImmersion_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedImmersionTFAE/Basic.lean, line 163. References: EGA I (4.2.2), “(b) closed case”.

The six equivalent descriptions of a closed immersion of schemes.

theorem closedImmersion_tfae {Z X : Scheme.{u}} (i : Z ⟶ X) :
    List.TFAE [
      IsClosedImmersion i,
      ∀ (U : X.Opens) (hU : IsAffineOpen U), IsQuotientOverAffineOpen i U hU,
      ∃ (𝒰 : Scheme.AffineOpenCover.{u} X), ∀ j : 𝒰.I₀,
        IsQuotientOverAffineOpen i (𝒰.f j).opensRange
          (isAffineOpen_opensRange (𝒰.f j)),
      Topology.IsClosedEmbedding i.base ∧
        Epi (SheafOfModules.unitToPushforwardObjUnit (structureSheafHom i.toLRSHom.toShHom)),
      (Topology.IsClosedEmbedding i.base ∧
        Epi (SheafOfModules.unitToPushforwardObjUnit (structureSheafHom i.toLRSHom.toShHom))) ∧
        (Stacks.ClosedImmersion.idealSheaf i.toLRSHom.toShHom).IsQuasicoherent,
      Stacks.ClosedImmersion.IsClosedImmersion i.toLRSHom.toShHom]
Tag 01QP, a lemma

Tag 01QP in the Stacks Project.

Declarations registered for the tag:

Tag 01QQ, a lemma

Tag 01QQ in the Stacks Project.

Stacks.Divisors.exists_isClosedImmersion_ker_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/QuasicoherentIdealSheafData/Basic.lean, line 165. The attribute's comment: “(2) implies (3), with the equality Ker(i^♯) = J recorded over affine opens only”.

Stacks Project, Tag 01QQ, the implication (2) ⇒ (3). A quasi-coherent sheaf of ideals J ⊆ 𝒪_X on a scheme is the sheaf of ideals of a closed immersion of schemes: the closed subscheme cut out by Stacks.Divisors.idealSheafDataOfSubmodule has, on every affine open, kernel exactly J.

The two remaining implications are proved in StacksFrontier/AlgebraicGeometry/Divisors/QuasicoherentIdealSheafData/Equivalence.lean, where Stacks.Divisors.isQuasicoherent_ideal_tfae assembles the whole tag: (1) ⇔ (2) is Stacks.ClosedImmersion.isQuasicoherent_iff_localGenerators, the sheaf-of-ideals half of Stacks Tag 01IN, and (3) ⇒ (2) is Stacks.Divisors.isQuasicoherent_of_ker_app_eq. Note that the latter is not just quasi-coherence of the kernel of a closed immersion, the other half of Tag 01IN: that statement is about the categorical kernel of 𝒪_X ⟶ i_* 𝒪_Z, and the step it leaves open is the identification of a submodule J whose sections agree with the kernel's with that kernel.

The equality of ideals below is recorded over affine opens only; Stacks.Divisors.subschemeι_app_eq_zero_iff_mem_of_isQuasicoherent upgrades it to every open, which is what the statement Ker(i^♯) = 𝓘 of the tag asks for.

theorem exists_isClosedImmersion_ker_eq :
    ∃ (Z : Scheme.{u}) (i : Z ⟶ X), IsClosedImmersion i ∧
      ∀ U : X.affineOpens, RingHom.ker (i.app U.1).hom = J.obj (op U.1)

Stacks.Divisors.isQuasicoherent_ideal_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/QuasicoherentIdealSheafData/Equivalence.lean, line 124. The attribute's comment: “the full equivalence: (1) locally generated by sections, (2) quasi-coherent, (3) the kernel of a closed immersion of schemes”.

For a sheaf of ideals J ⊆ 𝒪_X on a scheme the following are equivalent: J is locally generated by sections as a sheaf of 𝒪_X-modules; J is quasi-coherent; and there is a closed immersion of schemes i : Z ⟶ X whose ideal sheaf Ker(i^♯) is J, in the sense that over every open the kernel of i.app is the ideal that J cuts out there.

theorem isQuasicoherent_ideal_tfae (J : (SheafOfModules.unit X.ringCatSheaf).Submodule) :
    List.TFAE [
      Nonempty (SheafOfModules.LocalGeneratorsData.{u} J.toSheafOfModules),
      (J.toSheafOfModules : X.Modules).IsQuasicoherent,
      ∃ (Z : Scheme.{u}) (i : Z ⟶ X), IsClosedImmersion i ∧
        ∀ V : X.Opens, RingHom.ker (i.app V).hom = J.obj (op V)]
Tag 01QR, a lemma

Tag 01QR in the Stacks Project.

Declarations registered for the tag:

  • AlgebraicGeometry.IsClosedImmersion.isStableUnderBaseChange registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch29.lean, line 212 (StacksFrontier): “closed immersions are stable under base change”. References: EGA I (10.14.5), “(ii), ordinary schemes”; EGA I (4.3.1), “special case”; EGA I (4.3.2); EGA I (4.5.5), “(iii), special case”; EGA II (8.10.2), “j′ is a closed immersion”; EGA IV (17.13.1), “closed immersions”; EGA IV (2.7.1), “implication”; EGA IV (8.6.2), “more general”; SGA 1 VIII (5.5), “closed-immersion clause”; SGA 3 VIB (10.1), “partial”; SGA 4 XII (4.3), “Parenthetical clause”.
Tag 01QS, a lemma

Tag 01QS in the Stacks Project.

Declarations registered for the tag:

Tag 01QT, a lemma

Tag 01QT in the Stacks Project.

Declarations registered for the tag:

Tag 01QU, a lemma

Tag 01QU in the Stacks Project.

AlgebraicGeometry.IsClosedImmersion.isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/ClosedImmersionSeparated.lean, line 33.

A closed immersion of schemes is separated.

theorem IsClosedImmersion.isSeparated {X Y : Scheme.{u}} (f : X ⟶ Y) [IsClosedImmersion f] :
    IsSeparated f
Sources
LeanStacks.AlgebraicGeometry.ClosedImmersionTFAE.closedImmersion_tfae · AlgebraicGeometry.IsClosedImmersion.lift · AlgebraicGeometry.IsClosedImmersion.lift_fac · AlgebraicGeometry.Scheme.Hom.le_ker_comp · AlgebraicGeometry.IsClosedImmersion.of_comp_isClosedImmersion · AlgebraicGeometry.IsClosedImmersion.isIso_lift · AlgebraicGeometry.IsClosedImmersion.isIso_of_ker_eq · AlgebraicGeometry.Scheme.Hom.ker_comp_of_isIso

Section29.3 Immersions#

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

Tag 07RK, a lemma

Tag 07RK in the Stacks Project.

Declarations registered for the tag:

  • AlgebraicGeometry.IsImmersion.of_comp registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch29.lean, line 324 (StacksFrontier): “(1); also the immersion part of (2)”. References: EGA I (5.3.13); EGA I (5.3.14), “more general”; EGA I (5.5.12), “special case”; EGA IV (8.12.2), “more general”; EGA IV (16.2.3), “more general”; SGA 6 VIII (1.3), “(iv)”; SGA 6 VIII (1.8), “partial”.
  • AlgebraicGeometry.QuasiCompact.of_comp registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch29.lean, line 325 (StacksFrontier): “(2), quasi-compactness of Z → Y when Y → X is quasi-separated”. References: EGA I (5.5.12), “(i), special case”; EGA I (6.3.4), “(v)”; EGA I (6.6.4), “more general”; EGA II (8.14.6), “more general”; EGA IV (1.1.2), “more general”; EGA IV (1.2.4); EGA IV (1.5.4), “(v)”; EGA IV (18.12.13), “more general”; SGA 3 VIB (11.1), “partial”; SGA 3 VIB (12.9), “Quasi-compactness of ρ”; SGA 4 VI (1.9.1), “(iv), special case”.
  • AlgebraicGeometry.IsClosedImmersion.of_comp registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch29.lean, line 327 (StacksFrontier): “(3)”. References: EGA I (5.4.4); EGA I (5.4.6), “more general”; EGA I (5.5.12), “(i), special case”; EGA IV (17.9.3), “partial”; SGA 1 II (4.17), “more general”; SGA 3 VIB (5.6.3), “(i) ⇒ (ii)”; SGA 3 VIB (11.18.1), “more general”.
Tag 01QV, a lemma

Tag 01QV in the Stacks Project.

Declarations registered for the tag:

Tag 03DQ, a lemma

Tag 03DQ in the Stacks Project.

AlgebraicGeometry.exists_openImmersion_closedImmersion_factorization_of_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/ImmersionsAndAffine/Immersions.lean, line 48. References: EGA I (5.2.3), “factorization only”.

An immersion of a reduced scheme factors as an open immersion followed by a closed immersion.

theorem exists_openImmersion_closedImmersion_factorization_of_isReduced
    {Z X : Scheme.{u}} (f : Z ⟶ X) [IsImmersion f] [IsReduced Z] :
    ∃ (Y : Scheme.{u}) (j : Z ⟶ Y) (i : Y ⟶ X),
      IsOpenImmersion j ∧ IsClosedImmersion i ∧ j ≫ i = f
Tag 01QW, an example

Tag 01QW in the Stacks Project.

Stacks.Immersion.NotOpenThenClosed.chartIdeal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Immersion/NotOpenThenClosed.lean, line 94. The attribute's comment: “chart ideals”.

The ideal cutting out the closed subscheme on the n-th standard chart: it is generated by the n-th variable minus one, the (n + 1)-st powers of the earlier variables, and all later variables.

public def chartIdeal (k : Type u) [Field k] (n : ℕ) : Ideal (polynomialRing k)

Stacks.Immersion.NotOpenThenClosed.puncturedSpectrum, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Immersion/NotOpenThenClosed.lean, line 128. The attribute's comment: “union of standard opens”.

The union of the standard opens: the complement of the point at which every variable vanishes.

public abbrev puncturedSpectrum (k : Type u) [Field k] :
    (ambientSpectrum k).Opens

Stacks.Immersion.NotOpenThenClosed.nonextendableIdealSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Immersion/NotOpenThenClosed.lean, line 507. The attribute's comment: “glued quasi-coherent ideal sheaf”.

The ideal sheaf glued from the specified ideals on the standard-open cover.

public noncomputable def nonextendableIdealSheaf (k : Type u) [Field k] :
    { J : (puncturedSpectrum k).toScheme.IdealSheafData //
      ∀ n : ℕ,
        IsClosedImmersion
          (pullback.snd (J.subschemeι ≫ (puncturedSpectrum k).ι)
            (coordinateOpen k n).ι) ∧
        (pullback.snd (J.subschemeι ≫ (puncturedSpectrum k).ι)
          (coordinateOpen k n).ι).ker =
          ((Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (chartIdeal k n)))).ker).comap
            (coordinateOpen k n).ι }

Stacks.Immersion.NotOpenThenClosed.counterexampleImmersion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Immersion/NotOpenThenClosed.lean, line 524. The attribute's comment: “associated morphism”.

The immersion of the closed subscheme of the punctured spectrum into the ambient affine scheme.

public noncomputable def counterexampleImmersion (k : Type u) [Field k] :
    (nonextendableIdealSheaf k).1.subscheme ⟶ ambientSpectrum k

Stacks.Immersion.NotOpenThenClosed.chartIdeal_overlap_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Immersion/NotOpenThenClosed.lean, line 530. The attribute's comment: “unit ideal on distinct chart overlaps”.

Away from two distinct variables, the indicated chart ideal is the unit ideal.

public theorem chartIdeal_overlap_top (k : Type u) [Field k] (n m : ℕ) (hnm : n ≠ m) :
    (chartIdeal k n).map
      (algebraMap (polynomialRing k)
        (Localization.Away ((MvPolynomial.X n : polynomialRing k) *
          MvPolynomial.X m))) = ⊤

Stacks.Immersion.NotOpenThenClosed.iInf_chartIdeal_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Immersion/NotOpenThenClosed.lean, line 594. The attribute's comment: “intersection of chart ideals”.

The chart ideals have zero intersection in the original polynomial ring.

public theorem iInf_chartIdeal_eq_bot (k : Type u) [Field k] :
    (⨅ n : ℕ, chartIdeal k n) = ⊥

Stacks.Immersion.NotOpenThenClosed.counterexampleImmersion_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Immersion/NotOpenThenClosed.lean, line 623. The attribute's comment: “immersion”.

The closed subscheme of the punctured spectrum is an immersion in the ambient spectrum.

public theorem counterexampleImmersion_isImmersion (k : Type u) [Field k] :
    IsImmersion (counterexampleImmersion k)

Stacks.Immersion.NotOpenThenClosed.counterexampleImmersion_no_open_closed_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Immersion/NotOpenThenClosed.lean, line 721. The attribute's comment: “failure of open-then-closed factorization”.

This immersion cannot factor as an open immersion followed by a closed immersion.

public theorem counterexampleImmersion_no_open_closed_factorization
    (k : Type u) [Field k] :
    ¬ ∃ (T : Scheme.{u})
        (g : (nonextendableIdealSheaf k).1.subscheme ⟶ T)
        (h : T ⟶ ambientSpectrum k),
        IsOpenImmersion g ∧ IsClosedImmersion h ∧
          g ≫ h = counterexampleImmersion k
Tag 0FCZ, a lemma

Tag 0FCZ in the Stacks Project.

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.IsImmersion.of_comp · AlgebraicGeometry.QuasiCompact.of_comp · AlgebraicGeometry.IsClosedImmersion.of_comp · AlgebraicGeometry.IsImmersion.isImmersion_iff_exists_of_quasiCompact · AlgebraicGeometry.exists_openImmersion_closedImmersion_factorization_of_isReduced · Stacks.Immersion.NotOpenThenClosed.chartIdeal · Stacks.Immersion.NotOpenThenClosed.puncturedSpectrum · Stacks.Immersion.NotOpenThenClosed.nonextendableIdealSheaf

Section29.4 Closed immersions and quasi-coherent sheaves#

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

Tag 01QY, a lemma

Tag 01QY in the Stacks Project.

Stacks.ClosedImmersion.pushforwardQcoh_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedPushforward/Quasicoherent.lean, line 102. The attribute's comment: “exactness”. References: EGA I (1.6.4), “closed immersion”.

[Stacks, Tag 01QY], exactness. Direct image along a closed immersion is an exact functor on quasi-coherent modules.

theorem pushforwardQcoh_exact :
    exactFunctor (SheafOfModules.isQuasicoherent Z.ringCatSheaf).FullSubcategory
      (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory
      (Stacks.Modules.pushforwardQcoh i)

Stacks.ClosedImmersion.fullyFaithfulPushforwardQcoh, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedPushforward/Quasicoherent.lean, line 112. The attribute's comment: “full faithfulness”.

[Stacks, Tag 01QY], full faithfulness. Direct image along a closed immersion is fully faithful on quasi-coherent modules: it is fully faithful on all modules, and the inclusion of the quasi-coherent modules is faithful.

def fullyFaithfulPushforwardQcoh : (Stacks.Modules.pushforwardQcoh i).FullyFaithful

Stacks.ClosedImmersion.pushforwardQcoh_full, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedPushforward/Quasicoherent.lean, line 123. The attribute's comment: “fullness”.

[Stacks, Tag 01QY], fullness. Direct image along a closed immersion is full on quasi-coherent modules.

instance pushforwardQcoh_full : (Stacks.Modules.pushforwardQcoh i).Full

Stacks.ClosedImmersion.pushforwardQcoh_faithful, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedPushforward/Quasicoherent.lean, line 129. The attribute's comment: “faithfulness”.

[Stacks, Tag 01QY], faithfulness. Direct image along a closed immersion is faithful on quasi-coherent modules.

instance pushforwardQcoh_faithful : (Stacks.Modules.pushforwardQcoh i).Faithful

Stacks.ClosedImmersion.pushforwardQcoh_essImage_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedPushforward/Quasicoherent.lean, line 136. The attribute's comment: “essential image”.

[Stacks, Tag 01QY], the essential image. A quasi-coherent 𝒪_X-module is a direct image of a quasi-coherent 𝒪_Z-module exactly when the kernel of the comorphism of i annihilates it section by section, that is, when the ideal cutting out Z kills it.

theorem pushforwardQcoh_essImage_iff (G : X.Modules) (hG : G.IsQuasicoherent) :
    (Stacks.Modules.pushforwardQcoh i).essImage ⟨G, hG⟩ ↔
      ∀ (U : X.Opens) (a : Γ(X, U)), (i.app U).hom a = 0 → ∀ m : Γ(G, U), a • m = 0
Tag 01QZ, a lemma

Tag 01QZ in the Stacks Project.

AlgebraicGeometry.existsUnique_quasicoherentSubobject, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/QuasiCoherent/LargestSubsheaf.lean, line 81.

A subobject of a quasi-coherent module on a scheme contains a unique quasi-coherent subobject through which every morphism from a quasi-coherent module factors uniquely.

public lemma existsUnique_quasicoherentSubobject (X : AlgebraicGeometry.Scheme.{u})
    (F : X.Modules) [F.IsQuasicoherent] (G : Subobject F) :
    ∃! G' : { G' : Subobject (G : X.Modules) // (G' : X.Modules).IsQuasicoherent },
      ∀ (H : X.Modules) [H.IsQuasicoherent],
        Function.Bijective (fun f : H ⟶ (G'.1 : X.Modules) ↦ f ≫ G'.1.arrow)
Tag 01R0, a lemma

Tag 01R0 in the Stacks Project.

Stacks.ClosedImmersion.quasicoherentUpperShriek, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedPushforward/QuasicoherentAdjoint.lean, line 91. The attribute's comment: “the functor”.

i^! for a closed immersion, on quasi-coherent modules. It is the composite of the inclusion of quasi-coherent 𝒪_X-modules, the right adjoint of direct image on all modules, and the coherator on Z.

def quasicoherentUpperShriek :
    (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory ⥤
      (SheafOfModules.isQuasicoherent Z.ringCatSheaf).FullSubcategory

Stacks.ClosedImmersion.pushforwardQcohUpperShriekAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedPushforward/QuasicoherentAdjoint.lean, line 100. The attribute's comment: “the adjunction”.

[Stacks, Tag 01R0]. Direct image of quasi-coherent modules along a closed immersion of schemes is left adjoint to i^!.

def pushforwardQcohUpperShriekAdjunction :
    Stacks.Modules.pushforwardQcoh i ⊣ quasicoherentUpperShriek i

Stacks.ClosedImmersion.pushforwardQcoh_isLeftAdjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedPushforward/QuasicoherentAdjoint.lean, line 112. The attribute's comment: “existence of the right adjoint”.

[Stacks, Tag 01R0], as an existence statement. Direct image of quasi-coherent modules along a closed immersion of schemes has a right adjoint.

theorem pushforwardQcoh_isLeftAdjoint :
    (Stacks.Modules.pushforwardQcoh i).IsLeftAdjoint
Tag 0C4I, a lemma

Tag 0C4I in the Stacks Project.

AlgebraicGeometry.Scheme.IdealSheafData.isClosedImmersion_inclusion, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/ImmersionsAndAffine/ClosedImmersionIdealSheaves.lean, line 65. The attribute's comment: “closed immersions into the two factors”.

Stacks Project, Tag 0C4I and Tag 0C4J. An inclusion I ≤ J of quasi-coherent sheaves of ideals induces a closed immersion of the associated closed subschemes.

Applied to I ≤ I ⊔ J and J ≤ I ⊔ J this gives the closed immersions of the scheme theoretic intersection into either of the two subschemes, and applied to I ⊓ J ≤ I and I ⊓ J ≤ J it gives the closed immersions of either subscheme into their scheme theoretic union.

instance isClosedImmersion_inclusion {X : Scheme.{u}} {I J : X.IdealSheafData} (h : I ≤ J) :
    IsClosedImmersion (inclusion h)

AlgebraicGeometry.Scheme.IdealSheafData.isPullback_subscheme_sup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/ImmersionsAndAffine/ClosedImmersionIdealSheaves.lean, line 75. The attribute's comment: “cartesian intersection square”.

The subscheme cut out by the sum of two ideal sheaves is the fibre product of the corresponding closed subschemes over the ambient scheme.

theorem isPullback_subscheme_sup (X : Scheme.{u}) (I J : X.IdealSheafData) :
    IsPullback (I.inclusion le_sup_left : (I ⊔ J).subscheme ⟶ I.subscheme)
      (J.inclusion le_sup_right : (I ⊔ J).subscheme ⟶ J.subscheme)
      I.subschemeι J.subschemeι
Tag 0C4J, a lemma

Tag 0C4J in the Stacks Project.

AlgebraicGeometry.Scheme.IdealSheafData.isClosedImmersion_inclusion, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/ImmersionsAndAffine/ClosedImmersionIdealSheaves.lean, line 65. The attribute's comment: “union_closed_immersions”.

Stacks Project, Tag 0C4I and Tag 0C4J. An inclusion I ≤ J of quasi-coherent sheaves of ideals induces a closed immersion of the associated closed subschemes.

Applied to I ≤ I ⊔ J and J ≤ I ⊔ J this gives the closed immersions of the scheme theoretic intersection into either of the two subschemes, and applied to I ⊓ J ≤ I and I ⊓ J ≤ J it gives the closed immersions of either subscheme into their scheme theoretic union.

instance isClosedImmersion_inclusion {X : Scheme.{u}} {I J : X.IdealSheafData} (h : I ≤ J) :
    IsClosedImmersion (inclusion h)

AlgebraicGeometry.Scheme.IdealSheafData.unionIntersection_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/QuasiCoherent/ClosedUnionExactSequence.lean, line 436. The attribute's comment: “union_exact_sequence”.

Stacks Project, Tag 0C4J. The canonical sequence of structure sheaves of the scheme-theoretic union, the two closed subschemes and their scheme-theoretic intersection, whose last nonzero arrow is the difference of the two restriction maps, is short exact.

theorem unionIntersection_shortExact {S : Scheme.{u}} (I J : S.IdealSheafData) :
    ∃ zero : unionToBiprod I J ≫ biprodToIntersection I J = 0,
      (ShortComplex.mk (unionToBiprod I J) (biprodToIntersection I J) zero).ShortExact

AlgebraicGeometry.Scheme.IdealSheafData.isPushout_subscheme_inf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/QuasiCoherent/ClosedUnionPushout.lean, line 911. The attribute's comment: “union_pushout”.

The canonical square from the scheme-theoretic intersection of two closed subschemes to the two subschemes and then to their scheme-theoretic union is a pushout square.

theorem isPushout_subscheme_inf {S : Scheme.{u}} (I J : S.IdealSheafData) :
    IsPushout
      (Scheme.IdealSheafData.inclusion (I := I) (J := I ⊔ J) le_sup_left)
      (Scheme.IdealSheafData.inclusion (I := J) (J := I ⊔ J) le_sup_right)
      (Scheme.IdealSheafData.inclusion (I := I ⊓ J) (J := I) inf_le_left)
      (Scheme.IdealSheafData.inclusion (I := I ⊓ J) (J := J) inf_le_right)
Sources
LeanStacks.ClosedImmersion.pushforwardQcoh_exact · Stacks.ClosedImmersion.fullyFaithfulPushforwardQcoh · Stacks.ClosedImmersion.pushforwardQcoh_full · Stacks.ClosedImmersion.pushforwardQcoh_faithful · Stacks.ClosedImmersion.pushforwardQcoh_essImage_iff · AlgebraicGeometry.existsUnique_quasicoherentSubobject · Stacks.ClosedImmersion.quasicoherentUpperShriek · Stacks.ClosedImmersion.pushforwardQcohUpperShriekAdjunction

Section29.5 Supports of modules#

Section 29.5 of the Stacks Project, Tag 056H. 6 tags here are carried by 16 declarations of the repository (all in StacksFrontier) and 16 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 056H, the section

Tag 056H in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.fromSpec_preimage_supp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Support/SupportsOfModules.lean, line 41. The attribute's comment: “the sheaf-theoretic and module-theoretic supports agree”.

The sheaf-theoretic and module-theoretic supports agree. The inverse image of the support of a quasi-coherent module F under the inclusion Spec Γ(X, U) → X of an affine open U is the support of the Γ(X, U)-module Γ(F, U).

public theorem fromSpec_preimage_supp {X : Scheme.{u}} (F : X.Modules) [F.IsQuasicoherent]
    (U : X.affineOpens) :
    ⇑U.2.fromSpec ⁻¹' SheafOfModules.supp F = Module.support Γ(X, U.1) Γ(F, U.1)

Declarations registered for the tag:

Tag 056I, a lemma

Tag 056I in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.mem_support_sections_iff_mem_supp, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Support/AffineOpen.lean, line 52.

On an affine open, support of the sections module agrees with support of the quasi-coherent sheaf.

public lemma mem_support_sections_iff_mem_supp {X : Scheme.{u}} (F : X.Modules)
    [F.IsQuasicoherent] (U : X.affineOpens) (x : X) (hx : x ∈ U.1) :
    U.2.primeIdealOf ⟨x, hx⟩ ∈ Module.support Γ(X, U.1) Γ(F, U.1) ↔
      x ∈ SheafOfModules.supp F
Tag 05AC, a lemma

Tag 05AC in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.stableUnderSpecialization_supp, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Support/Specialization.lean, line 41.

The support of a quasi-coherent sheaf of modules on a scheme is stable under specialization.

public lemma stableUnderSpecialization_supp (X : Scheme.{u}) (F : X.Modules)
    [F.IsQuasicoherent] : StableUnderSpecialization (SheafOfModules.supp F)
Tag 056J, a lemma

Tag 056J in the Stacks Project.

SheafOfModules.isClosed_supp, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/Support.lean, line 151. The attribute's comment: “closed_support”.

The support of a sheaf of modules of finite type on a topological space is closed.

lemma isClosed_supp {X : TopCat.{u}} {R : TopCat.Sheaf RingCat.{u} X}
    (F : SheafOfModules.{u} R) [F.IsFiniteType] :
    IsClosed (supp F)

SheafOfModules.mem_supp_iff_nontrivial_stalk, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Support/Defs.lean, line 53. The attribute's comment: “support_by_stalk”.

A point is in the support of a sheaf of modules if and only if its stalk is nonzero.

lemma mem_supp_iff_nontrivial_stalk {X : TopCat.{u}}
    {R : TopCat.Sheaf RingCat.{u} X} (F : SheafOfModules.{u} R) (x : X) :
    x ∈ supp F ↔
      Nontrivial ((show TopCat.Presheaf Ab.{u} X from F.val.presheaf).stalk x)

AlgebraicGeometry.Scheme.Modules.nontrivial_stalk_iff_nontrivial_fibre, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Support/FiniteType.lean, line 218. The attribute's comment: “support_by_fibre”.

A finite type quasi-coherent module has nonzero stalk at x exactly when its fibre over the residue field at x is nonzero.

lemma nontrivial_stalk_iff_nontrivial_fibre
    {X : Scheme.{u}} (F : X.Modules) [F.IsFiniteType] [F.IsQuasicoherent] (x : X) :
    letI : Module (X.presheaf.stalk x) (F.presheaf.stalk x) :=
      PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
        F.val x
    letI : Algebra (X.presheaf.stalk x) (X.residueField x) :=
      (X.residue x).hom.toAlgebra
    Nontrivial (F.presheaf.stalk x) ↔
      Nontrivial (TensorProduct (X.presheaf.stalk x)
        (F.presheaf.stalk x) (X.residueField x))

SheafOfModules.supp_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportPullback/Basic.lean, line 51. The attribute's comment: “pullback_support”.

Stacks Project, Tag 056J. The support of the pullback of a module of finite type along a morphism of schemes is the inverse image of its support.

theorem supp_pullback {X Y : Scheme.{u}} (f : Y ⟶ X) (F : X.Modules) [F.IsFiniteType] :
    supp ((Scheme.Modules.pullback f).obj F) = f ⁻¹' supp F

Declarations registered for the tag:

Tag 05JU, a lemma

Tag 05JU in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.schemeTheoreticSupport, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Support/SchemeTheoretic.lean, line 94. The attribute's comment: “the closed subscheme”.

The scheme-theoretic support of a finite type quasi-coherent module, as an ideal sheaf: its component at an affine open U is the annihilator of the Γ(X, U)-module Γ(F, U). The closed subscheme it cuts out is the smallest one from which F is a direct image.

def schemeTheoreticSupport : X.IdealSheafData

AlgebraicGeometry.Scheme.Modules.schemeTheoreticSupport_ideal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Support/SchemeTheoretic.lean, line 102. The attribute's comment: “part (1): affine annihilator formula”.

On an affine open U = Spec A the scheme-theoretic support of F is cut out by the annihilator of the A-module Γ(F, U); equivalently, if F|_U is M~ then the scheme-theoretic support meets U in Spec (A / Ann_A M).

theorem schemeTheoreticSupport_ideal (U : X.affineOpens) :
    (schemeTheoreticSupport F).ideal U = Module.annihilator Γ(X, U.1) Γ(F, U.1)

AlgebraicGeometry.Scheme.Modules.exists_module_on_schemeTheoreticSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Support/SchemeTheoretic.lean, line 177. The attribute's comment: “existence of the descended module”.

A quasi-coherent module of finite type is the direct image of a quasi-coherent module of finite type on its scheme-theoretic support.

theorem exists_module_on_schemeTheoreticSupport :
    ∃ G : (schemeTheoreticSupport F).subscheme.Modules,
      G.IsQuasicoherent ∧ G.IsFiniteType ∧
        Nonempty ((Scheme.Modules.pushforward
          (schemeTheoreticSupport F).subschemeι).obj G ≅ F)

AlgebraicGeometry.Scheme.Modules.schemeTheoreticSupport_isSmallest, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Support/SchemeTheoretic.lean, line 189. The attribute's comment: “minimality”.

Every closed subscheme of X from which F is a direct image contains the scheme-theoretic support of F; equivalently, its ideal sheaf is contained in the ideal sheaf of the scheme-theoretic support.

theorem schemeTheoreticSupport_isSmallest (J : X.IdealSheafData)
    (G : J.subscheme.Modules)
    (e : (Scheme.Modules.pushforward J.subschemeι).obj G ≅ F) :
    J ≤ schemeTheoreticSupport F

AlgebraicGeometry.Scheme.Modules.module_on_schemeTheoreticSupport_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Support/SchemeTheoretic.lean, line 203. The attribute's comment: “part (2): uniqueness”.

A descent of F to its scheme-theoretic support is unique up to a unique isomorphism compatible with the chosen identifications of the direct images with F.

theorem module_on_schemeTheoreticSupport_unique
    (G H : (schemeTheoreticSupport F).subscheme.Modules)
    (eG : (Scheme.Modules.pushforward (schemeTheoreticSupport F).subschemeι).obj G ≅ F)
    (eH : (Scheme.Modules.pushforward (schemeTheoreticSupport F).subschemeι).obj H ≅ F) :
    ∃! φ : G ≅ H,
      (Scheme.Modules.pushforward (schemeTheoreticSupport F).subschemeι).map φ.hom ≫
        eH.hom = eG.hom

AlgebraicGeometry.Scheme.Modules.module_on_schemeTheoreticSupport_isFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Support/SchemeTheoretic.lean, line 219. The attribute's comment: “part (3): finite type”.

Every descent of F to its scheme-theoretic support is of finite type.

theorem module_on_schemeTheoreticSupport_isFiniteType
    (G : (schemeTheoreticSupport F).subscheme.Modules)
    (e : (Scheme.Modules.pushforward (schemeTheoreticSupport F).subschemeι).obj G ≅ F) :
    G.IsFiniteType

AlgebraicGeometry.Scheme.Modules.supp_eq_support_schemeTheoreticSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Support/SchemeTheoretic.lean, line 256. The attribute's comment: “part (4): support on the ambient scheme”.

The support of F is the closed set underlying its scheme-theoretic support.

theorem supp_eq_support_schemeTheoreticSupport :
    SheafOfModules.supp F = ((schemeTheoreticSupport F).support : Set X)

AlgebraicGeometry.Scheme.Modules.module_on_schemeTheoreticSupport_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Support/SchemeTheoretic.lean, line 269. The attribute's comment: “part (4): support on the closed subscheme”.

A descent of F to its scheme-theoretic support has support the whole closed subscheme.

theorem module_on_schemeTheoreticSupport_support
    (G : (schemeTheoreticSupport F).subscheme.Modules)
    (e : (Scheme.Modules.pushforward (schemeTheoreticSupport F).subschemeι).obj G ≅ F) :
    SheafOfModules.supp G = Set.univ
Tag 05JV, a definition

Tag 05JV in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.schemeTheoreticSupport, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Support/SchemeTheoretic.lean, line 94. The attribute's comment: “the scheme-theoretic support”.

The scheme-theoretic support of a finite type quasi-coherent module, as an ideal sheaf: its component at an affine open U is the annihilator of the Γ(X, U)-module Γ(F, U). The closed subscheme it cuts out is the smallest one from which F is a direct image.

def schemeTheoreticSupport : X.IdealSheafData
Sources
LeanAlgebraicGeometry.Scheme.Modules.fromSpec_preimage_supp · AlgebraicGeometry.Scheme.Modules.mem_support_sections_iff_mem_supp · AlgebraicGeometry.Scheme.Modules.stableUnderSpecialization_supp · SheafOfModules.isClosed_supp · SheafOfModules.mem_supp_iff_nontrivial_stalk · AlgebraicGeometry.Scheme.Modules.nontrivial_stalk_iff_nontrivial_fibre · AlgebraicGeometry.SheafOfModules.pullback_isFiniteType · Stacks.Modules.supp_pullback

Section29.6 Scheme theoretic image#

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

Tag 01R6, a lemma

Tag 01R6 in the Stacks Project.

Declarations registered for the tag:

Tag 01R7, a definition

Tag 01R7 in the Stacks Project.

Declarations registered for the tag:

Tag 01R8, a lemma

Tag 01R8 in the Stacks Project.

AlgebraicGeometry.isQuasicoherent_kernel_unitToPushforwardObjUnit, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/ImageQuasicoherent.lean, line 117. The attribute's comment: “part (1)”.

The sheaf of ideals cutting out the image of a quasi-compact morphism is quasi-coherent.

public instance isQuasicoherent_kernel_unitToPushforwardObjUnit
    {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] :
    (kernel (SheafOfModules.unitToPushforwardObjUnit f.toRingCatSheafHom)).IsQuasicoherent

AlgebraicGeometry.ker_morphismRestrict_eq_comap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/ImageQuasicoherent.lean, line 129. The attribute's comment: “part (3)”.

Scheme-theoretic images commute with restriction to an open subscheme of the target.

public theorem ker_morphismRestrict_eq_comap
    {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] (U : Y.Opens) :
    (f ∣_ U).ker = f.ker.comap U.ι

AlgebraicGeometry.imageMorphismRestrictIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/ImageQuasicoherent.lean, line 140. The attribute's comment: “part (3): canonical closed subscheme”. References: EGA I (9.5.8).

The scheme-theoretic image restricted to an open target is canonically the intersection of the original image with that open subscheme.

public noncomputable def imageMorphismRestrictIso
    {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] (U : Y.Opens) :
    (f ∣_ U).image ≅ pullback U.ι f.imageι

AlgebraicGeometry.imageMorphismRestrictIso_hom_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/ImageQuasicoherent.lean, line 148. The attribute's comment: “part (3): compatibility with inclusions”. References: EGA I (9.5.8), “identification over V”.

The canonical identification of restricted images respects their embeddings in U.

public theorem imageMorphismRestrictIso_hom_fst
    {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] (U : Y.Opens) :
    (imageMorphismRestrictIso f U).hom ≫ pullback.fst U.ι f.imageι =
      (f ∣_ U).imageι

Declarations registered for the tag:

Tag 056A, an example

Tag 056A in the Stacks Project.

AlgebraicGeometry.ker_SpecMap_eq_ker_SpecMap_quotientMk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/ImageSpecMap.lean, line 51. The attribute's comment: “equal closed subschemes”.

The scheme-theoretic image of Spec B ⟶ Spec A and the closed subscheme Spec (A ⧸ ker φ) of Spec A are cut out by the same ideal sheaf.

theorem ker_SpecMap_eq_ker_SpecMap_quotientMk :
    (Spec.map φ).ker =
      (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (RingHom.ker φ.hom)))).ker

AlgebraicGeometry.imageSpecMapIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/ImageSpecMap.lean, line 59.

The scheme-theoretic image of Spec B ⟶ Spec A is Spec (A ⧸ ker φ).

noncomputable def imageSpecMapIso :
    (Spec.map φ).image ≅ Spec (.of (A ⧸ RingHom.ker φ.hom))

AlgebraicGeometry.imageSpecMapIso_hom_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/ImageSpecMap.lean, line 70. The attribute's comment: “over Spec A”.

The isomorphism imageSpecMapIso lies over Spec A.

theorem imageSpecMapIso_hom_comp :
    (imageSpecMapIso φ).hom ≫
        Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (RingHom.ker φ.hom))) =
      (Spec.map φ).imageι
Tag 02JQ, a lemma

Tag 02JQ in the Stacks Project.

AlgebraicGeometry.exists_valuationRing_of_image_point, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/ImageValuativeDiagram.lean, line 192. The attribute's comment: “valuative diagram”.

Every point of the scheme-theoretic image of a quasi-compact morphism is reached by a map from a valuation ring whose generic point factors through the source.

public theorem exists_valuationRing_of_image_point
    {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] (z : f.image) :
    ∃ (A : Type u) (_ : CommRing A) (_ : IsDomain A) (_ : ValuationRing A)
      (K : Type u) (_ : Field K) (_ : Algebra A K) (_ : IsFractionRing A K)
      (g : Spec (.of K) ⟶ X) (h : Spec (.of A) ⟶ f.image),
      g ≫ f.toImage =
        Spec.map (CommRingCat.ofHom (algebraMap A K)) ≫ h ∧
      h (closedPoint A) = z

AlgebraicGeometry.exists_specializes_of_image_point, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/ImageValuativeDiagram.lean, line 212. The attribute's comment: “specialization consequence”.

A point of the scheme-theoretic image is a specialization of a point coming from the source.

public theorem exists_specializes_of_image_point
    {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] (z : f.image) :
    ∃ x : X, f x ⤳ f.imageι z
Tag 01R9, a lemma

Tag 01R9 in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.imageMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SchemeTheoreticImage/Basic.lean, line 92.

The morphism of scheme-theoretic images induced by a commutative square: for x : X ⟶ A, y : Y ⟶ B, f : X ⟶ Y and g : A ⟶ B with x ≫ g = f ≫ y, the closed immersion x.imageι ≫ g factors through the closed subscheme y.image of B.

noncomputable def imageMap (x : X ⟶ A) (y : Y ⟶ B) (f : X ⟶ Y) (g : A ⟶ B)
    (h : x ≫ g = f ≫ y) : x.image ⟶ y.image

AlgebraicGeometry.Scheme.Hom.imageMap_imageι, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SchemeTheoreticImage/Basic.lean, line 102.

The induced morphism imageMap x y f g h followed by the closed immersion y.imageι is x.imageι ≫ g.

lemma imageMap_imageι (x : X ⟶ A) (y : Y ⟶ B) (f : X ⟶ Y) (g : A ⟶ B)
    (h : x ≫ g = f ≫ y) : imageMap x y f g h ≫ y.imageι = x.imageι ≫ g

AlgebraicGeometry.Scheme.Hom.toImage_imageMap, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SchemeTheoreticImage/Basic.lean, line 109.

The morphism x.toImage followed by the induced morphism imageMap x y f g h is f ≫ y.toImage.

lemma toImage_imageMap (x : X ⟶ A) (y : Y ⟶ B) (f : X ⟶ Y) (g : A ⟶ B)
    (h : x ≫ g = f ≫ y) : x.toImage ≫ imageMap x y f g h = f ≫ y.toImage
Tag 056B, a lemma

Tag 056B in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.ker_eq_vanishingIdeal_closure_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SchemeTheoreticImage/Reduced.lean, line 48. References: EGA I (9.5.4), “partial”.

The scheme-theoretic image of a morphism f : X ⟶ Y with X reduced is the reduced induced closed subscheme structure on the closure of Set.range f, that is, the closed subscheme cut out by the vanishing ideal sheaf of that closure.

theorem ker_eq_vanishingIdeal_closure_range [IsReduced X] (f : X ⟶ Y) :
    f.ker = IdealSheafData.vanishingIdeal (.closure (Set.range f))
Tag 0CNG, a lemma

Tag 0CNG in the Stacks Project.

AlgebraicGeometry.isIso_pullback_snd_imageι_comp_of_section, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/ImmersionsAndAffine/SchemeTheoreticImage.lean, line 70.

Stacks 0CNG. The scheme-theoretic image of a section over a retrocompact open subset of the target of a separated morphism is isomorphic to that open subset after base change.

lemma isIso_pullback_snd_imageι_comp_of_section {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsSeparated f] (V : Y.Opens) (hV : IsRetrocompact (V : Set Y))
    (s : V.toScheme ⟶ X) (hs : s ≫ f = V.ι) :
    IsIso (pullback.snd (s.imageι ≫ f) V.ι)
Sources
LeanAlgebraicGeometry.Scheme.Hom.image · AlgebraicGeometry.Scheme.Hom.imageι · AlgebraicGeometry.Scheme.Hom.toImage · AlgebraicGeometry.Scheme.Hom.toImage_imageι · AlgebraicGeometry.Scheme.Hom.le_ker_comp · AlgebraicGeometry.IsClosedImmersion.lift · AlgebraicGeometry.IsClosedImmersion.lift_fac · AlgebraicGeometry.isQuasicoherent_kernel_unitToPushforwardObjUnit

Section29.7 Scheme theoretic closure and density#

Section 29.7 of the Stacks Project, Tag 01RA. 10 tags here are carried by 20 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01RB, a definition

Tag 01RB in the Stacks Project.

AlgebraicGeometry.Scheme.Opens.IsSchemeTheoreticallyDense, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/SchemeTheoreticallyDense.lean, line 71. The attribute's comment: “part (2)”. References: SGA 3 IX (4.1), “single open subscheme”.

An open subscheme U of X is scheme-theoretically dense if, for every open subscheme V of X, the scheme-theoretic image in V of U ∩ V is all of V.

abbrev IsSchemeTheoreticallyDense {X : Scheme.{u}} (U : X.Opens) : Prop

Declarations registered for the tag:

Tag 01RC, an example

Tag 01RC in the Stacks Project.

Stacks.Morphisms.DenseNotTopologicallyDense.injective_localizationProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/DenseNotTopologicallyDense.lean, line 233. The attribute's comment: “localization injection”.

The canonical map from A to the product of its localizations at the zₙ is injective.

public theorem injective_localizationProduct :
    Function.Injective (fun a : coordinateRing k =>
      fun n : ℕ => (algebraMap (coordinateRing k) (Localization.Away (z k n))) a)

Stacks.Morphisms.DenseNotTopologicallyDense.schemeTheoreticImage_openInclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/DenseNotTopologicallyDense.lean, line 374. The attribute's comment: “scheme-theoretic closure”.

The scheme-theoretic closure of the open U is all of X.

public theorem schemeTheoreticImage_openInclusion :
    IsSchemeTheoreticallyDominant (openComplement k).ι

Stacks.Morphisms.DenseNotTopologicallyDense.surjective_xProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/DenseNotTopologicallyDense.lean, line 390. The attribute's comment: “surjective projection”.

The projection X = Spec A → Spec k[x] is surjective.

public theorem surjective_xProjection : Function.Surjective (xProjection k).base

Stacks.Morphisms.DenseNotTopologicallyDense.xProjection_openComplement_avoids_xOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/DenseNotTopologicallyDense.lean, line 400. The attribute's comment: “restricted projection”.

The image of U under the projection to Spec k[x] avoids the basic open D(x).

public theorem xProjection_openComplement_avoids_xOpen :
    ∀ p : exampleScheme k, p ∈ (openComplement k : Set (exampleScheme k)) →
      (xProjection k).base p ∉
        (PrimeSpectrum.basicOpen (MvPolynomial.X () : xRing k) :
          Set (PrimeSpectrum (xRing k)))

Stacks.Morphisms.DenseNotTopologicallyDense.not_surjective_xProjection_openComplement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/DenseNotTopologicallyDense.lean, line 430. The attribute's comment: “restricted projection not surjective”.

The restriction of the projection to Spec k[x] to the open U is not surjective.

public theorem not_surjective_xProjection_openComplement :
    ¬ Set.SurjOn (xProjection k).base
      (openComplement k : Set (exampleScheme k))
      (Set.univ : Set (PrimeSpectrum (xRing k)))

Stacks.Morphisms.DenseNotTopologicallyDense.not_dense_openComplement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/DenseNotTopologicallyDense.lean, line 441. The attribute's comment: “not topologically dense”.

Although its scheme-theoretic closure is all of X, the open U is not topologically dense in X.

public theorem not_dense_openComplement :
    ¬ Dense (openComplement k : Set (exampleScheme k))
Tag 01RD, a lemma

Tag 01RD in the Stacks Project.

AlgebraicGeometry.Scheme.Opens.isSchemeTheoreticallyDense_iff_isSchemeTheoreticallyDominant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/SchemeTheoreticallyDense.lean, line 133.

An open subscheme whose inclusion is quasi-compact is scheme-theoretically dense exactly when its scheme-theoretic closure is the whole scheme, that is, when its inclusion is scheme-theoretically dominant.

theorem isSchemeTheoreticallyDense_iff_isSchemeTheoreticallyDominant {X : Scheme.{u}}
    (U : X.Opens) [QuasiCompact U.ι] :
    IsSchemeTheoreticallyDense U ↔ IsSchemeTheoreticallyDominant U.ι
Tag 056C, an example

Tag 056C in the Stacks Project.

Stacks.Morphisms.schemeTheoreticImage_iso_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Fibres/StandardOpenUnion.lean, line 187. The attribute's comment: “scheme-theoretic closure”.

The scheme-theoretic closure of the finite union of standard opens is the closed subscheme Spec (A/I), with its canonical map to Spec A.

public theorem schemeTheoreticImage_iso_quotient [Finite ι] (f : ι → A) :
    ∃ e : (standardOpenUnion f).ι.image ≅ Spec (.of (A ⧸ localizationKernel f)),
      (standardOpenUnion f).ι.imageι =
        e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (localizationKernel f)))

Stacks.Morphisms.quasiCompact_standardOpenUnion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Fibres/StandardOpenUnion.lean, line 241. The attribute's comment: “quasi-compactness”.

The inclusion of a finite union of standard opens is quasi-compact.

public theorem quasiCompact_standardOpenUnion [Finite ι] (f : ι → A) :
    QuasiCompact (standardOpenUnion f).ι

Stacks.Morphisms.schemeTheoreticallyDense_iff_localizationKernel_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Fibres/StandardOpenUnion.lean, line 257. The attribute's comment: “scheme-theoretic density”.

A finite union of standard opens is scheme-theoretically dense precisely when the canonical map to the product of localizations is injective.

public theorem schemeTheoreticallyDense_iff_localizationKernel_eq_bot [Finite ι]
    (f : ι → A) :
    AlgebraicGeometry.Scheme.Opens.IsSchemeTheoreticallyDense (standardOpenUnion f) ↔
      localizationKernel f = ⊥
Tag 01RE, a lemma

Tag 01RE in the Stacks Project.

AlgebraicGeometry.isSchemeTheoreticallyDense_opensRange_iff_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/DenseOpenImmersion.lean, line 181.

An open immersion has scheme-theoretically dense image if and only if its structure-sheaf map is injective.

public theorem isSchemeTheoreticallyDense_opensRange_iff_mono
    {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j] :
    Scheme.Opens.IsSchemeTheoreticallyDense j.opensRange ↔ Mono j.c
Tag 01RF, a lemma

Tag 01RF in the Stacks Project.

AlgebraicGeometry.Scheme.Opens.isSchemeTheoreticallyDense_inf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/SchemeTheoreticallyDense.lean, line 77.

The intersection of scheme-theoretically dense open subschemes is scheme-theoretically dense.

theorem isSchemeTheoreticallyDense_inf {X : Scheme.{u}} (U V : X.Opens)
    (hU : IsSchemeTheoreticallyDense U)
    (hV : IsSchemeTheoreticallyDense V) :
    IsSchemeTheoreticallyDense (U ⊓ V)
Tag 01RG, a lemma

Tag 01RG in the Stacks Project.

AlgebraicGeometry.isOpenImmersion_toImage, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/ImmersionImage.lean, line 97. The attribute's comment: “open immersion”. References: EGA I (9.5.10), “Y open in closure”.

An immersion which is quasi-compact, or has reduced source, is open in its scheme-theoretic image.

lemma isOpenImmersion_toImage {Z X : Scheme.{u}} (h : Z ⟶ X)
    [IsImmersion h] (hq_or_hr : QuasiCompact h ∨ IsReduced Z) :
    IsOpenImmersion h.toImage

AlgebraicGeometry.isSchemeTheoreticallyDense_toImage, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/ImmersionImage.lean, line 107. The attribute's comment: “scheme-theoretic density”.

The open subscheme corresponding to an immersion in its scheme-theoretic image is scheme-theoretically dense.

lemma isSchemeTheoreticallyDense_toImage {Z X : Scheme.{u}} (h : Z ⟶ X)
    [IsImmersion h] (hq_or_hr : QuasiCompact h ∨ IsReduced Z) :
    (letI : IsOpenImmersion h.toImage := isOpenImmersion_toImage h hq_or_hr
     Scheme.Opens.IsSchemeTheoreticallyDense h.toImage.opensRange)

AlgebraicGeometry.isDominant_toImage, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/ImmersionImage.lean, line 138. The attribute's comment: “topological density”. References: EGA I (9.5.10), “topological density”.

The image of an immersion is topologically dense in its scheme-theoretic image.

lemma isDominant_toImage {Z X : Scheme.{u}} (h : Z ⟶ X)
    [IsImmersion h] (hq_or_hr : QuasiCompact h ∨ IsReduced Z) :
    IsDominant h.toImage
Tag 056D, a lemma

Tag 056D in the Stacks Project.

AlgebraicGeometry.dense_open_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/ImmersionsAndAffine/SchemeTheoreticClosure.lean, line 66.

For an open subscheme of a reduced scheme, topological density, having the whole scheme as scheme-theoretic closure, and scheme-theoretic density are equivalent.

theorem dense_open_tfae {X : Scheme.{u}} [IsReduced X]
    (U : X.Opens) :
    List.TFAE [
      Dense (U : Set X),
      IsIso U.ι.imageι,
      Scheme.Opens.IsSchemeTheoreticallyDense U]
Tag 056E, a lemma

Tag 056E in the Stacks Project.

AlgebraicGeometry.isSchemeTheoreticallyDominant_iff_isSchemeTheoreticallyDense, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/ImmersionsAndAffine/SchemeTheoreticClosure.lean, line 117. The attribute's comment: “equivalence”.

For a reduced open subscheme, having scheme-theoretic closure equal to the ambient scheme is equivalent to being scheme-theoretically dense.

lemma isSchemeTheoreticallyDominant_iff_isSchemeTheoreticallyDense
    {X : Scheme.{u}} (U : X.Opens) [IsReduced U] :
    IsSchemeTheoreticallyDominant U.ι ↔ Scheme.Opens.IsSchemeTheoreticallyDense U

AlgebraicGeometry.isReduced_of_isSchemeTheoreticallyDense, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/ImmersionsAndAffine/SchemeTheoreticClosure.lean, line 126. The attribute's comment: “reducedness”.

A scheme with a reduced scheme-theoretically dense open subscheme is reduced.

lemma isReduced_of_isSchemeTheoreticallyDense
    {X : Scheme.{u}} (U : X.Opens) [IsReduced U]
    (hU : Scheme.Opens.IsSchemeTheoreticallyDense U) : IsReduced X
Tag 01RH, a lemma

Tag 01RH in the Stacks Project.

AlgebraicGeometry.eq_of_isSchemeTheoreticallyDominant_ι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/SchemeTheoreticallyDense.lean, line 146. The attribute's comment: “hypothesis: the scheme-theoretic closure of U in X is X, i.e. U.ι is scheme-theoretically dominant”.

Let X, Y be schemes over S and let f, g : X ⟶ Y be morphisms over S which agree after restriction to an open subscheme U ⊆ X. If the scheme-theoretic closure of U in X is X, that is, U.ι is scheme-theoretically dominant, and Y ⟶ S is separated, then f = g.

theorem eq_of_isSchemeTheoreticallyDominant_ι {S : Scheme.{u}} {X Y : Over S}
    (f g : X ⟶ Y) (U : X.left.Opens) [IsSchemeTheoreticallyDominant U.ι]
    [IsSeparated Y.hom] (hfg : U.ι ≫ f.left = U.ι ≫ g.left) :
    f = g
Sources
LeanAlgebraicGeometry.Scheme.Opens.IsSchemeTheoreticallyDense · AlgebraicGeometry.Scheme.Hom.image · Stacks.Morphisms.DenseNotTopologicallyDense.injective_localizationProduct · Stacks.Morphisms.DenseNotTopologicallyDense.schemeTheoreticImage_openInclusion · Stacks.Morphisms.DenseNotTopologicallyDense.surjective_xProjection · Stacks.Morphisms.DenseNotTopologicallyDense.xProjection_openComplement_avoids_xOpen · Stacks.Morphisms.DenseNotTopologicallyDense.not_surjective_xProjection_openComplement · Stacks.Morphisms.DenseNotTopologicallyDense.not_dense_openComplement

Section29.8 Dominant morphisms#

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

Tag 01RJ, a definition

Tag 01RJ in the Stacks Project.

Declarations registered for the tag:

Tag 01RK, a lemma

Tag 01RK in the Stacks Project.

AlgebraicGeometry.isDominant_of_genericPoints_subset_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Birational/Dominant.lean, line 51.

A morphism of schemes whose image contains the generic point of every irreducible component of the target is dominant.

theorem isDominant_of_genericPoints_subset_range {X S : Scheme.{u}} (f : X ⟶ S)
    (h : genericPoints S ⊆ Set.range f) : IsDominant f
Tag 01RL, a lemma

Tag 01RL in the Stacks Project.

AlgebraicGeometry.isDominant_iff_genericPoints_subset_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Dominant/GenericPoints.lean, line 234. References: EGA IV (1.1.5), “a) <=> b)”; EGA I (6.6.5).

Stacks Project, Tag 01RL. A quasi-compact morphism of schemes is dominant if and only if its image contains every generic point of an irreducible component of the target.

theorem isDominant_iff_genericPoints_subset_range {X S : Scheme.{u}} (f : X ⟶ S)
    [QuasiCompact f] :
    IsDominant f ↔ genericPoints S ⊆ Set.range f
Tag 0H3F, a lemma

Tag 0H3F in the Stacks Project.

AlgebraicGeometry.isDominant_pullback_snd_of_liftsGeneralizations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Dominant/BaseChange.lean, line 77.

Stacks Project, Tag 0H3F. A generizing base change of a quasi-compact dominant morphism of schemes is dominant.

public theorem isDominant_pullback_snd_of_liftsGeneralizations
    {X S S' : Scheme.{u}} (f : X ⟶ S) (g : S' ⟶ S) [QuasiCompact f] [IsDominant f]
    (hg : LiftsGeneralizations g) : IsDominant (pullback.snd f g)
Tag 0H8F, a lemma

Tag 0H8F in the Stacks Project.

AlgebraicGeometry.isDominant_pullback_snd_of_isOpenMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Dominant/BaseChange.lean, line 50.

Stacks Project, Tag 0H8F. The base change of a dominant morphism of schemes along an open morphism is dominant.

public theorem isDominant_pullback_snd_of_isOpenMap {X S S' : Scheme.{u}}
    (f : X ⟶ S) (g : S' ⟶ S) [IsDominant f] (hg : IsOpenMap g) :
    IsDominant (pullback.snd f g)
Tag 02NE, a lemma

Tag 02NE in the Stacks Project.

AlgebraicGeometry.exists_open_nhds_disjoint_range_of_quasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Dominant/GenericPoints.lean, line 219. References: EGA IV (9.7.5.1), “more general”.

Stacks Project, Tag 02NE. If a generic point of an irreducible component is not in the image of a quasi-compact morphism of schemes, it has an open neighbourhood with empty inverse image.

theorem exists_open_nhds_disjoint_range_of_quasiCompact
    {X S : Scheme.{u}} (f : X ⟶ S) [QuasiCompact f]
    (η : S) (hη : η ∈ genericPoints S) (hηf : η ∉ Set.range f) :
    ∃ V : S.Opens, η ∈ V ∧ f ⁻¹ᵁ V = ⊥
Tag 01RM, a lemma

Tag 01RM in the Stacks Project.

AlgebraicGeometry.isDominant_iff_genericPoint_mem_range, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Dominant/GenericPoints.lean, line 282. The attribute's comment: “dominant_iff_generic_points_in_image”.

Stacks Project, Tag 01RM. A morphism from a scheme with finitely many irreducible components is dominant if and only if its image contains the generic point of every irreducible component of the target.

lemma isDominant_iff_genericPoint_mem_range
    {X S : Scheme.{u}} (f : X ⟶ S)
    [Finite (irreducibleComponents X)] :
      IsDominant f ↔
      ∀ Z : irreducibleComponents S, Z.2.1.genericPoint ∈ Set.range f

AlgebraicGeometry.finite_irreducibleComponents_of_isDominant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Dominant/GenericPoints.lean, line 313. The attribute's comment: “finite_irreducible_components_target”.

A dominant morphism of schemes with finitely many irreducible components in its source has finitely many irreducible components in its target.

theorem finite_irreducibleComponents_of_isDominant
    {X S : Scheme.{u}} (f : X ⟶ S) [IsDominant f]
    (hX : (irreducibleComponents X).Finite) :
    (irreducibleComponents S).Finite
Tag 0CC1, a lemma

Tag 0CC1 in the Stacks Project.

AlgebraicGeometry.tfae_isDominant_of_isIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Dominant/IntegralSchemes.lean, line 99.

Stacks Project, Tag 0CC1. For a morphism f : X ⟶ Y of integral schemes, the following are equivalent: f is dominant; it maps the generic point of X to that of Y; the map on sections is injective for some, or for every, pair of nonempty affine opens U ⊆ X, V ⊆ Y with f(U) ⊆ V; and the map on local rings is injective at some, or at every, point of X.

public theorem tfae_isDominant_of_isIntegral
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegral X] [IsIntegral Y] :
    List.TFAE [
      IsDominant f,
      f (genericPoint X) = genericPoint Y,
      ∃ (U : X.affineOpens) (V : Y.affineOpens)
        (_ : Nonempty U.1) (_ : Nonempty V.1)
        (hUV : U.1 ≤ f ⁻¹ᵁ V.1),
        Function.Injective (f.appLE V.1 U.1 hUV),
      ∀ (U : X.affineOpens) (V : Y.affineOpens)
        (_ : Nonempty U.1) (_ : Nonempty V.1)
        (hUV : U.1 ≤ f ⁻¹ᵁ V.1),
        Function.Injective (f.appLE V.1 U.1 hUV),
      ∃ x : X, Function.Injective (f.stalkMap x),
      ∀ x : X, Function.Injective (f.stalkMap x)]
Sources
LeanAlgebraicGeometry.IsDominant · AlgebraicGeometry.isDominant_of_genericPoints_subset_range · AlgebraicGeometry.isDominant_iff_genericPoints_subset_range · AlgebraicGeometry.isDominant_pullback_snd_of_liftsGeneralizations · AlgebraicGeometry.isDominant_pullback_snd_of_isOpenMap · AlgebraicGeometry.exists_open_nhds_disjoint_range_of_quasiCompact · AlgebraicGeometry.isDominant_iff_genericPoint_mem_range · AlgebraicGeometry.finite_irreducibleComponents_of_isDominant

Section29.9 Surjective morphisms#

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

Tag 01RZ, a definition

Tag 01RZ in the Stacks Project.

Declarations registered for the tag:

Tag 01S0, a lemma

Tag 01S0 in the Stacks Project.

Declarations registered for the tag:

Tag 0495, a lemma

Tag 0495 in the Stacks Project.

Declarations registered for the tag:

Tag 01S1, a lemma

Tag 01S1 in the Stacks Project.

Declarations registered for the tag:

Tag 0496, an example

Tag 0496 in the Stacks Project.

AlgebraicGeometry.complexSpecMap_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Surjective/Injective.lean, line 199. The attribute's comment: “bijectivity before base change”.

Spec ℂ ⟶ Spec ℝ is a bijection on points.

public theorem complexSpecMap_bijective : Function.Bijective complexSpecMap.base

AlgebraicGeometry.complexTensorSpec_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Surjective/Injective.lean, line 205. The attribute's comment: “the base-change square”.

The tensor-square spectrum realizes the base change of Spec ℂ ⟶ Spec ℝ along itself.

public theorem complexTensorSpec_isPullback :
    IsPullback
      (Scheme.Spec.map (CommRingCat.ofHom
        (Algebra.TensorProduct.includeLeft : ℂ →ₐ[ℝ] ℂ ⊗[ℝ] ℂ).toRingHom).op)
      complexTensorSpecMap complexSpecMap complexSpecMap

AlgebraicGeometry.complexTensor_ringEquiv_prod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Surjective/Injective.lean, line 216. The attribute's comment: “product decomposition and idempotent”.

The tensor square of ℂ over ℝ splits into two copies of ℂ, with the indicated idempotent selecting the first factor.

public theorem complexTensor_ringEquiv_prod :
    ∃ e : (ℂ ⊗[ℝ] ℂ) ≃+* (ℂ × ℂ),
      e ((1 / 2 : ℝ) • (1 + Complex.I ⊗ₜ[ℝ] Complex.I)) = (1, 0)

AlgebraicGeometry.complexTensorSpec_two_points, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Surjective/Injective.lean, line 228. The attribute's comment: “two points after base change”.

The spectrum of the tensor square has exactly two points.

public theorem complexTensorSpec_two_points :
    Nat.card (Spec (.of (ℂ ⊗[ℝ] ℂ))) = 2

AlgebraicGeometry.complexTensorSpecMap_not_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Surjective/Injective.lean, line 234. The attribute's comment: “noninjectivity after base change”.

The base-changed map is not injective on points.

public theorem complexTensorSpecMap_not_injective :
    ¬ Function.Injective complexTensorSpecMap.base

AlgebraicGeometry.injective_not_stableUnderBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Surjective/Injective.lean, line 242. The attribute's comment: “injectivity is not stable”.

Injectivity of the underlying point map is not stable under base change for scheme morphisms.

public theorem injective_not_stableUnderBaseChange :
    ¬ CategoryTheory.MorphismProperty.IsStableUnderBaseChange
      (P := fun ⦃X Y : Scheme⦄ (f : X ⟶ Y) => Function.Injective f.base)

AlgebraicGeometry.bijective_not_stableUnderBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Surjective/Injective.lean, line 254. The attribute's comment: “bijectivity is not stable”.

Bijectivity of the underlying point map is not stable under base change for scheme morphisms.

public theorem bijective_not_stableUnderBaseChange :
    ¬ CategoryTheory.MorphismProperty.IsStableUnderBaseChange
      (P := fun ⦃X Y : Scheme⦄ (f : X ⟶ Y) => Function.Bijective f.base)
Tag 04ZD, a lemma

Tag 04ZD in the Stacks Project.

AlgebraicGeometry.quasiCompact_of_comp_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Surjective/QuasiCompact.lean, line 41. References: EGA IV (1.1.3).

If f is surjective and f ≫ q is quasi-compact, then q is quasi-compact.

public theorem quasiCompact_of_comp_surjective {X Y Z : Scheme.{u}}
    (f : X ⟶ Y) (q : Y ⟶ Z) [Surjective f] [QuasiCompact (f ≫ q)] :
    QuasiCompact q
Sources
LeanAlgebraicGeometry.Surjective · AlgebraicGeometry.instSurjectiveCompScheme · AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback · AlgebraicGeometry.Scheme.pullbackComparison_forget_surjective · AlgebraicGeometry.Surjective.instIsStableUnderBaseChangeScheme · AlgebraicGeometry.complexSpecMap_bijective · AlgebraicGeometry.complexTensorSpec_isPullback · AlgebraicGeometry.complexTensor_ringEquiv_prod

Section29.10 Radicial and universally injective morphisms#

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

Tag 01S3, a definition

Tag 01S3 in the Stacks Project.

Declarations registered for the tag:

Tag 01S4, a lemma

Tag 01S4 in the Stacks Project.

AlgebraicGeometry.universallyInjective_of_subsingleton_of_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/UniversallyInjectiveSection.lean, line 61. The attribute's comment: “a morphism with a subsingleton source and a section is universally injective”.

A morphism of schemes whose source is a subsingleton and which admits a section is universally injective. This is condition (3) of Stacks 01S4: injectivity on points is the subsingleton hypothesis, and at a point x of the source the residue field map is an isomorphism because x coincides with the image under the section of its own image.

theorem universallyInjective_of_subsingleton_of_section {X Y : Scheme.{u}} [Subsingleton X]
    (f : X ⟶ Y) (s : Y ⟶ X) (hs : s ≫ f = 𝟙 Y) : UniversallyInjective f
Tag 05VE, a lemma

Tag 05VE in the Stacks Project.

Declarations registered for the tag:

Tag 0472, a lemma

Tag 0472 in the Stacks Project.

Declarations registered for the tag:

Tag 02V1, a lemma

Tag 02V1 in the Stacks Project.

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.UniversallyInjective · AlgebraicGeometry.universallyInjective_of_subsingleton_of_section · AlgebraicGeometry.Scheme.Hom.injective · AlgebraicGeometry.isSeparated_of_injective · AlgebraicGeometry.UniversallyInjective.isStableUnderBaseChange · AlgebraicGeometry.universallyInjective_isStableUnderComposition · AlgebraicGeometry.tfae_universallyInjective

Section29.11 Affine morphisms#

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

Tag 01S6, a definition

Tag 01S6 in the Stacks Project.

Declarations registered for the tag:

Tag 01S7, a lemma

Tag 01S7 in the Stacks Project.

Declarations registered for the tag:

Tag 01S8, a lemma

Tag 01S8 in the Stacks Project.

AlgebraicGeometry.isAffineHom_iff_forall_exists_isAffineOpen, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/OpenCoverCriterion.lean, line 43. The attribute's comment: “equivalence of (1) and (2)”.

Stacks Project, Tag 01S8, equivalence of (1) and (2). A morphism of schemes f : X ⟶ S is affine if and only if every point of S has an affine open neighbourhood whose inverse image under f is affine.

lemma isAffineHom_iff_forall_exists_isAffineOpen {X S : Scheme.{u}} (f : X ⟶ S) :
    IsAffineHom f ↔
      ∀ x : S, ∃ U : S.Opens, x ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)

AlgebraicGeometry.relativeSpecPushforwardAlgebraIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/RelativeSpecCriterion.lean, line 204. The attribute's comment: “the source is the relative spectrum of the pushforward algebra”. References: EGA II (1.3.2).

For an affine morphism f : X ⟶ S, the source is, over S, the relative spectrum of the pushforward f_* 𝒪_X of its structure sheaf, which is a quasi-coherent sheaf of 𝒪_S-algebras.

def relativeSpecPushforwardAlgebraIso (f : X ⟶ S) [IsAffineHom f] :
    Over.mk f ≅ Over.mk (@relativeSpecToBase S (pushforwardAlgebra f)
      (isQuasicoherent_pushforwardAlgebra f))

AlgebraicGeometry.isAffineHom_iff_exists_relativeSpecIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/RelativeSpecCriterion.lean, line 230. The attribute's comment: “equivalence of (1) and (3)”. References: EGA II (1.3.1), “partial”; SGA 3 I (4.2), “partial”.

Stacks Project, Tag 01S8, equivalence of (1) and (3). A morphism of schemes is affine if and only if it is isomorphic, as an object over its target, to the structure morphism of the relative spectrum of a quasi-coherent sheaf of algebras on the target.

theorem isAffineHom_iff_exists_relativeSpecIso (f : X ⟶ S) :
    IsAffineHom f ↔
      ∃ (A : AlgebraSheaf S) (hA : AlgebraSheaf.IsQuasicoherent A),
        Nonempty (Over.mk f ≅ Over.mk (@relativeSpecToBase S A hA))

Stacks.AffineAlgebraEquivalence.overRelativeSpecIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpecBaseChange/AntiEquivalence.lean, line 257. The attribute's comment: “the final statement: X = Spec_S(f_* O_X) for an affine morphism f : X → S”.

Stacks Project, Tag 01S8, the final statement. For an affine morphism f : X ⟶ S there is an isomorphism X ≅ \underline{Spec}_S(f_* 𝒪_X) of schemes over S.

public noncomputable def overRelativeSpecIso {X S : Scheme.{u}} (f : X ⟶ S) [IsAffineHom f] :
    letI := isQuasicoherent_pushforwardAlgebra f
    (Over.mk f : Over S) ≅ Over.mk (relativeSpecToBase (pushforwardAlgebra f))

Stacks.AffineAlgebraEquivalence.isAffineHom_iff_exists_quasicoherentAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpecBaseChange/AntiEquivalence.lean, line 280. The attribute's comment: “part (3): f is affine iff X is a relative spectrum over S”. References: SGA 3 I (4.2), “partial”; SGA 3 III (0.1.7), “0.1.7(a)”.

Stacks Project, Tag 01S8, part (3). A morphism of schemes f : X ⟶ S is affine if and only if there is a quasi-coherent sheaf of 𝒪_S-algebras A and an isomorphism X ≅ \underline{Spec}_S(A) of schemes over S.

The forward direction takes A = f_* 𝒪_X and is overRelativeSpecIso; the converse is isAffineHom_relativeSpecToBase together with isAffineHom_of_overIso.

public theorem isAffineHom_iff_exists_quasicoherentAlgebra {X S : Scheme.{u}} (f : X ⟶ S) :
    IsAffineHom f ↔ ∃ A : QuasicoherentAlgebra S,
      letI := A.property
      Nonempty ((Over.mk f : Over S) ≅ Over.mk (relativeSpecToBase A.obj))
Tag 01S9, a remark

Tag 01S9 in the Stacks Project.

AlgebraicGeometry.isAffineHom_of_iSup_eq_top_of_isAffineOpen_preimage, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/AffineCoverDirect.lean, line 84.

Stacks Project, Tag 01S9. If S = ⋃ⱼ Wⱼ is an affine open covering such that each f⁻¹(Wⱼ) is affine, then f : X ⟶ S is affine.

lemma isAffineHom_of_iSup_eq_top_of_isAffineOpen_preimage {ι : Type*} (W : ι → S.Opens)
    (hW : ∀ j, IsAffineOpen (W j)) (hcov : ⨆ j, W j = ⊤)
    (hfW : ∀ j, IsAffineOpen (f ⁻¹ᵁ W j)) :
    IsAffineHom f
Tag 01SA, a lemma

Tag 01SA in the Stacks Project.

Stacks.AlgebraPullbackQcoh.affineEquivalenceAlgebras, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AlgebraPullbackQcoh/BaseChangeIso.lean, line 438. References: SGA 3 I (4.2), “more general”.

All nine clauses of [Stacks, Tag 01SA]. The canonical anti-equivalence between the schemes affine over a base and the quasi-coherent sheaves of commutative algebras on that base, compatible with arbitrary base change.

The tag is registered by a single unqualified attribute on this nine-field structure.

def affineEquivalenceAlgebras : AffineAlgebraAntiEquivalence.{u}

Stacks.AffineAlgebraEquivalence.affineAlgebraAntiEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpecOpenRestriction/GeneralBaseChange.lean, line 191. The attribute's comment: “compatibility of the anti-equivalence with arbitrary base change”. References: EGA II (1.5.2); SGA 3 I (4.2), “more general”.

Stacks Project, Tag 01SA, the base-change clause. The anti-equivalence between the schemes affine over S and the quasi-coherent sheaves of 𝒪_S-algebras is compatible with arbitrary base change, unconditionally: the one assertion on which Stacks.AffineAlgebraEquivalence.antiEquivalenceOfQuasicoherentAlgebraPullback was left standing is isQuasicoherentAlgebraPullback, proved above.

public noncomputable def affineAlgebraAntiEquivalence : AffineAlgebraAntiEquivalence.{u}
Tag 0H88, a lemma

Tag 0H88 in the Stacks Project.

Stacks.AlgebraicGeometry.QcohLimits.isQuasicoherent_restrictScalars_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QcohLimits/RestrictScalars.lean, line 203. References: EGA I (9.6.1).

Stacks Project, Tag 0H88. Let α : 𝒪_S ⟶ A be a sheaf of rings on a scheme S which is quasi-coherent as an 𝒪_S-module. An A-module is quasi-coherent as an 𝒪_S-module if and only if it is quasi-coherent as an A-module.

theorem isQuasicoherent_restrictScalars_iff
    (hA : ((SheafOfModules.restrictScalars.{u} α).obj (SheafOfModules.unit A)).IsQuasicoherent)
    (G : SheafOfModules.{u} A) :
    ((SheafOfModules.restrictScalars.{u} α).obj G).IsQuasicoherent ↔ G.IsQuasicoherent
Tag 01SB, a lemma

Tag 01SB in the Stacks Project.

Stacks.AlgebraicGeometry.AffineQcohUnit.isEquivalence_affineQuasicoherentPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineQcohUnit/Equivalence.lean, line 61. The attribute's comment: “the equivalence”.

Stacks Project, Tag 01SB, first assertion. For an affine morphism f : X ⟶ S, direct image induces an equivalence from quasi-coherent 𝒪_X-modules to quasi-coherent modules over f_* 𝒪_X, with quasi-inverse 𝒢 ↦ f^*𝒢 ⊗_{f^*f_*𝒪_X} 𝒪_X.

theorem isEquivalence_affineQuasicoherentPushforward [IsAffineHom f] :
    (affineQuasicoherentPushforward f).IsEquivalence

Stacks.AlgebraicGeometry.QcohLimits.affine_isQuasicoherent_restrictScalars_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QcohLimits/RestrictScalars.lean, line 242. The attribute's comment: “quasi-coherence under scalar restriction”. References: EGA II (1.4.3), “special case”.

Stacks Project, Tag 01SB, second assertion. An f_* 𝒪_X-module is quasi-coherent as an 𝒪_S-module if and only if it is quasi-coherent as an f_* 𝒪_X-module.

This is the whole of the tag's final statement ("Moreover, an 𝒜-module is quasi-coherent as an 𝒪_S-module if and only if it is quasi-coherent as an 𝒜-module"). The tag's other assertion, the equivalence of categories, is not proved here, so the attribute is clause-qualified.

theorem affine_isQuasicoherent_restrictScalars_iff (f : X ⟶ S) [IsAffineHom f]
    (G : SheafOfModules.{u} (AffineQcohPushforward.pushforwardRing f.base X.ringCatSheaf)) :
    ((SheafOfModules.restrictScalars f.toRingCatSheafHom).obj G).IsQuasicoherent ↔
      G.IsQuasicoherent
Tag 01SC, a lemma

Tag 01SC in the Stacks Project.

Declarations registered for the tag:

Tag 01SD, a lemma

Tag 01SD in the Stacks Project.

AlgebraicGeometry.IsAffineHom.of_isPullback, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/BaseChange.lean, line 36.

The base change of an affine morphism is affine: if f : X ⟶ S is affine and g' ≫ f = f' ≫ g is a cartesian square, then the base change f' : X' ⟶ S' of f along g : S' ⟶ S is affine.

lemma IsAffineHom.of_isPullback {X S X' S' : Scheme.{u}} {g' : X' ⟶ X} {f' : X' ⟶ S'}
    {f : X ⟶ S} {g : S' ⟶ S} (sq : IsPullback g' f' f g) [IsAffineHom f] :
    IsAffineHom f'
Tag 01SE, a lemma

Tag 01SE in the Stacks Project.

Declarations registered for the tag:

Tag 01SF, a lemma

Tag 01SF in the Stacks Project.

Stacks.NonvanishingAffineIntersection.isAffineOpen_inf_nonvanishingOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NonvanishingAffineIntersection/Basic.lean, line 122. The attribute's comment: “affineness of the inclusion j : X_s -> X, i.e. preimages of affine opens under j”. References: EGA II (5.5.8); SGA 6 II (2.2.3.1).

Let X be a scheme, M an invertible 𝒪_X-module and s a global section of M. For every affine open U of X, the intersection U ∩ X_s of U with the nonvanishing locus of s is affine.

theorem isAffineOpen_inf_nonvanishingOpen {U : X.Opens} (hU : IsAffineOpen U) :
    IsAffineOpen (U ⊓ Stacks.NonvanishingOpen.nonvanishingOpen X M s)
Tag 01SG, a lemma

Tag 01SG in the Stacks Project.

AlgebraicGeometry.isAffineHom_of_isAffineHom_of_isAffineHom_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/AffineDiagonalTarget.lean, line 55. The attribute's comment: “part (1)”.

Let g : X ⟶ Y be a morphism of schemes over S. If X is affine over S and the diagonal Y ⟶ Y ×_S Y is affine, then g is affine.

public theorem isAffineHom_of_isAffineHom_of_isAffineHom_diagonal (g : X ⟶ Y) {a : X ⟶ S}
    (b : Y ⟶ S) (hab : g ≫ b = a) [IsAffineHom a]
    [IsAffineHom (pullback.diagonal b)] : IsAffineHom g

AlgebraicGeometry.isAffineHom_of_isAffineHom_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/AffineDiagonalTarget.lean, line 66. The attribute's comment: “part (2)”.

Let g : X ⟶ Y be a morphism of schemes over S. If X is affine over S and Y is separated over S, then g is affine.

public theorem isAffineHom_of_isAffineHom_of_isSeparated (g : X ⟶ Y) {a : X ⟶ S} (b : Y ⟶ S)
    (hab : g ≫ b = a) [IsAffineHom a] [IsSeparated b] : IsAffineHom g

AlgebraicGeometry.isAffineHom_of_isAffine_of_isAffineHom_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/AffineDiagonalTarget.lean, line 74. The attribute's comment: “part (3)”.

A morphism from an affine scheme to a scheme with affine diagonal is affine.

public theorem isAffineHom_of_isAffine_of_isAffineHom_diagonal (g : X ⟶ Y) [IsAffine X]
    [IsAffineHom (pullback.diagonal (terminal.from Y))] : IsAffineHom g

AlgebraicGeometry.isAffineHom_of_isAffine_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/AffineDiagonalTarget.lean, line 81. The attribute's comment: “part (4)”.

A morphism from an affine scheme to a separated scheme is affine.

public theorem isAffineHom_of_isAffine_of_isSeparated (g : X ⟶ Y) [IsAffine X]
    [Y.IsSeparated] : IsAffineHom g
Tag 01SH, a lemma

Tag 01SH in the Stacks Project.

Declarations registered for the tag:

Tag 01SI, a lemma

Tag 01SI in the Stacks Project.

AlgebraicGeometry.isAffineHom_of_isArtinianRing, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/Artinian.lean, line 39.

Stacks Project, Tag 01SI. Every morphism from the spectrum of an Artinian ring to a scheme is affine.

lemma isAffineHom_of_isArtinianRing {A : CommRingCat.{u}} [IsArtinianRing A]
    {S : Scheme.{u}} (f : Spec A ⟶ S) : IsAffineHom f
Tag 0C3A, a lemma

Tag 0C3A in the Stacks Project.

AlgebraicGeometry.isAffineHom_of_isAffineHom_restrict_of_isClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/ImmersionsAndAffine/AffineImmersion.lean, line 62. The attribute's comment: “immersion is affine”.

Stacks Project, Tag 0C3A, affineness of the immersion. An immersion j : Y ⟶ X is affine as soon as there is an open U ⊆ X with affine inclusion over which j restricts to an affine morphism and whose complement meets the image of j in a closed set.

theorem isAffineHom_of_isAffineHom_restrict_of_isClosed {X Y : Scheme.{u}} (j : Y ⟶ X)
    [IsImmersion j] (U : X.Opens) [IsAffineHom U.ι] [IsAffineHom (j ∣_ U)]
    (hZ : IsClosed (Set.range (j : Y → X) ∩ (U : Set X)ᶜ)) : IsAffineHom j

AlgebraicGeometry.isAffine_of_isAffineHom_restrict_of_isClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/ImmersionsAndAffine/AffineImmersion.lean, line 98. The attribute's comment: “source is affine”.

Stacks Project, Tag 0C3A, affineness of the source. In the situation of AlgebraicGeometry.isAffineHom_of_isAffineHom_restrict_of_isClosed with an affine target, the source of the immersion is affine.

theorem isAffine_of_isAffineHom_restrict_of_isClosed {X Y : Scheme.{u}} (j : Y ⟶ X)
    [IsImmersion j] [IsAffine X] (U : X.Opens) [IsAffineHom U.ι] [IsAffineHom (j ∣_ U)]
    (hZ : IsClosed (Set.range (j : Y → X) ∩ (U : Set X)ᶜ)) : IsAffine Y
Sources
LeanAlgebraicGeometry.IsAffineHom · AlgebraicGeometry.IsSeparated.of_isAffineHom · AlgebraicGeometry.instQuasiCompactOfIsAffineHom · AlgebraicGeometry.isAffineHom_iff_forall_exists_isAffineOpen · AlgebraicGeometry.relativeSpecPushforwardAlgebraIso · AlgebraicGeometry.isAffineHom_iff_exists_relativeSpecIso · Stacks.AffineAlgebraEquivalence.overRelativeSpecIso · Stacks.AffineAlgebraEquivalence.isAffineHom_iff_exists_quasicoherentAlgebra

Section29.12 Families of ample invertible modules#

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

Tag 0FXR, a definition

Tag 0FXR in the Stacks Project.

Declarations registered for the tag:

Tag 0FXS, a lemma

Tag 0FXS in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.isAffineHom_diagonal_of_affine_nonvanishingOpen_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineNonvanishing/AffineDiagonal.lean, line 67.

Stacks Project, Tag 0FXS. A cover by affine nonvanishing loci of sections of invertible modules implies that the diagonal is affine.

theorem isAffineHom_diagonal_of_affine_nonvanishingOpen_cover (X : Scheme.{u})
    (h : ∀ x : X, ∃ L : X.Modules,
      ∃ _ : IsInvertible X.presheaf (structureSheafRing X.toRingedSpace).property L,
      ∃ s : L.sections,
        x ∈ nonvanishingOpen (X := X.toRingedSpace) L s ∧
          IsAffineOpen (nonvanishingOpen (X := X.toRingedSpace) L s)) :
    IsAffineHom (pullback.diagonal (terminal.from X))
Sources
LeanAlgebraicGeometry.Scheme.IsAmpleFamily · AlgebraicGeometry.Scheme.Modules.isAffineHom_diagonal_of_affine_nonvanishingOpen_cover

Section29.13 Quasi-affine morphisms#

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

Tag 01SK, a definition

Tag 01SK in the Stacks Project.

AlgebraicGeometry.IsQuasiAffineHom, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/QuasiAffine.lean, line 47.

A morphism of schemes is quasi-affine if the inverse image of every affine open subscheme of the target is a quasi-affine scheme.

class IsQuasiAffineHom {X S : Scheme} (f : X ⟶ S) : Prop
Tag 01SL, a lemma

Tag 01SL in the Stacks Project.

AlgebraicGeometry.isSeparated_of_isQuasiAffineHom, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/QuasiAffine.lean, line 52. The attribute's comment: “separated”. References: EGA II (1.2.4), “more general”; EGA II (5.1.6), “partial”.

A quasi-affine morphism of schemes is separated.

instance isSeparated_of_isQuasiAffineHom {X S : Scheme.{u}} (f : X ⟶ S)
    [IsQuasiAffineHom f] : IsSeparated f

AlgebraicGeometry.quasiCompact_of_isQuasiAffineHom, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/QuasiAffine.lean, line 66. The attribute's comment: “quasi-compact”.

A quasi-affine morphism of schemes is quasi-compact.

instance quasiCompact_of_isQuasiAffineHom {X S : Scheme.{u}} (f : X ⟶ S)
    [IsQuasiAffineHom f] : QuasiCompact f
Tag 01SM, a lemma

Tag 01SM in the Stacks Project.

AlgebraicGeometry.isQuasiAffineHom_iff_toSpecΓ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiAffineFlatBaseChange.lean, line 140. The attribute's comment: “(4) over an affine base”. References: EGA II (5.1.6), “(a)<=>(b), affine base”; EGA II (5.1.8).

Stacks Project, Tag 01SM, part (4), over an affine base. A morphism to an affine scheme is quasi-affine if and only if the canonical morphism from its source to the spectrum of its global sections — the relative spectrum of the pushforward of the structure sheaf — is a quasi-compact open immersion.

theorem isQuasiAffineHom_iff_toSpecΓ [IsAffine S] (f : X ⟶ S) :
    IsQuasiAffineHom f ↔ IsOpenImmersion X.toSpecΓ ∧ QuasiCompact X.toSpecΓ

AlgebraicGeometry.isQuasiAffineHom_iff_exists_isOpenCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/QuasiAffineLocal.lean, line 154. The attribute's comment: “(1) ↔ (2)”. References: EGA II (5.1.1).

A morphism of schemes is quasi-affine if and only if there exists an affine open covering of the target all of whose members have quasi-affine inverse image.

theorem isQuasiAffineHom_iff_exists_isOpenCover {X S : Scheme.{u}} (f : X ⟶ S) :
    IsQuasiAffineHom f ↔ ∃ (ι : Type u) (U : ι → S.affineOpens),
      IsOpenCover (fun i ↦ (U i : S.Opens)) ∧
        ∀ i, Scheme.IsQuasiAffine (f ⁻¹ᵁ (U i : S.Opens)).toScheme

AlgebraicGeometry.isQuasiAffineHom_iff_canonicalMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/QuasiAffineRelativeSpec.lean, line 140. The attribute's comment: “(1) ↔ (4) over a general base, carrying the quasi-compact and quasi-separated hypotheses that make f_* 𝒪_X quasi-coherent”. References: EGA II (5.1.2), “more general”; EGA II (5.1.6).

A morphism of schemes which is quasi-compact and quasi-separated — so that f_* 𝒪_X is a quasi-coherent sheaf of 𝒪_S-algebras and the canonical morphism X ⟶ Spec_S(f_* 𝒪_X) exists — is quasi-affine if and only if that canonical morphism is a quasi-compact open immersion.

theorem isQuasiAffineHom_iff_canonicalMorphism :
    IsQuasiAffineHom f ↔
      IsOpenImmersion (canonicalMorphism f) ∧ QuasiCompact (canonicalMorphism f)

AlgebraicGeometry.isOpenImmersion_canonicalMorphism, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/QuasiAffineRelativeSpec.lean, line 161. The attribute's comment: “(1) ⇒ (4), the open-immersion half”.

The canonical morphism from the source of a quasi-affine morphism to the relative spectrum of the pushed-forward structure sheaf is an open immersion.

instance isOpenImmersion_canonicalMorphism (f : X ⟶ S) [IsQuasiAffineHom f] :
    IsOpenImmersion (canonicalMorphism f)

AlgebraicGeometry.quasiCompact_canonicalMorphism, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/QuasiAffineRelativeSpec.lean, line 168. The attribute's comment: “(1) ⇒ (4), the quasi-compactness half”.

The canonical morphism from the source of a quasi-affine morphism to the relative spectrum of the pushed-forward structure sheaf is quasi-compact.

instance quasiCompact_canonicalMorphism (f : X ⟶ S) [IsQuasiAffineHom f] :
    QuasiCompact (canonicalMorphism f)

AlgebraicGeometry.isQuasiAffineHom_iff_exists_relativeSpec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/QuasiAffineRelativeSpec.lean, line 175. The attribute's comment: “(1) ↔ (3) over a general base, no hypotheses”.

A morphism of schemes f : X ⟶ S is quasi-affine if and only if there is a quasi-coherent sheaf A of 𝒪_S-algebras and a quasi-compact open immersion X ⟶ Spec_S(A) over S.

theorem isQuasiAffineHom_iff_exists_relativeSpec (f : X ⟶ S) :
    IsQuasiAffineHom f ↔
      ∃ (A : AlgebraSheaf S) (hA : AlgebraSheaf.IsQuasicoherent A)
        (g : X ⟶ @relativeSpec S A hA),
        IsOpenImmersion g ∧ QuasiCompact g ∧ g ≫ @relativeSpecToBase S A hA = f

AlgebraicGeometry.isQuasiAffineHom_iff_of_iSup_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/QuasiAffineStability.lean, line 162. The attribute's comment: “(1) iff (2)”.

Stacks Project, Tag 01SM, (1) is equivalent to (2). A morphism of schemes is quasi-affine if and only if the preimages of the members of one affine open covering of the target are quasi-affine schemes.

theorem isQuasiAffineHom_iff_of_iSup_eq_top {X S : Scheme.{u}} (f : X ⟶ S) {ι : Type*}
    (U : ι → S.Opens) (hU : ∀ i, IsAffineOpen (U i)) (hU' : ⨆ i, U i = ⊤) :
    IsQuasiAffineHom f ↔ ∀ i, (f ⁻¹ᵁ U i).toScheme.IsQuasiAffine
Tag 01SN, a lemma

Tag 01SN in the Stacks Project.

AlgebraicGeometry.isQuasiAffineHom_isStableUnderComposition, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/QuasiAffineStability.lean, line 185. References: EGA II (5.1.10).

Stacks Project, Tag 01SN. A composition of quasi-affine morphisms of schemes is quasi-affine.

instance isQuasiAffineHom_isStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsQuasiAffineHom : MorphismProperty Scheme.{u})
Tag 01SO, a lemma

Tag 01SO in the Stacks Project.

AlgebraicGeometry.isQuasiAffineHom_isStableUnderBaseChange, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/QuasiAffineStability.lean, line 201. References: EGA IV (2.7.1), “(xiv)”.

Stacks Project, Tag 01SO. Quasi-affine morphisms of schemes are stable under arbitrary base change.

instance isQuasiAffineHom_isStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange
      (@IsQuasiAffineHom : MorphismProperty Scheme.{u})
Tag 02JR, a lemma

Tag 02JR in the Stacks Project.

AlgebraicGeometry.isQuasiAffineHom_of_isImmersion_of_quasiCompact, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/ImmersionsAndAffine/QuasiAffineImmersion.lean, line 40.

Stacks Project, Tag 02JR. Every quasi-compact immersion of schemes is quasi-affine.

instance isQuasiAffineHom_of_isImmersion_of_quasiCompact
    {X S : Scheme.{u}} (f : X ⟶ S) [IsImmersion f] [QuasiCompact f] :
    IsQuasiAffineHom f
Tag 01SP, a lemma

Tag 01SP in the Stacks Project.

AlgebraicGeometry.isQuasiAffineHom_iff_quasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/QuasiAffine.lean, line 74. The attribute's comment: “characterization”.

A morphism from an affine scheme is quasi-affine if and only if it is quasi-compact.

theorem isQuasiAffineHom_iff_quasiCompact {X S : Scheme.{u}} [IsAffine X]
    (f : X ⟶ S) : IsQuasiAffineHom f ↔ QuasiCompact f

AlgebraicGeometry.isQuasiAffineHom_of_isQuasiAffine_of_quasiSeparatedSpace, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/QuasiAffine.lean, line 85. The attribute's comment: “quasi-separated target”. References: EGA II (5.1.8), “X q-affine ⇒ f q-affine”.

Every morphism from a quasi-affine scheme to a quasi-separated scheme is quasi-affine.

instance isQuasiAffineHom_of_isQuasiAffine_of_quasiSeparatedSpace
    {X S : Scheme.{u}} [Scheme.IsQuasiAffine X] [QuasiSeparatedSpace S]
    (f : X ⟶ S) : IsQuasiAffineHom f
Tag 054G, a lemma

Tag 054G in the Stacks Project.

AlgebraicGeometry.isQuasiAffineHom_of_isQuasiAffine_of_quasiSeparatedSpace, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/QuasiAffine.lean, line 85. The attribute's comment: “absolute corollary”. References: EGA II (5.1.8), “X q-affine ⇒ f q-affine”.

Every morphism from a quasi-affine scheme to a quasi-separated scheme is quasi-affine.

instance isQuasiAffineHom_of_isQuasiAffine_of_quasiSeparatedSpace
    {X S : Scheme.{u}} [Scheme.IsQuasiAffine X] [QuasiSeparatedSpace S]
    (f : X ⟶ S) : IsQuasiAffineHom f

AlgebraicGeometry.IsQuasiAffineHom.of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/QuasiAffineQuasiSeparated.lean, line 36. The attribute's comment: “relative statement”.

A morphism g : X ⟶ Y to a scheme quasi-separated over a base S via h : Y ⟶ S is quasi-affine as soon as the structure morphism g ≫ h of X over S is quasi-affine.

theorem IsQuasiAffineHom.of_comp {X Y S : Scheme.{u}} (g : X ⟶ Y) (h : Y ⟶ S)
    [IsQuasiAffineHom (g ≫ h)] [QuasiSeparated h] : IsQuasiAffineHom g
Sources
LeanAlgebraicGeometry.IsQuasiAffineHom · AlgebraicGeometry.isSeparated_of_isQuasiAffineHom · AlgebraicGeometry.quasiCompact_of_isQuasiAffineHom · AlgebraicGeometry.isQuasiAffineHom_iff_toSpecΓ · AlgebraicGeometry.isQuasiAffineHom_iff_exists_isOpenCover · AlgebraicGeometry.isQuasiAffineHom_iff_canonicalMorphism · AlgebraicGeometry.isOpenImmersion_canonicalMorphism · AlgebraicGeometry.quasiCompact_canonicalMorphism

Section29.14 Types of morphisms defined by properties of ring maps#

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

Tag 01SR, a definition

Tag 01SR in the Stacks Project.

RingHom.StacksPropertyIsLocal, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/Defs.lean, line 71. The attribute's comment: “(1) local, all three conditions (a), (b), (c)”.

A property of commutative-ring homomorphisms is local if it is preserved by simultaneous principal localization, passes from a map R_f → A to the composite R → A_a, and can be checked on a finite principal open cover of the target.

structure StacksPropertyIsLocal
    (P : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop) : Prop

Declarations registered for the tag:

Tag 01SS, a definition

Tag 01SS in the Stacks Project.

AlgebraicGeometry.locallyOfType, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/Defs.lean, line 109.

A morphism of schemes is locally of type P if every point of its source lies in an affine open mapping into an affine open of the target on whose rings of sections the induced homomorphism satisfies P.

abbrev locallyOfType (P : ∀ {R S : Type u} [CommRing R] [CommRing S],
    (R →+* S) → Prop) : MorphismProperty Scheme.{u}
Tag 01ST, a lemma

Tag 01ST in the Stacks Project.

AlgebraicGeometry.appLE_of_locallyOfType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/LocallyOfType.lean, line 149.

If f is locally of type P for a local property P, then P holds for the ring map 𝒪_S(V) → 𝒪_X(U) of any affine opens U ⊆ X, V ⊆ S with f(U) ⊆ V.

theorem appLE_of_locallyOfType (hP : RingHom.StacksPropertyIsLocal P) {f : X ⟶ S}
    (hf : locallyOfType P f) (V : S.affineOpens) (U : X.affineOpens) (e : U.1 ≤ f ⁻¹ᵁ V.1) :
    P (f.appLE V U e).hom
Tag 01SU, a lemma

Tag 01SU in the Stacks Project.

AlgebraicGeometry.locallyOfType_resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/LocallyOfType.lean, line 158. The attribute's comment: “moreover: restriction to open subschemes”.

If f is locally of type P for a local property P, then so is its restriction U → V to any opens U ⊆ X, V ⊆ S with f(U) ⊆ V.

theorem locallyOfType_resLE (hP : RingHom.StacksPropertyIsLocal P) {f : X ⟶ S}
    (hf : locallyOfType P f) (V : S.Opens) (U : X.Opens) (e : U ≤ f ⁻¹ᵁ V) :
    locallyOfType P (f.resLE V U e)

AlgebraicGeometry.locallyOfType_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/LocallyOfType.lean, line 167. The attribute's comment: “equivalence of (1), (2), (3) and (4)”.

For a local property P, being locally of type P can be checked on all pairs of affine opens, on open coverings of target and preimages, or on affine such coverings.

theorem locallyOfType_tfae (hP : RingHom.StacksPropertyIsLocal P) (f : X ⟶ S) :
    List.TFAE [
      locallyOfType P f,
      ∀ (V : S.affineOpens) (U : X.affineOpens) (e : U.1 ≤ f ⁻¹ᵁ V.1), P (f.appLE V U e).hom,
      ∃ 𝒱 : Set S.Opens, sSup 𝒱 = ⊤ ∧ ∀ V ∈ 𝒱, ∃ 𝒰 : Set X.Opens, sSup 𝒰 = f ⁻¹ᵁ V ∧
        ∀ U ∈ 𝒰, ∃ e : U ≤ f ⁻¹ᵁ V, locallyOfType P (f.resLE V U e),
      ∃ 𝒱 : Set S.affineOpens, (⨆ V ∈ 𝒱, V.1) = ⊤ ∧ ∀ V ∈ 𝒱, ∃ 𝒰 : Set X.affineOpens,
        (⨆ U ∈ 𝒰, U.1) = f ⁻¹ᵁ V.1 ∧ ∀ U ∈ 𝒰, ∃ e : U.1 ≤ f ⁻¹ᵁ V.1, P (f.appLE V U e).hom]

AlgebraicGeometry.locallyOfType_tfae_and_resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/LocallyOfType.lean, line 226.

The whole statement: for a local property P, the four characterizations of being locally of type P agree, and being locally of type P passes to restrictions to open subschemes.

theorem locallyOfType_tfae_and_resLE (hP : RingHom.StacksPropertyIsLocal P) (f : X ⟶ S) :
    List.TFAE [
      locallyOfType P f,
      ∀ (V : S.affineOpens) (U : X.affineOpens) (e : U.1 ≤ f ⁻¹ᵁ V.1), P (f.appLE V U e).hom,
      ∃ 𝒱 : Set S.Opens, sSup 𝒱 = ⊤ ∧ ∀ V ∈ 𝒱, ∃ 𝒰 : Set X.Opens, sSup 𝒰 = f ⁻¹ᵁ V ∧
        ∀ U ∈ 𝒰, ∃ e : U ≤ f ⁻¹ᵁ V, locallyOfType P (f.resLE V U e),
      ∃ 𝒱 : Set S.affineOpens, (⨆ V ∈ 𝒱, V.1) = ⊤ ∧ ∀ V ∈ 𝒱, ∃ 𝒰 : Set X.affineOpens,
        (⨆ U ∈ 𝒰, U.1) = f ⁻¹ᵁ V.1 ∧ ∀ U ∈ 𝒰, ∃ e : U.1 ≤ f ⁻¹ᵁ V.1, P (f.appLE V U e).hom] ∧
    (locallyOfType P f → ∀ (U : X.Opens) (V : S.Opens) (e : U ≤ f ⁻¹ᵁ V),
      locallyOfType P (f.resLE V U e))
Tag 01SV, a lemma

Tag 01SV in the Stacks Project.

AlgebraicGeometry.locallyOfType_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/LocallyOfType.lean, line 241.

For a local property P stable under composition, a composition of morphisms locally of type P is locally of type P.

theorem locallyOfType_comp (hP : RingHom.StacksPropertyIsLocal P)
    (hPc : RingHom.StableUnderComposition P) {X Y Z : Scheme.{u}} {f : X ⟶ Y} {g : Y ⟶ Z}
    (hf : locallyOfType P f) (hg : locallyOfType P g) : locallyOfType P (f ≫ g)
Tag 01SW, a lemma

Tag 01SW in the Stacks Project.

Declarations registered for the tag:

Tag 01SX, a lemma

Tag 01SX in the Stacks Project.

RingHom.isOpenImmersion_localizationAwayPreserves, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/AffineOpenImmersionNotLocal.lean, line 118. The attribute's comment: “part (2) (open immersion), locality condition (1)(a) of 01SR only: the criterion is preserved by simultaneous principal localization. Part (2) itself is false; see not_stacksPropertyIsLocal_isOpenImmersion”.

Locality condition (1)(a): the affine open-immersion criterion is preserved by simultaneous principal localization. This is base change along R → R_r.

theorem isOpenImmersion_localizationAwayPreserves :
    RingHom.LocalizationAwayPreserves
      (fun {R A : Type u} [CommRing R] [CommRing A] (φ : R →+* A) ↦ φ.IsOpenImmersion)

RingHom.isOpenImmersion_compPrincipalLocalizations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/AffineOpenImmersionNotLocal.lean, line 128. The attribute's comment: “part (2) (open immersion), locality condition (1)(b) of 01SR only: P (R_f → A) ⟹ P (R → A_a). Part (2) itself is false; see not_stacksPropertyIsLocal_isOpenImmersion”.

Locality condition (1)(b): if R_f → A satisfies the affine open-immersion criterion then so does the induced composite R → A_a.

theorem isOpenImmersion_compPrincipalLocalizations
    {R A Rf Aa : Type u} [CommRing R] [CommRing A] [CommRing Rf] [CommRing Aa] (f : R) (a : A)
    [Algebra R Rf] [IsLocalization.Away f Rf] [Algebra A Aa] [IsLocalization.Away a Aa]
    (g : Rf →+* A) (hg : g.IsOpenImmersion) :
    ((algebraMap A Aa).comp (g.comp (algebraMap R Rf))).IsOpenImmersion

RingHom.not_ofLocalizationFiniteSpanTarget_isOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/AffineOpenImmersionNotLocal.lean, line 231. The attribute's comment: “refutation of part (2) (open immersion): locality condition (1)(c) of 01SR fails for the criterion, the witness being the diagonal k → k × k of a field, whose two localizations at the coordinate idempotents are bijective while the diagonal itself is not a principal localization”.

The affine open-immersion criterion does not descend from a finite principal open cover of the target: this is the third locality condition of RingHom.StacksPropertyIsLocal.

theorem not_ofLocalizationFiniteSpanTarget_isOpenImmersion :
    ¬ RingHom.OfLocalizationFiniteSpanTarget
      (fun {R S : Type u} [CommRing R] [CommRing S] (φ : R →+* S) ↦ φ.IsOpenImmersion)

RingHom.not_stacksPropertyIsLocal_isOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/AffineOpenImmersionNotLocal.lean, line 244. The attribute's comment: “refutation of part (2) (open immersion): the criterion is NOT a local property of ring maps, so part (2) is false as stated. Conditions (1)(a) and (1)(b) of 01SR do hold and are the two carriers above; (1)(c) fails by not_ofLocalizationFiniteSpanTarget_isOpenImmersion. Parts (1), (3), (4) and (5) of the tag are true and carried in LocalRingIso, ReducedFibers, FiberDimension and NoetherianTarget”.

The affine open-immersion criterion is not a local property of commutative-ring homomorphisms.

theorem not_stacksPropertyIsLocal_isOpenImmersion :
    ¬ RingHom.StacksPropertyIsLocal
      (fun {R S : Type u} [CommRing R] [CommRing S] (φ : R →+* S) ↦ φ.IsOpenImmersion)

RingHom.fiberDimensionLE_propertyIsLocal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/FiberDimension.lean, line 127. The attribute's comment: “fibre_dimension_bound_is_local”.

A uniform bound on the Krull dimensions of the fibres is a local property of commutative-ring homomorphisms.

theorem fiberDimensionLE_propertyIsLocal (n : ℕ) :
    RingHom.StacksPropertyIsLocal
      (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) =>
        letI : Algebra R S := f.toAlgebra
        ∀ (p : Ideal R) [p.IsPrime], ringKrullDim (p.Fiber S) ≤ (n : WithBot ℕ∞))

RingHom.localRingHom_bijective_propertyIsLocal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/LocalRingIso.lean, line 230. The attribute's comment: “isomorphism_on_local_rings_is_local”.

Having isomorphisms on the local rings at every prime of the target is a local property of ring homomorphisms.

theorem localRingHom_bijective_propertyIsLocal :
    RingHom.StacksPropertyIsLocal
      (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
        ∀ (q : Ideal S) [q.IsPrime],
          Function.Bijective
            (Localization.localRingHom (Ideal.comap f q) q f rfl))

RingHom.noetherianTarget_propertyIsLocal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/NoetherianTarget.lean, line 37. The attribute's comment: “noetherian_target_is_local”.

Having Noetherian target is local for commutative-ring homomorphisms.

theorem noetherianTarget_propertyIsLocal :
    RingHom.StacksPropertyIsLocal
      (fun {R S : Type u} [CommRing R] [CommRing S] (_ : R →+* S) =>
        IsNoetherianRing S)

RingHom.reducedFibers_propertyIsLocal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/ReducedFibers.lean, line 152. The attribute's comment: “reduced_fibres_is_local”.

Having reduced fibres is local for ring homomorphisms.

theorem reducedFibers_propertyIsLocal :
    RingHom.StacksPropertyIsLocal (fun f => RingHom.ReducedFibers f)
Tag 01SY, a lemma

Tag 01SY in the Stacks Project.

RingHom.isOpenImmersion_isStableUnderBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/AffineOpenImmersion.lean, line 229. The attribute's comment: “open_immersion_base_change”. References: EGA I (4.3.2), “affine open immersions”; EGA I (4.5.5), “(iii), special case”; SGA 1 VIII (5.5), “special case”.

The principal-localization criterion for an affine open immersion is stable under arbitrary base change of commutative rings.

theorem isOpenImmersion_isStableUnderBaseChange :
    RingHom.IsStableUnderBaseChange
      (fun {R A : Type u} [CommRing R] [CommRing A] (φ : R →+* A) =>
        φ.IsOpenImmersion)

RingHom.localRingHom_bijective_isStableUnderBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/LocalRingIso.lean, line 368. The attribute's comment: “local_rings_base_change”.

Isomorphisms on local rings at every prime of the target are preserved by arbitrary base change of commutative rings.

theorem localRingHom_bijective_isStableUnderBaseChange :
    RingHom.IsStableUnderBaseChange
      (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
        ∀ (q : Ideal S) [q.IsPrime],
          Function.Bijective
            (Localization.localRingHom (Ideal.comap f q) q f rfl))
Tag 01SZ, a lemma

Tag 01SZ in the Stacks Project.

RingHom.isOpenImmersion_stableUnderComposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/AffineOpenImmersion.lean, line 268. The attribute's comment: “open_immersion_composition”.

Being an isomorphism on some principal neighborhood of each target prime is stable under composition of commutative-ring homomorphisms.

theorem isOpenImmersion_stableUnderComposition :
    RingHom.StableUnderComposition
      (fun {R S : Type u} [CommRing R] [CommRing S] (φ : R →+* S) ↦
        φ.IsOpenImmersion)

RingHom.localRingHom_bijective_stableUnderComposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/LocalRingIso.lean, line 381. The attribute's comment: “local_rings_composition”.

The property that all induced maps on local rings are isomorphisms is stable under composition.

theorem localRingHom_bijective_stableUnderComposition :
    RingHom.StableUnderComposition
      (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
        ∀ (q : Ideal S) [q.IsPrime],
          Function.Bijective
            (Localization.localRingHom (Ideal.comap f q) q f rfl))

RingHom.noetherianTarget_stableUnderComposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/NoetherianTarget.lean, line 54. The attribute's comment: “noetherian_target_composition”.

Having Noetherian target is stable under composition of commutative-ring homomorphisms.

theorem noetherianTarget_stableUnderComposition : RingHom.StableUnderComposition
    (fun {R S : Type u} [CommRing R] [CommRing S] (_ : R →+* S) => IsNoetherianRing S)
Sources
LeanRingHom.StacksPropertyIsLocal · RingHom.IsStableUnderBaseChange · RingHom.StableUnderComposition · AlgebraicGeometry.locallyOfType · AlgebraicGeometry.appLE_of_locallyOfType · AlgebraicGeometry.locallyOfType_resLE · AlgebraicGeometry.locallyOfType_tfae · AlgebraicGeometry.locallyOfType_tfae_and_resLE

Section29.15 Morphisms of finite type#

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

Tag 01T1, a definition

Tag 01T1 in the Stacks Project.

AlgebraicGeometry.finiteTypeAt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteTypePoint.lean, line 70. The attribute's comment: “part (1)”. References: EGA IV (1.3.2), “finite type at x”.

A morphism of schemes is of finite type at x if it induces a finite-type ring map on some affine open neighbourhood of x mapping into an affine open of the target.

def finiteTypeAt {X Y : Scheme.{u}} (f : X ⟶ Y) (x : X) : Prop

Declarations registered for the tag:

Tag 01T2, a lemma

Tag 01T2 in the Stacks Project.

Declarations registered for the tag:

Tag 01T3, a lemma

Tag 01T3 in the Stacks Project.

Declarations registered for the tag:

Tag 01T4, a lemma

Tag 01T4 in the Stacks Project.

Declarations registered for the tag:

Tag 01T5, a lemma

Tag 01T5 in the Stacks Project.

Declarations registered for the tag:

Tag 01T6, a lemma

Tag 01T6 in the Stacks Project.

Declarations registered for the tag:

Tag 01T7, a lemma

Tag 01T7 in the Stacks Project.

AlgebraicGeometry.quasiSeparated_of_locallyOfFiniteType, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteType/LocallyNoetherian.lean, line 34.

A morphism locally of finite type over a locally Noetherian scheme is quasi-separated.

instance quasiSeparated_of_locallyOfFiniteType {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [IsLocallyNoetherian S] : QuasiSeparated f
Tag 01T8, a lemma

Tag 01T8 in the Stacks Project.

AlgebraicGeometry.LocallyOfFiniteType.of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/FiniteTypeLocalAtSource.lean, line 103. References: EGA IV (1.3.4).

Stacks Project, Tag 01T8. If a composite of morphisms of schemes is locally of finite type, then so is its first factor.

theorem LocallyOfFiniteType.of_comp {X Y Z : Scheme.{u}} {f : X ⟶ Y} {g : Y ⟶ Z}
    (h : LocallyOfFiniteType (f ≫ g)) : LocallyOfFiniteType f
Sources
LeanAlgebraicGeometry.finiteTypeAt · AlgebraicGeometry.LocallyOfFiniteType · AlgebraicGeometry.QuasiCompact · AlgebraicGeometry.locallyOfFiniteType_iff · AlgebraicGeometry.locallyOfFiniteType_comp · AlgebraicGeometry.quasiCompact_comp · AlgebraicGeometry.locallyOfFiniteType_isStableUnderBaseChange · AlgebraicGeometry.quasiCompact_isStableUnderBaseChange

Section29.16 Points of finite type and Jacobson schemes#

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

Tag 01TA, a lemma

Tag 01TA in the Stacks Project.

AlgebraicGeometry.finiteType_specField_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteType/SpecField.lean, line 136.

Stacks Project, Tag 01TA. For a morphism from the spectrum of a field, being of finite type, being locally of finite type, admitting a finite affine coordinate-ring map around its image, and having closed image with finite residue field extension are equivalent.

theorem finiteType_specField_tfae {k : Type u} [Field k] {S : Scheme.{u}}
    (f : Spec (.of k) ⟶ S) :
    List.TFAE [
      LocallyOfFiniteType f ∧ QuasiCompact f,
      LocallyOfFiniteType f,
      ∃ (U : S.affineOpens)
          (hU : (⊤ : (Spec (.of k)).Opens) ≤ f ⁻¹ᵁ U.1),
        ((f.appLE U ⊤ hU) ≫ (Scheme.ΓSpecIso (.of k)).hom).hom.Finite,
      ∃ (U : S.affineOpens)
          (_hU : (⊤ : (Spec (.of k)).Opens) ≤ f ⁻¹ᵁ U.1)
          (x : U.1),
        (x : S) = ((Scheme.SpecToEquivOfField k S) f).1 ∧
          IsClosed ({x} : Set U.1) ∧
          letI := ((Scheme.SpecToEquivOfField k S) f).2.hom.toAlgebra
          Module.Finite (S.residueField ((Scheme.SpecToEquivOfField k S) f).1) k]
Tag 02HV, a lemma

Tag 02HV in the Stacks Project.

AlgebraicGeometry.finiteType_iff_residueField_comp_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteType/ArtinianLocalRing.lean, line 43.

A morphism from the spectrum of an Artinian local ring is of finite type if and only if its composite with the spectrum of the residue field is of finite type.

theorem finiteType_iff_residueField_comp_finiteType
    (S : Scheme.{u}) (A : Type u) [CommRing A] [IsLocalRing A] [IsArtinianRing A]
    (f : Spec (CommRingCat.of A) ⟶ S) :
    (LocallyOfFiniteType f ∧ QuasiCompact f) ↔
      (LocallyOfFiniteType
          (Spec.map (CommRingCat.ofHom (IsLocalRing.residue A)) ≫ f) ∧
        QuasiCompact
          (Spec.map (CommRingCat.ofHom (IsLocalRing.residue A)) ≫ f))
Tag 02J1, a definition

Tag 02J1 in the Stacks Project.

AlgebraicGeometry.IsFiniteTypePoint, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteTypePoint.lean, line 108. The attribute's comment: “finite_type_point”.

A point s of a scheme S is a finite type point if the canonical morphism Spec(κ(s)) ⟶ S is of finite type.

public abbrev IsFiniteTypePoint {S : AlgebraicGeometry.Scheme.{u}} (s : S) : Prop

AlgebraicGeometry.Scheme.finiteTypePoints, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/JacobsonPoints/Basic.lean, line 71. The attribute's comment: “finite_type_points_set”.

The set of finite type points of a scheme.

abbrev Scheme.finiteTypePoints (S : Scheme.{u}) : Set S
Tag 02J2, a lemma

Tag 02J2 in the Stacks Project.

AlgebraicGeometry.Scheme.finiteTypePoints_eq_iUnion_closedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/JacobsonPoints/Basic.lean, line 276.

The set of finite type points of a scheme S is the union, over the open subschemes U of S, of the sets of closed points of U; the same union taken over the affine open subschemes of S has the same value.

theorem Scheme.finiteTypePoints_eq_iUnion_closedPoints (S : Scheme.{u}) :
    S.finiteTypePoints = (⋃ U : S.Opens, Subtype.val '' closedPoints ↑U) ∧
      S.finiteTypePoints = ⋃ U : S.affineOpens, Subtype.val '' closedPoints ↑U.1
Tag 02J3, a lemma

Tag 02J3 in the Stacks Project.

AlgebraicGeometry.mapsTo_finiteTypePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/JacobsonPoints/Basic.lean, line 110.

A locally finite type morphism of schemes sends finite type points to finite type points.

theorem mapsTo_finiteTypePoints {T S : Scheme.{u}} (f : T ⟶ S)
    [LocallyOfFiniteType f] :
    Set.MapsTo f.base T.finiteTypePoints S.finiteTypePoints
Tag 06EB, a lemma

Tag 06EB in the Stacks Project.

AlgebraicGeometry.image_finiteTypePoints_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/JacobsonPoints/Basic.lean, line 218.

A surjective morphism which is locally of finite type maps the finite type points of its source onto those of its target.

theorem image_finiteTypePoints_eq {T S : Scheme.{u}} (f : T ⟶ S)
    [LocallyOfFiniteType f] [Surjective f] :
    f.base '' T.finiteTypePoints = S.finiteTypePoints
Tag 02J4, a lemma

Tag 02J4 in the Stacks Project.

AlgebraicGeometry.inter_finiteTypePoints_nonempty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/JacobsonPoints/Basic.lean, line 157. The attribute's comment: “locally closed subsets”.

Every nonempty locally closed subset of a scheme contains a finite type point.

theorem inter_finiteTypePoints_nonempty {S : Scheme.{u}} {T : Set S}
    (hT : IsLocallyClosed T) (hne : T.Nonempty) :
    (T ∩ S.finiteTypePoints).Nonempty

AlgebraicGeometry.closure_inter_finiteTypePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/JacobsonPoints/Basic.lean, line 200. The attribute's comment: “closed subsets”.

The finite type points lying in a closed subset of a scheme are dense in that subset.

theorem closure_inter_finiteTypePoints {S : Scheme.{u}} {T : Set S}
    (hT : IsClosed T) : closure (T ∩ S.finiteTypePoints) = T
Tag 01TB, a lemma

Tag 01TB in the Stacks Project.

AlgebraicGeometry.isFiniteTypePoint_of_isClosed_singleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteTypePoint.lean, line 119. The attribute's comment: “closed points are finite type points”.

A closed point of a scheme is a finite type point: the morphism from the spectrum of its residue field is a closed immersion (AlgebraicGeometry.isClosed_singleton_iff_isClosedImmersion), hence both locally of finite type and quasi-compact.

public theorem isFiniteTypePoint_of_isClosed_singleton {X : Scheme.{u}} {x : X}
    (hx : IsClosed ({x} : Set X)) : IsFiniteTypePoint x

AlgebraicGeometry.jacobsonSpace_finiteTypePoints_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/JacobsonPoints/Tfae.lean, line 45. References: EGA IV (10.4.7), “(1) => (3)”; EGA IV (10.9.2), “more general”.

A scheme is Jacobson exactly when its finite type points are its closed points; equivalently, closed points under every locally finite type morphism to it have closed image, and the induced residue field extensions are finite.

public theorem jacobsonSpace_finiteTypePoints_tfae (S : Scheme.{u}) :
    List.TFAE [
      JacobsonSpace S,
      S.finiteTypePoints = {s | IsClosed ({s} : Set S)},
      ∀ (T : Scheme.{u}) (f : T ⟶ S) [LocallyOfFiniteType f] (t : T),
        IsClosed ({t} : Set T) → IsClosed ({f t} : Set S),
      ∀ (T : Scheme.{u}) (f : T ⟶ S) [LocallyOfFiniteType f] (t : T),
        IsClosed ({t} : Set T) → (
          IsClosed ({f t} : Set S) ∧
            letI := (f.residueFieldMap t).hom.toAlgebra
            Module.Finite (S.residueField (f t)) (T.residueField t))]
Tag 02J5, a lemma

Tag 02J5 in the Stacks Project.

Declarations registered for the tag:

Tag 02J6, a lemma

Tag 02J6 in the Stacks Project.

AlgebraicGeometry.jacobsonSpace_of_locallyOfFiniteType_over_integers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/JacobsonPoints/Jacobson.lean, line 67. The attribute's comment: “over_integers”. References: EGA IV (10.4.7), “base = Spec Z”; EGA IV (10.4.6), “over Z”; EGA IV (10.4.9), “over Z”; EGA IV (10.7.1), “1° over Z”.

A scheme locally of finite type over the integers is Jacobson.

theorem jacobsonSpace_of_locallyOfFiniteType_over_integers {X : Scheme.{u}}
    (f : X ⟶ ⊤_ Scheme.{u}) [LocallyOfFiniteType f] : JacobsonSpace X

AlgebraicGeometry.jacobsonSpace_of_locallyOfFiniteType_over_oneDimensionalNoetherianDomain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/JacobsonPoints/Jacobson.lean, line 81. The attribute's comment: “over_dimension_one_domain”. References: EGA IV (10.4.7), “1-dim Noeth domain base”; EGA IV (10.7.1), “special case”.

A scheme locally of finite type over a one-dimensional Noetherian domain with infinitely many prime ideals is Jacobson.

theorem jacobsonSpace_of_locallyOfFiniteType_over_oneDimensionalNoetherianDomain
    (A : Type u) [CommRing A] [IsDomain A] [IsNoetherianRing A]
    (hdim : ringKrullDim A = 1) (hprimes : {p : Ideal A | p.IsPrime}.Infinite)
    {X : Scheme.{u}} (f : X ⟶ Spec (.of A)) [LocallyOfFiniteType f] :
    JacobsonSpace X

AlgebraicGeometry.jacobsonSpace_puncturedSpectrum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/JacobsonPoints/Jacobson.lean, line 108. The attribute's comment: “part (4): the punctured spectrum itself, R Noetherian local”. References: EGA IV (10.4.7), “punctured spectrum base”; EGA IV (10.5.7), “special case”.

The punctured spectrum Spec R \ {𝔪} of a Noetherian local ring R is a Jacobson scheme.

theorem jacobsonSpace_puncturedSpectrum (R : Type u) [CommRing R] [IsLocalRing R]
    [IsNoetherianRing R] :
    JacobsonSpace (Stacks.Divisors.puncturedSpectrum R).toScheme

AlgebraicGeometry.jacobsonSpace_of_locallyOfFiniteType_over_puncturedSpectrum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/JacobsonPoints/Jacobson.lean, line 117. The attribute's comment: “part (4): schemes lft over the punctured spectrum, R Noetherian local”. References: EGA IV (10.4.7), “punctured spectrum base”; EGA IV (10.5.7), “special case”.

A scheme locally of finite type over the punctured spectrum of a Noetherian local ring is Jacobson.

theorem jacobsonSpace_of_locallyOfFiniteType_over_puncturedSpectrum
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    {X : Scheme.{u}} (f : X ⟶ (Stacks.Divisors.puncturedSpectrum R).toScheme)
    [LocallyOfFiniteType f] : JacobsonSpace X

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.finiteType_specField_tfae · AlgebraicGeometry.finiteType_iff_residueField_comp_finiteType · AlgebraicGeometry.IsFiniteTypePoint · AlgebraicGeometry.Scheme.finiteTypePoints · AlgebraicGeometry.Scheme.finiteTypePoints_eq_iUnion_closedPoints · AlgebraicGeometry.mapsTo_finiteTypePoints · AlgebraicGeometry.image_finiteTypePoints_eq · AlgebraicGeometry.inter_finiteTypePoints_nonempty

Section29.17 Universally catenary schemes#

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

Tag 02J8, a definition

Tag 02J8 in the Stacks Project.

AlgebraicGeometry.Scheme.IsUniversallyCatenary, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteType/UniversallyCatenary.lean, line 56.

A locally Noetherian scheme S is universally catenary if every scheme locally of finite type over S is catenary.

def IsUniversallyCatenary (S : Scheme.{u}) [IsLocallyNoetherian S] : Prop
Tag 02J9, a lemma

Tag 02J9 in the Stacks Project.

AlgebraicGeometry.Scheme.isUniversallyCatenary_of_locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteType/UniversallyCatenary.lean, line 75. The attribute's comment: “inheritance”. References: EGA IV (10.6.1), “(i), condition 2° for X”.

A scheme locally of finite type over a locally Noetherian universally catenary scheme is universally catenary.

theorem isUniversallyCatenary_of_locallyOfFiniteType
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] [IsLocallyNoetherian S]
    (hS : IsUniversallyCatenary S) :
    @IsUniversallyCatenary X
      (AlgebraicGeometry.LocallyOfFiniteType.isLocallyNoetherian f)

AlgebraicGeometry.Scheme.isUniversallyCatenary_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RecoveryCatenary/LocalCriteria.lean, line 44. The attribute's comment: “local_criteria”.

For a locally Noetherian scheme, universal catenarity is equivalent to holding on an open covering, to universal catenarity of the ring of sections over every affine open, and to that ring-theoretic condition holding over the members of one affine open covering.

theorem isUniversallyCatenary_tfae (S : Scheme.{u}) [IsLocallyNoetherian S] :
    List.TFAE [
      IsUniversallyCatenary S,
      ∃ (ι : Type u) (U : ι → S.Opens),
        IsOpenCover U ∧ ∀ i, IsUniversallyCatenary (U i).toScheme,
      ∀ U : S.affineOpens, Ring.IsUniversallyCatenary Γ(S, U),
      ∃ (ι : Type u) (U : ι → S.affineOpens),
        IsOpenCover (fun i ↦ (U i : S.Opens)) ∧
          ∀ i, Ring.IsUniversallyCatenary Γ(S, U i)]
Tag 02JA, a lemma

Tag 02JA in the Stacks Project.

AlgebraicGeometry.Scheme.isUniversallyCatenary_iff_stalk_isUniversallyCatenary, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RecoveryCatenary/Stalk.lean, line 110. References: EGA IV (5.6.3).

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

theorem isUniversallyCatenary_iff_stalk_isUniversallyCatenary
    (S : Scheme.{u}) [IsLocallyNoetherian S] :
    IsUniversallyCatenary S ↔
      ∀ s : S, Ring.IsUniversallyCatenary (S.presheaf.stalk s)
Tag 0G42, a lemma

Tag 0G42 in the Stacks Project.

AlgebraicGeometry.Scheme.isUniversallyCatenary_iff_irreducibleComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RecoveryCatenary/IrreducibleComponents.lean, line 92.

A locally Noetherian scheme is universally catenary if and only if its reduced irreducible components are universally catenary.

theorem isUniversallyCatenary_iff_irreducibleComponents
    (S : Scheme.{u}) [IsLocallyNoetherian S] :
    IsUniversallyCatenary S ↔
      ∀ Z : irreducibleComponents S,
        let I : S.IdealSheafData := Scheme.IdealSheafData.vanishingIdeal
          ⟨Z.1, isClosed_of_mem_irreducibleComponents Z.1 Z.2⟩
        let : IsLocallyNoetherian I.subscheme :=
          LocallyOfFiniteType.isLocallyNoetherian I.subschemeι
        IsUniversallyCatenary I.subscheme
Tag 02JB, a lemma

Tag 02JB in the Stacks Project.

AlgebraicGeometry.Scheme.isUniversallyCatenary_of_locallyOfFiniteType_over_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteType/UniversallyCatenaryExamples.lean, line 217. The attribute's comment: “part (1)”. References: EGA IV (10.7.1), “2° over a field”.

Stacks Project, Tag 02JB, part (1). A scheme locally of finite type over a field is universally catenary.

theorem isUniversallyCatenary_of_locallyOfFiniteType_over_field (k : Type u) [Field k]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f] :
    @IsUniversallyCatenary X (LocallyOfFiniteType.isLocallyNoetherian f)

AlgebraicGeometry.Scheme.isUniversallyCatenary_of_locallyOfFiniteType_over_isCohenMacaulay, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteType/UniversallyCatenaryExamples.lean, line 229. The attribute's comment: “part (2)”. References: EGA IV (10.6.1), “(i), special case”; EGA IV (10.7.1), “more general”; EGA IV (5.2.5), “more general”; SGA 6 X (1.5), “more general”.

Stacks Project, Tag 02JB, part (2). A scheme locally of finite type over a locally Noetherian Cohen–Macaulay scheme is universally catenary.

theorem isUniversallyCatenary_of_locallyOfFiniteType_over_isCohenMacaulay {X S : Scheme.{u}}
    (f : X ⟶ S) [LocallyOfFiniteType f] [IsLocallyNoetherian S] (hS : IsCohenMacaulay S) :
    @IsUniversallyCatenary X (LocallyOfFiniteType.isLocallyNoetherian f)

AlgebraicGeometry.Scheme.isUniversallyCatenary_of_locallyOfFiniteType_over_int, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteType/UniversallyCatenaryExamples.lean, line 249. The attribute's comment: “part (3)”. References: EGA IV (10.6.1), “(i), special case”; EGA IV (10.7.1), “2° over Z”.

Stacks Project, Tag 02JB, part (3). A scheme locally of finite type over the integers is universally catenary. The base is Spec (ULift ℤ), the terminal scheme of the ambient universe, so this is the statement for a scheme in an arbitrary universe.

theorem isUniversallyCatenary_of_locallyOfFiniteType_over_int {X : Scheme.{u}}
    (f : X ⟶ Spec (.of (ULift.{u} ℤ))) [LocallyOfFiniteType f] :
    @IsUniversallyCatenary X (LocallyOfFiniteType.isLocallyNoetherian f)

AlgebraicGeometry.Scheme.isUniversallyCatenary_of_locallyOfFiniteType_over_dimOneDomain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteType/UniversallyCatenaryExamples.lean, line 258. The attribute's comment: “part (4)”.

Stacks Project, Tag 02JB, part (4). A scheme locally of finite type over a one-dimensional Noetherian domain is universally catenary.

theorem isUniversallyCatenary_of_locallyOfFiniteType_over_dimOneDomain (A : Type u) [CommRing A]
    [IsNoetherianRing A] [IsDomain A] (hA : ringKrullDim A = 1) {X : Scheme.{u}}
    (f : X ⟶ Spec (.of A)) [LocallyOfFiniteType f] :
    @IsUniversallyCatenary X (LocallyOfFiniteType.isLocallyNoetherian f)
Sources
LeanAlgebraicGeometry.Scheme.IsUniversallyCatenary · AlgebraicGeometry.Scheme.isUniversallyCatenary_of_locallyOfFiniteType · AlgebraicGeometry.Scheme.isUniversallyCatenary_tfae · AlgebraicGeometry.Scheme.isUniversallyCatenary_iff_stalk_isUniversallyCatenary · AlgebraicGeometry.Scheme.isUniversallyCatenary_iff_irreducibleComponents · AlgebraicGeometry.Scheme.isUniversallyCatenary_of_locallyOfFiniteType_over_field · AlgebraicGeometry.Scheme.isUniversallyCatenary_of_locallyOfFiniteType_over_isCohenMacaulay · AlgebraicGeometry.Scheme.isUniversallyCatenary_of_locallyOfFiniteType_over_int

Section29.18 Nagata schemes, reprise#

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

Tag 035A, a lemma

Tag 035A in the Stacks Project.

AlgebraicGeometry.isUniversallyJapaneseScheme_of_locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteType/UniversallyJapanese.lean, line 42. The attribute's comment: “universally_japanese”. References: EGA IV (7.7.2), “finite type stability”.

Stacks Project, Tag 035A (universally Japanese case). The source of a locally finite type morphism to a universally Japanese scheme is universally Japanese.

public theorem isUniversallyJapaneseScheme_of_locallyOfFiniteType {X S : Scheme.{u}}
    (f : X ⟶ S) [LocallyOfFiniteType f] (hS : IsUniversallyJapaneseScheme S) :
    IsUniversallyJapaneseScheme X

AlgebraicGeometry.isNagataScheme_of_locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NagataNormalization/FiniteType.lean, line 51. The attribute's comment: “nagata”. References: EGA IV (7.7.2), “finite type stability”.

Stacks Project, Tag 035A (Nagata case). The source of a locally finite type morphism to a Nagata scheme is Nagata.

theorem isNagataScheme_of_locallyOfFiniteType {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (hS : IsNagataScheme S) : IsNagataScheme X
Tag 035B, a lemma

Tag 035B in the Stacks Project.

AlgebraicGeometry.isNagataScheme_of_locallyOfFiniteType_over_isPrecomplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NagataNormalization/Examples.lean, line 64. The attribute's comment: “(2) A scheme locally of finite type over a Noetherian complete local ring; completeness is IsPrecomplete (IsLocalRing.maximalIdeal R) R, the hypothesis of Tag 032W.”.

Stacks Project, Tag 035B (2). A scheme locally of finite type over a Noetherian complete local ring is a Nagata scheme: such a ring is Nagata by Tag 032W.

theorem isNagataScheme_of_locallyOfFiniteType_over_isPrecomplete (R : Type u) [CommRing R]
    [IsNoetherianRing R] [IsLocalRing R] [IsPrecomplete (IsLocalRing.maximalIdeal R) R]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) [LocallyOfFiniteType f] : IsNagataScheme X

AlgebraicGeometry.isNagataScheme_of_locallyOfFiniteType_over_int, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NagataNormalization/Examples.lean, line 74. The attribute's comment: “(3) A scheme locally of finite type over ℤ, for the base Spec ℤ, which forces the source to live at universe 0; isNagataScheme_of_locallyOfFiniteType_over_uliftInt is the same statement for a source at an arbitrary universe.”.

Stacks Project, Tag 035B (3). A scheme locally of finite type over ℤ is a Nagata scheme: ℤ is a Nagata ring by Tag 0335 (3).

theorem isNagataScheme_of_locallyOfFiniteType_over_int {X : Scheme.{0}} (f : X ⟶ Spec (.of ℤ))
    [LocallyOfFiniteType f] : IsNagataScheme X

AlgebraicGeometry.isNagataScheme_of_locallyOfFiniteType_over_uliftInt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NagataNormalization/Examples.lean, line 82. The attribute's comment: “(3) A scheme locally of finite type over ℤ with the source at an arbitrary universe, the base being Spec (ULift ℤ), the terminal scheme.”.

Stacks Project, Tag 035B (3), at an arbitrary universe. A scheme locally of finite type over Spec (ULift ℤ), the terminal scheme, is a Nagata scheme.

theorem isNagataScheme_of_locallyOfFiniteType_over_uliftInt {X : Scheme.{u}}
    (f : X ⟶ Spec (.of (ULift.{u} ℤ))) [LocallyOfFiniteType f] : IsNagataScheme X

AlgebraicGeometry.isNagataScheme_of_locallyOfFiniteType_over_isDedekindDomain_of_charZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NagataNormalization/Examples.lean, line 92. The attribute's comment: “(4) A scheme locally of finite type over a Dedekind ring of characteristic zero, the characteristic condition read as CharZero R as in Tag 0335 (4).”.

Stacks Project, Tag 035B (4). A scheme locally of finite type over a Dedekind domain whose fraction field has characteristic zero is a Nagata scheme: such a ring is Nagata by Tag 0335 (4).

theorem isNagataScheme_of_locallyOfFiniteType_over_isDedekindDomain_of_charZero (R : Type u)
    [CommRing R] [IsDedekindDomain R] [CharZero R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R))
    [LocallyOfFiniteType f] : IsNagataScheme X

AlgebraicGeometry.isNagataScheme_of_locallyOfFiniteType_over_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NagataNormalization/FiniteType.lean, line 76. The attribute's comment: “field”.

Stacks Project, Tag 035B (field case). A scheme locally of finite type over a field is Nagata.

theorem isNagataScheme_of_locallyOfFiniteType_over_field (k : Type u) [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f] : IsNagataScheme X

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.isUniversallyJapaneseScheme_of_locallyOfFiniteType · AlgebraicGeometry.isNagataScheme_of_locallyOfFiniteType · AlgebraicGeometry.isNagataScheme_of_locallyOfFiniteType_over_isPrecomplete · AlgebraicGeometry.isNagataScheme_of_locallyOfFiniteType_over_int · AlgebraicGeometry.isNagataScheme_of_locallyOfFiniteType_over_uliftInt · AlgebraicGeometry.isNagataScheme_of_locallyOfFiniteType_over_isDedekindDomain_of_charZero · AlgebraicGeometry.isNagataScheme_of_locallyOfFiniteType_over_field · isNagataScheme_of_isNagataRing

Section29.19 The singular locus, reprise#

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

Tag 07R3, a definition

Tag 07R3 in the Stacks Project.

AlgebraicGeometry.Scheme.IsJ2, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/SingularLocus/JTwo.lean, line 54.

A locally Noetherian scheme X is J-2 if the regular locus of every scheme locally of finite type over X is open.

public def IsJ2 (X : Scheme.{u}) [IsLocallyNoetherian X] : Prop
Tag 07R4, a lemma

Tag 07R4 in the Stacks Project.

AlgebraicGeometry.Scheme.isJ2_Spec_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/SingularLocus/JTwoCriteria.lean, line 163. The attribute's comment: “the affine case”.

Stacks Project, Tag 07R4. On the spectrum of a Noetherian ring the scheme-theoretic J-2 condition is the ring-theoretic one.

public theorem isJ2_Spec_iff (R : Type u) [CommRing R] [IsNoetherianRing R] :
    IsJ2 (Spec (.of R)) ↔ _root_.IsJ2 R

AlgebraicGeometry.Scheme.isJ2_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SchemeJTwoLocal/JTwoTFAE.lean, line 136. The attribute's comment: “equivalent conditions”.

Stacks Project, Tag 07R4. For a locally Noetherian scheme, the J-2 condition is equivalent to holding on the members of an open covering, to the section ring of every affine open being J-2, and to that ring-theoretic condition holding on one affine open covering.

public theorem isJ2_tfae (X : Scheme.{u}) [IsLocallyNoetherian X] :
    List.TFAE [
      IsJ2 X,
      ∃ (I : Type u) (U : I → X.Opens),
        (⨆ i, U i) = ⊤ ∧ ∀ i, IsJ2 (U i).toScheme,
      ∀ U : X.affineOpens, _root_.IsJ2 Γ(X, U.1),
      ∃ (I : Type u) (U : I → X.affineOpens),
        (⨆ i, (U i).1) = ⊤ ∧ ∀ i, _root_.IsJ2 Γ(X, (U i).1)]

AlgebraicGeometry.Scheme.isJ2_of_locallyOfFiniteType', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SchemeJTwoLocal/JTwoTFAE.lean, line 173. The attribute's comment: “locally finite type schemes”.

Stacks Project, Tag 07R4. A scheme locally of finite type over a J-2 scheme is J-2. Local Noetherianity of the source is derived from that of the base rather than assumed.

public theorem isJ2_of_locallyOfFiniteType' {X Y : Scheme.{u}} [IsLocallyNoetherian X]
    (hX : IsJ2 X) (f : Y ⟶ X) [LocallyOfFiniteType f] :
    letI : IsLocallyNoetherian Y := LocallyOfFiniteType.isLocallyNoetherian f
    IsJ2 Y
Tag 07R5, a lemma

Tag 07R5 in the Stacks Project.

AlgebraicGeometry.Scheme.isJ2_of_locallyOfFiniteType_over_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/SingularLocus/JTwoStandardClasses.lean, line 61. The attribute's comment: “field_case”. References: EGA IV (6.12.6), “(ii), field base”; SGA 5 I (3.1.1), “field base”.

Stacks Project, Tag 07R5. A scheme locally of finite type over a field is J-2.

public theorem isJ2_of_locallyOfFiniteType_over_field (k : Type u) [Field k] {X : Scheme.{u}}
    [IsLocallyNoetherian X] (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f] : IsJ2 X

AlgebraicGeometry.Scheme.isJ2_of_locallyOfFiniteType_over_completeLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/SingularLocus/JTwoStandardClasses.lean, line 68. The attribute's comment: “complete_local_case”. References: EGA IV (6.12.8); SGA 5 I (3.1.1), “complete local base”.

Stacks Project, Tag 07R5. A scheme locally of finite type over a Noetherian complete local ring is J-2.

public theorem isJ2_of_locallyOfFiniteType_over_completeLocalRing (R : Type u) [CommRing R]
    [IsNoetherianRing R] [IsLocalRing R] [IsPrecomplete (IsLocalRing.maximalIdeal R) R]
    {X : Scheme.{u}} [IsLocallyNoetherian X] (f : X ⟶ Spec (.of R)) [LocallyOfFiniteType f] :
    IsJ2 X

AlgebraicGeometry.Scheme.isJ2_of_locallyOfFiniteType_over_int, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/SingularLocus/JTwoStandardClasses.lean, line 76. The attribute's comment: “integers_case”.

Stacks Project, Tag 07R5. A scheme locally of finite type over the integers is J-2.

public theorem isJ2_of_locallyOfFiniteType_over_int {X : Scheme.{0}} [IsLocallyNoetherian X]
    (f : X ⟶ Spec (.of ℤ)) [LocallyOfFiniteType f] : IsJ2 X

AlgebraicGeometry.Scheme.isJ2_of_locallyOfFiniteType_over_localRing_of_dim_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/SingularLocus/JTwoStandardClasses.lean, line 83. The attribute's comment: “local_dimension_one_case”.

Stacks Project, Tag 07R5. A scheme locally of finite type over a Noetherian local ring of dimension one is J-2.

public theorem isJ2_of_locallyOfFiniteType_over_localRing_of_dim_one (R : Type u) [CommRing R]
    [IsNoetherianRing R] [IsLocalRing R] (hR : ringKrullDim R = 1) {X : Scheme.{u}}
    [IsLocallyNoetherian X] (f : X ⟶ Spec (.of R)) [LocallyOfFiniteType f] : IsJ2 X

AlgebraicGeometry.Scheme.isJ2_of_locallyOfFiniteType_over_nagataRing_of_dim_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/SingularLocus/JTwoStandardClasses.lean, line 92. The attribute's comment: “nagata_dimension_one_case”.

Stacks Project, Tag 07R5. A scheme locally of finite type over a Nagata ring of dimension one is J-2.

public theorem isJ2_of_locallyOfFiniteType_over_nagataRing_of_dim_one (R : Type u) [CommRing R]
    [IsNagataRing R] (hR : ringKrullDim R = 1) {X : Scheme.{u}} [IsLocallyNoetherian X]
    (f : X ⟶ Spec (.of R)) [LocallyOfFiniteType f] : IsJ2 X

AlgebraicGeometry.Scheme.isJ2_of_locallyOfFiniteType_over_dedekindDomain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/SingularLocus/JTwoStandardClasses.lean, line 103. The attribute's comment: “dedekind_characteristic_zero_case”. References: EGA IV (6.12.6), “(i)”; SGA 5 I (3.1.1), “Dedekind char 0 base”.

Stacks Project, Tag 07R5. A scheme locally of finite type over a Dedekind domain of characteristic zero is J-2.

public theorem isJ2_of_locallyOfFiniteType_over_dedekindDomain (R : Type u) [CommRing R]
    [IsDedekindDomain R] [CharZero R] {X : Scheme.{u}} [IsLocallyNoetherian X]
    (f : X ⟶ Spec (.of R)) [LocallyOfFiniteType f] : IsJ2 X
Sources
LeanAlgebraicGeometry.Scheme.IsJ2 · AlgebraicGeometry.Scheme.isJ2_Spec_iff · AlgebraicGeometry.Scheme.isJ2_tfae · AlgebraicGeometry.Scheme.isJ2_of_locallyOfFiniteType' · AlgebraicGeometry.Scheme.isJ2_of_locallyOfFiniteType_over_field · AlgebraicGeometry.Scheme.isJ2_of_locallyOfFiniteType_over_completeLocalRing · AlgebraicGeometry.Scheme.isJ2_of_locallyOfFiniteType_over_int · AlgebraicGeometry.Scheme.isJ2_of_locallyOfFiniteType_over_localRing_of_dim_one

Section29.21 Quasi-finite morphisms#

Section 29.21 of the Stacks Project, Tag 01TC. 17 tags here are carried by 24 declarations of the repository (all in StacksFrontier) and 11 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01TD, a definition

Tag 01TD in the Stacks Project.

AlgebraicGeometry.quasiFiniteAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/Defs.lean, line 68. The attribute's comment: “part (1)”.

A morphism of schemes is quasi-finite at x if it is of finite type at x and its stalk map at x is quasi-finite.

public abbrev quasiFiniteAt {X S : Scheme.{u}} (f : X ⟶ S) (x : X) : Prop

AlgebraicGeometry.quasiFiniteAt_iff_exists_affineOpens, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/Defs.lean, line 75. The attribute's comment: “part (1), affine-neighbourhood characterization”.

Quasi-finiteness at a point is equivalently witnessed on compatible affine neighbourhoods by a finite-type ring map which is quasi-finite at the corresponding prime.

public theorem quasiFiniteAt_iff_exists_affineOpens
    {X S : Scheme.{u}} (f : X ⟶ S) (x : X) :
    quasiFiniteAt f x ↔
      ∃ (U : S.affineOpens) (V : X.affineOpens) (hxV : x ∈ V.1)
        (hVU : V.1 ≤ f ⁻¹ᵁ U.1),
        (f.appLE U V hVU).hom.FiniteType ∧
          (f.appLE U V hVU).hom.QuasiFiniteAt
            (V.2.primeIdealOf ⟨x, hxV⟩).asIdeal

AlgebraicGeometry.forall_quasiFiniteAt_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/Defs.lean, line 130. The attribute's comment: “part (2), pointwise characterization”.

A morphism is quasi-finite at every point exactly when it is locally of finite type and locally quasi-finite.

public theorem forall_quasiFiniteAt_iff {X S : Scheme.{u}} (f : X ⟶ S) :
    (∀ x, quasiFiniteAt f x) ↔
      (AlgebraicGeometry.LocallyOfFiniteType f ∧
        AlgebraicGeometry.LocallyQuasiFinite f)

AlgebraicGeometry.quasiFinite_conditions_iff_isDiscrete_fibers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/Defs.lean, line 154. The attribute's comment: “part (3), fiber characterization”.

The conditions defining a quasi-finite morphism can be expressed either by local quasi-finiteness or by discreteness of every set-theoretic fiber.

public theorem quasiFinite_conditions_iff_isDiscrete_fibers
    {X S : Scheme.{u}} (f : X ⟶ S) :
    ((LocallyOfFiniteType f ∧ QuasiCompact f) ∧ LocallyQuasiFinite f) ↔
      ((LocallyOfFiniteType f ∧ QuasiCompact f) ∧
        ∀ s, IsDiscrete (f ⁻¹' {s}))

Declarations registered for the tag:

Tag 01TE, a lemma

Tag 01TE in the Stacks Project.

AlgebraicGeometry.isClosed_asFiber_of_isAlgebraic_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/ResidueField.lean, line 56. The attribute's comment: “part (1)”.

A point whose residue field is algebraic over that of its image is closed in its fibre.

public theorem isClosed_asFiber_of_isAlgebraic_residueField (f : X ⟶ S) (x : X)
    (h : letI := (f.residueFieldMap x).hom.toAlgebra
      Algebra.IsAlgebraic (S.residueField (f x)) (X.residueField x)) :
    IsClosed ({f.asFiber x} : Set (f.fiber (f x)))

AlgebraicGeometry.isClosed_of_isAlgebraic_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/ResidueField.lean, line 97. The attribute's comment: “part (2)”. References: EGA I (6.4.2), “sufficiency”.

If the image of a point is closed and its residue field extension is algebraic, then the point is closed.

public theorem isClosed_of_isAlgebraic_residueField (f : X ⟶ S) (x : X)
    (h : letI := (f.residueFieldMap x).hom.toAlgebra
      Algebra.IsAlgebraic (S.residueField (f x)) (X.residueField x))
    (hs : IsClosed ({f x} : Set S)) : IsClosed ({x} : Set X)
Tag 01TF, a lemma

Tag 01TF in the Stacks Project.

AlgebraicGeometry.isClosed_asFiber_iff_finite_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/ResidueField.lean, line 109.

A point of a fibre of a locally finite type morphism is closed exactly when its residue field is finite over the residue field of its image.

public theorem isClosed_asFiber_iff_finite_residueField (f : X ⟶ S) [LocallyOfFiniteType f]
    (x : X) :
    IsClosed ({f.asFiber x} : Set (f.fiber (f x))) ↔
      letI := (f.residueFieldMap x).hom.toAlgebra
      Module.Finite (S.residueField (f x)) (X.residueField x)
Tag 053M, a lemma

Tag 053M in the Stacks Project.

AlgebraicGeometry.isClosed_asFiber_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/BaseChange.lean, line 269.

A point above a point closed in its fibre remains closed in its fibre after base change of a locally finite type morphism.

public theorem isClosed_asFiber_of_isPullback
    {X S S' X' : Scheme.{u}} {f : X ⟶ S} {g : S' ⟶ S}
    {f' : X' ⟶ S'} {g' : X' ⟶ X} [LocallyOfFiniteType f]
    (sq : IsPullback g' f' f g) (x' : X')
    (hx : IsClosed ({f.asFiber (g' x')} : Set (f.fiber (f (g' x'))))) :
    IsClosed ({f'.asFiber x'} : Set (f'.fiber (f' x')))
Tag 01TG, a lemma

Tag 01TG in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.finite_residueField_of_quasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/StalkDimension.lean, line 142. The attribute's comment: “the hypothesis is the stalk half Scheme.Hom.QuasiFiniteAt of AlgebraicGeometry.quasiFiniteAt, so the finite-type half is not used”.

At a point where a morphism of schemes is quasi-finite, the residue field of the source is a finite extension of the residue field of the image: the stalk map is quasi-finite, the residue field of the source is a quotient of the source stalk, and a quasi-finite algebra over a field is finite.

theorem Scheme.Hom.finite_residueField_of_quasiFiniteAt {X S : Scheme.{u}} (f : X ⟶ S) (x : X)
    (h : f.QuasiFiniteAt x) :
    letI := (f.residueFieldMap x).hom.toAlgebra
    Module.Finite (S.residueField (f x)) (X.residueField x)
Tag 01TH, a lemma

Tag 01TH in the Stacks Project.

AlgebraicGeometry.quasiFiniteAt_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/Criteria.lean, line 94. References: EGA II (6.2.2), “a) <=> c)”; EGA II (6.2.1).

Stacks Project, Tag 01TH. For a morphism locally of finite type, quasi-finiteness at a point is equivalent to isolation of that point in the fibre, to the corresponding closedness and specialization condition, and to quasi-finiteness at the corresponding prime for every compatible pair of affine open neighbourhoods.

public theorem quasiFiniteAt_tfae {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (x : X) :
    List.TFAE [
      quasiFiniteAt f x,
      IsIsolatedPoint (f.asFiber x),
      IsClosed ({f.asFiber x} : Set (f.fiber (f x))) ∧
        (¬ ∃ x' : f.fiber (f x),
          x' ≠ f.asFiber x ∧ x' ⤳ f.asFiber x),
      ∀ (U : S.affineOpens) (V : X.affineOpens) (hxV : x ∈ V.1)
        (hVU : V.1 ≤ f ⁻¹ᵁ U.1),
        (f.appLE U V hVU).hom.QuasiFiniteAt
          (V.2.primeIdealOf ⟨x, hxV⟩).asIdeal]
Tag 02NG, a lemma

Tag 02NG in the Stacks Project.

AlgebraicGeometry.finite_fiber_of_finite_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/FiniteFibre.lean, line 72. The attribute's comment: “the fibre is finite”.

Stacks Project, Tag 02NG. If the set-theoretic fibre of f over s is finite, then so is the scheme-theoretic fibre: the two are homeomorphic.

theorem finite_fiber_of_finite_preimage {X S : Scheme.{u}} (f : X ⟶ S) (s : S)
    (hfin : (f ⁻¹' {s}).Finite) : Finite (f.fiber s)

AlgebraicGeometry.discreteTopology_fiber_of_finite_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/FiniteFibre.lean, line 81. The attribute's comment: “the fibre is discrete”.

Stacks Project, Tag 02NG. A fibre of a morphism locally of finite type that is finite as a set is a discrete topological space: it is locally of finite type over the residue field at the base point, hence Jacobson, and a finite Jacobson space is discrete.

theorem discreteTopology_fiber_of_finite_preimage {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (s : S) (hfin : (f ⁻¹' {s}).Finite) :
    DiscreteTopology (f.fiber s)

AlgebraicGeometry.quasiFiniteAt_of_finite_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/FiniteFibre.lean, line 91. The attribute's comment: “quasi-finite at every point over the base point”.

Stacks Project, Tag 02NG. A morphism locally of finite type with finite fibre over s is quasi-finite at every point lying over s: the point is isolated in the fibre, because the fibre is discrete.

theorem quasiFiniteAt_of_finite_preimage {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (s : S) (hfin : (f ⁻¹' {s}).Finite) (x : X) (hx : f x = s) : quasiFiniteAt f x
Tag 01TJ, a lemma

Tag 01TJ in the Stacks Project.

Declarations registered for the tag:

Tag 02NH, a lemma

Tag 02NH in the Stacks Project.

AlgebraicGeometry.quasiFinite_conditions_iff_finite_fibers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/FiniteFibre.lean, line 100.

Stacks Project, Tag 02NH. A morphism of schemes is quasi-finite exactly when it is locally of finite type, quasi-compact and all of its set-theoretic fibres are finite.

theorem quasiFinite_conditions_iff_finite_fibers {X S : Scheme.{u}} (f : X ⟶ S) :
    ((LocallyOfFiniteType f ∧ QuasiCompact f) ∧ LocallyQuasiFinite f) ↔
      ((LocallyOfFiniteType f ∧ QuasiCompact f) ∧ ∀ s, (f ⁻¹' {s}).Finite)

AlgebraicGeometry.exists_isOpen_finite_preimage_inter_of_locallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedLocallyFiniteCharts.lean, line 49. The attribute's comment: “the preimage of a locally finite set under a locally quasi-finite morphism”.

Let f : X ⟶ Y be a morphism of schemes, locally of finite type and locally quasi-finite, and let Z be a set of points of Y such that every point of Y has an open neighbourhood meeting Z in a finite set. Then every point of X has an open neighbourhood meeting f⁻¹ Z in a finite set.

theorem exists_isOpen_finite_preimage_inter_of_locallyQuasiFinite {X Y : Scheme.{u}} (f : X ⟶ Y)
    [LocallyOfFiniteType f] [LocallyQuasiFinite f] {Z : Set Y}
    (hZ : ∀ y : Y, ∃ W : Y.Opens, y ∈ W ∧ (Z ∩ (W : Set Y)).Finite) (x : X) :
    ∃ Ω : X.Opens, x ∈ Ω ∧ (f.base ⁻¹' Z ∩ (Ω : Set X)).Finite
Tag 01TK, a lemma

Tag 01TK in the Stacks Project.

AlgebraicGeometry.locallyQuasiFinite_conditions_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/Defs.lean, line 186. The attribute's comment: “equivalence of (1), (2), (3) and (4)”.

Stacks Project, Tag 01TK. Local quasi-finiteness can be checked on all pairs of affine opens, on open coverings of the target and of the preimages, or on affine such coverings; on affine opens it is the condition that the ring map be quasi-finite, that is of finite type and quasi-finite at every prime.

public theorem locallyQuasiFinite_conditions_tfae {X S : Scheme.{u}} (f : X ⟶ S) :
    List.TFAE [
      LocallyOfFiniteType f ∧ LocallyQuasiFinite f,
      ∀ (V : S.affineOpens) (U : X.affineOpens) (e : U.1 ≤ f ⁻¹ᵁ V.1),
        (f.appLE V U e).hom.FiniteType ∧ (f.appLE V U e).hom.QuasiFinite,
      ∃ 𝒱 : Set S.Opens, sSup 𝒱 = ⊤ ∧ ∀ V ∈ 𝒱, ∃ 𝒰 : Set X.Opens, sSup 𝒰 = f ⁻¹ᵁ V ∧
        ∀ U ∈ 𝒰, ∃ e : U ≤ f ⁻¹ᵁ V,
          LocallyOfFiniteType (f.resLE V U e) ∧ LocallyQuasiFinite (f.resLE V U e),
      ∃ 𝒱 : Set S.affineOpens, (⨆ V ∈ 𝒱, V.1) = ⊤ ∧ ∀ V ∈ 𝒱, ∃ 𝒰 : Set X.affineOpens,
        (⨆ U ∈ 𝒰, U.1) = f ⁻¹ᵁ V.1 ∧ ∀ U ∈ 𝒰, ∃ e : U.1 ≤ f ⁻¹ᵁ V.1,
          (f.appLE V U e).hom.FiniteType ∧ (f.appLE V U e).hom.QuasiFinite]

AlgebraicGeometry.locallyQuasiFinite_conditions_resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/Defs.lean, line 252. The attribute's comment: “moreover: restriction to open subschemes”.

Stacks Project, Tag 01TK. If f is locally quasi-finite then so is its restriction U → V to any opens U ⊆ X, V ⊆ S with f(U) ⊆ V.

public theorem locallyQuasiFinite_conditions_resLE {X S : Scheme.{u}} {f : X ⟶ S}
    (hf : LocallyOfFiniteType f ∧ LocallyQuasiFinite f) (V : S.Opens) (U : X.Opens)
    (e : U ≤ f ⁻¹ᵁ V) :
    LocallyOfFiniteType (f.resLE V U e) ∧ LocallyQuasiFinite (f.resLE V U e)
Tag 01TL, a lemma

Tag 01TL in the Stacks Project.

AlgebraicGeometry.locallyQuasiFinite_conditions_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/Composition.lean, line 47. The attribute's comment: “locally quasi-finite morphisms”.

Stacks Project, Tag 01TL. The composition of two locally quasi-finite morphisms is locally quasi-finite.

theorem locallyQuasiFinite_conditions_comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
    [LocallyOfFiniteType f] [LocallyQuasiFinite f]
    [LocallyOfFiniteType g] [LocallyQuasiFinite g] :
    LocallyOfFiniteType (f ≫ g) ∧ LocallyQuasiFinite (f ≫ g)

AlgebraicGeometry.quasiFinite_conditions_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/Composition.lean, line 56. The attribute's comment: “quasi-finite morphisms”.

Stacks Project, Tag 01TL. The composition of two quasi-finite morphisms is quasi-finite.

theorem quasiFinite_conditions_comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
    [LocallyOfFiniteType f] [QuasiCompact f] [LocallyQuasiFinite f]
    [LocallyOfFiniteType g] [QuasiCompact g] [LocallyQuasiFinite g] :
    (LocallyOfFiniteType (f ≫ g) ∧ QuasiCompact (f ≫ g)) ∧ LocallyQuasiFinite (f ≫ g)
Tag 01TM, a lemma

Tag 01TM in the Stacks Project.

AlgebraicGeometry.quasiFiniteLocus_eq_preimage_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/BaseChange.lean, line 452. The attribute's comment: “part (1)”.

Stacks Project, Tag 01TM. In a cartesian square, the quasi-finite locus of the base-changed morphism is the inverse image of the quasi-finite locus of the original morphism.

public theorem quasiFiniteLocus_eq_preimage_of_isPullback {X S S' X' : Scheme.{u}} {f : X ⟶ S}
    {g : S' ⟶ S} {f' : X' ⟶ S'} {g' : X' ⟶ X} [LocallyOfFiniteType f]
    (sq : IsPullback g' f' f g) : quasiFiniteLocus f' = g' ⁻¹ᵁ quasiFiniteLocus f

Declarations registered for the tag:

Tag 0AAY, a lemma

Tag 0AAY in the Stacks Project.

AlgebraicGeometry.finite_setOf_mapsTo_and_quasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/Fibre.lean, line 51.

For a finite-type morphism of schemes, the set of points over a fixed point at which the morphism is quasi-finite is finite.

public theorem finite_setOf_mapsTo_and_quasiFiniteAt
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] [QuasiCompact f] (s : S) :
    {x : X | f x = s ∧ quasiFiniteAt f x}.Finite
Tag 0CT8, a lemma

Tag 0CT8 in the Stacks Project.

AlgebraicGeometry.isSeparated_and_locallyQuasiFinite_of_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/Monomorphism.lean, line 56.

A monomorphism of schemes which is locally of finite type is separated and locally quasi-finite.

theorem isSeparated_and_locallyQuasiFinite_of_mono {X Y : Scheme.{u}} (f : X ⟶ Y)
    [LocallyOfFiniteType f] [Mono f] :
    IsSeparated f ∧ LocallyQuasiFinite f
Tag 01TN, a lemma

Tag 01TN in the Stacks Project.

Declarations registered for the tag:

Tag 03WR, a lemma

Tag 03WR in the Stacks Project.

AlgebraicGeometry.quasiFiniteAt_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/Permanence.lean, line 115. The attribute's comment: “quasi-finite at a point”.

Stacks Project, Tag 03WR. If a composite is quasi-finite at a point of its source, then its first factor is quasi-finite there.

public theorem quasiFiniteAt_of_comp {X Y S : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ S)
    (x : X) (h : quasiFiniteAt (f ≫ g) x) :
    quasiFiniteAt f x

Declarations registered for the tag:

Tag 0GWS, a lemma

Tag 0GWS in the Stacks Project.

AlgebraicGeometry.locallyQuasiFinite_of_comp_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/Permanence.lean, line 169.

Stacks Project, Tag 0GWS. If f is surjective, f ≫ g is locally quasi-finite, and g is locally of finite type, then g is locally quasi-finite.

public theorem locallyQuasiFinite_of_comp_surjective
    {X Y S : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ S)
    [Surjective f]
    [LocallyOfFiniteType (f ≫ g)]
    [LocallyQuasiFinite (f ≫ g)]
    [LocallyOfFiniteType g] :
    LocallyQuasiFinite g
Sources
LeanAlgebraicGeometry.quasiFiniteAt · AlgebraicGeometry.quasiFiniteAt_iff_exists_affineOpens · AlgebraicGeometry.forall_quasiFiniteAt_iff · AlgebraicGeometry.quasiFinite_conditions_iff_isDiscrete_fibers · AlgebraicGeometry.LocallyOfFiniteType · AlgebraicGeometry.LocallyQuasiFinite · AlgebraicGeometry.QuasiCompact · AlgebraicGeometry.isClosed_asFiber_of_isAlgebraic_residueField

Section29.22 Morphisms of finite presentation#

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

Tag 01TP, a definition

Tag 01TP in the Stacks Project.

AlgebraicGeometry.FinitePresentationAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FinitePresentationPoint.lean, line 51. The attribute's comment: “part (1)”. References: EGA IV (1.4.2), “fin. presentation at x”.

A morphism of schemes is of finite presentation at x if it induces a ring map of finite presentation on some affine neighbourhood of x mapping into an affine open of the target.

public abbrev FinitePresentationAt {X S : Scheme.{u}} (f : X ⟶ S) (x : X) : Prop

AlgebraicGeometry.FinitePresentation, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FinitePresentationPoint.lean, line 62. The attribute's comment: “part (3)”.

A morphism of schemes is of finite presentation if it is locally of finite presentation, quasi-compact, and quasi-separated.

public abbrev FinitePresentation {X S : Scheme.{u}} (f : X ⟶ S) : Prop

Declarations registered for the tag:

Tag 01TQ, a lemma

Tag 01TQ in the Stacks Project.

AlgebraicGeometry.locallyOfFinitePresentation_resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/FinitePresentation.lean, line 74. The attribute's comment: “moreover: restriction to open subschemes”.

If f is locally of finite presentation then so is its restriction U → V to any opens U ⊆ X, V ⊆ S with f(U) ⊆ V.

theorem locallyOfFinitePresentation_resLE {f : X ⟶ S} (hf : LocallyOfFinitePresentation f)
    (V : S.Opens) (U : X.Opens) (e : U ≤ f ⁻¹ᵁ V) :
    LocallyOfFinitePresentation (f.resLE V U e)

AlgebraicGeometry.locallyOfFinitePresentation_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/FinitePresentation.lean, line 84. The attribute's comment: “equivalence of (1), (2), (3) and (4)”.

Being locally of finite presentation can be checked on all pairs of affine opens, on open coverings of target and preimages, or on affine such coverings.

theorem locallyOfFinitePresentation_tfae (f : X ⟶ S) :
    List.TFAE [
      LocallyOfFinitePresentation f,
      ∀ (V : S.affineOpens) (U : X.affineOpens) (e : U.1 ≤ f ⁻¹ᵁ V.1),
        (f.appLE V U e).hom.FinitePresentation,
      ∃ 𝒱 : Set S.Opens, sSup 𝒱 = ⊤ ∧ ∀ V ∈ 𝒱, ∃ 𝒰 : Set X.Opens, sSup 𝒰 = f ⁻¹ᵁ V ∧
        ∀ U ∈ 𝒰, ∃ e : U ≤ f ⁻¹ᵁ V, LocallyOfFinitePresentation (f.resLE V U e),
      ∃ 𝒱 : Set S.affineOpens, (⨆ V ∈ 𝒱, V.1) = ⊤ ∧ ∀ V ∈ 𝒱, ∃ 𝒰 : Set X.affineOpens,
        (⨆ U ∈ 𝒰, U.1) = f ⁻¹ᵁ V.1 ∧ ∀ U ∈ 𝒰, ∃ e : U.1 ≤ f ⁻¹ᵁ V.1,
          (f.appLE V U e).hom.FinitePresentation]

AlgebraicGeometry.locallyOfFinitePresentation_tfae_and_resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/RingMapProperty/FinitePresentation.lean, line 100.

The whole statement: the four characterizations of being locally of finite presentation agree, and being locally of finite presentation passes to restrictions to open subschemes.

theorem locallyOfFinitePresentation_tfae_and_resLE (f : X ⟶ S) :
    List.TFAE [
      LocallyOfFinitePresentation f,
      ∀ (V : S.affineOpens) (U : X.affineOpens) (e : U.1 ≤ f ⁻¹ᵁ V.1),
        (f.appLE V U e).hom.FinitePresentation,
      ∃ 𝒱 : Set S.Opens, sSup 𝒱 = ⊤ ∧ ∀ V ∈ 𝒱, ∃ 𝒰 : Set X.Opens, sSup 𝒰 = f ⁻¹ᵁ V ∧
        ∀ U ∈ 𝒰, ∃ e : U ≤ f ⁻¹ᵁ V, LocallyOfFinitePresentation (f.resLE V U e),
      ∃ 𝒱 : Set S.affineOpens, (⨆ V ∈ 𝒱, V.1) = ⊤ ∧ ∀ V ∈ 𝒱, ∃ 𝒰 : Set X.affineOpens,
        (⨆ U ∈ 𝒰, U.1) = f ⁻¹ᵁ V.1 ∧ ∀ U ∈ 𝒰, ∃ e : U.1 ≤ f ⁻¹ᵁ V.1,
          (f.appLE V U e).hom.FinitePresentation] ∧
    (LocallyOfFinitePresentation f → ∀ (U : X.Opens) (V : S.Opens) (e : U ≤ f ⁻¹ᵁ V),
      LocallyOfFinitePresentation (f.resLE V U e))
Tag 01TR, a lemma

Tag 01TR in the Stacks Project.

Declarations registered for the tag:

Tag 01TS, a lemma

Tag 01TS in the Stacks Project.

Declarations registered for the tag:

Tag 01TT, a lemma

Tag 01TT in the Stacks Project.

Declarations registered for the tag:

Tag 01TU, a lemma

Tag 01TU in the Stacks Project.

AlgebraicGeometry.finitePresentation_iff_quasiCompact_of_isOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/ImmersionsAndAffine/FinitePresentationOpenImmersion.lean, line 34. References: EGA IV (1.6.2).

Stacks Project, Tag 01TU. An open immersion is of finite presentation if and only if it is quasi-compact.

theorem finitePresentation_iff_quasiCompact_of_isOpenImmersion
    {X S : Scheme.{u}} (f : X ⟶ S) [IsOpenImmersion f] :
    FinitePresentation f ↔ QuasiCompact f
Tag 01TV, a lemma

Tag 01TV in the Stacks Project.

AlgebraicGeometry.finitePresentation_iff_fg_ker, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedImmersionFinitePresentation/Basic.lean, line 75. References: EGA IV (1.4.5), “closed immersion case”.

[Stacks Project, Tag 01TV]. A closed immersion is of finite presentation exactly when the associated quasi-coherent sheaf of ideals is of finite type, i.e. when its ideal over every affine open of the target is finitely generated.

Quasi-compactness and quasi-separatedness of a closed immersion hold unconditionally, so finite presentation asks nothing beyond local finite presentation here.

theorem finitePresentation_iff_fg_ker (f : X ⟶ Y) [IsClosedImmersion f] :
    FinitePresentation f ↔ ∀ U : Y.affineOpens, (f.ker.ideal U).FG
Tag 01TW, a lemma

Tag 01TW in the Stacks Project.

Declarations registered for the tag:

Tag 01TX, a lemma

Tag 01TX in the Stacks Project.

AlgebraicGeometry.finitePresentation_of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FinitePresentation/LocallyNoetherian.lean, line 52. The attribute's comment: “part (2)”.

Stacks Project, Tag 01TX, part (2). A morphism of finite type over a locally Noetherian scheme is of finite presentation.

theorem finitePresentation_of_finiteType {X S : Scheme.{u}} (f : X ⟶ S)
    [IsLocallyNoetherian S] [LocallyOfFiniteType f] [QuasiCompact f] :
    AlgebraicGeometry.FinitePresentation f

Declarations registered for the tag:

Tag 01TY, a lemma

Tag 01TY in the Stacks Project.

Declarations registered for the tag:

Tag 02FV, a lemma

Tag 02FV in the Stacks Project.

AlgebraicGeometry.locallyOfFinitePresentation_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FinitePresentation/Basic.lean, line 76. The attribute's comment: “part (1)”.

If X ⟶ S is locally of finite presentation and Y ⟶ S is locally of finite type, then a factor X ⟶ Y is locally of finite presentation.

theorem locallyOfFinitePresentation_of_comp {X Y S : Scheme.{u}}
    (f : X ⟶ Y) (g : Y ⟶ S) [LocallyOfFinitePresentation (f ≫ g)]
    [LocallyOfFiniteType g] : LocallyOfFinitePresentation f

AlgebraicGeometry.finitePresentation_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FinitePresentation/Basic.lean, line 87. The attribute's comment: “part (2)”.

If X ⟶ S is of finite presentation and Y ⟶ S is quasi-separated and locally of finite type, then a factor X ⟶ Y is of finite presentation.

theorem finitePresentation_of_comp {X Y S : Scheme.{u}}
    (f : X ⟶ Y) (g : Y ⟶ S) (hX : AlgebraicGeometry.FinitePresentation (f ≫ g))
    [QuasiSeparated g] [LocallyOfFiniteType g] :
    AlgebraicGeometry.FinitePresentation f
Tag 0818, a lemma

Tag 0818 in the Stacks Project.

AlgebraicGeometry.locallyOfFinitePresentation_diagonal, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FinitePresentation/Diagonal.lean, line 44. The attribute's comment: “local finite-presentation assertion”. References: EGA IV (17.4.1.2), “Delta loc. of fin. pres.”; EGA IV (1.4.3.1).

The diagonal of a morphism locally of finite type is locally of finite presentation.

lemma locallyOfFinitePresentation_diagonal {X Y : Scheme.{u}} (f : X ⟶ Y)
    [LocallyOfFiniteType f] : LocallyOfFinitePresentation (pullback.diagonal f)

AlgebraicGeometry.finitePresentation_diagonal, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FinitePresentation/Diagonal.lean, line 54. The attribute's comment: “finite-presentation assertion”. References: EGA IV (1.4.3.1), “special case”; EGA IV (17.4.1.2), “special case”.

The diagonal of a quasi-separated morphism locally of finite type is of finite presentation.

lemma finitePresentation_diagonal {X Y : Scheme.{u}} (f : X ⟶ Y)
    [QuasiSeparated f] [LocallyOfFiniteType f] :
    AlgebraicGeometry.FinitePresentation (pullback.diagonal f)
Sources
LeanAlgebraicGeometry.FinitePresentationAt · AlgebraicGeometry.FinitePresentation · AlgebraicGeometry.LocallyOfFinitePresentation · AlgebraicGeometry.locallyOfFinitePresentation_resLE · AlgebraicGeometry.locallyOfFinitePresentation_tfae · AlgebraicGeometry.locallyOfFinitePresentation_tfae_and_resLE · AlgebraicGeometry.locallyOfFinitePresentation_comp · AlgebraicGeometry.locallyOfFinitePresentation_isStableUnderBaseChange

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.