67.4 Separation axioms to 67.16 Scheme theoretic image

Section67.4 Separation axioms#

Section 67.4 of the Stacks Project, Tag 03HJ. 14 tags here are carried by 55 declarations of the repository (all in StacksFrontier) and 5 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03HJ, the section

Tag 03HJ in the Stacks Project.

Declarations registered for the tag:

Tag 03HK, a lemma

Tag 03HK in the Stacks Project.

AlgebraicGeometry.relativelyRepresentable_pullbackDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeDiagonal.lean, line 96. The attribute's comment: “part (1)”.

Stacks 03HK, part (1). The relative diagonal of a morphism out of an algebraic space over S is relatively representable. The target need not be an algebraic space: the relative diagonal is a base change of the absolute diagonal of the source, which is representable by the second defining clause of AlgebraicGeometry.IsAlgebraicSpace.

theorem relativelyRepresentable_pullbackDiagonal (f : F ⟶ G)
    (hF : IsAlgebraicSpace B S hS F) :
    yoneda.relativelyRepresentable (pullback.diagonal f)

AlgebraicGeometry.presheaf_locallyOfFiniteType_pullbackDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeDiagonalProperties.lean, line 53. The attribute's comment: “part (2)”.

Stacks 03HK, part (2). The relative diagonal of a morphism out of an algebraic space over S is locally of finite type.

theorem presheaf_locallyOfFiniteType_pullbackDiagonal (f : F ⟶ G)
    (hF : IsAlgebraicSpace B S hS F) :
    (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@LocallyOfFiniteType.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS))) (pullback.diagonal f)

AlgebraicGeometry.presheaf_monomorphisms_pullbackDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeDiagonalProperties.lean, line 64. The attribute's comment: “part (3)”.

Stacks 03HK, part (3). Every represented base change of the relative diagonal of a morphism out of an algebraic space over S is a monomorphism of schemes.

theorem presheaf_monomorphisms_pullbackDiagonal (f : F ⟶ G)
    (hF : IsAlgebraicSpace B S hS F) :
    (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (MorphismProperty.monomorphisms Scheme.{u})
      (BigFppfOver.toScheme B S hS))) (pullback.diagonal f)

AlgebraicGeometry.presheaf_isSeparated_pullbackDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeDiagonalProperties.lean, line 75. The attribute's comment: “part (4)”.

Stacks 03HK, part (4). The relative diagonal of a morphism out of an algebraic space over S is separated.

theorem presheaf_isSeparated_pullbackDiagonal (f : F ⟶ G)
    (hF : IsAlgebraicSpace B S hS F) :
    (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@IsSeparated.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS))) (pullback.diagonal f)

AlgebraicGeometry.presheaf_locallyQuasiFinite_pullbackDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeDiagonalProperties.lean, line 86. The attribute's comment: “part (5)”.

Stacks 03HK, part (5). The relative diagonal of a morphism out of an algebraic space over S is locally quasi-finite.

theorem presheaf_locallyQuasiFinite_pullbackDiagonal (f : F ⟶ G)
    (hF : IsAlgebraicSpace B S hS F) :
    (MorphismProperty.presheaf (MorphismProperty.inverseImage
      ((@LocallyOfFiniteType.{u} : MorphismProperty Scheme.{u}) ⊓
        (@LocallyQuasiFinite.{u} : MorphismProperty Scheme.{u}))
      (BigFppfOver.toScheme B S hS))) (pullback.diagonal f)

AlgebraicGeometry.Space.monomorphisms_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UnramifiedDiagonal.lean, line 192. The attribute's comment: “representable and a monomorphism”.

Stacks 03HK, representability and the monomorphism condition. The relative diagonal of a morphism of algebraic spaces over S is representable and a monomorphism after every represented base change.

It is the base change of the absolute diagonal of the source along X ×_Y X ⟶ X ⨯ X (AlgebraicGeometry.isPullback_pullbackDiagonal_diag), and for the absolute diagonal this is part (2) of [Stacks Project, Tag 02X4]. Algebraicity of the target is not needed.

theorem monomorphisms_diagonal (hX : IsAlgebraicSpace B S hS X) (f : X ⟶ Y) :
    (MorphismProperty.inverseImage (MorphismProperty.monomorphisms Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf (pullback.diagonal f)

AlgebraicGeometry.Space.locallyOfFiniteType_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UnramifiedDiagonal.lean, line 203. The attribute's comment: “locally of finite type”.

Stacks 03HK, local finite type. Every represented base change of the relative diagonal of a morphism of algebraic spaces over S is a morphism of schemes which is locally of finite type. This is part (1) of [Stacks Project, Tag 02X4] transported along AlgebraicGeometry.isPullback_pullbackDiagonal_diag.

theorem locallyOfFiniteType_diagonal (hX : IsAlgebraicSpace B S hS X) (f : X ⟶ Y) :
    (MorphismProperty.inverseImage
      (@AlgebraicGeometry.LocallyOfFiniteType.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf (pullback.diagonal f)

AlgebraicGeometry.Space.isSeparated_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UnramifiedDiagonal.lean, line 215. The attribute's comment: “separated”.

Stacks 03HK, separatedness. Every represented base change of the relative diagonal of a morphism of algebraic spaces over S is a separated morphism of schemes. This is part (3) of [Stacks Project, Tag 02X4] transported along AlgebraicGeometry.isPullback_pullbackDiagonal_diag.

theorem isSeparated_diagonal (hX : IsAlgebraicSpace B S hS X) (f : X ⟶ Y) :
    (MorphismProperty.inverseImage
      (@_root_.AlgebraicGeometry.IsSeparated.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf (pullback.diagonal f)

AlgebraicGeometry.Space.locallyQuasiFinite_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UnramifiedDiagonal.lean, line 227. The attribute's comment: “locally quasi-finite”.

Stacks 03HK, local quasi-finiteness. Every represented base change of the relative diagonal of a morphism of algebraic spaces over S is a morphism of schemes which is locally of finite type and locally quasi-finite. This is part (4) of [Stacks Project, Tag 02X4] transported along AlgebraicGeometry.isPullback_pullbackDiagonal_diag.

theorem locallyQuasiFinite_diagonal (hX : IsAlgebraicSpace B S hS X) (f : X ⟶ Y) :
    (MorphismProperty.inverseImage
      ((@AlgebraicGeometry.LocallyOfFiniteType.{u} : MorphismProperty Scheme.{u}) ⊓
        (@AlgebraicGeometry.LocallyQuasiFinite.{u} : MorphismProperty Scheme.{u}))
      (BigFppfOver.toScheme B S hS)).presheaf (pullback.diagonal f)
Tag 03HL, a definition

Tag 03HL in the Stacks Project.

AlgebraicGeometry.Space.IsSeparated, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms.lean, line 274. The attribute's comment: “part (1): separated”. References: EGA I (5.4.1).

Stacks 03HL, part (1). A morphism of algebraic spaces over S is separated when its relative diagonal is a closed immersion.

abbrev IsSeparated (f : F ⟶ G) : Prop

AlgebraicGeometry.Space.IsLocallySeparated, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms.lean, line 280. The attribute's comment: “part (2): locally separated”.

Stacks 03HL, part (2). A morphism of algebraic spaces over S is locally separated when its relative diagonal is an immersion.

abbrev IsLocallySeparated (f : F ⟶ G) : Prop

AlgebraicGeometry.Space.IsQuasiSeparated, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms.lean, line 286. The attribute's comment: “part (3): quasi-separated”. References: EGA IV (1.2.1); SGA 4 VI (1.7), “quasi-separated”.

Stacks 03HL, part (3). A morphism of algebraic spaces over S is quasi-separated when its relative diagonal is quasi-compact.

abbrev IsQuasiSeparated (f : F ⟶ G) : Prop
Tag 03KK, a lemma

Tag 03KK in the Stacks Project.

AlgebraicGeometry.Space.isLocallySeparated_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparatedVariants.lean, line 65. The attribute's comment: “locally separated”.

A separated morphism of algebraic spaces over S is locally separated.

theorem isLocallySeparated_of_isSeparated
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : F ⟶ G} (hf : IsSeparated B S hS f) :
    IsLocallySeparated B S hS f

AlgebraicGeometry.Space.isQuasiSeparated_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparatedVariants.lean, line 72. The attribute's comment: “quasi-separated”.

A separated morphism of algebraic spaces over S is quasi-separated.

theorem isQuasiSeparated_of_isSeparated
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : F ⟶ G} (hf : IsSeparated B S hS f) :
    IsQuasiSeparated B S hS f
Tag 03KL, a lemma

Tag 03KL in the Stacks Project.

AlgebraicGeometry.Space.isQuasiSeparated_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentationBaseChange.lean, line 63. The attribute's comment: “quasi_separated_base_change”. References: SGA 4 VI (1.9.1), “(ii), special case”.

A base change of a quasi-separated morphism of algebraic spaces over S is quasi-separated.

theorem isQuasiSeparated_pullback {X Y Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : X ⟶ Y) (g : Y' ⟶ Y) (hf : IsQuasiSeparated B S hS f) :
    IsQuasiSeparated B S hS (pullback.snd f g)

AlgebraicGeometry.Space.isSeparated_pullbackSnd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparatedTfae.lean, line 666. The attribute's comment: “separated_base_change”.

A separated morphism stays separated after any base change.

theorem isSeparated_pullbackSnd {Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : X ⟶ Y} (g : Z ⟶ Y)
    (h : IsSeparated B S hS f) : IsSeparated B S hS (pullback.snd f g)

AlgebraicGeometry.Space.isSeparated_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparationMorphismProperties.lean, line 82. The attribute's comment: “separated_base_change”.

A base change of a separated morphism of algebraic spaces over S is separated.

theorem isSeparated_pullback {X Y Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : X ⟶ Y) (g : Y' ⟶ Y) (hf : IsSeparated B S hS f) :
    IsSeparated B S hS (pullback.snd f g)

AlgebraicGeometry.Space.isLocallySeparated_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparationMorphismProperties.lean, line 92. The attribute's comment: “locally_separated_base_change”.

A base change of a locally separated morphism of algebraic spaces over S is locally separated.

theorem isLocallySeparated_pullback {X Y Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : X ⟶ Y) (g : Y' ⟶ Y) (hf : IsLocallySeparated B S hS f) :
    IsLocallySeparated B S hS (pullback.snd f g)
Tag 03KN, a lemma

Tag 03KN in the Stacks Project.

AlgebraicGeometry.Space.isLocallyOfFiniteType_mapDesc', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleChartBridge.lean, line 167. The attribute's comment: “part (1): locally of finite type”.

Stacks 03KN, part (1). The comparison X ×[Z] Y ⟶ X ×[T] Y is locally of finite type in the sense of Stacks 03XF. This is AlgebraicGeometry.Space.isLocallyOfFiniteType_mapDesc with its hypothesis discharged.

theorem isLocallyOfFiniteType_mapDesc' (f : X ⟶ Z) (g : Y ⟶ Z) (h : Z ⟶ T)
    (hZ : IsAlgebraicSpace B S hS Z) :
    IsLocallyOfFiniteType B S hS (pullback.mapDesc f g h)

AlgebraicGeometry.Space.isLocallyQuasiFinite_mapDesc', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleChartBridge.lean, line 177. The attribute's comment: “part (1): locally quasi-finite”.

Stacks 03KN, part (1). The comparison X ×[Z] Y ⟶ X ×[T] Y is locally quasi-finite in the sense of Stacks 03XJ. This is AlgebraicGeometry.Space.isLocallyQuasiFinite_mapDesc with its hypothesis discharged.

theorem isLocallyQuasiFinite_mapDesc' (f : X ⟶ Z) (g : Y ⟶ Z) (h : Z ⟶ T)
    (hZ : IsAlgebraicSpace B S hS Z) :
    IsLocallyQuasiFinite B S hS (pullback.mapDesc f g h)

CategoryTheory.Limits.pullback.mono_mapDesc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MapDescent.lean, line 60. The attribute's comment: “part (1): monomorphism”.

The canonical comparison X ×[Z] Y ⟶ X ×[T] Y induced by a morphism Z ⟶ T is a monomorphism.

instance pullback.mono_mapDesc {X Y Z T : C} (f : X ⟶ Z) (g : Y ⟶ Z) (i : Z ⟶ T)
    [HasPullback f g] [HasPullback (f ≫ i) (g ≫ i)] :
    Mono (pullback.mapDesc f g i)

AlgebraicGeometry.Space.relativelyRepresentable_mapDesc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MapDescent.lean, line 162. The attribute's comment: “part (1): representable”.

The comparison of fibre products is representable.

theorem relativelyRepresentable_mapDesc (f : X ⟶ Z) (g : Y ⟶ Z) (h : Z ⟶ T)
    (hZ : IsAlgebraicSpace B S hS Z) :
    yoneda.relativelyRepresentable (pullback.mapDesc f g h)

AlgebraicGeometry.Space.isSeparated_mapDesc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MapDescent.lean, line 171. The attribute's comment: “part (1): separated”.

The comparison of fibre products is separated.

theorem isSeparated_mapDesc (f : X ⟶ Z) (g : Y ⟶ Z) (h : Z ⟶ T) :
    IsSeparated B S hS (pullback.mapDesc f g h)

AlgebraicGeometry.Space.isImmersion_mapDesc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MapDescent.lean, line 180. The attribute's comment: “part (2)”. References: EGA I (5.3.10).

The comparison of fibre products is an immersion when h : Z ⟶ T is locally separated.

theorem isImmersion_mapDesc (f : X ⟶ Z) (g : Y ⟶ Z) (h : Z ⟶ T)
    (hh : IsLocallySeparated B S hS h) :
    IsImmersion B S hS (pullback.mapDesc f g h)

AlgebraicGeometry.Space.isClosedImmersion_mapDesc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MapDescent.lean, line 187. The attribute's comment: “part (3)”. References: EGA I (5.4.2).

The comparison of fibre products is a closed immersion when h : Z ⟶ T is separated.

theorem isClosedImmersion_mapDesc (f : X ⟶ Z) (g : Y ⟶ Z) (h : Z ⟶ T)
    (hh : IsSeparated B S hS h) :
    IsClosedImmersion B S hS (pullback.mapDesc f g h)

AlgebraicGeometry.Space.isQuasiCompact_mapDesc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MapDescent.lean, line 194. The attribute's comment: “part (4)”.

The comparison of fibre products is quasi-compact when h : Z ⟶ T is quasi-separated.

theorem isQuasiCompact_mapDesc (f : X ⟶ Z) (g : Y ⟶ Z) (h : Z ⟶ T)
    (hh : IsQuasiSeparated B S hS h) :
    IsQuasiCompact B S hS (pullback.mapDesc f g h)
Tag 03KO, a lemma

Tag 03KO in the Stacks Project.

AlgebraicGeometry.Space.separationProperties_graph, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GraphSeparationProperties.lean, line 54.

Stacks 03KO. Let Z be an algebraic space over the scheme S and let f : X ⟶ Y be a morphism of algebraic spaces over Z. For the graph i : X ⟶ X ×[Z] Y of f:

  1. i is representable, locally of finite type, locally quasi-finite, separated and a monomorphism;
  2. if Y ⟶ Z is locally separated then i is an immersion;
  3. if Y ⟶ Z is separated then i is a closed immersion; and
  4. if Y ⟶ Z is quasi-separated then i is quasi-compact.

The graph is a section of the first projection of X ×[Z] Y, and all four parts are the corresponding parts of Stacks 03KP for that section; parts (2), (3) and (4) use in addition that the first projection inherits the relevant separation property from Y ⟶ Z as a base change of it.

theorem separationProperties_graph {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (g : Y ⟶ Z) (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) :
    (yoneda.relativelyRepresentable (graph B S hS f g) ∧
        IsLocallyOfFiniteType B S hS (graph B S hS f g) ∧
        IsLocallyQuasiFinite B S hS (graph B S hS f g) ∧
        IsSeparated B S hS (graph B S hS f g) ∧
        Mono (graph B S hS f g)) ∧
      (IsLocallySeparated B S hS g → IsImmersion B S hS (graph B S hS f g)) ∧
      (IsSeparated B S hS g → IsClosedImmersion B S hS (graph B S hS f g)) ∧
      (IsQuasiSeparated B S hS g → IsQuasiCompact B S hS (graph B S hS f g))
Tag 03KP, a lemma

Tag 03KP in the Stacks Project.

AlgebraicGeometry.Space.mono_of_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparatedCriteria.lean, line 340. The attribute's comment: “part (1): monomorphism”.

Stacks 03KP, part (1). A section of a morphism of algebraic spaces over S is a monomorphism, being a split monomorphism.

theorem mono_of_section (p : P ⟶ V) (s : V ⟶ P) (hs : s ≫ p = 𝟙 V) : Mono s

AlgebraicGeometry.Space.isSeparated_of_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparatedCriteria.lean, line 347. The attribute's comment: “part (1): separated”.

Stacks 03KP, part (1). A section of a morphism of algebraic spaces over S is separated.

theorem isSeparated_of_section (p : P ⟶ V) (s : V ⟶ P) (hs : s ≫ p = 𝟙 V) :
    IsSeparated B S hS s

AlgebraicGeometry.Space.relativelyRepresentable_of_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparatedCriteria.lean, line 377. The attribute's comment: “part (1): representable”.

Stacks 03KP, part (1). A section of a morphism of algebraic spaces over S with algebraic total space is representable.

theorem relativelyRepresentable_of_section (p : P ⟶ V)
    (hP : IsAlgebraicSpace B S hS P) (s : V ⟶ P) (hs : s ≫ p = 𝟙 V) :
    yoneda.relativelyRepresentable s

AlgebraicGeometry.Space.isLocallyOfFiniteType_of_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparatedCriteria.lean, line 385. The attribute's comment: “part (1): locally of finite type”.

Stacks 03KP, part (1). A section of a morphism of algebraic spaces over S with algebraic total space is locally of finite type in the sense of Stacks 03XF.

theorem isLocallyOfFiniteType_of_section (p : P ⟶ V)
    (hP : IsAlgebraicSpace B S hS P) (s : V ⟶ P) (hs : s ≫ p = 𝟙 V) :
    IsLocallyOfFiniteType B S hS s

AlgebraicGeometry.Space.isLocallyQuasiFinite_of_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparatedCriteria.lean, line 394. The attribute's comment: “part (1): locally quasi-finite”.

Stacks 03KP, part (1). A section of a morphism of algebraic spaces over S with algebraic total space is locally quasi-finite in the sense of Stacks 03XJ.

theorem isLocallyQuasiFinite_of_section (p : P ⟶ V)
    (hP : IsAlgebraicSpace B S hS P) (s : V ⟶ P) (hs : s ≫ p = 𝟙 V) :
    IsLocallyQuasiFinite B S hS s

AlgebraicGeometry.Space.isImmersion_of_isLocallySeparated_of_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparatedCriteria.lean, line 403. The attribute's comment: “part (2)”.

Stacks 03KP, part (2). A section of a locally separated morphism of algebraic spaces over S is an immersion.

theorem isImmersion_of_isLocallySeparated_of_section (p : P ⟶ V)
    (hp : IsLocallySeparated B S hS p) (s : V ⟶ P) (hs : s ≫ p = 𝟙 V) :
    IsImmersion B S hS s

AlgebraicGeometry.Space.isClosedImmersion_of_isSeparated_of_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparatedCriteria.lean, line 412. The attribute's comment: “part (3)”. References: SGA 3 VIB (5.6.3), “more general”.

Stacks 03KP, part (3). A section of a separated morphism of algebraic spaces over S is a closed immersion.

theorem isClosedImmersion_of_isSeparated_of_section (p : P ⟶ V)
    (hp : IsSeparated B S hS p) (s : V ⟶ P) (hs : s ≫ p = 𝟙 V) :
    IsClosedImmersion B S hS s

AlgebraicGeometry.Space.isQuasiCompact_of_isQuasiSeparated_of_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparatedCriteria.lean, line 421. The attribute's comment: “part (4)”.

Stacks 03KP, part (4). A section of a quasi-separated morphism of algebraic spaces over S is quasi-compact.

theorem isQuasiCompact_of_isQuasiSeparated_of_section (p : P ⟶ V)
    (hp : IsQuasiSeparated B S hS p) (s : V ⟶ P) (hs : s ≫ p = 𝟙 V) :
    IsQuasiCompact B S hS s
Tag 03KQ, a lemma

Tag 03KQ in the Stacks Project.

AlgebraicGeometry.Space.isQuasiSeparated_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SeparationAxioms.lean, line 86. The attribute's comment: “quasi-separated”.

The composite of two quasi-separated morphisms of algebraic spaces over S is quasi-separated.

theorem isQuasiSeparated_comp (hF : IsAlgebraicSpace B S hS F) (hG : IsAlgebraicSpace B S hS G)
    (p : F ⟶ G) (q : G ⟶ H) (hp : IsQuasiSeparated B S hS p)
    (hq : IsQuasiSeparated B S hS q) : IsQuasiSeparated B S hS (p ≫ q)

AlgebraicGeometry.Space.isSeparated_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparatedTfae.lean, line 1074. The attribute's comment: “separated”.

Separatedness of morphisms of algebraic spaces is stable under composition.

theorem isSeparated_comp {F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (p : F ⟶ G) (q : G ⟶ H)
    (hp : IsSeparated B S hS p) (hq : IsSeparated B S hS q) :
    IsSeparated B S hS (p ≫ q)

AlgebraicGeometry.Space.isLocallySeparated_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparatedTfae.lean, line 1156. The attribute's comment: “locally separated”.

Local separatedness of morphisms of algebraic spaces is stable under composition.

theorem isLocallySeparated_comp {F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (p : F ⟶ G) (q : G ⟶ H)
    (hp : IsLocallySeparated B S hS p) (hq : IsLocallySeparated B S hS q) :
    IsLocallySeparated B S hS (p ≫ q)
Tag 04ZH, a lemma

Tag 04ZH in the Stacks Project.

AlgebraicGeometry.Space.isSeparatedOver_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SeparationAxioms.lean, line 107. The attribute's comment: “part (4)”.

If G is separated over S and f : F ⟶ G is separated, then F is separated over S.

theorem isSeparatedOver_of_isSeparated {f : F ⟶ G} (hG : IsSeparatedOver B S hS G)
    (hf : IsSeparated B S hS f) : IsSeparatedOver B S hS F

AlgebraicGeometry.Space.isLocallySeparatedOver_of_isLocallySeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SeparationAxioms.lean, line 119. The attribute's comment: “part (6)”.

If G is locally separated over S and f : F ⟶ G is locally separated, then F is locally separated over S.

theorem isLocallySeparatedOver_of_isLocallySeparated {f : F ⟶ G}
    (hG : IsLocallySeparatedOver B S hS G) (hf : IsLocallySeparated B S hS f) :
    IsLocallySeparatedOver B S hS F

AlgebraicGeometry.Space.isQuasiSeparatedOver_of_isQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SeparationAxioms.lean, line 145. The attribute's comment: “part (5)”.

If G is quasi-separated over S and f : F ⟶ G is quasi-separated, then F is quasi-separated over S.

theorem isQuasiSeparatedOver_of_isQuasiSeparated (hF : IsAlgebraicSpace B S hS F) {f : F ⟶ G}
    (hG : IsQuasiSeparatedOver B S hS G) (hf : IsQuasiSeparated B S hS f) :
    IsQuasiSeparatedOver B S hS F

AlgebraicGeometry.Space.isAbsolutelySeparated_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SeparationAxioms.lean, line 157. The attribute's comment: “part (1)”.

If G is separated and f : F ⟶ G is separated, then F is separated.

theorem isAbsolutelySeparated_of_isSeparated {f : F ⟶ G}
    (hG : IsAbsolutelySeparated B S hS hZ G) (hf : IsSeparated B S hS f) :
    IsAbsolutelySeparated B S hS hZ F

AlgebraicGeometry.Space.isAbsolutelyLocallySeparated_of_isLocallySeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SeparationAxioms.lean, line 166. The attribute's comment: “part (3)”.

If G is locally separated and f : F ⟶ G is locally separated, then F is locally separated.

theorem isAbsolutelyLocallySeparated_of_isLocallySeparated {f : F ⟶ G}
    (hG : IsAbsolutelyLocallySeparated B S hS hZ G) (hf : IsLocallySeparated B S hS f) :
    IsAbsolutelyLocallySeparated B S hS hZ F

AlgebraicGeometry.Space.isAbsolutelyQuasiSeparated_of_isQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SeparationAxioms.lean, line 175. The attribute's comment: “part (2)”.

If G is quasi-separated and f : F ⟶ G is quasi-separated, then F is quasi-separated.

theorem isAbsolutelyQuasiSeparated_of_isQuasiSeparated (hF : IsAlgebraicSpace B S hS F)
    {f : F ⟶ G} (hG : IsAbsolutelyQuasiSeparated B S hS hZ G)
    (hf : IsQuasiSeparated B S hS f) : IsAbsolutelyQuasiSeparated B S hS hZ F
Tag 03KR, a lemma

Tag 03KR in the Stacks Project.

AlgebraicGeometry.Space.separationAxioms_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparationAxiomsCancellation.lean, line 74.

Stacks 03KR. Let S be a scheme contained in the big fppf site B and let f : X ⟶ Y and g : Y ⟶ Z be morphisms of algebraic spaces over S. Then:

  1. if f ≫ g is separated, so is f;
  2. if f ≫ g is locally separated, so is f; and
  3. if f ≫ g is quasi-separated, so is f.

Each of the three separation axioms is a condition on the relative diagonal which is stable under base change, and the relative diagonal of f is a base change of that of f ≫ g along the comparison map X ×_Y X ⟶ X ×_Z X.

theorem separationAxioms_of_comp (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y) (g : Y ⟶ Z) :
    (IsSeparated B S hS (f ≫ g) → IsSeparated B S hS f) ∧
      (IsLocallySeparated B S hS (f ≫ g) → IsLocallySeparated B S hS f) ∧
      (IsQuasiSeparated B S hS (f ≫ g) → IsQuasiSeparated B S hS f)
Tag 04ZI, a lemma

Tag 04ZI in the Stacks Project.

AlgebraicGeometry.Space.isSeparatedOver_of_isAbsolutelySeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SeparationAxioms.lean, line 186. The attribute's comment: “part (1)”.

A separated algebraic space over S is separated over S, that is, an algebraic space which is separated over the terminal scheme is separated over its own base scheme.

theorem isSeparatedOver_of_isAbsolutelySeparated (hF : IsAlgebraicSpace B S hS F)
    (h : IsAbsolutelySeparated B S hS hZ F) : IsSeparatedOver B S hS F

AlgebraicGeometry.Space.isLocallySeparatedOver_of_isAbsolutelyLocallySeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SeparationAxioms.lean, line 197. The attribute's comment: “part (2)”.

A locally separated algebraic space is locally separated over its base scheme.

theorem isLocallySeparatedOver_of_isAbsolutelyLocallySeparated (hF : IsAlgebraicSpace B S hS F)
    (h : IsAbsolutelyLocallySeparated B S hS hZ F) : IsLocallySeparatedOver B S hS F

AlgebraicGeometry.Space.isQuasiSeparatedOver_of_isAbsolutelyQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SeparationAxioms.lean, line 208. The attribute's comment: “part (3)”.

A quasi-separated algebraic space is quasi-separated over its base scheme.

theorem isQuasiSeparatedOver_of_isAbsolutelyQuasiSeparated (hF : IsAlgebraicSpace B S hS F)
    (h : IsAbsolutelyQuasiSeparated B S hS hZ F) : IsQuasiSeparatedOver B S hS F

AlgebraicGeometry.Space.isQuasiSeparated_of_isQuasiSeparatedOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SeparationAxioms.lean, line 220. The attribute's comment: “part (6)”.

Every morphism out of an algebraic space which is quasi-separated over S is quasi-separated.

theorem isQuasiSeparated_of_isQuasiSeparatedOver (hF : IsQuasiSeparatedOver B S hS F)
    (p : F ⟶ G) : IsQuasiSeparated B S hS p

AlgebraicGeometry.Space.isSeparated_of_isSeparatedOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparatedTfae.lean, line 1088. The attribute's comment: “part (4)”.

Every morphism out of an algebraic space which is separated over S is separated.

theorem isSeparated_of_isSeparatedOver {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hF : IsSeparatedOver B S hS F) (p : F ⟶ G) : IsSeparated B S hS p

AlgebraicGeometry.Space.isLocallySeparated_of_isLocallySeparatedOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparatedTfae.lean, line 1171. The attribute's comment: “part (5)”.

Every morphism out of an algebraic space which is locally separated over S is locally separated.

theorem isLocallySeparated_of_isLocallySeparatedOver {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hF : IsLocallySeparatedOver B S hS F) (p : F ⟶ G) : IsLocallySeparated B S hS p
Tag 03KM, a lemma

Tag 03KM in the Stacks Project.

AlgebraicGeometry.Space.isQuasiSeparated_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiSeparatedTfae.lean, line 527. The attribute's comment: “quasi-separated”.

For a morphism f : X ⟶ Y of algebraic spaces over a scheme S the following six conditions are equivalent: f is quasi-separated; the base change of f along every morphism from a representable presheaf is quasi-separated; the same for the test objects with affine underlying scheme; for every affine test object the fibre product is a quasi-separated algebraic space, that is quasi-separated over the terminal scheme; there is a surjective étale scheme chart of the target along which the base change of f is quasi-separated; and there is a Zariski covering of the target over whose members the base changes of f are quasi-separated.

theorem isQuasiSeparated_tfae (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) :
    List.TFAE [
      IsQuasiSeparated B S hS f,
      (∀ (T : BigFppfOver B S hS) (g : yoneda.obj T ⟶ Y),
        IsQuasiSeparated B S hS (pullback.snd f g)),
      (∀ (T : BigFppfOver B S hS) (g : yoneda.obj T ⟶ Y),
        IsAffine ((BigFppfOver.toScheme B S hS).obj T) →
          IsQuasiSeparated B S hS (pullback.snd f g)),
      (∀ (T : BigFppfOver B S hS) (g : yoneda.obj T ⟶ Y),
        IsAffine ((BigFppfOver.toScheme B S hS).obj T) →
          IsAbsolutelyQuasiSeparated B S hS hZ (pullback f g)),
      (∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
        (MorphismProperty.presheaf (MorphismProperty.inverseImage
          (@Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS))) g ∧
        (MorphismProperty.presheaf (MorphismProperty.inverseImage
          (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS))) g ∧
        IsQuasiSeparated B S hS (pullback.snd f g)),
      (∃ (I : Type u) (U : I → Subfunctor Y),
        IsZariskiCover B S hS I U ∧
        ∀ i, IsQuasiSeparated B S hS (pullback.snd f (U i).ι))
    ]

AlgebraicGeometry.Space.isSeparated_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparatedTfae.lean, line 1360. The attribute's comment: “separated”.

For a morphism f : X ⟶ Y of algebraic spaces over a scheme S the following are equivalent: f is separated; the base change of f along every morphism from a representable presheaf is separated; the same for the test objects with affine underlying scheme; for every affine test object the fibre product is a separated algebraic space over the terminal scheme; there is a surjective étale scheme chart of the target along which the base change of f is separated; and there is a Zariski covering of the target over whose members the base changes of f are separated.

theorem isSeparated_tfae (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) :
    List.TFAE [
      IsSeparated B S hS f,
      (∀ (T : BigFppfOver B S hS) (g : yoneda.obj T ⟶ Y),
        IsSeparated B S hS (pullback.snd f g)),
      (∀ (T : BigFppfOver B S hS) (g : yoneda.obj T ⟶ Y),
        IsAffine ((BigFppfOver.toScheme B S hS).obj T) →
          IsSeparated B S hS (pullback.snd f g)),
      (∀ (T : BigFppfOver B S hS) (g : yoneda.obj T ⟶ Y),
        IsAffine ((BigFppfOver.toScheme B S hS).obj T) →
          IsAbsolutelySeparated B S hS hZ (pullback f g)),
      (∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
        (MorphismProperty.presheaf (MorphismProperty.inverseImage
          (@Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS))) g ∧
        (MorphismProperty.presheaf (MorphismProperty.inverseImage
          (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS))) g ∧
        IsSeparated B S hS (pullback.snd f g)),
      (∃ (I : Type u) (U : I → Subfunctor Y),
        IsZariskiCover B S hS I U ∧
        ∀ i, IsSeparated B S hS (pullback.snd f (U i).ι))
    ]

AlgebraicGeometry.Space.isLocallySeparated_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparatedTfae.lean, line 1407. The attribute's comment: “locally separated”.

For a morphism f : X ⟶ Y of algebraic spaces over a scheme S the following are equivalent: f is locally separated; the base change of f along every morphism from a representable presheaf is locally separated; the same for the test objects with affine underlying scheme; for every affine test object the fibre product is a locally separated algebraic space over the terminal scheme; there is a surjective étale scheme chart of the target along which the base change of f is locally separated; and there is a Zariski covering of the target over whose members the base changes of f are locally separated.

theorem isLocallySeparated_tfae (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    List.TFAE [
      IsLocallySeparated B S hS f,
      (∀ (T : BigFppfOver B S hS) (g : yoneda.obj T ⟶ Y),
        IsLocallySeparated B S hS (pullback.snd f g)),
      (∀ (T : BigFppfOver B S hS) (g : yoneda.obj T ⟶ Y),
        IsAffine ((BigFppfOver.toScheme B S hS).obj T) →
          IsLocallySeparated B S hS (pullback.snd f g)),
      (∀ (T : BigFppfOver B S hS) (g : yoneda.obj T ⟶ Y),
        IsAffine ((BigFppfOver.toScheme B S hS).obj T) →
          IsAbsolutelyLocallySeparated B S hS hZ (pullback f g)),
      (∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
        (MorphismProperty.presheaf (MorphismProperty.inverseImage
          (@Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS))) g ∧
        (MorphismProperty.presheaf (MorphismProperty.inverseImage
          (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS))) g ∧
        IsLocallySeparated B S hS (pullback.snd f g)),
      (∃ (I : Type u) (U : I → Subfunctor Y),
        IsZariskiCover B S hS I U ∧
        ∀ i, IsLocallySeparated B S hS (pullback.snd f (U i).ι))
    ]
Tag 03KY, a lemma

Tag 03KY in the Stacks Project.

AlgebraicGeometry.Space.separationProperties_of_relativelyRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RepresentableSeparationMatch.lean, line 68.

Stacks 03KY. Let S be a scheme and let f : X ⟶ Y be a representable morphism of algebraic spaces over S. Then:

  1. f is locally separated; and
  2. f is separated in the sense of Stacks 03HL if and only if it is separated in the sense of Stacks 03HA, that is, if and only if every represented base change of f is a separated morphism of schemes, and likewise for quasi-separatedness.

In particular, a morphism m of schemes over S is (quasi-)separated in the sense of Stacks 03HL, as the morphism of algebraic spaces yoneda.map m, if and only if it is (quasi-)separated as a morphism of schemes.

Part (1) holds because the relative diagonal of a morphism of schemes is an immersion, by Stacks 01KJ, and local separatedness of a morphism with algebraic source is tested on its represented base changes, by Stacks 03KM, each of which is the Yoneda image of a morphism of the site. Part (2) is the equivalence of conditions (1) and (2) of Stacks 03KM for separatedness and for quasi-separatedness, taken together with the fact that separatedness and quasi-separatedness of the Yoneda image of a morphism of the site are those properties of the underlying morphism of schemes; that last fact, stated for every morphism of the site, is also the concluding assertion.

theorem separationProperties_of_relativelyRepresentable
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y) (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (hf : yoneda.relativelyRepresentable f) :
    IsLocallySeparated B S hS f ∧
      (IsSeparated B S hS f ↔
          (MorphismProperty.presheaf (MorphismProperty.inverseImage
            (@_root_.AlgebraicGeometry.IsSeparated.{u} : MorphismProperty Scheme.{u})
            (BigFppfOver.toScheme B S hS))) f) ∧
      (IsQuasiSeparated B S hS f ↔
          (MorphismProperty.presheaf (MorphismProperty.inverseImage
            (@_root_.AlgebraicGeometry.QuasiSeparated.{u} : MorphismProperty Scheme.{u})
            (BigFppfOver.toScheme B S hS))) f) ∧
      ∀ (a b : BigFppfOver B S hS) (m : a ⟶ b),
        (IsSeparated B S hS (yoneda.map m) ↔
            _root_.AlgebraicGeometry.IsSeparated ((BigFppfOver.toScheme B S hS).map m)) ∧
          (IsQuasiSeparated B S hS (yoneda.map m) ↔
            _root_.AlgebraicGeometry.QuasiSeparated ((BigFppfOver.toScheme B S hS).map m))
Sources
LeanAlgebraicGeometry.relativelyRepresentable_pullbackDiagonal · AlgebraicGeometry.Space.IsSeparated · AlgebraicGeometry.Space.IsLocallySeparated · AlgebraicGeometry.Space.IsQuasiSeparated · AlgebraicGeometry.Space.separationProperties_of_relativelyRepresentable · AlgebraicGeometry.presheaf_locallyOfFiniteType_pullbackDiagonal · AlgebraicGeometry.presheaf_monomorphisms_pullbackDiagonal · AlgebraicGeometry.presheaf_isSeparated_pullbackDiagonal

Section67.5 Surjective morphisms#

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

Tag 03MD, a lemma

Tag 03MD in the Stacks Project.

AlgebraicGeometry.Space.surjective_iff_pointsMap_surjective_of_representable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Surjective.lean, line 337.

Stacks 03MD. A representable morphism of presheaves on the big fppf site of S is surjective — surjective after every representable base change — if and only if the induced map on points is surjective.

No algebraic-space hypothesis is needed: representability of the morphism, which is part of surjectivity in the relative sense, is the only one used.

theorem surjective_iff_pointsMap_surjective_of_representable
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : F ⟶ G)
    (hf : yoneda.relativelyRepresentable f) :
    (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf f ↔
      Function.Surjective (pointsMap B S hS F f)
Tag 03ME, a definition

Tag 03ME in the Stacks Project.

AlgebraicGeometry.Space.IsSurjective, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat.lean, line 48.

A morphism of algebraic spaces over S is surjective when the induced map |X| → |Y| on their sets of points is surjective.

abbrev IsSurjective (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y) : Prop
Tag 03MF, a lemma

Tag 03MF in the Stacks Project.

AlgebraicGeometry.Space.isSurjective_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Surjective.lean, line 233.

Stacks 03MF. For a morphism f : X ⟶ Y of algebraic spaces over S the following are equivalent:

  1. f is surjective;
  2. for every scheme Z in the site and every Z ⟶ Y the projection X ×_Y Z ⟶ Z is surjective;
  3. the same for every affine scheme Z in the site;
  4. there is a scheme V in the site and a surjective étale V ⟶ Y with X ×_Y V ⟶ V surjective;
  5. there is a scheme U in the site and a surjective étale φ : U ⟶ X with φ ≫ f surjective;
  6. there is a commuting square whose vertical arrows are surjective étale charts U ⟶ X and V ⟶ Y of schemes in the site and whose top arrow U ⟶ V is surjective;
  7. there is a Zariski covering of Y by open subspaces Y_i with each f⁻¹(Y_i) ⟶ Y_i surjective.
theorem isSurjective_tfae (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) :
    List.TFAE
      [IsSurjective B S hS f,
        ∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ Y),
          IsSurjective B S hS (pullback.snd f g),
        ∀ (Z : BigFppfOver B S hS), IsAffine ((BigFppfOver.toScheme B S hS).obj Z) →
          ∀ g : yoneda.obj Z ⟶ Y, IsSurjective B S hS (pullback.snd f g),
        ∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
          IsSurjective B S hS g ∧ IsEtale B S hS g ∧
            IsSurjective B S hS (pullback.snd f g),
        ∃ (U : BigFppfOver B S hS) (φ : yoneda.obj U ⟶ X),
          IsSurjective B S hS φ ∧ IsEtale B S hS φ ∧ IsSurjective B S hS (φ ≫ f),
        ∃ (U V : BigFppfOver B S hS) (φ : yoneda.obj U ⟶ X) (ψ : yoneda.obj V ⟶ Y)
            (h : yoneda.obj U ⟶ yoneda.obj V),
          φ ≫ f = h ≫ ψ ∧ IsSurjective B S hS φ ∧ IsEtale B S hS φ ∧
            IsSurjective B S hS ψ ∧ IsEtale B S hS ψ ∧ IsSurjective B S hS h,
        ∃ (I : Type u) (U : I → Subfunctor Y), IsZariskiCover B S hS I U ∧
          ∀ i, IsSurjective B S hS (pullback.snd f (U i).ι)]
Tag 03MG, a lemma

Tag 03MG in the Stacks Project.

AlgebraicGeometry.Space.isSurjective_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SurjectiveFpqcLocalAtTarget.lean, line 76.

A composite of morphisms surjective on points is surjective on points.

theorem isSurjective_comp {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {f : X ⟶ Y} {g : Y ⟶ Z}
    (hf : IsSurjective B S hS f) (hg : IsSurjective B S hS g) :
    IsSurjective B S hS (f ≫ g)
Tag 03MH, a lemma

Tag 03MH in the Stacks Project.

AlgebraicGeometry.Space.isSurjective_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SurjectiveOnPoints.lean, line 373.

A base change of a morphism of algebraic spaces surjective on points is surjective on points.

theorem isSurjective_of_isPullback {W Z X Y : AlgebraicSpaces B S hS}
    {p : W ⟶ Z} {q : W ⟶ X} {g : Z ⟶ Y} {f : X ⟶ Y}
    (sq : IsPullback p q g f) (hg : IsSurjective B S hS g.hom) :
    IsSurjective B S hS q.hom
Sources
LeanAlgebraicGeometry.Space.surjective_iff_pointsMap_surjective_of_representable · AlgebraicGeometry.Space.IsSurjective · AlgebraicGeometry.Space.isSurjective_tfae · AlgebraicGeometry.Space.isSurjective_comp · AlgebraicGeometry.Space.isSurjective_of_isPullback

Section67.6 Open morphisms#

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

Tag 03Z1, a lemma

Tag 03Z1 in the Stacks Project.

AlgebraicGeometry.Space.presheaf_universallyOpen_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Open.lean, line 669.

A representable morphism of algebraic spaces over S is universally open, that is, every base change of it by an algebraic space over S is open on points, exactly when each of its represented base changes is a universally open morphism of schemes.

theorem presheaf_universallyOpen_iff {f : X ⟶ Y}
    (hf : yoneda.relativelyRepresentable f) :
    (MorphismProperty.inverseImage
      (@AlgebraicGeometry.UniversallyOpen.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf f ↔ UniversallyOpen B S hS f
Tag 03Z2, a definition

Tag 03Z2 in the Stacks Project.

AlgebraicGeometry.Space.IsOpenMorphism, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Open.lean, line 117. The attribute's comment: “part (1): open”.

A morphism of algebraic spaces over S is open when the map it induces on points is an open map for the topology detected by scheme-valued points.

abbrev IsOpenMorphism (f : F ⟶ G) : Prop

AlgebraicGeometry.Space.UniversallyOpen, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Open.lean, line 125. The attribute's comment: “part (2): universally open”.

A morphism of algebraic spaces over S is universally open when its base change along every morphism to its target from an algebraic space over S is open.

abbrev UniversallyOpen (f : F ⟶ G) : Prop
Tag 03Z3, a lemma

Tag 03Z3 in the Stacks Project.

AlgebraicGeometry.Space.universallyOpen_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Open.lean, line 211.

A base change of a universally open morphism of algebraic spaces over S is universally open.

theorem universallyOpen_pullback {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (_hX : IsAlgebraicSpace B S hS X) (_hY : IsAlgebraicSpace B S hS Y)
    (_hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Z ⟶ Y)
    (hf : UniversallyOpen B S hS f) :
    UniversallyOpen B S hS (pullback.fst g f)
Tag 03Z4, a lemma

Tag 03Z4 in the Stacks Project.

AlgebraicGeometry.Space.IsOpenMorphism.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Open.lean, line 201. The attribute's comment: “open”.

A composition of open morphisms of algebraic spaces over S is open.

theorem IsOpenMorphism.comp {f : F ⟶ G} {g : G ⟶ H} (hg : IsOpenMorphism B S hS g)
    (hf : IsOpenMorphism B S hS f) :
    IsOpenMorphism B S hS (f ≫ g)

AlgebraicGeometry.Space.universallyOpen_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Open.lean, line 221. The attribute's comment: “universally open”.

A composition of universally open morphisms of algebraic spaces over S is universally open.

theorem universallyOpen_comp {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (_hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : UniversallyOpen B S hS f) (hg : UniversallyOpen B S hS g) :
    UniversallyOpen B S hS (f ≫ g)
Tag 03Z5, a lemma

Tag 03Z5 in the Stacks Project.

AlgebraicGeometry.Space.universallyOpen_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Open.lean, line 422.

For a morphism f : X ⟶ Y of algebraic spaces over S the following are equivalent:

  1. f is universally open;
  2. for every scheme Z in the site and every Z ⟶ Y the projection |Z ×_Y X| → |Z| is open;
  3. the same for every affine scheme Z in the site;
  4. there is a scheme V in the site and a surjective étale V ⟶ Y with V ×_Y X ⟶ V universally open;
  5. there is a Zariski covering of Y by open subspaces Y_i with each f⁻¹(Y_i) ⟶ Y_i universally open.
theorem universallyOpen_tfae (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    List.TFAE
      [UniversallyOpen B S hS f,
        ∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ Y),
          IsOpenMorphism B S hS (pullback.fst g f),
        ∀ (Z : BigFppfOver B S hS), IsAffine ((BigFppfOver.toScheme B S hS).obj Z) →
          ∀ g : yoneda.obj Z ⟶ Y, IsOpenMorphism B S hS (pullback.fst g f),
        ∃ (V : BigFppfOver B S hS) (v : yoneda.obj V ⟶ Y),
          IsSurjective B S hS v ∧ IsEtale B S hS v ∧
            UniversallyOpen B S hS (pullback.fst v f),
        ∃ (I : Type u) (U : I → Subfunctor Y), IsZariskiCover B S hS I U ∧
          ∀ i, UniversallyOpen B S hS (pullback.fst (U i).ι f)]
Tag 06DN, a lemma

Tag 06DN in the Stacks Project.

AlgebraicGeometry.Space.universallyOpen_to_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Open.lean, line 523. References: EGA IV (2.4.10); EGA IV (2.4.9), “Y = Spec k”; SGA 4 VIII (9.4.4), “more general”.

A morphism from an algebraic space over S to a representable presheaf whose representing scheme is the spectrum of a field is universally open.

theorem universallyOpen_to_field (hX : IsAlgebraicSpace B S hS X)
    {K : BigFppfOver B S hS} {k : Type u} [Field k]
    (e : (BigFppfOver.toScheme B S hS).obj K ≅ Spec (CommRingCat.of k))
    (p : X ⟶ yoneda.obj K) :
    UniversallyOpen B S hS p
Sources
LeanAlgebraicGeometry.Space.presheaf_universallyOpen_iff · AlgebraicGeometry.Space.IsOpenMorphism · AlgebraicGeometry.Space.UniversallyOpen · AlgebraicGeometry.Space.universallyOpen_pullback · AlgebraicGeometry.Space.IsOpenMorphism.comp · AlgebraicGeometry.Space.universallyOpen_comp · AlgebraicGeometry.Space.universallyOpen_tfae · AlgebraicGeometry.Space.universallyOpen_to_field

Section67.7 Submersive morphisms#

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

Tag 0CFQ, a lemma

Tag 0CFQ in the Stacks Project.

AlgebraicGeometry.Space.presheaf_universallySubmersive_iff_universallySubmersive, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Submersive.lean, line 1123.

Stacks 0CFQ. A representable morphism f : X ⟶ Y of algebraic spaces over S is universally submersive in the sense of Stacks 03HA — each of its represented base changes is a universally submersive morphism of schemes — if and only if every base change of it by an algebraic space over S is submersive on points, which is universal submersiveness in the sense of Stacks 0412, part (2).

The implication from left to right chooses a scheme atlas a : U ⟶ Z of the base Z: the chosen represented base change of f along a ≫ g is a quotient map of schemes, hence on points, and it factors through the base change along g by a continuous map, so Topology.IsQuotientMap.of_comp gives the conclusion.

The converse must upgrade quotient-map-ness of the base changes available inside the size cutoff of the site to the unbounded CategoryTheory.MorphismProperty.universally. That is what the affine-space test AlgebraicGeometry.Space.quotientMap_of_affineSpace_tests is for: the base changes of a represented base change to the affine spaces over its target are inside the cutoff once the index type is small, by AlgebraicGeometry.Space.quotientMap_of_small_baseChange, and AlgebraicGeometry.Space.quotientMap_affineSpace_map_of_small removes the smallness restriction. No algebraicity hypothesis on X or Y is needed, only representability of f.

theorem presheaf_universallySubmersive_iff_universallySubmersive (f : X ⟶ Y)
    (hf : yoneda.relativelyRepresentable f) :
    (MorphismProperty.inverseImage
        ((topologically @Topology.IsQuotientMap : MorphismProperty Scheme.{u}).universally)
        (BigFppfOver.toScheme B S hS)).presheaf f ↔
      UniversallySubmersive B S hS f
Tag 0412, a definition

Tag 0412 in the Stacks Project.

AlgebraicGeometry.Space.IsSubmersive, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Submersive.lean, line 142. The attribute's comment: “part (1): submersive”. References: EGA IV (15.7.8), “more general”; SGA 1 IX (2.1), “submersive”.

Stacks 0412, part (1). A morphism of algebraic spaces over S is submersive when the map it induces on points is a quotient map for the topology detected by scheme-valued points.

This is unrelated to the notion of a submersion of differential manifolds.

abbrev IsSubmersive (f : F ⟶ G) : Prop

AlgebraicGeometry.Space.UniversallySubmersive, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Submersive.lean, line 151. The attribute's comment: “part (2): universally submersive”. References: SGA 1 IX (2.1), “univ. submersive”.

Stacks 0412, part (2). A morphism of algebraic spaces over S is universally submersive when its base change along every morphism to its target from an algebraic space over S is submersive.

abbrev UniversallySubmersive (f : F ⟶ G) : Prop
Tag 0CFR, a lemma

Tag 0CFR in the Stacks Project.

AlgebraicGeometry.Space.universallySubmersive_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Submersive.lean, line 263.

Stacks 0CFR. A base change of a universally submersive morphism of algebraic spaces over S is universally submersive.

Nothing is needed beyond unwinding the definition: a base change of Z ×_Y X ⟶ Z along k : W ⟶ Z is a base change of X ⟶ Y along k ≫ g.

theorem universallySubmersive_pullback {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (_hX : IsAlgebraicSpace B S hS X) (_hY : IsAlgebraicSpace B S hS Y)
    (_hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Z ⟶ Y)
    (hf : UniversallySubmersive B S hS f) :
    UniversallySubmersive B S hS (pullback.fst g f)
Tag 0CFS, a lemma

Tag 0CFS in the Stacks Project.

AlgebraicGeometry.Space.IsSubmersive.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Submersive.lean, line 250. The attribute's comment: “submersive”.

Stacks 0CFS, submersive morphisms. A composition of submersive morphisms of algebraic spaces over S is submersive: the map on points of a composition is the composition of the maps on points.

theorem IsSubmersive.comp {f : F ⟶ G} {g : G ⟶ H} (hg : IsSubmersive B S hS g)
    (hf : IsSubmersive B S hS f) :
    IsSubmersive B S hS (f ≫ g)

AlgebraicGeometry.Space.universallySubmersive_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Submersive.lean, line 277. The attribute's comment: “universally submersive”.

Stacks 0CFS, universally submersive morphisms. A composition of universally submersive morphisms of algebraic spaces over S is universally submersive.

The base change W ×_Z X ⟶ W of the composite along k : W ⟶ Z is identified by the pasting isomorphism W ×_Z X ≅ (W ×_Z Y) ×_Y X with the composition of a base change of X ⟶ Y and a base change of Y ⟶ Z.

theorem universallySubmersive_comp {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (_hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : UniversallySubmersive B S hS f) (hg : UniversallySubmersive B S hS g) :
    UniversallySubmersive B S hS (f ≫ g)
Sources
LeanAlgebraicGeometry.Space.presheaf_universallySubmersive_iff_universallySubmersive · AlgebraicGeometry.Space.IsSubmersive · AlgebraicGeometry.Space.UniversallySubmersive · AlgebraicGeometry.Space.universallySubmersive_pullback · AlgebraicGeometry.Space.IsSubmersive.comp · AlgebraicGeometry.Space.universallySubmersive_comp

Section67.8 Quasi-compact morphisms#

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

Tag 03HC, the section

Tag 03HC in the Stacks Project.

Declarations registered for the tag:

Tag 03HD, a lemma

Tag 03HD in the Stacks Project.

AlgebraicGeometry.Space.presheaf_quasiCompact_iff_isQuasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/QuasiCompact.lean, line 128.

For a representable morphism of algebraic spaces over S the two readings of quasi-compactness agree: every represented base change of it is a quasi-compact morphism of schemes exactly when every base change of it along a morphism from a quasi-compact algebraic space has quasi-compact source.

theorem presheaf_quasiCompact_iff_isQuasiCompact {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {f : F ⟶ G} (hf : yoneda.relativelyRepresentable f) :
    (MorphismProperty.inverseImage (@AlgebraicGeometry.QuasiCompact.{u})
        (BigFppfOver.toScheme B S hS)).presheaf f ↔
      IsQuasiCompact B S hS f

AlgebraicGeometry.Space.isQuasiCompact_of_presheaf_quasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactComposition.lean, line 56. The attribute's comment: “part (1) implies part (2)”.

A morphism of presheaves on the big fppf site of S which is representable and quasi-compact after every representable base change is quasi-compact: every base change of it along a morphism from a quasi-compact algebraic space has quasi-compact source.

theorem isQuasiCompact_of_presheaf_quasiCompact
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : X ⟶ Y}
    (hf : (MorphismProperty.inverseImage
      (@AlgebraicGeometry.QuasiCompact.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf f) :
    IsQuasiCompact B S hS f
Tag 03HE, a definition

Tag 03HE in the Stacks Project.

AlgebraicGeometry.Space.IsQuasiCompact, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms.lean, line 262.

Stacks 03HE. A morphism of algebraic spaces over S is quasi-compact when every base change of it along a morphism from a quasi-compact algebraic space has quasi-compact source.

abbrev IsQuasiCompact (f : F ⟶ G) : Prop
Tag 0EMK, a lemma

Tag 0EMK in the Stacks Project.

AlgebraicGeometry.Space.isQuasiCompactMap_pointsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactOnPoints.lean, line 52.

A quasi-compact morphism f : X ⟶ Y of algebraic spaces over S induces a quasi-compact map |X| → |Y| of point spaces: the preimage of a quasi-compact open subset of |Y| is quasi-compact.

theorem isQuasiCompactMap_pointsMap {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (hf : IsQuasiCompact B S hS f) :
    ∀ ⦃U : Set (points B S hS Y)⦄, IsOpen U → IsCompact U →
      IsCompact (pointsMap B S hS X f ⁻¹' U)
Tag 03HF, a lemma

Tag 03HF in the Stacks Project.

AlgebraicGeometry.Space.isQuasiCompact_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MapDescent.lean, line 137.

Quasi-compactness of a morphism of algebraic spaces is stable under base change: in a cartesian square, the base change b of a quasi-compact p is quasi-compact.

theorem isQuasiCompact_of_isPullback {F G F' G' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {a : F ⟶ F'} {b : F ⟶ G} {p : F' ⟶ G'} {q : G ⟶ G'}
    (sq : IsPullback a b p q) (hp : IsQuasiCompact B S hS p) : IsQuasiCompact B S hS b
Tag 03HG, a lemma

Tag 03HG in the Stacks Project.

AlgebraicGeometry.Space.IsQuasiCompact.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactComposition.lean, line 80.

The composition of a pair of quasi-compact morphisms of algebraic spaces over S is quasi-compact.

theorem IsQuasiCompact.comp
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : X ⟶ Y} {g : Y ⟶ Z}
    (hY : IsAlgebraicSpace B S hS Y) (hZ : IsAlgebraicSpace B S hS Z)
    (hf : IsQuasiCompact B S hS f) (hg : IsQuasiCompact B S hS g) :
    IsQuasiCompact B S hS (f ≫ g)
Tag 040W, a lemma

Tag 040W in the Stacks Project.

AlgebraicGeometry.Space.isQuasiCompactSpaceULift_of_isSurjectiveULift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LargeValuedQuasiCompactPoints.lean, line 208. The attribute's comment: “part (1), for a value universe independent of the universe of the schemes”.

Stacks 040W, part (1), for a value universe max w u independent of the universe u of the schemes: if f : F ⟶ G is a surjective morphism of algebraic spaces over S and F is quasi-compact, then G is quasi-compact. The point space of G is the image of the quasi-compact point space of F under a continuous surjection.

theorem isQuasiCompactSpaceULift_of_isSurjectiveULift
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type (max w u)}
    (hF : IsAlgebraicSpaceULift.{w} B S hS F) (hG : IsAlgebraicSpaceULift.{w} B S hS G)
    (f : F ⟶ G) (hf : IsSurjectiveULift.{w} B S hS f)
    (h : IsQuasiCompactSpaceULift.{w} B S hS F) :
    IsQuasiCompactSpaceULift.{w} B S hS G

AlgebraicGeometry.Space.isQuasiCompactSpace_of_isSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/QuasiCompact.lean, line 178. The attribute's comment: “part (1)”.

The image of a quasi-compact algebraic space over S under a surjective morphism of algebraic spaces over S is quasi-compact.

theorem isQuasiCompactSpace_of_isSurjective {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hF : IsAlgebraicSpace B S hS F) (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G)
    (hf : IsSurjective B S hS f) (hFqc : IsQuasiCompactSpace B S hS F) :
    IsQuasiCompactSpace B S hS G

AlgebraicGeometry.Space.isQuasiCompact_of_comp_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/QuasiCompact.lean, line 189. The attribute's comment: “part (2)”.

In a commuting triangle p = f ≫ q of morphisms of algebraic spaces over S whose horizontal morphism f is surjective, quasi-compactness of p implies quasi-compactness of q.

theorem isQuasiCompact_of_comp_surjective {F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hF : IsAlgebraicSpace B S hS F) (hG : IsAlgebraicSpace B S hS G)
    (hH : IsAlgebraicSpace B S hS H) (f : F ⟶ G) (p : F ⟶ H) (q : G ⟶ H) (hcomm : p = f ≫ q)
    (hf : IsSurjective B S hS f) (hp : IsQuasiCompact B S hS p) :
    IsQuasiCompact B S hS q

AlgebraicGeometry.Space.IsQuasiCompactSpace.of_isSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactSurjection.lean, line 60. The attribute's comment: “part (1): quasi-compactness of the target”.

Stacks 040W, part (1). The image of a quasi-compact algebraic space under a surjective morphism of algebraic spaces over S is quasi-compact: if f : X ⟶ Y is surjective on points and X is quasi-compact, then Y is quasi-compact.

theorem IsQuasiCompactSpace.of_isSurjective {f : X ⟶ Y}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsSurjective B S hS f) (h : IsQuasiCompactSpace B S hS X) :
    IsQuasiCompactSpace B S hS Y

AlgebraicGeometry.Space.IsQuasiCompact.of_isSurjective_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactSurjection.lean, line 72. The attribute's comment: “part (2): quasi-compactness of a morphism”. References: EGA IV (1.1.3).

Stacks 040W, part (2). In a commuting triangle f ≫ q = p of morphisms of algebraic spaces over S whose horizontal arrow f is surjective, quasi-compactness of p implies quasi-compactness of q.

theorem IsQuasiCompact.of_isSurjective_comp {f : X ⟶ Y} {p : X ⟶ Z} {q : Y ⟶ Z}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (hcomm : f ≫ q = p)
    (hf : IsSurjective B S hS f) (hp : IsQuasiCompact B S hS p) :
    IsQuasiCompact B S hS q
Tag 04ZJ, a lemma

Tag 04ZJ in the Stacks Project.

AlgebraicGeometry.Space.isQuasiCompact_of_universallyOpen_isSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/QuasiCompact.lean, line 322.

Let g : G' ⟶ G be a universally open surjective morphism of algebraic spaces over S. If the base change of f : F ⟶ G along g is quasi-compact, then so is f.

theorem isQuasiCompact_of_universallyOpen_isSurjective
    {F G G' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hF : IsAlgebraicSpace B S hS F)
    (hG : IsAlgebraicSpace B S hS G) (hG' : IsAlgebraicSpace B S hS G') (f : F ⟶ G)
    (g : G' ⟶ G) (hgopen : UniversallyOpen B S hS g) (hgsurj : IsSurjective B S hS g)
    (hf : IsQuasiCompact B S hS (pullback.fst g f)) :
    IsQuasiCompact B S hS f
Tag 03KG, a lemma

Tag 03KG in the Stacks Project.

AlgebraicGeometry.Space.isQuasiCompact_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/QuasiCompact.lean, line 248.

For a morphism f : F ⟶ G of algebraic spaces over S the following six conditions are equivalent: f is quasi-compact; the base change of f along every morphism to G from a presheaf represented by an object of the site is quasi-compact; for every such object with affine underlying scheme the fibre product is a quasi-compact algebraic space; the base change of f along some surjective étale morphism to G from a represented presheaf is quasi-compact; the same for some surjective étale morphism from an arbitrary algebraic space; and there is a Zariski covering of G along each member of which the base change of f is quasi-compact.

theorem isQuasiCompact_tfae {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hF : IsAlgebraicSpace B S hS F) (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G) :
    List.TFAE
      [IsQuasiCompact B S hS f,
        ∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ G),
          IsQuasiCompact B S hS (pullback.fst g f),
        ∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ G),
          IsAffine ((BigFppfOver.toScheme B S hS).obj Z) →
            IsQuasiCompactSpace B S hS (pullback g f),
        ∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ G),
          IsSurjective B S hS g ∧ IsEtale B S hS g ∧
            IsQuasiCompact B S hS (pullback.fst g f),
        ∃ (G' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_ : IsAlgebraicSpace B S hS G')
          (g : G' ⟶ G), IsSurjective B S hS g ∧ IsEtale B S hS g ∧
            IsQuasiCompact B S hS (pullback.fst g f),
        ∃ (I : Type u) (U : I → Subfunctor G) (_ : IsZariskiCover B S hS I U),
          ∀ i, IsQuasiCompact B S hS (pullback.fst (U i).ι f)]

AlgebraicGeometry.Space.isQuasiCompact_pullback_snd_of_isQuasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactEtaleLocalTarget.lean, line 319. The attribute's comment: “part (1) implies part (2)”.

Stacks 03KG, part (1) implies part (2). If f : X ⟶ Y is a quasi-compact morphism of algebraic spaces over S, then for every object Z of the site and every g : h_Z ⟶ Y the projection Z ×_Y X ⟶ h_Z is quasi-compact.

This is Stacks 03HF, AlgebraicGeometry.Space.isQuasiCompact_of_isPullback, read at the cartesian square of the chosen fibre product; no representability of Z is used.

theorem isQuasiCompact_pullback_snd_of_isQuasiCompact
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : X ⟶ Y} (hf : IsQuasiCompact B S hS f)
    (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ Y) :
    IsQuasiCompact B S hS (pullback.snd f g)

AlgebraicGeometry.Space.isQuasiCompactSpace_pullback_of_isQuasiCompact_pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactEtaleLocalTarget.lean, line 335. The attribute's comment: “part (2) implies part (3)”.

Stacks 03KG, part (2) implies part (3). If every projection Z ×_Y X ⟶ h_Z of f : X ⟶ Y along a morphism from a represented presheaf is quasi-compact, then Z ×_Y X is a quasi-compact algebraic space whenever the scheme underlying Z is affine.

An affine object of the site represents a quasi-compact algebraic space, and AlgebraicGeometry.Space.isQuasiCompactSpace_source_of_isQuasiCompact then transfers quasi-compactness from the target of the projection to its source. Only the single instance g of part (2) is used, not the whole of it, and the algebraic-space hypotheses _hX and _hY are retained from the source but are not needed.

theorem isQuasiCompactSpace_pullback_of_isQuasiCompact_pullback_snd
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (_hX : IsAlgebraicSpace B S hS X) (_hY : IsAlgebraicSpace B S hS Y)
    (h : ∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ Y),
      IsQuasiCompact B S hS (pullback.snd f g))
    (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ Y)
    (hZ : IsAffine ((BigFppfOver.toScheme B S hS).obj Z)) :
    IsQuasiCompactSpace B S hS (pullback f g)

AlgebraicGeometry.Space.isQuasiCompact_of_isQuasiCompactSpace_pullback_affine', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactEtaleLocalTarget.lean, line 362. The attribute's comment: “part (3) implies part (1)”.

Stacks 03KG, part (3) implies part (1): quasi-compactness of a morphism of algebraic spaces may be tested on affine schemes. If Z ×_Y X is a quasi-compact algebraic space for every object Z of the site with affine underlying scheme and every g : h_Z ⟶ Y, then f : X ⟶ Y is quasi-compact.

A quasi-compact algebraic space has a surjective étale morphism from an affine scheme by Stacks 03H6, and AlgebraicGeometry.Space.isQuasiCompactSpace_pullback_of_isSurjective replaces the test object by that affine scheme.

AlgebraicGeometry.Space.isQuasiCompact_of_isQuasiCompactSpace_pullback_affine is the same assertion with the fibre product of the hypothesis taken in the other order and the two algebraic-space hypotheses in front of the morphism.

theorem isQuasiCompact_of_isQuasiCompactSpace_pullback_affine'
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (h : ∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ Y),
      IsAffine ((BigFppfOver.toScheme B S hS).obj Z) →
        IsQuasiCompactSpace B S hS (pullback f g)) :
    IsQuasiCompact B S hS f

AlgebraicGeometry.Space.isQuasiCompact_of_surjectiveEtale_atlas, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactEtaleLocalTarget.lean, line 389. The attribute's comment: “part (4) implies part (1)”.

Stacks 03KG, part (4) implies part (1): quasi-compactness of a morphism of algebraic spaces is étale-local on the target. Let f : X ⟶ Y be a morphism of algebraic spaces over S. If there are an object V of the site and a surjective étale morphism φ : h_V ⟶ Y such that the projection V ×_Y X ⟶ h_V is quasi-compact, then f is quasi-compact.

This is the leg of Stacks 03KG that the proof of Stacks 03JV uses in passing from its condition (3) to its condition (4). Quasi-compactness of an arbitrary test object is reduced in two steps — to an affine scheme chart of it, which is part (3) implies part (1), and from there to a quasi-compact object factoring through φ by AlgebraicGeometry.Space.exists_compactSpace_factoring_of_isSurjective_isEtale — after which the hypothesis applies directly.

theorem isQuasiCompact_of_surjectiveEtale_atlas
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (V : BigFppfOver B S hS) (φ : yoneda.obj V ⟶ Y)
    (hsurj : IsSurjective B S hS φ) (hφ : IsEtale B S hS φ)
    (h : IsQuasiCompact B S hS (pullback.snd f φ)) :
    IsQuasiCompact B S hS f

AlgebraicGeometry.Space.exists_surjectiveEtale_atlas_isQuasiCompact_pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactEtaleLocalTarget.lean, line 423. The attribute's comment: “part (1) implies part (4)”.

Stacks 03KG, part (1) implies part (4). A quasi-compact morphism f : X ⟶ Y of algebraic spaces over S has a surjective étale chart φ : h_V ⟶ Y of its target along which its base change V ×_Y X ⟶ h_V is quasi-compact.

Any scheme atlas of Y will do: it is surjective and étale by Stacks 03H5 and by multiplicativity of the represented étale morphisms, and the base change of f along it is quasi-compact by Stacks 03HF. Together with AlgebraicGeometry.Space.isQuasiCompact_of_surjectiveEtale_atlas this makes conditions (1) and (4) of Stacks 03KG equivalent, and it exhibits the hypothesis of that statement as satisfiable.

theorem exists_surjectiveEtale_atlas_isQuasiCompact_pullback_snd
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hY : IsAlgebraicSpace B S hS Y) (hf : IsQuasiCompact B S hS f) :
    ∃ (V : BigFppfOver B S hS) (φ : yoneda.obj V ⟶ Y),
      IsSurjective B S hS φ ∧ IsEtale B S hS φ ∧
      IsQuasiCompact B S hS (pullback.snd f φ)

AlgebraicGeometry.Space.exists_isAlgebraicSpace_surjectiveEtale_isQuasiCompact_pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactEtaleLocalTarget.lean, line 441. The attribute's comment: “part (4) implies part (5)”.

Stacks 03KG, part (4) implies part (5). A surjective étale chart of Y by an object of the site is in particular a surjective étale morphism of algebraic spaces onto Y.

The presheaf represented by an object of the site is an algebraic space, so this is a repackaging; it is stated so that the implications recorded for Tag 03KG reach condition (5) in the shape the source gives it.

theorem exists_isAlgebraicSpace_surjectiveEtale_isQuasiCompact_pullback_snd
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (V : BigFppfOver B S hS) (φ : yoneda.obj V ⟶ Y)
    (hsurj : IsSurjective B S hS φ) (hφ : IsEtale B S hS φ)
    (h : IsQuasiCompact B S hS (pullback.snd f φ)) :
    ∃ (Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_hY' : IsAlgebraicSpace B S hS Y')
      (g : Y' ⟶ Y), IsSurjective B S hS g ∧ IsEtale B S hS g ∧
        IsQuasiCompact B S hS (pullback.snd f g)

AlgebraicGeometry.Space.exists_surjectiveEtale_atlas_of_isAlgebraicSpace_surjectiveEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactEtaleLocalTarget.lean, line 462. The attribute's comment: “part (5) implies part (4)”.

Stacks 03KG, part (5) implies part (4): an algebraic-space chart may be replaced by a scheme chart. If g : Y' ⟶ Y is a surjective étale morphism of algebraic spaces over S along which the base change of f : X ⟶ Y is quasi-compact, then the same holds for a chart of Y by an object of the site.

Compose g with a scheme atlas a : h_V ⟶ Y' of Y'. The composite is surjective on points because AlgebraicGeometry.Space.pointsMap is functorial, étale because AlgebraicGeometry.Space.IsEtale g tests exactly the étale charts of Y', and the base change of f along it is a base change of the base change along g, hence quasi-compact by Stacks 03HF. Note that Y itself need not be assumed an algebraic space.

theorem exists_surjectiveEtale_atlas_of_isAlgebraicSpace_surjectiveEtale
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    {Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hY' : IsAlgebraicSpace B S hS Y')
    (g : Y' ⟶ Y) (hsurj : IsSurjective B S hS g) (hg : IsEtale B S hS g)
    (h : IsQuasiCompact B S hS (pullback.snd f g)) :
    ∃ (V : BigFppfOver B S hS) (φ : yoneda.obj V ⟶ Y),
      IsSurjective B S hS φ ∧ IsEtale B S hS φ ∧
      IsQuasiCompact B S hS (pullback.snd f φ)

AlgebraicGeometry.Space.isQuasiCompact_of_zariskiCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactZariskiLocalTarget.lean, line 218. The attribute's comment: “part (6) implies part (1)”.

Let f : X ⟶ Y be a morphism of algebraic spaces over S. If there is a Zariski covering of Y by open subspaces W i, that is one whose point sets cover the space of points of Y, such that each of the morphisms f⁻¹(W i) ⟶ W i, that is pullback.snd f (W i).ι, is quasi-compact, then f is quasi-compact.

theorem isQuasiCompact_of_zariskiCover
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    {I : Type u} (W : I → Subfunctor Y) (hW : ∀ i, IsOpenSubspace B S hS (W i))
    (hcov : ∀ y : points B S hS Y, ∃ i,
      y ∈ Set.range (pointsMap B S hS (W i).toFunctor (W i).ι))
    (h : ∀ i, IsQuasiCompact B S hS (pullback.snd f (W i).ι)) :
    IsQuasiCompact B S hS f

AlgebraicGeometry.Space.exists_zariskiCover_isQuasiCompact_pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactZariskiLocalTarget.lean, line 232. The attribute's comment: “part (1) implies part (6)”.

A quasi-compact morphism f : X ⟶ Y of algebraic spaces over S admits a Zariski covering of Y over each member of which its restriction is quasi-compact.

theorem exists_zariskiCover_isQuasiCompact_pullback_snd
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hY : IsAlgebraicSpace B S hS Y) (hf : IsQuasiCompact B S hS f) :
    ∃ (I : Type u) (W : I → Subfunctor Y), (∀ i, IsOpenSubspace B S hS (W i)) ∧
      (∀ y : points B S hS Y, ∃ i,
        y ∈ Set.range (pointsMap B S hS (W i).toFunctor (W i).ι)) ∧
      ∀ i, IsQuasiCompact B S hS (pullback.snd f (W i).ι)
Tag 03KS, a lemma

Tag 03KS in the Stacks Project.

AlgebraicGeometry.Space.isQuasiCompact_of_comp_of_isQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/QuasiCompact.lean, line 148. References: EGA IV (1.2.4).

If a composite of morphisms of algebraic spaces over S is quasi-compact and its second factor is quasi-separated, then its first factor is quasi-compact.

theorem isQuasiCompact_of_comp_of_isQuasiSeparated {F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : F ⟶ G) (g : G ⟶ H) (hF : IsAlgebraicSpace B S hS F)
    (hH : IsAlgebraicSpace B S hS H) (hgf : IsQuasiCompact B S hS (f ≫ g))
    (hg : IsQuasiSeparated B S hS g) :
    IsQuasiCompact B S hS f
Tag 073B, a lemma

Tag 073B in the Stacks Project.

AlgebraicGeometry.Space.isQuasiSeparated_of_isAbsolutelyQuasiSeparated_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/QuasiCompact.lean, line 401. The attribute's comment: “part (2): quasi-separated”.

Every morphism of algebraic spaces over S out of a quasi-separated algebraic space is quasi-separated.

theorem isQuasiSeparated_of_isAbsolutelyQuasiSeparated_source
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hF : IsAlgebraicSpace B S hS F)
    (hFqs : IsAbsolutelyQuasiSeparated B S hS hZ F) (f : F ⟶ G) :
    IsQuasiSeparated B S hS f

AlgebraicGeometry.Space.isQuasiCompactSpace_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/QuasiCompact.lean, line 411. The attribute's comment: “part (3): quasi-compact”.

A fibre product of quasi-compact algebraic spaces over S over a quasi-separated algebraic space is quasi-compact.

theorem isQuasiCompactSpace_pullback {F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : F ⟶ H)
    (g : G ⟶ H) (hF : IsAlgebraicSpace B S hS F) (hH : IsAlgebraicSpace B S hS H)
    (hFqc : IsQuasiCompactSpace B S hS F) (hGqc : IsQuasiCompactSpace B S hS G)
    (hHqs : IsAbsolutelyQuasiSeparated B S hS hZ H) :
    IsQuasiCompactSpace B S hS (pullback f g)

AlgebraicGeometry.Space.isAbsolutelyQuasiSeparated_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/QuasiCompact.lean, line 420. The attribute's comment: “part (3): quasi-separated”.

A fibre product of quasi-separated algebraic spaces over S is quasi-separated.

theorem isAbsolutelyQuasiSeparated_pullback {F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : F ⟶ H) (g : G ⟶ H) (hF : IsAlgebraicSpace B S hS F)
    (hG : IsAlgebraicSpace B S hS G) (hH : IsAlgebraicSpace B S hS H)
    (hFqs : IsAbsolutelyQuasiSeparated B S hS hZ F)
    (hGqs : IsAbsolutelyQuasiSeparated B S hS hZ G) :
    IsAbsolutelyQuasiSeparated B S hS hZ (pullback f g)

AlgebraicGeometry.Space.isQuasiCompact_of_isQuasiCompactSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactSupport.lean, line 171. The attribute's comment: “part (1)”. References: SGA 4 VI (1.14), “(i), algebraic spaces”.

A morphism from a quasi-compact algebraic space into a quasi-separated algebraic space is quasi-compact.

theorem isQuasiCompact_of_isQuasiCompactSpace
    {X U : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hXqs : IsAbsolutelyQuasiSeparated B S hS hZ X)
    (hUqc : IsQuasiCompactSpace B S hS U) (ι : U ⟶ X) :
    IsQuasiCompact B S hS ι
Sources
LeanAlgebraicGeometry.Space.IsQuasiCompact · AlgebraicGeometry.Space.presheaf_quasiCompact_iff_isQuasiCompact · AlgebraicGeometry.Space.isQuasiCompact_of_isQuasiCompactSpace · AlgebraicGeometry.Space.isQuasiCompact_of_presheaf_quasiCompact · AlgebraicGeometry.Space.isQuasiCompactMap_pointsMap · AlgebraicGeometry.Space.isQuasiCompact_of_isPullback · AlgebraicGeometry.Space.IsQuasiCompact.comp · AlgebraicGeometry.Space.isQuasiCompactSpaceULift_of_isSurjectiveULift

Section67.9 Universally closed morphisms#

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

Tag 03XD, a lemma

Tag 03XD in the Stacks Project.

AlgebraicGeometry.Space.presheaf_universallyClosed_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversallyClosedRepresentable.lean, line 265.

Stacks 03XD. A representable morphism of algebraic spaces over S is universally closed in the sense of Stacks 03HI exactly when each of its represented base changes is a universally closed morphism of schemes.

theorem presheaf_universallyClosed_iff
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (hf : yoneda.relativelyRepresentable f) :
    (MorphismProperty.inverseImage
      (@AlgebraicGeometry.UniversallyClosed.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf f ↔ UniversallyClosed B S hS f
Tag 03HI, a definition

Tag 03HI in the Stacks Project.

AlgebraicGeometry.Space.IsClosedMorphism, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversallyClosed.lean, line 117. The attribute's comment: “closed”.

A morphism of algebraic spaces over S is closed when the map it induces on points is a closed map for the topology detected by scheme-valued points.

abbrev IsClosedMorphism (f : F ⟶ G) : Prop

AlgebraicGeometry.Space.UniversallyClosed, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversallyClosed.lean, line 125. The attribute's comment: “universally closed”.

A morphism of algebraic spaces over S is universally closed when its base change along every morphism to its target from an algebraic space over S is closed.

abbrev UniversallyClosed (f : F ⟶ G) : Prop
Tag 03IS, a lemma

Tag 03IS in the Stacks Project.

AlgebraicGeometry.Space.universallyClosed_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparationMorphismProperties.lean, line 143.

A base change of a universally closed morphism of algebraic spaces over S is universally closed.

theorem universallyClosed_pullback {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : X ⟶ Y) (g : Z ⟶ Y) (hf : UniversallyClosed B S hS f) :
    UniversallyClosed B S hS (pullback.fst g f)
Tag 03IU, a lemma

Tag 03IU in the Stacks Project.

AlgebraicGeometry.Space.isClosedMorphism_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparationMorphismProperties.lean, line 129. The attribute's comment: “closed”.

A composition of closed morphisms of algebraic spaces over S is closed.

theorem isClosedMorphism_comp {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : X ⟶ Y) (g : Y ⟶ Z) (hf : IsClosedMorphism B S hS f)
    (hg : IsClosedMorphism B S hS g) :
    IsClosedMorphism B S hS (f ≫ g)

AlgebraicGeometry.Space.universallyClosed_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparationMorphismProperties.lean, line 158. The attribute's comment: “universally closed”.

A composition of universally closed morphisms of algebraic spaces over S is universally closed.

theorem universallyClosed_comp {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hY : IsAlgebraicSpace B S hS Y) (hZ : IsAlgebraicSpace B S hS Z)
    (f : X ⟶ Y) (g : Y ⟶ Z) (hf : UniversallyClosed B S hS f)
    (hg : UniversallyClosed B S hS g) :
    UniversallyClosed B S hS (f ≫ g)
Tag 03IT, a lemma

Tag 03IT in the Stacks Project.

AlgebraicGeometry.Space.universallyClosed_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/UniversallyClosed.lean, line 427.

Stacks 03IT. For a morphism f : X ⟶ Y of algebraic spaces over S the following are equivalent: f is universally closed; the base change of f along every morphism to Y from a presheaf represented by an object of the site is closed; the same for the objects with affine underlying scheme; the base change of f along some surjective étale morphism to Y from a represented presheaf is universally closed; and there is a Zariski covering of Y along each member of which the base change of f is universally closed.

Algebraicity of the source is retained from the source statement and is not used.

theorem universallyClosed_tfae (_hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    List.TFAE
      [UniversallyClosed B S hS f,
        ∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ Y),
          IsClosedMorphism B S hS (pullback.fst g f),
        ∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ Y),
          IsAffine ((BigFppfOver.toScheme B S hS).obj Z) →
            IsClosedMorphism B S hS (pullback.fst g f),
        ∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
          IsSurjective B S hS g ∧ IsEtale B S hS g ∧
            UniversallyClosed B S hS (pullback.fst g f),
        ∃ (I : Type u) (U : I → Subfunctor Y) (_ : IsZariskiCover B S hS I U),
          ∀ i, UniversallyClosed B S hS (pullback.fst (U i).ι f)]
Tag 03IV, an example

Tag 03IV in the Stacks Project.

AlgebraicGeometry.AffineLineTranslation.structureMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/UniversallyClosed.lean, line 1342. The attribute's comment: “the structure morphism”.

Stacks 03IV. The structure morphism of the quotient 𝔸¹_k/ℤ of Stacks 02Z7, the unique morphism to the terminal object Spec k of the big fppf site over Spec k.

noncomputable def structureMap :
    translationQuotient k B hS hU ⟶ yoneda.obj (Over.mk (𝟙 (B.obj hS)))

AlgebraicGeometry.AffineLineTranslation.universallyClosed_structureMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/UniversallyClosed.lean, line 1440. The attribute's comment: “universally closed”.

Stacks 03IV. For a field k of characteristic zero the structure morphism of the quotient 𝔸¹_k/ℤ of Stacks 02Z7 to Spec k is universally closed.

The source calls this a strange example because the quotient is, by Stacks 02Z7, an algebraic space which is not a scheme. The statement needs no hypothesis beyond characteristic zero — in particular none of the effective fppf descent of Stacks 0265, which the representability of the quotient's chart does need.

theorem universallyClosed_structureMap [CharZero k] :
    Space.UniversallyClosed B (Spec (.of k)) hS (structureMap k B hS hU)
Tag 04XW, a lemma

Tag 04XW in the Stacks Project.

AlgebraicGeometry.Space.isQuasiCompact_of_universallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/UniversallyClosed.lean, line 670.

Stacks 04XW. A universally closed morphism of algebraic spaces over S is quasi-compact.

theorem isQuasiCompact_of_universallyClosed
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hF : IsAlgebraicSpace B S hS F)
    (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G) (hf : UniversallyClosed B S hS f) :
    IsQuasiCompact B S hS f
Tag 05Z2, a lemma

Tag 05Z2 in the Stacks Project.

AlgebraicGeometry.Space.isSeparated_of_isSurjective_of_universallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/UniversallyClosed.lean, line 695. The attribute's comment: “part (4): separated over the base”.

Stacks 05Z2, part (4). Let X ⟶ Y ⟶ T be morphisms of algebraic spaces over S, with X ⟶ Y surjective and universally closed. If X is separated over T, then so is Y.

theorem isSeparated_of_isSurjective_of_universallyClosed
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hT : IsAlgebraicSpace B S hS T) (f : X ⟶ Y) (g : Y ⟶ T)
    (hfsurj : IsSurjective B S hS f) (hfclosed : UniversallyClosed B S hS f)
    (hsep : IsSeparated B S hS (f ≫ g)) :
    IsSeparated B S hS g

AlgebraicGeometry.Space.isQuasiSeparated_of_isSurjective_of_universallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/UniversallyClosed.lean, line 753. The attribute's comment: “part (3): quasi-separated over the base”.

Stacks 05Z2, part (3). Let X ⟶ Y ⟶ T be morphisms of algebraic spaces over S, with X ⟶ Y surjective and universally closed. If X is quasi-separated over T, then so is Y.

theorem isQuasiSeparated_of_isSurjective_of_universallyClosed
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hT : IsAlgebraicSpace B S hS T) (f : X ⟶ Y) (g : Y ⟶ T)
    (hfsurj : IsSurjective B S hS f) (hfclosed : UniversallyClosed B S hS f)
    (hqs : IsQuasiSeparated B S hS (f ≫ g)) :
    IsQuasiSeparated B S hS g

AlgebraicGeometry.Space.isAbsolutelyQuasiSeparated_of_isSurjective_of_universallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/UniversallyClosed.lean, line 952. The attribute's comment: “part (1): quasi-separated”.

Stacks 05Z2, part (1). Let X ⟶ Y be a surjective universally closed morphism of algebraic spaces over S. If X is quasi-separated, then so is Y.

This is part (3) over the terminal scheme, as the source says: quasi-separatedness of an algebraic space is quasi-separatedness over Spec ℤ of its lower-shriek extension along S ⟶ Spec ℤ, by Stacks 03BS, and that extension of X ⟶ Y is again surjective and universally closed by AlgebraicGeometry.Space.isSurjective_relocalize and AlgebraicGeometry.Space.universallyClosed_relocalize.

theorem isAbsolutelyQuasiSeparated_of_isSurjective_of_universallyClosed
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hfsurj : IsSurjective B S hS f) (hfclosed : UniversallyClosed B S hS f)
    (hqs : IsAbsolutelyQuasiSeparated B S hS hZ X) :
    IsAbsolutelyQuasiSeparated B S hS hZ Y

AlgebraicGeometry.Space.isAbsolutelySeparated_of_isSurjective_of_universallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/UniversallyClosed.lean, line 974. The attribute's comment: “part (2): separated”.

Stacks 05Z2, part (2). Let X ⟶ Y be a surjective universally closed morphism of algebraic spaces over S. If X is separated, then so is Y.

This is part (4) over the terminal scheme, as the source says: separatedness of an algebraic space is separatedness over Spec ℤ of its lower-shriek extension along S ⟶ Spec ℤ, by Stacks 03BS, and that extension of X ⟶ Y is again surjective and universally closed by AlgebraicGeometry.Space.isSurjective_relocalize and AlgebraicGeometry.Space.universallyClosed_relocalize.

theorem isAbsolutelySeparated_of_isSurjective_of_universallyClosed
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hfsurj : IsSurjective B S hS f) (hfclosed : UniversallyClosed B S hS f)
    (hsep : IsAbsolutelySeparated B S hS hZ X) :
    IsAbsolutelySeparated B S hS hZ Y
Sources
LeanAlgebraicGeometry.Space.presheaf_universallyClosed_iff · AlgebraicGeometry.Space.IsClosedMorphism · AlgebraicGeometry.Space.UniversallyClosed · AlgebraicGeometry.Space.universallyClosed_pullback · AlgebraicGeometry.Space.isClosedMorphism_comp · AlgebraicGeometry.Space.universallyClosed_comp · AlgebraicGeometry.Space.universallyClosed_tfae · AlgebraicGeometry.AffineLineTranslation.structureMap

Section67.10 Monomorphisms#

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

Tag 042L, a definition

Tag 042L in the Stacks Project.

Declarations registered for the tag:

Tag 042M, a lemma

Tag 042M in the Stacks Project.

AlgebraicGeometry.Space.mono_hom_iff_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Monomorphisms.lean, line 213. The attribute's comment: “parts (1) and (2)”.

Stacks 042M, parts (1) and (2). A morphism of algebraic spaces over S is a monomorphism of the underlying presheaves exactly when it is a monomorphism of the category of algebraic spaces over S.

theorem mono_hom_iff_mono {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) :
    Mono f.hom ↔ Mono f

AlgebraicGeometry.Space.mono_iff_isIso_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Monomorphisms.lean, line 227. The attribute's comment: “parts (2) and (3)”. References: EGA I (5.3.8).

Stacks 042M, parts (2) and (3). A morphism of algebraic spaces over S is a monomorphism of the category of algebraic spaces over S exactly when its relative diagonal is an isomorphism.

theorem mono_iff_isIso_diagonal {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) :
    Mono f ↔ IsIso (pullback.diagonal f)
Tag 042N, a lemma

Tag 042N in the Stacks Project.

AlgebraicGeometry.Space.isSeparated_of_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparatedQuasiFiniteEtaleDescent.lean, line 218.

Stacks 042N. A monomorphism of presheaves on the big fppf site of S is a separated morphism of algebraic spaces over S: its relative diagonal is an isomorphism, and an isomorphism is a closed immersion. The statement is made for an arbitrary morphism of presheaves on the big fppf site of S; no algebraic-space hypothesis is used.

This strictly generalises AlgebraicGeometry.Space.isSeparated_of_isIso, which is the same statement for an isomorphism.

theorem isSeparated_of_mono {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (m : F ⟶ G) (hm : Mono m) :
    IsSeparated B S hS m

AlgebraicGeometry.Space.isSeparated_of_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeDiagonalMonomorphism.lean, line 148.

Stacks 042N. A monomorphism of algebraic spaces over S is separated: its relative diagonal is an isomorphism, and an isomorphism is a closed immersion.

The statement is made for an arbitrary morphism of presheaves on the big fppf site of S; no algebraic-space hypothesis is used.

theorem isSeparated_of_mono {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (g : F ⟶ G) (hg : Mono g) :
    IsSeparated B S hS g
Tag 042O, a lemma

Tag 042O in the Stacks Project.

Declarations registered for the tag:

Tag 042P, a lemma

Tag 042P in the Stacks Project.

Declarations registered for the tag:

Tag 042Q, a lemma

Tag 042Q in the Stacks Project.

AlgebraicGeometry.Space.mono_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Monomorphisms.lean, line 239.

Stacks 042Q. For a morphism f : X ⟶ Y of algebraic spaces over S the following are equivalent: f is a monomorphism; every base change of f to a scheme of the site is a monomorphism; every base change of f to an affine scheme of the site is a monomorphism; the base change of f along some surjective étale chart of Y is a monomorphism; and the base changes of f along the members of some Zariski covering of Y are monomorphisms.

theorem mono_tfae {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    List.TFAE [
      Mono f,
      (∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ Y), Mono (pullback.snd f g)),
      (∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ Y),
        IsAffine ((BigFppfOver.toScheme B S hS).obj Z) → Mono (pullback.snd f g)),
      (∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
        IsSurjective B S hS g ∧ IsEtale B S hS g ∧ Mono (pullback.snd f g)),
      (∃ (I : Type u) (U : I → Subfunctor Y),
        IsZariskiCover B S hS I U ∧ ∀ i, Mono (pullback.snd f (U i).ι))]
Tag 042R, a lemma

Tag 042R in the Stacks Project.

AlgebraicGeometry.Space.mono_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Monomorphisms.lean, line 306. The attribute's comment: “monomorphism”.

Stacks 042R. An immersion of algebraic spaces over S is a monomorphism: an immersion of schemes is a monomorphism, and a morphism of presheaves all of whose represented base changes are monomorphisms is a monomorphism.

theorem mono_of_isImmersion {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : F ⟶ G}
    (hf : IsImmersion B S hS f) : Mono f

AlgebraicGeometry.Space.isSeparated_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Monomorphisms.lean, line 322. The attribute's comment: “separatedness”. References: EGA I (5.5.1), “(i) immersions”.

Stacks 042R. An immersion of algebraic spaces over S is separated: it is a monomorphism, so its relative diagonal is an isomorphism, and an isomorphism of presheaves is a closed immersion.

theorem isSeparated_of_isImmersion {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : F ⟶ G}
    (hf : IsImmersion B S hS f) : IsSeparated B S hS f
Tag 06MG, a lemma

Tag 06MG in the Stacks Project.

AlgebraicGeometry.Space.isEmpty_points_or_isIso_of_mono_to_spec_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MonoToZeroDimensionalLocalSpectra.lean, line 235.

Stacks 06MG. A monomorphism of algebraic spaces over S whose target is the spectrum of a field k is either a morphism out of an algebraic space with no points, or an isomorphism.

A field is a zero-dimensional local ring, so the source is a scheme by Stacks 06RZ, and the dichotomy is then the scheme-level one.

theorem isEmpty_points_or_isIso_of_mono_to_spec_field
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hF : IsAlgebraicSpace B S hS F) (f : F ⟶ G)
    [Mono f] (Y : BigFppfOver B S hS) (eG : G ≅ yoneda.obj Y) (k : Type u) [Field k]
    (eY : (BigFppfOver.toScheme B S hS).obj Y ≅ Spec (.of k)) :
    IsEmpty (points B S hS F) ∨ IsIso f
Tag 06RV, a lemma

Tag 06RV in the Stacks Project.

AlgebraicGeometry.Space.pointsMap_injective_of_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PointsMono.lean, line 67.

Stacks 06RV. A monomorphism induces an injective map on equivalence classes of field-valued points.

theorem pointsMap_injective_of_mono
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : F ⟶ G) [Mono f] :
    Function.Injective (pointsMap B S hS F f)
Sources
LeanCategoryTheory.Mono · AlgebraicGeometry.Space.mono_hom_iff_mono · AlgebraicGeometry.Space.mono_iff_isIso_diagonal · AlgebraicGeometry.Space.isSeparated_of_mono · CategoryTheory.mono_comp · CategoryTheory.MorphismProperty.IsStableUnderBaseChange.monomorphisms · AlgebraicGeometry.Space.mono_tfae · AlgebraicGeometry.Space.mono_of_isImmersion

Section67.11 Pushforward of quasi-coherent sheaves#

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

Tag 03M8, a lemma

Tag 03M8 in the Stacks Project.

AlgebraicGeometry.Space.exact_moduleChartDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModulePushforwardPresentationExactSequence.lean, line 459.

Stacks 03M8. Let f : X ⟶ Y be a morphism of algebraic spaces over S, let U be a surjective étale scheme chart of X with structure morphism τ, let R = U ×_X U (the cartesian square hR in the spaces-étale site of X) with its two projections t, s : R ⟶ U and structure morphism ρ, and put a = τ ≫ f, b = ρ ≫ f. For every 𝒪_X-module F the sequence

0 → f_*F → a_*(F|_U) → b_*(F|_R)

of 𝒪_Y-modules, whose first arrow is AlgebraicGeometry.Space.moduleChartDirectImageUnitArrow and whose second arrow is the difference t^* - s^* of the two arrows AlgebraicGeometry.Space.moduleChartDirectImageParallelArrow, is exact: the short complex is exact and its first arrow is a monomorphism.

theorem exact_moduleChartDirectImage (hU : IsSurjective B S hS U.1.hom) {t s : R ⟶ U}
    (hR : IsPullback ((comparisonFunctor B S hS X).map t) ((comparisonFunctor B S hS X).map s)
      ((SpacesEtale.isTerminal_idObj B S hS X).from ((comparisonFunctor B S hS X).obj U))
      ((SpacesEtale.isTerminal_idObj B S hS X).from ((comparisonFunctor B S hS X).obj U)))
    (F : Modules.{u, u} B S hS X.1 X.2) :
    (ShortComplex.mk
        (moduleChartDirectImageUnitArrow B S hS f ((comparisonFunctor B S hS X).obj U).2 F)
        (moduleChartDirectImageParallelArrow B S hS f ((comparisonFunctor B S hS X).obj U).2
            (isEtale_chartMap B S hS X t) ((comparisonFunctor B S hS X).obj R).2
            (Over.w ((comparisonFunctor B S hS X).map t).hom) F -
          moduleChartDirectImageParallelArrow B S hS f ((comparisonFunctor B S hS X).obj U).2
            (isEtale_chartMap B S hS X s) ((comparisonFunctor B S hS X).obj R).2
            (Over.w ((comparisonFunctor B S hS X).map s).hom) F)
        (moduleChartDirectImage_comp_sub_eq_zero B S hS f t s F)).Exact ∧
      Mono (moduleChartDirectImageUnitArrow B S hS f ((comparisonFunctor B S hS X).obj U).2 F)
Tag 04CF, an equation

Tag 04CF in the Stacks Project.

AlgebraicGeometry.Space.modulePushforward_comp_overFunctorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModulePushforwardChartRestriction.lean, line 484. The attribute's comment: “for an arbitrary morphism of algebraic spaces, with the restriction to the base-changed chart taken on the slice of the spaces-étale site”.

Stacks 04CF, for an arbitrary morphism of algebraic spaces. Let f : X ⟶ Y be a morphism of algebraic spaces over S and let V be an étale scheme chart of Y. Write U = V ×_Y X for the base change of the chart, an étale algebraic space over X, and f' : U ⟶ V for the base change of f. Then for every 𝒪_X-module F

f'_*(F|_U) = (f_*F)|_V.

The restriction (-)|_V is restriction to the slice of the small étale site of Y at V, the restriction (-)|_U is restriction to the slice of the spaces-étale site of X at U — both readings of Stacks' Equation 03LW — and f'_* is the direct image along the localized base-change functor of Stacks 03CF with the localized structure map AlgebraicGeometry.Space.chartLocalizedStructureSharp of Stacks 04J0, part (1).

No representability hypothesis is made on f; this is the form in which the proof of Stacks 03M9 invokes the identity. It is an isomorphism rather than an equality of functors because AlgebraicGeometry.Space.smallEtaleDirectImage is conjugated by the comparison equivalence of Stacks 03G1; for a representable f an equality is available in the reading of AlgebraicGeometry.Space.overFunctor_comp_smallBaseChangeModulePushforward.

noncomputable def modulePushforward_comp_overFunctorIso (f : X ⟶ Y)
    (V : SmallEtale B S hS Y.1) :
    modulePushforward B S hS f ⋙
        SheafOfModules.overFunctor.{u} (structureRingSheaf B S hS Y) V ≅
      moduleChartBaseChangeRestriction B S hS f V ⋙
        chartLocalizedModulePushforward B S hS f V
Tag 03M9, a lemma

Tag 03M9 in the Stacks Project.

AlgebraicGeometry.Space.isQuasicoherentOnSite_modulePushforward_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionQuasicoherentPushforward.lean, line 110. The attribute's comment: “the direct image along a closed immersion of algebraic spaces”.

Stacks 03M9 along a closed immersion of algebraic spaces. The direct image i_*G of a quasi-coherent 𝒪_Z-module along a closed immersion i : Z ⟶ X is quasi-coherent.

A closed immersion is representable and affine, so its direct image is computed on base-changed charts by AlgebraicGeometry.Space.modulePushforwardChartIso and that one is cartesian on affine charts.

theorem isQuasicoherentOnSite_modulePushforward_of_isClosedImmersion (i : Z ⟶ X)
    (hi : IsClosedImmersion B S hS i.hom) (G : Modules.{u, u} B S hS Z.1 Z.2)
    (hG : G.IsQuasicoherentOnSite) :
    ((modulePushforward B S hS i).obj G).IsQuasicoherentOnSite

AlgebraicGeometry.Space.isQuasicoherentOnSite_modulePushforward_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentPushforwardQcqs.lean, line 202.

Stacks 03M9. Let f : X ⟶ Y be a quasi-compact and quasi-separated morphism of algebraic spaces over S. Then the direct image f_*F of a quasi-coherent 𝒪_X-module F is quasi-coherent.

Quasi-coherence of f_*F is tested on the affine étale charts V of Y, over which f_*F restricts to the direct image along the base change V ×_Y X ⟶ V of the restriction of F (AlgebraicGeometry.Space.pushforward_isQuasicoherentOnSite_of_forall_affine_chart); that base change is quasi-separated with quasi-compact source, and the affine-base case is AlgebraicGeometry.Space.isQuasicoherentOnSite_modulePushforward_of_affine_target.

theorem isQuasicoherentOnSite_modulePushforward_of_qcqs (f : X ⟶ Y)
    (quasiCompact : IsQuasiCompact B S hS f.hom)
    (quasiSeparated : IsQuasiSeparated B S hS f.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) (F_qcoh : F.IsQuasicoherentOnSite) :
    ((modulePushforward B S hS f).obj F).IsQuasicoherentOnSite
Sources
LeanAlgebraicGeometry.Space.exact_moduleChartDirectImage · AlgebraicGeometry.Space.modulePushforward_comp_overFunctorIso · AlgebraicGeometry.Space.isQuasicoherentOnSite_modulePushforward_of_isClosedImmersion · AlgebraicGeometry.Space.isQuasicoherentOnSite_modulePushforward_of_qcqs

Section67.12 Immersions#

Section 67.12 of the Stacks Project, Tag 03HB. 6 tags here are carried by 27 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03M4, a lemma

Tag 03M4 in the Stacks Project.

AlgebraicGeometry.Space.isClosedImmersion_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/ClosedImmersionLocalCriterion.lean, line 78. The attribute's comment: “closed immersions”. References: EGA I (4.2.4), “(b)”.

Stacks 03M4 for closed immersions, unconditionally.

A morphism of algebraic spaces over S is a closed immersion exactly when every one of its base changes to a representable presheaf is, exactly when every one of its base changes to an affine object of the site is, exactly when its base change along one surjective étale scheme chart of the target is, and exactly when its base changes along the members of some Zariski covering of the target are.

This is AlgebraicGeometry.Space.presheaf_tfae at the closed immersions, whose descent hypothesis — Stacks 03I2 for the closed immersions of schemes — is AlgebraicGeometry.Space.isEffectiveDescentAlongSurjectiveEtale_isClosedImmersion.

theorem isClosedImmersion_tfae
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hF : IsAlgebraicSpace B S hS F)
    (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G) :
    List.TFAE [
      IsClosedImmersion B S hS f,
      (∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ G),
        IsClosedImmersion B S hS (pullback.snd f g)),
      (∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ G),
        IsAffine ((BigFppfOver.toScheme B S hS).obj Z) →
          IsClosedImmersion B S hS (pullback.snd f g)),
      (∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ G),
        (MorphismProperty.presheaf (MorphismProperty.inverseImage
          (@Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS))) g ∧
        (MorphismProperty.presheaf (MorphismProperty.inverseImage
          (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS))) g ∧
        IsClosedImmersion B S hS (pullback.snd f g)),
      (∃ (I : Type u) (U : I → Subfunctor G),
        IsZariskiCover B S hS I U ∧
        ∀ i, IsClosedImmersion B S hS (pullback.snd f (U i).ι))
    ]

AlgebraicGeometry.Space.isImmersion_tfae_of_isAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/ImmersionEtaleDescent.lean, line 303. The attribute's comment: “immersions”. References: EGA I (4.2.4), “(a) immersion case”.

A morphism of algebraic spaces over S is an immersion exactly when every one of its base changes to a representable presheaf is, exactly when every one of its base changes to an affine object of the site is, exactly when its base change along one surjective étale scheme chart of the target is, and exactly when its base changes along the members of some Zariski covering of the target are.

This is AlgebraicGeometry.Space.isImmersion_tfae with its hypothesis hdesc supplied by AlgebraicGeometry.Space.isEffectiveDescentAlongSurjectiveEtale_isImmersion.

theorem isImmersion_tfae_of_isAlgebraicSpace
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hF : IsAlgebraicSpace B S hS F)
    (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G) :
    List.TFAE [
      IsImmersion B S hS f,
      (∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ G),
        IsImmersion B S hS (pullback.snd f g)),
      (∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ G),
        IsAffine ((BigFppfOver.toScheme B S hS).obj Z) →
          IsImmersion B S hS (pullback.snd f g)),
      (∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ G),
        (MorphismProperty.presheaf (MorphismProperty.inverseImage
          (@Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS))) g ∧
        (MorphismProperty.presheaf (MorphismProperty.inverseImage
          (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS))) g ∧
        IsImmersion B S hS (pullback.snd f g)),
      (∃ (I : Type u) (U : I → Subfunctor G),
        IsZariskiCover B S hS I U ∧
        ∀ i, IsImmersion B S hS (pullback.snd f (U i).ι))
    ]

AlgebraicGeometry.Space.isOpenImmersion_tfae_of_isAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/OpenImmersionEtaleDescent.lean, line 510. The attribute's comment: “open immersions”.

Stacks 03M4 for open immersions, unconditionally.

A morphism of algebraic spaces over S is an open immersion exactly when every one of its base changes to a representable presheaf is, exactly when every one of its base changes to an affine object of the site is, exactly when its base change along one surjective étale scheme chart of the target is, and exactly when its base changes along the members of some Zariski covering of the target are.

This is AlgebraicGeometry.Space.isOpenImmersion_tfae with its hypothesis hdesc — Stacks 03I2 for open immersions — supplied by AlgebraicGeometry.Space.isEffectiveDescentAlongSurjectiveEtale_isOpenImmersion.

theorem isOpenImmersion_tfae_of_isAlgebraicSpace
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hF : IsAlgebraicSpace B S hS F)
    (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G) :
    List.TFAE [
      IsOpenImmersion B S hS f,
      (∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ G),
        IsOpenImmersion B S hS (pullback.snd f g)),
      (∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ G),
        IsAffine ((BigFppfOver.toScheme B S hS).obj Z) →
          IsOpenImmersion B S hS (pullback.snd f g)),
      (∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ G),
        (MorphismProperty.presheaf (MorphismProperty.inverseImage
          (@Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS))) g ∧
        (MorphismProperty.presheaf (MorphismProperty.inverseImage
          (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS))) g ∧
        IsOpenImmersion B S hS (pullback.snd f g)),
      (∃ (I : Type u) (U : I → Subfunctor G),
        IsZariskiCover B S hS I U ∧
        ∀ i, IsOpenImmersion B S hS (pullback.snd f (U i).ι))
    ]
Tag 0AGC, a lemma

Tag 0AGC in the Stacks Project.

AlgebraicGeometry.Space.isLocallyOfFiniteType_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteTypeProperties.lean, line 206. The attribute's comment: “part (1): locally of finite type”. References: EGA I (6.6.6), “(v)”; EGA IV (1.3.4), “(v)”.

Stacks 0462. If a composite of morphisms of algebraic spaces over S is locally of finite type, then so is its first factor.

This is also the locally-of-finite-type clause of part (1) of Stacks 0AGC, whose other clauses are in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Immersions.lean.

theorem isLocallyOfFiniteType_of_comp
    {F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hF : IsAlgebraicSpace B S hS F) (hG : IsAlgebraicSpace B S hS G)
    (hH : IsAlgebraicSpace B S hS H)
    (f : F ⟶ G) (g : G ⟶ H)
    (hfg : IsLocallyOfFiniteType B S hS (f ≫ g)) :
    IsLocallyOfFiniteType B S hS f

AlgebraicGeometry.Space.relativelyRepresentable_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Immersions.lean, line 270. The attribute's comment: “part (1): representable”.

Stacks 0AGC, part (1): representability. If a composite of morphisms of presheaves on the big fppf site of S is representable and the intermediate presheaf has representable diagonal — in particular, if it is an algebraic space over S — then the first factor is representable.

theorem relativelyRepresentable_of_comp (hY : yoneda.relativelyRepresentable (diag Y))
    (g : Z ⟶ Y) (f : Y ⟶ X) (hgf : yoneda.relativelyRepresentable (g ≫ f)) :
    yoneda.relativelyRepresentable g

AlgebraicGeometry.Space.isSeparated_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Immersions.lean, line 292. The attribute's comment: “part (1): separated”. References: EGA I (5.5.1), “(v)”.

Stacks 0AGC, part (1): separatedness. If a composite of morphisms of algebraic spaces over S is separated, so is its first factor.

This is also the separated part of Stacks 03KR, whose locally separated and quasi-separated parts are AlgebraicGeometry.Space.isLocallySeparated_of_comp and AlgebraicGeometry.Space.isQuasiSeparated_of_comp.

theorem isSeparated_of_comp (g : Z ⟶ Y) (f : Y ⟶ X)
    (hgf : IsSeparated B S hS (g ≫ f)) :
    IsSeparated B S hS g

AlgebraicGeometry.Space.mono_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Immersions.lean, line 316. The attribute's comment: “part (1): monomorphism”.

Stacks 0AGC, part (1): monomorphisms. If a composite of morphisms of algebraic spaces over S is a monomorphism, so is its first factor.

Monomorphy of a morphism of algebraic spaces over S is monomorphy of the underlying morphism of presheaves on the big fppf site of S, by AlgebraicGeometry.Space.mono_hom_iff_mono of StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Monomorphisms.lean, so this clause is the cancellation of monomorphisms CategoryTheory.mono_of_mono read in that presheaf category. Nothing is required of Y.

theorem mono_of_comp (g : Z ⟶ Y) (f : Y ⟶ X) (hgf : Mono (g ≫ f)) : Mono g

AlgebraicGeometry.Space.isImmersion_of_comp_of_isLocallySeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Immersions.lean, line 346. The attribute's comment: “part (2): immersion”.

Stacks 0AGC, part (2). If a composite of morphisms of algebraic spaces over S is an immersion and its second factor is locally separated, then its first factor is an immersion.

theorem isImmersion_of_comp_of_isLocallySeparated (g : Z ⟶ Y) (f : Y ⟶ X)
    (hgf : IsImmersion B S hS (g ≫ f)) (hf : IsLocallySeparated B S hS f) :
    IsImmersion B S hS g

AlgebraicGeometry.Space.isClosedImmersion_of_comp_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Immersions.lean, line 357. The attribute's comment: “part (3): closed immersion”. References: EGA I (5.4.4).

Stacks 0AGC, part (3). If a composite of morphisms of algebraic spaces over S is a closed immersion and its second factor is separated, then its first factor is a closed immersion.

theorem isClosedImmersion_of_comp_of_isSeparated (g : Z ⟶ Y) (f : Y ⟶ X)
    (hgf : IsClosedImmersion B S hS (g ≫ f)) (hf : IsSeparated B S hS f) :
    IsClosedImmersion B S hS g

AlgebraicGeometry.Space.isLocallyQuasiFinite_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/QuasiFinite.lean, line 417. The attribute's comment: “part (1): locally quasi-finite”.

Stacks 03XN. If a composite of morphisms of algebraic spaces over S is locally quasi-finite, then so is its first factor.

Local quasi-finiteness of morphisms of schemes is étale local on the source and target (Stacks 04R3) and is inherited by the first factor of a composite that has it, local finite type by Stacks 01T8 and the fibre condition by AlgebraicGeometry.LocallyQuasiFinite.of_comp, so this is an instance of the cancellation form of Stacks 03MJ.

This is also the locally-quasi-finite clause of part (1) of Stacks 0AGC, whose other clauses are in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Immersions.lean.

theorem isLocallyQuasiFinite_of_comp {F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hF : IsAlgebraicSpace B S hS F) (hG : IsAlgebraicSpace B S hS G)
    (hH : IsAlgebraicSpace B S hS H)
    (f : F ⟶ G) (g : G ⟶ H)
    (hfg : IsLocallyQuasiFinite B S hS (f ≫ g)) :
    IsLocallyQuasiFinite B S hS f
Tag 04CD, a lemma

Tag 04CD in the Stacks Project.

AlgebraicGeometry.Space.isClosedImmersion_iff_isClosed_range_pointsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionPoints.lean, line 167. The attribute's comment: “closed immersion criterion”.

Stacks 04CD. An immersion of algebraic spaces over S is a closed immersion exactly when the image of its point set is a closed subset of the point space of the target.

theorem isClosedImmersion_iff_isClosed_range_pointsMap (hX : IsAlgebraicSpace B S hS X)
    (i : Z ⟶ X) (hi : IsImmersion B S hS i) :
    IsClosedImmersion B S hS i ↔ IsClosed (Set.range (pointsMap B S hS Z i))

Declarations registered for the tag:

Tag 04CE, a remark

Tag 04CE in the Stacks Project.

AlgebraicGeometry.Space.range_pointsMap_ι_boundarySubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Immersions.lean, line 680. The attribute's comment: “the points of the boundary subspace”.

Stacks 04CE. The point set of the boundary subspace of an immersion is the boundary of the image of that immersion.

theorem range_pointsMap_ι_boundarySubspace (hX : IsAlgebraicSpace B S hS X) (i : Z ⟶ X)
    (hi : IsImmersion B S hS i) :
    Set.range (pointsMap B S hS (boundarySubspace B S hS hX i hi).toFunctor
        (boundarySubspace B S hS hX i hi).ι) =
      closure (Set.range (pointsMap B S hS Z i)) \ Set.range (pointsMap B S hS Z i)

AlgebraicGeometry.Space.hasEtaleLocalProperty_isReduced_boundarySubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Immersions.lean, line 690. The attribute's comment: “the boundary subspace is reduced”.

Stacks 04CE. The boundary subspace of an immersion is reduced, in the étale-local sense of Stacks 03E6.

theorem hasEtaleLocalProperty_isReduced_boundarySubspace (hX : IsAlgebraicSpace B S hS X)
    (i : Z ⟶ X) (hi : IsImmersion B S hS i) :
    HasEtaleLocalProperty B S hS (boundarySubspace B S hS hX i hi).toFunctor
      (fun Y : Scheme.{u} => IsReduced Y)

AlgebraicGeometry.Space.range_pointsMap_ι_boundaryComplement_eq_compl, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Immersions.lean, line 699. The attribute's comment: “the open subspace is the complement of the boundary subspace”.

Stacks 04CE. The open subspace through which an immersion is to be factored is the complement of its boundary subspace: the two have complementary point sets.

theorem range_pointsMap_ι_boundaryComplement_eq_compl (hX : IsAlgebraicSpace B S hS X)
    (i : Z ⟶ X) (hi : IsImmersion B S hS i) :
    Set.range (pointsMap B S hS
        (boundaryComplement B S hS X (Set.range (pointsMap B S hS Z i))).toFunctor
        (boundaryComplement B S hS X (Set.range (pointsMap B S hS Z i))).ι) =
      (Set.range (pointsMap B S hS (boundarySubspace B S hS hX i hi).toFunctor
        (boundarySubspace B S hS hX i hi).ι))ᶜ

AlgebraicGeometry.Space.isClosed_range_pointsMap_of_comp_ι_boundaryComplement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Immersions.lean, line 742. The attribute's comment: “the image is closed away from the boundary”.

Stacks 04CE. The image of an immersion is closed in the complement of its boundary: any factorisation of the immersion through that open subspace has closed image on points.

theorem isClosed_range_pointsMap_of_comp_ι_boundaryComplement (i : Z ⟶ X)
    (g : Z ⟶ (boundaryComplement B S hS X (Set.range (pointsMap B S hS Z i))).toFunctor)
    (hg : g ≫ (boundaryComplement B S hS X (Set.range (pointsMap B S hS Z i))).ι = i) :
    IsClosed (Set.range (pointsMap B S hS Z g))

AlgebraicGeometry.Space.exists_isClosedImmersion_comp_ι_boundaryComplement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Immersions.lean, line 753. The attribute's comment: “an immersion is a closed immersion followed by an open immersion”.

Stacks 04CE. Every immersion of algebraic spaces over S factors as a closed immersion into the complement of its boundary, followed by the open immersion of that open subspace into the target.

theorem exists_isClosedImmersion_comp_ι_boundaryComplement
    (hX : IsAlgebraicSpace B S hS X) (hZ : IsAlgebraicSpace B S hS Z) (i : Z ⟶ X)
    (hi : IsImmersion B S hS i) :
    ∃ g : Z ⟶ (boundaryComplement B S hS X (Set.range (pointsMap B S hS Z i))).toFunctor,
      IsClosedImmersion B S hS g ∧
        g ≫ (boundaryComplement B S hS X (Set.range (pointsMap B S hS Z i))).ι = i
Tag 06EC, a remark

Tag 06EC in the Stacks Project.

AlgebraicGeometry.Space.boundaryComplement, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Immersions.lean, line 394. The attribute's comment: “the open subspace U with |U| = |X| ∖ ∂T”.

Stacks 06EC, the open subspace. The open subspace of X obtained by removing the boundary closure T \ T of a set T of points of X: its point set is Mathlib's coborder T.

This is AlgebraicGeometry.Space.openSubspaceOfPoints at coborder T; the definition needs no hypothesis on T, local closedness entering only through AlgebraicGeometry.Space.isOpenSubspace_boundaryComplement.

noncomputable def boundaryComplement (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (T : Set (points B S hS X)) : Subfunctor X

AlgebraicGeometry.Space.range_pointsMap_ι_boundaryComplement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Immersions.lean, line 402. The attribute's comment: “the point set of U is the complement of the boundary of T”.

The point set of the complement of the boundary of T is coborder T, that is, the complement of closure T \ T. This is the defining property |U| = |X| ∖ ∂T of the open subspace U of Stacks 06EC.

theorem range_pointsMap_ι_boundaryComplement (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (T : Set (points B S hS X)) :
    Set.range (pointsMap B S hS (boundaryComplement B S hS X T).toFunctor
      (boundaryComplement B S hS X T).ι) = coborder T

AlgebraicGeometry.Space.isOpenSubspace_boundaryComplement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Immersions.lean, line 412. The attribute's comment: “U is an open subspace of X”.

The complement of the boundary of a locally closed set of points of an algebraic space is an open subspace of it. This is the open subspace U of Stacks 06EC, whose existence the source takes from Stacks 03BZ.

theorem isOpenSubspace_boundaryComplement (hX : IsAlgebraicSpace B S hS X)
    {T : Set (points B S hS X)} (hT : IsLocallyClosed T) :
    IsOpenSubspace B S hS (boundaryComplement B S hS X T)

AlgebraicGeometry.Space.reducedInducedSubspace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Immersions.lean, line 560. The attribute's comment: “the reduced induced subspace Z on a locally closed set of points”.

Stacks 06EC, the reduced induced subspace Z. The reduced induced subspace structure on a locally closed set T of points of an algebraic space X over S: the reduced induced closed subspace of Stacks 03IQ on T, formed inside the open subspace AlgebraicGeometry.Space.boundaryComplement complementary to the boundary of T, where T is closed.

noncomputable def reducedInducedSubspace (hX : IsAlgebraicSpace B S hS X)
    {T : Set (points B S hS X)} (hT : IsLocallyClosed T) :
    Subfunctor (boundaryComplement B S hS X T).toFunctor

AlgebraicGeometry.Space.isClosedSubspace_reducedInducedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Immersions.lean, line 573. The attribute's comment: “Z is a closed subspace of U, so Z ⟶ U is a closed immersion”.

Stacks 06EC. The reduced induced subspace on T is a closed subspace of the open subspace complementary to the boundary of T, so Z ⟶ U is a closed immersion.

theorem isClosedSubspace_reducedInducedSubspace (hX : IsAlgebraicSpace B S hS X)
    {T : Set (points B S hS X)} (hT : IsLocallyClosed T) :
    IsClosedSubspace B S hS (reducedInducedSubspace B S hS hX hT)

AlgebraicGeometry.Space.hasEtaleLocalProperty_isReduced_reducedInducedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Immersions.lean, line 581. The attribute's comment: “Z is a reduced algebraic space”.

Stacks 06EC. The reduced induced subspace on T is reduced, in the étale-local sense of Stacks 03E6.

theorem hasEtaleLocalProperty_isReduced_reducedInducedSubspace
    (hX : IsAlgebraicSpace B S hS X) {T : Set (points B S hS X)} (hT : IsLocallyClosed T) :
    HasEtaleLocalProperty B S hS (reducedInducedSubspace B S hS hX hT).toFunctor
      (fun Y : Scheme.{u} => IsReduced Y)

AlgebraicGeometry.Space.range_pointsMap_comp_ι_reducedInducedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Immersions.lean, line 600. The attribute's comment: “|Z| = T as subsets of |X|”.

Stacks 06EC. The point set of the reduced induced subspace on T is T itself, as a subset of the points of X.

theorem range_pointsMap_comp_ι_reducedInducedSubspace (hX : IsAlgebraicSpace B S hS X)
    {T : Set (points B S hS X)} (hT : IsLocallyClosed T) :
    Set.range (pointsMap B S hS (reducedInducedSubspace B S hS hX hT).toFunctor
      ((reducedInducedSubspace B S hS hX hT).ι ≫ (boundaryComplement B S hS X T).ι)) = T

AlgebraicGeometry.Space.isImmersion_comp_ι_reducedInducedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Immersions.lean, line 612. The attribute's comment: “Z ⟶ U ⟶ X is an immersion”.

Stacks 06EC. The composite Z ⟶ U ⟶ X of the reduced induced subspace on T with the open subspace complementary to the boundary of T is an immersion: a closed immersion followed by an open immersion, by Stacks 02YV.

theorem isImmersion_comp_ι_reducedInducedSubspace (hX : IsAlgebraicSpace B S hS X)
    {T : Set (points B S hS X)} (hT : IsLocallyClosed T) :
    IsImmersion B S hS ((reducedInducedSubspace B S hS hX hT).ι ≫
      (boundaryComplement B S hS X T).ι)

AlgebraicGeometry.Space.eq_reducedInducedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Immersions.lean, line 625. The attribute's comment: “uniqueness of the reduced induced subspace”.

Stacks 06EC, uniqueness. A reduced closed subspace of the open subspace complementary to the boundary of T whose point set in |X| is T is the reduced induced subspace on T.

theorem eq_reducedInducedSubspace (hX : IsAlgebraicSpace B S hS X)
    {T : Set (points B S hS X)} (hT : IsLocallyClosed T)
    (W : Subfunctor (boundaryComplement B S hS X T).toFunctor)
    (hWc : IsClosedSubspace B S hS W)
    (hWT : Set.range (pointsMap B S hS W.toFunctor
      (W.ι ≫ (boundaryComplement B S hS X T).ι)) = T)
    (hWr : HasEtaleLocalProperty B S hS W.toFunctor (fun Y : Scheme.{u} => IsReduced Y)) :
    W = reducedInducedSubspace B S hS hX hT

AlgebraicGeometry.Space.existsUnique_reducedInducedSubspace_of_isLocallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Immersions.lean, line 646. The attribute's comment: “existence and uniqueness of the reduced induced subspace”.

Stacks 06EC. A locally closed set T of points of an algebraic space X over S carries a unique reduced closed subspace structure inside the open subspace complementary to its boundary, and that subspace is an immersion into X with point set T. This is the reduced induced subspace structure on T, and it is AlgebraicGeometry.Space.reducedInducedSubspace.

theorem existsUnique_reducedInducedSubspace_of_isLocallyClosed
    (hX : IsAlgebraicSpace B S hS X) {T : Set (points B S hS X)} (hT : IsLocallyClosed T) :
    ∃! W : Subfunctor (boundaryComplement B S hS X T).toFunctor,
      IsClosedSubspace B S hS W ∧
        HasEtaleLocalProperty B S hS W.toFunctor (fun Y : Scheme.{u} => IsReduced Y) ∧
          Set.range (pointsMap B S hS W.toFunctor
            (W.ι ≫ (boundaryComplement B S hS X T).ι)) = T ∧
            IsImmersion B S hS (W.ι ≫ (boundaryComplement B S hS X T).ι)
Tag 081U, a lemma

Tag 081U in the Stacks Project.

AlgebraicGeometry.Space.exists_isOpenImmersion_isClosedImmersion_comp_eq_of_isQuasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/QuasiCompactImmersionFactorization.lean, line 457.

Stacks 081U. An immersion of algebraic spaces over S which is quasi-compact factors as an open immersion followed by a closed immersion.

The intermediate algebraic space is the scheme-theoretic image of the morphism: it is a closed subspace of the target by Stacks 082X, and the morphism onto it is an open immersion by the quasi-compact case of Stacks 088G.

theorem exists_isOpenImmersion_isClosedImmersion_comp_eq_of_isQuasiCompact
    (hX : IsAlgebraicSpace B S hS X) (f : Z ⟶ X) (hf : IsImmersion B S hS f)
    (hq : IsQuasiCompact B S hS f) :
    ∃ (W : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (j : Z ⟶ W) (i : W ⟶ X),
      IsAlgebraicSpace B S hS W ∧ IsOpenImmersion B S hS j ∧
        IsClosedImmersion B S hS i ∧ j ≫ i = f
Sources
LeanAlgebraicGeometry.Space.isClosedImmersion_tfae · AlgebraicGeometry.Space.isImmersion_tfae_of_isAlgebraicSpace · AlgebraicGeometry.Space.isOpenImmersion_tfae_of_isAlgebraicSpace · AlgebraicGeometry.Space.isLocallyOfFiniteType_of_comp · AlgebraicGeometry.Space.relativelyRepresentable_of_comp · AlgebraicGeometry.Space.isSeparated_of_comp · AlgebraicGeometry.Space.mono_of_comp · AlgebraicGeometry.Space.isImmersion_of_comp_of_isLocallySeparated

Section67.13 Closed immersions#

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

Tag 03MB, a lemma

Tag 03MB in the Stacks Project.

AlgebraicGeometry.Space.closedImmersion_quasicoherentIdeal_correspondence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionIdealCorrespondence.lean, line 214.

Stacks 03MB. Let X be an algebraic space over S.

  1. For every closed immersion i : Z ⟶ X of algebraic spaces the direct image i_*𝒪_Z is a quasi-coherent 𝒪_X-module, the map i♯ : 𝒪_X ⟶ i_*𝒪_Z is surjective — locally surjective as a map of sheaves of rings, and an epimorphism of 𝒪_X-modules — and its kernel is a quasi-coherent sheaf of ideals.
  2. The rule Z ↦ 𝓘_Z = Ker(𝒪_X ⟶ i_*𝒪_Z), with i the inclusion of Z, is an inclusion-reversing bijection from the closed subspaces of X onto the quasi-coherent sheaves of ideals of 𝒪_X.
  3. If Z corresponds to 𝓘 = 𝓘_Z, a morphism h : Y ⟶ X of algebraic spaces factors through Z if and only if the map h^*𝓘 ⟶ h^*𝒪_X = 𝒪_Y is zero.
theorem closedImmersion_quasicoherentIdeal_correspondence :
    (∀ {Z : AlgebraicSpaces B S hS} (i : Z ⟶ X), IsClosedImmersion B S hS i.hom →
      (structureSheafPushforward B S hS i).IsQuasicoherentOnSite ∧
        Sheaf.IsLocallySurjective (structureSharp B S hS i) ∧
        Epi (pushforwardStructureProjection B S hS i) ∧
        (SheafOfModules.Submodule.ker
          (pushforwardStructureProjection B S hS i)).toSheafOfModules.IsQuasicoherentOnSite) ∧
    (∀ Z : ClosedSubspaces B S hS X.1,
      definingIdealSheaf B S hS X Z = SheafOfModules.Submodule.ker
        (pushforwardStructureProjection B S hS (ObjectProperty.homMk Z.1.ι :
          (⟨Z.1.toFunctor, Z.2.1⟩ : AlgebraicSpaces B S hS) ⟶ X))) ∧
    Set.BijOn (definingIdealSheaf B S hS X) Set.univ
      {I | I.toSheafOfModules.IsQuasicoherentOnSite} ∧
    (∀ Z W : ClosedSubspaces B S hS X.1,
      Z ≤ W ↔ definingIdealSheaf B S hS X W ≤ definingIdealSheaf B S hS X Z) ∧
    ∀ (Z : ClosedSubspaces B S hS X.1) {Y : AlgebraicSpaces B S hS} (h : Y ⟶ X),
      (∃ g : Y ⟶ (⟨Z.1.toFunctor, Z.2.1⟩ : AlgebraicSpaces B S hS),
          g ≫ ObjectProperty.homMk Z.1.ι = h) ↔
        (modulePullback B S hS h).map (definingIdealSheaf B S hS X Z).ι ≫
          (modulePullbackUnitIso B S hS h).hom = 0
Tag 083Q, a definition

Tag 083Q in the Stacks Project.

AlgebraicGeometry.Space.isPullback_gysinBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/GysinCompatibility.lean, line 201. The attribute's comment: “the square of Remark 0ER3 is cartesian”.

Remark 0ER3. The square of Remark 0ER3 is cartesian: D' is the fibre product D ×_X X', by Stacks 083Q.

theorem isPullback_gysinBaseChange :
    IsPullback (gysinBaseChangeHom D p hp p' hp' f E)
      (gysinBaseChangeSubspace D p hp p' hp' f E).1.ι E.1.ι f

CategoryTheory.Subfunctor.isPullback_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SubspacePreimage.lean, line 67. The attribute's comment: “fibre-product characterization”.

Stacks 083Q. The inverse image of a subfunctor along a morphism of presheaves is canonically the fibre product of that subfunctor with the source of the morphism.

theorem isPullback_preimage {C : Type*} [Category C] {X Y : C ⥤ Type u}
    (f : Y ⟶ X) (Z : Subfunctor X) :
    IsPullback (Z.fromPreimage f) (Z.preimage f).ι Z.ι f

AlgebraicGeometry.Space.isClosedSubspace_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SubspacePreimage.lean, line 147. The attribute's comment: “closedness of inverse image”.

Stacks 083Q. The inverse image of a closed subspace of an algebraic space along a morphism of algebraic spaces over S is a closed subspace of the source.

theorem isClosedSubspace_preimage
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : Y ⟶ X) (Z : Subfunctor X)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsClosedSubspace B S hS Z) :
    IsClosedSubspace B S hS (Z.preimage f)

Declarations registered for the tag:

Tag 04CG, a lemma

Tag 04CG in the Stacks Project.

AlgebraicGeometry.Space.isQuasiCompact_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionQC.lean, line 94.

A closed immersion of algebraic spaces over S is quasi-compact.

theorem isQuasiCompact_of_isClosedImmersion {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : F ⟶ G)
    (_hF : IsAlgebraicSpace B S hS F) (_hG : IsAlgebraicSpace B S hS G)
    (hf : IsClosedImmersion B S hS f) :
    IsQuasiCompact B S hS f
Tag 04CH, a lemma

Tag 04CH in the Stacks Project.

AlgebraicGeometry.Space.isSeparated_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperClosedImmersion.lean, line 123.

Stacks 04CH. A closed immersion of algebraic spaces over S is separated. Its relative diagonal is an isomorphism, because the morphism is a monomorphism, and an isomorphism of presheaves is a closed immersion.

theorem isSeparated_of_isClosedImmersion (f : X ⟶ Y) (hf : IsClosedImmersion B S hS f) :
    IsSeparated B S hS f
Tag 04E5, a lemma

Tag 04E5 in the Stacks Project.

AlgebraicGeometry.Space.fullyFaithfulSmallEtalePushforwardOfIsClosedImmersion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionChartBaseChangeDense.lean, line 287. The attribute's comment: “part (1): full faithfulness on sheaves of sets”. References: SGA 4 VIII (6.3), “fully faithful”.

Stacks 04E5, part (1). For a closed immersion f : X ⟶ Y of algebraic spaces over S, the direct image of sheaves of sets along the morphism of small étale topoi of Stacks 03G2, part (3) is fully faithful.

noncomputable def fullyFaithfulSmallEtalePushforwardOfIsClosedImmersion (f : X ⟶ Y)
    (hf : IsClosedImmersion B S hS f.hom) :
    (smallToposMorphismTypeU B S hS f).pushforward.FullyFaithful

AlgebraicGeometry.Space.smallEtalePullbackPushforwardCounitIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionChartBaseChangeDense.lean, line 299. The attribute's comment: “part (1): inverse image is a left inverse”. References: SGA 4 VIII (5.7), “partial”.

Stacks 04E5, part (1). For a closed immersion f : X ⟶ Y of algebraic spaces over S the inverse image of sheaves of sets is a left inverse of the direct image: the counit f^{-1}f_*G ⟶ G of the adjunction of the morphism of small étale topoi of Stacks 03G2, part (3) is an isomorphism for every sheaf G on the small étale site of X.

noncomputable def smallEtalePullbackPushforwardCounitIso (f : X ⟶ Y)
    (hf : IsClosedImmersion B S hS f.hom) :
    (smallToposMorphismTypeU B S hS f).pushforward ⋙
        (smallToposMorphismTypeU B S hS f).inverseImage ≅
      𝟭 (Sheaf (SmallEtale.topology B S hS X.1) (Type u))

AlgebraicGeometry.Space.fullyFaithfulSmallEtaleAbelianPushforwardOfIsClosedImmersion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionChartBaseChangeDense.lean, line 313. The attribute's comment: “part (2): full faithfulness on abelian sheaves”.

Stacks 04E5, part (2), full faithfulness. For a closed immersion f : X ⟶ Y of algebraic spaces over S, the direct image of sheaves of abelian groups along f — restriction along the chart base-change morphism of small étale sites of Stacks 03G2, part (4) — is fully faithful.

noncomputable def fullyFaithfulSmallEtaleAbelianPushforwardOfIsClosedImmersion (f : X ⟶ Y)
    (hf : IsClosedImmersion B S hS f.hom) :
    letI := (smallBaseChange_isMorphismOfSites B S hS f hf.rep).toIsContinuous
    ((smallBaseChange B S hS f hf.rep).sheafPushforwardContinuous AddCommGrpCat.{w}
      (SmallEtale.topology B S hS Y.1) (SmallEtale.topology B S hS X.1)).FullyFaithful

AlgebraicGeometry.Space.smallEtaleAbelianPullbackPushforwardCounitIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionChartBaseChangeDense.lean, line 328. The attribute's comment: “part (2): inverse image is a left inverse”. References: SGA 4 VIII (5.7), “partial”.

Stacks 04E5, part (2). For a closed immersion f : X ⟶ Y of algebraic spaces over S the inverse image of sheaves of abelian groups is a left inverse of the direct image: the counit of the adjunction of CategoryTheory.Functor.sheafAdjunctionContinuous for chart base change is a natural isomorphism f_* ⋙ f^{-1} ≅ 𝟭. The abelian groups are taken at the universe u + 1, at which the small étale site has sheafification.

noncomputable def smallEtaleAbelianPullbackPushforwardCounitIso (f : X ⟶ Y)
    (hf : IsClosedImmersion B S hS f.hom) :
    letI := (smallBaseChange_isMorphismOfSites B S hS f hf.rep).toIsContinuous
    letI : ((smallBaseChange B S hS f hf.rep).sheafPushforwardContinuous AddCommGrpCat.{u + 1}
      (SmallEtale.topology B S hS Y.1) (SmallEtale.topology B S hS X.1)).IsRightAdjoint :=
      (Functor.sheafPullbackConstruction.sheafAdjunctionContinuous _ _ _ _).isRightAdjoint
    (smallBaseChange B S hS f hf.rep).sheafPushforwardContinuous AddCommGrpCat.{u + 1}
        (SmallEtale.topology B S hS Y.1) (SmallEtale.topology B S hS X.1) ⋙
      (smallBaseChange B S hS f hf.rep).sheafPullback AddCommGrpCat.{u + 1}
        (SmallEtale.topology B S hS Y.1) (SmallEtale.topology B S hS X.1) ≅
      𝟭 (Sheaf (SmallEtale.topology B S hS X.1) AddCommGrpCat.{u + 1})

AlgebraicGeometry.Space.smallBaseChange_isCoverDense_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionChartCoverDensity.lean, line 258. The attribute's comment: “part (1): cover density of chart base change”.

Stacks 04E5, part (1). Let i : Z ⟶ X be a closed immersion of algebraic spaces over a scheme S. Base change along i of étale scheme charts of X is cover dense for the small étale topology of Z: every étale chart of Z is covered by base changes along i of étale charts of X.

theorem smallBaseChange_isCoverDense_of_isClosedImmersion
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {Z X : AlgebraicSpaces B S hS} (i : Z ⟶ X)
    (hi : IsClosedImmersion B S hS i.hom) :
    (smallBaseChange B S hS i hi.rep).IsCoverDense (SmallEtale.topology B S hS Z.1)

AlgebraicGeometry.Space.smallBaseChange_isLocallyFull_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionChartLocalFullness.lean, line 366. The attribute's comment: “part (1), local fullness of base change on scheme charts”.

Stacks 04E5, part (1), local fullness. For a closed immersion i : Z ⟶ X of algebraic spaces over a scheme S, base change along i of étale scheme charts is a locally full functor from the small étale site of X to the small étale site of Z: a morphism over Z between the base changes of two étale charts of X is, locally on the source, the base change of a morphism of charts of X.

No covering family has to be produced: the chart of AlgebraicGeometry.Space.exists_isIso_smallBaseChange_map_of_isClosedImmersion already has invertible base change, so the sieve it generates is the whole sieve.

theorem smallBaseChange_isLocallyFull_of_isClosedImmersion
    {Z X : AlgebraicSpaces B S hS} (i : Z ⟶ X)
    (hi : IsClosedImmersion B S hS i.hom) :
    (smallBaseChange B S hS i hi.rep).IsLocallyFull (SmallEtale.topology B S hS Z.1)

AlgebraicGeometry.Space.smallEtalePushforward_essImage_iff_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionSetSheafEssentialImage.lean, line 224. The attribute's comment: “part (1): the essential image”.

Stacks 04E5, part (1), the essential image. For a closed immersion i : Z ⟶ X of algebraic spaces over S, a sheaf of sets on the small étale site of X lies in the essential image of the direct image along i exactly when it has exactly one section over every étale chart of X whose points avoid the point set of Z, that is exactly when its restriction to X ∖ Z is a singleton.

The forward direction is Étale Cohomology 04FX away from Z, AlgebraicGeometry.Space.nonempty_isTerminal_smallEtaleDirectImage_obj_of_chartPreimage_eq_empty. The converse is Étale Cohomology 04CA: the unit of the adjunction is invertible on the fibre at every geometric point of X, on the point set of Z by the triangle identity and Stacks 04K2, part (4), and off it because both fibres are singletons; the geometric points are a conservative family, and the unit of a fully faithful right adjoint is invertible exactly on its essential image.

theorem smallEtalePushforward_essImage_iff_of_isClosedImmersion (i : Z ⟶ X)
    (hi : IsClosedImmersion B S hS i.hom)
    (F : Sheaf (SmallEtale.topology B S hS X.1) (Type u)) :
    (smallToposMorphismTypeU B S hS i).pushforward.essImage F ↔
      ∀ V : SmallEtale B S hS X.1, chartPreimage B S hS i V = ∅ →
        Nonempty (IsTerminal (F.obj.obj (op V)))

AlgebraicGeometry.Space.smallEtalePushforward_essImage_iff_abelian_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ComplexesWithSupport.lean, line 633. The attribute's comment: “part (2): the essential image”.

Stacks 04E5, part (2), the essential image. For a closed immersion i : Z ⟶ X of algebraic spaces over S, an abelian sheaf on the small étale site of X lies in the essential image of the direct image along i exactly when its support is contained in the point set of Z.

Both directions are now unconditional: the forward one is AlgebraicGeometry.Space.supportOfSheaf_subset_of_essImage, resting on Étale Cohomology 04FX for algebraic spaces, and the converse is AlgebraicGeometry.Space.isIso_unit_app_of_supportOfSheaf_subset, Étale Cohomology 04CA for algebraic spaces, together with the characterization of the essential image of a fully faithful right adjoint by invertibility of the unit.

theorem smallEtalePushforward_essImage_iff_abelian_of_isClosedImmersion (i : Z ⟶ X)
    (hi : IsClosedImmersion B S hS i.hom)
    (F : Sheaf (SmallEtale.topology B S hS X.1) AddCommGrpCat.{u + 1}) :
    (smallEtaleAbelianPushforward.{u + 1} B S hS i hi.rep).essImage F ↔
      supportOfSheaf B S hS X.1 F ⊆ Set.range (pointsMap B S hS Z.1 i.hom)
Tag 0DK1, a lemma

Tag 0DK1 in the Stacks Project.

AlgebraicGeometry.Space.stalkPushforwardIsoOfIsClosedImmersion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionStalkPushforward.lean, line 114.

Stacks 0DK1. Let i : Z ⟶ X be a closed immersion of algebraic spaces over a scheme S and let z be a geometric point of Z with image x in X. Then (i_*F)_x = F_z for every sheaf of sets F on the small étale site of Z, naturally in F.

def stalkPushforwardIsoOfIsClosedImmersion (hci : IsClosedImmersion B S hS i.hom)
    (z : GeometricPoint B S hS Z.1) :
    (smallToposMorphism B S hS i).pushforward ⋙
        sheafToPresheaf (SmallEtale.topology B S hS X.1) (Type (u + 1)) ⋙
          stalkSetFunctor (geometricPointMap i.hom z) ≅
      sheafToPresheaf (SmallEtale.topology B S hS Z.1) (Type (u + 1)) ⋙
        stalkSetFunctor z
Tag 04G0, a lemma

Tag 04G0 in the Stacks Project.

AlgebraicGeometry.Space.smallEtaleRingedToposHomOfSharp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionModuleTensorPushforward.lean, line 181. The attribute's comment: “the morphism of ringed topoi determined by i, 𝒜, ℬ and φ”.

The morphism of ringed topoi of Stacks 04G0, f : (Sh(Z_étale), ℬ) ⟶ (Sh(X_étale), 𝒜): its underlying morphism of topoi is that of Stacks 03G2, part (3), and its structure map is φ.

No hypothesis on i enters, so this is equally the morphism of ringed topoi of Stacks 0DK4, whose datum is the same (i, φ) in the same direction, with i finite instead of a closed immersion.

noncomputable def smallEtaleRingedToposHomOfSharp (i : Z ⟶ X)
    {𝒜 : Sheaf (SmallEtale.topology B S hS X.1) CommRingCat.{u}}
    {ℬ : Sheaf (SmallEtale.topology B S hS Z.1) CommRingCat.{u}}
    (φ : 𝒜 ⟶ (pushforwardCommRingFunctor.{u, u, u, u + 1, u, u + 1}
      (smallToposMorphismTypeU B S hS i)).obj ℬ) :
    Stacks.Sheaves.RingedToposModules.RingedToposHom
      (smallEtaleRingedToposOfRings B S hS Z ℬ) (smallEtaleRingedToposOfRings B S hS X 𝒜)

AlgebraicGeometry.Space.tensorPushforwardMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionModuleTensorPushforward.lean, line 201. The attribute's comment: “the canonical map 𝓕 ⊗_𝒜 f_*𝓖 ⟶ f_*(f^*𝓕 ⊗_ℬ 𝓖)”.

The canonical map of Stacks 04G0, 𝓕 ⊗_𝒜 f_*𝓖 ⟶ f_*(f^*𝓕 ⊗_ℬ 𝓖): the adjoint transpose of f^*(𝓕 ⊗_𝒜 f_*𝓖) = f^*𝓕 ⊗_ℬ f^*f_*𝓖 ⟶ f^*𝓕 ⊗_ℬ 𝓖, built from the identity of f^*𝓕 and the adjunction map f^*f_*𝓖 ⟶ 𝓖.

No hypothesis on i enters, so this is equally the canonical map of Stacks 0DK4, which is the adjoint transpose of the same comparison for the same datum with i finite.

noncomputable def tensorPushforwardMap (i : Z ⟶ X)
    {𝒜 : Sheaf (SmallEtale.topology B S hS X.1) CommRingCat.{u}}
    {ℬ : Sheaf (SmallEtale.topology B S hS Z.1) CommRingCat.{u}}
    (φ : 𝒜 ⟶ (pushforwardCommRingFunctor.{u, u, u, u + 1, u, u + 1}
      (smallToposMorphismTypeU B S hS i)).obj ℬ)
    (𝓕 : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedToposOfRings B S hS X 𝒜).O))
    (𝓖 : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedToposOfRings B S hS Z ℬ).O)) :
    ((Stacks.SheafOfModules.Tensor.sheafTensor.{u + 1, u, u, u, u} 𝒜).obj 𝓕).obj
      ((pushforwardModules (smallEtaleRingedToposHomOfSharp B S hS i φ)).obj 𝓖) ⟶
      (pushforwardModules (smallEtaleRingedToposHomOfSharp B S hS i φ)).obj
        (((Stacks.SheafOfModules.Tensor.sheafTensor.{u + 1, u, u, u, u} ℬ).obj
          (((smallEtaleRingedToposHomOfSharp B S hS i φ).pullbackModules).obj 𝓕)).obj 𝓖)

AlgebraicGeometry.Space.isIso_tensorPushforwardMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionModuleTensorPushforward.lean, line 219. The attribute's comment: “invertibility, given the counit at 𝓖 and the unit at 𝓕 ⊗_𝒜 f_*𝓖”.

Stacks 04G0, the invertibility clause, reduced to the adjunction of Stacks 03D7: the canonical map is an isomorphism once the counit of f^* ⊣ f_* is invertible at 𝓖 and its unit is invertible at 𝓕 ⊗_𝒜 f_*𝓖.

theorem isIso_tensorPushforwardMap (i : Z ⟶ X)
    {𝒜 : Sheaf (SmallEtale.topology B S hS X.1) CommRingCat.{u}}
    {ℬ : Sheaf (SmallEtale.topology B S hS Z.1) CommRingCat.{u}}
    (φ : 𝒜 ⟶ (pushforwardCommRingFunctor.{u, u, u, u + 1, u, u + 1}
      (smallToposMorphismTypeU B S hS i)).obj ℬ)
    (𝓕 : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedToposOfRings B S hS X 𝒜).O))
    (𝓖 : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedToposOfRings B S hS Z ℬ).O))
    (hε : IsIso ((pullbackAdjPushforwardModules
      (smallEtaleRingedToposHomOfSharp B S hS i φ)).counit.app 𝓖))
    (hη : IsIso ((pullbackAdjPushforwardModules
        (smallEtaleRingedToposHomOfSharp B S hS i φ)).unit.app
      (((Stacks.SheafOfModules.Tensor.sheafTensor.{u + 1, u, u, u, u} 𝒜).obj 𝓕).obj
        ((pushforwardModules (smallEtaleRingedToposHomOfSharp B S hS i φ)).obj 𝓖)))) :
    IsIso (tensorPushforwardMap B S hS i φ 𝓕 𝓖)

AlgebraicGeometry.Space.isIso_tensorPushforwardMap_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionTensorPushforwardIso.lean, line 127.

Stacks 04G0. Let i : Z ⟶ X be a closed immersion of algebraic spaces over S, let 𝒜 be a sheaf of rings on X_étale, ℬ a sheaf of rings on Z_étale and φ : 𝒜 ⟶ i_{small,*}ℬ a homomorphism of sheaves of rings, giving a morphism of ringed topoi f : (Sh(Z_étale), ℬ) ⟶ (Sh(X_étale), 𝒜). Then for every sheaf of 𝒜-modules 𝓕 and every sheaf of ℬ-modules 𝓖 the canonical map

𝓕 ⊗_𝒜 f_*𝓖 ⟶ f_*(f^*𝓕 ⊗_ℬ 𝓖)

is an isomorphism.

The canonical map is split into its inverse-image factor and its change-of-rings factor; the second is always invertible and the first is invertible because the inverse-image adjunction of a closed immersion has an invertible counit and a unit that is invertible at a tensor product with a direct image.

theorem isIso_tensorPushforwardMap_of_isClosedImmersion (i : Z ⟶ X)
    (hi : IsClosedImmersion B S hS i.hom)
    {𝒜 : Sheaf (SmallEtale.topology B S hS X.1) CommRingCat.{u}}
    {ℬ : Sheaf (SmallEtale.topology B S hS Z.1) CommRingCat.{u}}
    (φ : 𝒜 ⟶ (pushforwardCommRingFunctor.{u, u, u, u + 1, u, u + 1}
      (smallToposMorphismTypeU B S hS i)).obj ℬ)
    (𝓕 : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedToposOfRings B S hS X 𝒜).O))
    (𝓖 : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedToposOfRings B S hS Z ℬ).O)) :
    IsIso (tensorPushforwardMap B S hS i φ 𝓕 𝓖)
Sources
LeanAlgebraicGeometry.Space.closedImmersion_quasicoherentIdeal_correspondence · AlgebraicGeometry.Space.isPullback_gysinBaseChange · CategoryTheory.Subfunctor.isPullback_preimage · AlgebraicGeometry.Space.isClosedSubspace_preimage · CategoryTheory.Subfunctor.preimage · AlgebraicGeometry.Space.isQuasiCompact_of_isClosedImmersion · AlgebraicGeometry.Space.isSeparated_of_isClosedImmersion · AlgebraicGeometry.Space.fullyFaithfulSmallEtalePushforwardOfIsClosedImmersion

Section67.14 Closed immersions and quasi-coherent sheaves#

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

Tag 04CJ, a lemma

Tag 04CJ in the Stacks Project.

AlgebraicGeometry.Space.kerIdealSmulQuotientUnitIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionIdealQuotient.lean, line 253. The attribute's comment: “part (1): the unit identifies the quotient by the defining ideal with the direct image of the inverse image”.

Stacks 04CJ, part (1). Let i : Z ⟶ X be a closed immersion of algebraic spaces over S and let 𝓘 = ker(i♯) ⊆ 𝒪_X be the ideal cutting out Z. For every 𝒪_X-module 𝓕 the unit 𝓕 ⟶ i_*i^*𝓕 of the adjunction of Stacks 03LU induces an isomorphism 𝓕/𝓘𝓕 ≅ i_*i^*𝓕.

The isomorphism is the one the adjunction gives: cokernel.π ≫ e.hom is the unit, by AlgebraicGeometry.Space.cokernel_π_comp_kerIdealSmulQuotientUnitMap.

def kerIdealSmulQuotientUnitIso (i : Z ⟶ X) (hi : IsClosedImmersion B S hS i.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) :
    kerIdealSmulQuotient B S hS i F ≅
      (modulePushforward B S hS i).obj ((modulePullback B S hS i).obj F)

AlgebraicGeometry.Space.cokernel_π_comp_kerIdealSmulQuotientUnitIso_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionIdealQuotient.lean, line 264. The attribute's comment: “part (1): the isomorphism is the one induced by the unit of the adjunction”.

Stacks 04CJ, part (1), the normalisation of the isomorphism: it is induced by the unit of the adjunction of Stacks 03LU, that is, composing the projection 𝓕 ⟶ 𝓕/𝓘𝓕 with it gives the unit.

theorem cokernel_π_comp_kerIdealSmulQuotientUnitIso_hom (i : Z ⟶ X)
    (hi : IsClosedImmersion B S hS i.hom) (F : Modules.{u, u} B S hS X.1 X.2) :
    cokernel.π (kerIdealSmul B S hS i F).ι ≫
        (kerIdealSmulQuotientUnitIso B S hS i hi F).hom =
      (modulePullbackAdjunction B S hS i).unit.app F

AlgebraicGeometry.Space.isIso_modulePullbackAdjunction_counit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionModulePushforward.lean, line 206. The attribute's comment: “part (2): inverse image is a left inverse of direct image”.

Stacks 04CJ, part (2) for the modules of AlgebraicGeometry.Space.Modules: for a closed immersion f : X ⟶ Y of algebraic spaces and any sheaf of 𝒪_X-modules G, the adjunction map f^*f_*G ⟶ G is an isomorphism.

This is full faithfulness of the direct image read through the adjunction of Stacks 03LU: the counit of an adjunction is an isomorphism exactly when its right adjoint is fully faithful.

theorem isIso_modulePullbackAdjunction_counit (f : X ⟶ Y) (hf : IsClosedImmersion B S hS f.hom)
    (G : Modules.{u, u} B S hS X.1 X.2) :
    IsIso ((modulePullbackAdjunction B S hS f).counit.app G)

AlgebraicGeometry.Space.modulePullbackCounitIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionModulePushforward.lean, line 218. The attribute's comment: “part (2): inverse image is a left inverse of direct image”.

Stacks 04CJ, part (2), functorially: inverse image along a closed immersion of algebraic spaces is a left inverse of direct image, the counit of the adjunction of Stacks 03LU being a natural isomorphism f_* ⋙ f^* ≅ 𝟭. This is the functorial form of AlgebraicGeometry.Space.isIso_modulePullbackAdjunction_counit.

def modulePullbackCounitIso (f : X ⟶ Y) (hf : IsClosedImmersion B S hS f.hom) :
    modulePushforward B S hS f ⋙ modulePullback B S hS f ≅
      𝟭 (Modules.{u, u} B S hS X.1 X.2)

AlgebraicGeometry.Space.annihilatedByKerIdeal_modulePushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionModulePushforward.lean, line 269. The attribute's comment: “part (3): the essential image is annihilated by the defining ideal”.

Stacks 04CJ, part (3), half of the essential-image assertion: the ideal cutting out the closed subspace annihilates every direct image f_*G.

Restriction of scalars along f♯ makes a section a of 𝒪_Y act on f_*G as f♯(a), so a section killed by f♯ acts as zero. Neither the closed-immersion hypothesis on f nor surjectivity of f♯ is used.

This is also one inclusion of the essential-image clause of Stacks 08KS for algebraic spaces; the containment form of it is AlgebraicGeometry.Space.essImage_modulePushforward_le_annihilatedByKerIdeal of StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionModulePushforwardExactness.lean, which carries no tag of its own, and the reverse inclusion is AlgebraicGeometry.Space.essImage_modulePushforward_of_annihilatedByKerIdeal, proved with no hypothesis beyond the closed immersion.

theorem annihilatedByKerIdeal_modulePushforward (f : X ⟶ Y)
    (G : Modules.{u, u} B S hS X.1 X.2) :
    AnnihilatedByKerIdeal B S hS f ((modulePushforward B S hS f).obj G)

AlgebraicGeometry.Space.annihilatedByKerIdeal_of_essImage_modulePushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionModulePushforward.lean, line 285. The attribute's comment: “part (3): the essential image is annihilated by the defining ideal”.

Stacks 04CJ, part (3), half of the essential-image assertion, in essential-image form: every 𝒪_Y-module isomorphic to a direct image along f is annihilated by the ideal cutting out the closed subspace. This is AlgebraicGeometry.Space.annihilatedByKerIdeal_modulePushforward transported along an isomorphism, and is the inclusion essImage f_* ⊆ {𝓕 | 𝓘𝓕 = 0} of the essential-image clause of Stacks 08KS for algebraic spaces, whose tag is carried by AlgebraicGeometry.Space.essImage_modulePushforward_le_annihilatedByKerIdeal of StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionModulePushforwardExactness.lean.

theorem annihilatedByKerIdeal_of_essImage_modulePushforward (f : X ⟶ Y)
    {G : Modules.{u, u} B S hS Y.1 Y.2} (hG : (modulePushforward B S hS f).essImage G) :
    AnnihilatedByKerIdeal B S hS f G

AlgebraicGeometry.Space.fullyFaithfulQuasicoherentModulePushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionModulePushforward.lean, line 321. The attribute's comment: “part (3): the direct image is fully faithful on quasi-coherent modules”.

Stacks 04CJ, part (3), the full-faithfulness assertion: direct image along a closed immersion of algebraic spaces is fully faithful on quasi-coherent modules.

It is fully faithful on all modules by AlgebraicGeometry.Space.fullyFaithfulModulePushforward, and a full subcategory inclusion is fully faithful.

def fullyFaithfulQuasicoherentModulePushforward (f : X ⟶ Y)
    (hf : IsClosedImmersion B S hS f.hom) :
    (quasicoherentModulePushforward B S hS f).FullyFaithful

AlgebraicGeometry.Space.quasicoherentDirectImageEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionQuasicoherentEquivalence.lean, line 97. The attribute's comment: “part (3): quasi-coherence of the direct image, and quasi-coherence of the module whose direct image an annihilated quasi-coherent module is”.

Part (3) of Stacks 04CJ in the form Stacks 04CL consumes. For a closed immersion i : Z ⟶ X of algebraic spaces the direct image carries quasi-coherent 𝒪_Z-modules to quasi-coherent 𝒪_X-modules, and every quasi-coherent 𝒪_X-module annihilated by 𝓘 = ker(i♯) is the direct image of a quasi-coherent 𝒪_Z-module.

The first clause is the closed-immersion case of Stacks 03M9, AlgebraicGeometry.Space.isQuasicoherentOnSite_modulePushforward_of_isClosedImmersion. For the second, an annihilated 𝒪_X-module is a direct image by the unconditional essential-image clause AlgebraicGeometry.Space.essImage_modulePushforward_iff, so the unit 𝓕 ⟶ i_*i^*𝓕 is an isomorphism, and the witness i^*𝓕 is quasi-coherent by the closed-immersion case of Stacks 03GA.

theorem quasicoherentDirectImageEquivalence (i : Z ⟶ X)
    (hi : IsClosedImmersion B S hS i.hom) :
    QuasicoherentDirectImageEquivalence B S hS i

AlgebraicGeometry.Space.quasicoherentDirectImageOfClosedImmersion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionQuasicoherentEquivalence.lean, line 118. The attribute's comment: “part (3): the induced functor on quasi-coherent modules”.

The functor i_* : QCoh(𝒪_Z) ⥤ QCoh(𝒪_X) of Stacks 04CJ, part (3), for a closed immersion i : Z ⟶ X of algebraic spaces.

This is AlgebraicGeometry.Space.quasicoherentPushforwardOfEquivalence with its hypothesis discharged by AlgebraicGeometry.Space.quasicoherentDirectImageEquivalence; composing it with the inclusion of the quasi-coherent modules gives back the direct image of all modules, so it is the functor the source names and not another one of the same type.

def quasicoherentDirectImageOfClosedImmersion (i : Z ⟶ X) (hi : IsClosedImmersion B S hS i.hom) :
    QuasicoherentSheaves.{u, u} B S hS Z.1 Z.2 ⥤ QuasicoherentSheaves.{u, u} B S hS X.1 X.2

AlgebraicGeometry.Space.fullyFaithfulQuasicoherentDirectImage, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionQuasicoherentEquivalence.lean, line 138. The attribute's comment: “part (3): the direct image on quasi-coherent modules is fully faithful”.

Stacks 04CJ, part (3), the full-faithfulness clause. The direct image i_* : QCoh(𝒪_Z) ⥤ QCoh(𝒪_X) along a closed immersion of algebraic spaces is fully faithful.

The direct image is fully faithful on all modules by AlgebraicGeometry.Space.fullyFaithfulModulePushforward (part (2)), and a lift along a full subcategory inclusion inherits that.

def fullyFaithfulQuasicoherentDirectImage (i : Z ⟶ X) (hi : IsClosedImmersion B S hS i.hom) :
    (quasicoherentDirectImageOfClosedImmersion B S hS i hi).FullyFaithful

AlgebraicGeometry.Space.exactFunctor_quasicoherentDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionQuasicoherentEquivalence.lean, line 171. The attribute's comment: “part (3): the direct image on quasi-coherent modules is exact”.

Stacks 04CJ, part (3), the exactness clause. The direct image i_* : QCoh(𝒪_Z) ⥤ QCoh(𝒪_X) along a closed immersion of algebraic spaces is an exact functor.

theorem exactFunctor_quasicoherentDirectImage (i : Z ⟶ X)
    (hi : IsClosedImmersion B S hS i.hom) :
    exactFunctor (QuasicoherentSheaves.{u, u} B S hS Z.1 Z.2)
      (QuasicoherentSheaves.{u, u} B S hS X.1 X.2)
      (quasicoherentDirectImageOfClosedImmersion B S hS i hi)

AlgebraicGeometry.Space.essImage_quasicoherentDirectImage_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionQuasicoherentEquivalence.lean, line 189. The attribute's comment: “part (3): the essential image is the quasi-coherent modules annihilated by the defining ideal”.

Stacks 04CJ, part (3), the essential-image clause. A quasi-coherent 𝒪_X-module is the direct image of a quasi-coherent 𝒪_Z-module along the closed immersion i exactly when the ideal 𝓘 = ker(i♯) cutting out Z annihilates it.

The forward implication is AlgebraicGeometry.Space.annihilatedByKerIdeal_of_essImage_modulePushforward, applied to the underlying 𝒪_X-module. The converse is the second clause of AlgebraicGeometry.Space.quasicoherentDirectImageEquivalence.

theorem essImage_quasicoherentDirectImage_iff (i : Z ⟶ X)
    (hi : IsClosedImmersion B S hS i.hom)
    (F : QuasicoherentSheaves.{u, u} B S hS X.1 X.2) :
    (quasicoherentDirectImageOfClosedImmersion B S hS i hi).essImage F ↔
      AnnihilatedByKerIdeal B S hS i F.obj
Tag 04CK, a lemma

Tag 04CK in the Stacks Project.

AlgebraicGeometry.Space.existsUnique_largestQuasicoherentSubobject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleKernelQuasicoherent.lean, line 363.

Stacks 04CK. Let S be a scheme, let X be an algebraic space over S, let 𝓕 be a quasi-coherent 𝒪_X-module and let 𝒢 ⊆ 𝓕 be an 𝒪_X-submodule. There is a unique quasi-coherent 𝒪_X-submodule 𝒢' ⊆ 𝒢 for which composition with the inclusion 𝒢' ⊆ 𝒢 is a bijection Hom(𝓗, 𝒢') ⟶ Hom(𝓗, 𝒢) for every quasi-coherent 𝒪_X-module 𝓗.

This is AlgebraicGeometry.Space.existsUnique_quasicoherentSubobject_of_isClosedUnderKernels with its kernel hypothesis discharged by AlgebraicGeometry.Space.isClosedUnderKernels.

theorem existsUnique_largestQuasicoherentSubobject (M : Modules.{u, m} B S hS F hF)
    [M.IsQuasicoherentOnSite] (G : Subobject M) :
    ∃! G' : { G' : Subobject (G : Modules.{u, m} B S hS F hF) //
        (G' : Modules.{u, m} B S hS F hF).IsQuasicoherentOnSite },
      ∀ (H : Modules.{u, m} B S hS F hF) [H.IsQuasicoherentOnSite],
        Function.Bijective
          (fun f : H ⟶ (G'.1 : Modules.{u, m} B S hS F hF) ↦ f ≫ G'.1.arrow)

AlgebraicGeometry.Space.exists_greatest_quasicoherentSubobject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleKernelQuasicoherent.lean, line 381.

Stacks 04CK, the maximality clause. The quasi-coherent submodule of AlgebraicGeometry.Space.existsUnique_largestQuasicoherentSubobject is the largest quasi-coherent submodule of 𝓕 contained in 𝒢.

This is AlgebraicGeometry.Space.exists_greatest_quasicoherentSubobject_of_isClosedUnderKernels with its kernel hypothesis discharged by AlgebraicGeometry.Space.isClosedUnderKernels.

theorem exists_greatest_quasicoherentSubobject (M : Modules.{u, m} B S hS F hF)
    [M.IsQuasicoherentOnSite] (G : Subobject M) :
    ∃ G' : Subobject (G : Modules.{u, m} B S hS F hF),
      (G' : Modules.{u, m} B S hS F hF).IsQuasicoherentOnSite ∧
        ∀ K : Subobject (G : Modules.{u, m} B S hS F hF),
          (K : Modules.{u, m} B S hS F hF).IsQuasicoherentOnSite → K ≤ G'
Tag 04CL, a lemma

Tag 04CL in the Stacks Project.

AlgebraicGeometry.Space.isLeftAdjoint_quasicoherentDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionQuasicoherentUpperShriek.lean, line 56.

Stacks 04CL. Let S be a scheme and let i : Z ⟶ X be a closed immersion of algebraic spaces over S. Then the direct image i_* : QCoh(𝒪_Z) ⥤ QCoh(𝒪_X) has a right adjoint, the functor i^! of the source.

theorem isLeftAdjoint_quasicoherentDirectImage (i : Z ⟶ X)
    (hi : IsClosedImmersion B S hS i.hom) :
    (quasicoherentDirectImageOfClosedImmersion B S hS i hi).IsLeftAdjoint

AlgebraicGeometry.Space.quasicoherentRightAdjointOfClosedImmersion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionQuasicoherentUpperShriek.lean, line 67. The attribute's comment: “the functor i^!”.

Stacks 04CL, the functor i^!: the right adjoint of the direct image i_* : QCoh(𝒪_Z) ⥤ QCoh(𝒪_X) along a closed immersion i : Z ⟶ X of algebraic spaces. For a quasi-coherent 𝒪_X-module 𝓖, the direct image of i^! 𝓖 is the largest quasi-coherent submodule of 𝓖 annihilated by the ideal cutting out Z.

def quasicoherentRightAdjointOfClosedImmersion (i : Z ⟶ X)
    (hi : IsClosedImmersion B S hS i.hom) :
    QuasicoherentSheaves.{u, u} B S hS X.1 X.2 ⥤ QuasicoherentSheaves.{u, u} B S hS Z.1 Z.2

AlgebraicGeometry.Space.quasicoherentDirectImageAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionQuasicoherentUpperShriek.lean, line 76. The attribute's comment: “the adjunction i_* ⊣ i^!”.

Stacks 04CL, the adjunction i_* ⊣ i^! exhibiting AlgebraicGeometry.Space.quasicoherentRightAdjointOfClosedImmersion as a right adjoint of the direct image of quasi-coherent modules along a closed immersion of algebraic spaces.

def quasicoherentDirectImageAdjunction (i : Z ⟶ X) (hi : IsClosedImmersion B S hS i.hom) :
    quasicoherentDirectImageOfClosedImmersion B S hS i hi ⊣
      quasicoherentRightAdjointOfClosedImmersion B S hS i hi
Tag 0CYZ, a definition

Tag 0CYZ in the Stacks Project.

AlgebraicGeometry.Space.definingIdealSheaf_schemeTheoreticUnion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedSubspaceIdealLattice.lean, line 279. The attribute's comment: “the defining ideal of the scheme-theoretic union is the meet of the two defining ideals”.

Stacks 0CYZ. The defining ideal sheaf of the scheme-theoretic union of two closed subspaces is the meet of their defining ideal sheaves.

One containment is inclusion-reversal. For the other, the meet of the two ideal sheaves is quasi-coherent, hence by Stacks 03MB cuts out a closed subspace W; that W contains both Y and Z because its ideal is contained in each of theirs, so the scheme-theoretic union, being the smallest closed subspace containing both, is contained in W, and inclusion-reversal gives the containment of ideals back.

theorem definingIdealSheaf_schemeTheoreticUnion :
    definingIdealSheaf B S hS X (schemeTheoreticUnion B S hS X.1 X.2 Y Z) =
      definingIdealSheaf B S hS X Y ⊓ definingIdealSheaf B S hS X Z

AlgebraicGeometry.Space.definingIdealSheaf_schemeTheoreticIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedSubspaceIdealLattice.lean, line 307. The attribute's comment: “the defining ideal of the scheme-theoretic intersection is the sum of the two defining ideals”.

Stacks 0CYZ. The defining ideal sheaf of the scheme-theoretic intersection of two closed subspaces is the sum of their defining ideal sheaves.

One containment is inclusion-reversal. For the other, the sum of the two ideal sheaves is quasi-coherent, hence by Stacks 03MB cuts out a closed subspace W; that W is contained in both Y and Z because its ideal contains each of theirs, hence in their intersection, and inclusion-reversal gives the containment of ideals back.

theorem definingIdealSheaf_schemeTheoreticIntersection :
    definingIdealSheaf B S hS X (schemeTheoreticIntersection B S hS X.1 X.2 Y Z) =
      definingIdealSheaf B S hS X Y ⊔ definingIdealSheaf B S hS X Z

AlgebraicGeometry.Space.schemeTheoreticIntersection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZeroScheme.lean, line 261. The attribute's comment: “scheme-theoretic intersection”.

Stacks 0CYZ. The closed subspace cut out by the sum of the defining quasi-coherent ideal sheaves.

def schemeTheoreticIntersection (hF : IsAlgebraicSpace B S hS F)
    (Z Y : ClosedSubspaces B S hS F) :
    ClosedSubspaces B S hS F

AlgebraicGeometry.Space.schemeTheoreticUnion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZeroScheme.lean, line 280. The attribute's comment: “scheme-theoretic union”.

Stacks 0CYZ. The closed subspace cut out by the intersection of the defining quasi-coherent ideal sheaves.

def schemeTheoreticUnion (hF : IsAlgebraicSpace B S hS F)
    (Z Y : ClosedSubspaces B S hS F) :
    ClosedSubspaces B S hS F
Tag 0CZ0, a lemma

Tag 0CZ0 in the Stacks Project.

AlgebraicGeometry.Space.isPullback_schemeTheoreticIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ClosedImmersions.lean, line 182. The attribute's comment: “the intersection square is cartesian”.

The scheme-theoretic intersection of two closed subspaces of an algebraic space over S is the fibre product of the two over the ambient space: the square formed by the four inclusions is Cartesian in the category of presheaves on the big fppf site of S.

theorem isPullback_schemeTheoreticIntersection (hF : IsAlgebraicSpace B S hS F)
    (Z Y : ClosedSubspaces B S hS F) :
    IsPullback
      (Subfunctor.homOfLe (show (schemeTheoreticIntersection B S hS F hF Z Y).1 ≤ Z.1 from
        inf_le_left))
      (Subfunctor.homOfLe (show (schemeTheoreticIntersection B S hS F hF Z Y).1 ≤ Y.1 from
        inf_le_right))
      Z.1.ι Y.1.ι

AlgebraicGeometry.Space.isClosedImmersion_schemeTheoreticIntersection_le_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ClosedImmersions.lean, line 195. The attribute's comment: “closed immersion into the first factor”.

The scheme-theoretic intersection of two closed subspaces of an algebraic space over S is a closed subspace of the first of them.

theorem isClosedImmersion_schemeTheoreticIntersection_le_left
    (hF : IsAlgebraicSpace B S hS F) (Z Y : ClosedSubspaces B S hS F) :
    IsClosedImmersion B S hS
      (Subfunctor.homOfLe (show (schemeTheoreticIntersection B S hS F hF Z Y).1 ≤ Z.1 from
        inf_le_left))

AlgebraicGeometry.Space.isClosedImmersion_schemeTheoreticIntersection_le_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ClosedImmersions.lean, line 205. The attribute's comment: “closed immersion into the second factor”.

The scheme-theoretic intersection of two closed subspaces of an algebraic space over S is a closed subspace of the second of them.

theorem isClosedImmersion_schemeTheoreticIntersection_le_right
    (hF : IsAlgebraicSpace B S hS F) (Z Y : ClosedSubspaces B S hS F) :
    IsClosedImmersion B S hS
      (Subfunctor.homOfLe (show (schemeTheoreticIntersection B S hS F hF Z Y).1 ≤ Y.1 from
        inf_le_right))
Tag 0CZ1, a lemma

Tag 0CZ1 in the Stacks Project.

AlgebraicGeometry.Space.unionIntersectionShortComplex_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedUnionIntersectionSequence.lean, line 423. The attribute's comment: “the short exact sequence of the structure sheaves of the union, the two subspaces and the intersection”.

Stacks 0CZ1, second assertion. For two closed subspaces Y, Z of an algebraic space X over S, with Y ∪ Z and Y ∩ Z their scheme-theoretic union and intersection,

0 ⟶ 𝒪_{Y ∪ Z} ⟶ 𝒪_Y × 𝒪_Z ⟶ 𝒪_{Y ∩ Z} ⟶ 0

is a short exact sequence of 𝒪_X-modules, the four structure sheaves being taken as modules on X under Stacks 04CJ, the first map built from the two canonical maps 𝒪_{Y ∪ Z} ⟶ 𝒪_Y and 𝒪_{Y ∪ Z} ⟶ 𝒪_Z and the second from the canonical map 𝒪_Y ⟶ 𝒪_{Y ∩ Z} and the negative of the canonical map 𝒪_Z ⟶ 𝒪_{Y ∩ Z}.

This is AlgebraicGeometry.Space.shortExact_biprod_of_ker_eq_inf_sup applied to the four structure projections of 𝒪_X, which are epimorphisms by AlgebraicGeometry.Space.epi_structureProjection and whose kernels are the four defining ideals; the two identifications of Stacks 0CYZ say that the kernels for the union and the intersection are the meet and the join of the kernels for Y and Z.

theorem unionIntersectionShortComplex_shortExact :
    (unionIntersectionShortComplex B S hS X Y Z).ShortExact

AlgebraicGeometry.Space.isPushout_schemeTheoreticUnion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedUnionPushout.lean, line 610. The attribute's comment: “the square of the two subspaces, their scheme-theoretic intersection and their scheme-theoretic union is cocartesian in the category of algebraic spaces over the base”.

[Stacks, Tag 0CZ1], third assertion. Let X be an algebraic space over a scheme S and let Y, Z ⊆ X be closed subspaces, with Y ∪ Z and Y ∩ Z the scheme-theoretic union and intersection of [Stacks Project, Tag 0CYZ]. Then the square

Y ∩ Z ⟶ Y
  ↓        ↓
  Z   ⟶ Y ∪ Z

of the four closed subspaces and the four inclusions is cocartesian in the category of algebraic spaces over S, that is, Y ∪ Z = Y ⨿_{Y ∩ Z} Z.

This is AlgebraicGeometry.Space.existsUnique_desc_schemeTheoreticUnion packaged as a colimit; the square commutes because both composites are the inclusion of Y ∩ Z into Y ∪ Z.

theorem isPushout_schemeTheoreticUnion (X : AlgebraicSpaces B S hS)
    (Y Z : ClosedSubspaces B S hS X.1) :
    IsPushout
      (ObjectProperty.homMk (Subfunctor.homOfLe (inf_le_left : Y.1 ⊓ Z.1 ≤ Y.1)) :
        closedSubspaceToSpace B S hS X (schemeTheoreticIntersection B S hS X.1 X.2 Y Z) ⟶
          closedSubspaceToSpace B S hS X Y)
      (ObjectProperty.homMk (Subfunctor.homOfLe (inf_le_right : Y.1 ⊓ Z.1 ≤ Z.1)) :
        closedSubspaceToSpace B S hS X (schemeTheoreticIntersection B S hS X.1 X.2 Y Z) ⟶
          closedSubspaceToSpace B S hS X Z)
      (ObjectProperty.homMk
          (Subfunctor.homOfLe (le_schemeTheoreticUnion_left B S hS X.2 Y Z)) :
        closedSubspaceToSpace B S hS X Y ⟶
          closedSubspaceToSpace B S hS X (schemeTheoreticUnion B S hS X.1 X.2 Y Z))
      (ObjectProperty.homMk
          (Subfunctor.homOfLe (le_schemeTheoreticUnion_right B S hS X.2 Y Z)) :
        closedSubspaceToSpace B S hS X Z ⟶
          closedSubspaceToSpace B S hS X (schemeTheoreticUnion B S hS X.1 X.2 Y Z))

AlgebraicGeometry.Space.isClosedImmersion_le_schemeTheoreticUnion_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ClosedImmersions.lean, line 229. The attribute's comment: “closed immersion of the first subspace into the union”.

The first of two closed subspaces of an algebraic space over S is a closed subspace of their scheme-theoretic union.

theorem isClosedImmersion_le_schemeTheoreticUnion_left (hF : IsAlgebraicSpace B S hS F)
    (Y Z : ClosedSubspaces B S hS F) :
    IsClosedImmersion B S hS
      (Subfunctor.homOfLe (le_schemeTheoreticUnion_left B S hS hF Y Z))

AlgebraicGeometry.Space.isClosedImmersion_le_schemeTheoreticUnion_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ClosedImmersions.lean, line 238. The attribute's comment: “closed immersion of the second subspace into the union”.

The second of two closed subspaces of an algebraic space over S is a closed subspace of their scheme-theoretic union.

theorem isClosedImmersion_le_schemeTheoreticUnion_right (hF : IsAlgebraicSpace B S hS F)
    (Y Z : ClosedSubspaces B S hS F) :
    IsClosedImmersion B S hS
      (Subfunctor.homOfLe (le_schemeTheoreticUnion_right B S hS hF Y Z))
Sources
LeanAlgebraicGeometry.Space.kerIdealSmulQuotientUnitIso · AlgebraicGeometry.Space.cokernel_π_comp_kerIdealSmulQuotientUnitIso_hom · AlgebraicGeometry.Space.isIso_modulePullbackAdjunction_counit · AlgebraicGeometry.Space.modulePullbackCounitIso · AlgebraicGeometry.Space.annihilatedByKerIdeal_modulePushforward · AlgebraicGeometry.Space.annihilatedByKerIdeal_of_essImage_modulePushforward · AlgebraicGeometry.Space.fullyFaithfulQuasicoherentModulePushforward · AlgebraicGeometry.Space.quasicoherentDirectImageEquivalence

Section67.15 Supports of modules#

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

Tag 07TY, a lemma

Tag 07TY in the Stacks Project.

AlgebraicGeometry.Space.supp_restrictToChart_eq_preimage_supportOfSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SupportChartZariski.lean, line 342. The attribute's comment: “the support equality, given the comparison isomorphism of Stacks 05VP”.

Stacks 07TY. Let X be an algebraic space over S, let F be an 𝒪_X-module and let φ : U ⟶ X be an étale morphism from a scheme, that is, an object of the small étale site of X. Then the support of φ^* F as a module on the scheme U is the inverse image under |φ| of the support of F on X: Supp(φ^* F) = |φ|^{-1}(Supp(F)).

The hypothesis h05VP is the comparison of Stacks 05VP, (φ^* F)_u ⊗_{𝒪_{U, u}} 𝒪_{X, x̄} ≅ F_{x̄}, which this development does not prove; it holds for a quasi-coherent F, which is the hypothesis Stacks 07TY carries, and it is the only place quasi-coherence is used in the proof. Everything else is unconditional: faithful flatness of the base change turns the comparison into the equivalence of the two vanishings (AlgebraicGeometry.Space.nontrivial_chartStalkTensorEtaleLocalRing_iff_mem_supp), a geometric representative of a point of the chart gives one inclusion (AlgebraicGeometry.Space.exists_geometricRepresentative), and the étale lift of a geometric point, Stacks 05VN, gives the other (AlgebraicGeometry.Space.exists_geometricPoint_lift_of_isEtale).

theorem supp_restrictToChart_eq_preimage_supportOfSheaf
    (F : Modules.{u, u} B S hS X.1 X.2)
    (h05VP : ∀ (x : GeometricPoint B S hS X.1) (V : SmallEtaleNeighborhood x),
      Nonempty (chartStalkTensorEtaleLocalRing.{u, u} B S hS X.1 X.2 V F ≅
        geometricModuleStalk B S hS X x F)) :
    SheafOfModules.supp (restrictToChart B S hS X.2 F U) =
      (fun u => pointsMap B S hS (yoneda.obj ((SmallEtale.toOver B S hS X.1).obj U))
          U.obj.hom
          ((pointsEquivScheme B S hS ((SmallEtale.toOver B S hS X.1).obj U)).symm u)) ⁻¹'
        supportOfSheaf B S hS X.1 ((SheafOfModules.toSheaf _).obj F)

AlgebraicGeometry.Space.supp_restrictToChart_eq_preimage_supportOfSheaf_of_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SupportGeometricStalkCriterion.lean, line 88. The attribute's comment: “the support equality for a quasi-coherent module”.

Stacks 07TY. Let X be an algebraic space over S, let F be a quasi-coherent 𝒪_X-module and let φ : U ⟶ X be an étale morphism from a scheme, that is, an object of the small étale site of X. Then the support of φ^* F as a module on the scheme U is the inverse image under |φ| of the support of F: Supp(φ^* F) = |φ|^{-1}(Supp(F)).

The comparison (φ^* F)_u ⊗_{𝒪_{U, u}} 𝒪_{X, x̄} ≅ F_{x̄} which the general form of the statement carries as a hypothesis is Stacks 05VP, available because F is quasi-coherent.

theorem supp_restrictToChart_eq_preimage_supportOfSheaf_of_isQuasicoherent
    (X : AlgebraicSpaces B S hS) (U : SmallEtale B S hS X.1)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite] :
    SheafOfModules.supp (restrictToChart B S hS X.2 F U) =
      (fun u => pointsMap B S hS (yoneda.obj ((SmallEtale.toOver B S hS X.1).obj U))
          U.obj.hom
          ((pointsEquivScheme B S hS ((SmallEtale.toOver B S hS X.1).obj U)).symm u)) ⁻¹'
        supportOfSheaf B S hS X.1 ((SheafOfModules.toSheaf _).obj F)
Tag 07TZ, a lemma

Tag 07TZ in the Stacks Project.

AlgebraicGeometry.Space.nontrivial_geometricModuleStalk_iff_nontrivial_residueFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricStalkResidueFibre.lean, line 105. The attribute's comment: “part (2), second equivalence: the stalk at a geometric point is nonzero iff the fibre over the residue field is nonzero”.

Stacks 07TZ, part (2), second equivalence. Let F be a quasi-coherent 𝒪_X-module of finite type on an algebraic space X over S and let x̄ be a geometric point of X. Then

F_{x̄} ≠ 0 ↔ F_{x̄} ⊗_{𝒪_{X, x̄}} κ(x̄) ≠ 0.

This is Nakayama's lemma. The stalk is a finite module over the étale local ring by AlgebraicGeometry.Space.module_finite_geometricModuleStalk, and the residue map is a local homomorphism of local rings, so base change along it keeps a nonzero finite module nonzero (AlgebraicGeometry.Space.nontrivial_extendScalars_of_isLocalHom); the converse direction needs no hypotheses at all (AlgebraicGeometry.Space.nontrivial_of_nontrivial_extendScalars).

theorem nontrivial_geometricModuleStalk_iff_nontrivial_residueFibre (X : AlgebraicSpaces B S hS)
    (F : Modules.{u, u} B S hS X.1 X.2) (hqc : F.IsQuasicoherentOnSite)
    (hft : SheafOfModules.IsFiniteTypeOnSite F) (x : GeometricPoint B S hS X.1) :
    Nontrivial ↥(geometricModuleStalk B S hS X x F) ↔
      letI := isLocalRing_etaleLocalRing B S hS X.1 X.2 x
      Nontrivial ↥(geometricModuleResidueFibre B S hS X x F)

AlgebraicGeometry.Space.supportOfSheaf_modulePullback_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModulePullbackSupportEquality.lean, line 228. The attribute's comment: “part (3): the stalk of a pullback at a geometric point, and the equality of supports”.

Stacks 07TZ, part (3). Let g : X' ⟶ X be a morphism of algebraic spaces over S and let F be a quasi-coherent 𝒪_X-module of finite type. Then the support of the pullback g^* F of Stacks 03LU is the inverse image of the support of F:

Supp(g^* F) = |g|^{-1}(Supp(F)).

The pullback is again of finite type by Stacks 03DO, AlgebraicGeometry.Space.isFiniteTypeOnSite_modulePullback, which is the other clause of this part of the tag.

At a geometric point ȳ of X' the stalk of the pullback is the base change (g^* F)_{ȳ} ≅ 𝒪_{X', ȳ} ⊗_{𝒪_{X, g ∘ ȳ}} F_{g ∘ ȳ} of the stalk of F at the image geometric point, by AlgebraicGeometry.Space.geometricModuleStalkPullbackIso. One inclusion is AlgebraicGeometry.Space.nontrivial_of_nontrivial_extendScalars, which needs no hypotheses. The other is AlgebraicGeometry.Space.nontrivial_extendScalars_of_isLocalHom: the stalk of F is a finite module over the étale local ring, the homomorphism of étale local rings of Stacks 04NG is local, and the image geometric point detects the support because F is quasi-coherent (the first equivalence of part (2)).

theorem supportOfSheaf_modulePullback_eq (g : X' ⟶ X) (F : Modules.{u, u} B S hS X.1 X.2)
    (hqc : F.IsQuasicoherentOnSite) (hft : SheafOfModules.IsFiniteTypeOnSite F) :
    supportOfSheaf B S hS X'.1
        ((SheafOfModules.toSheaf _).obj ((modulePullback B S hS g).obj F)) =
      pointsMap B S hS X'.1 g.hom ⁻¹'
        supportOfSheaf B S hS X.1 ((SheafOfModules.toSheaf _).obj F)

AlgebraicGeometry.Space.isClosed_supportOfSheaf_of_isFiniteTypeOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SupportClosedFiniteType.lean, line 335. The attribute's comment: “support_closed”.

Stacks 07TZ, part (1). The support of an 𝒪_X-module of finite type on an algebraic space X is closed in the point set of X.

Outside the support pick a geometric point over the given point; its stalk vanishes, so there is an étale chart carrying only the zero section of the module. The image of the point set of that chart is open, because an étale chart is open on points by clause (3) of Stacks 03BX, it contains the given point, and it misses the support: a geometric point of X over a point of the image lifts to the chart by Stacks 05VN, so the chart is a neighbourhood of it and its stalk vanishes too.

theorem isClosed_supportOfSheaf_of_isFiniteTypeOnSite (hX : IsAlgebraicSpace B S hS X)
    (F : Modules.{u, m} B S hS X hX) [SheafOfModules.IsFiniteTypeOnSite F] :
    IsClosed (supportOfSheaf B S hS X ((SheafOfModules.toSheaf _).obj F))

AlgebraicGeometry.Space.supportOfSheaf_of_isQuasicoherentOnSite_isFiniteTypeOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SupportFiniteTypeModule.lean, line 92.

Stacks 07TZ. Let X be an algebraic space over a scheme S and let F be a quasi-coherent 𝒪_X-module of finite type. Then

  1. the support of F is closed;
  2. for a geometric point x̄ of X lying over a point x, x ∈ Supp(F) ↔ F_{x̄} ≠ 0 and F_{x̄} ≠ 0 ↔ F_{x̄} ⊗_{𝒪_{X, x̄}} κ(x̄) ≠ 0;
  3. for every morphism g : X' ⟶ X of algebraic spaces over S the pullback g^* F of Stacks 03LU is again of finite type and Supp(g^* F) = |g|^{-1}(Supp(F)).

Clause (1) is AlgebraicGeometry.Space.isClosed_supportOfSheaf_of_isFiniteTypeOnSite, which does not use quasi-coherence. The two equivalences of clause (2) are AlgebraicGeometry.Space.mem_supportOfSheaf_iff_nontrivial_geometricModuleStalk_of_liesOver and AlgebraicGeometry.Space.nontrivial_geometricModuleStalk_iff_nontrivial_residueFibre. The two conclusions of clause (3) are AlgebraicGeometry.Space.isFiniteTypeOnSite_modulePullback and AlgebraicGeometry.Space.supportOfSheaf_modulePullback_eq.

theorem supportOfSheaf_of_isQuasicoherentOnSite_isFiniteTypeOnSite
    (X : AlgebraicSpaces B S hS) (F : Modules.{u, u} B S hS X.1 X.2)
    (hqc : F.IsQuasicoherentOnSite) (hft : SheafOfModules.IsFiniteTypeOnSite F) :
    IsClosed (supportOfSheaf B S hS X.1 ((SheafOfModules.toSheaf _).obj F)) ∧
      (∀ (x : GeometricPoint B S hS X.1) (pt : points B S hS X.1), x.LiesOver pt →
        (pt ∈ supportOfSheaf B S hS X.1 ((SheafOfModules.toSheaf _).obj F) ↔
            Nontrivial (geometricModuleStalk B S hS X x F)) ∧
          (Nontrivial (geometricModuleStalk B S hS X x F) ↔
            letI := isLocalRing_etaleLocalRing B S hS X.1 X.2 x
            Nontrivial (geometricModuleResidueFibre B S hS X x F))) ∧
      ∀ (X' : AlgebraicSpaces B S hS) (g : X' ⟶ X),
        SheafOfModules.IsFiniteTypeOnSite ((modulePullback B S hS g).obj F) ∧
          supportOfSheaf B S hS X'.1
              ((SheafOfModules.toSheaf _).obj ((modulePullback B S hS g).obj F)) =
            pointsMap B S hS X'.1 g.hom ⁻¹'
              supportOfSheaf B S hS X.1 ((SheafOfModules.toSheaf _).obj F)

AlgebraicGeometry.Space.mem_supportOfSheaf_iff_nontrivial_geometricModuleStalk_of_liesOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SupportGeometricStalkCriterion.lean, line 133. The attribute's comment: “part (2), first equivalence: the support against the stalk at a geometric point”.

Stacks 07TZ, part (2), first equivalence. Let F be a quasi-coherent 𝒪_X-module on an algebraic space X and let x̄ be a geometric point lying over a point x of X. Then

x ∈ Supp(F) ↔ F_{x̄} ≠ 0.

The support of Stacks 04KA is defined by nonvanishing of the stalk at some geometric point over x; the content here is that for a quasi-coherent module every geometric point over x detects the support, so the equivalence holds at the given x̄.

Pick a small étale neighbourhood of x̄. Nonvanishing of F_{x̄} is membership of the chart point in the support of the chart restriction, and that support is the inverse image of the support of F by Stacks 07TY; the chart point maps to the image of x̄, which is x.

theorem mem_supportOfSheaf_iff_nontrivial_geometricModuleStalk_of_liesOver
    (X : AlgebraicSpaces B S hS) (F : Modules.{u, u} B S hS X.1 X.2)
    [F.IsQuasicoherentOnSite] (x : GeometricPoint B S hS X.1)
    (pt : points B S hS X.1) (hx : x.LiesOver pt) :
    pt ∈ supportOfSheaf B S hS X.1 ((SheafOfModules.toSheaf _).obj F) ↔
      Nontrivial (geometricModuleStalk B S hS X x F)
Tag 07U0, a lemma

Tag 07U0 in the Stacks Project.

AlgebraicGeometry.Space.supportOfSheaf_eq_range_pointsMap_schemeTheoreticSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/ProperModuleSupport.lean, line 178. The attribute's comment: “part (4): the support of F is the point set of its scheme-theoretic support”.

The support of a finite type 𝒪_X-module is the set of points of its scheme-theoretic support.

The point set of a closed subspace is the zero locus of its defining ideal sheaf, and the ideal sheaf cutting out the scheme-theoretic support is the annihilator ideal of F; so the claim is that the support of F is the zero locus of its annihilator ideal sheaf. One inclusion needs only that the unit function lies in the annihilator ideal wherever that ideal is the whole of 𝒪_X, so F vanishes on every chart over such a chart and its support misses the image. The other is where finite type enters: off the support every geometric stalk of F vanishes, and for a module of finite type that produces a small étale neighbourhood over which F has no nonzero sections at all, hence a chart whose image contains the point and on which the annihilator ideal is everything.

That the scheme-theoretic support is a closed subspace cut out by the annihilator ideal sheaf is AlgebraicGeometry.Space.exists_isClosedSubspace_schemeTheoreticSupport, which quasi- coherence and finite type supply.

This is part (4) of [Stacks, Tag 07U0] for the module on the ambient space.

theorem supportOfSheaf_eq_range_pointsMap_schemeTheoreticSupport
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : F.IsQuasicoherentOnSite)
    (hFft : SheafOfModules.IsFiniteTypeOnSite F) :
    supportOfSheaf B S hS X.1 ((SheafOfModules.toSheaf _).obj F) =
      Set.range (pointsMap B S hS (schemeTheoreticSupport B S hS X F).toFunctor
        (schemeTheoreticSupport B S hS X F).ι)

AlgebraicGeometry.Space.exists_module_on_schemeTheoreticSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SchemeTheoreticSupport.lean, line 505. The attribute's comment: “existence of the quasi-coherent module on the scheme-theoretic support”.

Stacks 07U0, existence. A finite type quasi-coherent 𝒪_X-module F is the direct image of a quasi-coherent module on its scheme-theoretic support, which is a closed subspace of X.

That the scheme-theoretic support is a closed subspace, and that the ideal cutting it out is the annihilator ideal of F, are AlgebraicGeometry.Space.exists_isClosedSubspace_schemeTheoreticSupport; so that ideal annihilates F, and AlgebraicGeometry.Space.isQuasicoherentEssImagePushforward_of_isClosedImmersion turns that into the module.

theorem exists_module_on_schemeTheoreticSupport (F : Modules.{u, u} B S hS X.1 X.2)
    (hF : F.IsQuasicoherentOnSite)
    (hft : PresheafOfModules.IsFiniteType (smallEtaleRingedSite B S hS X.1 X.2).J F.val) :
    ∃ (hZ : IsClosedSubspace B S hS (schemeTheoreticSupport B S hS X F))
      (G : Modules.{u, u} B S hS
        (closedSubspaceToSpace B S hS X ⟨schemeTheoreticSupport B S hS X F, hZ⟩).1
        (closedSubspaceToSpace B S hS X ⟨schemeTheoreticSupport B S hS X F, hZ⟩).2),
      G.IsQuasicoherentOnSite ∧ Nonempty ((modulePushforward B S hS
        (closedSubspaceInclusion B S hS X
          ⟨schemeTheoreticSupport B S hS X F, hZ⟩)).obj G ≅ F)

AlgebraicGeometry.Space.schemeTheoreticSupport_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SchemeTheoreticSupport.lean, line 527. The attribute's comment: “minimality: the scheme-theoretic support is contained in every closed subspace from which F is a direct image”.

Stacks 07U0, minimality. The scheme-theoretic support of F is contained in every closed subspace of X from which F is a direct image.

The ideal cutting out such a closed subspace annihilates F by the first half of Stacks 04CJ part (3), so that subspace is a member of the family being intersected.

theorem schemeTheoreticSupport_le (F : Modules.{u, u} B S hS X.1 X.2)
    (Z : ClosedSubspaces B S hS X.1)
    (G : Modules.{u, u} B S hS (closedSubspaceToSpace B S hS X Z).1
      (closedSubspaceToSpace B S hS X Z).2)
    (e : (modulePushforward B S hS (closedSubspaceInclusion B S hS X Z)).obj G ≅ F) :
    schemeTheoreticSupport B S hS X F ≤ Z.1

AlgebraicGeometry.Space.module_on_closedSubspace_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SchemeTheoreticSupport.lean, line 543. The attribute's comment: “part (2): uniqueness up to unique isomorphism”.

Stacks 07U0, part (2). A module on a closed subspace of X whose direct image is F is unique up to a unique isomorphism compatible with the chosen identifications of the direct images with F.

This is full faithfulness of the direct image along a closed immersion, Stacks 04CJ part (2).

theorem module_on_closedSubspace_unique (F : Modules.{u, u} B S hS X.1 X.2)
    (Z : ClosedSubspaces B S hS X.1)
    (G H : Modules.{u, u} B S hS (closedSubspaceToSpace B S hS X Z).1
      (closedSubspaceToSpace B S hS X Z).2)
    (eG : (modulePushforward B S hS (closedSubspaceInclusion B S hS X Z)).obj G ≅ F)
    (eH : (modulePushforward B S hS (closedSubspaceInclusion B S hS X Z)).obj H ≅ F) :
    ∃! φ : G ≅ H,
      (modulePushforward B S hS (closedSubspaceInclusion B S hS X Z)).map φ.hom ≫ eH.hom =
        eG.hom

AlgebraicGeometry.Space.isFiniteTypeOnSite_module_on_closedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SchemeTheoreticSupport.lean, line 572. The attribute's comment: “part (3): the module on the closed subspace is of finite type”.

Stacks 07U0, part (3). A module on a closed subspace of X whose direct image is a module of finite type is itself of finite type.

By Stacks 04CJ part (2) it is isomorphic to the inverse image of F, which is of finite type by Stacks 03DO, and finite type passes along an epimorphism.

theorem isFiniteTypeOnSite_module_on_closedSubspace (F : Modules.{u, u} B S hS X.1 X.2)
    (hFft : SheafOfModules.IsFiniteTypeOnSite F) (Z : ClosedSubspaces B S hS X.1)
    (G : Modules.{u, u} B S hS (closedSubspaceToSpace B S hS X Z).1
      (closedSubspaceToSpace B S hS X Z).2)
    (e : (modulePushforward B S hS (closedSubspaceInclusion B S hS X Z)).obj G ≅ F) :
    SheafOfModules.IsFiniteTypeOnSite G

AlgebraicGeometry.Space.schemeTheoreticSupport_isSmallest_and_properties, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SchemeTheoreticSupportCharacterization.lean, line 72.

Stacks 07U0. Let F be a finite type quasi-coherent 𝒪_X-module on an algebraic space X. Its scheme-theoretic support Z is a closed subspace of X carrying a quasi-coherent 𝒪_Z-module G with i_*G ≅ F, and it is the smallest closed subspace from which F is a direct image. Moreover:

  1. on every étale scheme chart U of X, the scheme-theoretic support of the restriction of F to U is Z ×_X U;
  2. a module G on Z with i_*G ≅ F is unique up to unique isomorphism;
  3. such a G is of finite type;
  4. the support of F is |Z|, and the support of such a G is all of |Z|.
theorem schemeTheoreticSupport_isSmallest_and_properties (F : Modules.{u, u} B S hS X.1 X.2)
    (hF : F.IsQuasicoherentOnSite) (hFft : SheafOfModules.IsFiniteTypeOnSite F) :
    ∃ hZ : IsClosedSubspace B S hS (schemeTheoreticSupport B S hS X F),
      -- existence of a quasi-coherent module on `Z` whose direct image is `F`
      (∃ G : Modules.{u, u} B S hS
          (closedSubspaceToSpace B S hS X ⟨schemeTheoreticSupport B S hS X F, hZ⟩).1
          (closedSubspaceToSpace B S hS X ⟨schemeTheoreticSupport B S hS X F, hZ⟩).2,
        G.IsQuasicoherentOnSite ∧ Nonempty ((modulePushforward B S hS
          (closedSubspaceInclusion B S hS X
            ⟨schemeTheoreticSupport B S hS X F, hZ⟩)).obj G ≅ F)) ∧
      -- minimality
      (∀ (Z' : ClosedSubspaces B S hS X.1)
        (G' : Modules.{u, u} B S hS (closedSubspaceToSpace B S hS X Z').1
          (closedSubspaceToSpace B S hS X Z').2),
        ((modulePushforward B S hS (closedSubspaceInclusion B S hS X Z')).obj G' ≅ F) →
          schemeTheoreticSupport B S hS X F ≤ Z'.1) ∧
      -- part (1)
      (∀ A : SmallEtale B S hS X.1,
        letI : (chartRestrictionSheaf B S hS X F A).IsQuasicoherent :=
          isQuasicoherent_chartRestrictionSheaf B S hS X F hF A
        letI : (chartRestrictionSheaf B S hS X F A).IsFiniteType :=
          Stacks.AlgebraicGeometry.TopDegreeFiniteType.isFiniteType_of_forall_moduleFinite_sections
            (chartRestrictionSheaf B S hS X F A)
            (moduleFinite_sections_chartRestrictionSheaf B S hS X F hF hFft A)
        Scheme.Modules.schemeTheoreticSupport (chartRestrictionSheaf B S hS X F A) =
          idealSheafDataOfChart B S hS X
            (definingIdealSheaf B S hS X ⟨schemeTheoreticSupport B S hS X F, hZ⟩)
            (definingIdealSheaf_isCartesianOnAffineCharts B S hS X
              ⟨schemeTheoreticSupport B S hS X F, hZ⟩) A) ∧
      -- part (2)
      (∀ (G H : Modules.{u, u} B S hS
          (closedSubspaceToSpace B S hS X ⟨schemeTheoreticSupport B S hS X F, hZ⟩).1
          (closedSubspaceToSpace B S hS X ⟨schemeTheoreticSupport B S hS X F, hZ⟩).2)
        (eG : (modulePushforward B S hS (closedSubspaceInclusion B S hS X
          ⟨schemeTheoreticSupport B S hS X F, hZ⟩)).obj G ≅ F)
        (eH : (modulePushforward B S hS (closedSubspaceInclusion B S hS X
          ⟨schemeTheoreticSupport B S hS X F, hZ⟩)).obj H ≅ F),
        ∃! φ : G ≅ H, (modulePushforward B S hS (closedSubspaceInclusion B S hS X
          ⟨schemeTheoreticSupport B S hS X F, hZ⟩)).map φ.hom ≫ eH.hom = eG.hom) ∧
      -- part (3)
      (∀ (G : Modules.{u, u} B S hS
          (closedSubspaceToSpace B S hS X ⟨schemeTheoreticSupport B S hS X F, hZ⟩).1
          (closedSubspaceToSpace B S hS X ⟨schemeTheoreticSupport B S hS X F, hZ⟩).2),
        ((modulePushforward B S hS (closedSubspaceInclusion B S hS X
          ⟨schemeTheoreticSupport B S hS X F, hZ⟩)).obj G ≅ F) →
          SheafOfModules.IsFiniteTypeOnSite G) ∧
      -- part (4)
      supportOfSheaf B S hS X.1 ((SheafOfModules.toSheaf _).obj F) =
          Set.range (pointsMap B S hS (schemeTheoreticSupport B S hS X F).toFunctor
            (schemeTheoreticSupport B S hS X F).ι) ∧
      (∀ (G : Modules.{u, u} B S hS
          (closedSubspaceToSpace B S hS X ⟨schemeTheoreticSupport B S hS X F, hZ⟩).1
          (closedSubspaceToSpace B S hS X ⟨schemeTheoreticSupport B S hS X F, hZ⟩).2),
        ((modulePushforward B S hS (closedSubspaceInclusion B S hS X
          ⟨schemeTheoreticSupport B S hS X F, hZ⟩)).obj G ≅ F) →
          supportOfSheaf B S hS
            (closedSubspaceToSpace B S hS X ⟨schemeTheoreticSupport B S hS X F, hZ⟩).1
            ((SheafOfModules.toSheaf _).obj G) = Set.univ)

AlgebraicGeometry.Space.schemeTheoreticSupport_chartRestrictionSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SchemeTheoreticSupportChartComparison.lean, line 207. The attribute's comment: “part (1): on a scheme U étale over X the scheme-theoretic support of the restriction of F, in the sense of schemes, is the sheaf of ideals that the scheme-theoretic support of F cuts out on U”.

Stacks 07U0, part (1), with the support of the restriction taken in the sense of schemes. Let F be a finite type quasi-coherent 𝒪_X-module, let Z ⊆ X be its scheme-theoretic support and let A be an étale scheme chart of X — a scheme U with an étale morphism to X. Then the scheme-theoretic support of Stacks 05JV of the restriction of F to U is the sheaf of ideals that Z cuts out on U, that is, Z ×_X U.

Over an affine open V of U both sides are the annihilator of the sections of F over the étale chart V cuts out: the left-hand side by AlgebraicGeometry.Space.annihilator_sections_chartRestrictionSheaf and the right-hand side because the ideal cutting out the scheme-theoretic support is the annihilator ideal sheaf of F.

theorem schemeTheoreticSupport_chartRestrictionSheaf (F : Modules.{u, u} B S hS X.1 X.2)
    (hF : F.IsQuasicoherentOnSite) (hFft : SheafOfModules.IsFiniteTypeOnSite F)
    (Z : ClosedSubspaces B S hS X.1) (hZ : Z.1 = schemeTheoreticSupport B S hS X F)
    (A : SmallEtale B S hS X.1) :
    letI : (chartRestrictionSheaf B S hS X F A).IsQuasicoherent :=
      isQuasicoherent_chartRestrictionSheaf B S hS X F hF A
    letI : (chartRestrictionSheaf B S hS X F A).IsFiniteType :=
      Stacks.AlgebraicGeometry.TopDegreeFiniteType.isFiniteType_of_forall_moduleFinite_sections
        (chartRestrictionSheaf B S hS X F A)
        (moduleFinite_sections_chartRestrictionSheaf B S hS X F hF hFft A)
    Scheme.Modules.schemeTheoreticSupport (chartRestrictionSheaf B S hS X F A) =
      idealSheafDataOfChart B S hS X (definingIdealSheaf B S hS X Z)
        (definingIdealSheaf_isCartesianOnAffineCharts B S hS X Z) A

AlgebraicGeometry.Space.schemeTheoreticSupport_modulePullback_schemeSpace_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SchemeTheoreticSupportEtaleChart.lean, line 90. The attribute's comment: “part (1): on a scheme étale over X the scheme-theoretic support of the inverse image of F is the inverse image of the scheme-theoretic support of F”.

Stacks 07U0, part (1). Let F be a finite type quasi-coherent 𝒪_X-module with scheme-theoretic support Z ⊆ X, let U be a scheme over S and let φ : U → X be an étale morphism. Then the fibre product Z ×_X U is the scheme-theoretic support of φ^*F.

An étale morphism of algebraic spaces is flat (Stacks 0467, AlgebraicGeometry.Space.isFlat_of_isEtale), so this is Stacks 089C, AlgebraicGeometry.Space.schemeTheoreticSupport_modulePullback, at φ.

theorem schemeTheoreticSupport_modulePullback_schemeSpace_of_isEtale
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : F.IsQuasicoherentOnSite)
    (hft : PresheafOfModules.IsFiniteType (smallEtaleRingedSite B S hS X.1 X.2).J F.val)
    (U : BigFppfOver B S hS) (φ : schemeSpace U ⟶ X) (hφ : IsEtale B S hS φ.hom) :
    schemeTheoreticSupport B S hS (schemeSpace U) ((modulePullback B S hS φ).obj F) =
      (schemeTheoreticSupport B S hS X F).preimage φ.hom

AlgebraicGeometry.Space.supportOfSheaf_module_on_schemeTheoreticSupport_eq_univ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SchemeTheoreticSupportEtaleChart.lean, line 110. The attribute's comment: “part (4): the module on the scheme-theoretic support has support all of it”.

Stacks 07U0, part (4), for the module on the scheme-theoretic support. Let F be a finite type quasi-coherent 𝒪_X-module, let Z ⊆ X be its scheme-theoretic support and let G be an 𝒪_Z-module whose direct image along the inclusion is F. Then the support of G is all of |Z|.

G is of finite type by part (3), so the support of its direct image is the image of its support under the injective map on points of a closed immersion; that direct image is F, whose support is |Z| by the other half of part (4), AlgebraicGeometry.Space.supportOfSheaf_eq_range_pointsMap_schemeTheoreticSupport.

theorem supportOfSheaf_module_on_schemeTheoreticSupport_eq_univ
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : F.IsQuasicoherentOnSite)
    (hFft : SheafOfModules.IsFiniteTypeOnSite F) (Z : ClosedSubspaces B S hS X.1)
    (hZeq : Z.1 = schemeTheoreticSupport B S hS X F)
    (G : Modules.{u, u} B S hS (closedSubspaceToSpace B S hS X Z).1
      (closedSubspaceToSpace B S hS X Z).2)
    (e : (modulePushforward B S hS (closedSubspaceInclusion B S hS X Z)).obj G ≅ F) :
    supportOfSheaf B S hS (closedSubspaceToSpace B S hS X Z).1
      ((SheafOfModules.toSheaf _).obj G) = Set.univ
Tag 07U1, a definition

Tag 07U1 in the Stacks Project.

AlgebraicGeometry.Space.schemeTheoreticSupport, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SchemeTheoreticSupport.lean, line 398.

Stacks 07U1. The scheme theoretic support of a finite type quasi-coherent 𝒪_X-module F: the intersection of the closed subspaces of X whose defining ideal annihilates F.

By AlgebraicGeometry.Space.schemeTheoreticSupport_eq_of_definingIdealSheaf_eq this is the closed subspace cut out by the annihilator ideal sheaf of F, which for a quasi-coherent F of finite type is a quasi-coherent sheaf of ideals; so the intersection is itself a closed subspace and it is the smallest member of the family, which is the content of Stacks 07U0.

def schemeTheoreticSupport (F : Modules.{u, u} B S hS X.1 X.2) : Subfunctor X.1
Sources
LeanAlgebraicGeometry.Space.supp_restrictToChart_eq_preimage_supportOfSheaf · AlgebraicGeometry.Space.supp_restrictToChart_eq_preimage_supportOfSheaf_of_isQuasicoherent · AlgebraicGeometry.Space.nontrivial_geometricModuleStalk_iff_nontrivial_residueFibre · AlgebraicGeometry.Space.supportOfSheaf_modulePullback_eq · AlgebraicGeometry.Space.isClosed_supportOfSheaf_of_isFiniteTypeOnSite · AlgebraicGeometry.Space.supportOfSheaf_of_isQuasicoherentOnSite_isFiniteTypeOnSite · AlgebraicGeometry.Space.mem_supportOfSheaf_iff_nontrivial_geometricModuleStalk_of_liesOver · AlgebraicGeometry.Space.supportOfSheaf_eq_range_pointsMap_schemeTheoreticSupport

Section67.16 Scheme theoretic image#

Section 67.16 of the Stacks Project, Tag 082W. 7 tags here are carried by 17 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 082X, a lemma

Tag 082X in the Stacks Project.

AlgebraicGeometry.Space.schemeTheoreticImageSubfunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SchemeTheoreticImage.lean, line 155. The attribute's comment: “underlying subfunctor construction”.

Stacks 082X. The scheme-theoretic image of a morphism of algebraic spaces over S: the intersection of all closed subspaces of the target containing the image of the morphism.

def schemeTheoreticImageSubfunctor (f : X ⟶ Y) : Subfunctor Y

AlgebraicGeometry.Space.range_le_schemeTheoreticImageSubfunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SchemeTheoreticImage.lean, line 161. The attribute's comment: “the morphism factors through the image”.

Stacks 082X. A morphism of algebraic spaces over S factors through its scheme-theoretic image.

theorem range_le_schemeTheoreticImageSubfunctor (f : X ⟶ Y) :
    Subfunctor.range f ≤ schemeTheoreticImageSubfunctor B S hS f

AlgebraicGeometry.Space.schemeTheoreticImageSubfunctor_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SchemeTheoreticImage.lean, line 168. The attribute's comment: “minimality of the image”.

Stacks 082X. The scheme-theoretic image is contained in every closed subspace of the target through which the morphism factors.

theorem schemeTheoreticImageSubfunctor_le (f : X ⟶ Y) {Z : Subfunctor Y}
    (hZ : IsClosedSubspace B S hS Z) (hfZ : Subfunctor.range f ≤ Z) :
    schemeTheoreticImageSubfunctor B S hS f ≤ Z

AlgebraicGeometry.Space.isClosedSubspace_schemeTheoreticImageSubfunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SchemeTheoreticImage.lean, line 175. The attribute's comment: “the image is a closed subspace”.

Stacks 082X. The scheme-theoretic image is a closed subspace of the target.

theorem isClosedSubspace_schemeTheoreticImageSubfunctor (f : X ⟶ Y)
    (hY : IsAlgebraicSpace B S hS Y) :
    IsClosedSubspace B S hS (schemeTheoreticImageSubfunctor B S hS f)
Tag 082Y, a definition

Tag 082Y in the Stacks Project.

AlgebraicGeometry.Space.schemeTheoreticImageSubfunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SchemeTheoreticImage.lean, line 155. The attribute's comment: “the scheme-theoretic image”.

Stacks 082X. The scheme-theoretic image of a morphism of algebraic spaces over S: the intersection of all closed subspaces of the target containing the image of the morphism.

def schemeTheoreticImageSubfunctor (f : X ⟶ Y) : Subfunctor Y
Tag 082Z, a lemma

Tag 082Z in the Stacks Project.

AlgebraicGeometry.Space.schemeTheoreticImageSubfunctor_pullback_snd_of_isEtale_of_isQuasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/QuasiCompactImageEtaleLocal.lean, line 96. The attribute's comment: “part (3): compatibility with étale localization of the target”.

Stacks 082Z, part (3). The scheme-theoretic image of a quasi-compact morphism f : X ⟶ Y of algebraic spaces over S commutes with étale base change of the target: for g : V ⟶ Y étale, the scheme-theoretic image of X ×_Y V ⟶ V is the inverse image along g of the scheme-theoretic image of f.

Both sides are closed subspaces of V, hence are determined by their defining ideal sheaves, and on an étale scheme chart W of V both of those ideals are the kernel ideal of f on the chart g ∘ W of Y — by Stacks 082Z for the base change of f and for f itself.

theorem schemeTheoreticImageSubfunctor_pullback_snd_of_isEtale_of_isQuasiCompact
    (f : X ⟶ Y) (g : V ⟶ Y) (hf : IsQuasiCompact B S hS f.hom)
    (hg : IsEtale B S hS g.hom) :
    schemeTheoreticImageSubfunctor B S hS (pullback.snd f.hom g.hom) =
      (schemeTheoreticImageSubfunctor B S hS f.hom).preimage g.hom

AlgebraicGeometry.Space.definingIdealSheaf_schemeTheoreticImage_eq_kernelIdealSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/QuasiCompactImageIdeal.lean, line 126. The attribute's comment: “part (2): the image is the closed subspace cut out by that ideal”.

Stacks 082Z. For a quasi-compact morphism f : X ⟶ Y of algebraic spaces over S the scheme-theoretic image of f is the closed subspace of Y cut out by the kernel of the structure map f♯ : 𝒪_Y ⟶ f_*𝒪_X: its defining ideal sheaf of Stacks 03MB is that kernel.

theorem definingIdealSheaf_schemeTheoreticImage_eq_kernelIdealSheaf (f : X ⟶ Y)
    (hf : IsQuasiCompact B S hS f.hom) :
    definingIdealSheaf B S hS Y (schemeTheoreticImage B S hS f.hom Y.2) =
      kernelIdealSheaf B S hS f

AlgebraicGeometry.Space.range_pointsMap_ι_schemeTheoreticImage_eq_closure_of_isQuasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/QuasiCompactSchemeTheoreticImageDense.lean, line 54. The attribute's comment: “part (4): the image is dense in the scheme-theoretic image”.

Stacks 082Z, part (4). The set of points of the scheme-theoretic image of a quasi-compact morphism of algebraic spaces is the closure of the image of its point map.

theorem range_pointsMap_ι_schemeTheoreticImage_eq_closure_of_isQuasiCompact (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsQuasiCompact B S hS f) :
    Set.range (pointsMap B S hS (schemeTheoreticImageSubfunctor B S hS f).toFunctor
        (schemeTheoreticImageSubfunctor B S hS f).ι) =
      closure (Set.range (pointsMap B S hS X f))

AlgebraicGeometry.Space.denseRange_pointsMap_toSchemeTheoreticImage_of_isQuasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/QuasiCompactSchemeTheoreticImageDense.lean, line 68. The attribute's comment: “part (4): density of the image on points”.

Stacks 082Z, part (4), read inside the scheme-theoretic image: a quasi-compact morphism of algebraic spaces has dense image on the points of its scheme-theoretic image.

theorem denseRange_pointsMap_toSchemeTheoreticImage_of_isQuasiCompact (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsQuasiCompact B S hS f) :
    DenseRange (pointsMap B S hS X (toSchemeTheoreticImage B S hS f))

AlgebraicGeometry.Space.isQuasicoherentOnSite_kernelIdealSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactKernelQuasicoherent.lean, line 84. The attribute's comment: “part (1): the ideal sheaf of the image is quasi-coherent”.

The kernel of the structure map of a quasi-compact morphism of algebraic spaces is a quasi-coherent sheaf of ideals.

theorem isQuasicoherentOnSite_kernelIdealSheaf (f : X ⟶ Y)
    (hf : IsQuasiCompact B S hS f.hom) :
    (kernelIdealSheaf B S hS f).toSheafOfModules.IsQuasicoherentOnSite
Tag 0830, a lemma

Tag 0830 in the Stacks Project.

AlgebraicGeometry.Space.schemeTheoreticImageSubfunctor_eq_reducedClosedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SchemeTheoreticImage.lean, line 370. The attribute's comment: “part (1): the image is the reduced induced structure on the closure”.

Stacks 0830, part (1). The scheme-theoretic image of a morphism out of a reduced algebraic space is the reduced closed subspace supported on the closure of the image of its point map.

The identification itself is AlgebraicGeometry.Space.schemeTheoreticImageSubfunctor_eq_of_isReduced_of_range_pointsMap_eq, which needs no descent; what it has to be fed is that AlgebraicGeometry.Space.reducedClosedSubspace is a closed subspace, the existence half of Stacks 03IQ. That comes from AlgebraicGeometry.Space.isClosedSubspace_reducedClosedSubspace together with AlgebraicGeometry.Space.isEffectiveDescentAlongSurjectiveEtale_isClosedImmersion, effective descent for closed immersions along the surjective étale morphisms of the site.

theorem schemeTheoreticImageSubfunctor_eq_reducedClosedSubspace (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hXred : HasEtaleLocalProperty B S hS X (fun W : Scheme.{u} => IsReduced W)) :
    schemeTheoreticImageSubfunctor B S hS f =
      reducedClosedSubspace B S hS Y hY
        (closure (Set.range (pointsMap B S hS X f))) isClosed_closure

AlgebraicGeometry.Space.schemeTheoreticImageSubfunctor_pullback_snd_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SchemeTheoreticImage.lean, line 407. The attribute's comment: “part (2): compatibility with étale base change of the target”.

Stacks 0830, part (2). The scheme-theoretic image of a morphism out of a reduced algebraic space commutes with étale base change of the target: for an étale morphism g : V ⟶ Y, the scheme-theoretic image of X ×_Y V ⟶ V is the inverse image along g of the scheme-theoretic image of f.

By part (1) both sides are reduced closed subspaces, so it is enough to identify their point sets and appeal to the uniqueness half of Stacks 03IQ, AlgebraicGeometry.Space.eq_reducedClosedSubspace. The inverse image along g of the reduced closed subspace on the closure of the image of f is a closed subspace by Stacks 083Q, is étale-locally reduced because its projection to that subspace is a base change of g, hence étale, and has point set the preimage along |g| of that closure. That preimage is the closure of the image of X ×_Y V ⟶ V, because |g| is open by Stacks 03IR and the image of X ×_Y V ⟶ V is the preimage along |g| of the image of f by Stacks 03H4.

theorem schemeTheoreticImageSubfunctor_pullback_snd_of_isEtale
    {V : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y) (g : V ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hV : IsAlgebraicSpace B S hS V)
    (hXred : HasEtaleLocalProperty B S hS X (fun W : Scheme.{u} => IsReduced W))
    (hg : IsEtale B S hS g) :
    schemeTheoreticImageSubfunctor B S hS (pullback.snd f g) =
      (schemeTheoreticImageSubfunctor B S hS f).preimage g
Tag 089B, a lemma

Tag 089B in the Stacks Project.

AlgebraicGeometry.Space.exists_valuativeSquare_toSchemeTheoreticImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SchemeTheoreticImageValuativePoint.lean, line 188.

Let f : X ⟶ Y be a quasi-compact morphism of algebraic spaces over S, let Z be its scheme-theoretic image and let z be a point of |Z|. There is a valuation ring A with fraction field K, a morphism Spec K ⟶ X and a morphism Spec A ⟶ Z making the square over the canonical morphism X ⟶ Z commute, such that the closed point of Spec A maps to z.

theorem exists_valuativeSquare_toSchemeTheoreticImage (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsQuasiCompact B S hS f)
    (z : points B S hS (schemeTheoreticImageSubfunctor B S hS f).toFunctor) :
    ∃ (q : ValuativeSquare (toSchemeTheoreticImage B S hS f))
      (w : points B S hS (yoneda.obj (siteObject B S hS q.ring_mem q.base))),
      pointsToScheme B S hS (siteObject B S hS q.ring_mem q.base) w = closedPoint q.R ∧
        pointsMap B S hS (yoneda.obj (siteObject B S hS q.ring_mem q.base)) q.special w = z
Tag 0CP2, a lemma

Tag 0CP2 in the Stacks Project.

AlgebraicGeometry.Space.schemeTheoreticImageMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SchemeTheoreticImage.lean, line 235. The attribute's comment: “the induced morphism of scheme-theoretic images”.

Stacks 0CP2. The morphism of scheme-theoretic images induced by a commutative square of algebraic spaces over S.

def schemeTheoreticImageMap (hY₁ : IsAlgebraicSpace B S hS Y₁)
    (hY₂ : IsAlgebraicSpace B S hS Y₂) (hsq : f₁ ≫ q = p ≫ f₂) :
    (schemeTheoreticImageSubfunctor B S hS f₁).toFunctor ⟶
      (schemeTheoreticImageSubfunctor B S hS f₂).toFunctor

AlgebraicGeometry.Space.schemeTheoreticImageMap_ι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SchemeTheoreticImage.lean, line 245. The attribute's comment: “the right square”.

Stacks 0CP2, the right square: the induced morphism of scheme-theoretic images is compatible with their inclusions into the targets.

theorem schemeTheoreticImageMap_ι (hY₁ : IsAlgebraicSpace B S hS Y₁)
    (hY₂ : IsAlgebraicSpace B S hS Y₂) (hsq : f₁ ≫ q = p ≫ f₂) :
    schemeTheoreticImageMap B S hS hY₁ hY₂ hsq ≫
        (schemeTheoreticImageSubfunctor B S hS f₂).ι =
      (schemeTheoreticImageSubfunctor B S hS f₁).ι ≫ q

AlgebraicGeometry.Space.toSchemeTheoreticImage_comp_schemeTheoreticImageMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SchemeTheoreticImage.lean, line 269. The attribute's comment: “the left square”.

Stacks 0CP2, the left square: a morphism of scheme-theoretic images compatible with the inclusions into the targets is also compatible with the factorizations of the horizontal morphisms through their images.

theorem toSchemeTheoreticImage_comp_schemeTheoreticImageMap (hsq : f₁ ≫ q = p ≫ f₂)
    (h : (schemeTheoreticImageSubfunctor B S hS f₁).toFunctor ⟶
      (schemeTheoreticImageSubfunctor B S hS f₂).toFunctor)
    (hh : h ≫ (schemeTheoreticImageSubfunctor B S hS f₂).ι =
      (schemeTheoreticImageSubfunctor B S hS f₁).ι ≫ q) :
    toSchemeTheoreticImage B S hS f₁ ≫ h = p ≫ toSchemeTheoreticImage B S hS f₂
Tag 0CP3, a lemma

Tag 0CP3 in the Stacks Project.

AlgebraicGeometry.Space.isIso_pullback_snd_schemeTheoreticImageSubfunctor_comp_of_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SchemeTheoreticImagePartialSection.lean, line 137.

Stacks 0CP3. Let f : X ⟶ Y be a separated morphism of algebraic spaces over S, let V ⊆ Y be an open subspace whose inclusion into Y is quasi-compact, and let s : V ⟶ X satisfy s ≫ f = 𝟙 V. Let Y' be the scheme-theoretic image of s, a closed subspace of X, and let Y' ⟶ Y be its inclusion followed by f. Then Y' ⟶ Y is an isomorphism over V: the projection Y' ×_Y V ⟶ V of its base change along V ⟶ Y is an isomorphism.

theorem isIso_pullback_snd_schemeTheoreticImageSubfunctor_comp_of_section
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (hf : IsSeparated B S hS f)
    (V : Subfunctor Y) (hV : IsOpenSubspace B S hS V)
    (hVqc : IsQuasiCompact B S hS V.ι)
    (s : V.toFunctor ⟶ X) (hs : s ≫ f = V.ι) :
    IsIso (pullback.snd ((schemeTheoreticImageSubfunctor B S hS s).ι ≫ f) V.ι)
Sources
LeanAlgebraicGeometry.Space.schemeTheoreticImageSubfunctor · AlgebraicGeometry.Space.range_le_schemeTheoreticImageSubfunctor · AlgebraicGeometry.Space.schemeTheoreticImageSubfunctor_le · AlgebraicGeometry.Space.isClosedSubspace_schemeTheoreticImageSubfunctor · AlgebraicGeometry.Space.schemeTheoreticImageSubfunctor_pullback_snd_of_isEtale_of_isQuasiCompact · AlgebraicGeometry.Space.definingIdealSheaf_schemeTheoreticImage_eq_kernelIdealSheaf · AlgebraicGeometry.Space.range_pointsMap_ι_schemeTheoreticImage_eq_closure_of_isQuasiCompact · AlgebraicGeometry.Space.denseRange_pointsMap_toSchemeTheoreticImage_of_isQuasiCompact

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.