26.21 Separation axioms to 26.24 Functoriality for…

Section26.21 Separation axioms#

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

Tag 01KI, a lemma

Tag 01KI in the Stacks Project.

Declarations registered for the tag:

Tag 01KK, a definition

Tag 01KK in the Stacks Project.

Declarations registered for the tag:

Tag 01KL, an example

Tag 01KL in the Stacks Project.

AlgebraicGeometry.structureMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Separation/DoubledOrigin.lean, line 193. The attribute's comment: “structure_morphism”.

The structure morphism of infinite-dimensional affine space with doubled origin, restricting on both charts to the canonical affine-space morphism.

public noncomputable def structureMorphism {k : Type u} [CommRing k]
    (D : DoubledOriginData k) :
    { f : D.scheme ⟶ Spec (.of k) //
      ∀ i : Fin 2,
        D.chart i ≫ f = Spec.map (CommRingCat.ofHom (MvPolynomial.C :
          k →+* MvPolynomial ℕ k)) }

AlgebraicGeometry.diagonal_preimage_mixedCharts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Separation/DoubledOrigin.lean, line 363. The attribute's comment: “diagonal_inverse_image”.

The diagonal inverse image of the product of the two affine charts is the punctured affine space, embedded in the doubled-origin scheme through its first chart.

public theorem diagonal_preimage_mixedCharts {k : Type u} [CommRing k]
    (D : DoubledOriginData k) {S : Scheme.{u}} (f : D.scheme ⟶ S) :
    (pullback.diagonal f) ⁻¹'
        ((pullback.fst f f) ⁻¹' Set.range (D.chart 0) ∩
          (pullback.snd f f) ⁻¹' Set.range (D.chart 1)) =
      Set.range ((puncturedInfiniteAffineSpace k).ι ≫ D.chart 0)

AlgebraicGeometry.structureMorphism_not_quasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Separation/DoubledOrigin.lean, line 439. The attribute's comment: “not_quasi_separated”.

The structure morphism of a doubled-origin infinite-dimensional affine space over a field is not quasi-separated.

public theorem structureMorphism_not_quasiSeparated {k : Type u} [Field k]
    (D : DoubledOriginData k) :
    ¬ QuasiSeparated (structureMorphism D).1

AlgebraicGeometry.puncturedSpectrum_not_isCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Separation/PuncturedAffineSpace.lean, line 72. The attribute's comment: “punctured_spectrum_not_quasi_compact”.

The complement of the origin in countably infinite-dimensional affine space over a field is not quasi-compact.

public theorem puncturedSpectrum_not_isCompact (k : Type*) [Field k] :
    ¬ IsCompact {p : PrimeSpectrum (MvPolynomial ℕ k) |
      p.asIdeal ≠ Ideal.span (Set.range (MvPolynomial.X : ℕ → MvPolynomial ℕ k))}

AlgebraicGeometry.doubledOriginDatum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ObstructionIX/DoubledOriginDatum.lean, line 196. The attribute's comment: “doubled_origin_scheme”.

Stacks Project, Tag 01KL. Countably infinite-dimensional affine space with its origin doubled, as a DoubledOriginData: the canonical gluing data of two copies of the affine space, together with the identifications of its charts and overlaps with the standard models.

public def doubledOriginDatum : DoubledOriginData k

Declarations registered for the tag:

Tag 01KO, a lemma

Tag 01KO in the Stacks Project.

AlgebraicGeometry.quasiSeparated_iff_isCompact_inf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/QuasiSeparated.lean, line 124. The attribute's comment: “conditions (1) and (2)”.

A morphism f : X ⟶ S is quasi-separated if and only if for every pair of affine opens U, V of X which map into a common affine open W of S, the intersection U ∩ V is quasi-compact.

public theorem quasiSeparated_iff_isCompact_inf {X S : Scheme.{u}} (f : X ⟶ S) :
    QuasiSeparated f ↔
      ∀ (W : S.Opens), IsAffineOpen W → ∀ U ≤ f ⁻¹ᵁ W, ∀ V ≤ f ⁻¹ᵁ W,
        IsAffineOpen U → IsAffineOpen V → IsCompact ((U ⊓ V : X.Opens) : Set X)

AlgebraicGeometry.quasiSeparated_iff_finite_iSup_affineOpens, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/QuasiSeparated.lean, line 136. The attribute's comment: “condition (2), as a finite union of affine opens”.

A morphism f : X ⟶ S is quasi-separated if and only if for every pair of affine opens U, V of X which map into a common affine open of S, the intersection U ∩ V is a finite union of affine opens of X.

public theorem quasiSeparated_iff_finite_iSup_affineOpens {X S : Scheme.{u}} (f : X ⟶ S) :
    QuasiSeparated f ↔
      ∀ (W : S.Opens), IsAffineOpen W → ∀ U ≤ f ⁻¹ᵁ W, ∀ V ≤ f ⁻¹ᵁ W,
        IsAffineOpen U → IsAffineOpen V →
        ∃ s : Set X.affineOpens, s.Finite ∧ (U ⊓ V : X.Opens) = ⨆ i ∈ s, (i : X.Opens)

AlgebraicGeometry.quasiSeparated_of_openCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/QuasiSeparated.lean, line 150. The attribute's comment: “condition (3) implies (1)”.

Given an affine open covering 𝒰 of S and, for each i, an affine open covering 𝒱 i of f ⁻¹ U i, if every fibre product V j ×_{U i} V k is quasi-compact then f is quasi-separated.

public theorem quasiSeparated_of_openCover {X S : Scheme.{u}} (f : X ⟶ S)
    (𝒰 : Scheme.OpenCover.{v} S) [∀ i, IsAffine (𝒰.X i)]
    (𝒱 : ∀ i, Scheme.OpenCover.{w} (pullback f (𝒰.f i))) [∀ i j, IsAffine ((𝒱 i).X j)]
    (h : ∀ i j k, CompactSpace (pullback ((𝒱 i).f j) ((𝒱 i).f k) : Scheme.{u})) :
    QuasiSeparated f

AlgebraicGeometry.quasiSeparated_of_isOpenCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/QuasiSeparated.lean, line 164. The attribute's comment: “condition (3) implies (1), for families of opens”.

Given an affine open covering S = ⋃ i, W i and for each i an affine open covering f ⁻¹ (W i) = ⋃ j, V i j, if each intersection V i j ∩ V i k is quasi-compact then f is quasi-separated.

public theorem quasiSeparated_of_isOpenCover {X S : Scheme.{u}} (f : X ⟶ S)
    {ι : Type*} (W : ι → S.Opens) (hW : IsOpenCover W) (hWaff : ∀ i, IsAffineOpen (W i))
    {κ : ι → Type*} (V : ∀ i, κ i → X.Opens) (hV : ∀ i, ⨆ j, V i j = f ⁻¹ᵁ W i)
    (hVaff : ∀ i j, IsAffineOpen (V i j))
    (hVcompact : ∀ i j k, IsCompact ((V i j ⊓ V i k : X.Opens) : Set X)) :
    QuasiSeparated f

AlgebraicGeometry.exists_isOpenCover_of_quasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/QuasiSeparated.lean, line 185. The attribute's comment: “condition (1) implies (3)”.

A quasi-separated morphism admits an affine open covering of the base and an affine open covering of each preimage whose pairwise intersections are quasi-compact; one may take all the affine opens there are.

public theorem exists_isOpenCover_of_quasiSeparated {X S : Scheme.{u}} (f : X ⟶ S)
    [QuasiSeparated f] :
    ∃ (ι : Type u) (W : ι → S.Opens), IsOpenCover W ∧ (∀ i, IsAffineOpen (W i)) ∧
      ∃ (κ : ι → Type u) (V : ∀ i, κ i → X.Opens),
        (∀ i, ⨆ j, V i j = f ⁻¹ᵁ W i) ∧ (∀ i j, IsAffineOpen (V i j)) ∧
        (∀ i j k, IsCompact ((V i j ⊓ V i k : X.Opens) : Set X))
Tag 01KP, a lemma

Tag 01KP in the Stacks Project.

AlgebraicGeometry.sectionTensorMap_surjective_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/Separated.lean, line 357. The attribute's comment: “part (1)(b)”. References: EGA I (5.5.6), “necessity of generation”.

For a separated morphism, the tensor product of sections surjects onto sections of the intersection of compatible affine opens.

public theorem sectionTensorMap_surjective_of_isSeparated {X S : Scheme.{u}}
    (f : X ⟶ S) [IsSeparated f] (U V : X.Opens)
    (hU : IsAffineOpen U) (hV : IsAffineOpen V)
    (W : S.Opens) (hW : IsAffineOpen W)
    (hUW : U ≤ f ⁻¹ᵁ W) (hVW : V ≤ f ⁻¹ᵁ W) :
    Function.Surjective (sectionTensorMap X U V)

AlgebraicGeometry.isSeparated_of_affine_intersections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/Separated.lean, line 388. The attribute's comment: “part (2)”. References: EGA I (5.5.6), “sufficiency”.

Affine neighborhoods of every pair of points in a fiber, with affine intersection and surjective tensor map on sections, imply separatedness.

public theorem isSeparated_of_affine_intersections {X S : Scheme.{u}}
    (f : X ⟶ S)
    (h : ∀ x₁ x₂ : X, f.base x₁ = f.base x₂ →
      ∃ (U V : X.Opens) (W : S.Opens),
        x₁ ∈ U ∧ x₂ ∈ V ∧ IsAffineOpen U ∧ IsAffineOpen V ∧
        IsAffineOpen W ∧ U ≤ f ⁻¹ᵁ W ∧ V ≤ f ⁻¹ᵁ W ∧
        IsAffineOpen (U ⊓ V) ∧ Function.Surjective (sectionTensorMap X U V)) :
    IsSeparated f

Declarations registered for the tag:

Tag 01KQ, an example

Tag 01KQ in the Stacks Project.

AlgebraicGeometry.projectiveLine_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/ProjectiveLineSeparated.lean, line 391.

Stacks Project, Tag 01KQ. The structure morphism of the projective line is separated. This holds over an arbitrary commutative ring, not only over a field.

theorem projectiveLine_isSeparated :
    IsSeparated (projectiveLine k ↘ Spec (.of k))
Tag 01KR, a lemma

Tag 01KR in the Stacks Project.

AlgebraicGeometry.isImmersion_pullbackMapDesc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/MapDescImmersion.lean, line 48. The attribute's comment: “immersion”.

The canonical morphism X ×[T] Y ⟶ X ×[S] Y is an immersion.

theorem isImmersion_pullbackMapDesc : IsImmersion (pullback.mapDesc f g h)

AlgebraicGeometry.isClosedImmersion_pullbackMapDesc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/MapDescImmersion.lean, line 54. The attribute's comment: “closed immersion if T → S is separated”.

If h : T ⟶ S is separated, the canonical morphism X ×[T] Y ⟶ X ×[S] Y is a closed immersion.

theorem isClosedImmersion_pullbackMapDesc [IsSeparated h] :
    IsClosedImmersion (pullback.mapDesc f g h)

AlgebraicGeometry.quasiCompact_pullbackMapDesc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/MapDescImmersion.lean, line 61. The attribute's comment: “quasi-compact if T → S is quasi-separated”.

If h : T ⟶ S is quasi-separated, the canonical morphism X ×[T] Y ⟶ X ×[S] Y is quasi-compact, being a base change of the quasi-compact diagonal of h.

theorem quasiCompact_pullbackMapDesc [QuasiSeparated h] :
    QuasiCompact (pullback.mapDesc f g h)
Tag 01KS, a lemma

Tag 01KS in the Stacks Project.

Declarations registered for the tag:

  • AlgebraicGeometry.IsImmersion.of_comp registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch26.lean, line 272 (StacksFrontier): “the graph X ⟶ X ×_S Y is an immersion: more general, cancellation for immersions, applied to the graph followed by the first projection, which is 𝟙 X”. References: EGA I (5.3.13); EGA I (5.3.14), “more general”; EGA I (5.5.12), “special case”; EGA IV (8.12.2), “more general”; EGA IV (16.2.3), “more general”; SGA 6 VIII (1.3), “(iv)”; SGA 6 VIII (1.8), “partial”.
  • AlgebraicGeometry.IsSeparated.instIsClosedImmersionLiftSchemeId registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch26.lean, line 275 (StacksFrontier): “the graph is a closed immersion if Y is separated over S”. References: EGA I (5.4.2), “special case”; EGA I (5.4.3); EGA I (5.4.5), “j = id_X”.
  • AlgebraicGeometry.QuasiCompact.of_comp registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch26.lean, line 277 (StacksFrontier): “the graph is quasi-compact if Y is quasi-separated over S: more general, cancellation of quasi-compactness against a quasi-separated map, applied to the graph followed by the first projection (quasi-separated as a base change of Y ⟶ S)”. References: EGA I (5.5.12), “(i), special case”; EGA I (6.3.4), “(v)”; EGA I (6.6.4), “more general”; EGA II (8.14.6), “more general”; EGA IV (1.1.2), “more general”; EGA IV (1.2.4); EGA IV (1.5.4), “(v)”; EGA IV (18.12.13), “more general”; SGA 3 VIB (11.1), “partial”; SGA 3 VIB (12.9), “Quasi-compactness of ρ”; SGA 4 VI (1.9.1), “(iv), special case”.
Tag 01KT, a lemma

Tag 01KT in the Stacks Project.

Declarations registered for the tag:

  • AlgebraicGeometry.IsImmersion.of_comp registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch26.lean, line 282 (StacksFrontier): “a section s of f is an immersion: more general, cancellation for immersions, applied to s ≫ f = 𝟙 S”. References: EGA I (5.3.13); EGA I (5.3.14), “more general”; EGA I (5.5.12), “special case”; EGA IV (8.12.2), “more general”; EGA IV (16.2.3), “more general”; SGA 6 VIII (1.3), “(iv)”; SGA 6 VIII (1.8), “partial”.
  • AlgebraicGeometry.IsClosedImmersion.of_comp registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch26.lean, line 285 (StacksFrontier): “s is a closed immersion if f is separated: more general, cancellation for closed immersions against a separated map, applied to s ≫ f = 𝟙 S”. References: EGA I (5.4.4); EGA I (5.4.6), “more general”; EGA I (5.5.12), “(i), special case”; EGA IV (17.9.3), “partial”; SGA 1 II (4.17), “more general”; SGA 3 VIB (5.6.3), “(i) ⇒ (ii)”; SGA 3 VIB (11.18.1), “more general”.
  • AlgebraicGeometry.QuasiCompact.of_comp registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch26.lean, line 288 (StacksFrontier): “s is quasi-compact if f is quasi-separated: more general, cancellation of quasi-compactness against a quasi-separated map, applied to s ≫ f = 𝟙 S”. References: EGA I (5.5.12), “(i), special case”; EGA I (6.3.4), “(v)”; EGA I (6.6.4), “more general”; EGA II (8.14.6), “more general”; EGA IV (1.1.2), “more general”; EGA IV (1.2.4); EGA IV (1.5.4), “(v)”; EGA IV (18.12.13), “more general”; SGA 3 VIB (11.1), “partial”; SGA 3 VIB (12.9), “Quasi-compactness of ρ”; SGA 4 VI (1.9.1), “(iv), special case”.
Tag 01KU, a lemma

Tag 01KU in the Stacks Project.

Declarations registered for the tag:

Tag 01KV, a lemma

Tag 01KV in the Stacks Project.

Declarations registered for the tag:

Tag 03GI, a lemma

Tag 03GI in the Stacks Project.

Declarations registered for the tag:

  • AlgebraicGeometry.QuasiCompact.of_comp registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch26.lean, line 65 (StacksFrontier). References: EGA I (5.5.12), “(i), special case”; EGA I (6.3.4), “(v)”; EGA I (6.6.4), “more general”; EGA II (8.14.6), “more general”; EGA IV (1.1.2), “more general”; EGA IV (1.2.4); EGA IV (1.5.4), “(v)”; EGA IV (18.12.13), “more general”; SGA 3 VIB (11.1), “partial”; SGA 3 VIB (12.9), “Quasi-compactness of ρ”; SGA 4 VI (1.9.1), “(iv), special case”.
Tag 01KN, a lemma

Tag 01KN in the Stacks Project.

Declarations registered for the tag:

Tag 01KW, a lemma

Tag 01KW in the Stacks Project.

AlgebraicGeometry.isAffineOpen_inf_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/Separated.lean, line 443. The attribute's comment: “the intersection is affine”. References: EGA III (6.6.4), “binary intersections”.

Stacks 01KW. For a separated morphism f : X ⟶ S over a separated scheme S, the intersection of two affine opens of X is affine. The hypotheses make X separated over the terminal scheme, so its absolute diagonal is affine.

public theorem isAffineOpen_inf_of_isSeparated {X S : Scheme.{u}} (f : X ⟶ S)
    [IsSeparated f] [S.IsSeparated] {U V : X.Opens}
    (hU : IsAffineOpen U) (hV : IsAffineOpen V) : IsAffineOpen (U ⊓ V)

AlgebraicGeometry.isClosedImmersion_prodLift_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/Separated.lean, line 458. The attribute's comment: “closed subscheme of the absolute product”.

Stacks 01KW. Under the hypotheses, U ∩ V is a closed subscheme of the absolute product U × V, the product being taken over the terminal scheme.

The map exhibiting it is the canonical prod.lift of the two inclusions U ⊓ V ⟶ U and U ⊓ V ⟶ V. It is obtained from the base change pullback U.ι V.ι ⟶ pullback (U.ι ≫ 𝟙\_) (V.ι ≫ 𝟙\_) of the absolute diagonal of X, which is a closed immersion because X is a separated scheme, by transporting along (isPullback_opens_inf U V).isoPullback on the source and prodIsoPullback on the target.

public theorem isClosedImmersion_prodLift_of_isSeparated {X S : Scheme.{u}} (f : X ⟶ S)
    [IsSeparated f] [S.IsSeparated] (U V : X.Opens) :
    IsClosedImmersion (prod.lift (X.homOfLE (inf_le_left : U ⊓ V ≤ U))
      (X.homOfLE (inf_le_right : U ⊓ V ≤ V)))
Tag 01KX, an example

Tag 01KX in the Stacks Project.

AlgebraicGeometry.generalLinearTwoScheme, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Separation/GeneralLinearGroup.lean, line 62. The attribute's comment: “gl2”.

The rank-two general linear scheme over k.

public abbrev generalLinearTwoScheme (k : Type u) [CommRing k] : AlgebraicGeometry.Scheme

AlgebraicGeometry.generalLinearTwoToProjectiveLine, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Separation/GeneralLinearGroupProjectiveLine.lean, line 387. The attribute's comment: “gl2_to_projective_line”.

Stacks Project, Tag 01KX (gl2_to_projective_line). The morphism [a : b] from GL₂ to the projective line, glued from b/a on D(a) and a/b on D(b).

noncomputable def generalLinearTwoToProjectiveLine :
    generalLinearTwoScheme k ⟶ projectiveLine k

AlgebraicGeometry.surjective_generalLinearTwoToProjectiveLine, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Separation/GeneralLinearGroupProjectiveLine.lean, line 455. The attribute's comment: “gl2_to_projective_line_surjective”.

Stacks Project, Tag 01KX (gl2_to_projective_line_surjective). The morphism [a : b] from GL₂ to the projective line is surjective: over the first chart the matrix !![1, X; 0, 1] is a section, and over the second the matrix !![X, 1; -1, 0].

instance surjective_generalLinearTwoToProjectiveLine (k : Type u) [Field k] :
    Surjective (generalLinearTwoToProjectiveLine k)

AlgebraicGeometry.generalLinearTwoToPuncturedPlane, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Separation/GeneralLinearGroupPuncturedPlane.lean, line 203. The attribute's comment: “gl2_to_punctured_plane”.

Stacks Project, Tag 01KX (gl2_to_punctured_plane). The morphism from GL₂ to the punctured affine plane U = Spec k[x, y] ∖ {(x, y)} determined by x ↦ a, y ↦ b.

noncomputable def generalLinearTwoToPuncturedPlane :
    generalLinearTwoScheme k ⟶ (puncturedAffinePlaneOf k).puncturedScheme

AlgebraicGeometry.surjective_generalLinearTwoToPuncturedPlane, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Separation/GeneralLinearGroupPuncturedPlane.lean, line 219. The attribute's comment: “gl2_to_punctured_plane_surjective”.

Stacks Project, Tag 01KX (gl2_to_punctured_plane_surjective). The morphism from GL₂ to the punctured affine plane is surjective.

instance surjective_generalLinearTwoToPuncturedPlane :
    Surjective (generalLinearTwoToPuncturedPlane k)

AlgebraicGeometry.not_range_subset_of_isAffineOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Separation/GeneralLinearGroupPuncturedPlane.lean, line 235. The attribute's comment: “image_in_no_affine_open”.

Stacks Project, Tag 01KX (image_in_no_affine_open). The image of the morphism from GL₂ to the punctured affine plane is contained in no affine open of the punctured plane: it is everything, and the punctured plane is not affine.

theorem not_range_subset_of_isAffineOpen
    (V : ((puncturedAffinePlaneOf k).puncturedScheme).Opens) (hV : IsAffineOpen V) :
    ¬ Set.range (generalLinearTwoToPuncturedPlane k).base ⊆ (V : Set _)

AlgebraicGeometry.not_isImmersion_to_affine_projectiveLine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Separation/ProjectiveLineNoAffineImmersion.lean, line 59. The attribute's comment: “projective_line_no_immersion_into_affine”.

The projective line over a field admits no immersion into any affine scheme.

theorem not_isImmersion_to_affine_projectiveLine
    (k : Type u) [Field k] (A : Scheme.{u}) [IsAffine A] (f : projectiveLine k ⟶ A) :
    ¬ IsImmersion f
Tag 0816, a remark

Tag 0816 in the Stacks Project.

AlgebraicGeometry.compactSpace_and_quasiSeparatedSpace_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/SchemePropertiesPermanence.lean, line 176. The attribute's comment: “(1), quasi-compact and quasi-separated”.

An affine scheme is quasi-compact and quasi-separated.

theorem compactSpace_and_quasiSeparatedSpace_of_isAffine (X : Scheme.{u}) [IsAffine X] :
    CompactSpace X ∧ QuasiSeparatedSpace X

AlgebraicGeometry.compactSpace_and_isSeparated_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/SchemePropertiesPermanence.lean, line 181. The attribute's comment: “(1), quasi-compact and separated”.

An affine scheme is quasi-compact and separated.

theorem compactSpace_and_isSeparated_of_isAffine (X : Scheme.{u}) [IsAffine X] :
    CompactSpace X ∧ X.IsSeparated

AlgebraicGeometry.isSeparated_iff_scheme_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/SchemePropertiesPermanence.lean, line 195. The attribute's comment: “(2), separated”.

A morphism to a separated scheme is separated if and only if its source is a separated scheme. The direction from the source to the morphism holds with no hypothesis on the target; it is the converse that uses Y.IsSeparated.

theorem isSeparated_iff_scheme_isSeparated (f : X ⟶ Y) [Y.IsSeparated] :
    IsSeparated f ↔ X.IsSeparated

AlgebraicGeometry.quasiCompact_and_quasiSeparated_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/SchemePropertiesPermanence.lean, line 203. The attribute's comment: “(2), quasi-compact and quasi-separated”.

A morphism to a quasi-compact quasi-separated scheme is quasi-compact and quasi-separated if and only if its source is a quasi-compact quasi-separated scheme.

theorem quasiCompact_and_quasiSeparated_iff (f : X ⟶ Y) [CompactSpace Y]
    [QuasiSeparatedSpace Y] :
    (QuasiCompact f ∧ QuasiSeparated f) ↔ (CompactSpace X ∧ QuasiSeparatedSpace X)

AlgebraicGeometry.quasiCompact_and_isSeparated_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/SchemePropertiesPermanence.lean, line 211. The attribute's comment: “(2), quasi-compact and separated”.

A morphism to a quasi-compact separated scheme is quasi-compact and separated if and only if its source is a quasi-compact separated scheme.

theorem quasiCompact_and_isSeparated_iff (f : X ⟶ Y) [CompactSpace Y] [Y.IsSeparated] :
    (QuasiCompact f ∧ IsSeparated f) ↔ (CompactSpace X ∧ X.IsSeparated)

AlgebraicGeometry.quasiSeparatedSpace_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/SchemePropertiesPermanence.lean, line 222. The attribute's comment: “(3), quasi-separated”.

A fibre product of quasi-separated schemes over a quasi-separated scheme is quasi-separated.

theorem quasiSeparatedSpace_pullback (f : X ⟶ Y) (g : Z ⟶ Y)
    [QuasiSeparatedSpace X] [QuasiSeparatedSpace Y] [QuasiSeparatedSpace Z] :
    QuasiSeparatedSpace ↑(pullback f g)

AlgebraicGeometry.isSeparated_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/SchemePropertiesPermanence.lean, line 233. The attribute's comment: “(3), separated”.

A fibre product of separated schemes over a separated scheme is separated.

theorem isSeparated_pullback (f : X ⟶ Y) (g : Z ⟶ Y)
    [X.IsSeparated] [Y.IsSeparated] [Z.IsSeparated] : (pullback f g).IsSeparated

AlgebraicGeometry.compactSpace_and_quasiSeparatedSpace_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/SchemePropertiesPermanence.lean, line 251. The attribute's comment: “(3), quasi-compact and quasi-separated”.

A fibre product of quasi-compact quasi-separated schemes over a quasi-compact quasi-separated scheme is quasi-compact and quasi-separated.

theorem compactSpace_and_quasiSeparatedSpace_pullback (f : X ⟶ Y) (g : Z ⟶ Y)
    [CompactSpace X] [QuasiSeparatedSpace X] [CompactSpace Y] [QuasiSeparatedSpace Y]
    [CompactSpace Z] [QuasiSeparatedSpace Z] :
    CompactSpace ↑(pullback f g) ∧ QuasiSeparatedSpace ↑(pullback f g)

AlgebraicGeometry.compactSpace_and_isSeparated_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Schemes/ZariskiAndSeparation/SchemePropertiesPermanence.lean, line 260. The attribute's comment: “(3), quasi-compact and separated”.

A fibre product of quasi-compact separated schemes over a quasi-compact separated scheme is quasi-compact and separated.

theorem compactSpace_and_isSeparated_pullback (f : X ⟶ Y) (g : Z ⟶ Y)
    [CompactSpace X] [X.IsSeparated] [CompactSpace Y] [Y.IsSeparated]
    [CompactSpace Z] [Z.IsSeparated] :
    CompactSpace ↑(pullback f g) ∧ (pullback f g).IsSeparated

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.IsSeparated.instMap · AlgebraicGeometry.IsSeparated · AlgebraicGeometry.QuasiSeparated · AlgebraicGeometry.Scheme.IsSeparated · AlgebraicGeometry.quasiSeparatedSpace_iff_quasiSeparated · AlgebraicGeometry.structureMorphism · AlgebraicGeometry.diagonal_preimage_mixedCharts · AlgebraicGeometry.structureMorphism_not_quasiSeparated

Section26.23 Monomorphisms#

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

Tag 01L2, a definition

Tag 01L2 in the Stacks Project.

Declarations registered for the tag:

Tag 01L3, a lemma

Tag 01L3 in the Stacks Project.

Declarations registered for the tag:

Tag 01L4, a lemma

Tag 01L4 in the Stacks Project.

Declarations registered for the tag:

Tag 01L5, a lemma

Tag 01L5 in the Stacks Project.

Declarations registered for the tag:

Tag 02YC, a lemma

Tag 02YC in the Stacks Project.

Declarations registered for the tag:

Tag 01L6, a lemma

Tag 01L6 in the Stacks Project.

Declarations registered for the tag:

Tag 01L7, a lemma

Tag 01L7 in the Stacks Project.

Declarations registered for the tag:

Tag 01L9, an example

Tag 01L9 in the Stacks Project.

Declarations registered for the tag:

Tag 03DP, a lemma

Tag 03DP in the Stacks Project.

AlgebraicGeometry.exists_iso_coproduct_spec_of_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Immersion/Monomorphism.lean, line 105.

A monomorphism into a disjoint union of spectra of fields is, over that disjoint union, the inclusion of precisely a subset of its components.

public theorem exists_iso_coproduct_spec_of_mono {ι : Type v} [Small.{u} ι] (k : ι → Type u)
    [∀ i, Field (k i)] {Y : Scheme.{u}}
    (f : Y ⟶ ∐ fun i ↦ Spec (.of (k i))) [Mono f] :
    ∃ J : Set ι, ∃ e : Y ≅ ∐ fun j : J ↦ Spec (.of (k j.1)),
      e.hom ≫ Sigma.desc (fun j : J ↦ Sigma.ι (fun i ↦ Spec (.of (k i))) j.1) = f
Sources
LeanCategoryTheory.Mono · CategoryTheory.Limits.pullback.isIso_diagonal_iff · AlgebraicGeometry.IsSeparated.isSeparated_of_mono · CategoryTheory.mono_comp · CategoryTheory.MorphismProperty.IsStableUnderBaseChange.monomorphisms · AlgebraicGeometry.SurjectiveOnStalks.mono_of_injective · AlgebraicGeometry.IsPreimmersion.instMonoScheme · AlgebraicGeometry.instIsPreimmersionFromSpecStalk

Section26.24 Functoriality for quasi-coherent modules#

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

Tag 01LA, the section

Tag 01LA in the Stacks Project.

Stacks.AlgebraicGeometry.FunctorialityQcoh.isQuasicoherent_iff_forall_isAffineOpen_exists_tilde, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/FunctorialityQuasiCoherent/Enumeration.lean, line 117. The attribute's comment: “the section's item (1): a sheaf of modules is quasi-coherent exactly when its restriction to each affine open U = Spec Γ(X, U) is the sheaf associated to a Γ(X, U)-module”.

[Stacks, Tag 01LA], item (1). A sheaf of 𝒪_X-modules F is quasi-coherent if and only if the restriction of F to each affine open U = Spec Γ(X, U) is of the form M^~ for some Γ(X, U)-module M.

Forwards, the module is Γ(F, U) and the isomorphism is Stacks.Modules.tildeIsoRestrictFromSpec. Backwards, M^~ is quasi-coherent, hence so is the restriction of F to Spec Γ(X, U); transporting along hU.isoSpec.hom ≫ hU.fromSpec = U.ι makes the restriction of F to U quasi-coherent, and quasi-coherence is local on X.

theorem isQuasicoherent_iff_forall_isAffineOpen_exists_tilde (F : X.Modules) :
    F.IsQuasicoherent ↔
      ∀ (U : X.Opens) (hU : IsAffineOpen U),
        ∃ M : ModuleCat.{u} Γ(X, U),
          Nonempty (tilde (R := Γ(X, U)) M ≅ F.restrict hU.fromSpec)

Stacks.AlgebraicGeometry.FunctorialityQcoh.isQuasicoherent_iff_forall_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/FunctorialityQuasiCoherent/Enumeration.lean, line 145. The attribute's comment: “the section's item (2): a sheaf of modules is quasi-coherent exactly when its restriction to each member of an affine open covering is quasi-coherent”.

[Stacks, Tag 01LA], item (2). A sheaf of 𝒪_X-modules F is quasi-coherent if and only if the restriction of F to each of the members of an affine open covering of X is quasi-coherent.

Forwards this is restriction along an open immersion, which preserves quasi-coherence; backwards it is Stacks.Modules.isQuasicoherent_of_restrict, the locality of quasi-coherence.

theorem isQuasicoherent_iff_forall_restrict {I : Type w} (F : X.Modules)
    (U : I → X.affineOpens) (hU : ⨆ i, (U i : X.Opens) = ⊤) :
    F.IsQuasicoherent ↔ ∀ i, (F.restrict (U i : X.Opens).ι).IsQuasicoherent

Stacks.AlgebraicGeometry.FunctorialityQcoh.isQuasicoherent_X₁_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/FunctorialityQuasiCoherent/Enumeration.lean, line 158. The attribute's comment: “the section's item (6), the kernel case on an arbitrary scheme: in a short exact sequence, if the last two terms are quasi-coherent then so is the first”.

[Stacks, Tag 01LA], item (6), the kernel case. Let 0 ⟶ F₁ ⟶ F₂ ⟶ F₃ ⟶ 0 be a short exact sequence of 𝒪_X-modules on an arbitrary scheme X. If F₂ and F₃ are quasi-coherent then so is F₁, being the kernel of F₂ ⟶ F₃.

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

Stacks.AlgebraicGeometry.FunctorialityQcoh.isQuasicoherent_X₃_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/FunctorialityQuasiCoherent/Enumeration.lean, line 170. The attribute's comment: “the section's item (6), the cokernel case on an arbitrary scheme: in a short exact sequence, if the first two terms are quasi-coherent then so is the last”.

[Stacks, Tag 01LA], item (6), the cokernel case. Let 0 ⟶ F₁ ⟶ F₂ ⟶ F₃ ⟶ 0 be a short exact sequence of 𝒪_X-modules on an arbitrary scheme X. If F₁ and F₂ are quasi-coherent then so is F₃, being the cokernel of F₁ ⟶ F₂.

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

Declarations registered for the tag:

Tag 01LB, an item

Tag 01LB in the Stacks Project.

Declarations registered for the tag:

Tag 01LC, a lemma

Tag 01LC in the Stacks Project.

Stacks.AlgebraicGeometry.RelativeMayerVietoris.pushforward_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeMayerVietoris/Qcoh.lean, line 174.

[Stacks, Tag 01LC]. The direct image of a quasi-coherent module along a quasi-compact quasi-separated morphism of schemes is quasi-coherent.

The statement is local on the target: over an affine open V of S the restriction of f_* F is the direct image along f ∣_ V of the restriction of F to f ⁻¹ᵁ V, and f ∣_ V is again quasi-compact and quasi-separated with affine target.

theorem pushforward_isQuasicoherent (f : X ⟶ S) [QuasiCompact f] [QuasiSeparated f]
    (F : X.Modules) [F.IsQuasicoherent] :
    ((Scheme.Modules.pushforward f).obj F).IsQuasicoherent

AlgebraicGeometry.pushforward_isQuasicoherent, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/FunctorialityQuasiCoherent/Basic/Pushforward.lean, line 899. References: EGA III (1.4.10), “q = 0”.

Stacks Project, Tag 01LC. Pushforward along a quasi-compact and quasi-separated morphism of schemes preserves quasi-coherence.

public instance pushforward_isQuasicoherent
    {X S : Scheme.{u}} (f : X ⟶ S) [QuasiCompact f] [QuasiSeparated f]
    (F : X.Modules) [F.IsQuasicoherent] :
    ((Scheme.Modules.pushforward f).obj F).IsQuasicoherent
Tag 02V0, a lemma

Tag 02V0 in the Stacks Project.

Declarations registered for the tag:

Sources
LeanStacks.AlgebraicGeometry.FunctorialityQcoh.isQuasicoherent_iff_forall_isAffineOpen_exists_tilde · Stacks.AlgebraicGeometry.FunctorialityQcoh.isQuasicoherent_iff_forall_restrict · Stacks.AlgebraicGeometry.FunctorialityQcoh.isQuasicoherent_X₁_of_shortExact · Stacks.AlgebraicGeometry.FunctorialityQcoh.isQuasicoherent_X₃_of_shortExact · Stacks.AlgebraicGeometry.QuasicoherentColimits.isQuasicoherent_sigma · Stacks.AlgebraicGeometry.QuasicoherentColimits.isQuasicoherent_colimit · Stacks.AlgebraicGeometry.QcohLimits.isQuasicoherent_kernel · Stacks.AlgebraicGeometry.QuasicoherentColimits.isQuasicoherent_cokernel

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.