26.2 Locally ringed spaces to 26.20 Valuative criterion for…

Section26.2 Locally ringed spaces#

Section 26.2 of the Stacks Project, Tag 01HA. 2 tags here are carried by 6 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01HB, a definition

Tag 01HB in the Stacks Project.

Declarations registered for the tag:

Tag 01HC, a lemma

Tag 01HC in the Stacks Project.

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.LocallyRingedSpace · AlgebraicGeometry.LocallyRingedSpace.isLocalRing · AlgebraicGeometry.LocallyRingedSpace.residueField · AlgebraicGeometry.LocallyRingedSpace.Hom · AlgebraicGeometry.LocallyRingedSpace.isoOfSheafedSpaceIso · AlgebraicGeometry.LocallyRingedSpace.homOfSheafedSpaceHomOfIsIso

Section26.3 Open immersions of locally ringed spaces#

Section 26.3 of the Stacks Project, Tag 01HD. 5 tags here are carried by 13 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01HE, a definition

Tag 01HE in the Stacks Project.

Declarations registered for the tag:

Tag 01HF, an example

Tag 01HF in the Stacks Project.

Declarations registered for the tag:

Tag 01HG, a definition

Tag 01HG in the Stacks Project.

Declarations registered for the tag:

Tag 01HH, a lemma

Tag 01HH in the Stacks Project.

Declarations registered for the tag:

Tag 01HI, a lemma

Tag 01HI in the Stacks Project.

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion · AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso · AlgebraicGeometry.LocallyRingedSpace.restrict · AlgebraicGeometry.LocallyRingedSpace.ofRestrict · AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.ofRestrict · LocallyRingedSpace.restrict · LocallyRingedSpace.ofRestrict · LocallyRingedSpace.IsOpenImmersion.isoRestrict

Section26.4 Closed immersions of locally ringed spaces#

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

Tag 01HK, a definition

Tag 01HK in the Stacks Project.

Stacks.ClosedImmersion.IsClosedImmersion, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedImmersion/Defs.lean, line 69. The attribute's comment: “the same three conditions for a morphism of locally ringed spaces”.

Stacks Project, Tag 01C2. A morphism of ringed spaces is a closed immersion when its underlying continuous map is a closed embedding, its map on structure sheaves is surjective, and the kernel of that map is locally generated by sections.

class IsClosedImmersion {X Z : RingedSpace.{u, u}} (i : Z ⟶ X) : Prop
Tag 01HL, a lemma

Tag 01HL in the Stacks Project.

Stacks.ClosedImmersion.isClosedImmersion_of_iSup_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedImmersion/LocalAtTarget.lean, line 700. The attribute's comment: “stated for ringed spaces; the source states it for locally ringed spaces”.

Stacks Project, Tag 01HL. A morphism of ringed spaces whose restrictions over the members of an open covering of the target are closed immersions is itself a closed immersion.

This is the Stacks statement with locally ringed spaces relaxed to ringed spaces; see Stacks.ClosedImmersion.isClosedImmersion_toShHom_of_iSup_eq_top for the source's own formulation.

theorem isClosedImmersion_of_iSup_eq_top
    {X Z : RingedSpace.{u, u}} (f : Z ⟶ X) {ι : Type v} (U : ι → Opens X)
    (hU : ⨆ i, U i = ⊤)
    (hf : ∀ i, IsClosedImmersion (pullback.fst (X.ofRestrict (U i).isOpenEmbedding) f)) :
    IsClosedImmersion f

Stacks.ClosedImmersion.isClosedImmersion_toShHom_of_iSup_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedImmersion/LocalAtTarget.lean, line 755.

Stacks Project, Tag 01HL. Let f : Z ⟶ X be a morphism of locally ringed spaces. For f to be a closed immersion it suffices that there is an open covering X = ⋃ Uᵢ such that each f : f⁻¹ Uᵢ ⟶ Uᵢ is a closed immersion.

This is the source's formulation. It is the ringed-space statement Stacks.ClosedImmersion.isClosedImmersion_of_iSup_eq_top applied to the underlying morphism of ringed spaces, since being a closed immersion of locally ringed spaces is by definition the corresponding condition on that morphism.

theorem isClosedImmersion_toShHom_of_iSup_eq_top
    {X Z : LocallyRingedSpace.{u}} (f : Z ⟶ X) {ι : Type v} (U : ι → Opens X)
    (hU : ⨆ i, U i = ⊤)
    (hf : ∀ i, IsClosedImmersion
      (pullback.fst (X.toRingedSpace.ofRestrict (U i).isOpenEmbedding) f.toShHom)) :
    IsClosedImmersion f.toShHom
Tag 01HM, an example

Tag 01HM in the Stacks Project.

Stacks.ClosedImmersion.closedSubspace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedImmersion/ClosedSubspaceExistence.lean, line 1164. The attribute's comment: “the construction of the example: the subspace is the support of the quotient”.

The closed subspace associated to a locally generated sheaf of ideals on a locally ringed space.

public noncomputable def closedSubspace
    (J : SheafOfModules.{u} (structureSheafRing X.toRingedSpace))
    (j : J ⟶ SheafOfModules.unit (structureSheafRing X.toRingedSpace)) [Mono j]
    (hJ : Nonempty (SheafOfModules.LocalGeneratorsData.{u} J)) :
    ClosedSubspaceData X J j
Tag 01HN, a definition

Tag 01HN in the Stacks Project.

Stacks.ClosedImmersion.closedSubspace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedImmersion/ClosedSubspaceExistence.lean, line 1164.

The closed subspace associated to a locally generated sheaf of ideals on a locally ringed space.

public noncomputable def closedSubspace
    (J : SheafOfModules.{u} (structureSheafRing X.toRingedSpace))
    (j : J ⟶ SheafOfModules.unit (structureSheafRing X.toRingedSpace)) [Mono j]
    (hJ : Nonempty (SheafOfModules.LocalGeneratorsData.{u} J)) :
    ClosedSubspaceData X J j
Tag 01HO, a lemma

Tag 01HO in the Stacks Project.

Stacks.ClosedImmersion.existsUnique_iso_closedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ClosedImmersions/IsomorphismOfClosedSubspaces.lean, line 256.

A closed immersion is uniquely isomorphic over its target to the closed subspace defined by its ideal sheaf.

theorem existsUnique_iso_closedSubspace {X Y : LocallyRingedSpace.{u}} (f : X ⟶ Y)
    [hf : IsClosedImmersion f.toShHom] :
    let Z := closedSubspace Y (idealSheaf f.toShHom) (kernel.ι _) hf.kernel_locallyGenerated
    ∃! e : X ≅ Z.space, e.hom ≫ Z.inclusion = f
Tag 01HP, a lemma

Tag 01HP in the Stacks Project.

Stacks.ClosedImmersion.subsingleton_factorizations_closedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedImmersion/ClosedSubspace.lean, line 113. The attribute's comment: “uniqueness”.

Stacks Project, Tag 01HP. A factorization of a morphism of locally ringed spaces through the closed subspace associated to an ideal sheaf, when it exists, is unique.

theorem subsingleton_factorizations_closedSubspace {X' Y : LocallyRingedSpace.{u}}
    (J : SheafOfModules.{u} (structureSheafRing X'.toRingedSpace))
    (j : J ⟶ SheafOfModules.unit (structureSheafRing X'.toRingedSpace)) [Mono j]
    (D : ClosedSubspaceData X' J j) (f : Y ⟶ X') :
    Subsingleton {g : Y ⟶ D.space // g ≫ D.inclusion = f}

Stacks.ClosedImmersion.factorsThrough_closedSubspace_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ClosedImmersions/FactorizationExistence.lean, line 359. The attribute's comment: “factorization criterion”.

A morphism of locally ringed spaces factors through the closed subspace cut out by j exactly when the canonical map f^* J ⟶ 𝒪_Y vanishes.

theorem factorsThrough_closedSubspace_iff [Mono j] (D : ClosedSubspaceData X J j) (f : Y ⟶ X) :
    (∃ g : Y ⟶ D.space, g ≫ D.inclusion = f) ↔ pullbackIdealMap f J j = 0

Stacks.ClosedImmersion.factorsThrough_closedSubspace_of_localGenerators_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ClosedImmersions/FactorizationLocalGenerators.lean, line 50. The attribute's comment: “factorization criterion”.

A morphism f : Y ⟶ X of locally ringed spaces factors through the closed subspace cut out by a sheaf of ideals j : J ⟶ 𝒪_X which is locally generated by sections exactly when the canonical map f^* J ⟶ 𝒪_Y vanishes.

theorem factorsThrough_closedSubspace_of_localGenerators_iff {X Y : LocallyRingedSpace.{u}}
    (J : SheafOfModules.{u} (structureSheafRing X.toRingedSpace))
    (j : J ⟶ SheafOfModules.unit (structureSheafRing X.toRingedSpace)) [Mono j]
    (hJ : Nonempty (SheafOfModules.LocalGeneratorsData.{u} J)) (f : Y ⟶ X) :
    (∃ g : Y ⟶ (closedSubspace X J j hJ).space,
        g ≫ (closedSubspace X J j hJ).inclusion = f) ↔ pullbackIdealMap f J j = 0

Stacks.ClosedImmersion.subsingleton_factorizations_closedSubspace_of_localGenerators, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ClosedImmersions/FactorizationLocalGenerators.lean, line 61. The attribute's comment: “uniqueness”.

A factorization of a morphism of locally ringed spaces through the closed subspace cut out by a sheaf of ideals which is locally generated by sections, when it exists, is unique.

theorem subsingleton_factorizations_closedSubspace_of_localGenerators
    {X Y : LocallyRingedSpace.{u}}
    (J : SheafOfModules.{u} (structureSheafRing X.toRingedSpace))
    (j : J ⟶ SheafOfModules.unit (structureSheafRing X.toRingedSpace)) [Mono j]
    (hJ : Nonempty (SheafOfModules.LocalGeneratorsData.{u} J)) (f : Y ⟶ X) :
    Subsingleton {g : Y ⟶ (closedSubspace X J j hJ).space //
      g ≫ (closedSubspace X J j hJ).inclusion = f}
Tag 01HQ, a lemma

Tag 01HQ in the Stacks Project.

Stacks.ClosedImmersion.pullbackIdeal_locallyGenerated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ClosedImmersions/Pullback.lean, line 229. The attribute's comment: “local generation”.

Stacks Project, Tag 01HQ. The inverse-image ideal of a locally generated ideal sheaf is locally generated. Tag 01B3 gives local generators for the pullback f^* I, and the inverse-image ideal is a quotient of f^* I, so the images of those generators generate it.

theorem pullbackIdeal_locallyGenerated (I : SheafOfModules.{u} (structureSheafRing Y.toRingedSpace))
    (i : I ⟶ SheafOfModules.unit (structureSheafRing Y.toRingedSpace))
    (hI : Nonempty (SheafOfModules.LocalGeneratorsData.{u} I)) :
    Nonempty (SheafOfModules.LocalGeneratorsData.{u} (pullbackIdeal f I i))

Stacks.ClosedImmersion.restrictedMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ClosedImmersions/Pullback.lean, line 311. The attribute's comment: “restricted map”.

Stacks Project, Tag 01HQ. The morphism of closed subspaces induced by f.

noncomputable def restrictedMap (I : SheafOfModules.{u} (structureSheafRing Y.toRingedSpace))
    (i : I ⟶ SheafOfModules.unit (structureSheafRing Y.toRingedSpace)) [Mono i]
    (hI : Nonempty (SheafOfModules.LocalGeneratorsData.{u} I)) :
    (pullbackClosedSubspace f I i hI).space ⟶ (closedSubspace Y I i hI).space

Stacks.ClosedImmersion.restrictedMap_commutes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ClosedImmersions/Pullback.lean, line 320. The attribute's comment: “commutative square”.

Stacks Project, Tag 01HQ. The induced map commutes with the inclusions into the ambient spaces.

theorem restrictedMap_commutes (I : SheafOfModules.{u} (structureSheafRing Y.toRingedSpace))
    (i : I ⟶ SheafOfModules.unit (structureSheafRing Y.toRingedSpace)) [Mono i]
    (hI : Nonempty (SheafOfModules.LocalGeneratorsData.{u} I)) :
    restrictedMap f I i hI ≫ (closedSubspace Y I i hI).inclusion =
      (pullbackClosedSubspace f I i hI).inclusion ≫ f

Stacks.ClosedImmersion.restrictedMap_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ClosedImmersions/Pullback.lean, line 330. The attribute's comment: “uniqueness”.

Stacks Project, Tag 01HQ. A morphism between the associated closed subspaces over f is the induced one.

theorem restrictedMap_unique (I : SheafOfModules.{u} (structureSheafRing Y.toRingedSpace))
    (i : I ⟶ SheafOfModules.unit (structureSheafRing Y.toRingedSpace)) [Mono i]
    (hI : Nonempty (SheafOfModules.LocalGeneratorsData.{u} I))
    (g : (pullbackClosedSubspace f I i hI).space ⟶ (closedSubspace Y I i hI).space)
    (hg : g ≫ (closedSubspace Y I i hI).inclusion =
      (pullbackClosedSubspace f I i hI).inclusion ≫ f) :
    g = restrictedMap f I i hI

Stacks.ClosedImmersion.restrictedMap_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ClosedImmersions/Pullback.lean, line 345. The attribute's comment: “fibre square”.

Stacks Project, Tag 01HQ. The restriction square is a fibre square of locally ringed spaces.

theorem restrictedMap_isPullback (I : SheafOfModules.{u} (structureSheafRing Y.toRingedSpace))
    (i : I ⟶ SheafOfModules.unit (structureSheafRing Y.toRingedSpace)) [Mono i]
    (hI : Nonempty (SheafOfModules.LocalGeneratorsData.{u} I)) :
    IsPullback (pullbackClosedSubspace f I i hI).inclusion (restrictedMap f I i hI) f
      (closedSubspace Y I i hI).inclusion
Sources
LeanStacks.ClosedImmersion.IsClosedImmersion · Stacks.ClosedImmersion.isClosedImmersion_of_iSup_eq_top · Stacks.ClosedImmersion.isClosedImmersion_toShHom_of_iSup_eq_top · Stacks.ClosedImmersion.closedSubspace · Stacks.ClosedImmersion.existsUnique_iso_closedSubspace · Stacks.ClosedImmersion.subsingleton_factorizations_closedSubspace · Stacks.ClosedImmersion.factorsThrough_closedSubspace_iff · Stacks.ClosedImmersion.factorsThrough_closedSubspace_of_localGenerators_iff

Section26.5 Affine schemes#

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

Tag 01HS, a lemma

Tag 01HS in the Stacks Project.

Stacks.Cohomology.Cech.exists_isStandardOpenCoverOfSpectrum_refinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Cech/StandardCoverCofinality.lean, line 105. The attribute's comment: “part (2), for an affine open of a scheme”.

Any open covering of an affine open of a scheme is refined by a finite standard open covering of it. This is the scheme-level form of [Stacks, Tag 01HS] part (2), and it is condition (2) of [Stacks, Tag 01EW] for the system of finite standard open coverings of affine opens: the returned family g of sections over U satisfies the standard-covering condition of [Stacks, Tag 01HT], its ambient basic opens cover U, and each of them is contained in a member of the given family.

theorem exists_isStandardOpenCoverOfSpectrum_refinement {U : X.Opens} (hU : IsAffineOpen U)
    {ι : Type v} (W : ι → X.Opens) (hW : U ≤ ⨆ i, W i) :
    ∃ (n : ℕ) (g : Fin n → Γ(X, U)) (a : Fin n → ι),
      PrimeSpectrum.IsStandardOpenCoverOfSpectrum g ∧ (⨆ j, X.basicOpen (g j)) = U ∧
        ∀ j, X.basicOpen (g j) ≤ W (a j)

PrimeSpectrum.ringRestrictionMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Zariski/RestrictionMaps.lean, line 55. The attribute's comment: “ring_restriction_map”.

The canonical R-algebra map R_f → R_g attached to an inclusion D(g) ⊆ D(f).

noncomputable def ringRestrictionMap {R : Type u} [CommRing R] (f g : R)
    (hfg : PrimeSpectrum.basicOpen g ≤ PrimeSpectrum.basicOpen f) :
    Localization.Away f →ₐ[R] Localization.Away g

PrimeSpectrum.ringRestrictionMap_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Zariski/RestrictionMaps.lean, line 66. The attribute's comment: “ring_restriction_map”.

The restriction map is canonical: it is the unique R-algebra homomorphism from R_f to R_g.

theorem ringRestrictionMap_unique {R : Type u} [CommRing R] (f g : R)
    (hfg : PrimeSpectrum.basicOpen g ≤ PrimeSpectrum.basicOpen f)
    (φ : Localization.Away f →ₐ[R] Localization.Away g) :
    φ = ringRestrictionMap f g hfg

PrimeSpectrum.moduleRestrictionMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Zariski/RestrictionMaps.lean, line 76. The attribute's comment: “module_restriction_map”.

The canonical R_f-linear restriction map M_f → M_g associated to an inclusion D(g) ⊆ D(f).

noncomputable def moduleRestrictionMap {R : Type u} [CommRing R]
    {M : Type v} [AddCommGroup M] [Module R M] (f g : R)
    (hfg : PrimeSpectrum.basicOpen g ≤ PrimeSpectrum.basicOpen f) :
    let φ := ringRestrictionMap f g hfg
    letI := Module.compHom (R := Localization.Away g) (S := Localization.Away f)
      (LocalizedModule.Away (R := R) g M) φ.toRingHom
    LocalizedModule.Away (R := R) f M →ₗ[Localization.Away f]
      LocalizedModule.Away (R := R) g M

PrimeSpectrum.moduleRestrictionMap_mk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Zariski/RestrictionMaps.lean, line 118. The attribute's comment: “module_restriction_map”.

The module restriction map agrees with the canonical localization maps on elements of M.

theorem moduleRestrictionMap_mk {R : Type u} [CommRing R]
    {M : Type v} [AddCommGroup M] [Module R M] (f g : R)
    (hfg : PrimeSpectrum.basicOpen g ≤ PrimeSpectrum.basicOpen f) (m : M) :
    moduleRestrictionMap f g hfg
        (LocalizedModule.mkLinearMap (Submonoid.powers f) M m) =
      LocalizedModule.mkLinearMap (Submonoid.powers g) M m

PrimeSpectrum.moduleRestrictionMap_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Zariski/RestrictionMaps.lean, line 130. The attribute's comment: “module_restriction_map”.

An R_f-linear map M_f → M_g which agrees with the localization maps from M is the canonical module restriction map.

theorem moduleRestrictionMap_unique {R : Type u} [CommRing R]
    {M : Type v} [AddCommGroup M] [Module R M] (f g : R)
    (hfg : PrimeSpectrum.basicOpen g ≤ PrimeSpectrum.basicOpen f)
    (F :
      let φ := ringRestrictionMap f g hfg
      letI := Module.compHom (R := Localization.Away g) (S := Localization.Away f)
        (LocalizedModule.Away (R := R) g M) φ.toRingHom
      LocalizedModule.Away (R := R) f M →ₗ[Localization.Away f]
        LocalizedModule.Away (R := R) g M)
    (hF : ∀ m : M,
      F (LocalizedModule.mkLinearMap (Submonoid.powers f) M m) =
        LocalizedModule.mkLinearMap (Submonoid.powers g) M m) :
    F = moduleRestrictionMap f g hfg

PrimeSpectrum.basicOpen_le_iSup_iff_span_algebraMap_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Zariski/StandardOpenCover.lean, line 66. The attribute's comment: “cover_iff_unit_ideal”.

A standard open D(f) is contained in the union of the standard opens D(g i) if and only if the images of the g i generate the unit ideal after localizing away from f.

theorem basicOpen_le_iSup_iff_span_algebraMap_eq_top
    {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
    {ι : Type w} (f : R) [IsLocalization.Away f S] (g : ι → R) :
      PrimeSpectrum.basicOpen f ≤ ⨆ i, PrimeSpectrum.basicOpen (g i) ↔
      Ideal.span (Set.range fun i ↦ algebraMap R S (g i)) = ⊤

PrimeSpectrum.exists_finite_basicOpen_refinement, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Zariski/StandardOpenCover.lean, line 88. The attribute's comment: “finite_standard_refinement”.

Every open cover of a standard open in the prime spectrum has a finite refinement by standard opens.

lemma exists_finite_basicOpen_refinement {R : Type u} [CommSemiring R]
    {ι : Type*} (f : R) (U : ι → Opens (PrimeSpectrum R))
    (hU : PrimeSpectrum.basicOpen f ≤ ⨆ i, U i) :
    ∃ (n : ℕ) (g : Fin n → R) (a : Fin n → ι),
      PrimeSpectrum.basicOpen f = ⨆ j, PrimeSpectrum.basicOpen (g j) ∧
        ∀ j, PrimeSpectrum.basicOpen (g j) ≤ U (a j)

PrimeSpectrum.exists_pow_eq_mul_of_basicOpen_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Zariski/StandardOpenCover.lean, line 128. The attribute's comment: “power_divisible”. References: EGA I (1.1.9), “partial”.

If D(g) ⊆ D(f), a positive power of g is a multiple of f.

theorem exists_pow_eq_mul_of_basicOpen_le {R : Type*} [CommRing R] {f g : R}
    (hfg : PrimeSpectrum.basicOpen g ≤ PrimeSpectrum.basicOpen f) :
    ∃ e : ℕ, 1 ≤ e ∧ ∃ a : R, g ^ e = a * f

Declarations registered for the tag:

Tag 01HT, a definition

Tag 01HT in the Stacks Project.

PrimeSpectrum.IsStandardOpenCover, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Zariski/StandardOpenCover.lean, line 55. The attribute's comment: “part (2)”.

A family D(g i), indexed by Fin n, is a standard open covering of D(f) when its supremum is D(f).

def IsStandardOpenCover {R : Type u} [CommRing R] (f : R) {n : ℕ} (g : Fin n → R) : Prop

PrimeSpectrum.IsStandardOpenCoverOfSpectrum, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Zariski/StandardOpenCover.lean, line 60. The attribute's comment: “part (1)”.

A standard open covering of Spec R, expressed as the case D(1) = Spec R.

abbrev IsStandardOpenCoverOfSpectrum {R : Type u} [CommRing R] {n : ℕ} (g : Fin n → R) : Prop
Tag 01HU, a definition

Tag 01HU in the Stacks Project.

Declarations registered for the tag:

Tag 01HV, a lemma

Tag 01HV in the Stacks Project.

AlgebraicGeometry.tilde.basicOpen_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Affine/Functoriality.lean, line 146. The attribute's comment: “functorial_identifications”.

Under the canonical localization identifications, the map on sections over a standard open induced by a module map is its localization.

theorem basicOpen_map {R : CommRingCat.{u}} {M N : ModuleCat.{u} R}
    (f : M ⟶ N) (a : R) (m : LocalizedModule.Away (R := R) a M) :
    ((modulesSpecToSheaf.map (tilde.map f)).1.app
        (.op (PrimeSpectrum.basicOpen a)))
      ((IsLocalizedModule.iso (Submonoid.powers a)
        (tilde.toOpen M (PrimeSpectrum.basicOpen a)).hom) m) =
      (IsLocalizedModule.iso (Submonoid.powers a)
        (tilde.toOpen N (PrimeSpectrum.basicOpen a)).hom)
        (IsLocalizedModule.map (Submonoid.powers a)
          (LocalizedModule.mkLinearMap (Submonoid.powers a) M)
          (LocalizedModule.mkLinearMap (Submonoid.powers a) N) f.hom m)

AlgebraicGeometry.tilde.toStalk_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Affine/Functoriality.lean, line 179. The attribute's comment: “functorial_identifications”.

The canonical identification of the stalk of an associated sheaf with localization at a prime is natural in the module.

theorem toStalk_map {R : CommRingCat.{u}} {M N : ModuleCat.{u} R}
    (f : M ⟶ N) (x : PrimeSpectrum.Top R)
    (m : (tilde M).presheaf.stalk x) :
    ((TopCat.Presheaf.stalkFunctor Ab x).map
      (Scheme.Modules.Hom.mapPresheaf (tilde.map f))) m =
      IsLocalizedModule.map x.asIdeal.primeCompl
        (tilde.toStalk M x).hom (tilde.toStalk N x).hom f.hom m

AlgebraicGeometry.StructureSheaf.map_basicOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Affine/Sections.lean, line 74. The attribute's comment: “restriction_maps”.

Under the canonical identifications of sections on standard opens with localizations, restriction in the structure sheaf is the canonical map R_f → R_g.

theorem map_basicOpen {R : CommRingCat.{u}} (f g : R)
    (hfg : PrimeSpectrum.basicOpen g ≤ PrimeSpectrum.basicOpen f) :
    ((AlgebraicGeometry.Spec.structureSheaf R).obj.map (homOfLE hfg).op).hom.comp
        (IsLocalization.algEquiv (Submonoid.powers f) (Localization.Away f)
          ((AlgebraicGeometry.Spec.structureSheaf R).obj.obj
            (.op (PrimeSpectrum.basicOpen f)))).toRingHom =
      (IsLocalization.algEquiv (Submonoid.powers g) (Localization.Away g)
        ((AlgebraicGeometry.Spec.structureSheaf R).obj.obj
          (.op (PrimeSpectrum.basicOpen g)))).toRingHom.comp
        (PrimeSpectrum.ringRestrictionMap f g hfg).toRingHom

AlgebraicGeometry.tilde.map_basicOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Affine/Sections.lean, line 111. The attribute's comment: “restriction_maps”.

Sections of the associated sheaf on D(f) and D(g) are canonically isomorphic to M_f and M_g. The isomorphisms identify sheaf restriction with the canonical map M_f → M_g.

theorem map_basicOpen {R : CommRingCat.{u}} (M : ModuleCat.{u} R) (f g : R)
    (hfg : PrimeSpectrum.basicOpen g ≤ PrimeSpectrum.basicOpen f) :
    ∀ x : LocalizedModule.Away (R := R) f M,
      (modulesSpecToSheaf.obj (tilde M)).presheaf.map (homOfLE hfg).op
          ((IsLocalizedModule.iso (Submonoid.powers f)
            (tilde.toOpen M (PrimeSpectrum.basicOpen f)).hom) x) =
        (IsLocalizedModule.iso (Submonoid.powers g)
          (tilde.toOpen M (PrimeSpectrum.basicOpen g)).hom)
            (PrimeSpectrum.moduleRestrictionMap f g hfg x)

Declarations registered for the tag:

Tag 01HW, a definition

Tag 01HW in the Stacks Project.

Declarations registered for the tag:

Sources
LeanStacks.Cohomology.Cech.exists_isStandardOpenCoverOfSpectrum_refinement · PrimeSpectrum.ringRestrictionMap · PrimeSpectrum.ringRestrictionMap_unique · PrimeSpectrum.moduleRestrictionMap · PrimeSpectrum.moduleRestrictionMap_mk · PrimeSpectrum.moduleRestrictionMap_unique · PrimeSpectrum.basicOpen_le_iSup_iff_span_algebraMap_eq_top · PrimeSpectrum.exists_finite_basicOpen_refinement

Section26.6 The category of affine schemes#

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

Tag 01HY, a lemma

Tag 01HY in the Stacks Project.

AlgebraicGeometry.isoSpec_hom_base_apply_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/MorphismsToAffine.lean, line 215.

Let X be a locally ringed space, let Y be an affine scheme and let f : X ⟶ Y be a morphism of locally ringed spaces. Given x : X, consider the ring maps

Γ(Y, 𝒪_Y) --f^♯--> Γ(X, 𝒪_X) ⟶ 𝒪_{X,x}

and let p ⊆ Γ(Y, 𝒪_Y) be the inverse image of the maximal ideal m_x. Let y ∈ Y be the corresponding point. Then f x = y.

The point y of the affine scheme Y corresponding to a prime of Γ(Y, 𝒪_Y) is named by transporting along AlgebraicGeometry.Scheme.isoSpec, the identification of Y with Spec Γ(Y, 𝒪_Y): the statement here is that Y.isoSpec.hom sends f x to p, and AlgebraicGeometry.base_eq_isoSpec_inv_base_of_isAffine is the same thing written as f x = y. The prime p is spelled as the inverse image along f^♯ of the inverse image along Γ(X, 𝒪_X) ⟶ 𝒪_{X,x} of the maximal ideal, which is the inverse image along the composite.

theorem isoSpec_hom_base_apply_of_isAffine (X : LocallyRingedSpace.{u}) (Y : Scheme.{u})
    [IsAffine Y] (f : X ⟶ Y.toLocallyRingedSpace) (x : X) :
    Y.isoSpec.hom.base (f.base x) =
      PrimeSpectrum.comap (LocallyRingedSpace.Γ.map f.op).hom
        (PrimeSpectrum.comap (X.presheaf.Γgerm x).hom
          (IsLocalRing.closedPoint (X.presheaf.stalk x)))
Tag 01HZ, a lemma

Tag 01HZ in the Stacks Project.

Declarations registered for the tag:

Tag 01I0, a lemma

Tag 01I0 in the Stacks Project.

Declarations registered for the tag:

Tag 01I1, a lemma

Tag 01I1 in the Stacks Project.

AlgebraicGeometry.bijective_Γ_map_op_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/MorphismsToAffine.lean, line 146. References: EGA I (1.7.3), “more general”.

Let X be a locally ringed space and let Y be an affine scheme. The map

Mor(X, Y) ⟶ Hom(Γ(Y, 𝒪_Y), Γ(X, 𝒪_X))

sending a morphism to the ring map it induces on global sections is bijective.

The target is read as a locally ringed space, which is where the morphisms of the source live.

theorem bijective_Γ_map_op_of_isAffine (X : LocallyRingedSpace.{u}) (Y : Scheme.{u}) [IsAffine Y] :
    Function.Bijective (fun f : X ⟶ Y.toLocallyRingedSpace =>
      LocallyRingedSpace.Γ.map f.op)
Tag 01I2, a lemma

Tag 01I2 in the Stacks Project.

Declarations registered for the tag:

Tag 01I3, a lemma

Tag 01I3 in the Stacks Project.

Declarations registered for the tag:

Tag 01I4, a lemma

Tag 01I4 in the Stacks Project.

AlgebraicGeometry.AffineScheme.preservesLimits_forgetToLocallyRingedSpace, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Affine/FibreProductsLocallyRingedSpaces.lean, line 55. The attribute's comment: “limits agree with those of locally ringed spaces”.

The forgetful functor from affine schemes to locally ringed spaces preserves all limits: limits of affine schemes, in particular products and fibre products, are the same as those computed in locally ringed spaces.

instance preservesLimits_forgetToLocallyRingedSpace :
    PreservesLimits (forgetToScheme.{u} ⋙ Scheme.forgetToLocallyRingedSpace)

AlgebraicGeometry.LocallyRingedSpace.prodSpecIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Affine/FibreProductsLocallyRingedSpaces.lean, line 96. The attribute's comment: “products in locally ringed spaces”.

In the category of locally ringed spaces, Spec R × Spec S ≅ Spec (R ⊗[ℤ] S).

noncomputable def prodSpecIso :
    Spec.locallyRingedSpaceObj (.of R) ⨯ Spec.locallyRingedSpaceObj (.of S) ≅
      Spec.locallyRingedSpaceObj (.of (R ⊗[ℤ] S))

AlgebraicGeometry.LocallyRingedSpace.pullbackSpecIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Affine/FibreProductsLocallyRingedSpaces.lean, line 142. The attribute's comment: “fibre products in locally ringed spaces”.

In the category of locally ringed spaces, Spec A ×_{Spec R} Spec B ≅ Spec (A ⊗[R] B).

noncomputable def pullbackSpecIso :
    pullback (Spec.locallyRingedSpaceMap (ofHom (algebraMap R A)))
      (Spec.locallyRingedSpaceMap (ofHom (algebraMap R B))) ≅
      Spec.locallyRingedSpaceObj (.of (A ⊗[R] B))

Declarations registered for the tag:

Tag 01I5, a lemma

Tag 01I5 in the Stacks Project.

Stacks.ZariskiAndSeparation.AffineDisjointUnion.isAffine_of_sup_eq_top_of_disjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/AffineDisjointUnion.lean, line 39. The attribute's comment: “for a scheme; a locally ringed space with an affine open cover is one”.

A scheme covered by two disjoint affine opens is affine.

theorem isAffine_of_sup_eq_top_of_disjoint {X : Scheme.{u}} (U V : X.Opens)
    (hUV : U ⊔ V = ⊤) (hd : Disjoint U V) (hU : IsAffineOpen U) (hV : IsAffineOpen V) :
    IsAffine X
Sources
LeanAlgebraicGeometry.isoSpec_hom_base_apply_of_isAffine · RingedSpace.basicOpen · RingedSpace.mem_top_basicOpen · RingedSpace.isUnit_res_basicOpen · basicOpen_eq_of_affine · Scheme.toSpecΓ_preimage_basicOpen · AlgebraicGeometry.bijective_Γ_map_op_of_isAffine · AffineScheme.equivCommRingCat

Section26.7 Quasi-coherent sheaves on affines#

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

Tag 01I7, a lemma

Tag 01I7 in the Stacks Project.

AlgebraicGeometry.tildeAssociatedSheafNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/QuasiCoherentSheaves/Basic.lean, line 60. The attribute's comment: “canonical functorial comparison”. References: EGA I (1.8.6), “u = id on Spec R”.

The canonical comparison between the affine construction M ↦ M̃ on Spec R and tensor sheafification along R → Γ(Spec R, 𝒪): a natural isomorphism of the two functors, together with the equation that on global sections it sends m to 1 ⊗ m.

noncomputable def tildeAssociatedSheafNatIso (R : CommRingCat.{u}) :
    { e : tilde.functor R ≅
        associatedSheafFunctor (Spec R).toRingedSpace
          (Scheme.ΓSpecIso R).inv.hom //
      ∀ (M : ModuleCat R) (m : M),
        (e.hom.app M).val.app (op ⊤) (tilde.toOpen M ⊤ m) =
          tensorUnitSection (X := (Spec R).toRingedSpace)
            (Scheme.ΓSpecIso R).inv.hom M (op ⊤) m }

Declarations registered for the tag:

Tag 01I8, a lemma

Tag 01I8 in the Stacks Project.

Stacks.AffineExteriorPower.tildeExteriorPowerIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineExteriorPowerCompare/Basic.lean, line 51. The attribute's comment: “exterior_power”.

The affine exterior-power comparison. The associated sheaf of the n-th exterior power of M is the n-th exterior power of M̃.

def tildeExteriorPowerIso (n : ℕ) :
    (tilde (ModuleCat.of ↥R ↥(⋀[↥R]^n ↥M)) : SheafOfModules.{u} (Spec R).ringCatSheaf) ≅
      A.exteriorPower n

Stacks.AffineExteriorPower.tildeExteriorPowerIso_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineExteriorPowerCompare/Natural.lean, line 156. The attribute's comment: “exterior_power”.

The affine exterior-power comparison is natural. It respects every unital homomorphism of exterior algebra sheaves extending the map M̃ ⟶ Ñ of generating module sheaves on the degree-one generators; the universal property of the exterior algebra makes such a homomorphism unique, so this determines the degree-n square.

theorem tildeExteriorPowerIso_natural (n : ℕ)
    (A : SheafOfModules.TensorExteriorSymmetricAlgebras
      (Opens.grothendieckTopology ↥(Spec R)) (tilde M))
    (B : SheafOfModules.TensorExteriorSymmetricAlgebras
      (Opens.grothendieckTopology ↥(Spec R)) (tilde N))
    (g : SheafOfModules.GradedAlgebra.UnitalHom A.exterior B.exterior)
    (hg : A.exteriorGenerator ≫ g.app 1 = tilde.map f ≫ B.exteriorGenerator) :
    tilde.map (ModuleCat.ofHom (R := R)
          (X := ModuleCat.of ↥R ↥(⋀[↥R]^n ↥M)) (Y := ModuleCat.of ↥R ↥(⋀[↥R]^n ↥N))
          (exteriorPower.map n f.hom)) ≫ (tildeExteriorPowerIso N B n).hom =
      (tildeExteriorPowerIso M A n).hom ≫ g.app (n : ℤ)

Stacks.AffineExteriorPower.tildeExteriorPowerIso_hom_ιMulti, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineExteriorPowerCompare/Wedge.lean, line 163. The attribute's comment: “exterior_power”.

The affine exterior-power comparison on a wedge of global sections. The global section of (⋀ⁿ_R M)~ attached to m₁ ∧ ⋯ ∧ mₙ is carried to the ordered product, in ⋀(M̃), of the degree-one generators at the global sections of M̃ attached to the mᵢ.

theorem tildeExteriorPowerIso_hom_ιMulti
    (A : SheafOfModules.TensorExteriorSymmetricAlgebras
      (Opens.grothendieckTopology ↥(Spec R)) (tilde M)) (s : Fin n → ↥M) :
    (((tilde.adjunction (R := R)).homEquiv (ModuleCat.of ↥R ↥(⋀[↥R]^n ↥M))
          (A.exteriorPower n)) (tildeExteriorPowerIso M A n).hom).hom
        (exteriorPower.ιMulti ↥R n s) =
      A.exterior.toPresheafGradedAlgebra.homogeneousProd (specGlobalOpen R) n
        (fun i => A.exteriorGenerator.val.app (specGlobalOpen R)
          ((tilde.toOpen M ⊤).hom (s i)))

Stacks.SymGraded.tildeSymmetricPowerIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineSymmetricPowerCompare/Basic.lean, line 72. The attribute's comment: “symmetric_power”.

The affine symmetric-power comparison. The associated sheaf of the n-th symmetric power of M is the n-th symmetric power of M̃.

def tildeSymmetricPowerIso (n : ℕ) :
    (tilde (ModuleCat.of R (SymPow.symmetricPower n R M)) :
        SheafOfModules.{u} (Spec R).ringCatSheaf) ≅ A.symmetricPower n

Stacks.SymGraded.tildeSymmetricPowerIso_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineSymmetricPowerCompare/Basic.lean, line 124. The attribute's comment: “symmetric_power”.

In degree zero the comparison takes the algebraic unit to the unit of the symmetric algebra sheaf.

theorem tildeSymmetricPowerIso_unit :
    let x : SymPow.symmetricPower 0 R M := ⟨1, one_mem_gradedPiece (R := R) M⟩
    (((tilde.adjunction (R := R)).homEquiv
      (ModuleCat.of R (SymPow.symmetricPower 0 R M))
      (A.symmetricPower 0))
      (tildeSymmetricPowerIso M A 0).hom).hom x =
        A.symmetric.one.eval (.op (⊤ : Opens (Spec R).carrier))

Stacks.SymGraded.tildeSymmetricPowerIso_generator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineSymmetricPowerCompare/Basic.lean, line 144. The attribute's comment: “symmetric_power”.

In degree one the comparison takes an algebraic generator to the corresponding generator of the symmetric algebra sheaf.

theorem tildeSymmetricPowerIso_generator (m : M) :
    let x : SymPow.symmetricPower 1 R M :=
      ⟨SymmetricAlgebra.ι R M m, ι_mem_gradedPiece_one (R := R) M m⟩
    (((tilde.adjunction (R := R)).homEquiv
      (ModuleCat.of R (SymPow.symmetricPower 1 R M))
      (A.symmetricPower 1))
      (tildeSymmetricPowerIso M A 1).hom).hom x =
        (A.symmetricGenerator.val.app (.op (⊤ : Opens (Spec R).carrier)))
          ((tilde.toOpen M ⊤).hom m)

Stacks.SymGraded.tildeSymmetricPowerIso_mul_generator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineSymmetricPowerCompare/Mul.lean, line 99. The attribute's comment: “symmetric_power”.

The comparison in degree n + 1 takes multiplication by an algebraic degree-one generator to multiplication by the corresponding sheaf generator. Together with the degree-one normalization this fixes the canonical comparison in every degree.

theorem tildeSymmetricPowerIso_mul_generator (n : ℕ) (m : M)
    (x : SymPow.symmetricPower n R M) :
    HEq
      ((((tilde.adjunction (R := R)).homEquiv
        (ModuleCat.of R (SymPow.symmetricPower (n + 1) R M))
        (A.symmetricPower (n + 1)))
        (tildeSymmetricPowerIso M A (n + 1)).hom).hom
          (SymPow.symMulMap n (LinearMap.id : M →ₗ[R] M) (m ⊗ₜ[R] x)))
      ((A.symmetric.mul 1 (n : ℤ)).app (.op (⊤ : Opens (Spec R).carrier))
        (A.symmetricGenerator.val.app (.op (⊤ : Opens (Spec R).carrier))
          ((tilde.toOpen M ⊤).hom m))
        ((tildeSymmetricPowerIso M A n).hom.val.app (.op (⊤ : Opens (Spec R).carrier))
          ((tilde.toOpen (ModuleCat.of R (SymPow.symmetricPower n R M)) ⊤).hom x)))

Stacks.SymGraded.tildeSymmetricPowerIso_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineSymmetricPowerCompare/Natural.lean, line 58. The attribute's comment: “symmetric_power”.

The affine symmetric-power comparison is natural. It respects every unital homomorphism of symmetric algebra sheaves extending the map of generating module sheaves; the universal property of the symmetric algebra makes such a homomorphism unique.

theorem tildeSymmetricPowerIso_natural (n : ℕ)
    (A : SheafOfModules.TensorExteriorSymmetricAlgebras
      (Opens.grothendieckTopology ↥(Spec R)) (tilde M))
    (B : SheafOfModules.TensorExteriorSymmetricAlgebras
      (Opens.grothendieckTopology ↥(Spec R)) (tilde N))
    (g : SheafOfModules.GradedAlgebra.UnitalHom A.symmetric B.symmetric)
    (hg : A.symmetricGenerator ≫ g.app 1 = tilde.map f ≫ B.symmetricGenerator) :
    tilde.map (ModuleCat.ofHom (R := R)
          (X := ModuleCat.of R (SymPow.symmetricPower n R M))
          (Y := ModuleCat.of R (SymPow.symmetricPower n R N)) (SymPow.symMap n f.hom)) ≫
        (tildeSymmetricPowerIso N B n).hom =
      (tildeSymmetricPowerIso M A n).hom ≫ g.app (n : ℤ)

Stacks.SymGraded.tildeSymmetricPowerIso_natural_symMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineSymmetricPowerCompare/Natural.lean, line 129. The attribute's comment: “symmetric_power”.

The affine symmetric-power comparison is natural, for the canonical induced map. This is Stacks.SymGraded.tildeSymmetricPowerIso_natural instantiated at symmetricAlgebraHom, the unital homomorphism the universal property of the symmetric algebra provides, so that the square is stated against a canonical map rather than a hypothesised one. The left-hand map is the associated sheaf of SymPow.symMap, the n-th symmetric power of f.

theorem tildeSymmetricPowerIso_natural_symMap (n : ℕ)
    (A : SheafOfModules.TensorExteriorSymmetricAlgebras
      (Opens.grothendieckTopology ↥(Spec R)) (tilde M))
    (B : SheafOfModules.TensorExteriorSymmetricAlgebras
      (Opens.grothendieckTopology ↥(Spec R)) (tilde N)) :
    tilde.map (ModuleCat.ofHom (R := R)
          (X := ModuleCat.of R (SymPow.symmetricPower n R M))
          (Y := ModuleCat.of R (SymPow.symmetricPower n R N)) (SymPow.symMap n f.hom)) ≫
        (tildeSymmetricPowerIso N B n).hom =
      (tildeSymmetricPowerIso M A n).hom ≫ (symmetricAlgebraHom f A B).app (n : ℤ)

AlgebraicGeometry.InternalHomTildeIso, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Modules/AffineInternalHom.lean, line 104. The attribute's comment: “internal_hom”.

An isomorphism from an affine internal Hom to the associated sheaf of the module of linear maps, together with the characterization that makes the isomorphism canonical.

The inverse sends the global section associated to f : M ⟶ N to the section of the internal Hom represented by the sheaf morphism tilde.map f. This is the content of [Stacks, Tag 01I8].

structure InternalHomTildeIso (R : CommRingCat.{u}) (M N : ModuleCat.{u} R)
    (H : SheafHom (Spec R).sheaf (tilde M) (tilde N))

AlgebraicGeometry.internalHomTildeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Modules/AffineInternalHom.lean, line 121. The attribute's comment: “internal_hom”. References: EGA I (1.3.12), “(ii)”.

Stacks Project, Tag 01I8 (internal_hom).

Let M and N be modules over a commutative ring R, with M finitely presented. The internal Hom between the associated sheaves of M and N on Spec R is canonically isomorphic to the sheaf associated to the R-module Hom_R(M, N).

noncomputable def internalHomTildeIso (R : CommRingCat.{u})
    (M N : ModuleCat.{u} R)
    [Module.FinitePresentation R M]
    (H : SheafHom (Spec R).sheaf (tilde M) (tilde N)) :
    InternalHomTildeIso R M N H

AlgebraicGeometry.internalHomTildeIsoIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Modules/AffineInternalHom.lean, line 156. The attribute's comment: “internal_hom”.

Stacks Project, Tag 01I8 (internal_hom).

The affine internal-Hom isomorphism itself: for M finitely presented, the internal Hom of the associated sheaves of M and N on Spec R is isomorphic to the associated sheaf of the R-module Hom_R(M, N). This is the iso field of internalHomTildeIso, named so that the isomorphism asserted by the tag is readable as a type. It is canonical by internalHomTildeIsoIso_inv_app_toOpen.

noncomputable def internalHomTildeIsoIso (R : CommRingCat.{u}) (M N : ModuleCat.{u} R)
    [Module.FinitePresentation R M]
    (H : SheafHom (Spec R).sheaf (tilde M) (tilde N)) :
    H.obj ≅ tilde (ModuleCat.of R (M ⟶ N))

AlgebraicGeometry.internalHomTildeIsoIso_inv_app_toOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Modules/AffineInternalHom.lean, line 166. The attribute's comment: “internal_hom”.

Stacks Project, Tag 01I8 (internal_hom). The affine internal-Hom isomorphism is canonical: its inverse sends the global section associated to f : M ⟶ N to the section of the internal Hom represented by the sheaf morphism tilde.map f.

theorem internalHomTildeIsoIso_inv_app_toOpen (R : CommRingCat.{u}) (M N : ModuleCat.{u} R)
    [Module.FinitePresentation R M]
    (H : SheafHom (Spec R).sheaf (tilde M) (tilde N)) (f : M ⟶ N) :
    H.sectionsEquiv ⊤
        ((internalHomTildeIsoIso R M N H).inv.val.app (op ⊤)
          (tilde.toOpen (ModuleCat.of R (M ⟶ N)) ⊤ f)) =
      (tilde.map f).over ⊤

AlgebraicGeometry.internalHomTildeIso_natural_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Modules/AffineInternalHomNatural.lean, line 115. The attribute's comment: “internal_hom”.

The affine internal-Hom comparison is natural in the target module: a morphism of internal Homs exhibited as post-composition with tilde.map u is carried to the associated sheaf of post-composition with u.

theorem internalHomTildeIso_natural_right (R : CommRingCat.{u}) (M N N' : ModuleCat.{u} R)
    [Module.FinitePresentation R M]
    (H : SheafHom (Spec R).sheaf (tilde M) (tilde N))
    (H' : SheafHom (Spec R).sheaf (tilde M) (tilde N'))
    (u : N ⟶ N') (m : H.obj ⟶ H'.obj)
    (hm : SheafHom.IsPostcomp (Spec R).sheaf (tilde.map u) H H' m) :
    m ≫ (internalHomTildeIso R M N' H').iso.hom =
      (internalHomTildeIso R M N H).iso.hom ≫ tilde.map (ModuleCat.homPostcomp M u)

AlgebraicGeometry.internalHomTildeIso_natural_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Modules/AffineInternalHomNatural.lean, line 150. The attribute's comment: “internal_hom”.

The affine internal-Hom comparison is contravariantly natural in the source module: a morphism of internal Homs exhibited as pre-composition with tilde.map β is carried to the associated sheaf of pre-composition with β.

theorem internalHomTildeIso_natural_left (R : CommRingCat.{u}) (M M' N : ModuleCat.{u} R)
    [Module.FinitePresentation R M] [Module.FinitePresentation R M']
    (H : SheafHom (Spec R).sheaf (tilde M) (tilde N))
    (H' : SheafHom (Spec R).sheaf (tilde M') (tilde N))
    (β : M' ⟶ M) (m : H.obj ⟶ H'.obj)
    (hm : SheafHom.IsPrecomp (Spec R).sheaf (tilde.map β) H H' m) :
    m ≫ (internalHomTildeIso R M' N H').iso.hom =
      (internalHomTildeIso R M N H).iso.hom ≫ tilde.map (ModuleCat.homPrecomp N β)

AlgebraicGeometry.tildeTensorPowerIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Modules/TildeTensorPower.lean, line 168. The attribute's comment: “tensor_power”.

Stacks Project, Tag 01I8 (tensor-power part). The associated sheaf of a tensor power is canonically the tensor power of the associated sheaf.

noncomputable def tildeTensorPowerIso (R : CommRingCat.{u}) (M : ModuleCat.{u} R) :
    (n : ℕ) → (tilde (ModuleCat.of R (TensorPower R n M)) ≅ specTildeTensorPower R M n)

AlgebraicGeometry.tildeTensorPowerIso_hom_tprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Modules/TildeTensorPower.lean, line 344. The attribute's comment: “tensor_power”.

Stacks Project, Tag 01I8 (tensor-power part). The canonical affine tensor-power comparison carries a pure tensor to the tensor product of its associated global sections.

theorem tildeTensorPowerIso_hom_tprod (R : CommRingCat.{u}) (M : ModuleCat.{u} R) (n : ℕ)
    (a : Fin n → M) :
    (tildeTensorPowerIso R M n).hom.val.app (specGlobalOpen R)
        ((tilde.toOpen (ModuleCat.of R (TensorPower R n M)) ⊤).hom
          (PiTensorProduct.tprod R a)) =
      tildeTensorPowerSection R M n a

AlgebraicGeometry.tildeTensorPowerIso_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Modules/TildeTensorPower.lean, line 554. The attribute's comment: “tensor_power”.

Stacks Project, Tag 01I8 (tensor-power part). Naturality of the affine tensor-power comparison. The right-hand map is the degree-n component of a unital graded-algebra map extending tilde.map f on degree-one generators; the universal property of the tensor algebra makes such a map unique, so quantifying over it is a statement about the canonical one.

theorem tildeTensorPowerIso_natural
    (hg : (specTildeAlgebras R M).tensorGenerator ≫ g.app 1 =
      tilde.map f ≫ (specTildeAlgebras R N).tensorGenerator) (n : ℕ) :
    tilde.map (ModuleCat.ofHom (PiTensorProduct.map (fun _ : Fin n => f.hom))) ≫
        (tildeTensorPowerIso R N n).hom =
      (tildeTensorPowerIso R M n).hom ≫ ((specTildeAlgebras R M).tensorPieceIso n).inv ≫
        g.app (n : ℤ) ≫ ((specTildeAlgebras R N).tensorPieceIso n).hom

AlgebraicGeometry.tildeTensorPowerIso_natural_piTensorProductMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Modules/TildeTensorPower.lean, line 592. The attribute's comment: “tensor_power”.

Stacks Project, Tag 01I8 (tensor-power part). Naturality of the affine tensor-power comparison against the canonical induced map, rather than against a hypothesised one: this is tildeTensorPowerIso_natural instantiated at specTildeTensorAlgebraMap, the unital graded-algebra map the universal property of the tensor algebra provides. The left-hand map is the associated sheaf of PiTensorProduct.map, the n-fold tensor power of f.

theorem tildeTensorPowerIso_natural_piTensorProductMap (n : ℕ) :
    tilde.map (ModuleCat.ofHom (PiTensorProduct.map (fun _ : Fin n => f.hom))) ≫
        (tildeTensorPowerIso R N n).hom =
      (tildeTensorPowerIso R M n).hom ≫ ((specTildeAlgebras R M).tensorPieceIso n).inv ≫
        (specTildeTensorAlgebraMap R f).app (n : ℤ) ≫
          ((specTildeAlgebras R N).tensorPieceIso n).hom

AlgebraicGeometry.tildeTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/AffineTensor.lean, line 407. The attribute's comment: “tensor_product”. References: EGA I (1.3.12), “(i)”.

For modules M and N over R, there is a canonical isomorphism (M ⊗[R] N)~ ≅ M~ ⊗_{𝒪_(Spec R)} N~.

noncomputable def tildeTensorIso (R : CommRingCat.{u})
    (M N : ModuleCat.{u} R) :
    tilde (M ⊗ N) ≅
      specTensorSheaf R (tilde M) (tilde N)

AlgebraicGeometry.tildeTensorIso_hom_tmul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/AffineTensor.lean, line 417. The attribute's comment: “tensor_product”.

The canonical isomorphism sends a pure tensor, under the tilde--global-sections adjunction, to the section obtained by tensoring the two canonical global sections and applying the sheafification unit.

theorem tildeTensorIso_hom_tmul (R : CommRingCat.{u})
    (M N : ModuleCat.{u} R) (m : M) (n : N) :
    (((tilde.adjunction (R := R)).homEquiv (M ⊗ N)
      (specTensorSheaf R (tilde M) (tilde N))) (tildeTensorIso R M N).hom).hom
        (TensorProduct.tmul R m n) =
      ((Stacks.SheafOfModules.TensorSheafification.toSheafify (Spec R).presheaf
        (isSheaf_specStructureRingPresheaf R)
        (specTensorPresheaf R (tilde M) (tilde N))).app (.op ⊤)).hom
        (TensorProduct.tmul ((Spec R).presheaf.obj (.op ⊤))
          ((tilde.toOpen M ⊤).hom m) ((tilde.toOpen N ⊤).hom n))

AlgebraicGeometry.tildeTensorIso_eq_of_hom_tmul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/AffineTensor.lean, line 433. The attribute's comment: “tensor_product”.

The comparison is canonical: it is the only isomorphism (M ⊗ N)~ ≅ M~ ⊗ N~ satisfying the pure-tensor equation tildeTensorIso_hom_tmul, so tildeTensorIso does not depend on the choice Classical.choose makes to produce it.

theorem tildeTensorIso_eq_of_hom_tmul (R : CommRingCat.{u})
    (M N : ModuleCat.{u} R)
    (e : tilde (M ⊗ N) ≅ specTensorSheaf R (tilde M) (tilde N))
    (he : ∀ (m : M) (n : N),
      (((tilde.adjunction (R := R)).homEquiv (M ⊗ N)
        (specTensorSheaf R (tilde M) (tilde N))) e.hom).hom
          (TensorProduct.tmul R m n) =
        ((Stacks.SheafOfModules.TensorSheafification.toSheafify (Spec R).presheaf
          (isSheaf_specStructureRingPresheaf R)
          (specTensorPresheaf R (tilde M) (tilde N))).app (.op ⊤)).hom
          (TensorProduct.tmul ((Spec R).presheaf.obj (.op ⊤))
            ((tilde.toOpen M ⊤).hom m) ((tilde.toOpen N ⊤).hom n))) :
    e = tildeTensorIso R M N

AlgebraicGeometry.tildeTensorIso_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/AffineTensor.lean, line 455. The attribute's comment: “tensor_product”.

The canonical tensor comparison is natural in both modules.

theorem tildeTensorIso_natural (R : CommRingCat.{u})
    {M M' N N' : ModuleCat.{u} R} (f : M ⟶ M') (g : N ⟶ N') :
    tilde.map (f ⊗ₘ g) ≫ (tildeTensorIso R M' N').hom =
      (tildeTensorIso R M N).hom ≫ tildeTensorSheafMap R f g

Stacks.AssociatedSheaf.associatedSheafTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/AssociatedSheaf/Tensor.lean, line 141. The attribute's comment: “construction (3) commutes with the tensor product, on an arbitrary ringed space”.

Construction (3) carries the tensor product of R-modules to the tensor product of sheaves of modules: ℱ_{M ⊗_R N} ≅ ℱ_M ⊗_{𝒪_X} ℱ_N, on an arbitrary ringed space.

This is the clause of Tag 01I8 that the determinant argument of Tag 0FJN needs on the trivialising open of Tag 08BL rather than on an affine scheme.

def associatedSheafTensorIso (M N : ModuleCat.{u} R) :
    associatedSheaf X α (M ⊗ N) ≅
      ((Stacks.SheafOfModules.Tensor.sheafTensor
        ⟨X.presheaf, Presheaf.isSheaf_of_isSheaf_comp _ X.presheaf
          (forget₂ CommRingCat RingCat) (structureSheafRing X).property⟩).obj
        (associatedSheaf X α M)).obj (associatedSheaf X α N)
Tag 01I9, a lemma

Tag 01I9 in the Stacks Project.

Stacks.AlgebraicGeometry.AffineBaseChange.tilde_map_comp_pushforwardTildeIso_inv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineBaseChange/StructureSheaf.lean, line 327. The attribute's comment: “affine_pushforward_tilde at the ring itself: the comparison carries the structure map of φ to the structure morphism of Spec φ”.

The associated sheaf of a map of R-modules R ⟶ S sending 1 to 1, followed by the inverse of the comparison identifying the direct image along Spec φ of the associated sheaf of S with the associated sheaf of S restricted to an R-module, is the structure morphism 𝒪_{Spec R} ⟶ (Spec φ)_* 𝒪_{Spec S}.

theorem tilde_map_comp_pushforwardTildeIso_inv
    (u : ModuleCat.of R R ⟶ (ModuleCat.restrictScalars φ.hom).obj (ModuleCat.of S S))
    (hu : u.hom (1 : R) = (1 : S)) :
    (tilde.functor R).map u ≫ ((pushforwardTildeIso R S φ).app (ModuleCat.of S S)).inv =
      structureUnitHom (Spec.map φ)

AlgebraicGeometry.pullbackTildeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/QuasiCoherent/AffineTilde.lean, line 87. The attribute's comment: “affine_pullback_tilde”.

Pullback along the map of affine schemes induced by f : R ⟶ S carries the associated sheaf of an R-module to the associated sheaf of its extension of scalars to S, naturally in the module.

public noncomputable def pullbackTildeIso (R S : CommRingCat.{u}) (f : R ⟶ S) :
    tilde.functor R ⋙ Scheme.Modules.pullback (Spec.map f) ≅
      ModuleCat.extendScalars f.hom ⋙ tilde.functor S

AlgebraicGeometry.pullbackTildeIso_hom_app_unit_toOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/QuasiCoherent/AffineTilde.lean, line 99. The attribute's comment: “affine_pullback_tilde”.

The canonical affine pullback comparison sends the pullback of the global section represented by m to the global section represented by 1 ⊗ m. Here the first map is the pullback--pushforward adjunction unit.

public theorem pullbackTildeIso_hom_app_unit_toOpen
    (R S : CommRingCat.{u}) (f : R ⟶ S) (M : ModuleCat R) (m : M) :
    ((pullbackTildeIso R S f).hom.app M).val.app (.op ⊤)
      (((Scheme.Modules.pullbackPushforwardAdjunction (Spec.map f)).unit.app
        (tilde M)).val.app (.op ⊤) (tilde.toOpen M ⊤ m)) =
    tilde.toOpen ((ModuleCat.extendScalars f.hom).obj M) ⊤
      ((1 : S) ⊗ₜ[R, f.hom] m)

AlgebraicGeometry.pushforwardTildeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/QuasiCoherent/AffineTilde.lean, line 155. The attribute's comment: “affine_pushforward_tilde”.

Pushforward along the map of affine schemes induced by φ : R ⟶ S carries the associated sheaf of an S-module to the associated sheaf of its restriction of scalars along φ, naturally in the module.

public noncomputable def pushforwardTildeIso (R S : CommRingCat.{u}) (φ : R ⟶ S) :
    tilde.functor S ⋙ Scheme.Modules.pushforward (Spec.map φ) ≅
      ModuleCat.restrictScalars φ.hom ⋙ tilde.functor R

AlgebraicGeometry.pushforwardTildeIso_hom_app_toOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/QuasiCoherent/AffineTilde.lean, line 193. The attribute's comment: “affine_pushforward_tilde”.

The canonical affine pushforward comparison is normalized by the canonical identifications of a module with the global sections of its associated sheaf: its component at N sends the global section represented by n on Spec S to the global section represented by the same element of the restricted R-module on Spec R.

public theorem pushforwardTildeIso_hom_app_toOpen
    (R S : CommRingCat.{u}) (φ : R ⟶ S) (N : ModuleCat S) (n : N) :
    ((pushforwardTildeIso R S φ).hom.app N).val.app (Opposite.op (⊤ : (Spec R).Opens))
      (tilde.toOpen N (⊤ : (Spec S).Opens) n) =
    tilde.toOpen ((ModuleCat.restrictScalars φ.hom).obj N) (⊤ : (Spec R).Opens) n

Deformation.Artin.SectionsSheaf.tildePullbackIso_id_hom_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/SectionsFirstFactorIdentity.lean, line 447. The attribute's comment: “the affine base-change comparison at the identity ring map: the pullback of the associated sheaf along Spec of the identity ring map is the identity law for pullback followed by the associated sheaf of m ↦ 1 ⊗ m”.

The affine base-change comparison of [Stacks, Tag 01I9] at the identity ring map. The isomorphism (Spec (𝟙 A))^* M̃ ≅ (A ⊗_A M)~ is the identity law for pullback followed by the associated sheaf of the unit m ↦ 1 ⊗ m of extension of scalars.

Neither factor is an identity: A ⊗_A M is not M and (Spec (𝟙 A))^* is an abstract left adjoint. What the statement says is that the comparison, which is built by uniqueness of left adjoints and so has no formula, is the composite of the two canonical maps that are available.

The proof is the uniqueness itself: CategoryTheory.Adjunction.unit_leftAdjointUniq_hom_app evaluates the comparison after the unit of tildePullbackAdjunction (𝟙 A), and eq_of_unit_comp says that this determines a morphism out of (tilde.functor A ⋙ (Spec (𝟙 A))^*).obj M; the four lemmas above evaluate the right-hand side there.

theorem tildePullbackIso_id_hom_app (M : ModuleCat.{u} A) :
    (tildePullbackIso (𝟙 A)).hom.app M =
      ((Scheme.Modules.pullbackCongr (Spec.map_id A)).hom.app ((tilde.functor A).obj M) ≫
          (Scheme.Modules.pullbackId (Spec A)).hom.app ((tilde.functor A).obj M)) ≫
        (tilde.functor A).map (extendUnitId M)
Tag 01IA, a lemma

Tag 01IA in the Stacks Project.

Declarations registered for the tag:

Tag 01IB, a lemma

Tag 01IB in the Stacks Project.

Declarations registered for the tag:

Tag 01IC, a lemma

Tag 01IC in the Stacks Project.

Stacks.DerivedQCoh.abelianQuasiCoherent, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DerivedQCoh/QuasiCoherentAbelian.lean, line 121. The attribute's comment: “abelian category”.

Stacks Project, Tag 01IC (abelian category). The quasi-coherent modules on Spec R form an abelian category, kernels, cokernels and finite products being computed as in all 𝒪_{Spec R}-modules.

instance abelianQuasiCoherent :
    Abelian (SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf).FullSubcategory

AlgebraicGeometry.Scheme.Modules.isQuasicoherent_cokernel, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/QuasiCoherent/Affine.lean, line 85. The attribute's comment: “cokernel”. References: EGA I (4.1.1), “affine, cokernel”.

Stacks Project, Tag 01IC (cokernel). The cokernel of a morphism between quasi-coherent modules on an affine scheme is quasi-coherent.

public instance isQuasicoherent_cokernel {X : Scheme.{u}} [IsAffine X]
    {M N : X.Modules} [M.IsQuasicoherent] [N.IsQuasicoherent] (f : M ⟶ N) :
    (cokernel f).IsQuasicoherent

Stacks.AffineTilde.isQuasicoherent_kernel, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/PseudoCoherentRelative/TildeExact.lean, line 317. The attribute's comment: “kernel”. References: EGA I (4.1.1), “affine, kernel”.

Stacks Project, Tag 01IC (kernel). The kernel of a morphism of quasi-coherent modules on an affine scheme is quasi-coherent. The cokernel half is AlgebraicGeometry.Scheme.Modules.isQuasicoherent_cokernel.

instance isQuasicoherent_kernel {X : Scheme.{u}} [IsAffine X] {M N : X.Modules}
    [M.IsQuasicoherent] [N.IsQuasicoherent] (f : M ⟶ N) : (kernel f).IsQuasicoherent

Declarations registered for the tag:

Tag 01ID, a lemma

Tag 01ID in the Stacks Project.

Stacks.AlgebraicGeometry.QuasicoherentColimits.isQuasicoherent_of_isColimit_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineQcohPushforward/Colimits.lean, line 71. The attribute's comment: “colimits”.

On a spectrum, the point of a colimit cocone of quasi-coherent modules is quasi-coherent.

theorem isQuasicoherent_of_isColimit_spec (R : CommRingCat.{u})
    [HasColimitsOfShape K (ModuleCat.{u} R)] {D : K ⥤ (Spec R).Modules}
    (hD : ∀ k, (D.obj k).IsQuasicoherent) {c : Cocone D} (hc : IsColimit c) :
    c.pt.IsQuasicoherent

Stacks.AlgebraicGeometry.QuasicoherentColimits.isQuasicoherent_sigma, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineQcohPushforward/Colimits.lean, line 170. The attribute's comment: “direct sums”.

A coproduct of quasi-coherent modules is quasi-coherent.

instance isQuasicoherent_sigma {X : Scheme.{u}} {I : Type u} (M : I → X.Modules)
    [∀ i, (M i).IsQuasicoherent] : (∐ M).IsQuasicoherent
Tag 01IE, a lemma

Tag 01IE in the Stacks Project.

Stacks.AlgebraicGeometry.QcohExtension.isQuasicoherent_X₂_of_shortExact_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QcohShortExact/QcohExtension.lean, line 146. References: EGA III (1.4.17), “affine case”.

[Stacks, Tag 01IE], the extension case. If the two outer terms of a short exact sequence of 𝒪_{Spec R}-modules are quasi-coherent then so is the middle one.

theorem isQuasicoherent_X₂_of_shortExact_spec (S : ShortComplex (Spec R).Modules)
    (hS : S.ShortExact) (h₁ : S.X₁.IsQuasicoherent) (h₃ : S.X₃.IsQuasicoherent) :
    S.X₂.IsQuasicoherent

Stacks.AlgebraicGeometry.QcohExtension.isQuasicoherent_X₁_of_shortExact_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QcohShortExact/QcohExtension.lean, line 168.

[Stacks, Tag 01IE], the kernel case. If the last two terms of a short exact sequence of 𝒪_{Spec R}-modules are quasi-coherent then so is the first: it is the kernel of the last map.

theorem isQuasicoherent_X₁_of_shortExact_spec (S : ShortComplex (Spec R).Modules)
    (hS : S.ShortExact) (h₂ : S.X₂.IsQuasicoherent) (h₃ : S.X₃.IsQuasicoherent) :
    S.X₁.IsQuasicoherent

Stacks.AlgebraicGeometry.QcohExtension.isQuasicoherent_X₃_of_shortExact_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QcohShortExact/QcohExtension.lean, line 181.

[Stacks, Tag 01IE], the cokernel case. If the first two terms of a short exact sequence of 𝒪_{Spec R}-modules are quasi-coherent then so is the last: it is the cokernel of the first map, and [Stacks, Tag 01IC] applies because Spec R is affine.

theorem isQuasicoherent_X₃_of_shortExact_spec (S : ShortComplex (Spec R).Modules)
    (hS : S.ShortExact) (h₁ : S.X₁.IsQuasicoherent) (h₂ : S.X₂.IsQuasicoherent) :
    S.X₃.IsQuasicoherent

Stacks.AlgebraicGeometry.QuasicoherentExtension.isQuasicoherent_left_of_shortExact, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasicoherentExtension/Basic.lean, line 157. The attribute's comment: “left term”.

In a short exact sequence of modules on an affine scheme, the left term is quasi-coherent if the middle and right terms are.

lemma isQuasicoherent_left_of_shortExact {X : Scheme.{u}} [IsAffine X]
    (S : ShortComplex X.Modules) (hS : S.ShortExact)
    [S.X₂.IsQuasicoherent] [S.X₃.IsQuasicoherent] :
    S.X₁.IsQuasicoherent

Stacks.AlgebraicGeometry.QuasicoherentExtension.isQuasicoherent_middle_of_shortExact, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasicoherentExtension/Basic.lean, line 168. The attribute's comment: “middle term”.

In a short exact sequence of modules on an affine scheme, the middle term is quasi-coherent if both outer terms are.

lemma isQuasicoherent_middle_of_shortExact {X : Scheme.{u}} [IsAffine X]
    (S : ShortComplex X.Modules) (hS : S.ShortExact)
    [S.X₁.IsQuasicoherent] [S.X₃.IsQuasicoherent] :
    S.X₂.IsQuasicoherent

Stacks.AlgebraicGeometry.QuasicoherentExtension.isQuasicoherent_right_of_shortExact, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasicoherentExtension/Basic.lean, line 190. The attribute's comment: “right term”.

In a short exact sequence of modules on an affine scheme, the right term is quasi-coherent if the left and middle terms are.

lemma isQuasicoherent_right_of_shortExact {X : Scheme.{u}} [IsAffine X]
    (S : ShortComplex X.Modules) (hS : S.ShortExact)
    [S.X₁.IsQuasicoherent] [S.X₂.IsQuasicoherent] :
    S.X₃.IsQuasicoherent
Sources
LeanAlgebraicGeometry.tildeAssociatedSheafNatIso · AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde · AlgebraicGeometry.tilde.adjunction · Stacks.AffineExteriorPower.tildeExteriorPowerIso · Stacks.AffineExteriorPower.tildeExteriorPowerIso_natural · Stacks.AffineExteriorPower.tildeExteriorPowerIso_hom_ιMulti · Stacks.SymGraded.tildeSymmetricPowerIso · Stacks.SymGraded.tildeSymmetricPowerIso_unit

Section26.8 Closed subspaces of affine schemes#

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

Tag 01IG, an example

Tag 01IG in the Stacks Project.

AlgebraicGeometry.quotientPrime_comap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Immersion/Quotient.lean, line 70. The attribute's comment: “quotient_stalk_map”.

Stacks Project, Tag 01IG. The point p / I of Spec(R / I) maps to the point p of Spec R.

public theorem quotientPrime_comap {R : Type u} [CommRing R] (I p : Ideal R) [p.IsPrime]
    (hIp : I ≤ p) :
    PrimeSpectrum.comap (Ideal.Quotient.mk I) (quotientPrime I p hIp) =
      (⟨p, inferInstance⟩ : PrimeSpectrum R)

AlgebraicGeometry.stalkMap_quotient_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Immersion/Quotient.lean, line 103. The attribute's comment: “quotient_stalk_map”.

Stacks Project, Tag 01IG. The map on stalks induced by Spec(R / I) → Spec R at p / I is surjective.

public theorem stalkMap_quotient_surjective {R : Type u} [CommRing R]
    (I p : Ideal R) [p.IsPrime] (hIp : I ≤ p) :
    Function.Surjective
      ((Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))).stalkMap
        (quotientPrime I p hIp)).hom

AlgebraicGeometry.stalkMap_quotient_ker, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Immersion/Quotient.lean, line 124. The attribute's comment: “quotient_stalk_map”.

Stacks Project, Tag 01IG. The kernel of the map on stalks induced by Spec(R / I) → Spec R at p / I is the extended ideal I R_p.

public theorem stalkMap_quotient_ker {R : Type u} [CommRing R]
    (I p : Ideal R) [p.IsPrime] (hIp : I ≤ p) :
    RingHom.ker
        ((Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))).stalkMap
          (quotientPrime I p hIp)).hom =
      Ideal.map
        (StructureSheaf.toStalk R
          (PrimeSpectrum.comap (Ideal.Quotient.mk I) (quotientPrime I p hIp))).hom I

Stacks.ClosedImmersion.isClosedImmersion_specMap_quotientMk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Immersion/QuotientClosedImmersion.lean, line 84. The attribute's comment: “closed_immersion_of_locally_ringed_spaces”.

For an ideal I of a ring R the morphism Spec (R ⧸ I) ⟶ Spec R is a closed immersion of locally ringed spaces, in the sense of Definition 01HK: a closed embedding on spaces whose structure-sheaf map is surjective with kernel locally generated by sections.

theorem isClosedImmersion_specMap_quotientMk :
    IsClosedImmersion
      (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))).toLRSHom.toShHom

Stacks.ClosedImmersion.isClosedEmbedding_specMap_quotientMk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Immersion/QuotientClosedImmersion.lean, line 95. The attribute's comment: “closed_embedding_onto_closed_subset”.

The map Spec (R ⧸ I) → Spec R is a homeomorphism of Spec (R ⧸ I) onto a closed subset of Spec R.

theorem isClosedEmbedding_specMap_quotientMk :
    Topology.IsClosedEmbedding ⇑(Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))).base

Stacks.ClosedImmersion.existsUnique_iso_tildeSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Immersion/QuotientClosedImmersion.lean, line 180. The attribute's comment: “iso_closed_subspace_of_tilde”.

Spec (R ⧸ I) is the closed subspace of Spec R cut out by the quasi-coherent sheaf of ideals I^~: there is a unique isomorphism of locally ringed spaces from Spec (R ⧸ I) to that closed subspace commuting with the two morphisms to Spec R.

theorem existsUnique_iso_tildeSubspace :
    ∃! t : (Spec (CommRingCat.of (↑R ⧸ I))).toLocallyRingedSpace ≅ tildeSubspace I,
      t.hom ≫ tildeSubspaceInclusion I =
        (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))).toLRSHom
Tag 01IH, a lemma

Tag 01IH in the Stacks Project.

Stacks.ClosedImmersion.existsUnique_ideal_iso_quotientSpec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedImmersion/IntoAffine.lean, line 230.

A closed immersion of locally ringed spaces into Spec R is, over Spec R, the spectrum of the quotient by a unique ideal of R.

theorem existsUnique_ideal_iso_quotientSpec {Z : LocallyRingedSpace.{u}}
    (i : Z ⟶ (Spec R).toLocallyRingedSpace) [IsClosedImmersion i.toShHom] :
    ∃! I : Ideal ↑R, ∃ e : Z ≅ (Spec (CommRingCat.of (↑R ⧸ I))).toLocallyRingedSpace,
      i = e.hom ≫ (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))).toLRSHom
Sources
LeanAlgebraicGeometry.quotientPrime_comap · AlgebraicGeometry.stalkMap_quotient_surjective · AlgebraicGeometry.stalkMap_quotient_ker · Stacks.ClosedImmersion.isClosedImmersion_specMap_quotientMk · Stacks.ClosedImmersion.isClosedEmbedding_specMap_quotientMk · Stacks.ClosedImmersion.existsUnique_iso_tildeSubspace · Stacks.ClosedImmersion.existsUnique_ideal_iso_quotientSpec

Section26.9 Schemes#

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

Tag 01IJ, a definition

Tag 01IJ in the Stacks Project.

Declarations registered for the tag:

Tag 01IK, a lemma

Tag 01IK in the Stacks Project.

Declarations registered for the tag:

Tag 01IL, an example

Tag 01IL in the Stacks Project.

AlgebraicGeometry.PuncturedAffinePlane.xOpen_sup_yOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Affine/PuncturedPlane.lean, line 229. The attribute's comment: “affine_open_cover”.

The two coordinate standard opens cover the punctured affine plane.

theorem xOpen_sup_yOpen : xOpen S ⊔ yOpen S = ⊤

AlgebraicGeometry.PuncturedAffinePlane.isAffineOpen_xOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Affine/PuncturedPlane.lean, line 251. The attribute's comment: “affine_open_cover”.

The first-coordinate member of the standard cover is affine.

theorem isAffineOpen_xOpen : IsAffineOpen (xOpen S)

AlgebraicGeometry.PuncturedAffinePlane.isAffineOpen_yOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Affine/PuncturedPlane.lean, line 256. The attribute's comment: “affine_open_cover”.

The second-coordinate member of the standard cover is affine.

theorem isAffineOpen_yOpen : IsAffineOpen (yOpen S)

AlgebraicGeometry.PuncturedAffinePlane.xOpen_inf_yOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Affine/PuncturedPlane.lean, line 261. The attribute's comment: “affine_open_cover”.

The intersection of the two members of the cover is the product standard open.

theorem xOpen_inf_yOpen : xOpen S ⊓ yOpen S = xyOpen S

AlgebraicGeometry.PuncturedAffinePlane.toScheme_iso_specAway_x, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Affine/PuncturedPlane.lean, line 267. The attribute's comment: “affine_open_cover”.

The first-coordinate standard open has coordinate ring k[x,y,1/x].

theorem toScheme_iso_specAway_x :
    Nonempty ((xOpen S).toScheme ≅
      Spec (.of (Localization.Away (MvPolynomial.X (0 : Fin 2) : S.R))))

AlgebraicGeometry.PuncturedAffinePlane.toScheme_iso_specAway_y, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Affine/PuncturedPlane.lean, line 274. The attribute's comment: “affine_open_cover”.

The second-coordinate standard open has coordinate ring k[x,y,1/y].

theorem toScheme_iso_specAway_y :
    Nonempty ((yOpen S).toScheme ≅
      Spec (.of (Localization.Away (MvPolynomial.X (1 : Fin 2) : S.R))))

AlgebraicGeometry.PuncturedAffinePlane.toScheme_iso_specAway_xy, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Affine/PuncturedPlane.lean, line 281. The attribute's comment: “affine_open_cover”.

The intersection standard open has coordinate ring k[x,y,1/(xy)].

theorem toScheme_iso_specAway_xy :
    Nonempty ((xyOpen S).toScheme ≅ Spec (.of (Localization.Away
      (MvPolynomial.X (0 : Fin 2) * MvPolynomial.X (1 : Fin 2) : S.R))))

AlgebraicGeometry.not_isAffine_puncturedScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Affine/PuncturedPlaneNotAffine.lean, line 40. The attribute's comment: “punctured_plane_not_affine”.

The affine plane with its origin removed is not affine.

theorem not_isAffine_puncturedScheme (S : PuncturedAffinePlane.{u}) :
    ¬ IsAffine S.puncturedScheme

AlgebraicGeometry.restrictionPair_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Affine/PuncturedPlaneSections.lean, line 344. The attribute's comment: “sections_exact_sequence”.

Stacks Project, Tag 01IL, sections exact sequence. Restriction of global sections to the two standard affine opens is injective.

theorem restrictionPair_injective (S : PuncturedAffinePlane.{u}) :
    Function.Injective (restrictionPair S)

AlgebraicGeometry.restrictionPair_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Affine/PuncturedPlaneSections.lean, line 431. The attribute's comment: “sections_exact_sequence”.

Stacks Project, Tag 01IL, sections exact sequence. The image of global sections in the product of the two localizations is the kernel of the difference of restrictions to the intersection.

theorem restrictionPair_exact (S : PuncturedAffinePlane.{u}) :
    Function.Exact (restrictionPair S) (localizationDifference S)

AlgebraicGeometry.isIso_coordinateRingToGlobalSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Affine/PuncturedPlaneSections.lean, line 564. The attribute's comment: “punctured_plane_global_sections”.

The canonical homomorphism from the coordinate ring of the affine plane to the global sections of the punctured affine plane is an isomorphism.

theorem isIso_coordinateRingToGlobalSections (S : PuncturedAffinePlane.{u}) :
    IsIso ((Scheme.ΓSpecIso (.of S.R)).inv ≫ S.openImmersion.appTop)
Sources
LeanAlgebraicGeometry.Scheme · AlgebraicGeometry.Scheme.Hom · AlgebraicGeometry.Scheme.instCategory · AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme · AlgebraicGeometry.Scheme.Opens.toScheme · AlgebraicGeometry.PuncturedAffinePlane.xOpen_sup_yOpen · AlgebraicGeometry.PuncturedAffinePlane.isAffineOpen_xOpen · AlgebraicGeometry.PuncturedAffinePlane.isAffineOpen_yOpen

Section26.10 Immersions of schemes#

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

Tag 01IN, a lemma

Tag 01IN in the Stacks Project.

Stacks.ClosedImmersion.exists_ideal_iso_quotient_of_isAffineOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Immersion/ClosedSubspaceScheme.lean, line 114. The attribute's comment: “affine_local_quotient”.

Over an affine open U of a scheme X, a closed immersion of locally ringed spaces i : Z ⟶ X is, compatibly with the canonical presentation of U as Spec Γ(X, U), the spectrum of a quotient of Γ(X, U).

theorem exists_ideal_iso_quotient_of_isAffineOpen (X : Scheme.{u}) (Z : LocallyRingedSpace.{u})
    (i : Z ⟶ X.toLocallyRingedSpace) [hi : IsClosedImmersion i.toShHom]
    (U : X.Opens) (hU : IsAffineOpen U) :
    ∃ (I : Ideal Γ(X, U)) (e : pullback i U.ι.toLRSHom ≅
        (Spec (CommRingCat.of (Γ(X, U) ⧸ I))).toLocallyRingedSpace),
      pullback.snd i U.ι.toLRSHom ≫ hU.isoSpec.hom.toLRSHom =
        e.hom ≫ (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))).toLRSHom

Stacks.ClosedImmersion.exists_scheme_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Immersion/ClosedSubspaceScheme.lean, line 134. The attribute's comment: “source_is_scheme”.

The source of a closed immersion of locally ringed spaces into a scheme carries a scheme structure.

theorem exists_scheme_of_isClosedImmersion (X : Scheme.{u}) (Z : LocallyRingedSpace.{u})
    (i : Z ⟶ X.toLocallyRingedSpace) [IsClosedImmersion i.toShHom] :
    ∃ Z' : Scheme.{u}, Z'.toLocallyRingedSpace = Z

Stacks.ClosedImmersion.exists_scheme_of_closedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Immersion/ClosedSubspaceScheme.lean, line 195. The attribute's comment: “closed_subspace_is_scheme”.

The closed subspace of a scheme cut out by a locally generated ideal sheaf carries a scheme structure on its underlying locally ringed space.

theorem exists_scheme_of_closedSubspace (X : Scheme.{u})
    (J : SheafOfModules.{u} (structureSheafRing X.toLocallyRingedSpace.toRingedSpace))
    (j : J ⟶ SheafOfModules.unit (structureSheafRing X.toLocallyRingedSpace.toRingedSpace))
    [Mono j] (hJ : Nonempty (SheafOfModules.LocalGeneratorsData.{u} J)) :
    ∃ Z : Scheme.{u}, Z.toLocallyRingedSpace =
      (closedSubspace X.toLocallyRingedSpace J j hJ).space

Stacks.ClosedImmersion.exists_ideal_idealSheaf_restrict_iso_tilde_of_locallyRingedSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Immersion/IdealSheafAffineOpen.lean, line 264. The attribute's comment: “kernel_on_affine_open”.

The affine-local description of the ideal sheaf for a closed immersion of locally ringed spaces i : Z ⟶ X into a scheme: over an affine open U = Spec R of X there is an ideal I ⊆ R = Γ(X, U) presenting the fibre over U as Spec (R ⧸ I), and the kernel ℐ of 𝒪_X ⟶ i_* 𝒪_Z restricts on U to I^~.

The source Z is a scheme by Stacks.ClosedImmersion.sourceScheme, so i is a morphism of schemes Stacks.ClosedImmersion.sourceSchemeHom with the same ideal sheaf, and this is Stacks.ClosedImmersion.exists_ideal_idealSheaf_restrict_iso_tilde for that morphism.

theorem exists_ideal_idealSheaf_restrict_iso_tilde_of_locallyRingedSpace (X : Scheme.{u})
    (Z : LocallyRingedSpace.{u}) (i : Z ⟶ X.toLocallyRingedSpace)
    [hi : IsClosedImmersion i.toShHom] (U : X.Opens) (hU : IsAffineOpen U) :
    ∃ (I : Ideal Γ(X, U)) (e : pullback (sourceSchemeHom X Z i) U.ι ≅
        Spec (CommRingCat.of (Γ(X, U) ⧸ I))),
      pullback.snd (sourceSchemeHom X Z i) U.ι ≫ hU.isoSpec.hom =
          e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) ∧
        ∃ φ : (Scheme.Modules.restrictFunctor U.ι).obj (idealSheaf i.toShHom) ≅
            (modulePullback hU.isoSpec.hom.toLRSHom.toShHom).obj
              (tilde (ModuleCat.of Γ(X, U) I)),
          φ.hom ≫ (modulePullback hU.isoSpec.hom.toLRSHom.toShHom).map
                (tildeIdealι Γ(X, U) I) ≫
              (Stacks.IdealSheafRestrict.pullbackUnitIso hU.isoSpec.hom).hom =
            (Scheme.Modules.restrictFunctor U.ι).map
                (kernel.ι (SheafOfModules.unitToPushforwardObjUnit
                  (structureSheafHom i.toShHom))) ≫
              (Scheme.Modules.restrictUnitIso U.ι).hom

Stacks.ClosedImmersion.isQuasicoherent_idealSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Immersion/IdealSheafQuasicoherent.lean, line 53. The attribute's comment: “kernel_quasi_coherent”.

Stacks Project, Tag 01IN. The kernel of 𝒪_X ⟶ i_* 𝒪_Z for a closed immersion of locally ringed spaces i : Z ⟶ X into a scheme is a quasi-coherent sheaf of ideals.

theorem isQuasicoherent_idealSheaf (X : Scheme.{u}) (Z : LocallyRingedSpace.{u})
    (i : Z ⟶ X.toLocallyRingedSpace) [hi : IsClosedImmersion i.toShHom] :
    (idealSheaf i.toShHom).IsQuasicoherent

Stacks.ClosedImmersion.isQuasicoherent_iff_localGenerators, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Immersion/IdealSheafQuasicoherent.lean, line 66. The attribute's comment: “ideal_quasi_coherent_iff_locally_generated”.

Stacks Project, Tag 01IN. A sheaf of ideals on a scheme is locally generated by sections if and only if it is quasi-coherent.

theorem isQuasicoherent_iff_localGenerators (X : Scheme.{u})
    (J : (SheafOfModules.unit X.ringCatSheaf).Submodule) :
    J.toSheafOfModules.IsQuasicoherent ↔
      Nonempty (SheafOfModules.LocalGeneratorsData.{u} J.toSheafOfModules)
Tag 01IO, a definition

Tag 01IO in the Stacks Project.

Declarations registered for the tag:

Tag 01IQ, a lemma

Tag 01IQ in the Stacks Project.

Declarations registered for the tag:

Sources
LeanStacks.ClosedImmersion.exists_ideal_iso_quotient_of_isAffineOpen · Stacks.ClosedImmersion.exists_scheme_of_isClosedImmersion · Stacks.ClosedImmersion.exists_scheme_of_closedSubspace · Stacks.ClosedImmersion.exists_ideal_idealSheaf_restrict_iso_tilde_of_locallyRingedSpace · Stacks.ClosedImmersion.isQuasicoherent_idealSheaf · Stacks.ClosedImmersion.isQuasicoherent_iff_localGenerators · AlgebraicGeometry.IsOpenImmersion · AlgebraicGeometry.Scheme.Opens

Section26.11 Zariski topology of schemes#

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

Tag 01IS, a lemma

Tag 01IS in the Stacks Project.

Declarations registered for the tag:

Tag 01IT, a lemma

Tag 01IT in the Stacks Project.

Declarations registered for the tag:

Tag 01IV, a lemma

Tag 01IV in the Stacks Project.

Declarations registered for the tag:

Tag 01IW, a lemma

Tag 01IW in the Stacks Project.

Declarations registered for the tag:

Tag 01IX, a lemma

Tag 01IX in the Stacks Project.

AlgebraicGeometry.Scheme.exists_isStandardOpenCover_basicOpen_eq_of_iSup_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Affine/StandardRefinement.lean, line 44.

Every affine open has a finite standard open cover each of whose members is also a standard open in a member of a given affine open cover of the ambient scheme.

theorem exists_isStandardOpenCover_basicOpen_eq_of_iSup_eq_top
    (X : Scheme.{u}) {ι : Type v} (U : ι → X.Opens)
    (hU : ∀ i, IsAffineOpen (U i)) (hUcover : ⨆ i, U i = ⊤)
    (V : X.Opens) (hV : IsAffineOpen V) :
    ∃ (n : ℕ) (f : Fin n → Γ(X, V)) (i : Fin n → ι)
      (g : ∀ j, Γ(X, U (i j))),
      PrimeSpectrum.IsStandardOpenCoverOfSpectrum f ∧
        (⨆ j, X.basicOpen (f j)) = V ∧
        ∀ j, X.basicOpen (f j) = X.basicOpen (g j)
Tag 0F1A, a lemma

Tag 0F1A in the Stacks Project.

AlgebraicGeometry.Scheme.isRestriction_iff_isSheafOnAffineBasis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Affine/SheafOnBasis.lean, line 618. The attribute's comment: “equivalence of (1) and (2)”. References: EGA 0 (3.2.2), “affine basis of a scheme”.

A presheaf on the affine opens is (up to isomorphism) the restriction of a sheaf if and only if it is a sheaf on the affine-open basis.

theorem isRestriction_iff_isSheafOnAffineBasis (X : Scheme.{u})
    (F : PresheafOnBasis X.affineOpens) :
    (∃ G : TopCat.Sheaf (Type u) (TopCat.of X),
      Nonempty (F ≅ restrictOfSheaf X.affineOpens G)) ↔
      IsSheafOnBasis X.affineOpens F

AlgebraicGeometry.Scheme.isSheafOnAffineBasis_iff_standardPairs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Affine/SheafOnBasis.lean, line 642. The attribute's comment: “equivalence of (2) and (3)”.

A presheaf on the affine-open basis is a sheaf exactly when its section set on the empty open is a singleton and compatible sections glue uniquely across every standard two-open cover of an affine open.

theorem isSheafOnAffineBasis_iff_standardPairs (X : Scheme.{u})
    (F : PresheafOnBasis X.affineOpens) :
    IsSheafOnBasis X.affineOpens F ↔
      ((∃! _s : F.obj (op (affineBasisOpen X ⟨⊥, isAffineOpen_bot X⟩)), True) ∧
      ∀ (U : X.affineOpens) (f g : Γ(X, U.1))
        (_hcov : U.1 = X.basicOpen f ⊔ X.basicOpen g)
        (s : F.obj (op (affineBasisOpen X (X.affineBasicOpen f))))
        (t : F.obj (op (affineBasisOpen X (X.affineBasicOpen g)))),
        (F.restrictMap X.affineOpens
            (show (affineBasisOpen X (X.affineBasicOpen (f * g))).obj ≤
                (affineBasisOpen X (X.affineBasicOpen f)).obj by
              change X.basicOpen (f * g) ≤ X.basicOpen f
              rw [X.basicOpen_mul]
              exact inf_le_left) s =
          F.restrictMap X.affineOpens
            (show (affineBasisOpen X (X.affineBasicOpen (f * g))).obj ≤
                (affineBasisOpen X (X.affineBasicOpen g)).obj by
              change X.basicOpen (f * g) ≤ X.basicOpen g
              rw [X.basicOpen_mul]
              exact inf_le_right) t) ↔
        ∃! r : F.obj (op (affineBasisOpen X U)),
          (F.restrictMap X.affineOpens (by exact (X.affineBasicOpen_le f)) r = s) ∧
          (F.restrictMap X.affineOpens (by exact (X.affineBasicOpen_le g)) r = t))
Tag 02O0, a lemma

Tag 02O0 in the Stacks Project.

Declarations registered for the tag:

Tag 01IY, an example

Tag 01IY in the Stacks Project.

AlgebraicGeometry.exists_valuationRing_with_spectrum_chain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/NoClosedPoints.lean, line 495. The attribute's comment: “valuation ring with the specified prime spectrum”.

There is a valuation ring whose spectrum is a countable strictly increasing chain of prime ideals, with one further maximal ideal above all of them.

theorem exists_valuationRing_with_spectrum_chain :
    ∃ (R : Type u) (ring : CommRing R),
      letI : CommRing R := ring
      ∃ (domain : IsDomain R),
        letI : IsDomain R := domain
        ∃ (localRing : IsLocalRing R),
          letI : IsLocalRing R := localRing
          IsValuationRing R ∧
            ∃ p : ℕ → PrimeSpectrum R,
              ((p 0).asIdeal = ⊥) ∧
                (∀ n, (p n).asIdeal < (p (n + 1)).asIdeal) ∧
                (∀ q : PrimeSpectrum R,
                  (q = IsLocalRing.closedPoint R) ∨ (∃ n, q = p n))

AlgebraicGeometry.puncturedSpectrum_no_closed_points, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/NoClosedPoints.lean, line 537. The attribute's comment: “the punctured spectrum has no closed points”.

Removing the unique closed point from a local spectrum with the indicated unbounded chain of other primes gives an open subscheme without closed points.

theorem puncturedSpectrum_no_closed_points
    (R : Type u) [CommRing R] [IsLocalRing R]
    (p : ℕ → PrimeSpectrum R)
    (hchain : ∀ n, (p n).asIdeal < (p (n + 1)).asIdeal)
    (hexhaust : ∀ q : PrimeSpectrum R,
      (q = IsLocalRing.closedPoint R) ∨ (∃ n, q = p n)) :
    ∀ x : Scheme.Opens.toScheme
      (⟨({IsLocalRing.closedPoint R} : Set (PrimeSpectrum R))ᶜ,
        (IsLocalRing.isClosed_singleton_closedPoint R).isOpen_compl⟩ :
        (Spec (.of R)).Opens),
      ¬ IsClosed ({x} : Set _)

AlgebraicGeometry.exists_scheme_without_closed_points, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/NoClosedPoints.lean, line 565. The attribute's comment: “existence of a scheme without closed points”.

A nonempty scheme may have no closed points.

theorem exists_scheme_without_closed_points :
    ∃ X : Scheme.{u}, Nonempty X ∧ ∀ x : X, ¬ IsClosed ({x} : Set X)
Sources
LeanAlgebraicGeometry.instQuasiSoberCarrierCarrierCommRingCat · AlgebraicGeometry.instT0SpaceCarrierCarrierCommRingCat · AlgebraicGeometry.Scheme.isBasis_affineOpens · AlgebraicGeometry.instPrespectralSpaceCarrierCarrierCommRingCat · instLocallyCompactSpaceOfPrespectralSpace · AlgebraicGeometry.exists_basicOpen_le_affine_inter · AlgebraicGeometry.Scheme.exists_isStandardOpenCover_basicOpen_eq_of_iSup_eq_top · AlgebraicGeometry.Scheme.isRestriction_iff_isSheafOnAffineBasis

Section26.12 Reduced schemes#

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

Tag 01J0, a definition

Tag 01J0 in the Stacks Project.

Declarations registered for the tag:

Tag 01J1, a lemma

Tag 01J1 in the Stacks Project.

Declarations registered for the tag:

Tag 01J2, a lemma

Tag 01J2 in the Stacks Project.

Declarations registered for the tag:

Tag 01J3, a lemma

Tag 01J3 in the Stacks Project.

AlgebraicGeometry.Scheme.IdealSheafData.eq_vanishingIdeal_of_isReduced_subscheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/ReducedClosedSubscheme.lean, line 72. The attribute's comment: “uniqueness”. References: EGA I (5.1.2), “uniqueness”; EGA I (5.2.1), “closed case, uniqueness”.

A reduced closed subscheme structure on a closed subset is its vanishing-ideal structure.

theorem eq_vanishingIdeal_of_isReduced_subscheme {X : Scheme.{u}}
    (I : X.IdealSheafData) (T : Closeds X) (hT : I.support = T)
    [IsReduced I.subscheme] : I = Scheme.IdealSheafData.vanishingIdeal T

Declarations registered for the tag:

Tag 01J4, a definition

Tag 01J4 in the Stacks Project.

AlgebraicGeometry.Scheme.reduction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Reduction.lean, line 57. The attribute's comment: “the reduction X_red of X”. References: EGA I (5.1.3).

The reduction X_red of a scheme X: the closed subscheme cut out by the nilradical ideal sheaf, that is the reduced induced closed subscheme structure on all of X.

noncomputable def reduction : Scheme.{u}

AlgebraicGeometry.Scheme.reducedInduced, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/SchemeStructure.lean, line 108. The attribute's comment: “the reduced induced scheme structure on Z”. References: EGA I (5.5.4); EGA IV (4.9.4).

The reduced induced scheme structure on a closed subset Z of X: the closed subscheme cut out by the vanishing ideal sheaf of Z.

noncomputable def reducedInduced {X : Scheme.{u}} (Z : Closeds X) : X.SchemeStructure Z

Declarations registered for the tag:

Tag 0F2L, a remark

Tag 0F2L in the Stacks Project.

Stacks.ZariskiAndSeparation.ReducedInducedLocallyClosed.reducedInducedIdealSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/ReducedInducedLocallyClosed.lean, line 35. The attribute's comment: “reduced_induced_scheme_structure_on_a_locally_closed_subset”.

The defining ideal sheaf of the reduced induced scheme structure on a locally closed subset.

noncomputable def reducedInducedIdealSheaf {X : Scheme.{u}} (T : Set X)
    (hT : IsLocallyClosed T) : (reducedInducedOpen T hT).toScheme.IdealSheafData
Tag 0356, a lemma

Tag 0356 in the Stacks Project.

AlgebraicGeometry.Scheme.IdealSheafData.exists_lift_subschemeι_iff_range_subset_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/ReducedClosedSubscheme.lean, line 95. The attribute's comment: “factorization criterion”. References: EGA I (5.2.2), “more general”; SGA 3 VIB (7.3.0), “factorization criterion”; SGA 3 VIB (7.1), “partial”.

A map from a reduced scheme factors through a closed subscheme precisely when its set-theoretic image lies in the support of that subscheme.

theorem exists_lift_subschemeι_iff_range_subset_support {X Y : Scheme.{u}}
    [IsReduced Y] (I : X.IdealSheafData) (f : Y ⟶ X) :
    (∃ g : Y ⟶ I.subscheme, g ≫ I.subschemeι = f) ↔
      Set.range f ⊆ (I.support : Set X)

AlgebraicGeometry.Scheme.existsUnique_lift_nilradical_subschemeι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/ReducedClosedSubscheme.lean, line 118. The attribute's comment: “factorization through the reduction”. References: EGA I (5.1.5), “reduced source factors”; EGA I (4.1.8), “special case”.

Every map from a reduced scheme factors uniquely through the reduction of its target.

theorem Scheme.existsUnique_lift_nilradical_subschemeι {X Y : Scheme.{u}} [IsReduced Y]
    (f : Y ⟶ X) :
    ∃! g : Y ⟶ X.nilradical.subscheme, g ≫ X.nilradical.subschemeι = f
Sources
LeanAlgebraicGeometry.IsReduced · AlgebraicGeometry.isReduced_of_isReduced_stalk · AlgebraicGeometry.isReduced_stalk_of_isReduced · AlgebraicGeometry.affine_isReduced_iff · AlgebraicGeometry.Scheme.IdealSheafData.eq_vanishingIdeal_of_isReduced_subscheme · AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal · AlgebraicGeometry.Scheme.IdealSheafData.coe_support_vanishingIdeal · AlgebraicGeometry.Scheme.IdealSheafData.isReduced_subscheme_vanishingIdeal

Section26.13 Points of schemes#

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

Tag 01J6, a lemma

Tag 01J6 in the Stacks Project.

Declarations registered for the tag:

Tag 02NA, an equation

Tag 02NA in the Stacks Project.

Declarations registered for the tag:

Tag 01J9, a lemma

Tag 01J9 in the Stacks Project.

AlgebraicGeometry.pointsEquivFieldValuedPointClasses, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Points/FieldValued.lean, line 102. The attribute's comment: “the bijection with equivalence classes”.

Points of a scheme correspond bijectively to equivalence classes of field-valued points.

noncomputable def pointsEquivFieldValuedPointClasses (X : Scheme.{u}) :
    X ≃ Quotient (FieldValuedPoint.setoid X)

AlgebraicGeometry.FieldValuedPoint.hasCommonExtension_iff_point_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Points/FieldValued.lean, line 121. The attribute's comment: “the common-extension relation”. References: EGA I (3.4.5), “location map”.

Two field-valued points have a common field-valued extension if and only if they have the same image point.

theorem hasCommonExtension_iff_point_eq {X : Scheme.{u}} (p q : FieldValuedPoint X) :
    p.HasCommonExtension q ↔ p.point = q.point

AlgebraicGeometry.FieldValuedPoint.canonical_isSmallest, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Points/FieldValued.lean, line 171. The attribute's comment: “the smallest representative”. References: EGA I (2.4.6), “factorization via κ(x)”.

The canonical morphism Spec(κ(x)) ⟶ X is the smallest representative of the equivalence class corresponding to x.

theorem canonical_isSmallest {X : Scheme.{u}} (x : X) :
    (canonical X x).IsSmallest

AlgebraicGeometry.FieldValuedPoint.uniqueIso_of_isSmallest, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Points/FieldValued.lean, line 195. The attribute's comment: “uniqueness up to unique isomorphism”.

Any two smallest representatives of the same point are uniquely isomorphic over X.

theorem uniqueIso_of_isSmallest {X : Scheme.{u}} {p q : FieldValuedPoint X}
    (hp : p.IsSmallest) (hq : q.IsSmallest) (h : p.point = q.point) :
    ∃! e : Spec (.of p.carrier) ≅ Spec (.of q.carrier), e.hom ≫ q.map = p.map

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.SpecToEquivOfLocalRing · AlgebraicGeometry.Scheme.fromSpecStalk · AlgebraicGeometry.pointsEquivFieldValuedPointClasses · AlgebraicGeometry.FieldValuedPoint.hasCommonExtension_iff_point_eq · AlgebraicGeometry.FieldValuedPoint.canonical_isSmallest · AlgebraicGeometry.FieldValuedPoint.uniqueIso_of_isSmallest · AlgebraicGeometry.Scheme.SpecToEquivOfField

Section26.14 Glueing schemes#

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

Tag 01JA, the section

Tag 01JA in the Stacks Project.

AlgebraicGeometry.isPushout_opens_ι_of_sup_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/OpenImmersionPushout.lean, line 88. The attribute's comment: “the two-chart glueing as a pushout square of schemes”.

A scheme covered by two opens is glued from them: the square formed by the two inclusions of the intersection and the two inclusions into the ambient scheme is a pushout square.

theorem isPushout_opens_ι_of_sup_eq_top {S : Scheme.{u}} {U V : S.Opens} (h : U ⊔ V = ⊤) :
    IsPushout (S.homOfLE inf_le_left) (S.homOfLE inf_le_right) U.ι V.ι

AlgebraicGeometry.existsUnique_comp_ι_eq_of_sup_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/OpenImmersionPushout.lean, line 119. The attribute's comment: “the two-chart case of the mapping property for morphisms out of a glueing”.

The mapping property for morphisms out of a glueing with two charts: if the opens U, V of a scheme S satisfy U ⊔ V = ⊤, then a morphism out of S is the same thing as a pair of morphisms out of U and out of V agreeing on U ⊓ V.

theorem existsUnique_comp_ι_eq_of_sup_eq_top {S T : Scheme.{u}} {U V : S.Opens}
    (h : U ⊔ V = ⊤) {a : U.toScheme ⟶ T} {b : V.toScheme ⟶ T}
    (w : S.homOfLE inf_le_left ≫ a = S.homOfLE inf_le_right ≫ b) :
    ∃! m : S ⟶ T, U.ι ≫ m = a ∧ V.ι ≫ m = b

AlgebraicGeometry.opensRange_pushout_inl_sup_opensRange_pushout_inr, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/OpenImmersionPushout.lean, line 136. The attribute's comment: “the two-chart case of part (1): the charts cover the glued scheme”.

The two charts of the scheme obtained by glueing X and Y along a span of open immersions cover it.

theorem opensRange_pushout_inl_sup_opensRange_pushout_inr :
    (pushout.inl f g).opensRange ⊔ (pushout.inr f g).opensRange = ⊤

AlgebraicGeometry.preimage_opensRange_pushout_inl, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/OpenImmersionPushout.lean, line 152. The attribute's comment: “the two-chart case of part (2): the overlap of the two charts”.

Inside the second chart of the scheme obtained by glueing X and Y along a span of open immersions, the overlap with the first chart is exactly the image of the span's vertex.

theorem preimage_opensRange_pushout_inl :
    (pushout.inr f g) ⁻¹ᵁ (pushout.inl f g).opensRange = g.opensRange

AlgebraicGeometry.isPullback_pushout_inl_inr, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/OpenImmersionPushout.lean, line 169. The attribute's comment: “the two-chart case of part (2), as a cartesian square”.

The pushout square of a span of open immersions of schemes is also cartesian: the span's vertex is the intersection of the two charts of the glued scheme.

theorem isPullback_pushout_inl_inr :
    IsPullback f g (pushout.inl f g) (pushout.inr f g)
Tag 01JB, a lemma

Tag 01JB in the Stacks Project.

AlgebraicGeometry.LocallyRingedSpace.GlueData.range_overlap, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/LocallyRingedSpaces.lean, line 94. The attribute's comment: “part (2): the overlap is the intersection of two charts”.

The prescribed overlap V i j, viewed inside the chart U i through D.f i j, is exactly the part of that chart lying over the chart U j: φ i '' U i j = U i ∩ U j in the glued space, stated as an equality of subsets of U i.

lemma range_overlap (D : LocallyRingedSpace.GlueData.{u}) (i j : D.J) :
    Set.range (D.f i j).base = (D.ι i).base ⁻¹' Set.range (D.ι j).base

AlgebraicGeometry.LocallyRingedSpace.GlueData.t_f_eq_restrictOverlapIso_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/LocallyRingedSpaces.lean, line 133. The attribute's comment: “part (3): the transition map is the restriction of φ j⁻¹ ∘ φ i”.

The transition map is φ j⁻¹ ∘ φ i on the overlap: for any morphism s : U i ∩ U j ⟶ U j with s ≫ φ j the inclusion of U i ∩ U j (the restriction of φ j⁻¹ to U i ∩ U j), the map φ i j, read in the chart U j, is s composed with the restriction isomorphism.

theorem t_f_eq_restrictOverlapIso_comp (D : LocallyRingedSpace.GlueData.{u}) (i j : D.J)
    (s : pullback (D.ι i) (D.ι j) ⟶ D.U j)
    (hs : s ≫ D.ι j = pullback.fst (D.ι i) (D.ι j) ≫ D.ι i) :
    D.t i j ≫ D.f j i = (D.restrictOverlapIso i j).hom ≫ s

AlgebraicGeometry.LocallyRingedSpace.GlueData.homOutEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/LocallyRingedSpaces.lean, line 146. The attribute's comment: “the mapping property for morphisms out of the glueing”.

The mapping property for morphisms out of a gluing: a morphism D.glued ⟶ Y is the same thing as a family of morphisms D.U i ⟶ Y agreeing on the prescribed overlaps, the agreement being read through the transition maps. The bijection sends a morphism to the family of its restrictions D.ι i ≫ h.

noncomputable def homOutEquiv
    (D : LocallyRingedSpace.GlueData.{u}) (Y : LocallyRingedSpace.{u}) :
    (D.glued ⟶ Y) ≃
      { f : ∀ i, D.U i ⟶ Y //
          ∀ i j, D.f i j ≫ f i = D.t i j ≫ D.f j i ≫ f j }

AlgebraicGeometry.LocallyRingedSpace.GlueData.hom_pullbackCharts_jointlySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/LocallyRingedSpaces.lean, line 173. The attribute's comment: “canonical inverse-image cover”.

The pullbacks of the canonical charts along a morphism into the glued space jointly cover its source.

theorem hom_pullbackCharts_jointlySurjective (D : LocallyRingedSpace.GlueData.{u})
    {Y : LocallyRingedSpace.{u}} (g : Y ⟶ D.glued) (y : Y) :
    ∃ (i : D.J) (x : pullback (C := LocallyRingedSpace) g (D.ι i)),
      (pullback.fst g (D.ι i)).base x = y

AlgebraicGeometry.LocallyRingedSpace.GlueData.hom_pullbackCharts_preimage_overlap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/LocallyRingedSpaces.lean, line 183. The attribute's comment: “inverse images of overlaps”.

On the inverse-image chart indexed by i, the inverse image of V i j is exactly its intersection with the chart indexed by j.

theorem hom_pullbackCharts_preimage_overlap (D : LocallyRingedSpace.GlueData.{u})
    {Y : LocallyRingedSpace.{u}} (g : Y ⟶ D.glued) (i j : D.J) :
    (pullback.snd g (D.ι i)).base ⁻¹' Set.range (D.f i j).base =
      Set.range
        (pullback.fst (pullback.fst g (D.ι i))
          (pullback.fst g (D.ι j))).base

AlgebraicGeometry.LocallyRingedSpace.GlueData.hom_pullbackCharts_transition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/LocallyRingedSpaces.lean, line 202. The attribute's comment: “transition compatibility for morphisms into the gluing”.

The local morphisms on the inverse-image charts are related on intersections by the prescribed transition map.

theorem hom_pullbackCharts_transition (D : LocallyRingedSpace.GlueData.{u})
    {Y : LocallyRingedSpace.{u}} (g : Y ⟶ D.glued) (i j : D.J) :
    ∃! k : pullback (pullback.fst g (D.ι i)) (pullback.fst g (D.ι j)) ⟶ D.V (i, j),
      k ≫ D.f i j =
          pullback.fst (pullback.fst g (D.ι i)) (pullback.fst g (D.ι j)) ≫
            pullback.snd g (D.ι i) ∧
        k ≫ D.t i j ≫ D.f j i =
          pullback.snd (pullback.fst g (D.ι i)) (pullback.fst g (D.ι j)) ≫
            pullback.snd g (D.ι j)

AlgebraicGeometry.LocallyRingedSpace.GlueData.existsUnique_hom_of_openCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/MorphismsIntoGluing/GluingReconstruction.lean, line 268. The attribute's comment: “morphisms of locally ringed spaces glue over an open covering of the source”.

Morphisms of locally ringed spaces glue over an open covering of the source: a family of morphisms out of the members of the covering which agree on the pairwise overlaps comes from a unique morphism out of the covered space.

This is the locally ringed space counterpart of AlgebraicGeometry.Scheme.Cover.glueMorphisms, and the reason it is available here is that the covered space is the gluing of its own covering (openCoverFromGlued_isIso), so the morphism is obtained from the universal property of the multicoequalizer.

theorem existsUnique_hom_of_openCover
    {I : Type u} {Y Z : LocallyRingedSpace.{u}}
    {V : I → LocallyRingedSpace.{u}} (v : ∀ i, V i ⟶ Y)
    [∀ i, LocallyRingedSpace.IsOpenImmersion (v i)]
    (hv : ∀ y : Y, ∃ i x, (v i).base x = y)
    (h : ∀ i, V i ⟶ Z)
    (hcompat : ∀ i j, pullback.fst (v i) (v j) ≫ h i = pullback.snd (v i) (v j) ≫ h j) :
    ∃! f : Y ⟶ Z, ∀ i, v i ≫ f = h i

AlgebraicGeometry.LocallyRingedSpace.GlueData.existsUnique_hom_to_glued_of_compatibleCharts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/MorphismsIntoGluing/GluingReconstruction.lean, line 312. The attribute's comment: “reconstruction from compatible charts”.

Compatible morphisms from an open covering of a locally ringed space to the pieces of a gluing datum determine a unique morphism to the glued space. The two equations for transitionLift say that on V i ×_Y V j the maps are related by the transition D.t i j.

theorem existsUnique_hom_to_glued_of_compatibleCharts
    (D : LocallyRingedSpace.GlueData.{u}) (Y : LocallyRingedSpace.{u})
    (V : D.J → LocallyRingedSpace.{u}) (v : ∀ i, V i ⟶ Y)
    (v_open : ∀ i, LocallyRingedSpace.IsOpenImmersion (v i))
    (v_jointly_surjective : ∀ y : Y, ∃ (i : D.J) (x : V i), (v i).base x = y)
    (g : ∀ i, V i ⟶ D.U i)
    (transitionLift : ∀ i j, pullback (v i) (v j) ⟶ D.V (i, j))
    (transitionLift_f : ∀ i j,
      transitionLift i j ≫ D.f i j = pullback.fst (v i) (v j) ≫ g i)
    (transitionLift_t_f : ∀ i j,
      transitionLift i j ≫ D.t i j ≫ D.f j i = pullback.snd (v i) (v j) ≫ g j) :
    ∃! f : Y ⟶ D.glued, ∀ i, v i ≫ f = g i ≫ D.ι i

AlgebraicGeometry.LocallyRingedSpace.GlueData.hom_chartDatumOfHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/MorphismsIntoGluing/GluingReconstruction.lean, line 418. The attribute's comment: “the mapping property for morphisms into the glueing”.

The mapping property for morphisms into a glueing: a morphism g : Y ⟶ D.glued is recovered from the descent datum it induces, so that passing from a morphism to its chart datum and back is the identity. Combined with AlgebraicGeometry.LocallyRingedSpace.GlueData.existsUnique_hom_to_glued, which says that every chart datum determines a unique morphism, this identifies Mor(Y, D.glued) with the set of descent data arising from morphisms.

theorem hom_chartDatumOfHom (D : LocallyRingedSpace.GlueData.{u})
    {Y : LocallyRingedSpace.{u}} (g : Y ⟶ D.glued) :
    ∀ f : Y ⟶ D.glued,
      (∀ i, (D.chartDatumOfHom g).v i ≫ f = (D.chartDatumOfHom g).g i ≫ D.ι i) → f = g

AlgebraicGeometry.LocallyRingedSpace.GlueData.ChartDatum.chartIso_hom_fst_and_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/MorphismsIntoGluing/GluingReconstruction.lean, line 499. The attribute's comment: “a descent datum is its own inverse-image covering”.

The other half of the round trip for morphisms into a glueing: a descent datum is carried isomorphically, chart by chart and compatibly with both the covering maps and the local morphisms, onto the descent datum induced by the morphism it determines — whose charts, covering maps and local morphisms are pullback f (D.ι i), pullback.fst f (D.ι i) and pullback.snd f (D.ι i) by chartDatumOfHom_V, chartDatumOfHom_v and chartDatumOfHom_g. Together with AlgebraicGeometry.LocallyRingedSpace.GlueData.hom_chartDatumOfHom this identifies Mor(Y, D.glued) with the descent data of the statement.

theorem ChartDatum.chartIso_hom_fst_and_snd {D : LocallyRingedSpace.GlueData.{u}}
    {Y : LocallyRingedSpace.{u}} (C : D.ChartDatum Y) {f : Y ⟶ D.glued}
    (hf : ∀ i, C.v i ≫ f = C.g i ≫ D.ι i) (i : D.J) :
    (C.chartIso hf i).hom ≫ pullback.fst f (D.ι i) = C.v i ∧
      (C.chartIso hf i).hom ≫ pullback.snd f (D.ι i) = C.g i

AlgebraicGeometry.LocallyRingedSpace.GlueData.homIntoEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/MorphismsIntoGluing/MappingProperty.lean, line 273. The attribute's comment: “Mor(Y, X) is the set of descent data on an open covering of Y”.

The mapping property for morphisms into a gluing, as a bijection: a morphism Y ⟶ D.glued is the same thing as a descent datum on Y, namely an open covering of Y together with compatible morphisms from its members to the pieces of the gluing datum. The bijection sends f to the covering by the inverse images f ⁻¹' (U i) and the factorisations of f through the charts. This is the counterpart for morphisms into the gluing of AlgebraicGeometry.LocallyRingedSpace.GlueData.homOutEquiv.

noncomputable def homIntoEquiv (D : LocallyRingedSpace.GlueData.{u})
    (Y : LocallyRingedSpace.{u}) : (Y ⟶ D.glued) ≃ D.ChartDatumOpens Y

Declarations registered for the tag:

Tag 01JC, a lemma

Tag 01JC in the Stacks Project.

Declarations registered for the tag:

Tag 01JD, an example

Tag 01JD in the Stacks Project.

AlgebraicGeometry.affineSpaceWithDoubledZero, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/DoubledOrigin.lean, line 105. The attribute's comment: “doubled_zero_construction”. References: EGA I (5.5.11), “doubled origin constr.”.

Affine n-space over k with its origin doubled, obtained by gluing two copies along the complements of their origins via the coordinate identification.

noncomputable abbrev affineSpaceWithDoubledZero (k : Type u) [Field k] (n : ℕ) :
    Scheme.{u}

AlgebraicGeometry.coordinateMorphismData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/DoubledOrigin.lean, line 125. The attribute's comment: “coordinate_morphism”. References: EGA I (5.5.11), “morphism to Spec k[t]”; SGA 6 II (2.2.7.2), “more general”.

The coordinate maps on the two charts of affine space with doubled origin glue to a scheme morphism to affine space, restricting to the identity on each chart.

noncomputable def coordinateMorphismData (k : Type u) [Field k] (n : ℕ) :
    { f : affineSpaceWithDoubledZero k n ⟶
        Spec (.of (MvPolynomial (Fin n) k)) //
      ∀ i : Fin 2,
        chartInclusion k n i ≫ f = 𝟙 _ }

AlgebraicGeometry.coordinateMorphism_map_origin, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/DoubledOrigin.lean, line 161. The attribute's comment: “origins_map_to_origin”. References: EGA I (5.5.11), “two origins over 0”.

The coordinate morphism maps the origin of each affine chart to the origin of affine space.

theorem coordinateMorphism_map_origin (k : Type u) [Field k] (n : ℕ)
    (i : Fin 2) :
    coordinateMorphism k n
        (chartInclusion k n i
          (affineOrigin k n)) = affineOrigin k n

AlgebraicGeometry.intersection_iso_puncturedAffinePlane, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/DoubledOriginIntersection.lean, line 153. The attribute's comment: “non_affine_intersection”.

In dimension two, the overlap of the two affine charts of the doubled-origin scheme is the punctured affine plane.

theorem intersection_iso_puncturedAffinePlane (S : PuncturedAffinePlane.{u}) :
    Nonempty (((chartInclusion S.k 2 0).opensRange ⊓
      (chartInclusion S.k 2 1).opensRange).toScheme ≅ S.puncturedScheme)

AlgebraicGeometry.not_isAffineOpen_chartIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/DoubledOriginIntersection.lean, line 162. The attribute's comment: “non_affine_intersection”.

For dimension greater than one, the two affine charts of affine space with doubled origin have a non-affine intersection.

theorem not_isAffineOpen_chartIntersection (k : Type u) [Field k] (n : ℕ)
    (hn : 1 < n) :
    ¬ IsAffineOpen ((chartInclusion k n 0).opensRange ⊓
      (chartInclusion k n 1).opensRange)

AlgebraicGeometry.exists_affineOpens_nonaffine_inf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/DoubledOriginIntersection.lean, line 174. The attribute's comment: “non_affine_intersection”.

The intersection of two affine opens in a scheme need not be affine.

theorem exists_affineOpens_nonaffine_inf :
    ∃ (X : Scheme.{u}) (U V : X.Opens),
      IsAffineOpen U ∧ IsAffineOpen V ∧ ¬ IsAffineOpen (U ⊓ V)

AlgebraicGeometry.infinite_irreducibleClosed_closures, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/DoubledOriginPoints.lean, line 132. The attribute's comment: “many_irreducible_closed”.

In dimension greater than one, infinitely many irreducible closed subsets of affine space with doubled origin are closures of nonclosed points in its first affine chart.

theorem infinite_irreducibleClosed_closures (k : Type u) [Field k] (n : ℕ) (hn : 1 < n) :
    Set.Infinite
      { T : Set (affineSpaceWithDoubledZero k n) |
        IsClosed T ∧ IsIrreducible T ∧
          ∃ x : Spec (.of (MvPolynomial (Fin n) k)),
            ¬ IsClosed ({x} : Set (Spec (.of (MvPolynomial (Fin n) k)))) ∧
              T = closure ({(chartInclusion k n 0).base x} :
                Set (affineSpaceWithDoubledZero k n)) }

AlgebraicGeometry.mem_origin_iff_mem_origin, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/DoubledOriginPoints.lean, line 264. The attribute's comment: “origins_in_closed_subset”.

Apart from the two singleton origins, an irreducible closed subset of affine space with the origin doubled contains either both origins or neither.

theorem mem_origin_iff_mem_origin (k : Type u) [Field k] (n : ℕ)
    (T : Set (affineSpaceWithDoubledZero k n))
    (hT : IsIrreducible T) (hT_closed : IsClosed T)
    (hT₀ : T ≠ {chartInclusion k n 0 (affineOrigin k n)})
    (hT₁ : T ≠ {chartInclusion k n 1 (affineOrigin k n)}) :
    (chartInclusion k n 0 (affineOrigin k n) ∈ T ↔
      chartInclusion k n 1 (affineOrigin k n) ∈ T)

AlgebraicGeometry.isIso_coordinateMorphism_globalSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/DoubledOriginSections.lean, line 146. The attribute's comment: “global_sections”. References: EGA I (5.5.11), “more general”; SGA 6 II (2.2.7.2), “more general”.

In positive dimension, every global function on affine space with doubled origin is induced uniquely by a polynomial via the coordinate morphism.

theorem isIso_coordinateMorphism_globalSections (k : Type u) [Field k]
    (n : ℕ) (hn : 0 < n) :
    IsIso ((Scheme.ΓSpecIso (.of (MvPolynomial (Fin n) k))).inv ≫
      (coordinateMorphism k n).appTop)

AlgebraicGeometry.not_isAffine_affineSpaceWithDoubledZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/DoubledOriginSections.lean, line 176. The attribute's comment: “not_affine”.

Affine space of positive dimension with its origin doubled is not affine.

theorem not_isAffine_affineSpaceWithDoubledZero (k : Type u) [Field k]
    (n : ℕ) (hn : 0 < n) :
    ¬ IsAffine (affineSpaceWithDoubledZero k n)

Declarations registered for the tag:

Tag 01JE, an example

Tag 01JE in the Stacks Project.

AlgebraicGeometry.projectiveLineInversionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLine.lean, line 83. The attribute's comment: “projective_line_gluing”. References: EGA I (2.3.2), “partial”.

The isomorphism φ₁₂ of the gluing datum: the automorphism of the punctured affine line induced by T ↦ T⁻¹, which is the identification y = 1/x of the two coordinates on the overlap.

noncomputable def projectiveLineInversionIso :
    Spec (.of (LaurentPolynomial k)) ≅ Spec (.of (LaurentPolynomial k))

AlgebraicGeometry.projectiveLineGluingData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLine.lean, line 126. The attribute's comment: “projective_line_gluing”.

The gluing datum for the projective line: two copies of Spec k[X], glued along D(X) = Spec k[T,T⁻¹] by inversion.

noncomputable def projectiveLineGluingData : Scheme.GlueData.{u}

AlgebraicGeometry.projectiveLine, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLine.lean, line 136. The attribute's comment: “projective_line_gluing”. References: EGA I (2.3.2), “gluing construction”.

The projective line over k, constructed by gluing its two standard affine charts.

noncomputable abbrev projectiveLine : Scheme.{u}

AlgebraicGeometry.projectiveLineZero, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLine.lean, line 216. The attribute's comment: “projective_line_gluing”.

The point 0 of the projective line, namely the point (X) in the x-chart.

def projectiveLineZero [IsDomain k] : projectiveLine k

AlgebraicGeometry.projectiveLineInfinity, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLine.lean, line 221. The attribute's comment: “projective_line_gluing”. References: EGA II (7.4.14).

The point ∞ of the projective line, namely the point (X) in the y-chart.

def projectiveLineInfinity [IsDomain k] : projectiveLine k

AlgebraicGeometry.affineLineOne, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLineAffineOpen.lean, line 162. The attribute's comment: “projective_line_one”.

The point 1 of an affine-line chart, represented by the prime ideal (X - 1).

def affineLineOne : Spec (.of (Polynomial k))

AlgebraicGeometry.projectiveLineOne, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLineAffineOpen.lean, line 185. The attribute's comment: “projective_line_one”.

The point 1 of the projective line, namely the point (x - 1) in the x-chart.

def projectiveLineOne : projectiveLine k

AlgebraicGeometry.projectiveLineYChart_affineLineOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLineAffineOpen.lean, line 190. The attribute's comment: “projective_line_one”.

The point 1 is also the point (y - 1) of the second chart.

theorem projectiveLineYChart_affineLineOne :
    projectiveLineYChart k (affineLineOne k) = projectiveLineOne k

AlgebraicGeometry.projectiveLineSChart, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLineAffineOpen.lean, line 1075. The attribute's comment: “projective_line_affine_open_through_zero_and_infinity”.

The third chart of the projective line: the affine line with coordinate s = 1/(x-1) = y/(1-y), mapping onto the complement of the point 1.

def projectiveLineSChart : Spec (.of (Polynomial k)) ⟶ projectiveLine k

AlgebraicGeometry.projectiveLineSXPiece_comp_projectiveLineSChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLineAffineOpen.lean, line 1082. The attribute's comment: “projective_line_affine_open_coordinate_ring”.

On D(x-1) ⊂ X₁ the third chart is the inclusion of that open into the first chart; equivalently, s restricts to 1/(x-1) there.

theorem projectiveLineSXPiece_comp_projectiveLineSChart :
    projectiveLineSXPiece k ≫ projectiveLineSChart k =
      Spec.map (CommRingCat.ofHom (algebraMap (Polynomial k) (affineLineAwayOne k))) ≫
        projectiveLineXChart k

AlgebraicGeometry.projectiveLineSYPiece_comp_projectiveLineSChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLineAffineOpen.lean, line 1091. The attribute's comment: “projective_line_affine_open_coordinate_ring”.

On D(y-1) ⊂ X₂ the third chart is the inclusion of that open into the second chart; equivalently, s restricts to y/(1-y) there.

theorem projectiveLineSYPiece_comp_projectiveLineSChart :
    projectiveLineSYPiece k ≫ projectiveLineSChart k =
      Spec.map (CommRingCat.ofHom (algebraMap (Polynomial k) (affineLineAwayOne k))) ≫
        projectiveLineYChart k

AlgebraicGeometry.range_projectiveLineSChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLineAffineOpen.lean, line 1345. The attribute's comment: “projective_line_affine_open_through_zero_and_infinity”.

The image of the third chart is exactly the complement of the point 1: U = ℙ¹ \ {1}.

theorem range_projectiveLineSChart :
    Set.range (projectiveLineSChart k).base = {projectiveLineOne k}ᶜ

AlgebraicGeometry.isAffineOpen_projectiveLineSChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLineAffineOpen.lean, line 1376. The attribute's comment: “projective_line_affine_open_through_zero_and_infinity”.

U = ℙ¹ \ {1} is an affine open.

theorem isAffineOpen_projectiveLineSChart :
    IsAffineOpen (projectiveLineSChart k).opensRange

AlgebraicGeometry.projectiveLineZero_mem_opensRange_projectiveLineSChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLineAffineOpen.lean, line 1382. The attribute's comment: “projective_line_affine_open_through_zero_and_infinity”.

The point 0 lies in U = ℙ¹ \ {1}.

theorem projectiveLineZero_mem_opensRange_projectiveLineSChart :
    projectiveLineZero k ∈ (projectiveLineSChart k).opensRange

AlgebraicGeometry.projectiveLineInfinity_mem_opensRange_projectiveLineSChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLineAffineOpen.lean, line 1393. The attribute's comment: “projective_line_affine_open_through_zero_and_infinity”.

The point ∞ lies in U = ℙ¹ \ {1}.

theorem projectiveLineInfinity_mem_opensRange_projectiveLineSChart :
    projectiveLineInfinity k ∈ (projectiveLineSChart k).opensRange

AlgebraicGeometry.projectiveLineSChartIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLineAffineOpen.lean, line 1408. The attribute's comment: “projective_line_affine_open_coordinate_ring”.

U = ℙ¹ \ {1} is isomorphic to Spec k[s], and so Γ(U, O_U) = k[s].

def projectiveLineSChartIso :
    Spec (.of (Polynomial k)) ≅ ((projectiveLineSChart k).opensRange).toScheme

AlgebraicGeometry.projectiveLineSChartSectionsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLineAffineOpen.lean, line 1422. The attribute's comment: “projective_line_affine_open_coordinate_ring”.

Γ(U, O_U) is the polynomial ring k[s], for the coordinate s = 1/(x-1) = y/(1-y) of AlgebraicGeometry.affineLineSOnXChart and AlgebraicGeometry.affineLineSOnYChart.

def projectiveLineSChartSectionsIso :
    CommRingCat.of (Polynomial k) ≅ Γ(((projectiveLineSChart k).opensRange).toScheme, ⊤)

AlgebraicGeometry.mem_range_projectiveLinePuncturedChart_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLinePoints.lean, line 66. The attribute's comment: “projective_line_overlap”.

The overlap U₁₂ of the two charts of the projective line, seen in the first chart, is D(x), the locus where the coordinate is invertible.

theorem mem_range_projectiveLinePuncturedChart_iff (y : Spec (.of (Polynomial k))) :
    y ∈ Set.range (projectiveLinePuncturedChart k).base ↔
      (Polynomial.X : Polynomial k) ∉ y.asIdeal

AlgebraicGeometry.mem_range_projectiveLineOverlapYInclusion_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLinePoints.lean, line 80. The attribute's comment: “projective_line_overlap”.

The overlap U₂₁ of the two charts of the projective line, seen in the second chart, is D(y), the locus where the coordinate of that chart is invertible.

theorem mem_range_projectiveLineOverlapYInclusion_iff (y : Spec (.of (Polynomial k))) :
    y ∈ Set.range (projectiveLineOverlapYInclusion k).base ↔
      (Polynomial.X : Polynomial k) ∉ y.asIdeal

AlgebraicGeometry.eq_affineLineOrigin_of_X_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLinePoints.lean, line 106. The attribute's comment: “projective_line_overlap”.

The complement of the overlap in a chart is the single point 0 of that chart: the only point of the affine line over a field at which the coordinate vanishes is the origin.

theorem eq_affineLineOrigin_of_X_mem (y : Spec (.of (Polynomial k)))
    (hy : (Polynomial.X : Polynomial k) ∈ y.asIdeal) : y = affineLineOrigin k

AlgebraicGeometry.projectiveLineZero_ne_projectiveLineInfinity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLinePoints.lean, line 213. The attribute's comment: “projective_line_gluing”.

The points 0 and ∞ of the projective line are distinct.

theorem projectiveLineZero_ne_projectiveLineInfinity (k : Type u) [Field k] :
    projectiveLineZero k ≠ projectiveLineInfinity k

AlgebraicGeometry.infinite_projectiveLine, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLinePoints.lean, line 262. The attribute's comment: “projective_line_infinite”.

The projective line over a field is infinite.

instance infinite_projectiveLine (k : Type u) [Field k] : Infinite (projectiveLine k)

AlgebraicGeometry.isIso_constantsToGlobalSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLineSections.lean, line 155. The attribute's comment: “projective_line_global_sections”. References: EGA I (2.3.2), “Γ(X,O_X) ≅ K”.

The canonical map from k to the global sections of the structure sheaf on the projective line over k is an isomorphism.

theorem isIso_constantsToGlobalSections (k : Type u) [CommRing k] :
    IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫
      (projectiveLine k ↘ Spec (.of k)).appTop)

AlgebraicGeometry.not_isAffine_projectiveLine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLineSections.lean, line 212. The attribute's comment: “projective_line_not_affine”. References: EGA I (2.3.2), “X not affine”.

The projective line over a field is not affine.

theorem not_isAffine_projectiveLine (k : Type u) [Field k] :
    ¬ IsAffine (projectiveLine k)
Sources
LeanAlgebraicGeometry.isPushout_opens_ι_of_sup_eq_top · AlgebraicGeometry.existsUnique_comp_ι_eq_of_sup_eq_top · AlgebraicGeometry.opensRange_pushout_inl_sup_opensRange_pushout_inr · AlgebraicGeometry.preimage_opensRange_pushout_inl · AlgebraicGeometry.isPullback_pushout_inl_inr · AlgebraicGeometry.LocallyRingedSpace.GlueData.range_overlap · AlgebraicGeometry.LocallyRingedSpace.GlueData.t_f_eq_restrictOverlapIso_comp · AlgebraicGeometry.LocallyRingedSpace.GlueData.homOutEquiv

Section26.15 A representability criterion#

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

Tag 01JG, a definition

Tag 01JG in the Stacks Project.

Declarations registered for the tag:

Tag 01JH, an example

Tag 01JH in the Stacks Project.

Declarations registered for the tag:

Tag 01JI, a definition

Tag 01JI in the Stacks Project.

AlgebraicGeometry.Covers, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/FunctorOfPoints.lean, line 68. The attribute's comment: “part (4): covering by subfunctors”.

An indexed family of subfunctors covers a functor if each section belongs, after restriction to an indexed open covering, to the corresponding subfunctor.

public abbrev Covers {C : Type u} [Category.{v} C] (toTop : C ⥤ TopCat.{u'})
    (isOpenImmersion : MorphismProperty C) (F : Cᵒᵖ ⥤ Type w) {I : Type v'}
    (H : I → Subfunctor F) : Prop

Declarations registered for the tag:

Tag 01JJ, a lemma

Tag 01JJ in the Stacks Project.

AlgebraicGeometry.Space.isRepresentable_of_openCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SiteGluing.lean, line 639. The attribute's comment: “big fppf site over a scheme”.

Stacks 01JJ for the big fppf site over S. A sheaf on the big fppf site over S which admits a jointly locally surjective family of relatively representable open immersions from representable presheaves is representable, by an object of that site.

This is the statement Mathlib's AlgebraicGeometry.Scheme.LocalRepresentability.isRepresentable does not give: Mathlib glues in Scheme with no size control, so its representing object need not satisfy the site's size cutoff. The hypothesis on the index type is one set-theoretic condition which makes the glued scheme an object of the site; an at most countable family satisfies it automatically, since uncountable cofinality of the cutoff is a field of AlgebraicGeometry.BigFppfSite. It is not the weakest such condition: AlgebraicGeometry.Space.isRepresentable_of_openCover_of_contains asks only that the glued scheme lie in the site, however that is established.

theorem isRepresentable_of_openCover (hι : #ι < B.cutoff.ord.cof)
    [HasCoproduct fun i => yoneda.obj (X i)]
    (hsurj : Presheaf.IsLocallySurjective (BigFppfOver.topology B S hS) (Sigma.desc f)) :
    G.obj.IsRepresentable
Tag 01JK, a remark

Tag 01JK in the Stacks Project.

AlgebraicGeometry.lrsRepresentableByScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/MorphismsIntoGluing/RepresentableByScheme.lean, line 831.

A Zariski sheaf on locally ringed spaces, covered by subfunctors represented by schemes and relatively represented by open immersions, is itself represented by a scheme.

public theorem lrsRepresentableByScheme
    (F : LocallyRingedSpace.{u}ᵒᵖ ⥤ Type u)
    (hF : Presheaf.IsSheaf lrsZariskiTopology F)
    {I : Type v} [Small.{u} I] (H : I → Subfunctor F)
    (hrep : ∀ i, ∃ S : Scheme.{u}, Nonempty ((H i).toFunctor.RepresentableBy
      S.toLocallyRingedSpace))
    (hopen : ∀ i, (MorphismProperty.presheaf
      lrsIsOpenImmersion.{u}) (H i).ι)
    (hcover : Covers LocallyRingedSpace.forgetToTop
      lrsIsOpenImmersion.{u} F H) :
    ∃ S : Scheme.{u}, Nonempty (F.RepresentableBy S.toLocallyRingedSpace)
Sources
LeanCategoryTheory.Functor.IsRepresentable · AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv · AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp · AlgebraicGeometry.Covers · CategoryTheory.Presheaf.IsSheaf · CategoryTheory.Subfunctor · CategoryTheory.MorphismProperty.presheaf · AlgebraicGeometry.Space.isRepresentable_of_openCover

Section26.16 Existence of fibre products of schemes#

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

Tag 01JM, a lemma

Tag 01JM in the Stacks Project.

Declarations registered for the tag:

Tag 01JN, a remark

Tag 01JN in the Stacks Project.

AlgebraicGeometry.Scheme.isPullback_toLRSHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/LocallyRingedSpaceFibreProduct.lean, line 477.

The fibre product of two morphisms of schemes, formed in Scheme, is already the fibre product in locally ringed spaces. Neither leg of the cospan is assumed to be an open immersion.

theorem isPullback_toLRSHom {X Y S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S) :
    IsPullback (pullback.fst f g).toLRSHom (pullback.snd f g).toLRSHom f.toLRSHom g.toLRSHom

AlgebraicGeometry.LocallyRingedSpace.hasPullback_of_scheme, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/LocallyRingedSpaceFibreProduct.lean, line 518.

The fibre product of two morphisms of schemes exists in the category of locally ringed spaces.

instance hasPullback_of_scheme {X Y S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S) :
    HasPullback f.toLRSHom g.toLRSHom
Sources
LeanAlgebraicGeometry.instHasFiniteLimitsScheme · AlgebraicGeometry.specZIsTerminal · AlgebraicGeometry.Scheme.Pullback.instHasPullbacks · AlgebraicGeometry.Scheme.isPullback_toLRSHom · AlgebraicGeometry.LocallyRingedSpace.hasPullback_of_scheme

Section26.17 Fibre products of schemes#

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

Tag 01JP, a definition

Tag 01JP in the Stacks Project.

Declarations registered for the tag:

Tag 01JQ, a lemma

Tag 01JQ in the Stacks Project.

Declarations registered for the tag:

Tag 01JR, a lemma

Tag 01JR in the Stacks Project.

Declarations registered for the tag:

Tag 01JS, a lemma

Tag 01JS in the Stacks Project.

AlgebraicGeometry.Scheme.Pullback.isAffine_openCoverOfBase_bind_openCoverOfLeftRight, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/AffineFibreProductCover.lean, line 35. References: EGA III (6.5.2), “more general”; EGA III (6.6.4), “partial”.

Every member of the open cover of a fibre product assembled from affine open covers over an affine open cover of the base is affine.

theorem isAffine_openCoverOfBase_bind_openCoverOfLeftRight
    {X Y S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S)
    (𝒰 : Scheme.OpenCover.{v} S)
    (𝒱 : ∀ i : 𝒰.I₀, Scheme.OpenCover.{w} (pullback f (𝒰.f i)))
    (𝒲 : ∀ i : 𝒰.I₀, Scheme.OpenCover.{t} (pullback g (𝒰.f i)))
    (h𝒰 : ∀ i, IsAffine (𝒰.X i))
    (h𝒱 : ∀ i j, IsAffine ((𝒱 i).X j))
    (h𝒲 : ∀ i k, IsAffine ((𝒲 i).X k)) :
    ∀ a : ((Scheme.Pullback.openCoverOfBase 𝒰 f g).bind fun i =>
      Scheme.Pullback.openCoverOfLeftRight (𝒱 i) (𝒲 i)
        (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i))).I₀,
      IsAffine (((Scheme.Pullback.openCoverOfBase 𝒰 f g).bind fun i =>
        Scheme.Pullback.openCoverOfLeftRight (𝒱 i) (𝒲 i)
          (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i))).X a)
Tag 01JT, a lemma

Tag 01JT in the Stacks Project.

AlgebraicGeometry.Scheme.Pullback.isIso_residueFieldMap_specTensorTo_comp_residueFieldIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/BaseChange/Points.lean, line 78. The attribute's comment: “residue fields”.

Stacks Project, Tag 01JT (residue fields). For a point of the fibre product represented by a prime p of κ(x) ⊗[κ(s)] κ(y), the canonical map from the residue field of the corresponding point to the residue field at p is an isomorphism.

public theorem isIso_residueFieldMap_specTensorTo_comp_residueFieldIso
    (T : Scheme.Pullback.Triplet f g) (p : Spec T.tensor) :
    IsIso (T.SpecTensorTo.residueFieldMap p ≫
      (Scheme.Spec.residueFieldIso T.tensor p).hom)

Declarations registered for the tag:

Tag 01JU, a lemma

Tag 01JU in the Stacks Project.

Stacks.ClosedImmersion.existsUnique_idealSheaf_pullbackSnd_iso_pullbackIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Immersion/BaseChange.lean, line 226. The attribute's comment: “part (1): inverse-image ideal”.

Stacks Project, Tag 01JU, part (1). Let f : X ⟶ S be a closed immersion of schemes corresponding to the sheaf of ideals i : I ⟶ 𝒪_S, and let g : Y ⟶ S be any morphism of schemes. Then the base change X ×_S Y ⟶ Y, which is a closed immersion by AlgebraicGeometry.IsClosedImmersion.isStableUnderBaseChange, corresponds to the inverse-image ideal Im(g^* I ⟶ 𝒪_Y): its ideal sheaf is that ideal, by a unique isomorphism compatible with the two inclusions into 𝒪_Y.

theorem existsUnique_idealSheaf_pullbackSnd_iso_pullbackIdeal {X Y S : Scheme.{u}} (f : X ⟶ S)
    (g : Y ⟶ S) [hcl : AlgebraicGeometry.IsClosedImmersion f]
    (I : SheafOfModules.{u} (structureSheafRing S.toLocallyRingedSpace.toRingedSpace))
    (i : I ⟶ SheafOfModules.unit (structureSheafRing S.toLocallyRingedSpace.toRingedSpace))
    (e : I ≅ idealSheaf f.toLRSHom.toShHom)
    (he : e.hom ≫ kernel.ι (SheafOfModules.unitToPushforwardObjUnit
      (structureSheafHom f.toLRSHom.toShHom)) = i) :
    ∃! e' : idealSheaf (pullback.snd f g).toLRSHom.toShHom ≅ pullbackIdeal g.toLRSHom I i,
      e'.hom ≫ pullbackIdealInclusion g.toLRSHom I i =
        kernel.ι (SheafOfModules.unitToPushforwardObjUnit
          (structureSheafHom (pullback.snd f g).toLRSHom.toShHom))

Declarations registered for the tag:

Tag 01JV, a definition

Tag 01JV in the Stacks Project.

Declarations registered for the tag:

Sources
LeanCategoryTheory.Limits.pullback · CategoryTheory.Limits.pullback.fst · CategoryTheory.Limits.pullback.snd · CategoryTheory.Limits.pullbackIsPullback · AlgebraicGeometry.Scheme.Pullback.isAffine_of_isAffine_isAffine_isAffine · AlgebraicGeometry.Scheme.pullback_map_isOpenImmersion · AlgebraicGeometry.Scheme.Pullback.range_map · AlgebraicGeometry.Scheme.Pullback.isAffine_openCoverOfBase_bind_openCoverOfLeftRight

Section26.18 Base change in algebraic geometry#

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

Tag 01JX, a definition

Tag 01JX in the Stacks Project.

Declarations registered for the tag:

Tag 01JY, a lemma

Tag 01JY in the Stacks Project.

Declarations registered for the tag:

Tag 01JZ, a definition

Tag 01JZ in the Stacks Project.

CategoryTheory.IsStableUnderBaseChange, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/BaseChange/Stability.lean, line 62. The attribute's comment: “part (1): properties of objects over a base”.

A family of properties of objects over a base is stable under base change if the property passes across every pullback square.

public class IsStableUnderBaseChange
    (P : (S : C) → ObjectProperty (Over S)) : Prop

CategoryTheory.MorphismPropertyOverBase.IsStableUnderBaseChange, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/BaseChange/Stability.lean, line 85. The attribute's comment: “part (2): properties of morphisms over a base”. References: EGA I (3.5.1), “more general”; EGA I (5.5.12); SGA 3 VIB (2.0), “stable under base change”; SGA 3 IV (4.7), “more general”; SGA 3 VIB (10.1).

A family of properties of morphisms over a base is stable under arbitrary base change if it passes across every pair of pullback squares defining the base change of a morphism.

public class IsStableUnderBaseChange : Prop

Declarations registered for the tag:

Tag 01K0, a definition

Tag 01K0 in the Stacks Project.

Declarations registered for the tag:

Tag 01K1, a lemma

Tag 01K1 in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isEmbedding_fiberι_and_pullbackSnd_fromSpecStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/EmbeddingOverPoint.lean, line 43.

Let f : X ⟶ S be a morphism of schemes and s ∈ S. Both the inclusion of the fibre X_s = X ×_S Spec κ(s) ⟶ X and the projection Spec 𝒪_{S,s} ×_S X ⟶ X are homeomorphisms onto their images.

theorem isEmbedding_fiberι_and_pullbackSnd_fromSpecStalk {X S : Scheme.{u}} (f : X ⟶ S)
    (s : S) :
    IsEmbedding (f.fiberι s) ∧ IsEmbedding (pullback.snd (S.fromSpecStalk s) f)

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.Scheme.Over · AlgebraicGeometry.Scheme.Hom.IsOver · AlgebraicGeometry.Scheme.Hom.isOver_iff · AlgebraicGeometry.Scheme.asOver · AlgebraicGeometry.Scheme.canonicallyOverPullback · CategoryTheory.Over.pullback · AlgebraicGeometry.IsImmersion.isStableUnderBaseChange · AlgebraicGeometry.IsClosedImmersion.isStableUnderBaseChange

Section26.19 Quasi-compact morphisms#

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

Tag 01K3, a definition

Tag 01K3 in the Stacks Project.

Declarations registered for the tag:

Tag 01K4, a lemma

Tag 01K4 in the Stacks Project.

AlgebraicGeometry.quasiCompact_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiCompactAffineCover.lean, line 44.

For a morphism of schemes f : X ⟶ S the following are equivalent: 1. f is quasi-compact; 2. the preimage of every affine open of S is quasi-compact; 3. there is a covering S = ⋃ᵢ Uᵢ by affine opens such that every f⁻¹(Uᵢ) is quasi-compact.

theorem quasiCompact_tfae {X S : Scheme.{u}} (f : X ⟶ S) :
    List.TFAE [QuasiCompact f,
      ∀ U : S.Opens, IsAffineOpen U → IsCompact (f ⁻¹ᵁ U : Set X),
      ∃ (ι : Type u) (U : ι → S.Opens), (∀ i, IsAffineOpen (U i)) ∧ iSup U = ⊤ ∧
        ∀ i, IsCompact (f ⁻¹ᵁ U i : Set X)]

Declarations registered for the tag:

Tag 01K5, a lemma

Tag 01K5 in the Stacks Project.

Declarations registered for the tag:

  • AlgebraicGeometry.quasiCompact_isStableUnderBaseChange registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch26.lean, line 216 (StacksFrontier). References: EGA I (6.3.4), “clause (iv)”; EGA I (6.6.4); EGA III (6.9.1), “partial”; EGA III (6.9.4), “more general”; EGA III (7.7.2), “quasi-compactness of f'”; EGA IV (1.1.2); EGA IV (2.3.7), “(i)”; EGA IV (2.6.4), “necessity in (v)”; SGA 1 VIII (3.3), “quasi-compact clause”; SGA 4 VI (1.8), “(ii), special case”; SGA 4 VI (1.9.1), “(ii), special case”; SGA 4 VIII (5.1), “partial”; SGA 7 VII (1.3.8), “partial”.
Tag 01K6, a lemma

Tag 01K6 in the Stacks Project.

Declarations registered for the tag:

Tag 01K7, a lemma

Tag 01K7 in the Stacks Project.

Declarations registered for the tag:

Tag 01K8, an example

Tag 01K8 in the Stacks Project.

AlgebraicGeometry.puncturedInfiniteAffineSpace_carrier, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/QuasiCompact.lean, line 79. The attribute's comment: “the punctured spectrum”.

The union of the coordinate basic opens is precisely the complement of the origin.

public theorem puncturedInfiniteAffineSpace_carrier (k : Type u) [Field k] :
    (puncturedInfiniteAffineSpace k : Set (infiniteAffineSpace k)) =
      {p : PrimeSpectrum (MvPolynomial ℕ k) |
        p.asIdeal ≠ Ideal.span (Set.range (MvPolynomial.X : ℕ → MvPolynomial ℕ k))}

AlgebraicGeometry.puncturedInfiniteAffineSpace_ι_not_quasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/QuasiCompact.lean, line 98. The attribute's comment: “not quasi-compact”.

The open immersion of the punctured infinite-dimensional affine space is not quasi-compact.

public theorem puncturedInfiniteAffineSpace_ι_not_quasiCompact (k : Type u) [Field k] :
    ¬ QuasiCompact (puncturedInfiniteAffineSpace k).ι
Tag 05JL, a lemma

Tag 05JL in the Stacks Project.

AlgebraicGeometry.isClosed_range_iff_stableUnderSpecialization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Valuative/Specialization.lean, line 207.

The image of a quasi-compact morphism of schemes is closed if and only if it is stable under specialization.

public theorem isClosed_range_iff_stableUnderSpecialization
    {X S : Scheme.{u}} (f : X ⟶ S) [QuasiCompact f] :
    IsClosed (Set.range (f : X → S)) ↔
      StableUnderSpecialization (Set.range (f : X → S))
Sources
LeanAlgebraicGeometry.QuasiCompact · AlgebraicGeometry.quasiCompact_tfae · AlgebraicGeometry.quasiCompact_iff_forall_isAffineOpen · AlgebraicGeometry.quasiCompact_isStableUnderBaseChange · AlgebraicGeometry.quasiCompact_comp · AlgebraicGeometry.instUniversallyClosedOfIsClosedImmersion · AlgebraicGeometry.instQuasiCompactOfUniversallyClosed · AlgebraicGeometry.puncturedInfiniteAffineSpace_carrier

Section26.20 Valuative criterion for universal closedness#

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

Tag 01KB, a definition

Tag 01KB in the Stacks Project.

Declarations registered for the tag:

Tag 01KC, a lemma

Tag 01KC in the Stacks Project.

Declarations registered for the tag:

Tag 01KD, a definition

Tag 01KD in the Stacks Project.

Declarations registered for the tag:

Tag 01J8, a lemma

Tag 01J8 in the Stacks Project.

AlgebraicGeometry.exists_valuation_ring_of_specializes, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Valuative/Specialization.lean, line 49.

A specialization of points of a scheme is witnessed by a valuation ring. The valuation ring may be chosen so that the residue-field extension at its generic point is any prescribed extension.

public lemma exists_valuation_ring_of_specializes (S : AlgebraicGeometry.Scheme.{u})
    {s' s : S} (h : s' ⤳ s) (K : Type u) [Field K]
    (i : S.residueField s' ⟶ CommRingCat.of K) :
    ∃ (A : Type u) (_ : CommRing A) (_ : IsDomain A) (_ : ValuationRing A)
      (f : AlgebraicGeometry.Spec (.of A) ⟶ S)
      (e : (AlgebraicGeometry.Spec (.of A)).residueField
        (genericPoint (AlgebraicGeometry.Spec (.of A))) ≅ CommRingCat.of K)
      (hη : f (genericPoint (AlgebraicGeometry.Spec (.of A))) = s'),
      f (closedPoint A) = s ∧
        (S.residueFieldCongr hη).inv ≫
          f.residueFieldMap (genericPoint (AlgebraicGeometry.Spec (.of A))) ≫ e.hom = i
Tag 01KG, an example

Tag 01KG in the Stacks Project.

AlgebraicGeometry.projectiveLine_valuativeCriterion_existence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLineUniversallyClosed.lean, line 127. The attribute's comment: “valuative extension”.

Every valuative square for the structure morphism of the projective line has a diagonal lift.

theorem projectiveLine_valuativeCriterion_existence (k : Type u) [CommRing k] :
    ValuativeCriterion.Existence
      (projectiveLine k ↘ Spec (.of k))

AlgebraicGeometry.projectiveLine_quasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLineUniversallyClosed.lean, line 346. The attribute's comment: “quasi-compactness”.

The structure morphism of the projective line is quasi-compact.

theorem projectiveLine_quasiCompact (k : Type u) [CommRing k] :
    QuasiCompact (projectiveLine k ↘ Spec (.of k))

AlgebraicGeometry.projectiveLine_universallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLineUniversallyClosed.lean, line 353. The attribute's comment: “universal closedness”.

The structure morphism of the projective line is universally closed.

theorem projectiveLine_universallyClosed (k : Type u) [CommRing k] :
    UniversallyClosed (projectiveLine k ↘ Spec (.of k))
Sources
LeanAlgebraicGeometry.UniversallyClosed · AlgebraicGeometry.universallyClosed_eq_universallySpecializing · AlgebraicGeometry.ValuativeCriterion.Existence · AlgebraicGeometry.ValuativeCriterion.Uniqueness · AlgebraicGeometry.exists_valuation_ring_of_specializes · AlgebraicGeometry.projectiveLine_valuativeCriterion_existence · AlgebraicGeometry.projectiveLine_quasiCompact · AlgebraicGeometry.projectiveLine_universallyClosed

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.