29.36 Unramified morphisms to 29.47 Universal homeomorphisms…
Section29.36 Unramified morphisms#
Section 29.36 of the Stacks Project, Tag 02G3. 17 tags here are carried by 46 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 02G4, a definition
Tag 02G4 in the Stacks Project.
AlgebraicGeometry.UnramifiedAt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Defs.lean, line 55. The attribute's comment: “part (1)”. References: SGA 3 XI (1.3); SGA 3 XI (1.5).
A morphism of schemes
f : X ⟶ Sis unramified atx : Xif there are affine open neighbourhoodsUofxandVof its image, withU ≤ f ⁻¹ᵁ V, such that the induced map on rings of sections is unramified.
public def UnramifiedAt {X S : Scheme.{u}} (f : X ⟶ S) (x : X) : Prop
AlgebraicGeometry.GUnramifiedAt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Defs.lean, line 65. The attribute's comment: “part (2)”. References: EGA IV (17.3.7), “unramified case”.
A morphism of schemes
f : X ⟶ Sis G-unramified atx : Xif there are affine open neighbourhoodsUofxandVof its image, withU ≤ f ⁻¹ᵁ V, such that the induced map on rings of sections is G-unramified.
public def GUnramifiedAt {X S : Scheme.{u}} (f : X ⟶ S) (x : X) : Prop
AlgebraicGeometry.Unramified, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Defs.lean, line 73. The attribute's comment: “part (3)”.
A morphism of schemes is unramified if it is unramified at every point of its source.
public class Unramified {X S : Scheme.{u}} (f : X ⟶ S) : Prop
AlgebraicGeometry.GUnramified, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Defs.lean, line 79. The attribute's comment: “part (4)”.
A morphism of schemes is G-unramified if it is G-unramified at every point of its source.
public class GUnramified {X S : Scheme.{u}} (f : X ⟶ S) : Prop
Tag 02G5, a lemma
Tag 02G5 in the Stacks Project.
AlgebraicGeometry.unramified_iff_locallyOfFiniteType_and_isZero_relativeDifferentials, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Differentials.lean, line 96. The attribute's comment: “part (1)”. References: EGA IV (17.4.1.2), “Omega = 0 criterion”; SGA 1 II (4.1), “S=Y, unramified clause”.
A morphism of schemes is unramified if and only if it is locally of finite type and its sheaf of relative differentials is zero.
theorem unramified_iff_locallyOfFiniteType_and_isZero_relativeDifferentials (f : X ⟶ S) :
Unramified f ↔
(LocallyOfFiniteType f ∧ IsZero (Scheme.Hom.relativeDifferentials f))
AlgebraicGeometry.gUnramified_iff_locallyOfFinitePresentation_and_isZero_relativeDifferentials, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Differentials.lean, line 106. The attribute's comment: “part (2)”.
A morphism of schemes is G-unramified if and only if it is locally of finite presentation and its sheaf of relative differentials is zero.
theorem gUnramified_iff_locallyOfFinitePresentation_and_isZero_relativeDifferentials
(f : X ⟶ S) :
GUnramified f ↔
(LocallyOfFinitePresentation f ∧ IsZero (Scheme.Hom.relativeDifferentials f))
Tag 02G6, a lemma
Tag 02G6 in the Stacks Project.
AlgebraicGeometry.unramified_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Local.lean, line 149. The attribute's comment: “unramified characterization”.
The four characterizations of an unramified morphism: the global condition, the condition on every compatible pair of affine opens, an open-covering criterion, and an affine-open-covering criterion on rings of sections.
public theorem unramified_tfae {X S : Scheme.{u}} (f : X ⟶ S) :
List.TFAE [
Unramified f,
∀ (U : X.Opens) (_ : IsAffineOpen U) (V : S.Opens) (_ : IsAffineOpen V)
(hUV : U ≤ f ⁻¹ᵁ V),
letI : Algebra Γ(S, V) Γ(X, U) := (f.appLE V U hUV).hom.toAlgebra
Algebra.Unramified Γ(S, V) Γ(X, U),
∃ (J : Type u) (V : J → S.Opens),
IsOpenCover V ∧
∀ j, ∃ (I : Type u) (U : I → X.Opens)
(hU : (⨆ i, U i) = f ⁻¹ᵁ V j),
∀ i, Unramified
(f.resLE (V j) (U i) ((le_iSup U i).trans hU.le)),
∃ (J : Type u) (V : J → S.Opens),
IsOpenCover V ∧
(∀ j, IsAffineOpen (V j)) ∧
∀ j, ∃ (I : Type u) (U : I → X.Opens)
(hU : (⨆ i, U i) = f ⁻¹ᵁ V j),
(∀ i, IsAffineOpen (U i)) ∧
∀ i,
let hUV : U i ≤ f ⁻¹ᵁ V j := (le_iSup U i).trans hU.le
letI : Algebra Γ(S, V j) Γ(X, U i) := (f.appLE (V j) (U i) hUV).hom.toAlgebra
Algebra.Unramified Γ(S, V j) Γ(X, U i)]
AlgebraicGeometry.gUnramified_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Local.lean, line 299. The attribute's comment: “G-unramified characterization”.
The four characterizations of a G-unramified morphism: the global condition, the condition on every compatible pair of affine opens, an open-covering criterion, and an affine-open-covering criterion on rings of sections.
public theorem gUnramified_tfae {X S : Scheme.{u}} (f : X ⟶ S) :
List.TFAE [
GUnramified f,
∀ (U : X.Opens) (_ : IsAffineOpen U) (V : S.Opens) (_ : IsAffineOpen V)
(hUV : U ≤ f ⁻¹ᵁ V),
letI : Algebra Γ(S, V) Γ(X, U) := (f.appLE V U hUV).hom.toAlgebra
Algebra.GUnramified Γ(S, V) Γ(X, U),
∃ (J : Type u) (V : J → S.Opens),
IsOpenCover V ∧
∀ j, ∃ (I : Type u) (U : I → X.Opens)
(hU : (⨆ i, U i) = f ⁻¹ᵁ V j),
∀ i, GUnramified
(f.resLE (V j) (U i) ((le_iSup U i).trans hU.le)),
∃ (J : Type u) (V : J → S.Opens),
IsOpenCover V ∧
(∀ j, IsAffineOpen (V j)) ∧
∀ j, ∃ (I : Type u) (U : I → X.Opens)
(hU : (⨆ i, U i) = f ⁻¹ᵁ V j),
(∀ i, IsAffineOpen (U i)) ∧
∀ i,
let hUV : U i ≤ f ⁻¹ᵁ V j := (le_iSup U i).trans hU.le
letI : Algebra Γ(S, V j) Γ(X, U i) := (f.appLE (V j) (U i) hUV).hom.toAlgebra
Algebra.GUnramified Γ(S, V j) Γ(X, U i)]
AlgebraicGeometry.unramified_resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Local.lean, line 375. The attribute's comment: “restriction of an unramified morphism”.
Restricting an unramified morphism to compatible open subschemes of its source and target is unramified.
public theorem unramified_resLE {X S : Scheme.{u}} {f : X ⟶ S}
(hf : Unramified f) (U : X.Opens) (V : S.Opens) (hUV : U ≤ f ⁻¹ᵁ V) :
Unramified (f.resLE V U hUV)
AlgebraicGeometry.gUnramified_resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Local.lean, line 388. The attribute's comment: “restriction of a G-unramified morphism”.
Restricting a G-unramified morphism to compatible open subschemes of its source and target is G-unramified.
public theorem gUnramified_resLE {X S : Scheme.{u}} {f : X ⟶ S}
(hf : GUnramified f) (U : X.Opens) (V : S.Opens) (hUV : U ≤ f ⁻¹ᵁ V) :
GUnramified (f.resLE V U hUV)
Tag 02G9, a lemma
Tag 02G9 in the Stacks Project.
AlgebraicGeometry.unramified_isStableUnderComposition, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Properties.lean, line 235. The attribute's comment: “unramified”. References: EGA IV (17.3.3), “(ii), special case”; SGA 1 I (3.5), “more general”.
Unramified morphisms of schemes are stable under composition.
public instance unramified_isStableUnderComposition :
MorphismProperty.IsStableUnderComposition (@Unramified.{u})
AlgebraicGeometry.gUnramified_isStableUnderComposition, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Properties.lean, line 243. The attribute's comment: “G-unramified”. References: EGA IV (17.3.3), “(ii)”; SGA 1 I (3.5), “more general”.
G-unramified morphisms of schemes are stable under composition.
public instance gUnramified_isStableUnderComposition :
MorphismProperty.IsStableUnderComposition (@GUnramified.{u})
Tag 02GA, a lemma
Tag 02GA in the Stacks Project.
AlgebraicGeometry.unramified_isStableUnderBaseChange, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Properties.lean, line 251. The attribute's comment: “unramified”. References: SGA 1 I (3.5), “(iii)”.
Unramified morphisms of schemes are stable under arbitrary base change.
public instance unramified_isStableUnderBaseChange :
MorphismProperty.IsStableUnderBaseChange
(fun {X S : Scheme.{u}} (f : X ⟶ S) ↦ Unramified f)
AlgebraicGeometry.gUnramified_isStableUnderBaseChange, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Properties.lean, line 260. The attribute's comment: “G-unramified”. References: SGA 1 I (3.5), “(iii)”.
G-unramified morphisms of schemes are stable under arbitrary base change.
public instance gUnramified_isStableUnderBaseChange :
MorphismProperty.IsStableUnderBaseChange
(fun {X S : Scheme.{u}} (f : X ⟶ S) ↦ GUnramified f)
Tag 04EV, a lemma
Tag 04EV in the Stacks Project.
AlgebraicGeometry.unramified_iff_gUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Noetherian.lean, line 39.
Over a locally Noetherian target, a morphism of schemes is unramified if and only if it is G-unramified.
theorem unramified_iff_gUnramified {X S : Scheme.{u}} (f : X ⟶ S) [IsLocallyNoetherian S] :
Unramified f ↔ GUnramified f
Tag 02GB, a lemma
Tag 02GB in the Stacks Project.
AlgebraicGeometry.gUnramified_of_isOpenImmersion, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/DifferentialsAndValuative/UnramifiedOpenImmersion.lean, line 32.
An open immersion of schemes is G-unramified.
public instance gUnramified_of_isOpenImmersion {X S : Scheme.{u}} (f : X ⟶ S)
[IsOpenImmersion f] : GUnramified f
Tag 02GC, a lemma
Tag 02GC in the Stacks Project.
AlgebraicGeometry.unramified_of_isClosedImmersion, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/ClosedImmersion.lean, line 48. The attribute's comment: “unramified”. References: EGA IV (17.3.3), “(i), special case”.
A closed immersion of schemes is unramified.
instance unramified_of_isClosedImmersion {Z X : Scheme.{u}} (i : Z ⟶ X)
[IsClosedImmersion i] : Unramified i
AlgebraicGeometry.gUnramified_iff_isFiniteType_idealSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/ClosedImmersion.lean, line 55. The attribute's comment: “G-unramified iff finite-type ideal sheaf”.
A closed immersion of schemes is G-unramified exactly when its ideal sheaf is of finite type.
theorem gUnramified_iff_isFiniteType_idealSheaf {Z X : Scheme.{u}} (i : Z ⟶ X)
[IsClosedImmersion i] :
GUnramified i ↔ (Stacks.ClosedImmersion.idealSheaf i.toLRSHom.toShHom).IsFiniteType
Tag 02GD, a lemma
Tag 02GD in the Stacks Project.
AlgebraicGeometry.unramified_iff_locallyOfFiniteType_and_isZero_relativeDifferentials, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Differentials.lean, line 96. The attribute's comment: “first sentence: an unramified morphism is locally of finite type”. References: EGA IV (17.4.1.2), “Omega = 0 criterion”; SGA 1 II (4.1), “S=Y, unramified clause”.
A morphism of schemes is unramified if and only if it is locally of finite type and its sheaf of relative differentials is zero.
theorem unramified_iff_locallyOfFiniteType_and_isZero_relativeDifferentials (f : X ⟶ S) :
Unramified f ↔
(LocallyOfFiniteType f ∧ IsZero (Scheme.Hom.relativeDifferentials f))
AlgebraicGeometry.gUnramified_iff_locallyOfFinitePresentation_and_isZero_relativeDifferentials, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Differentials.lean, line 106. The attribute's comment: “first sentence: an unramified morphism is locally of finite type”.
A morphism of schemes is G-unramified if and only if it is locally of finite presentation and its sheaf of relative differentials is zero.
theorem gUnramified_iff_locallyOfFinitePresentation_and_isZero_relativeDifferentials
(f : X ⟶ S) :
GUnramified f ↔
(LocallyOfFinitePresentation f ∧ IsZero (Scheme.Hom.relativeDifferentials f))
Tag 02V5, a lemma
Tag 02V5 in the Stacks Project.
AlgebraicGeometry.locallyOfFiniteType_of_unramified, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Properties.lean, line 99. The attribute's comment: “local finite-type part of the global consequence”.
An unramified morphism of schemes is locally of finite type.
public instance locallyOfFiniteType_of_unramified (f : X ⟶ S) [Unramified f] :
LocallyOfFiniteType f
AlgebraicGeometry.quasiFiniteAt_of_unramifiedAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Properties.lean, line 126. The attribute's comment: “the pointwise claim: unramified at x implies quasi-finite at x”.
Stacks Project, Tag 02V5, the pointwise claim. A morphism of schemes unramified at
xis quasi-finite atx. No hypothesis beyond unramifiedness at the point: the affine chart witnessing it carries an unramified, hence finite-type, map of sections, which is finite type at the point and makes the stalk map both essentially of finite type and formally unramified, and such an algebra is quasi-finite.
public theorem quasiFiniteAt_of_unramifiedAt (f : X ⟶ S) {x : X} (h : UnramifiedAt f x) :
quasiFiniteAt f x
AlgebraicGeometry.locallyQuasiFinite_of_unramified, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Properties.lean, line 159. The attribute's comment: “fiber-isolation part of the global consequence”. References: EGA IV (17.4.3).
The fibers of an unramified morphism are locally discrete.
public instance locallyQuasiFinite_of_unramified (f : X ⟶ S) [Unramified f] :
LocallyQuasiFinite f
Tag 02G7, a lemma
Tag 02G7 in the Stacks Project.
AlgebraicGeometry.unramified_iff_iso_coproduct_spectra_finite_separable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Fibers.lean, line 195. The attribute's comment: “part (1)”. References: EGA IV (17.15.11), “b) <=> c)”; SGA 3 XI (1.3), “(a)<=>(e) over field”.
Stacks Project, Tag 02G7, part (1). A morphism to the spectrum of a field is unramified if and only if its source is, over that spectrum, a coproduct of spectra of finite separable field extensions.
public theorem unramified_iff_iso_coproduct_spectra_finite_separable
(k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) :
Unramified f ↔
∃ (I : Type u) (K : I → Type u) (_ : ∀ i, Field (K i))
(_ : ∀ i, Algebra k (K i)) (_ : ∀ i, Module.Finite k (K i))
(_ : ∀ i, Algebra.IsSeparable k (K i))
(e : X ≅ ∐ fun i ↦ Spec (.of (K i))),
e.hom ≫ Sigma.desc (fun i ↦ Spec.map (CommRingCat.ofHom (algebraMap k (K i)))) = f
AlgebraicGeometry.Unramified.exists_iso_fiber_coproduct_spectra_finite_separable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Fibers.lean, line 270. The attribute's comment: “part (2)”. References: SGA 3 XI (1.3), “(a) => (e)”.
Stacks Project, Tag 02G7, part (2). Every fibre of an unramified morphism is, over the residue field of the base point, a coproduct of spectra of finite separable field extensions.
public theorem Unramified.exists_iso_fiber_coproduct_spectra_finite_separable
{X S : Scheme.{u}} (f : X ⟶ S) [Unramified f] (s : S) :
∃ (I : Type u) (K : I → Type u) (_ : ∀ i, Field (K i))
(_ : ∀ i, Algebra (S.residueField s) (K i))
(_ : ∀ i, Module.Finite (S.residueField s) (K i))
(_ : ∀ i, Algebra.IsSeparable (S.residueField s) (K i))
(e : f.fiber s ≅ ∐ fun i ↦ Spec (.of (K i))),
e.hom ≫ Sigma.desc (fun i ↦
Spec.map (CommRingCat.ofHom (algebraMap (S.residueField s) (K i)))) =
f.fiberToSpecResidueField s
Tag 02G8, a lemma
Tag 02G8 in the Stacks Project.
AlgebraicGeometry.unramified_of_fibres, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/FiberCriterion.lean, line 100. The attribute's comment: “part (2): a morphism locally of finite type all of whose fibres are disjoint unions of spectra of finite separable extensions of the residue field of the base point is unramified”. References: EGA IV (17.4.2), “Implication d′ ⇒ a”; SGA 3 XI (1.3), “(i)(e)⇒(a)”.
A morphism locally of finite type whose fibres are disjoint unions of spectra of finite separable extensions of the corresponding residue fields is unramified.
public theorem unramified_of_fibres {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
(h : ∀ s : S,
∃ (I : Type u) (K : I → Type u) (_ : ∀ i, Field (K i))
(_ : ∀ i, Algebra (S.residueField s) (K i))
(_ : ∀ i, Module.Finite (S.residueField s) (K i))
(_ : ∀ i, Algebra.IsSeparable (S.residueField s) (K i))
(e : f.fiber s ≅ ∐ fun i ↦ Spec (.of (K i))),
e.hom ≫ Sigma.desc (fun i ↦
Spec.map (CommRingCat.ofHom (algebraMap (S.residueField s) (K i)))) =
f.fiberToSpecResidueField s) :
Unramified f
AlgebraicGeometry.gUnramified_of_fibres, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/FiberCriterion.lean, line 119. The attribute's comment: “part (3): a morphism locally of finite presentation all of whose fibres are disjoint unions of spectra of finite separable extensions of the residue field of the base point is G-unramified”. References: EGA IV (17.4.2), “Implication d′ ⇒ a”; SGA 3 XI (1.3), “(i)(e)⇒(a)”.
A morphism locally of finite presentation whose fibres are disjoint unions of spectra of finite separable extensions of the corresponding residue fields is G-unramified.
public theorem gUnramified_of_fibres {X S : Scheme.{u}} (f : X ⟶ S)
[LocallyOfFinitePresentation f]
(h : ∀ s : S,
∃ (I : Type u) (K : I → Type u) (_ : ∀ i, Field (K i))
(_ : ∀ i, Algebra (S.residueField s) (K i))
(_ : ∀ i, Module.Finite (S.residueField s) (K i))
(_ : ∀ i, Algebra.IsSeparable (S.residueField s) (K i))
(e : f.fiber s ≅ ∐ fun i ↦ Spec (.of (K i))),
e.hom ≫ Sigma.desc (fun i ↦
Spec.map (CommRingCat.ofHom (algebraMap (S.residueField s) (K i)))) =
f.fiberToSpecResidueField s) :
GUnramified f
AlgebraicGeometry.finite_residueField_of_unramified, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Properties.lean, line 294. The attribute's comment: “finite_separable_residue”. References: EGA IV (17.4.1), “a) => d'' finiteness”; SGA 3 XI (1.3), “(ii) k(B)/k(A) finite”; SGA 1 I (3.1), “(ii)=>(i) finiteness”.
The residue field extension at a point of an unramified morphism is finite.
public instance finite_residueField_of_unramified (f : X ⟶ S) [Unramified f] (x : X) :
letI := (f.residueFieldMap x).hom.toAlgebra
Module.Finite (S.residueField (f x)) (X.residueField x)
AlgebraicGeometry.isSeparable_residueField_of_unramified, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Properties.lean, line 320. The attribute's comment: “finite_separable_residue”. References: EGA IV (17.4.1), “a) => d'' separability”; SGA 3 XI (1.3), “(ii) k(B)/k(A) separable”; SGA 1 I (3.1), “(ii)=>(i) separability”.
The residue field extension at a point of an unramified morphism is separable.
public instance isSeparable_residueField_of_unramified (f : X ⟶ S) [Unramified f] (x : X) :
letI := (f.residueFieldMap x).hom.toAlgebra
Algebra.IsSeparable (S.residueField (f x)) (X.residueField x)
Tag 02GE, a lemma
Tag 02GE in the Stacks Project.
AlgebraicGeometry.Unramified.isOpenImmersion_diagonal, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Diagonal.lean, line 43. The attribute's comment: “part (1)”. References: EGA IV (17.4.2), “a) ⇒ b)”; EGA IV (17.4.1), “a) => b)”; SGA 3 XI (1.3), “(a) => (b)”; SGA 1 I (3.4), “diagonal case (g = id)”; SGA 1 I (3.1), “(ii) => (iii)”.
The diagonal of an unramified morphism is an open immersion.
public instance isOpenImmersion_diagonal {X S : Scheme.{u}} (f : X ⟶ S) [Unramified f] :
IsOpenImmersion (pullback.diagonal f)
AlgebraicGeometry.Unramified.of_isOpenImmersion_diagonal, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Diagonal.lean, line 55. The attribute's comment: “part (2)”. References: EGA IV (17.4.2), “b) ⇒ a)”; EGA IV (17.4.1.2), “diagonal => unramified”; EGA IV (17.4.1), “b) => a)”; SGA 3 XI (1.3), “(b) => (a)”; SGA 1 I (3.1), “(iii) => (ii)”.
A morphism locally of finite type whose diagonal is an open immersion is unramified.
public instance of_isOpenImmersion_diagonal {X S : Scheme.{u}} (f : X ⟶ S)
[LocallyOfFiniteType f] [IsOpenImmersion (pullback.diagonal f)] :
Unramified f
AlgebraicGeometry.GUnramified.of_isOpenImmersion_diagonal, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Diagonal.lean, line 71. The attribute's comment: “part (3)”. References: EGA IV (17.4.2), “b) ⇒ a)”; EGA IV (17.4.1), “b) => a)”; SGA 3 XI (1.3), “(b) => (a)”; SGA 1 I (3.1), “(iii)=>(ii), fin pres”.
A morphism locally of finite presentation whose diagonal is an open immersion is G-unramified.
public instance of_isOpenImmersion_diagonal {X S : Scheme.{u}} (f : X ⟶ S)
[LocallyOfFinitePresentation f] [IsOpenImmersion (pullback.diagonal f)] :
GUnramified f
Tag 02GF, a lemma
Tag 02GF in the Stacks Project.
AlgebraicGeometry.unramifiedAt_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/AtPointCriteria.lean, line 220.
Stacks Project, Tag 02GF. For a morphism of schemes
f : X ⟶ Slocally of finite type and a pointxofXwith images = f x, the following are equivalent:fis unramified atx; the fibreX_sis unramified overκ(s)atx; the𝒪_{X,x}-moduleΩ_{X/S,x}is zero; the𝒪_{X_s,x}-moduleΩ_{X_s/s,x}is zero; theκ(x)-vector spaceΩ_{X_s/s,x} ⊗ κ(x) = Ω_{X/S,x} ⊗ κ(x)is zero, in either of its two canonically identified spellings; and𝔪_s 𝒪_{X,x} = 𝔪_xwithκ(x)/κ(s)finite separable.
public theorem unramifiedAt_tfae (f : X ⟶ S) [LocallyOfFiniteType f] (x : X) :
List.TFAE [
UnramifiedAt f x,
UnramifiedAt (f.fiberToSpecResidueField (f x)) (f.asFiber x),
Subsingleton (relativeDifferentialStalk f x),
Subsingleton (relativeDifferentialStalk (f.fiberToSpecResidueField (f x))
(f.asFiber x)),
Subsingleton (fiberRelativeCotangentSpace f x),
Subsingleton (relativeCotangentSpace f x),
Ideal.map (f.stalkMap x).hom
(IsLocalRing.maximalIdeal (S.presheaf.stalk (f x))) =
IsLocalRing.maximalIdeal (X.presheaf.stalk x) ∧
(letI := (f.residueFieldMap x).hom.toAlgebra
Module.Finite (S.residueField (f x)) (X.residueField x) ∧
Algebra.IsSeparable (S.residueField (f x)) (X.residueField x))]
AlgebraicGeometry.gUnramifiedAt_iff_unramifiedAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/GUnramifiedLocusBaseChange.lean, line 96. The attribute's comment: “the G-unramified reading of condition (1): for f locally of finite presentation, G-unramified at x is equivalent to unramified at x”.
Stacks Project, Tag 02GF, the G-unramified clause. A morphism of schemes locally of finite presentation is G-unramified at a point exactly when it is unramified there: the affine chart witnessing either notion witnesses the other, local finite presentation of the morphism supplying finite presentation of the map of sections.
public theorem gUnramifiedAt_iff_unramifiedAt (f : X ⟶ S) [LocallyOfFinitePresentation f]
(x : X) : GUnramifiedAt f x ↔ UnramifiedAt f x
AlgebraicGeometry.gUnramifiedAt_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/GUnramifiedLocusBaseChange.lean, line 116. The attribute's comment: “the resp. G-unramified reading, under local finite presentation; the unramified reading is AlgebraicGeometry.unramifiedAt_tfae”.
Stacks Project, Tag 02GF, the G-unramified reading. For a morphism of schemes
f : X ⟶ Slocally of finite presentation and a pointxofXwith images = f x, the following are equivalent:fis G-unramified atx;fis unramified atx; the fibreX_sis unramified overκ(s)atx; the𝒪_{X,x}-moduleΩ_{X/S,x}is zero; the𝒪_{X_s,x}-moduleΩ_{X_s/s,x}is zero; theκ(x)-vector spaceΩ_{X_s/s,x} ⊗ κ(x) = Ω_{X/S,x} ⊗ κ(x)is zero, in either of its two canonically identified spellings; and𝔪_s 𝒪_{X,x} = 𝔪_xwithκ(x)/κ(s)finite separable.
public theorem gUnramifiedAt_tfae (f : X ⟶ S) [LocallyOfFinitePresentation f] (x : X) :
List.TFAE [
GUnramifiedAt f x,
UnramifiedAt f x,
UnramifiedAt (f.fiberToSpecResidueField (f x)) (f.asFiber x),
Subsingleton (relativeDifferentialStalk f x),
Subsingleton (relativeDifferentialStalk (f.fiberToSpecResidueField (f x))
(f.asFiber x)),
Subsingleton (fiberRelativeCotangentSpace f x),
Subsingleton (relativeCotangentSpace f x),
Ideal.map (f.stalkMap x).hom
(IsLocalRing.maximalIdeal (S.presheaf.stalk (f x))) =
IsLocalRing.maximalIdeal (X.presheaf.stalk x) ∧
(letI := (f.residueFieldMap x).hom.toAlgebra
Module.Finite (S.residueField (f x)) (X.residueField x) ∧
Algebra.IsSeparable (S.residueField (f x)) (X.residueField x))]
Tag 0475, a lemma
Tag 0475 in the Stacks Project.
AlgebraicGeometry.unramifiedAt_iff_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/BaseChangeLocus.lean, line 115. The attribute's comment: “base change of the unramified locus”. References: SGA 1 I (3.5), “more general”.
Stacks Project, Tag 0475, the base-change half, pointwise. Let
be a cartesian diagram of schemes withX' → X ↓ ↓ Y' → Yf : X ⟶ Ylocally of finite type, and letf' : X' ⟶ Y'be the base change offalongg : Y' ⟶ Y. A pointx'ofX'is a point of unramifiedness off'if and only if its imageg' x'inXis a point of unramifiedness off.
theorem unramifiedAt_iff_of_isPullback {X' X Y' Y : Scheme.{u}}
{g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y}
(sq : IsPullback g' f' f g) [LocallyOfFiniteType f] (x' : X') :
UnramifiedAt f (g'.base x') ↔ UnramifiedAt f' x'
AlgebraicGeometry.setOf_unramifiedAt_fiber_eq_setOf_unramifiedAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/GUnramifiedLocusBaseChange.lean, line 157. The attribute's comment: “the two descriptions of T agree, locally-of-finite-type reading”. References: EGA IV (17.4.1), “more general”; EGA IV (17.8.1), “case Y = S”; SGA 1 I (5.8), “Net clause, special case”; SGA 3 VIB (2.7), “(iii) ⇔ (iv)”.
Stacks Project, Tag 0475, the equality of the two descriptions of
T. For a morphism of schemes locally of finite type, the set of points at which the scheme-theoretic fibre is unramified over the residue field of its image is the set of points at which the morphism itself is unramified.
public theorem setOf_unramifiedAt_fiber_eq_setOf_unramifiedAt (f : X ⟶ S)
[LocallyOfFiniteType f] :
{x : X | UnramifiedAt (f.fiberToSpecResidueField (f x)) (f.asFiber x)} =
{x : X | UnramifiedAt f x}
AlgebraicGeometry.setOf_unramifiedAt_fiber_eq_setOf_gUnramifiedAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/GUnramifiedLocusBaseChange.lean, line 174. The attribute's comment: “the two descriptions of T agree in the locally-of-finite-presentation reading, identifying T with the G-unramified locus”. References: EGA IV (17.4.1); EGA IV (17.8.1), “case Y = S”; SGA 1 I (5.8), “Net clause, special case”; SGA 3 VIB (2.7), “(iii) ⇔ (iv)”.
Stacks Project, Tag 0475, the equality of the two descriptions of
T, G-unramified reading. For a morphism of schemes locally of finite presentation, the set of points at which the scheme-theoretic fibre is unramified over the residue field of its image is the set of points at which the morphism itself is G-unramified. Hence that set is the open G-unramified locus, which is what makes the second half of the tag follow from the first.
public theorem setOf_unramifiedAt_fiber_eq_setOf_gUnramifiedAt (f : X ⟶ S)
[LocallyOfFinitePresentation f] :
{x : X | UnramifiedAt (f.fiberToSpecResidueField (f x)) (f.asFiber x)} =
{x : X | GUnramifiedAt f x}
AlgebraicGeometry.setOf_unramifiedAt_eq_preimage_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/GUnramifiedLocusBaseChange.lean, line 195. The attribute's comment: “T' = (g')⁻¹ T in set form, for the unramified locus”. References: EGA IV (17.7.2), “more general”.
Stacks Project, Tag 0475, the base-change half in set form. Let
be a cartesian diagram of schemes withX' → X ↓ ↓ S' → Sf : X ⟶ Slocally of finite type andf' : X' ⟶ S'the base change offalongg : S' ⟶ S. Then the unramified locusT'off'is the inverse image underg' : X' ⟶ Xof the unramified locusToff.
public theorem setOf_unramifiedAt_eq_preimage_of_isPullback {X' X S' S : Scheme.{u}}
{g' : X' ⟶ X} {f' : X' ⟶ S'} {f : X ⟶ S} {g : S' ⟶ S}
(sq : IsPullback g' f' f g) [LocallyOfFiniteType f] :
{x' : X' | UnramifiedAt f' x'} = g'.base ⁻¹' {x : X | UnramifiedAt f x}
AlgebraicGeometry.gUnramifiedAt_iff_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/GUnramifiedLocusBaseChange.lean, line 214. The attribute's comment: “base change of the G-unramified locus, pointwise”. References: SGA 1 I (3.5), “more general”; SGA 3 XI (1.3), “more general”.
Stacks Project, Tag 0475, the base-change half for the G-unramified locus, pointwise. Let
be a cartesian diagram of schemes withX' → X ↓ ↓ S' → Sf : X ⟶ Slocally of finite presentation andf' : X' ⟶ S'the base change offalongg : S' ⟶ S. A pointx'ofX'is a point of G-unramifiedness off'if and only if its imageg' x'inXis a point of G-unramifiedness off.
public theorem gUnramifiedAt_iff_of_isPullback {X' X S' S : Scheme.{u}}
{g' : X' ⟶ X} {f' : X' ⟶ S'} {f : X ⟶ S} {g : S' ⟶ S}
(sq : IsPullback g' f' f g) [LocallyOfFinitePresentation f] (x' : X') :
GUnramifiedAt f (g'.base x') ↔ GUnramifiedAt f' x'
AlgebraicGeometry.setOf_gUnramifiedAt_eq_preimage_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/GUnramifiedLocusBaseChange.lean, line 228. The attribute's comment: “T' = (g')⁻¹ T in set form, for the G-unramified locus, under local finite presentation”.
Stacks Project, Tag 0475, the second half in set form. For a cartesian diagram of schemes with
f : X ⟶ Slocally of finite presentation, the G-unramified locus of the base changef' : X' ⟶ S'is the inverse image underg' : X' ⟶ Xof the G-unramified locus off.
public theorem setOf_gUnramifiedAt_eq_preimage_of_isPullback {X' X S' S : Scheme.{u}}
{g' : X' ⟶ X} {f' : X' ⟶ S'} {f : X ⟶ S} {g : S' ⟶ S}
(sq : IsPullback g' f' f g) [LocallyOfFinitePresentation f] :
{x' : X' | GUnramifiedAt f' x'} = g'.base ⁻¹' {x : X | GUnramifiedAt f x}
AlgebraicGeometry.isOpen_setOf_unramifiedAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/OpenLocus.lean, line 66. The attribute's comment: “openness of the unramified locus”. References: SGA 1 I (3.3).
Stacks Project, Tag 0475. The locus where a morphism of schemes is unramified is open.
theorem isOpen_setOf_unramifiedAt (f : X ⟶ Y) : IsOpen {x : X | UnramifiedAt f x}
AlgebraicGeometry.isOpen_setOf_gUnramifiedAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/OpenLocus.lean, line 74. The attribute's comment: “openness of the G-unramified locus”. References: SGA 1 I (3.3), “loc. finite presentation”.
Stacks Project, Tag 0475. The locus where a morphism of schemes is G-unramified is open.
theorem isOpen_setOf_gUnramifiedAt (f : X ⟶ Y) : IsOpen {x : X | GUnramifiedAt f x}
Tag 02GG, a lemma
Tag 02GG in the Stacks Project.
AlgebraicGeometry.unramified_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Properties.lean, line 269. The attribute's comment: “part (1)”. References: SGA 1 I (3.6), “(v)”.
If the composite
X ⟶ Y ⟶ Sis unramified, thenX ⟶ Yis unramified.
public theorem unramified_of_comp {X Y S : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ S)
[Unramified (f ≫ g)] : Unramified f
AlgebraicGeometry.gUnramified_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Properties.lean, line 281. The attribute's comment: “part (2): carries the hypothesis that g is locally of finite type”.
If the composite
X ⟶ Y ⟶ Sis G-unramified andY ⟶ Sis locally of finite type, thenX ⟶ Yis G-unramified.
public theorem gUnramified_of_comp {X Y S : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ S)
[GUnramified (f ≫ g)] [LocallyOfFiniteType g] : GUnramified f
Tag 04HB, a lemma
Tag 04HB in the Stacks Project.
AlgebraicGeometry.exists_open_eq_of_residueFieldMap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/DifferentialsAndValuative/UnramifiedLocalEquality.lean, line 62. References: EGA IV (17.4.7), “open nbhd U, f|U=g|U”.
Two morphisms over
Sto a scheme unramified overSwhich have the same value and induce the same residue-field map atxagree on an open neighbourhood ofx.
public theorem exists_open_eq_of_residueFieldMap_eq {S : Scheme.{u}} {X Y : Over S}
(f g : X ⟶ Y) (x : X.left) [Unramified Y.hom]
(hfg : f.left x = g.left x)
(hκ : f.left.residueFieldMap x =
(Y.left.residueFieldCongr hfg).hom ≫ g.left.residueFieldMap x) :
∃ U : X.left.Opens, x ∈ U ∧ U.ι ≫ f.left = U.ι ≫ g.left
Sources
Section29.37 Étale morphisms#
Section 29.37 of the Stacks Project, Tag 02GH. 20 tags here are carried by 21 declarations of the repository (all in StacksFrontier) and 7 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 02GI, a definition
Tag 02GI in the Stacks Project.
AlgebraicGeometry.EtaleAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/Defs.lean, line 59. The attribute's comment: “etale_at_point”. References: SGA 1 IX (1.1).
A morphism of schemes is étale at
xif it induces an étale map on the coordinate rings of some affine open neighbourhood ofxand some affine open neighbourhood of its image.
public abbrev EtaleAt (f : X ⟶ S) (x : X) : Prop
AlgebraicGeometry.IsStandardEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/StandardEtale.lean, line 59. The attribute's comment: “standard_etale_morphism”.
A morphism of affine schemes is standard étale if its map on global sections is a standard étale ring map.
public abbrev IsStandardEtale {X S : Scheme.{u}} [IsAffine X] [IsAffine S]
(f : X ⟶ S) : Prop
Declarations registered for the tag:
AlgebraicGeometry.Etaleregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Morphisms/Etale/Defs.lean, line 53 (StacksFrontier): “etale_morphism”. References: EGA IV (17.3.1); SGA 1 I (4.1); SGA 3 XI (1.1); SGA 3 XI (1.6); SGA 4 VII (1.1).
Tag 02GJ, a lemma
Tag 02GJ in the Stacks Project.
AlgebraicGeometry.etale_resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/LocalCharacterization.lean, line 52. The attribute's comment: “moreover: restriction to open subschemes”.
If
fis étale then so is its restrictionU → Vto any opensU ⊆ X,V ⊆ Swithf(U) ⊆ V.
theorem etale_resLE {f : X ⟶ S} (hf : Etale f) (U : X.Opens) (V : S.Opens)
(e : U ≤ f ⁻¹ᵁ V) : Etale (f.resLE V U e)
AlgebraicGeometry.etale_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/LocalCharacterization.lean, line 60. The attribute's comment: “equivalence of (1), (2), (3) and (4)”.
Étaleness of a morphism of schemes can be checked on all pairs of affine opens, on open coverings of the target and of the preimages of their members, or on affine such coverings.
theorem etale_tfae (f : X ⟶ S) :
List.TFAE [
Etale f,
∀ (U : X.affineOpens) (V : S.affineOpens) (e : U.1 ≤ f ⁻¹ᵁ V.1),
(f.appLE V U e).hom.Etale,
∃ (J : Type u) (V : J → S.Opens) (I : J → Type u) (U : ∀ j, I j → X.Opens),
⨆ j, V j = ⊤ ∧ (∀ j, ⨆ i, U j i = f ⁻¹ᵁ V j) ∧
∀ j i, ∃ e : U j i ≤ f ⁻¹ᵁ V j, Etale (f.resLE (V j) (U j i) e),
∃ (J : Type u) (V : J → S.affineOpens) (I : J → Type u) (U : ∀ j, I j → X.affineOpens),
⨆ j, (V j).1 = ⊤ ∧ (∀ j, ⨆ i, (U j i).1 = f ⁻¹ᵁ (V j).1) ∧
∀ j i, ∃ e : (U j i).1 ≤ f ⁻¹ᵁ (V j).1, (f.appLE (V j) (U j i) e).hom.Etale]
AlgebraicGeometry.etale_tfae_and_resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/LocalCharacterization.lean, line 110.
The whole statement: the four characterizations of étaleness agree, and étaleness passes to restrictions to open subschemes.
theorem etale_tfae_and_resLE (f : X ⟶ S) :
List.TFAE [
Etale f,
∀ (U : X.affineOpens) (V : S.affineOpens) (e : U.1 ≤ f ⁻¹ᵁ V.1),
(f.appLE V U e).hom.Etale,
∃ (J : Type u) (V : J → S.Opens) (I : J → Type u) (U : ∀ j, I j → X.Opens),
⨆ j, V j = ⊤ ∧ (∀ j, ⨆ i, U j i = f ⁻¹ᵁ V j) ∧
∀ j i, ∃ e : U j i ≤ f ⁻¹ᵁ V j, Etale (f.resLE (V j) (U j i) e),
∃ (J : Type u) (V : J → S.affineOpens) (I : J → Type u) (U : ∀ j, I j → X.affineOpens),
⨆ j, (V j).1 = ⊤ ∧ (∀ j, ⨆ i, (U j i).1 = f ⁻¹ᵁ (V j).1) ∧
∀ j i, ∃ e : (U j i).1 ≤ f ⁻¹ᵁ (V j).1, (f.appLE (V j) (U j i) e).hom.Etale] ∧
(Etale f → ∀ (U : X.Opens) (V : S.Opens) (e : U ≤ f ⁻¹ᵁ V), Etale (f.resLE V U e))
Tag 02GN, a lemma
Tag 02GN in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.Etale.etale_compregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 165 (StacksFrontier). References: EGA IV (17.3.3), “(ii), étale case”; EGA IV (17.3.5), “étale clause”; SGA 1 I (4.6); SGA 1 V (3.3), “special case”.
Tag 02GO, a lemma
Tag 02GO in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.Etale.etale_isStableUnderBaseChangeregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 166 (StacksFrontier). References: EGA IV (17.3.3), “(iii), étale case”; EGA IV (17.7.3), “(ii)”; SGA 1 I (4.6); SGA 1 IX (1.3); SGA 1 IX (4.2), “Étaleness of X₁' → S₁'”; SGA 3 VIB (10.1), “partial”; SGA 3 VIB (2.1.2), “partial”; SGA 3 VIIB (1.6.C), “special case”; SGA 4 VII (1.4), “partial”; SGA 4½ Arcata (2.1.3).
Tag 02GK, a lemma
Tag 02GK in the Stacks Project.
AlgebraicGeometry.etaleAt_iff_smoothAt_and_unramifiedAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/Basic.lean, line 116. References: EGA IV (17.6.2), “more general”; SGA 3 XI (1.4), “more general”.
A morphism of schemes is étale at a point if and only if it is smooth and unramified at that point.
public theorem etaleAt_iff_smoothAt_and_unramifiedAt {X S : Scheme.{u}}
(f : X ⟶ S) (x : X) :
EtaleAt f x ↔
(InfinitesimalLifting.SmoothAt f x ∧ UnramifiedAt f x)
AlgebraicGeometry.Space.isEtaleAt_iff_isSmoothAt_and_isUnramifiedAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleAtPointCriteria.lean, line 177. The attribute's comment: “for algebraic spaces, at a point”.
A morphism of algebraic spaces over
Sis étale at a point of its source if and only if it is smooth and unramified at that point.
theorem isEtaleAt_iff_isSmoothAt_and_isUnramifiedAt
(hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
(x : points B S hS X) :
IsEtaleAt B S hS f x ↔ IsSmoothAt B S hS f x ∧ IsUnramifiedAt B S hS f x
Tag 03WS, a lemma
Tag 03WS in the Stacks Project.
AlgebraicGeometry.locallyQuasiFinite_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germs/EtaleQuasiFinite.lean, line 54.
An étale morphism of schemes is locally quasi-finite.
theorem locallyQuasiFinite_of_etale {X S : Scheme.{u}} (f : X ⟶ S) [Etale f] :
LocallyOfFiniteType f ∧ LocallyQuasiFinite f
Tag 02GL, a lemma
Tag 02GL in the Stacks Project.
AlgebraicGeometry.Etale.exists_iso_fiber_coproduct_spectra_finite_separable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/OverField.lean, line 111. The attribute's comment: “part (2)”. References: EGA IV (17.6.2), “a) => c')”.
Stacks Project, Tag 02GL, part (2). Every fibre of an étale morphism is, over the residue field of the base point, a coproduct of spectra of finite separable field extensions.
public theorem Etale.exists_iso_fiber_coproduct_spectra_finite_separable
{X S : Scheme.{u}} (f : X ⟶ S) [Etale f] (s : S) :
∃ (I : Type u) (K : I → Type u) (_ : ∀ i, Field (K i))
(_ : ∀ i, Algebra (S.residueField s) (K i))
(_ : ∀ i, Module.Finite (S.residueField s) (K i))
(_ : ∀ i, Algebra.IsSeparable (S.residueField s) (K i))
(e : f.fiber s ≅ ∐ fun i ↦ Spec (.of (K i))),
e.hom ≫ Sigma.desc (fun i ↦
Spec.map (CommRingCat.ofHom (algebraMap (S.residueField s) (K i)))) =
f.fiberToSpecResidueField s
Declarations registered for the tag:
AlgebraicGeometry.etale_iff_iso_coproduct_spectra_finite_separable, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Morphisms/Etale/OverField.lean, line 105 (StacksFrontier): “part (1)”.
Tag 02GM, a lemma
Tag 02GM in the Stacks Project.
AlgebraicGeometry.etale_of_flat_of_fibers_finite_separable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/FlatFibers.lean, line 55. References: EGA IV (17.6.2), “c') => a)”; EGA IV (18.2.3), “a') ⇒ a)”; SGA 1 IX (1.2), “converse direction”; SGA 4 VII (1.1), “flat+fibers => étale”.
A flat, locally finitely presented morphism with fibres that are disjoint unions of spectra of finite separable extensions of residue fields is étale.
public theorem etale_of_flat_of_fibers_finite_separable
{X S : Scheme.{u}} (f : X ⟶ S) [Flat f] [LocallyOfFinitePresentation f]
(h : ∀ s : S,
∃ (I : Type u) (K : I → Type u) (_ : ∀ i, Field (K i))
(_ : ∀ i, Algebra (S.residueField s) (K i))
(_ : ∀ i, Module.Finite (S.residueField s) (K i))
(_ : ∀ i, Algebra.IsSeparable (S.residueField s) (K i))
(e : f.fiber s ≅ ∐ fun i ↦ Spec (.of (K i))),
e.hom ≫ Sigma.desc (fun i ↦
Spec.map (CommRingCat.ofHom (algebraMap (S.residueField s) (K i)))) =
f.fiberToSpecResidueField s) :
Etale f
Tag 02GP, a lemma
Tag 02GP in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.Etale.instOfIsOpenImmersionregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Morphisms/Etale/OpenImmersionCriterion.lean, line 49 (StacksFrontier). References: EGA IV (17.1.3), “more general”; EGA IV (17.3.3); EGA IV (17.9.1), “(a) ⇒ étaleness in (c)”; SGA 1 I (4.6); SGA 1 I (5.1), “necessity”; SGA 1 IX (1.4), “Necessity”.
Tag 02GQ, a lemma
Tag 02GQ in the Stacks Project.
AlgebraicGeometry.syntomic_of_etale, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Syntomic/Etale.lean, line 59.
An étale morphism of schemes is syntomic.
lemma syntomic_of_etale {X S : Scheme.{u}} (f : X ⟶ S) [Etale f] : Syntomic f
Tag 02GR, a lemma
Tag 02GR in the Stacks Project.
AlgebraicGeometry.locallyOfFinitePresentation_of_etale, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Syntomic/Etale.lean, line 64.
An étale morphism of schemes is locally of finite presentation.
lemma locallyOfFinitePresentation_of_etale {X S : Scheme.{u}} (f : X ⟶ S) [Etale f] :
LocallyOfFinitePresentation f
Tag 02GS, a lemma
Tag 02GS in the Stacks Project.
AlgebraicGeometry.flat_of_etale, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Syntomic/Etale.lean, line 70.
An étale morphism of schemes is flat.
lemma flat_of_etale {X S : Scheme.{u}} (f : X ⟶ S) [Etale f] : Flat f
Tag 03WT, a lemma
Tag 03WT in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.UniversallyOpen.of_flatregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Morphisms/Etale/Open.lean, line 36 (StacksFrontier): “a flat morphism locally of finite presentation is universally open”. References: EGA IV (1.10.4), “b) ⇒ a), special case”; EGA IV (11.3.1), “special case”; EGA IV (14.4.10), “special case”; EGA IV (15.2.1); EGA IV (15.2.4), “(ii), special case”; EGA IV (18.2.7), “partial”; EGA IV (2.4.6); EGA IV (2.4.7), “more general”; EGA IV (4.4.1), “special case”; SGA 1 IV (6.6), “F = O_X”; SGA 1 VIII (4.9), “more general”; SGA 3 V (10.1.1), “more general”; SGA 3 V (4.1.1), “flat and fp implies open”; SGA 3 VIA (2.5.4), “Final implication”; SGA 3 VIB (3.11), “more general”; SGA 3 VIB (4.3); SGA 3 VIB (7.5), “f|_V is an open morphism”; SGA 3 X (5.4), “partial”; SGA 3 XVI (2.1), “more general”; SGA 6 VIII (1.3), “more general”.AlgebraicGeometry.Scheme.Hom.isOpenMapregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Morphisms/Etale/Open.lean, line 58 (StacksFrontier): “a universally open morphism is open on the underlying spaces”.
Tag 02GT, a lemma
Tag 02GT in the Stacks Project.
AlgebraicGeometry.etaleAt_iff_exists_isStandardEtale_restrict, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/StandardEtale.lean, line 143.
A scheme morphism is étale at a point if and only if, over any fixed affine open neighbourhood of its image, it is standard étale on some affine open neighbourhood of the point.
public lemma etaleAt_iff_exists_isStandardEtale_restrict
{X S : Scheme.{u}} (f : X ⟶ S) (x : X) (V : S.Opens)
(hV : IsAffineOpen V) (hxV : f x ∈ V) :
EtaleAt f x ↔
∃ (U : X.Opens) (hU : IsAffineOpen U) (_ : x ∈ U)
(hUV : U ≤ f ⁻¹ᵁ V),
@AlgebraicGeometry.IsStandardEtale
U.toScheme V.toScheme hU hV (f.resLE V U hUV)
Tag 02GU, a lemma
Tag 02GU in the Stacks Project.
AlgebraicGeometry.etaleAt_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/AtPointCriteria.lean, line 408. References: SGA 4½ Arcata (2.1.1), “b) <=> c)”.
Stacks Project, Tag 02GU. Ten equivalent criteria for a morphism of schemes locally of finite presentation to be étale at a point.
public theorem etaleAt_tfae {X S : Scheme.{u}} (f : X ⟶ S)
[LocallyOfFinitePresentation f] (x : X) :
List.TFAE [
EtaleAt f x,
(f.stalkMap x).hom.Flat ∧
EtaleAt (f.fiberToSpecResidueField (f x)) (f.asFiber x),
(f.stalkMap x).hom.Flat ∧
UnramifiedAt (f.fiberToSpecResidueField (f x)) (f.asFiber x),
(f.stalkMap x).hom.Flat ∧
Subsingleton (relativeDifferentialStalk f x),
(f.stalkMap x).hom.Flat ∧
Subsingleton (fiberRelativeCotangentSpace f x),
(f.stalkMap x).hom.Flat ∧
Subsingleton (relativeCotangentSpace f x),
(f.stalkMap x).hom.Flat ∧
(Ideal.map (f.stalkMap x).hom
(IsLocalRing.maximalIdeal (S.presheaf.stalk (f x))) =
IsLocalRing.maximalIdeal (X.presheaf.stalk x) ∧
(letI := (f.residueFieldMap x).hom.toAlgebra
Module.Finite (S.residueField (f x)) (X.residueField x) ∧
Algebra.IsSeparable (S.residueField (f x)) (X.residueField x))),
∃ (U : X.affineOpens) (V : S.affineOpens) (_ : x ∈ U.1)
(hUV : U.1 ≤ f ⁻¹ᵁ V.1),
letI : Algebra Γ(S, V.1) Γ(X, U.1) :=
(f.appLE V U hUV).hom.toAlgebra
Algebra.IsStandardSmoothOfRelativeDimension 0 Γ(S, V.1) Γ(X, U.1),
∃ (U : X.affineOpens) (V : S.affineOpens) (hxU : x ∈ U.1)
(hUV : U.1 ≤ f ⁻¹ᵁ V.1),
letI : Algebra Γ(S, V.1) Γ(X, U.1) :=
(f.appLE V U hUV).hom.toAlgebra
∃ (n : ℕ) (P : Algebra.PreSubmersivePresentation
Γ(S, V.1) Γ(X, U.1) (Fin n) (Fin n)),
P.jacobian ∉ (U.2.primeIdealOf ⟨x, hxU⟩).asIdeal,
∃ (U : X.affineOpens) (V : S.affineOpens) (_ : x ∈ U.1)
(hUV : U.1 ≤ f ⁻¹ᵁ V.1),
IsStandardEtale (f.resLE V.1 U.1 hUV),
∃ (U : X.affineOpens) (V : S.affineOpens) (hxU : x ∈ U.1)
(hUV : U.1 ≤ f ⁻¹ᵁ V.1)
(p q : Γ(S, V.1)[X]),
p.Monic ∧
∃ e : Γ(X, U.1) ≃+* StandardEtale.StandardEtaleAlg Γ(S, V.1) p q,
e.toRingHom.comp (f.appLE V U hUV).hom =
StandardEtale.standardEtaleMap Γ(S, V.1) p q ∧
e.symm ((Ideal.Quotient.mk
(Ideal.span {(algebraMap Γ(S, V.1)[X]
(Localization.Away q)) p}))
((algebraMap Γ(S, V.1)[X] (Localization.Away q))
(derivative p))) ∉
(U.2.primeIdealOf ⟨x, hxU⟩).asIdeal]
Tag 02GV, a lemma
Tag 02GV in the Stacks Project.
AlgebraicGeometry.etaleAt_iff_isFlatAt_and_gUnramifiedAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/DifferentialsAndValuative/EtaleFlatUnramified.lean, line 123. The attribute's comment: “at a point”. References: EGA IV (17.6.2), “more general”; SGA 3 XI (1.4), “more general”.
A morphism of schemes is étale at a point if and only if it is flat and G-unramified at that point.
public theorem etaleAt_iff_isFlatAt_and_gUnramifiedAt {X S : Scheme.{u}}
(f : X ⟶ S) (x : X) :
EtaleAt f x ↔
(IsFlatAt (LocallyRingedSpace.forgetToSheafedSpace.map f.toLRSHom) x ∧
GUnramifiedAt f x)
AlgebraicGeometry.etale_iff_flat_and_gUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/DifferentialsAndValuative/EtaleFlatUnramified.lean, line 132. The attribute's comment: “globally”. References: EGA IV (17.6.2); SGA 3 XI (1.4), “more general”.
A morphism of schemes is étale if and only if it is flat and G-unramified.
public theorem etale_iff_flat_and_gUnramified {X S : Scheme.{u}} (f : X ⟶ S) :
Etale f ↔ (Flat f ∧ GUnramified f)
Tag 0476, a lemma
Tag 0476 in the Stacks Project.
AlgebraicGeometry.setOf_etaleAt_eq_preimage_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/LocusBaseChange.lean, line 125. References: EGA IV (17.7.4), “(vi)”; EGA IV (17.7.1), “(ii) étale”.
Stacks Project, Tag 0476. Let
be a cartesian diagram of schemes, and letX' → X ↓ ↓ S' → SW ⊆ X, respectivelyW' ⊆ X', be the open subscheme of points wheref : X ⟶ S, respectively the base-changed morphismf' : X' ⟶ S', is étale. ThenW' = (g')⁻¹(W)providedfis locally of finite presentation and, in addition, eitherfis flat — the source's case (1) — org : S' ⟶ Sis flat — the source's case (2).
theorem setOf_etaleAt_eq_preimage_of_isPullback {f : X ⟶ S} {g : S' ⟶ S} {f' : X' ⟶ S'}
{g' : X' ⟶ X} [LocallyOfFinitePresentation f] (sq : IsPullback g' f' f g)
(hflat : Flat f ∨ Flat g) :
{x' : X' | EtaleAt f' x'} = g'.base ⁻¹' {x : X | EtaleAt f x}
Tag 02GW, a lemma
Tag 02GW in the Stacks Project.
AlgebraicGeometry.etale_of_etale_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/Cancellation.lean, line 46. References: SGA 4 VII (1.2).
Stacks Project, Tag 02GW. A morphism between two schemes that are étale over a common base, and which commutes with the structure morphisms, is étale.
theorem etale_of_etale_over {X Y S : Scheme.{u}} (f : X ⟶ Y) {p : X ⟶ S} {q : Y ⟶ S}
(h : f ≫ q = p) [Etale p] [Etale q] : Etale f
Tag 02K6, a lemma
Tag 02K6 in the Stacks Project.
Stacks.Etale.etale_of_comp_surjective_etale_of_locallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Descent.lean, line 156.
Stacks Project, Tag 02K6. If
f : X ⟶ Yis surjective and étale, the compositionf ≫ qis étale andq : Y ⟶ Sis locally of finite presentation, thenqis étale.
theorem etale_of_comp_surjective_etale_of_locallyOfFinitePresentation (f : X ⟶ Y) (q : Y ⟶ S)
[Surjective f] [Etale f] [Etale (f ≫ q)] [LocallyOfFinitePresentation q] :
Etale q
Tag 054L, a lemma
Tag 054L in the Stacks Project.
AlgebraicGeometry.exists_affine_open_etale_affineSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Smooth/EtaleAffineSpace.lean, line 100. References: EGA IV (17.11.4), “smooth ⇒ étale/A^d”.
A morphism of schemes which is smooth at a point is, over any affine open neighbourhood
Vof the image of that point, étale-locally an affine space overV: there is an affine open neighbourhoodUof the point mapping intoVand an étale morphism fromUto an affine space overVcommuting with the morphism.
theorem exists_affine_open_etale_affineSpace {X Y : Scheme.{u}} (f : X ⟶ Y) (x : X)
(V : Y.Opens) (hV : IsAffineOpen V) (hxV : x ∈ f ⁻¹ᵁ V)
(hf : InfinitesimalLifting.SmoothAt f x) :
∃ (d : ℕ) (U : X.Opens) (_ : IsAffineOpen U) (_ : x ∈ U) (hUV : U ≤ f ⁻¹ᵁ V)
(π : U.toScheme ⟶ AffineSpace (ULift.{u} (Fin d)) V.toScheme),
Etale π ∧
π ≫ (AffineSpace (ULift.{u} (Fin d)) V.toScheme ↘ V.toScheme) =
f.resLE V U hUV
Sources
Section29.38 Relatively ample sheaves#
Section 29.38 of the Stacks Project, Tag 01VG. 10 tags here are carried by 23 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 01VH, a definition
Tag 01VH in the Stacks Project.
Stacks.RelativeAmple.IsRelativelyAmple, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeAmple/Basic.lean, line 164. References: EGA II (4.6.1).
Stacks Tag 01VH. An invertible
𝒪_X-moduleLis ample relative tof : X ⟶ Swhenfis quasi-compact and, for every affine openVofS, the restriction ofLto the open subschemef⁻¹(V)is ample. The restriction is the module pullback along the open immersion off⁻¹(V), whose invertibility is Stacks Tag 0B8L, and ampleness is Stacks Tag 01PS.
def IsRelativelyAmple {X S : Scheme.{u}} (f : X ⟶ S) (L : X.Modules)
[Stacks.Ample.IsInvertibleModule X L] : Prop
Tag 02NN, a lemma
Tag 02NN in the Stacks Project.
AlgebraicGeometry.Scheme.Modules.isRelativelyAmple_iff_tensorPower_isRelativelyAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeAmple/TensorPower.lean, line 136. References: EGA II (4.6.9).
An invertible sheaf of modules on a scheme is ample relative to a morphism if and only if any one of its positive tensor powers is.
theorem isRelativelyAmple_iff_tensorPower_isRelativelyAmple
{X S : Scheme.{u}} (f : X ⟶ S) (L : X.Modules)
[AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 L]
(n : ℕ) (hn : 1 ≤ n) :
letI := Invertible.tensorPower_isInvertible X.presheaf X.ringCatSheaf.2 L (n : ℤ)
Stacks.RelativeAmple.IsRelativelyAmple f L ↔
Stacks.RelativeAmple.IsRelativelyAmple f
(Invertible.tensorPower X.presheaf X.ringCatSheaf.2 L (n : ℤ))
Tag 01VI, a lemma
Tag 01VI in the Stacks Project.
AlgebraicGeometry.Scheme.Modules.IsRelativelyAmple.isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativelyAmple/Separated.lean, line 41. References: EGA II (4.6.3).
A morphism of schemes admitting a relatively ample invertible sheaf is separated.
theorem IsRelativelyAmple.isSeparated {X S : Scheme.{u}} {f : X ⟶ S} {L : X.Modules}
[AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 L]
(hL : Stacks.RelativeAmple.IsRelativelyAmple f L) : IsSeparated f
Tag 01VJ, a lemma
Tag 01VJ in the Stacks Project.
Stacks.RelativeAmple.IsRelativelyAmple.quasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeAmple/GradedDirectImage.lean, line 125. The attribute's comment: “(5), the quasi-separatedness assertion: a morphism carrying a relatively ample invertible module is quasi-separated”.
Stacks Tag 01VJ, clause (5), the quasi-separatedness assertion. A morphism carrying a relatively ample invertible module is quasi-separated. It is in fact separated, which is [Stacks, Tag 01VI] and is
AlgebraicGeometry.Scheme.Modules.IsRelativelyAmple.isSeparated; a separated morphism is quasi-separated.
theorem IsRelativelyAmple.quasiSeparated {X S : Scheme.{u}} {f : X ⟶ S} {L : X.Modules}
[IsInvertibleModule X L] (hL : IsRelativelyAmple f L) : QuasiSeparated f
Stacks.RelativeAmple.isQuasicoherent_gradedDirectImage_of_isRelativelyAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeAmple/GradedDirectImage.lean, line 185. The attribute's comment: “(5), the homogeneous pieces of the graded algebra A = f_*(⨁_{d ≥ 0} L^{⊗ d}) of the clause: their quasi-coherence in nonnegative degree (the step the source attributes to Schemes 26.24.1) and their vanishing in negative degree. The graded algebra A itself, with its multiplication, is Stacks.RelativeAmple.directImageAlgebra; see the module docstring”.
The pieces of
𝒜in nonnegative degree are quasi-coherent, for a relatively ampleL: both hypotheses of [Stacks, Tag 01LC] are then available, quasi-compactness from [Stacks, Tag 01VH] and quasi-separatedness fromStacks.RelativeAmple.IsRelativelyAmple.quasiSeparated.
theorem isQuasicoherent_gradedDirectImage_of_isRelativelyAmple
(hL : IsRelativelyAmple f L) (d : ℕ) :
(gradedDirectImage f L (d : ℤ)).IsQuasicoherent
Stacks.RelativeAmple.iSup_nonvanishingOpenOn_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeAmple/GradedDirectImage.lean, line 219. The attribute's comment: “(5), the assertion U(psi) = X: for L ample relative to f, the nonvanishing opens of the positive-degree sections of A = f_*(⨁_{d ≥ 0} L^{⊗ d}) cover X”.
Stacks Tag 01VJ, clause (5), the assertion
U(ψ) = X. ForLample relative tof, the nonvanishing opens of the sections of positive degree of𝒜 = f_*(⨁_{d ≥ 0} L^{⊗ d})coverX.The supremum is over triples of an affine open
VofS, a degreed ≥ 1, and a section of𝒜_doverV;U(ψ)is the union of exactly these nonvanishing opens, since the degree-dcomponent of the adjunction mapψis the identity on sections overVundersections_gradedDirectImage. See the section "WhyU(ψ) = Xis the supremum below" of the module docstring.
theorem iSup_nonvanishingOpenOn_eq_top (hL : IsRelativelyAmple f L) :
(⨆ p : Σ' (V : S.Opens) (_ : IsAffineOpen V) (d : ℕ) (_ : 1 ≤ d),
Γ(gradedDirectImage f L (d : ℤ), V),
nonvanishingOpenOn (tensorPowModule X L (p.2.2.1 : ℤ)) (f ⁻¹ᵁ p.1) p.2.2.2.2) = ⊤
Stacks.RelativeAmpleLocalOnBase.isRelativelyAmple_of_forall_exists_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeAmple/LocalOnBase.lean, line 391. The attribute's comment: “(3) implies (1): relative ampleness may be checked on an affine open covering”. References: EGA II (4.6.4), “Sufficiency”; EGA II (8.10.6), “partial”.
Stacks Tag 01VJ, clause (3) implies clause (1). Let
f : X ⟶ Sbe a quasi-compact morphism of schemes andLan invertible𝒪_X-module. If every point ofShas an affine open neighbourhoodVwithL|_{f⁻¹V}ample, thenLis ample relative tof, that is,L|_{f⁻¹V}is ample for every affine openV ⊆ S.For an affine open
W ⊆ Sthe preimagef⁻¹Wis covered by the preimages of basic opens ofWlying inside members of the given covering, and on each of those the restriction ofLis ample by [Stacks, Tag 0B3E]; those preimages are the basic opens of the pullbacks tof⁻¹Wof the cutting functions, soStacks.RelativeAmpleLocalOnBase.isAmple_of_basicOpen_coverassembles them.
theorem isRelativelyAmple_of_forall_exists_isAmple {X S : Scheme.{u}} (f : X ⟶ S)
(L : X.Modules) [IsInvertibleModule X L] (hf : QuasiCompact f)
(hcov : ∀ x : S, ∃ V : S.Opens, IsAffineOpen V ∧ x ∈ V ∧
IsAmple (f ⁻¹ᵁ V).toScheme (Stacks.AmpleLocallyClosed.pullbackModule (f ⁻¹ᵁ V).ι L)) :
Stacks.RelativeAmple.IsRelativelyAmple f L
Stacks.RelativeAmpleLocalOnBase.exists_affine_isAmple_cover_of_isRelativelyAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeAmple/LocalOnBase.lean, line 440. The attribute's comment: “(1) implies (3): the affine opens of the base are such a covering”.
Stacks Tag 01VJ, clause (1) implies clause (3). A relatively ample module restricts to an ample module on the preimage of some affine open neighbourhood of every point of the base, because the affine opens of the base are a basis of its topology.
theorem exists_affine_isAmple_cover_of_isRelativelyAmple {X S : Scheme.{u}} (f : X ⟶ S)
(L : X.Modules) [IsInvertibleModule X L]
(hL : Stacks.RelativeAmple.IsRelativelyAmple f L) (x : S) :
∃ V : S.Opens, IsAffineOpen V ∧ x ∈ V ∧
IsAmple (f ⁻¹ᵁ V).toScheme (Stacks.AmpleLocallyClosed.pullbackModule (f ⁻¹ᵁ V).ι L)
Stacks.RelativeAmple.IsRelativelyAmple.isOpenImmersion_globalMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeAmple/ProjCharacterization.lean, line 271. The attribute's comment: “(1) implies (5), the assertion that r_{L,psi} is an open immersion”.
[Stacks, Tag 01VJ], (1) implies the open-immersion assertion of (5). For
Lample relative tof, with𝒜 = f_*(⨁_{d ≥ 0} L^{⊗ d})andψthe adjunction map, the morphismr_{L, ψ} : U(ψ) ⟶ Proj_S(𝒜)is an open immersion.
theorem IsRelativelyAmple.isOpenImmersion_globalMorphism (hL : IsRelativelyAmple f L) :
haveI := hL.quasiCompact
haveI := hL.quasiSeparated
IsOpenImmersion
((directImagePowerMap f L).globalMorphism (relativeProj (directImageAlgebra f L)))
Stacks.RelativeAmple.isRelativelyAmple_of_isImmersion_globalMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeAmple/ProjCharacterization.lean, line 305. The attribute's comment: “(6) implies (1)”.
[Stacks, Tag 01VJ], (6) implies (1). Let
fbe quasi-compact,𝒜a quasi-coherent graded𝒪_S-algebra andψ : f^*𝒜 ⟶ ⨁_{d ≥ 0} L^{⊗ d}a graded map withU(ψ) = Xsuch thatr_{L, ψ} : X ⟶ Proj_S(𝒜)is an immersion. ThenLis ample relative tof.Over an affine open
VofSthe morphism is an immersionf⁻¹V ⟶ Proj 𝒜(V)byglobalMorphism_iff, andisAmple_of_isImmersion_gluedgives ampleness ofL|_{f⁻¹V}.
theorem isRelativelyAmple_of_isImmersion_globalMorphism (hf : QuasiCompact f)
{A : SheafGradedAlgebra.{u} S} (P : GradedPowerMap A f) (e : P.L ≅ L)
(hU : P.coveringOpen = ⊤) (hP : IsImmersion (P.globalMorphism (relativeProj A))) :
IsRelativelyAmple f L
Stacks.RelativeAmple.isRelativelyAmple_of_isOpenImmersion_globalMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeAmple/ProjCharacterization.lean, line 325. The attribute's comment: “(4) implies (1)”.
[Stacks, Tag 01VJ], (4) implies (1): an open immersion is an immersion.
theorem isRelativelyAmple_of_isOpenImmersion_globalMorphism (hf : QuasiCompact f)
{A : SheafGradedAlgebra.{u} S} (P : GradedPowerMap A f) (e : P.L ≅ L)
(hU : P.coveringOpen = ⊤) (hP : IsOpenImmersion (P.globalMorphism (relativeProj A))) :
IsRelativelyAmple f L
Stacks.RelativeAmple.isRelativelyAmple_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeAmple/ProjCharacterization.lean, line 345.
[Stacks, Tag 01VJ]. For a quasi-compact morphism of schemes
f : X ⟶ Sand an invertible𝒪_X-moduleLthe following are equivalent:
Lis ample relative tof;- every point of
Shas an open neighbourhoodVwithL|_{f⁻¹V}ample relative tof ∣_ V : f⁻¹V ⟶ V;- every point of
Shas an affine open neighbourhoodVwithL|_{f⁻¹V}ample;- there are a quasi-coherent graded
𝒪_S-algebra𝒜and a graded mapψ : f^*𝒜 ⟶ ⨁_{d ≥ 0} L^{⊗ d}withU(ψ) = Xandr_{L, ψ} : U(ψ) ⟶ Proj_S(𝒜)an open immersion;fis quasi-separated and, for𝒜 = f_*(⨁_{d ≥ 0} L^{⊗ d})andψthe adjunction map,U(ψ) = Xandr_{L, ψ}is an open immersion;- as (4), with
r_{L, ψ}an immersion.
theorem isRelativelyAmple_tfae (f : X ⟶ S) (L : X.Modules)
[Stacks.Ample.IsInvertibleModule X L] [QuasiCompact f] :
List.TFAE [
IsRelativelyAmple f L,
∀ x : S, ∃ V : S.Opens, x ∈ V ∧
IsRelativelyAmple (f ∣_ V) (Stacks.AmpleLocallyClosed.pullbackModule (f ⁻¹ᵁ V).ι L),
∀ x : S, ∃ V : S.Opens, IsAffineOpen V ∧ x ∈ V ∧
Stacks.Ample.IsAmple (f ⁻¹ᵁ V).toScheme
(Stacks.AmpleLocallyClosed.pullbackModule (f ⁻¹ᵁ V).ι L),
∃ (A : SheafGradedAlgebra.{u} S) (P : GradedPowerMap A f), Nonempty (P.L ≅ L) ∧
P.coveringOpen = ⊤ ∧ IsOpenImmersion (P.globalMorphism (relativeProj A)),
∃ h : QuasiSeparated f,
haveI := h
(directImagePowerMap f L).coveringOpen = ⊤ ∧ IsOpenImmersion
((directImagePowerMap f L).globalMorphism (relativeProj (directImageAlgebra f L))),
∃ (A : SheafGradedAlgebra.{u} S) (P : GradedPowerMap A f), Nonempty (P.L ≅ L) ∧
P.coveringOpen = ⊤ ∧ IsImmersion (P.globalMorphism (relativeProj A))]
Stacks.RelativeAmpleRestrictBase.isRelativelyAmple_morphismRestrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeAmple/RestrictBase.lean, line 214. The attribute's comment: “(1) implies (2): relative ampleness is inherited by the restriction of the morphism over an arbitrary open of the base, so every open covering witnesses clause (2)”. References: EGA II (4.6.4), “Necessity”.
Stacks Tag 01VJ, clause (1) implies clause (2). If
Lis ample relative tof : X ⟶ Sthen, for every openV ⊆ S, the restrictionL|_{f⁻¹V}is ample relative to the restricted morphismf ∣_ V : f⁻¹V ⟶ V. In particular every open covering ofS— for instance the one-member covering{S}— witnesses clause (2) of [Stacks, Tag 01VJ].Quasi-compactness of
f ∣_ Vholds because quasi-compactness of a morphism is local on the target. For an affine openA ⊆ Vthe imageW = V.ι ''ᵁ Ais an affine open ofS, where clause (1) gives ampleness ofL|_{f⁻¹W}, andStacks.RelativeAmpleRestrictBase.isAmple_preimage_morphismRestrict_iffmoves it onto(f ∣_ V)⁻¹A.This also records that
Stacks.RelativeAmple.IsRelativelyAmplerestricts to an open of the base.
theorem isRelativelyAmple_morphismRestrict
(hL : Stacks.RelativeAmple.IsRelativelyAmple f L) (V : S.Opens) :
Stacks.RelativeAmple.IsRelativelyAmple (f ∣_ V) (pullbackModule (f ⁻¹ᵁ V).ι L)
Stacks.RelativeAmpleRestrictBase.isRelativelyAmple_of_forall_exists_isRelativelyAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeAmple/RestrictBase.lean, line 235. The attribute's comment: “(2) implies (1): relative ampleness over the members of an arbitrary open covering of the base implies relative ampleness”.
Stacks Tag 01VJ, clause (2) implies clause (1). Let
f : X ⟶ Sbe quasi-compact andLinvertible. If every point ofShas an open neighbourhoodVsuch thatL|_{f⁻¹V}is ample relative tof ∣_ V : f⁻¹V ⟶ V, thenLis ample relative tof.The affine opens of
Sare a basis, so eachVcontains an affine openWaround the given point, andV.ι⁻¹Wis then an affine open ofV. Relative ampleness overVgives ampleness on(f ∣_ V)⁻¹(V.ι⁻¹W), whichStacks.RelativeAmpleRestrictBase.isAmple_preimage_morphismRestrict_iffturns into ampleness ofL|_{f⁻¹W}. That is an affine open covering of the kindStacks.RelativeAmpleLocalOnBase.isRelativelyAmple_of_forall_exists_isAmple— clause (3) implies clause (1) — consumes.
theorem isRelativelyAmple_of_forall_exists_isRelativelyAmple (hf : QuasiCompact f)
(hcov : ∀ x : S, ∃ V : S.Opens, x ∈ V ∧ Stacks.RelativeAmple.IsRelativelyAmple (f ∣_ V)
(pullbackModule (f ⁻¹ᵁ V).ι L)) :
Stacks.RelativeAmple.IsRelativelyAmple f L
Tag 01VK, a lemma
Tag 01VK in the Stacks Project.
Stacks.RelativeAmpleAffineBase.isRelativelyAmple_iff_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeAmpleAffineBase/Basic.lean, line 167. References: EGA II (4.6.6).
Stacks Tag 01VK. Over an affine base, an invertible
𝒪_X-module is ample relative tof : X ⟶ Sif and only if it is ample onX.Both implications are
Stacks.AmplePullback.isAmple_modulePullback_of_isAffineHom, the unconditional case of Stacks Tag 0B3E for an affine morphism. Forwards, atV = ⊤: the hypothesis gives ampleness of the restriction ofLtof⁻¹(⊤) = ⊤, andStacks.RelativeAmpleAffineBase.isAmple_of_isAmple_modulePullbackdescends it along the isomorphism⊤ ⟶ X. Backwards: quasi-compactness offover an affine base is quasi-compactness ofX, and on each affine openVofSthe open immersion off⁻¹Vis an affine morphism byStacks.RelativeAmpleAffineBase.isAffineHom_preimage_ι.
theorem isRelativelyAmple_iff_isAmple {X S : Scheme.{u}} [IsAffine S] (f : X ⟶ S)
(L : X.Modules) [IsInvertibleModule X L] :
Stacks.RelativeAmple.IsRelativelyAmple f L ↔ IsAmple X L
Tag 0891, a lemma
Tag 0891 in the Stacks Project.
Stacks.RelativeAmple.isRelativelyAmple_unitModule_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeAmple/Basic.lean, line 212. References: EGA II (5.1.6), “(a) <=> (c')”.
Stacks Tag 0891. The structure sheaf
𝒪_Xis ample relative tof : X ⟶ Sif and only if the preimage underfof every affine open ofSis a quasi-affine scheme — that is, if and only iffis quasi-affine.The quasi-compactness clause of Tag 01VH is not an extra condition on the right-hand side: it follows from quasi-affineness of the affine preimages by
Stacks.RelativeAmple.quasiCompact_of_forall_isQuasiAffine_preimage. On each preimage the equivalence is Tag 01QE applied to(f ⁻¹ᵁ V).ι^* 𝒪_X, whichStacks.RelativeAmple.pullbackUnitModuleIsoidentifies with the structure sheaf of the open subscheme.
theorem isRelativelyAmple_unitModule_iff {X S : Scheme.{u}} (f : X ⟶ S) :
IsRelativelyAmple f (Stacks.Ample.unitModule X) ↔
∀ V : S.Opens, IsAffineOpen V → (f ⁻¹ᵁ V).toScheme.IsQuasiAffine
Tag 0892, a lemma
Tag 0892 in the Stacks Project.
Stacks.AmplePullbackDatum.exists_threshold_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmplePullbackDatum/Basic.lean, line 259. The attribute's comment: “part (1)”.
Part (1) of [Stacks, Tag 0892]. For
Lample relative tof : X ⟶ SandMan ample invertible𝒪_S-module there is a thresholdnwithL ⊗ f^* M ^⊗ aample onXfor everya ≥ n.
Stacks.AmplePullbackPart1.exists_threshold_isAmplewith both of its inputs discharged: quasi-compactness ofXbyStacks.AmplePullbackPart1.compactSpace_of_isAmple, and the pointwise datum byStacks.AmplePullbackDatum.eventualAffineDatum. The module isStacks.AmplePullbackPart1.tensorPullbackPowModule, that isL ⊗ f^* (M ^⊗ a).The tree's nearest previous statement of part (1),
Stacks.AmplePullback.exists_isAmple_tensorPullbackPow_of_iso_unitModule, assumes bothL ≅ 𝒪_XandM ≅ 𝒪_Sand carries no attribute; this statement assumes neither.
theorem exists_threshold_isAmple (hL : Stacks.RelativeAmple.IsRelativelyAmple f L)
(hM : IsAmple S M) :
∃ n : ℕ, ∀ a : ℕ, n ≤ a →
IsAmple X (Stacks.AmplePullbackPart1.tensorPullbackPowModule f L M a)
Stacks.SectionRatioNoAmple.isAmple_modulePullback_of_isQuasiAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRatioNoAmple/Pullback.lean, line 93. The attribute's comment: “part (2)”. References: EGA II (5.1.12), “absolute case”.
The pullback of an ample invertible module along a quasi-affine morphism is ample.
theorem isAmple_modulePullback_of_isQuasiAffineHom [IsQuasiAffineHom f] (hM : IsAmple S M) :
IsAmple X ((modulePullback f.toLRSHom.toShHom).obj M)
Tag 0C4K, a lemma
Tag 0C4K in the Stacks Project.
Stacks.AmplePullbackDatum.exists_threshold_isRelativelyAmple_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmplePullbackDatum/Composition.lean, line 125.
[Stacks, Tag 0C4K]. Let
f : X ⟶ Yandg : Y ⟶ Sbe morphisms of schemes,Lan invertible𝒪_X-module andMan invertible𝒪_Y-module. IfSis quasi-compact,Lis ample relative tofandMis ample relative tog, then there is a thresholdnbeyond whichL ⊗ f^* M ^⊗ ais ample relative tog ∘ f.
Stacks.RelativeAmpleCompositionThreshold.exists_threshold_isRelativelyAmple_compcarries the datum of [Stacks, Tag 01PW] over each affine open of the base as an explicit premise;Stacks.AmplePullbackDatum.relativeEventualAffineDatumdischarges it, so nothing is assumed here beyond the three hypotheses of the source.
theorem exists_threshold_isRelativelyAmple_comp [CompactSpace S]
(hL : Stacks.RelativeAmple.IsRelativelyAmple f L)
(hM : Stacks.RelativeAmple.IsRelativelyAmple g M) :
∃ n : ℕ, ∀ a : ℕ, n ≤ a → Stacks.RelativeAmple.IsRelativelyAmple (f ≫ g)
(tensorPullbackPowModule f L M a)
Stacks.RelativeAmpleCompositionThreshold.exists_threshold_isRelativelyAmple_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeAmple/CompositionThreshold.lean, line 217. The attribute's comment: “on Tag 01PW as EventualAffineDatum over each affine open of the base”.
Stacks Tag 0C4K, on the single premise
Stacks.RelativeAmpleCompositionThreshold.RelativeEventualAffineDatum— [Stacks, Tag 01PW] over each affine open of the base.Let
f : X ⟶ Yandg : Y ⟶ Sbe morphisms of schemes,Lan invertible𝒪_X-module andMan invertible𝒪_Y-module. IfSis quasi-compact,Lis ample relative tofandMis ample relative tog, then there is a thresholdnwithL ⊗ f^* M ^⊗ aample relative tog ∘ ffor everya ≥ n.Relative ampleness of
Land ofMsupplies quasi-compactness offand ofg, hence of the composite, so the preimage of an affine open ofSis quasi-compact andStacks.RelativeAmpleCompositionThreshold.exists_threshold_isAmple_preimageapplies over each of them. Quasi-compactness ofSextracts a finite subfamily of the affine opens so chosen, and the maximum of their thresholds serves for all of them at once; beyond it the finite family is an affine open covering ofSon whose preimages the restriction is ample, whichStacks.RelativeAmpleLocalOnBase.isRelativelyAmple_of_forall_exists_isAmple— [Stacks, Tag 01VJ], clause (3) implies clause (1) — upgrades to relative ampleness over every affine open ofS.
theorem exists_threshold_isRelativelyAmple_comp [CompactSpace S]
(hdat : RelativeEventualAffineDatum f g L M)
(hL : Stacks.RelativeAmple.IsRelativelyAmple f L)
(hM : Stacks.RelativeAmple.IsRelativelyAmple g M) :
∃ n : ℕ, ∀ a : ℕ, n ≤ a → Stacks.RelativeAmple.IsRelativelyAmple (f ≫ g)
(tensorPullbackPowModule f L M a)
Tag 0893, a lemma
Tag 0893 in the Stacks Project.
Stacks.AmpleBridge.isRelativelyAmple_pullbackModule_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleBridge/BaseChange.lean, line 111. The attribute's comment: “for an arbitrary cartesian square”.
If
Lis ample relative tof : X ⟶ Sand the square with sidesp : X' ⟶ X,f' : X' ⟶ S',fandg : S' ⟶ Sis cartesian, then the pullback ofLalongpis ample relative tof'.
theorem isRelativelyAmple_pullbackModule_of_isPullback {X S X' S' : Scheme.{u}} {p : X' ⟶ X}
{f' : X' ⟶ S'} {f : X ⟶ S} {g : S' ⟶ S} (hsq : IsPullback p f' f g) (L : X.Modules)
[Stacks.Ample.IsInvertibleModule X L]
(hL : Stacks.RelativeAmple.IsRelativelyAmple f L) :
Stacks.RelativeAmple.IsRelativelyAmple f' (pullbackModule p L)
Stacks.RelativeAmpleBaseChange.isRelativelyAmple_modulePullback_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeAmpleBaseChange/Basic.lean, line 262.
If
Lis ample relative tof : X ⟶ S, then its pullback toX ×_S S'is ample relative to the base changeX ×_S S' ⟶ S', for anyg : S' ⟶ S.
theorem isRelativelyAmple_modulePullback_unconditional
(hL : Stacks.RelativeAmple.IsRelativelyAmple f L) :
Stacks.RelativeAmple.IsRelativelyAmple (pullback.snd f g)
(Stacks.AmpleLocallyClosed.pullbackModule (pullback.fst f g) L)
Tag 0C4L, a lemma
Tag 0C4L in the Stacks Project.
Stacks.RelativeAmpleCompositionPermanence.isRelativelyAmple_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeAmple/CompositionPermanence.lean, line 68.
Stacks Tag 0C4L. Let
f : X ⟶ Yandg : Y ⟶ Sbe morphisms of schemes and letLbe an invertible𝒪_X-module. IfLis ample relative tog ∘ fandfis quasi-compact, thenLis ample relative tof.Through a point
y : Ychoose an affine openU ⊆ Scontainingg(y)and then, since the affine opens ofYare a basis, an affine openVwithy ∈ V ≤ g⁻¹U. On thatVthe restriction ofLis ample byStacks.RelativeAmpleComposition.isAmple_preimage_of_le_preimage. TheseVcoverY, andStacks.RelativeAmpleLocalOnBase.relativeAmpleLocalOnBase— [Stacks, Tag 01VJ], clause (3) implies clause (1) — upgrades them to every affine open ofY.
theorem isRelativelyAmple_of_comp {X Y S : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ S) (L : X.Modules)
[IsInvertibleModule X L] (hL : Stacks.RelativeAmple.IsRelativelyAmple (f ≫ g) L)
(hf : QuasiCompact f) :
Stacks.RelativeAmple.IsRelativelyAmple f L
Sources
Section29.39 Very ample sheaves#
Section 29.39 of the Stacks Project, Tag 01VL. 8 tags here are carried by 23 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 01VM, a definition
Tag 01VM in the Stacks Project.
Stacks.Tag01VMVeryAmple.IsRelativelyVeryAmple, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeVeryAmpleTwist/DegreeOne.lean, line 189. References: EGA II (4.4.2).
Stacks Tag 01VM: relative very ampleness. An invertible
𝒪_X-moduleLis very ample relative tof : X ⟶ Swhen there are a quasi-coherent𝒪_S-moduleEand an immersioni : X ⟶ 𝐏(E) = Proj_S(Sym(E))overSwithL ≅ i^* 𝒪_{𝐏(E)}(1).
def IsRelativelyVeryAmple {X : Scheme.{u}} (f : X ⟶ S) (L : X.Modules)
[IsInvertibleModule X L] : Prop
Tag 01VN, a lemma
Tag 01VN in the Stacks Project.
Stacks.RelativeAmple.isRelativelyAmple_of_isRelativelyVeryAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeAmple/VeryAmple.lean, line 67.
Stacks Tag 01VN (EGA II, Proposition 4.6.2). Let
f : X ⟶ Sbe a morphism of schemes andLan invertible𝒪_X-module. Iffis quasi-compact andLis very ample relative tof, thenLis ample relative tof.Relative very ampleness is [Stacks, Tag 01VM] at the named twist of the projective bundle: an immersion
i : X ⟶ 𝐏(E)overSinto the projective bundle of a quasi-coherent𝒪_S-moduleE, withL ≅ i^* 𝒪_{𝐏(E)}(1). Relative ampleness is [Stacks, Tag 01VH]: quasi-compactness offtogether with ampleness ofL|_{f⁻¹V}for every affine openV ⊆ S.
theorem isRelativelyAmple_of_isRelativelyVeryAmple {X S : Scheme.{u}} (f : X ⟶ S)
(L : X.Modules) [Stacks.Ample.IsInvertibleModule X L] (hf : QuasiCompact f)
(hL : Stacks.Tag01VMVeryAmple.IsRelativelyVeryAmple f L) :
IsRelativelyAmple f L
Tag 07ZR, an example
Tag 07ZR in the Stacks Project.
Stacks.Tag01VMRelativeVeryAmple.isClosedImmersion_canonicalSymProjHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeVeryAmpleTwist/CanonicalSymSurjective.lean, line 257. The attribute's comment: “the morphism X -> P(A_1) associated to the canonical map Sym(A_1) -> A is a closed immersion”.
Stacks Tag 07ZR: the morphism
Proj_S(𝒜) ⟶ 𝐏(𝒜_1)is a closed immersion, for𝒜generated by𝒜_1over𝒜_0, with no hypothesis on the graded-algebra map because the map is the canonical one.
theorem isClosedImmersion_canonicalSymProjHom : IsClosedImmersion (canonicalSymProjHom A hgen)
Stacks.Tag07ZRVeryAmple.isInvertibleModule_twistOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeVeryAmpleTwist/GeneratedInDegreeOne.lean, line 132. The attribute's comment: “O_X(1) is invertible”.
Stacks Tag 07ZR:
𝒪_X(1)is an invertible𝒪_X-module, forX = Proj_S(A)the relative homogeneous spectrum of a quasi-coherent graded𝒪_S-algebra generated byA_1overA_0.This is Stacks Tag 01O4 in a single degree:
𝒪_X(1)is the absolute twist𝒪(1)on each affine chart ofX, and the graded ring of sections over each affine open of the base is generated by its degree-one part, which trivializes that twist near every point.
theorem isInvertibleModule_twistOne (A : SheafGradedAlgebra S)
(hgen : ProjRepresentsF1.IsGeneratedInDegreeOne A) :
IsInvertibleModule (relativeProj A).scheme (twistOne A)
Stacks.Tag07ZRVeryAmple.twistOneIsoPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeVeryAmpleTwist/GeneratedInDegreeOne.lean, line 156. The attribute's comment: “the closed immersion X -> P(A_1) pulls back O_{P(A_1)}(1) to O_X(1)”.
Stacks Tag 07ZR: the closed immersion
X ⟶ 𝐏(A_1)pulls𝒪_{𝐏(A_1)}(1)back to𝒪_X(1). The closed immersion isStacks.Tag01VMRelativeVeryAmple.canonicalSymProjHom, the morphism of Stacks Tag 07ZG attached to the canonical mapSym(A_1) ⟶ Aread on all ofX, and the isomorphism is the inverse of the mapθ_1of Tag 07ZG, which is an isomorphism by Stacks Tag 07ZK (3).
def twistOneIsoPullback :
twistOne A ≅
(Scheme.Modules.pullback (canonicalSymProjHom A hgen)).obj
(Stacks.Tag01VMVeryAmple.twistOne (A.piece 1))
Stacks.Tag07ZRVeryAmple.isRelativelyVeryAmple_twistOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeVeryAmpleTwist/GeneratedInDegreeOne.lean, line 186. The attribute's comment: “O_X(1) is relatively very ample on X/S”. References: EGA II (4.4.3), “Case X = Proj_Y(S)”.
Stacks Tag 07ZR:
𝒪_X(1)is very ample relative toX ⟶ S, forX = Proj_S(A)the relative homogeneous spectrum of a quasi-coherent graded𝒪_S-algebra generated byA_1overA_0.Relative very ampleness is Stacks Tag 01VM,
Stacks.Tag01VMVeryAmple.IsRelativelyVeryAmple: the quasi-coherent module on the base isA_1, the immersion over the base is the closed immersionStacks.Tag01VMRelativeVeryAmple.canonicalSymProjHomattached to the canonical mapSym(A_1) ⟶ A, and the identification of𝒪_X(1)with its pullback of𝒪_{𝐏(A_1)}(1)isStacks.Tag07ZRVeryAmple.twistOneIsoPullback.
theorem isRelativelyVeryAmple_twistOne :
have := isInvertibleModule_twistOne A hgen
Stacks.Tag01VMVeryAmple.IsRelativelyVeryAmple (relativeProj A).toBase (twistOne A)
Tag 01VO, an example
Tag 01VO in the Stacks Project.
Stacks.ProjEvenPowerRoots.instGradedAlgebra, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjEvenPowerRoots.lean, line 157. The attribute's comment: “the graded algebra of the example”.
The graded-algebra structure on
A, the decomposition of the quotient by the homogeneous relation ideal.
public instance instGradedAlgebra : _root_.GradedAlgebra (grading k)
Stacks.ProjEvenPowerRoots.sup_basicOpen_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjEvenPowerRoots.lean, line 585. The attribute's comment: “the two-chart cover of the example”.
X = Proj Ais covered by the two standard opensD₊(U)andD₊(V).
public theorem sup_basicOpen_eq_top :
Proj.basicOpen (grading k) (uGen k) ⊔ Proj.basicOpen (grading k) (vGen k) = ⊤
Stacks.ProjEvenPowerRoots.isInvertible_twistingSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjEvenPowerRoots.lean, line 621. The attribute's comment: “invertibility of the twists on the example”.
Every twist
𝒪_X(n)is invertible, althoughAis not generated in degree one.
public theorem isInvertible_twistingSheaf (n : ℤ) :
AlgebraicGeometry.SheafOfModules.IsInvertible
(AlgebraicGeometry.Proj (grading k)).toRingedSpace.presheaf
(structureSheafRing (AlgebraicGeometry.Proj (grading k)).toRingedSpace).property
(twistingSheaf (grading k) n)
Stacks.ProjEvenPowerRoots.isIso_twistMultiplicationMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjEvenPowerRoots.lean, line 633. The attribute's comment: “the twists are tensor powers of the first twist”.
The multiplication
𝒪_X(n) ⊗ 𝒪_X(m) → 𝒪_X(n + m)is an isomorphism, so each𝒪_X(n)is then-th tensor power of𝒪_X(1).
public theorem isIso_twistMultiplicationMap (n m : ℤ) :
IsIso (twistMultiplicationMap (grading k) n m)
Stacks.ProjEvenPowerRoots.isAmple_twistingModule_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjEvenPowerRoots.lean, line 641. The attribute's comment: “the ample invertible sheaf on the example”.
𝒪_X(1)is an ample invertible sheaf onX = Proj A.
public theorem isAmple_twistingModule_one :
@AlgebraicGeometry.Scheme.Modules.IsAmple (AlgebraicGeometry.Proj (grading k))
(Stacks.ProjTwistSection.twistingModule (grading k) 1)
(isInvertible_twistingSheaf k 1)
Stacks.ProjEvenPowerRoots.not_isRelativelyVeryAmple_tensorPowModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjEvenPowerRoots.lean, line 1061. The attribute's comment: “no power of 𝒪_X(1) is f-relatively very ample”.
No power
𝒪_X(1)^{⊗ n}withn ≥ 1isf-relatively very ample, forf : X ⟶ Spec kthe structure morphism.
public theorem not_isRelativelyVeryAmple_tensorPowModule (n : ℕ) (hn : 1 ≤ n) :
letI := isInvertible_twistingSheaf k 1
¬ Stacks.Tag01VMVeryAmple.IsRelativelyVeryAmple (structureMorphism k)
(Stacks.Ample.tensorPowModule (AlgebraicGeometry.Proj (grading k))
(Stacks.ProjTwistSection.twistingModule (grading k) 1) (n : ℤ))
Stacks.ProjEvenPowerRoots.isRelativelyAmple_twistingModule_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjEvenPowerRoots.lean, line 1075. The attribute's comment: “𝒪_X(1) is f-ample”.
𝒪_X(1)isf-ample for the structure morphismf : X ⟶ Spec k.
public theorem isRelativelyAmple_twistingModule_one :
@Stacks.RelativeAmple.IsRelativelyAmple _ _ (structureMorphism k)
(Stacks.ProjTwistSection.twistingModule (grading k) 1) (isInvertible_twistingSheaf k 1)
Tag 01VP, an example
Tag 01VP in the Stacks Project.
Stacks.ProjHyperellipticDoubleCover.instGradedAlgebra, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjHyperellipticDoubleCover.lean, line 198. The attribute's comment: “the graded algebra of the example”.
The graded-algebra structure on
A_d. It is constructed: the relation ideal is homogeneous because the relation is weighted homogeneous, and the grading is the decomposition of the quotient by a homogeneous ideal.
public instance instGradedAlgebra : _root_.GradedAlgebra (grading k d lam)
Stacks.ProjHyperellipticDoubleCover.sup_basicOpen_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjHyperellipticDoubleCover.lean, line 265. The attribute's comment: “the two-chart cover of the example”.
X_d = Proj A_dis covered by the two standard opensD₊(U)andD₊(V). The three variables generateA_dover(A_d)₀ = k, so their standard opens cover, andD₊(Z)is contained in the union of the other two.
public theorem sup_basicOpen_eq_top (hd : 0 < d) :
Proj.basicOpen (grading k d lam) (uGen k d lam) ⊔
Proj.basicOpen (grading k d lam) (vGen k d lam) = ⊤
Stacks.ProjHyperellipticDoubleCover.isInvertible_twistingSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjHyperellipticDoubleCover.lean, line 307. The attribute's comment: “invertibility of the twists on the example”.
Every twist
𝒪_{X_d}(n)is invertible. Ford ≥ 2the algebraA_dis not generated in degree one, so this does not come from degree-one generation; the two-chart cover is what supplies it.
public theorem isInvertible_twistingSheaf (hd : 0 < d) (n : ℤ) :
AlgebraicGeometry.SheafOfModules.IsInvertible
(AlgebraicGeometry.Proj (grading k d lam)).toRingedSpace.presheaf
(structureSheafRing (AlgebraicGeometry.Proj (grading k d lam)).toRingedSpace).property
(twistingSheaf (grading k d lam) n)
Stacks.ProjHyperellipticDoubleCover.isIso_twistMultiplicationMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjHyperellipticDoubleCover.lean, line 319. The attribute's comment: “the twists are tensor powers of the first twist”.
The multiplication
𝒪_{X_d}(n) ⊗ 𝒪_{X_d}(m) → 𝒪_{X_d}(n + m)is an isomorphism, so each𝒪_{X_d}(n)is then-th tensor power of𝒪_{X_d}(1).
public theorem isIso_twistMultiplicationMap (hd : 0 < d) (n m : ℤ) :
IsIso (twistMultiplicationMap (grading k d lam) n m)
Stacks.ProjHyperellipticDoubleCover.isAmple_twistingModule_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjHyperellipticDoubleCover.lean, line 329. The attribute's comment: “the ample invertible sheaf on the example”.
𝒪_{X_d}(1)is an ample invertible sheaf onX_d = Proj A_d— the positive assertion of the example.X_dis quasi-compact and every point lies in the affine standard open of one of the degree-one elementsU,V.
public theorem isAmple_twistingModule_one (hd : 0 < d) :
@AlgebraicGeometry.Scheme.Modules.IsAmple (AlgebraicGeometry.Proj (grading k d lam))
(Stacks.ProjTwistSection.twistingModule (grading k d lam) 1)
(isInvertible_twistingSheaf k d lam hd 1)
Stacks.ProjHyperellipticDoubleCover.bijective_degreeSection_binaryForm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjHyperellipticDoubleCover.lean, line 748. The attribute's comment: “the global sections of the twists of degree less than d”.
[Stacks, Tag 01VP]:
Γ(X_d, 𝒪_{X_d}(n)) = k[U, V]_nfor0 ≤ n < d. The map sending a binary formpof degreento the global sectionp / 1of𝒪_{X_d}(n)is bijective.
public theorem bijective_degreeSection_binaryForm (hd : 0 < d) {n : ℕ} (hn : n < d) :
Function.Bijective fun p : homogeneousSubmodule (Fin 2) k n =>
AlgebraicGeometry.ProjectiveSpectrum.Proj.degreeSection (grading k d lam) n
⟨binaryForm k d lam p, binaryForm_mem k d lam ((mem_homogeneousSubmodule _ _).mp p.2)⟩
Stacks.ProjHyperellipticDoubleCover.le_of_isRelativelyVeryAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjHyperellipticDoubleCover.lean, line 1246. The attribute's comment: “very ampleness of a twist forces its degree to be at least d”.
[Stacks, Tag 01VP]: if
𝒪_{X_d}(n)is very ample, thenn ≥ d. Here very ample is relative to any morphism fromX_dto an affine scheme, the case of the structure morphismX_d → Spec kincluded.The proof is the source's. Very ampleness gives an immersion
α : X_d → 𝐏(E)with𝒪_{X_d}(n) ≅ α^* 𝒪(1), and over an affine base𝐏(E)is theProjof a graded ring generated in degree one. Forn < devery global section of𝒪(n)is a form inU,Valone near the branch point(λ₁ : 1 : 0)— this isΓ(X_d, 𝒪(n)) = k[U, V]_n— so the twok[ε]-pointsZ ↦ εandZ ↦ 0at the branch point, which agree onUandV, have the same image underα. An immersion is a monomorphism, and the two points are different.
public theorem le_of_isRelativelyVeryAmple (hd : 0 < d) {S : Scheme.{u}} [IsAffine S]
(f : AlgebraicGeometry.Proj (grading k d lam) ⟶ S) (n : ℤ)
(h : @Stacks.Tag01VMVeryAmple.IsRelativelyVeryAmple _ _ f
(Stacks.ProjTwistSection.twistingModule (grading k d lam) n)
(isInvertible_twistingSheaf k d lam hd n)) :
(d : ℤ) ≤ n
Tag 01VQ, a lemma
Tag 01VQ in the Stacks Project.
Stacks.Tag01VMRelativeVeryAmple.isSeparated_of_isRelativelyVeryAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeVeryAmpleTwist/Separated.lean, line 60. References: EGA II (4.4.2).
Stacks Tag 01VQ: a morphism admitting a relatively very ample invertible sheaf is separated.
Relative very ampleness gives an immersion
i : X ⟶ 𝐏(E)over the base. The structure morphism of𝐏(E) = relativeProj (symAlgebra E)is separated, an immersion is a monomorphism and hence separated, and separatedness is stable under composition; the composite isf.
public theorem isSeparated_of_isRelativelyVeryAmple {X S : Scheme.{u}} (f : X ⟶ S)
(L : X.Modules) [IsInvertibleModule X L] (hL : IsRelativelyVeryAmple f L) :
IsSeparated f
Tag 01VR, a lemma
Tag 01VR in the Stacks Project.
Stacks.Tag01VMVeryAmple.tfae_isRelativelyVeryAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeVeryAmpleTwist/LocalOnBase.lean, line 171. References: EGA II (4.4.5).
Stacks Tag 01VR. Let
f : X ⟶ Sbe a quasi-compact morphism of schemes andLan invertible𝒪_X-module. The following are equivalent:
Lis relatively very ample onX/S;- there is an open covering
S = ⋃ V_jsuch thatL|_{f⁻¹(V_j)}is relatively very ample onf⁻¹(V_j)/V_jfor allj;- there are a quasi-coherent graded
𝒪_S-algebraAgenerated in degree one and a map of graded algebrasψ : f^* A ⟶ ⨁_{n ≥ 0} L^{⊗ n}such thatf^* A_1 ⟶ Lis surjective and the associated morphismr_{L, ψ} : X ⟶ Proj_S(A)is an immersion;fis quasi-separated, the canonical mapf^* f_* L ⟶ Lis surjective and the associated morphismr_{L, ψ} : X ⟶ 𝐏(f_* L)is an immersion.
theorem tfae_isRelativelyVeryAmple (f : X ⟶ S) [QuasiCompact f] (L : X.Modules)
[IsInvertibleModule X L] :
List.TFAE [IsRelativelyVeryAmple f L, IsRelativelyVeryAmpleLocallyOnBase f L,
HasImmersionToRelativeProj f L, IsImmersionDirectImageBundle f L]
Tag 0B3F, a lemma
Tag 0B3F in the Stacks Project.
Stacks.Tag01VMVeryAmple.isRelativelyVeryAmple_pullback_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeVeryAmpleTwist/BaseChangeTwist.lean, line 113. References: EGA II (4.4.10); SGA 1 VIII (5.8), “Very ample clause”.
Stacks Tag 0B3F: relative very ampleness is preserved by base change. Let
f : X ⟶ Sbe a morphism of schemes,Lan invertible𝒪_X-module which is very ample relative tof, andg : S' ⟶ Sa morphism of schemes. Then the pullback ofLtoS' ×_S Xis very ample relative to the projectionS' ×_S X ⟶ S'.The proof is the source's. Relative very ampleness gives a quasi-coherent
𝒪_S-moduleE, an immersioni : X ⟶ 𝐏(E)overSand an isomorphismL ≅ i^* 𝒪_{𝐏(E)}(1). The moduleg^* Eis quasi-coherent (Tag 01BG), its projective bundle is the base change of𝐏(E)and the comparison morphismbpulls the twist back to the twist (Tag 01O3,Stacks.Tag01VMVeryAmple.projectiveBundleTwistBaseChange), so the morphismi'induced byS' ×_S X ⟶ X ⟶ 𝐏(E)andS' ×_S X ⟶ S'is a base change ofi, hence an immersion (Tag 01JY), it lies overS', and the pullback ofLisi'^* 𝒪_{𝐏(g^* E)}(1).
theorem isRelativelyVeryAmple_pullback_fst {X S' : Scheme.{u}} (f : X ⟶ S) (g : S' ⟶ S)
(L : X.Modules) [IsInvertibleModule X L] (hL : IsRelativelyVeryAmple f L) :
IsRelativelyVeryAmple (pullback.fst g f)
((Scheme.Modules.pullback (pullback.snd g f)).obj L)
Sources
Section29.40 Ample and very ample sheaves relative to finite type morphisms#
Section 29.40 of the Stacks Project, Tag 02NO. 8 tags here are carried by 20 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 02NP, a lemma
Tag 02NP in the Stacks Project.
Stacks.CoordinateImmersion.hasImmersionTwistOver_of_isRelativelyVeryAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/VeryAmpleAffineBase/CoordinateImmersion.lean, line 593. References: EGA II (5.3.3), “special case”.
Stacks Tag 02NP. A relatively very ample invertible sheaf on a scheme of finite type over an affine base is the hyperplane sheaf pulled back along an immersion into a finite-dimensional projective space over that base, lying over the base.
Finite type is the conjunction of local finiteness of type with quasi-compactness, and the conclusion is
Stacks.AmpleProjectiveImmersion.HasImmersionTwistOver, the source's conclusion written out.
Stacks.VeryAmpleAffineBase.hasImmersionTwistOver_of_isRelativelyVeryAmpleis the same statement on the hypothesisStacks.VeryAmpleAffineBase.ProjCoordinateCut, the coordinate-cutting step of the source's proof; that hypothesis is discharged byStacks.CoordinateImmersion.projCoordinateCut.
theorem hasImmersionTwistOver_of_isRelativelyVeryAmple {S X : Scheme.{u}} (f : X ⟶ S)
(L : X.Modules) [Stacks.Ample.IsInvertibleModule X L] [LocallyOfFiniteType f]
[QuasiCompact f] [IsAffine S]
(hL : Tag01VMVeryAmple.IsRelativelyVeryAmple f L) :
AmpleProjectiveImmersion.HasImmersionTwistOver f L
Tag 04II, a lemma
Tag 04II in the Stacks Project.
AlgebraicGeometry.exists_immersion_affineSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/ImmersionsAndAffine/AffineSpaceImmersion.lean, line 162.
Stacks Project, Tag 04II. A quasi-affine scheme locally of finite type over
Sadmits, overS, an immersion into a finite-dimensional relative affine space.
theorem exists_immersion_affineSpace
{X S : Scheme.{u}} (f : X ⟶ S) [X.IsQuasiAffine] [LocallyOfFiniteType f] :
∃ (n : ℕ) (i : X ⟶ AffineSpace (ULift.{u} (Fin n)) S),
IsImmersion i ∧ i ≫ (AffineSpace (ULift.{u} (Fin n)) S ↘ S) = f
Tag 01VS, a lemma
Tag 01VS in the Stacks Project.
Stacks.StalkwiseGeneration.exists_immersion_projectiveSpaceOver_of_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/StalkwiseGeneration/Ample.lean, line 81.
[Stacks, Tag 01VS]. For
f : X ⟶ Slocally of finite type andLan ample invertible𝒪_X-module there is ad₀ ≥ 1such that every degreed ≥ d₀admits an immersioni : X ⟶ ℙⁿ_SoverSpulling the twisting sheaf𝒪(1)back toL ^⊗ d.
theorem exists_immersion_projectiveSpaceOver_of_isAmple {S : Scheme.{u}} (f : X ⟶ S)
(L : X.Modules) [IsInvertibleModule X L] (hL : IsAmple X L) [LocallyOfFiniteType f] :
∃ d₀ : ℕ, 1 ≤ d₀ ∧ ∀ d : ℕ, d₀ ≤ d →
∃ (n : ℕ) (i : X ⟶ projectiveSpaceOver n S),
IsImmersion i ∧
i ≫ pullback.fst (terminal.from S)
(terminal.from (projectiveSpaceAtUniverse.{u} n)) = f ∧
Nonempty (tensorPowModule X L (d : ℤ) ≅
(Scheme.Modules.pullback i).obj (projectiveSpaceTwistingSheaf n S))
Tag 01VT, a lemma
Tag 01VT in the Stacks Project.
Stacks.AmpleRelativeFiniteType.tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleRelativeFiniteType/Basic.lean, line 151. The attribute's comment: “conditions (1), (2), (5) and (6) of the six; conditions (3) and (4), relative very ampleness, are stated together with these four by Stacks.AmpleRelativeFiniteType.tfae_six, and (5), (6) are taken with no lower bound on n, which Stacks.AmpleProjectiveImmersion.hasImmersionTwistOverPos_iff shows is the source's n ≥ 1 clause”.
[Stacks, Tag 01VT], conditions (1), (2), (5) and (6), unconditionally. For
f : X ⟶ Sof finite type withSaffine andLan invertible𝒪_X-module, the following are equivalent:
Lis ample onX;Lis ample relative tof;- (the source's (5))
L ^⊗ dis𝒪(1)pulled back along an immersionX ⟶ ℙⁿ_SoverS, for somed ≥ 1;- (the source's (6)) the same, for every sufficiently large
d.The cycle is (1) ⟹ (4) ⟹ (3) ⟹ (2) ⟹ (1). The first step is [Stacks, Tag 01VS] at the single situation
(X, S, f, L)— no covering of the base and no glueing, which is what affineness ofSbuys — the second is dropping the lower bound on the degree, the third is [Stacks, Tag 01VN] together with [Stacks, Tag 02NN], and the last two are the two halves of [Stacks, Tag 01VK].The source's conditions (3) and (4), relative very ampleness, are not among the four; they join them in
Stacks.AmpleRelativeFiniteType.tfae_six, in the sibling moduleStacksFrontier.AlgebraicGeometry.AmpleRelativeFiniteType.VeryAmple.
theorem tfae [IsAffine S] (f : X ⟶ S) (L : X.Modules) [IsInvertibleModule X L]
[LocallyOfFiniteType f] [QuasiCompact f] :
List.TFAE [
IsAmple X L,
Stacks.RelativeAmple.IsRelativelyAmple f L,
∃ d : ℕ, 1 ≤ d ∧ HasImmersionTwistOver f (tensorPowModule X L (d : ℤ)),
∃ d₀ : ℕ, 1 ≤ d₀ ∧ ∀ d : ℕ, d₀ ≤ d →
HasImmersionTwistOver f (tensorPowModule X L (d : ℤ))]
Stacks.AmpleRelativeFiniteType.tfae_six, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleRelativeFiniteType/VeryAmple.lean, line 190. The attribute's comment: “all six conditions, with no named input: ampleness, f-ampleness, relative very ampleness of some and of every sufficiently high tensor power, and the two immersion clauses; the immersion clauses are taken with no lower bound on the dimension n of the projective space, where the source writes n ≥ 1 — the two agree by Stacks.AmpleProjectiveImmersion.hasImmersionTwistOverPos_iff, and Stacks.AmpleRelativeFiniteType.tfae_six_pos is the list with the source's clauses”.
[Stacks, Tag 01VT], all six conditions, with no named input. For
f : X ⟶ Sof finite type withSaffine andLan invertible𝒪_X-module, the following are equivalent:
Lis ample onX;Lis ample relative tof;L ^⊗ dis very ample relative tof, for somed ≥ 1;L ^⊗ dis very ample relative tof, for every sufficiently larged;L ^⊗ dis𝒪(1)pulled back along an immersionX ⟶ ℙⁿ_SoverS, for somed ≥ 1;- the same, for every sufficiently large
d.The cycle is (1) ⟹ (6) ⟹ (4) ⟹ (3) ⟹ (2) ⟹ (1), with (5) attached to (1) in both directions. Only (6) ⟹ (4) uses the module half of [Stacks, Tag 01OE], which over an affine base is
Stacks.SymGraded.hasFreeBundleTwistOne; see the module documentation for the rest.Conditions (5) and (6) are taken with no lower bound on
n, as inStacks.AmpleRelativeFiniteType.tfae.
theorem tfae_six [IsAffine S]
(f : X ⟶ S) (L : X.Modules) [IsInvertibleModule X L] [LocallyOfFiniteType f]
[QuasiCompact f] :
List.TFAE [
IsAmple X L,
Stacks.RelativeAmple.IsRelativelyAmple f L,
∃ d : ℕ, 1 ≤ d ∧
Stacks.Tag01VMVeryAmple.IsRelativelyVeryAmple f (tensorPowModule X L (d : ℤ)),
∃ d₀ : ℕ, 1 ≤ d₀ ∧ ∀ d : ℕ, d₀ ≤ d →
Stacks.Tag01VMVeryAmple.IsRelativelyVeryAmple f (tensorPowModule X L (d : ℤ)),
∃ d : ℕ, 1 ≤ d ∧ HasImmersionTwistOver f (tensorPowModule X L (d : ℤ)),
∃ d₀ : ℕ, 1 ≤ d₀ ∧ ∀ d : ℕ, d₀ ≤ d →
HasImmersionTwistOver f (tensorPowModule X L (d : ℤ))]
Stacks.AmpleRelativeFiniteType.isAmple_iff_exists_isRelativelyVeryAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleRelativeFiniteType/VeryAmple.lean, line 224. The attribute's comment: “the equivalence of conditions (1) and (3): ampleness and relative very ampleness of some positive tensor power”.
The equivalence of (1) and (3) of [Stacks, Tag 01VT]:
Lis ample exactly when some tensor powerL ^⊗ dwithd ≥ 1is very ample relative tof.
theorem isAmple_iff_exists_isRelativelyVeryAmple [IsAffine S] (f : X ⟶ S)
(L : X.Modules) [IsInvertibleModule X L] [LocallyOfFiniteType f] [QuasiCompact f] :
IsAmple X L ↔ ∃ d : ℕ, 1 ≤ d ∧
Stacks.Tag01VMVeryAmple.IsRelativelyVeryAmple f (tensorPowModule X L (d : ℤ))
Stacks.AmpleRelativeFiniteType.isAmple_iff_eventually_isRelativelyVeryAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleRelativeFiniteType/VeryAmple.lean, line 234. The attribute's comment: “the equivalence of conditions (1) and (4): ampleness and relative very ampleness of every sufficiently high tensor power”. References: EGA II (4.5.10), “more general”.
The equivalence of (1) and (4) of [Stacks, Tag 01VT]:
Lis ample exactly when every sufficiently high tensor power ofLis very ample relative tof.
theorem isAmple_iff_eventually_isRelativelyVeryAmple [IsAffine S] (f : X ⟶ S)
(L : X.Modules) [IsInvertibleModule X L] [LocallyOfFiniteType f] [QuasiCompact f] :
IsAmple X L ↔ ∃ d₀ : ℕ, 1 ≤ d₀ ∧ ∀ d : ℕ, d₀ ≤ d →
Stacks.Tag01VMVeryAmple.IsRelativelyVeryAmple f (tensorPowModule X L (d : ℤ))
Stacks.AmpleRelativeFiniteType.tfae_six_pos, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleRelativeFiniteType/VeryAmple.lean, line 256. The attribute's comment: “all six conditions verbatim and with no named input: ampleness, f-ampleness, relative very ampleness of some and of every sufficiently high tensor power, and the two immersion clauses with the source's lower bound n ≥ 1 on the dimension of the projective space”.
[Stacks, Tag 01VT], all six conditions, with the source's own immersion clauses. The immersion clauses (5) and (6) are
Stacks.AmpleProjectiveImmersion.HasImmersionTwistOverPos, which writes∃ n ≥ 1as the source does, rather thanStacks.AmpleProjectiveImmersion.HasImmersionTwistOver's∃ n : ℕ.The two agree —
Stacks.AmpleProjectiveImmersion.hasImmersionTwistOverPos_iff— because an immersion intoℙⁿ_Scomposed with the linear embeddingℙⁿ_S ↪ ℙᴺ_Sis an immersion intoℙᴺ_Scarrying the same hyperplane sheaf, so a witness atngives one atmax n 1. This is thereforeStacks.AmpleRelativeFiniteType.tfae_sixwith two clauses rewritten, and the tag's six conditions hold verbatim.
theorem tfae_six_pos [IsAffine S] (f : X ⟶ S) (L : X.Modules) [IsInvertibleModule X L]
[LocallyOfFiniteType f] [QuasiCompact f] :
List.TFAE [
IsAmple X L,
Stacks.RelativeAmple.IsRelativelyAmple f L,
∃ d : ℕ, 1 ≤ d ∧
Stacks.Tag01VMVeryAmple.IsRelativelyVeryAmple f (tensorPowModule X L (d : ℤ)),
∃ d₀ : ℕ, 1 ≤ d₀ ∧ ∀ d : ℕ, d₀ ≤ d →
Stacks.Tag01VMVeryAmple.IsRelativelyVeryAmple f (tensorPowModule X L (d : ℤ)),
∃ d : ℕ, 1 ≤ d ∧ HasImmersionTwistOverPos f (tensorPowModule X L (d : ℤ)),
∃ d₀ : ℕ, 1 ≤ d₀ ∧ ∀ d : ℕ, d₀ ≤ d →
HasImmersionTwistOverPos f (tensorPowModule X L (d : ℤ))]
Tag 01VU, a lemma
Tag 01VU in the Stacks Project.
Stacks.VeryAmplePowersQuasiCompactBase.existsVeryAmplePower_of_eventuallyVeryAmplePower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/VeryAmplePowersQuasiCompactBase/Basic.lean, line 92. The attribute's comment: “(3) implies (2)”. References: EGA II (4.5.10), “(ii): e) implies e')”.
If every sufficiently high tensor power of
Lis very ample relative tof, then some positive tensor power ofLis very ample relative tof.
theorem existsVeryAmplePower_of_eventuallyVeryAmplePower (f : X ⟶ S) (L : X.Modules)
[IsInvertibleModule X L] (h : EventuallyVeryAmplePower f L) : ExistsVeryAmplePower f L
Stacks.VeryAmplePowersQuasiCompactBase.isRelativelyAmple_of_existsVeryAmplePower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/VeryAmplePowersQuasiCompactBase/Basic.lean, line 100. The attribute's comment: “(2) implies (1)”. References: EGA II (4.5.10), “more general”; EGA II (4.6.2), “more general”.
If some positive tensor power of
Lis very ample relative to a quasi-compactf, thenLis ample relative tof.
theorem isRelativelyAmple_of_existsVeryAmplePower (f : X ⟶ S) (L : X.Modules)
[IsInvertibleModule X L] (hf : QuasiCompact f) (h : ExistsVeryAmplePower f L) :
Stacks.RelativeAmple.IsRelativelyAmple f L
Stacks.VeryAmplePowersQuasiCompactBase.isRelativelyAmple_of_eventuallyVeryAmplePower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/VeryAmplePowersQuasiCompactBase/Basic.lean, line 110. The attribute's comment: “(3) implies (1)”. References: EGA II (4.5.10), “(ii): e) implies ample”.
If every sufficiently high tensor power of
Lis very ample relative to a quasi-compactf, thenLis ample relative tof.
theorem isRelativelyAmple_of_eventuallyVeryAmplePower (f : X ⟶ S) (L : X.Modules)
[IsInvertibleModule X L] (hf : QuasiCompact f) (h : EventuallyVeryAmplePower f L) :
Stacks.RelativeAmple.IsRelativelyAmple f L
Stacks.VeryAmplePowersQuasiCompactBase.eventuallyVeryAmplePower_of_isRelativelyAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/VeryAmplePowersQuasiCompactBase/Basic.lean, line 124. The attribute's comment: “(1) implies (3)”. References: EGA II (4.5.10), “(ii): ample implies e)”; EGA II (4.5.11), “The case L' = O_X”; EGA II (4.6.11), “partial”.
Let
f : X ⟶ Sbe locally of finite type withSquasi-compact and letLbe ample relative tof. ThenL^{⊗ d}is very ample relative toffor every sufficiently larged.
theorem eventuallyVeryAmplePower_of_isRelativelyAmple (f : X ⟶ S)
(L : X.Modules) [IsInvertibleModule X L] [CompactSpace S] [LocallyOfFiniteType f]
(hL : Stacks.RelativeAmple.IsRelativelyAmple f L) :
EventuallyVeryAmplePower f L
Stacks.VeryAmplePowersQuasiCompactBase.tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/VeryAmplePowersQuasiCompactBase/Basic.lean, line 163.
For
f : X ⟶ Sof finite type withSquasi-compact andLan invertible𝒪_X-module, the three conditions
Lisf-relatively ample,L^{⊗ d}isf-relatively very ample for somed ≥ 1, andL^{⊗ d}isf-relatively very ample for every sufficiently largedare equivalent.
theorem tfae (f : X ⟶ S)
(L : X.Modules) [IsInvertibleModule X L] [CompactSpace S] [LocallyOfFiniteType f]
(hf : QuasiCompact f) :
List.TFAE [Stacks.RelativeAmple.IsRelativelyAmple f L, ExistsVeryAmplePower f L,
EventuallyVeryAmplePower f L]
Tag 02NQ, a lemma
Tag 02NQ in the Stacks Project.
Stacks.VeryAmpleFiniteTypeCover.hasProjectiveImmersionCover_of_isRelativelyVeryAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/VeryAmpleFiniteTypeCover/Equivalence.lean, line 114. The attribute's comment: “(1) implies (2)”.
Stacks Tag 02NQ, (1) implies (2). Let
f : X ⟶ Sbe of finite type andLan invertible𝒪_X-module. IfLisf-relatively very ample then there are an open coveringS = ⋃ V_j, for eachjan integern_j, and immersionsf⁻¹(V_j) ⟶ 𝐏^{n_j}_{V_j}overV_jcarrying the hyperplane sheaf toL|_{f⁻¹(V_j)}.This is the source's own proof: take an affine open covering of
Sand apply Stacks Tag 02NP,Stacks.CoordinateImmersion.hasImmersionTwistOver_of_isRelativelyVeryAmple, to each of the restrictions offandL; relative very ampleness of the restrictions is Stacks Tag 01VR's (1) implies (2) at the member,Stacks.Tag01VMVeryAmple.isRelativelyVeryAmple_morphismRestrict.
theorem hasProjectiveImmersionCover_of_isRelativelyVeryAmple (f : X ⟶ S) (L : X.Modules)
[IsInvertibleModule X L] [LocallyOfFiniteType f] [QuasiCompact f]
(hL : Tag01VMVeryAmple.IsRelativelyVeryAmple f L) :
HasProjectiveImmersionCover f L
Stacks.VeryAmpleFiniteTypeCover.isRelativelyVeryAmple_of_hasProjectiveImmersionCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/VeryAmpleFiniteTypeCover/Equivalence.lean, line 194. The attribute's comment: “(2) implies (1)”.
Stacks Tag 02NQ, (2) implies (1). Let
f : X ⟶ Sbe quasi-compact andLan invertible𝒪_X-module. If there are an open coveringS = ⋃ V_j, for eachjan integern_j, and immersionsf⁻¹(V_j) ⟶ 𝐏^{n_j}_{V_j}overV_jcarrying the hyperplane sheaf toL|_{f⁻¹(V_j)}, thenLisf-relatively very ample.The covering is refined to the affine opens of
Scontained in one of its members, which coverSbecause the affine opens are a basis (AlgebraicGeometry.Scheme.isBasis_affineOpens); over each of them the immersion clause is the restriction of the one over the member,Stacks.VeryAmpleFiniteTypeCover.hasImmersionTwistOver_morphismRestrict_of_le, and the immersions over an affine covering give relative very ampleness byStacks.VeryAmpleGlue.isRelativelyVeryAmple_of_affine_cover_hasImmersionTwistOver.Only quasi-compactness of
fis used, not the whole of the source's finite-type assumption.
theorem isRelativelyVeryAmple_of_hasProjectiveImmersionCover (f : X ⟶ S) (L : X.Modules)
[IsInvertibleModule X L] (hqc : QuasiCompact f) (h : HasProjectiveImmersionCover f L) :
Tag01VMVeryAmple.IsRelativelyVeryAmple f L
Stacks.VeryAmpleFiniteTypeCover.isRelativelyVeryAmple_iff_hasProjectiveImmersionCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/VeryAmpleFiniteTypeCover/Equivalence.lean, line 221.
Stacks Tag 02NQ. For
f : X ⟶ Sof finite type andLan invertible𝒪_X-module, relative very ampleness ofLis equivalent to the existence of an open coveringS = ⋃ V_j, of an integern_jfor eachj, and of immersionsf⁻¹(V_j) ⟶ 𝐏^{n_j}_{V_j}overV_jcarrying the hyperplane sheaf toL|_{f⁻¹(V_j)}.The two implications are
Stacks.VeryAmpleFiniteTypeCover.hasProjectiveImmersionCover_of_isRelativelyVeryAmpleandStacks.VeryAmpleFiniteTypeCover.isRelativelyVeryAmple_of_hasProjectiveImmersionCover.
theorem isRelativelyVeryAmple_iff_hasProjectiveImmersionCover (f : X ⟶ S) (L : X.Modules)
[IsInvertibleModule X L] [LocallyOfFiniteType f] [hqc : QuasiCompact f] :
Tag01VMVeryAmple.IsRelativelyVeryAmple f L ↔ HasProjectiveImmersionCover f L
Tag 02NR, a lemma
Tag 02NR in the Stacks Project.
Stacks.AmplePowerImmersionCover.hasPowerProjectiveImmersionCover_of_isRelativelyAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmplePowerImmersionCover/Basic.lean, line 247. The attribute's comment: “(a) implies (b), with no hypothesis”.
Stacks Tag 02NR, (a) ⟹ (b). Let
f : X ⟶ Sbe of finite type andLan invertible𝒪_X-module. IfLisf-relatively ample then there are an open coveringS = ⋃ V_j, for eachjintegersd_j ≥ 1andn_j ≥ 0, and immersionsf⁻¹(V_j) ⟶ 𝐏^{n_j}_{V_j}overV_jcarrying the hyperplane sheaf toL^{⊗ d_j}|_{f⁻¹(V_j)}.This is the source's own proof — take an affine open covering of
Sand apply Stacks Tag 01VS to each of the restrictions offandL— and it needs no hypothesis: Tag 01VS is proved unconditionally, and the stronger affine-and-eventual form isexists_affine_cover_eventually_hasImmersionTwistOver_of_isRelativelyAmple, from which one degree is read off at the bound itself. Only local finiteness of type is used; quasi-compactness offis already part of relative ampleness.
theorem hasPowerProjectiveImmersionCover_of_isRelativelyAmple (f : X ⟶ S) (L : X.Modules)
[IsInvertibleModule X L] [LocallyOfFiniteType f]
(hL : Stacks.RelativeAmple.IsRelativelyAmple f L) :
HasPowerProjectiveImmersionCover f L
Stacks.AmplePowerImmersionCover.isRelativelyAmple_of_hasPowerProjectiveImmersionCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmplePowerImmersionCover/Basic.lean, line 510. The attribute's comment: “(b) implies (a), with no hypothesis: the source's covering is by arbitrary opens, and the immersion clause at a member is restricted to the affine opens of that member by hasImmersionTwistOver_morphismRestrict, projective space over a base being a fibre product over the terminal scheme”.
Stacks Tag 02NR, (b) ⟹ (a). Let
f : X ⟶ Sbe quasi-compact andLan invertible𝒪_X-module. If there are an open coveringS = ⋃ V_j, for eachjintegersd_j ≥ 1andn_j ≥ 0, and immersionsf⁻¹(V_j) ⟶ 𝐏^{n_j}_{V_j}overV_jcarrying the hyperplane sheaf toL^{⊗ d_j}|_{f⁻¹(V_j)}, thenLisf-relatively ample.The route is the source's, taken member by member. At a member
V_jthe clause of (b) is the immersionf⁻¹(V_j) ⟶ 𝐏^{n_j}_{V_j}overV_jcarrying the hyperplane sheaf toL^{⊗ d_j}|_{f⁻¹(V_j)};Stacks.RelativeVeryAmple.pullbackTensorPowModuleIsorewrites that module as thed_j-th power ofL|_{f⁻¹(V_j)}, andStacks.AmplePowerImmersionCover.isRelativelyAmple_of_hasImmersionTwistOverturns the clause into relative ampleness ofL|_{f⁻¹(V_j)}overV_j— over a base that need not be affine, becauseStacks.AmplePowerImmersionCover.hasImmersionTwistOver_morphismRestrictrestricts the immersion clause to the affine opens ofV_j. The members are then glued byStacks.AmplePowerImmersionCover.isRelativelyAmple_of_forall_isRelativelyAmple_morphismRestrict, which is Stacks Tag 01VJ's (2) ⟹ (1) and is proved above — so the gluing of very ampleness, Stacks Tag 01VR's (2) ⟹ (1), is not needed, and neither is any statement about relative very ampleness. Because the degreesd_jare consumed one member at a time, no common degree has to be produced.Only quasi-compactness of
fis used, not the whole of the source's finite-type hypothesis.
theorem isRelativelyAmple_of_hasPowerProjectiveImmersionCover (f : X ⟶ S)
(L : X.Modules) [IsInvertibleModule X L] (hf : QuasiCompact f)
(h : HasPowerProjectiveImmersionCover f L) :
Stacks.RelativeAmple.IsRelativelyAmple f L
Stacks.AmplePowerImmersionCover.isRelativelyAmple_iff_hasPowerProjectiveImmersionCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmplePowerImmersionCover/Basic.lean, line 538. The attribute's comment: “the equivalence, with no hypothesis”.
Stacks Tag 02NR. For
f : X ⟶ Sof finite type andLan invertible𝒪_X-module, relative ampleness ofLis equivalent to the existence of an open coveringS = ⋃ V_j, of integersd_j ≥ 1andn_j ≥ 0for eachj, and of immersionsf⁻¹(V_j) ⟶ 𝐏^{n_j}_{V_j}overV_jcarrying the hyperplane sheaf toL^{⊗ d_j}|_{f⁻¹(V_j)}.The two implications are
Stacks.AmplePowerImmersionCover.hasPowerProjectiveImmersionCover_of_isRelativelyAmpleandStacks.AmplePowerImmersionCover.isRelativelyAmple_of_hasPowerProjectiveImmersionCover; neither has a hypothesis, and this is their conjunction.
theorem isRelativelyAmple_iff_hasPowerProjectiveImmersionCover (f : X ⟶ S)
(L : X.Modules) [IsInvertibleModule X L] [LocallyOfFiniteType f] (hf : QuasiCompact f) :
Stacks.RelativeAmple.IsRelativelyAmple f L ↔ HasPowerProjectiveImmersionCover f L
Tag 0FVC, a lemma
Tag 0FVC in the Stacks Project.
Stacks.VeryAmpleFixedTwist.eventuallyVeryAmpleFixedTwist_of_isRelativelyAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/VeryAmpleFixedTwist/Basic.lean, line 586. References: EGA II (4.5.10), “(ii): ample implies e)”; EGA II (4.5.11), “more general”; EGA II (4.6.12).
Stacks Tag 0FVC. Let
f : X ⟶ Sbe a morphism of schemes andN,Linvertible𝒪_X-modules. IfSis quasi-compact,fis of finite type andLisf-relatively ample, thenN ⊗ L^{⊗ d}isf-relatively very ample for every sufficiently larged.The proof is the source's. The affine open covering
S.affineCover.finiteSubcoverofSis finite becauseSis quasi-compact, andStacks.VeryAmpleFixedTwist.eventually_familyImmersion_tensorat the restriction off, whose ampleness hypothesis is the defining clause of relative ampleness, gives over each member a bound past whichN ⊗ L^{⊗ d}restricted to the member carries a generating family pinning an immersion into projective space over the member — the source's reduction to an affine base, Tag 02NQ, performed by hand so that the engine runs with absolute ampleness. The largest of the finitely many bounds serves every member, andStacks.VeryAmpleGlue.isRelativelyVeryAmple_of_cover(Stacks Tag 01VT's (5) ⟹ (3) and Stacks Tag 01VR's (2) ⟹ (1) together) turns the families into relative very ampleness overS; the restriction ofN ⊗ L^{⊗ d}is matched with the module the families live on byStacks.VeryAmpleFixedTwist.pullbackTensorTwistIso. Quasi-compactness offis taken from relative ampleness.
theorem eventuallyVeryAmpleFixedTwist_of_isRelativelyAmple {S : Scheme.{u}}
(f : X ⟶ S) (N L : X.Modules) [IsInvertibleModule X N] [IsInvertibleModule X L]
[CompactSpace S] [LocallyOfFiniteType f]
(hL : Stacks.RelativeAmple.IsRelativelyAmple f L) :
EventuallyVeryAmpleFixedTwist f N L
Sources
Section29.41 Quasi-projective morphisms#
Section 29.41 of the Stacks Project, Tag 01VV. 8 tags here are carried by 21 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 01VW, a definition
Tag 01VW in the Stacks Project.
AlgebraicGeometry.IsHQuasiProjective, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/QuasiProjective.lean, line 53. The attribute's comment: “H-quasi-projective”.
Stacks Project, Tag 01VW. A quasi-compact immersion into relative finite-dimensional projective space. This is
Stacks.HProjective.IsHQuasiProjective, which states the same thing with the structure morphism ofℙⁿ_Sspelled↘.
abbrev IsHQuasiProjective {X S : Scheme.{u}} (f : X ⟶ S) : Prop
AlgebraicGeometry.IsLocallyQuasiProjective, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/QuasiProjective.lean, line 59. The attribute's comment: “locally quasi-projective”.
Stacks Project, Tag 01VW. A morphism quasi-projective after restriction over an open cover of the base.
abbrev IsLocallyQuasiProjective {X S : Scheme.{u}} (f : X ⟶ S) : Prop
AlgebraicGeometry.IsQuasiProjective, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiProjective/Basic.lean, line 77. The attribute's comment: “quasi-projective”. References: EGA II (5.3.1).
A morphism of schemes is quasi-projective when it is of finite type — locally of finite type and quasi-compact — and the source carries an invertible sheaf that is ample relative to it.
public abbrev IsQuasiProjective {X S : Scheme.{u}} (f : X ⟶ S) : Prop
Tag 0B3G, a lemma
Tag 0B3G in the Stacks Project.
AlgebraicGeometry.IsQuasiProjective.of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiProjective/BaseChange.lean, line 78.
[Stacks, Tag 0B3G]. A base change of a quasi-projective morphism is quasi-projective: if
f' : X' ⟶ S'fits into a cartesian square over a quasi-projectivef : X ⟶ S, thenf'is quasi-projective.Finite type is stable under base change, which is the finite-type half of [Stacks, Tag 01T4], and the pullback along
X' ⟶ Xof a sheaf ample relative tofis ample relative tof', which is [Stacks, Tag 0893] in the formStacks.AmpleBridge.relativelyAmpleBaseChange.
public theorem of_isPullback {X S X' S' : Scheme.{u}} {p : X' ⟶ X} {f' : X' ⟶ S'} {f : X ⟶ S}
{g : S' ⟶ S} (hsq : IsPullback p f' f g) (hf : IsQuasiProjective f) :
IsQuasiProjective f'
Tag 0C4M, a lemma
Tag 0C4M in the Stacks Project.
AlgebraicGeometry.IsQuasiProjective.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiProjective/Composite.lean, line 67. References: EGA I (6.6.4), “(ii), special case”.
[Stacks, Tag 0C4M]. Let
f : X ⟶ Yandg : Y ⟶ Sbe morphisms of schemes withSquasi-compact. Iffandgare quasi-projective, then so isf ≫ g.Finite type composes. The relatively ample sheaf is produced by [Stacks, Tag 0C4K],
Stacks.AmplePullbackDatum.exists_threshold_isRelativelyAmple_comp: from sheavesLonXample relative tofandMonYample relative togit gives a threshold beyond whichL ⊗ f^* M ^⊗ ais ample relative tof ≫ g, and the threshold itself is used as the exponent.
public theorem comp {X Y S : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ S) [CompactSpace S]
(hf : IsQuasiProjective f) (hg : IsQuasiProjective g) : IsQuasiProjective (f ≫ g)
Tag 01VX, a lemma
Tag 01VX in the Stacks Project.
AlgebraicGeometry.IsQuasiProjective.locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiProjective/Basic.lean, line 101. The attribute's comment: “finite_type”.
Stacks Project, Tag 01VX, quasi-projective case. A quasi-projective morphism is locally of finite type; here this is part of the definition.
public theorem locallyOfFiniteType (h : IsQuasiProjective f) : LocallyOfFiniteType f
AlgebraicGeometry.IsQuasiProjective.quasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiProjective/Basic.lean, line 106. The attribute's comment: “finite_type”.
Stacks Project, Tag 01VX, quasi-projective case. A quasi-projective morphism is quasi-compact; here this is part of the definition.
public theorem quasiCompact (h : IsQuasiProjective f) : QuasiCompact f
AlgebraicGeometry.IsHQuasiProjective.locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiProjective/SeparatedFiniteType.lean, line 72. The attribute's comment: “finite_type”.
An H-quasi-projective morphism of schemes is locally of finite type.
theorem locallyOfFiniteType (hf : IsHQuasiProjective f) : LocallyOfFiniteType f
AlgebraicGeometry.IsHQuasiProjective.quasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiProjective/SeparatedFiniteType.lean, line 78. The attribute's comment: “finite_type”.
An H-quasi-projective morphism of schemes is quasi-compact.
theorem quasiCompact (hf : IsHQuasiProjective f) : QuasiCompact f
AlgebraicGeometry.IsHQuasiProjective.isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiProjective/SeparatedFiniteType.lean, line 84. The attribute's comment: “separated”.
An H-quasi-projective morphism of schemes is separated.
theorem isSeparated (hf : IsHQuasiProjective f) : IsSeparated f
AlgebraicGeometry.IsQuasiProjective.isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiProjective/SeparatedFiniteType.lean, line 94. The attribute's comment: “separated”. References: EGA II (4.6.3), “special case”.
A quasi-projective morphism of schemes is separated.
theorem isSeparated (hf : IsQuasiProjective f) : IsSeparated f
AlgebraicGeometry.IsLocallyQuasiProjective.locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiProjective/SeparatedFiniteType.lean, line 104. The attribute's comment: “finite_type”.
A locally quasi-projective morphism of schemes is locally of finite type.
theorem locallyOfFiniteType (hf : IsLocallyQuasiProjective f) : LocallyOfFiniteType f
AlgebraicGeometry.IsLocallyQuasiProjective.quasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiProjective/SeparatedFiniteType.lean, line 112. The attribute's comment: “finite_type”.
A locally quasi-projective morphism of schemes is quasi-compact.
theorem quasiCompact (hf : IsLocallyQuasiProjective f) : QuasiCompact f
AlgebraicGeometry.IsLocallyQuasiProjective.isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiProjective/SeparatedFiniteType.lean, line 120. The attribute's comment: “separated”.
A locally quasi-projective morphism of schemes is separated.
theorem isSeparated (hf : IsLocallyQuasiProjective f) : IsSeparated f
Tag 01VY, a lemma
Tag 01VY in the Stacks Project.
Stacks.HProjective.isQuasiProjective_of_isHQuasiProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/HProjective/QuasiProjectiveOfHQuasiProjective.lean, line 213.
Stacks Tag 01VY: an H-quasi-projective morphism is quasi-projective. Let
i : X ⟶ ℙⁿ_Sbe a quasi-compact immersion withi ≫ (ℙⁿ_S ↘ S) = f. Thenfis of finite type, becauseiis an immersion andℙⁿ_S ⟶ Sis proper, andi^* 𝒪(1)is an invertible module ample relative tofby [Stacks, Tag 01VN],𝒪(1)being ample relative toℙⁿ_S ⟶ S.
theorem isQuasiProjective_of_isHQuasiProjective {X S : Scheme.{u}} (f : X ⟶ S)
(hf : IsHQuasiProjective f) : IsQuasiProjective f
Tag 01VZ, a lemma
Tag 01VZ in the Stacks Project.
Stacks.HProjective.isLocallyQuasiProjective_of_exists_openCover_isHQuasiProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/HProjective/QuasiProjectiveOfHQuasiProjective.lean, line 312. The attribute's comment: “(2) implies (1): H-quasi-projective over a cover of the base”.
Stacks Tag 01VZ, the implication (2) ⟹ (1). If the base carries an open covering over whose members
fis H-quasi-projective, thenfis locally quasi-projective.This is [Stacks, Tag 01VY] applied over each member of the covering, which is the source's own proof of this implication.
theorem isLocallyQuasiProjective_of_exists_openCover_isHQuasiProjective {X S : Scheme.{u}}
(f : X ⟶ S) (h : ∃ 𝒰 : Scheme.OpenCover.{u} S, ∀ i : 𝒰.I₀,
AlgebraicGeometry.IsHQuasiProjective (pullback.snd f (𝒰.f i))) :
AlgebraicGeometry.IsLocallyQuasiProjective f
Stacks.HProjective.exists_openCover_isHQuasiProjective_of_isLocallyQuasiProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/HProjective/QuasiProjectiveOfHQuasiProjective.lean, line 333. The attribute's comment: “(1) implies (2): a cover of the base over which f is H-quasi-projective”.
Stacks Tag 01VZ, the implication (1) ⟹ (2). A locally quasi-projective morphism admits an open covering of the base over whose members it is H-quasi-projective.
Local quasi-projectivity gives a covering
𝒰of the base over whose membersfbecomes quasi-projective. Refining𝒰to an affine covering —AlgebraicGeometry.Scheme.OpenCover.affineRefinement, whose members are the affine covers of the members of𝒰— reduces to an affine base, whereStacks.HProjective.isHQuasiProjective_pullbackSnd_of_isQuasiProjectiveapplies. The refinement's base change is identified with the iterated one byAlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom, and H-quasi-projectivity travels across that identification byStacks.HProjective.isHQuasiProjective_of_iso.
theorem exists_openCover_isHQuasiProjective_of_isLocallyQuasiProjective {X S : Scheme.{u}}
(f : X ⟶ S) (hf : AlgebraicGeometry.IsLocallyQuasiProjective f) :
∃ 𝒰 : Scheme.OpenCover.{u} S, ∀ i : 𝒰.I₀,
AlgebraicGeometry.IsHQuasiProjective (pullback.snd f (𝒰.f i))
Stacks.HProjective.isLocallyQuasiProjective_iff_exists_openCover_isHQuasiProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/HProjective/QuasiProjectiveOfHQuasiProjective.lean, line 352. The attribute's comment: “(1) iff (2): the equivalence the tag states”.
Stacks Tag 01VZ. A morphism of schemes is locally quasi-projective if and only if the base has an open covering over whose members it is H-quasi-projective.
theorem isLocallyQuasiProjective_iff_exists_openCover_isHQuasiProjective {X S : Scheme.{u}}
(f : X ⟶ S) :
AlgebraicGeometry.IsLocallyQuasiProjective f ↔
∃ 𝒰 : Scheme.OpenCover.{u} S, ∀ i : 𝒰.I₀,
AlgebraicGeometry.IsHQuasiProjective (pullback.snd f (𝒰.f i))
Stacks.HProjective.exists_opens_isHQuasiProjective_of_isLocallyQuasiProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/HProjective/QuasiProjectiveOfHQuasiProjective.lean, line 370. The attribute's comment: “(1) implies (2), with the cover as opens Vⱼ of S and f⁻¹(Vⱼ) → Vⱼ”.
Stacks Tag 01VZ, condition (2) in the source's own phrasing. A locally quasi-projective
f : X ⟶ Sadmits a family of opensVⱼofSwithS = ⋃ Vⱼsuch that everyf⁻¹(Vⱼ) ⟶ Vⱼis H-quasi-projective.The opens are the images of the covering produced by
Stacks.HProjective.exists_openCover_isHQuasiProjective_of_isLocallyQuasiProjective; they coverSbyAlgebraicGeometry.Scheme.OpenCover.iSup_opensRange, and over each of them the base change and the restriction are isomorphic as arrows byAlgebraicGeometry.morphismRestrictOpensRange.
theorem exists_opens_isHQuasiProjective_of_isLocallyQuasiProjective
{X S : Scheme.{u}} (f : X ⟶ S) (hf : AlgebraicGeometry.IsLocallyQuasiProjective f) :
∃ (ι : Type u) (V : ι → S.Opens), (⨆ j, V j) = ⊤ ∧
∀ j, AlgebraicGeometry.IsHQuasiProjective (f ∣_ V j)
Tag 0B3H, a lemma
Tag 0B3H in the Stacks Project.
Stacks.HProjective.isQuasiProjective_of_isQuasiAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/HProjective/QuasiProjective.lean, line 194. References: EGA II (5.3.4), “(i)”.
Stacks Tag 0B3H. A quasi-affine morphism of finite type is quasi-projective: the structure sheaf
𝒪_Xis ample relative to a quasi-affine morphism by [Stacks, Tag 0891].Finite type is the conjunction of local finite type and quasi-compactness, as in Tag 01T1, and quasi-compactness is already a consequence of quasi-affineness, so only the local finite type half is a hypothesis.
theorem isQuasiProjective_of_isQuasiAffineHom {X S : Scheme.{u}} (f : X ⟶ S)
[IsQuasiAffineHom f] (hf : LocallyOfFiniteType f) : IsQuasiProjective f
Tag 0C4N, a lemma
Tag 0C4N in the Stacks Project.
AlgebraicGeometry.IsQuasiProjective.of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiProjective/Composition.lean, line 43.
Let
f : X ⟶ Yandg : Y ⟶ Sbe morphisms of schemes. Iff ≫ gis quasi-projective andfis quasi-compact, thenfis quasi-projective.
public theorem of_comp {X Y S : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ S)
(hfg : IsQuasiProjective (f ≫ g)) (hf : QuasiCompact f) : IsQuasiProjective f
Sources
Section29.42 Proper morphisms#
Section 29.42 of the Stacks Project, Tag 01W0. 10 tags here are carried by 15 declarations of the repository (all in StacksFrontier) and 8 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 01W1, a definition
Tag 01W1 in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.IsProperregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 259 (StacksFrontier). References: EGA II (5.4.1); EGA II (7.4.7).
Tag 02K7, a lemma
Tag 02K7 in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.universallyClosed_isZariskiLocalAtTargetregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 168 (StacksFrontier): “being universally closed is local on the target”.
Tag 01W2, a lemma
Tag 01W2 in the Stacks Project.
AlgebraicGeometry.isProper_iff_exists_iSup_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/Basic.lean, line 63.
[Stacks, Tag 01W2]. A morphism of schemes
f : X ⟶ Sis proper if and only if there is an open coveringS = ⋃ V jsuch that every restrictionf⁻¹(V j) ⟶ V jis proper. The index type of the covering may live in any universe.
theorem isProper_iff_exists_iSup_eq_top {X S : Scheme.{u}} (f : X ⟶ S) :
IsProper f ↔ ∃ (ι : Type*) (V : ι → S.Opens), iSup V = ⊤ ∧ ∀ j, IsProper (f ∣_ V j)
Tag 01W3, a lemma
Tag 01W3 in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.IsProper.stableUnderCompositionregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Morphisms/Proper/Basic.lean, line 139 (StacksFrontier): “the composition of proper morphisms is proper”. References: EGA II (5.4.2).AlgebraicGeometry.universallyClosed_isStableUnderCompositionregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Morphisms/Proper/Basic.lean, line 142 (StacksFrontier): “the composition of universally closed morphisms is universally closed”. References: EGA II (5.4.9), “5.4.2(ii)”; EGA IV (2.4.3), “(ii)”.
Tag 01W4, a lemma
Tag 01W4 in the Stacks Project.
Stacks.ProperAlgebraBaseChange.universallyClosed_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperAlgebraBaseChange/Basic.lean, line 115. The attribute's comment: “the base change of a universally closed morphism is universally closed”.
Stacks Project, Tag 01W4, second statement. The base change of a universally closed morphism is universally closed: in a cartesian square
Y' --f'--> Y | | g' g v v X ---f---> Sif
gis universally closed then so isg'.
theorem universallyClosed_of_isPullback {X Y Y' S : Scheme.{u}} {f : X ⟶ S} {g : Y ⟶ S}
{f' : Y' ⟶ Y} {g' : Y' ⟶ X} (sq : IsPullback f' g' g f) (hg : UniversallyClosed g) :
UniversallyClosed g'
Stacks.ProperAlgebraBaseChange.isProper_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperAlgebraBaseChange/Basic.lean, line 133. The attribute's comment: “the base change of a proper morphism is proper”.
Stacks Project, Tag 01W4, first statement. The base change of a proper morphism is proper: in a cartesian square
Y' --f'--> Y | | g' g v v X ---f---> Sif
gis proper then so isg'.
theorem isProper_of_isPullback {X Y Y' S : Scheme.{u}} {f : X ⟶ S} {g : Y ⟶ S}
{f' : Y' ⟶ Y} {g' : Y' ⟶ X} (sq : IsPullback f' g' g f) (hg : IsProper g) :
IsProper g'
Declarations registered for the tag:
AlgebraicGeometry.IsProper.isStableUnderBaseChangeregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Curves/VanishingResults/SituationBaseChange.lean, line 63 (StacksFrontier): “the proper case”. References: EGA II (5.4.2), “more general”; EGA III (4.3.4), “more general”; EGA IV (2.7.1), “implication”; SGA 1 IX (2.4), “partial”; SGA 1 VIII (4.8), “partial”; SGA 3 VIB (10.1), “partial”; SGA 6 X (7.5), “partial”.AlgebraicGeometry.universallyClosed_isStableUnderBaseChangeregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Curves/VanishingResults/SituationBaseChange.lean, line 65 (StacksFrontier): “the universally closed case”. References: EGA II (5.4.9), “5.4.2(iii)”; EGA IV (2.4.3), “(iii)”; EGA IV (2.6.4), “(ii)”; SGA 1 IX (2.4), “partial”; SGA 1 VIII (4.7), “necessity”; SGA 3 V (6.1), “partial”.
Tag 01W5, a lemma
Tag 01W5 in the Stacks Project.
AlgebraicGeometry.isProper_of_isClosedImmersion, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/Basic.lean, line 55. The attribute's comment: “proper”. References: EGA II (5.4.2); EGA II (5.4.9), “5.4.2(i)”.
A closed immersion of schemes is proper: it is a finite morphism, and a finite morphism is separated, universally closed and locally of finite type.
lemma isProper_of_isClosedImmersion {X Y : Scheme.{u}} (f : X ⟶ Y) [IsClosedImmersion f] :
IsProper f
Declarations registered for the tag:
AlgebraicGeometry.instUniversallyClosedOfIsClosedImmersionregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Morphisms/Proper/Basic.lean, line 146 (StacksFrontier): “a closed immersion is universally closed”. References: EGA II (5.4.9), “5.4.2(i)”; EGA II (6.1.10), “closed immersions”; EGA IV (2.4.3).
Tag 01W6, a lemma
Tag 01W6 in the Stacks Project.
AlgebraicGeometry.universallyClosed_of_universallyClosed_of_isSeparated, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/Basic.lean, line 78. The attribute's comment: “(1), in the triangle form of the source”.
[Stacks, Tag 01W6] part (1). Let
X ⟶ Y ⟶ Sbe a commutative triangle withYseparated overS. IfX ⟶ Sis universally closed, then so isX ⟶ Y.
lemma universallyClosed_of_universallyClosed_of_isSeparated (h : g ≫ q = p) [IsSeparated q]
[UniversallyClosed p] : UniversallyClosed g
AlgebraicGeometry.isProper_of_isProper_of_isSeparated, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/Basic.lean, line 86. The attribute's comment: “(2), in the triangle form of the source”.
[Stacks, Tag 01W6] part (2). Let
X ⟶ Y ⟶ Sbe a commutative triangle withYseparated overS. IfXis proper overS, thenX ⟶ Yis proper.
lemma isProper_of_isProper_of_isSeparated (h : g ≫ q = p) [IsSeparated q] [IsProper p] :
IsProper g
AlgebraicGeometry.isClosed_range_of_universallyClosed_of_isSeparated, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/Basic.lean, line 96. The attribute's comment: “the final clause: the image of X in Y is closed”.
The final clause of [Stacks, Tag 01W6]. In a commutative triangle
X ⟶ Y ⟶ SwithYseparated overSandXuniversally closed overS, the image ofXinYis closed: the morphismX ⟶ Yis universally closed, hence a closed map, and its image is the image of the whole space.
lemma isClosed_range_of_universallyClosed_of_isSeparated (h : g ≫ q = p) [IsSeparated q]
[UniversallyClosed p] : IsClosed (Set.range g.base)
Tag 03GN, a lemma
Tag 03GN in the Stacks Project.
AlgebraicGeometry.universallyClosed_of_universallyClosed_of_surjective, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/Basic.lean, line 115. The attribute's comment: “the universally closed half, in the triangle form of the source”.
[Stacks, Tag 03GN], the universally closed half. Let
X ⟶ Y ⟶ Sbe a commutative triangle withX ⟶ Ysurjective. IfX ⟶ Sis universally closed, then so isY ⟶ S: a map is closed as soon as its precomposition with a continuous surjection is, and surjectivity is stable under base change.
lemma universallyClosed_of_universallyClosed_of_surjective (h : g ≫ q = p) [Surjective g]
[UniversallyClosed p] : UniversallyClosed q
AlgebraicGeometry.isProper_of_isProper_of_surjective, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/Basic.lean, line 129. The attribute's comment: “the image of a proper scheme is proper, in the triangle form of the source: separatedness and locally-of-finite-typeness of the image are hypotheses, as they are there”. References: EGA II (5.4.3), “more general”.
[Stacks, Tag 03GN]. The image of a proper scheme is proper: in a commutative triangle
X ⟶ Y ⟶ SwithX ⟶ Ysurjective andXproper overS, the morphismY ⟶ Sis proper as soon as it is separated and locally of finite type.Universal closedness is the previous lemma; separatedness and locally-of-finite-typeness are hypotheses, exactly as in the source, since neither descends along a bare surjection.
lemma isProper_of_isProper_of_surjective (h : g ≫ q = p) [Surjective g] [IsProper p]
[IsSeparated q] [LocallyOfFiniteType q] : IsProper q
Declarations registered for the tag:
AlgebraicGeometry.UniversallyClosed.of_comp_surjectiveregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/ProperLimitStage/Basic.lean, line 98 (StacksFrontier): “the universal closedness conclusion”. References: EGA II (5.4.9), “more general”; EGA IV (2.4.3), “(v), universally closed”; SGA 3 V (7.4), “partial”.
Tag 0AH6, a lemma
Tag 0AH6 in the Stacks Project.
AlgebraicGeometry.isProper_imageι_comp, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/SchemeTheoreticImage.lean, line 43. The attribute's comment: “properness of the scheme-theoretic image”. References: EGA II (5.4.9), “5.4.3(ii), special case”.
Stacks 0AH6, properness. The scheme-theoretic image in a separated scheme locally of finite type over the base of a universally closed morphism to the base is proper over the base.
lemma isProper_imageι_comp {X Y S : Scheme.{u}} (h : X ⟶ Y) (g : Y ⟶ S)
[UniversallyClosed (h ≫ g)] [IsSeparated g] [LocallyOfFiniteType g] :
IsProper (h.imageι ≫ g)
AlgebraicGeometry.surjective_toImage, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/SchemeTheoreticImage.lean, line 55. The attribute's comment: “surjectivity onto the scheme-theoretic image”.
Stacks 0AH6, surjectivity. Under the separatedness hypothesis, the canonical morphism to the scheme-theoretic image of a universally closed composite is surjective.
lemma surjective_toImage {X Y S : Scheme.{u}} (h : X ⟶ Y) (g : Y ⟶ S)
[UniversallyClosed (h ≫ g)] [IsSeparated g] : Surjective h.toImage
Tag 09MQ, a lemma
Tag 09MQ in the Stacks Project.
AlgebraicGeometry.quasiSeparated_of_surjective_universallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/QuasiSeparated.lean, line 46. The attribute's comment: “quasi_separated_over_s”.
Stacks Project, Tag 09MQ (quasi-separated over the base). Quasi-separatedness over a base descends along a surjective universally closed morphism of schemes.
theorem quasiSeparated_of_surjective_universallyClosed {S : Scheme.{u}} {X Y : Over S}
(f : X ⟶ Y) [Surjective f.left] [UniversallyClosed f.left] [QuasiSeparated X.hom] :
QuasiSeparated Y.hom
AlgebraicGeometry.quasiSeparatedSpace_of_surjective_universallyClosed, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/QuasiSeparated.lean, line 80. The attribute's comment: “quasi_separated_scheme”.
Stacks Project, Tag 09MQ (scheme part). The target of a surjective universally closed morphism from a quasi-separated scheme is quasi-separated.
lemma quasiSeparatedSpace_of_surjective_universallyClosed
{X Y : Scheme.{u}} (f : X ⟶ Y) [Surjective f] [UniversallyClosed f]
[QuasiSeparatedSpace X] : QuasiSeparatedSpace Y
AlgebraicGeometry.isSeparated_of_surjective_universallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/SeparatedDescent.lean, line 81. The attribute's comment: “separated_over_s”. References: SGA 3 V (7.4).
Stacks Project, Tag 09MQ (separated over the base). Separatedness over a base descends along a surjective universally closed morphism of schemes.
theorem isSeparated_of_surjective_universallyClosed {S : Scheme.{u}} {X Y : Over S}
(f : X ⟶ Y) [Surjective f.left] [UniversallyClosed f.left] [IsSeparated X.hom] :
IsSeparated Y.hom
AlgebraicGeometry.Scheme.isSeparated_of_surjective_universallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/SeparatedDescent.lean, line 101. The attribute's comment: “separated_scheme”. References: SGA 3 V (7.4), “special case”.
Stacks Project, Tag 09MQ (separated scheme). A scheme receiving a surjective universally closed morphism from a separated scheme is itself separated.
This is the absolute form of
AlgebraicGeometry.isSeparated_of_surjective_universallyClosed, obtained by taking the base to be the terminal scheme.
theorem Scheme.isSeparated_of_surjective_universallyClosed {X Y : Scheme.{u}} (f : X ⟶ Y)
[Surjective f] [UniversallyClosed f] [X.IsSeparated] : Y.IsSeparated
Sources
Section29.43 Valuative criteria#
Section 29.43 of the Stacks Project, Tag 0BX4. 4 tags here are carried by 10 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0894, a lemma
Tag 0894 in the Stacks Project.
AlgebraicGeometry.universallyClosed_of_unique_lift_of_denseRange, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/DifferentialsAndValuative/ValuativeCriterionRefined.lean, line 542. The attribute's comment: “universally closed conclusion”.
Stacks 0894, universally closed part. Let
f : X ⟶ Sandh : U ⟶ Xbe quasi-compact morphisms of schemes and suppose thath(U)is dense inX. If every valuative square forfwhose generic-point map factors throughhhas a unique lift, thenfis universally closed.
public lemma universallyClosed_of_unique_lift_of_denseRange
{U X S : AlgebraicGeometry.Scheme.{u}}
(h : U ⟶ X) (f : X ⟶ S) [AlgebraicGeometry.QuasiCompact f]
[AlgebraicGeometry.QuasiCompact h] (hdense : DenseRange h)
(hvaluative : ∀ (D : AlgebraicGeometry.ValuativeCommSq f)
(g : AlgebraicGeometry.Spec (.of D.K) ⟶ U),
g ≫ h = D.i₁ → Nonempty (Unique D.commSq.LiftStruct)) :
AlgebraicGeometry.UniversallyClosed f
AlgebraicGeometry.isSeparated_of_unique_lift_of_denseRange, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/DifferentialsAndValuative/ValuativeCriterionRefined.lean, line 606. The attribute's comment: “separated conclusion”.
Stacks 0894, separated part. Under the hypotheses of the refined valuative criterion, a quasi-separated morphism
fis separated.
public lemma isSeparated_of_unique_lift_of_denseRange
{U X S : AlgebraicGeometry.Scheme.{u}}
(h : U ⟶ X) (f : X ⟶ S) [AlgebraicGeometry.QuasiCompact f]
[AlgebraicGeometry.QuasiCompact h] [AlgebraicGeometry.QuasiSeparated f]
(hdense : DenseRange h)
(hvaluative : ∀ (D : AlgebraicGeometry.ValuativeCommSq f)
(g : AlgebraicGeometry.Spec (.of D.K) ⟶ U),
g ≫ h = D.i₁ → Nonempty (Unique D.commSq.LiftStruct)) :
AlgebraicGeometry.IsSeparated f
Tag 0895, a remark
Tag 0895 in the Stacks Project.
AlgebraicGeometry.refinedValuative_unique_iff_hasLift_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/DifferentialsAndValuative/ValuativeCriterionRefinedNecessity.lean, line 55. The attribute's comment: “uniqueness of the dotted arrows is guaranteed when f is separated”.
If
fis separated, the dotted arrows in the refined valuative criterion are automatically unique: every valuative square forfwhose generic-point map factors throughhhas a unique lift as soon as it has one.
public theorem refinedValuative_unique_iff_hasLift_of_isSeparated
{U X S : Scheme.{u}} (h : U ⟶ X) (f : X ⟶ S) [IsSeparated f] :
(∀ (D : ValuativeCommSq f) (g : Spec (.of D.K) ⟶ U),
g ≫ h = D.i₁ → Nonempty (Unique D.commSq.LiftStruct)) ↔
(∀ (D : ValuativeCommSq f) (g : Spec (.of D.K) ⟶ U),
g ≫ h = D.i₁ → D.commSq.HasLift)
AlgebraicGeometry.exists_hasLift_of_denseRange_not_universallyClosed_not_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/DifferentialsAndValuative/ValuativeCriterionRefinedNecessity.lean, line 355. The attribute's comment: “the uniqueness assumption of Lemma 0894 is necessary”.
The uniqueness of the dotted arrows in the refined valuative criterion
universallyClosed_of_unique_lift_of_denseRangecannot be dropped. There are quasi-compact morphismsf : X ⟶ Sandh : U ⟶ X, withfquasi-separated andh(U)dense inX, such that every commutative square fromSpec K ⟶ Spec A(withAa valuation ring with fraction fieldK) whose top map factors throughhadmits a dotted arrow, whilefis neither universally closed nor separated.
public theorem exists_hasLift_of_denseRange_not_universallyClosed_not_isSeparated :
∃ (U X S : Scheme.{u}) (h : U ⟶ X) (f : X ⟶ S),
QuasiCompact f ∧ QuasiCompact h ∧ QuasiSeparated f ∧ DenseRange h ∧
(∀ (D : ValuativeCommSq f) (g : Spec (.of D.K) ⟶ U),
g ≫ h = D.i₁ → D.commSq.HasLift) ∧
¬ UniversallyClosed f ∧ ¬ IsSeparated f
Tag 0BX6, a lemma
Tag 0BX6 in the Stacks Project.
AlgebraicGeometry.exists_open_morphism_inducing_localHom_of_isReduced, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Valuative/LocalExtension.lean, line 257. The attribute's comment: “local_extension”. References: EGA I (6.5.1), “(ii), X reduced case”.
A compatible local homomorphism is induced by a morphism on an open neighbourhood when the target is locally of finite type and the source is reduced with finitely many irreducible components.
lemma exists_open_morphism_inducing_localHom_of_isReduced
{S X Y : Scheme.{u}} (pX : X ⟶ S) (pY : Y ⟶ S)
(s : S) (x : X) (y : Y) (hx : pX x = s) (hy : pY y = s)
(phi : Y.presheaf.stalk y →+* X.presheaf.stalk x)
(hphi : IsLocalHom phi)
(hphiS : phi.comp
((pY.stalkMap y).hom.comp
(eqToHom (congrArg (fun z ↦ S.presheaf.stalk z) hy).symm).hom) =
(pX.stalkMap x).hom.comp
(eqToHom (congrArg (fun z ↦ S.presheaf.stalk z) hx).symm).hom)
(hft : LocallyOfFiniteType pY) (hred : IsReduced X)
(hcomp : (irreducibleComponents X).Finite) :
∃ (U : X.Opens) (hxU : x ∈ U) (f : (U : Scheme.{u}) ⟶ Y)
(_hf : f ≫ pY = U.ι ≫ pX)
(hfy : f ⟨x, hxU⟩ = y),
((U.stalkIso ⟨x, hxU⟩).hom.hom.comp
((f.stalkMap ⟨x, hxU⟩).hom.comp
(eqToHom (congrArg (fun z ↦ Y.presheaf.stalk z) hfy).symm).hom)) = phi
AlgebraicGeometry.exists_open_morphism_inducing_localHom_of_isIntegral, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Valuative/LocalExtension.lean, line 282. The attribute's comment: “local_extension, Y locally of finite type and X integral”.
A compatible local homomorphism is induced by a morphism on an open neighbourhood when the target is locally of finite type over the base and the source is integral.
lemma exists_open_morphism_inducing_localHom_of_isIntegral
{S X Y : Scheme.{u}} (pX : X ⟶ S) (pY : Y ⟶ S)
(s : S) (x : X) (y : Y) (hx : pX x = s) (hy : pY y = s)
(phi : Y.presheaf.stalk y →+* X.presheaf.stalk x)
(hphi : IsLocalHom phi)
(hphiS : phi.comp
((pY.stalkMap y).hom.comp
(eqToHom (congrArg (fun z ↦ S.presheaf.stalk z) hy).symm).hom) =
(pX.stalkMap x).hom.comp
(eqToHom (congrArg (fun z ↦ S.presheaf.stalk z) hx).symm).hom)
(hft : LocallyOfFiniteType pY) (hint : IsIntegral X) :
∃ (U : X.Opens) (hxU : x ∈ U) (f : (U : Scheme.{u}) ⟶ Y)
(_hf : f ≫ pY = U.ι ≫ pX)
(hfy : f ⟨x, hxU⟩ = y),
((U.stalkIso ⟨x, hxU⟩).hom.hom.comp
((f.stalkMap ⟨x, hxU⟩).hom.comp
(eqToHom (congrArg (fun z ↦ Y.presheaf.stalk z) hfy).symm).hom)) = phi
AlgebraicGeometry.exists_open_morphism_inducing_localHom_of_isLocallyNoetherian, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Valuative/LocalExtension.lean, line 305. The attribute's comment: “local_extension, Y locally of finite type and X locally Noetherian”.
A compatible local homomorphism is induced by a morphism on an open neighbourhood when the target is locally of finite type over the base and the source is locally Noetherian.
lemma exists_open_morphism_inducing_localHom_of_isLocallyNoetherian
{S X Y : Scheme.{u}} (pX : X ⟶ S) (pY : Y ⟶ S)
(s : S) (x : X) (y : Y) (hx : pX x = s) (hy : pY y = s)
(phi : Y.presheaf.stalk y →+* X.presheaf.stalk x)
(hphi : IsLocalHom phi)
(hphiS : phi.comp
((pY.stalkMap y).hom.comp
(eqToHom (congrArg (fun z ↦ S.presheaf.stalk z) hy).symm).hom) =
(pX.stalkMap x).hom.comp
(eqToHom (congrArg (fun z ↦ S.presheaf.stalk z) hx).symm).hom)
(hft : LocallyOfFiniteType pY) (hnoeth : IsLocallyNoetherian X) :
∃ (U : X.Opens) (hxU : x ∈ U) (f : (U : Scheme.{u}) ⟶ Y)
(_hf : f ≫ pY = U.ι ≫ pX)
(hfy : f ⟨x, hxU⟩ = y),
((U.stalkIso ⟨x, hxU⟩).hom.hom.comp
((f.stalkMap ⟨x, hxU⟩).hom.comp
(eqToHom (congrArg (fun z ↦ Y.presheaf.stalk z) hfy).symm).hom)) = phi
AlgebraicGeometry.exists_open_morphism_inducing_localHom_of_locallyOfFinitePresentation, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Valuative/LocalExtensionFinitePresentation.lean, line 270. The attribute's comment: “local_extension”. References: EGA I (6.5.1), “(ii)”.
Stacks Project, Tag 0BX6 (local extension), finite-presentation case. A compatible local homomorphism of local rings is induced by a morphism on an open neighbourhood.
public lemma exists_open_morphism_inducing_localHom_of_locallyOfFinitePresentation
{S X Y : Scheme.{u}} (pX : X ⟶ S) (pY : Y ⟶ S)
(s : S) (x : X) (y : Y) (hx : pX x = s) (hy : pY y = s)
(phi : Y.presheaf.stalk y →+* X.presheaf.stalk x)
(hphi : IsLocalHom phi)
(hphiS : phi.comp
((pY.stalkMap y).hom.comp
(eqToHom (congrArg (fun z ↦ S.presheaf.stalk z) hy).symm).hom) =
(pX.stalkMap x).hom.comp
(eqToHom (congrArg (fun z ↦ S.presheaf.stalk z) hx).symm).hom)
(hfin : LocallyOfFinitePresentation pY) :
∃ (U : X.Opens) (hxU : x ∈ U) (f : (U : Scheme.{u}) ⟶ Y)
(_hf : f ≫ pY = U.ι ≫ pX)
(hfy : f ⟨x, hxU⟩ = y),
((U.stalkIso ⟨x, hxU⟩).hom.hom.comp
((f.stalkMap ⟨x, hxU⟩).hom.comp
(eqToHom (congrArg (fun z ↦ Y.presheaf.stalk z) hfy).symm).hom)) = phi
AlgebraicGeometry.exists_open_eq_of_stalkMap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Valuative/LocalUniqueness.lean, line 176. The attribute's comment: “local_uniqueness”. References: EGA I (6.5.1), “(i)”.
Two morphisms over a scheme which agree on the local ring at a point agree on some open neighbourhood of that point, provided the target is locally of finite type over the base, or the source is integral, locally Noetherian, or reduced with finitely many irreducible components.
theorem exists_open_eq_of_stalkMap_eq
{S X Y : Scheme.{u}} (pX : X ⟶ S) (pY : Y ⟶ S) (f g : X ⟶ Y)
(hf : f ≫ pY = pX) (hg : g ≫ pY = pX)
(s : S) (x : X) (y : Y) (hxs : pX x = s) (hys : pY y = s)
(hfx : f x = y) (hgx : g x = y)
(hfg : f.stalkMap x =
Y.presheaf.stalkSpecializes
(Inseparable.of_eq (hfx.trans hgx.symm).symm).specializes ≫ g.stalkMap x)
(h : LocallyOfFiniteType pY ∨ IsIntegral X ∨ IsLocallyNoetherian X ∨
(IsReduced X ∧ (irreducibleComponents X).Finite)) :
∃ U : X.Opens, x ∈ U ∧ U.ι ≫ f = U.ι ≫ g
Tag 0BX7, a lemma
Tag 0BX7 in the Stacks Project.
AlgebraicGeometry.exists_open_extension_of_valuationRing_stalk, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Valuative/Extension.lean, line 209.
Stacks Project, Tag 0BX7. A morphism from an open subscheme extends across a point whose local ring is a valuation ring, provided the target is proper over the base and the source is either reduced with finitely many irreducible components or Noetherian.
lemma exists_open_extension_of_valuationRing_stalk
{S X Y : Scheme.{u}} (pX : X ⟶ S) (pY : Y ⟶ S)
(x : X) (U : X.Opens) (f : (U : Scheme.{u}) ⟶ Y)
(hf : f ≫ pY = U.ι ≫ pX)
(hxU : x ∈ closure (U : Set X))
(hX : (IsReduced X ∧ (irreducibleComponents X).Finite) ∨
IsNoetherian X)
[IsDomain (X.presheaf.stalk x)] [ValuationRing (X.presheaf.stalk x)]
[IsProper pY] :
∃ (U' : X.Opens) (hUU' : U ≤ U') (_ : x ∈ U')
(f' : (U' : Scheme.{u}) ⟶ Y),
f' ≫ pY = U'.ι ≫ pX ∧ X.homOfLE hUU' ≫ f' = f
Sources
Section29.44 Projective morphisms#
Section 29.44 of the Stacks Project, Tag 01W7. 18 tags here are carried by 29 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 01W8, a definition
Tag 01W8 in the Stacks Project.
AlgebraicGeometry.IsProjective, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/Basic.lean, line 170. The attribute's comment: “projective”. References: EGA II (5.5.2).
Stacks Project, Tag 01W8, first condition. A morphism
f : X ⟶ Sis projective ifXis isomorphic, as a scheme overS, to a closed subscheme of the projective bundle𝐏(ℰ) = Proj_S(Sym(ℰ))of some quasi-coherent𝒪_S-moduleℰof finite type — equivalently, if there is a closed immersioni : X ⟶ 𝐏(ℰ)withifollowed by the projection equal tof.
def IsProjective (f : X ⟶ S) : Prop
AlgebraicGeometry.IsLocallyProjective, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/Basic.lean, line 221. The attribute's comment: “locally projective”.
Stacks Project, Tag 01W8, third condition. A morphism
f : X ⟶ Sis locally projective if the base is covered by opens over each of which the restriction offis projective.
def IsLocallyProjective (f : X ⟶ S) : Prop
AlgebraicGeometry.IsProjectiveMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/Projective.lean, line 108. The attribute's comment: “H-projective”.
Stacks Project, Tag 01W8 (H-projective). A morphism
f : X ⟶ Sis H-projective if for somenthere is a closed immersionX ⟶ ℙⁿ_SoverS.
def IsProjectiveMorphism (f : X ⟶ S) : Prop
Tag 07ZS, an example
Tag 07ZS in the Stacks Project.
AlgebraicGeometry.isProjective_relativeProj_toBase_and_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/RelativeProj.lean, line 56.
Stacks Project, Example 07ZS. Let
Sbe a scheme and𝒜a quasi-coherent graded𝒪_S-algebra generated by𝒜_1over𝒜_0, with𝒜_1of finite type over𝒪_S, and letX = Proj_S(𝒜). ThenX ⟶ Sis projective (Tag 01W8), and the morphismX ⟶ 𝐏(𝒜_1) = Proj_S(Sym(𝒜_1))associated to the canonical graded𝒪_S-algebra mapSym(𝒜_1) ⟶ 𝒜is a closed immersion overS.The three conjuncts are, in order: projectivity of the projection of
Proj_S(𝒜); the closed immersionStacks.Tag01VMRelativeVeryAmple.canonicalSymProjHom, which is Tag 07ZK (2) for the canonical map; and its compatibility with the projections toS. The first is Tag 0B3U,AlgebraicGeometry.isProjective_relativeProj_toBase, which is proved from the other two.
theorem isProjective_relativeProj_toBase_and_isClosedImmersion {S : Scheme.{u}}
(A : SheafGradedAlgebra.{u} S)
(hgen : Stacks.AlgebraicGeometry.ProjRepresentsF1.IsGeneratedInDegreeOne A)
(hfin : (A.piece 1).IsFiniteType) :
IsProjective (relativeProj A).toBase ∧
IsClosedImmersion (Stacks.Tag01VMRelativeVeryAmple.canonicalSymProjHom A hgen) ∧
Stacks.Tag01VMRelativeVeryAmple.canonicalSymProjHom A hgen ≫
(Stacks.SymGraded.schemeProjectiveBundle (A.piece 1)
(Stacks.SymGraded.isQuasicoherentPieces_of_isQuasicoherent (A.piece 1))).toBase =
(relativeProj A).toBase
Tag 01W9, a lemma
Tag 01W9 in the Stacks Project.
AlgebraicGeometry.IsProjectiveMorphism.isHQuasiProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiProjective/HProjective.lean, line 125. The attribute's comment: “H-quasi-projective”.
Stacks Project, Tag 01W9, first clause. An H-projective morphism is H-quasi-projective: the closed immersion into
ℙⁿ_Switnessing H-projectivity is an immersion, and it is quasi-compact because a closed immersion is affine.
theorem IsProjectiveMorphism.isHQuasiProjective (hf : IsProjectiveMorphism f) :
IsHQuasiProjective f
AlgebraicGeometry.IsProjectiveMorphism.isProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiProjective/HProjective.lean, line 139. The attribute's comment: “projective”.
Stacks Project, Tag 01W9, second clause. An H-projective morphism is projective.
Projective
n-space overSis the projective bundle of the free module𝒪_S^{n+1}, which is quasi-coherent and of finite type; so the closed immersionX ⟶ ℙⁿ_SoverSwitnessing H-projectivity becomes, after composing with the inverse of the isomorphism𝐏(𝒪_S^{n+1}) ≅ ℙⁿ_Sof [Stacks, Tag 01OE], a closed immersion ofXinto that projective bundle overS.
theorem IsProjectiveMorphism.isProjective (hf : IsProjectiveMorphism f) : IsProjective f
Tag 01WB, a lemma
Tag 01WB in the Stacks Project.
Stacks.LocallyProjectiveHProjective.isLocallyProjectiveMorphism_of_isLocallyProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocallyProjectiveHProjective/Sym.lean, line 274. The attribute's comment: “(1) ⟹ (2): locally projective implies locally H-projective”.
Stacks Project, Tag 01WB, the implication (1) ⟹ (2). A locally projective morphism is H-projective over the members of an open covering of its base.
Over each member
Uof the covering witnessing local projectivity the morphism is projective, so over each affine openVofUit is H-projective; and the images of those affine opens, over all members of the covering, cover the base.
theorem isLocallyProjectiveMorphism_of_isLocallyProjective (hf : IsLocallyProjective f) :
IsLocallyProjectiveMorphism f
Stacks.LocallyProjectiveHProjective.isLocallyProjective_iff_isLocallyProjectiveMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocallyProjectiveHProjective/Sym.lean, line 298.
Stacks Project, Tag 01WB. A morphism of schemes is locally projective if and only if its base is covered by opens over which it is H-projective.
theorem isLocallyProjective_iff_isLocallyProjectiveMorphism :
IsLocallyProjective f ↔ IsLocallyProjectiveMorphism f
AlgebraicGeometry.isLocallyProjective_of_isLocallyProjectiveMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiProjective/HProjective.lean, line 238. The attribute's comment: “the implication from a local H-projective cover”.
Stacks Project, Tag 01WB, the implication (2) ⟹ (1). If the base is covered by opens over each of which
fis H-projective, thenfis locally projective.The opens are the ranges of the maps of the covering, which cover the base; over each of them the base change of
fis isomorphic, as an arrow, to the restriction off, so the restriction is H-projective, hence projective by the second clause of [Stacks, Tag 01W9].
theorem isLocallyProjective_of_isLocallyProjectiveMorphism (hf : IsLocallyProjectiveMorphism f) :
IsLocallyProjective f
Tag 01WC, a lemma
Tag 01WC in the Stacks Project.
AlgebraicGeometry.isProper_of_isLocallyProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/LocallyProjective.lean, line 43.
Stacks Project, Tag 01WC. A locally projective morphism is proper.
Tag 01WB turns local projectivity into local H-projectivity, and a locally H-projective morphism is proper.
theorem isProper_of_isLocallyProjective (hf : IsLocallyProjective f) : IsProper f
Tag 0B5N, a lemma
Tag 0B5N in the Stacks Project.
Stacks.ProperRelativeAmpleProjective.isLocallyProjective_of_isProper_of_exists_isRelativelyAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperRelativeAmpleProjective/Basic.lean, line 191.
[Stacks, Tag 0B5N]. Let
f : X ⟶ Sbe a proper morphism of schemes. If there exists anf-ample invertible𝒪_X-module, thenfis locally projective.
theorem isLocallyProjective_of_isProper_of_exists_isRelativelyAmple {X S : Scheme.{u}}
(f : X ⟶ S) [IsProper f]
(hL : ∃ (L : X.Modules) (h : IsInvertibleModule X L),
letI := h; Stacks.RelativeAmple.IsRelativelyAmple f L) :
IsLocallyProjective f
Tag 01WE, a lemma
Tag 01WE in the Stacks Project.
AlgebraicGeometry.IsProjectiveMorphism.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/Projective.lean, line 183.
Stacks Project, Tag 01WE. A composition of H-projective morphisms is H-projective.
Closed immersions
i : X ⟶ ℙⁿ_YoverYandj : Y ⟶ ℙᵐ_ZoverZare composed as follows. The identificationℙⁿ_Z ×_Z Y ≅ ℙⁿ_Yturnsiinto a closed immersion ofXintoℙⁿ_Z ×_Z Y; base changingjalongℙⁿ_Z ⟶ Zembeds that closed intoℙⁿ_Z ×_Z ℙᵐ_Z; and the Segre embedding of [Stacks, Tag 01WD] embeds the product closed intoℙ^{nm+n+m}_Z.
theorem comp {Y Z : Scheme.{u}} {f : X ⟶ Y} {g : Y ⟶ Z} (hf : IsProjectiveMorphism f)
(hg : IsProjectiveMorphism g) : IsProjectiveMorphism (f ≫ g)
Tag 01WF, a lemma
Tag 01WF in the Stacks Project.
AlgebraicGeometry.IsProjectiveMorphism.baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/Projective.lean, line 161.
Stacks Project, Tag 01WF. H-projectivity is stable under base change. A closed immersion
X ⟶ ℙⁿ_SoverSbase changes to a closed immersionX ×_S T ⟶ ℙⁿ_S ×_S T ≅ ℙⁿ_ToverT.
theorem baseChange {f : X ⟶ S} (hf : IsProjectiveMorphism f) {T : Scheme.{u}} (g : T ⟶ S) :
IsProjectiveMorphism (pullback.snd f g)
Tag 02V6, a lemma
Tag 02V6 in the Stacks Project.
AlgebraicGeometry.IsProjective.pullback_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/BaseChange.lean, line 236. The attribute's comment: “projective”.
A base change of a projective morphism is projective. For
f : X ⟶ Sprojective andg : S' ⟶ Sarbitrary, the first projectionS' ×_S X ⟶ S'is projective.
theorem IsProjective.pullback_fst
{X S S' : Scheme.{u}} {f : X ⟶ S} (g : S' ⟶ S) (hf : IsProjective f) :
IsProjective (pullback.fst g f)
AlgebraicGeometry.IsLocallyProjective.pullback_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/BaseChange.lean, line 324. The attribute's comment: “locally projective”.
A base change of a locally projective morphism is locally projective. For
f : X ⟶ Slocally projective andg : S' ⟶ Sarbitrary, the first projectionS' ×_S X ⟶ S'is locally projective.The covering of
S'is the inverse image of the covering ofSover whose membersfis projective: overg ⁻¹ᵁ U ithe restriction of the base change is a base change of the restriction offoverU i.
theorem IsLocallyProjective.pullback_fst
{X S S' : Scheme.{u}} {f : X ⟶ S} (g : S' ⟶ S) (hf : IsLocallyProjective f) :
IsLocallyProjective (pullback.fst g f)
Tag 07RL, a lemma
Tag 07RL in the Stacks Project.
AlgebraicGeometry.isQuasiProjective_of_isProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/Composition.lean, line 116. The attribute's comment: “over a quasi-compact quasi-separated base, the forward half of clause (1) of Tag 0BCL; the source states the tag over an arbitrary base”.
Stacks Project, Tag 07RL over a quasi-compact quasi-separated base. A projective morphism is quasi-projective. This is the forward half of clause (1) of Tag 0BCL, which
AlgebraicGeometry.isProjective_iff_isQuasiProjective_and_isProperproves over such a base.
theorem isQuasiProjective_of_isProjective
{X S : Scheme.{u}} [CompactSpace S] [QuasiSeparatedSpace S] {f : X ⟶ S}
(hf : IsProjective f) : IsQuasiProjective f
AlgebraicGeometry.IsProjective.isQuasiProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundleProperFiniteType/Basic.lean, line 219.
Stacks Project, Tag 07RL. A projective morphism is quasi-projective. Properness supplies the finite-type half, and the
f-very ample module ofAlgebraicGeometry.IsProjective.exists_isRelativelyVeryAmpleisf-ample by [Stacks, Tag 01VN],fbeing quasi-compact. No hypothesis on the base is used, which is how the source states the tag.It is also clause (5) of [Stacks, Tag 0B43], which the source proves by citing Tag 07RL: membership of
Xin the categoryQP_Sof that tag isAlgebraicGeometry.IsQuasiProjective X.hom, so "ifX ⟶ Sis projective thenX ∈ QP_S" is this statement. Tag 0B43's hypothesis thatScarries an ample invertible sheaf is not needed for it and is not assumed.
theorem IsProjective.isQuasiProjective {f : X ⟶ S} (hf : IsProjective f) :
IsQuasiProjective f
Tag 01WA, a lemma
Tag 01WA in the Stacks Project.
AlgebraicGeometry.exists_isOpenImmersion_isProjectiveMorphism_of_isHQuasiProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiProjective/HProjective.lean, line 186.
Stacks Project, Tag 01WA. An H-quasi-projective morphism factors as an open immersion followed by an H-projective morphism.
H-quasi-projectivity gives a quasi-compact immersion
i : X ⟶ ℙⁿ_SoverS. Being quasi-compact,iis an open immersion onto its scheme-theoretic imageX'by [Stacks, Tag 01RG], which is the only place the quasi-compactness is used; andX'is a closed subscheme ofℙⁿ_S, so its structure morphismX' ⟶ Sis H-projective.
theorem exists_isOpenImmersion_isProjectiveMorphism_of_isHQuasiProjective
(hf : IsHQuasiProjective f) :
∃ (X' : Scheme.{u}) (j : X ⟶ X') (p : X' ⟶ S),
IsOpenImmersion j ∧ IsProjectiveMorphism p ∧ j ≫ p = f
Tag 07RM, a lemma
Tag 07RM in the Stacks Project.
Stacks.QuasiProjectiveCompactification.exists_isOpenImmersion_isProjective_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiProjectiveCompactification/Projective.lean, line 248.
[Stacks, Tag 07RM]. Let
f : X ⟶ Sbe a quasi-projective morphism withSquasi-compact and quasi-separated. Thenffactors asX ⟶ X' ⟶ SwhereX ⟶ X'is an open immersion andX' ⟶ Sis projective, in the sense of clause (1) of Definition 01W8.Half 1 of the source's proof is
Stacks.QuasiProjectiveCompactification.immersionIntoProjective_isProjective; half 2, the factorisation of a quasi-compact immersion through the closure of its image, isStacks.QuasiProjectiveCompactification.exists_isOpenImmersion_isProjective, whose two conditions on the projectivity predicate are discharged byAlgebraicGeometry.IsProjective.isSeparatedandStacks.QuasiProjectiveCompactification.isProjective_comp_of_isClosedImmersion.
theorem exists_isOpenImmersion_isProjective_of_qcqs {X S : Scheme.{u}} (f : X ⟶ S)
[CompactSpace S] [QuasiSeparatedSpace S] (hf : AlgebraicGeometry.IsQuasiProjective f) :
∃ (X' : Scheme.{u}) (j : X ⟶ X') (p : X' ⟶ S),
IsOpenImmersion j ∧ IsProjective p ∧ j ≫ p = f
Tag 0BCL, a lemma
Tag 0BCL in the Stacks Project.
AlgebraicGeometry.isProjective_iff_isQuasiProjective_and_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/Composition.lean, line 103. The attribute's comment: “(1)”. References: EGA II (5.5.3), “more general”.
Stacks Project, Tag 0BCL, clause (1). A morphism of schemes
f : X ⟶ Sto a quasi-compact quasi-separated scheme is projective — in the sense ofAlgebraicGeometry.IsProjective, a closed immersion overSinto the projective bundle of a quasi-coherent module of finite type — if and only if it is quasi-projective and proper.Forwards this is Tags 07RL and 01WC, which need no hypothesis on
S. Backwards, Tag 07RM factorsfas an open immersion followed by a projective morphism, andAlgebraicGeometry.isProjective_comp_of_isOpenImmersion_of_isProperconcludes.
theorem isProjective_iff_isQuasiProjective_and_isProper {X S : Scheme.{u}} [CompactSpace S]
[QuasiSeparatedSpace S] (f : X ⟶ S) :
IsProjective f ↔ IsQuasiProjective f ∧ IsProper f
AlgebraicGeometry.isProjectiveMorphism_iff_isHQuasiProjective_and_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiProjective/HProjective.lean, line 165. The attribute's comment: “(2)”. References: EGA II (5.5.3), “(i)+(ii) in H-form”; EGA II (7.3.9), “special case”.
Stacks Project, Tag 0BCL, clause (2). A morphism of schemes is H-projective if and only if it is H-quasi-projective and proper.
Forwards, an H-projective morphism is proper and H-quasi-projective. Backwards, let
i : X ⟶ ℙⁿ_Sbe an immersion overSwithi ≫ (ℙⁿ_S ↘ S) = fproper. The structure morphism ofℙⁿ_Sis separated, soiis proper, hence a closed map; an immersion with closed image is a closed immersion.The base carries no quasi-compactness or quasi-separatedness hypothesis; see the implementation notes of this file.
theorem isProjectiveMorphism_iff_isHQuasiProjective_and_isProper :
IsProjectiveMorphism f ↔ IsHQuasiProjective f ∧ IsProper f
Tag 0C4P, a lemma
Tag 0C4P in the Stacks Project.
AlgebraicGeometry.IsProjective.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/Composition.lean, line 149.
Stacks Project, Tag 0C4P. A composition of projective morphisms over a quasi-compact quasi-separated base is projective. For
f : X ⟶ Yandg : Y ⟶ Sprojective andSquasi-compact and quasi-separated, the compositionf ≫ gis projective.The proof is the source's. A projective morphism is quasi-projective and proper (Tags 07RL and 01WC), so
fandgare; a composition of proper morphisms is proper, and a composition of quasi-projective morphisms with quasi-compact target is quasi-projective (Tag 0C4M); clause (1) of Tag 0BCL,AlgebraicGeometry.isProjective_iff_isQuasiProjective_and_isProper, at the baseSreturns projectivity off ≫ g.
theorem IsProjective.comp {X Y S : Scheme.{u}} [CompactSpace S] [QuasiSeparatedSpace S]
{f : X ⟶ Y} {g : Y ⟶ S} (hf : IsProjective f) (hg : IsProjective g) :
IsProjective (f ≫ g)
Tag 0C4Q, a lemma
Tag 0C4Q in the Stacks Project.
AlgebraicGeometry.IsProjective.of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/BaseChange.lean, line 290. The attribute's comment: “projective case: closed immersion over the base into the projective bundle 𝐏(ℰ) of a quasi-coherent module of finite type, i.e. clause (1) of Definition 01W8; no hypothesis beyond the separatedness of g that the source states”.
If
f ≫ gis projective andgis separated thenfis projective. Here projective isAlgebraicGeometry.IsProjective, clause (1) of Definition 01W8: a closed immersion over the base into the projective bundle𝐏(ℰ)of a quasi-coherent module of finite type. The H-projective form, clause (2), isAlgebraicGeometry.IsProjectiveMorphism.of_comp.
theorem IsProjective.of_comp {X Y S : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ S) [IsSeparated g]
(h : IsProjective (f ≫ g)) : IsProjective f
AlgebraicGeometry.IsProjectiveMorphism.of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/Projective.lean, line 223. The attribute's comment: “H-projective case”.
Stacks Project, Tag 0C4Q, H-projective case. If
f ≫ gis H-projective andgis separated thenfis H-projective.The closed immersion
i : X ⟶ ℙⁿ_SoverSlifts tok : X ⟶ ℙⁿ_S ×_S Ybecauseiandfagree overS. The first projection of that fibre product is a base change ofg, hence separated, andkcomposed with it isi; sokis a closed immersion byAlgebraicGeometry.IsClosedImmersion.of_comp. Finallyℙⁿ_S ×_S Y ≅ ℙⁿ_YoverY.
theorem of_comp {Y : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ S) [IsSeparated g]
(h : IsProjectiveMorphism (f ≫ g)) : IsProjectiveMorphism f
Tag 087S, a lemma
Tag 087S in the Stacks Project.
Stacks.HProjective.isHQuasiProjective_of_isQuasiProjective_of_exists_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/HProjective/AmpleBase.lean, line 83. The attribute's comment: “part (2)”. References: EGA II (5.3.3), “more general”.
A quasi-projective morphism to a scheme admitting an ample invertible module is H-quasi-projective: it admits a quasi-compact immersion into a projective space over the base.
Quasi-projectivity is finite type together with an invertible module ample relative to the morphism, and H-quasi-projectivity is a quasi-compact immersion into
ℙⁿ_SoverS.
theorem isHQuasiProjective_of_isQuasiProjective_of_exists_isAmple {X S : Scheme.{u}} (f : X ⟶ S)
(hS : ∃ (M : S.Modules) (h : Stacks.Ample.IsInvertibleModule S M),
letI := h; Stacks.Ample.IsAmple S M)
(hf : AlgebraicGeometry.IsQuasiProjective f) : AlgebraicGeometry.IsHQuasiProjective f
AlgebraicGeometry.isHQuasiProjective_of_isQuasiProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/QuasiProjectiveOverAmpleBase.lean, line 203. The attribute's comment: “part (2)”.
Stacks Project, Tag 087S, part (2). Over a base carrying an ample invertible module, a quasi-projective morphism is H-quasi-projective.
The relatively ample module of quasi-projectivity and the ample module on the base combine into an absolutely ample module on
Xby [Stacks, Tag 0892] part (1), and [Stacks, Tag 01VS] turns that into a quasi-compact immersion intoℙⁿ_SoverS.
theorem isHQuasiProjective_of_isQuasiProjective (f : X ⟶ S) (M : S.Modules)
[Stacks.Ample.IsInvertibleModule S M] (hM : Stacks.Ample.IsAmple S M)
(hf : IsQuasiProjective f) : IsHQuasiProjective f
AlgebraicGeometry.isProjectiveMorphism_of_isProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/QuasiProjectiveOverAmpleBase.lean, line 217. The attribute's comment: “part (1)”.
Stacks Project, Tag 087S, part (1). Over a base carrying an ample invertible module, a projective morphism is H-projective.
AlgebraicGeometry.IsProjective.isQuasiProjective_and_isPropermakesfquasi-projective and proper, from [Stacks, Tag 07RL] and [Stacks, Tag 01WC]; part (2) makes it H-quasi-projective; and clause (2) of [Stacks, Tag 0BCL] turns H-quasi-projective and proper into H-projective. Nothing is assumed beyond the source's hypothesis thatMis an ample invertible module onS.
theorem isProjectiveMorphism_of_isProjective
(f : X ⟶ S) (M : S.Modules) [Stacks.Ample.IsInvertibleModule S M]
(hM : Stacks.Ample.IsAmple S M) (hf : IsProjective f) : IsProjectiveMorphism f
Tag 0C6J, a lemma
Tag 0C6J in the Stacks Project.
Stacks.RelativeAmple.isIso_relativeAmpleProjHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeAmple/ProjIso.lean, line 398.
[Stacks, Tag 0C6J]. Let
f : X ⟶ Sbe a universally closed morphism of schemes andLan invertible𝒪_X-module ample relative tof. Then the canonical morphismr : X ⟶ Proj_S(⨁_{d ≥ 0} f_* L^{⊗ d})of [Stacks, Tag 01VJ] is an isomorphism.Here
⨁_{d ≥ 0} f_* L^{⊗ d}isdirectImageAlgebra f L, the relativeProjis that of [Stacks, Tag 01NQ], andrisrelativeAmpleProjHom f L hL, the morphismr_{L, ψ}of [Stacks, Tag 01O9] for the adjunction mapψon its sourceU(ψ) = X. The quasi-compactness and quasi-separatedness offthat the algebra needs are part of, resp. a consequence of, relative ampleness ([Stacks, Tags 01VH, 01VI]); they are not hypotheses.
theorem isIso_relativeAmpleProjHom {X S : Scheme.{u}} (f : X ⟶ S) [UniversallyClosed f]
(L : X.Modules) [Stacks.Ample.IsInvertibleModule X L] (hL : IsRelativelyAmple f L) :
haveI := hL.quasiCompact
haveI := hL.quasiSeparated
IsIso (relativeAmpleProjHom f L hL)
Tag 0EKE, a lemma
Tag 0EKE in the Stacks Project.
Stacks.AmpleNonvanishingUniversallyClosed.isAffineHom_nonvanishingOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/AmpleNonvanishingUniversallyClosed.lean, line 122.
Stacks Tag 0EKE. Let
f : X ⟶ Sbe a universally closed morphism,Lan invertible𝒪_X-module ample relative tof, andsa global section ofL. Then the nonvanishing openX_sof Stacks Tag 01CY is affine overS.Affineness of a morphism is checked over an affine open
VofS. There the restriction ofLtof⁻¹Vis ample, by the very definition of relative ampleness, the restriction offis still universally closed, and the nonvanishing open of the restricted section is the preimage ofX_sby Stacks Tag 0H78; so the affine base case applies and givesX_s ∩ f⁻¹Vaffine.
theorem isAffineHom_nonvanishingOpen {X S : Scheme.{u}} (f : X ⟶ S) [UniversallyClosed f]
(L : X.Modules) [Stacks.Ample.IsInvertibleModule X L]
(hL : Stacks.RelativeAmple.IsRelativelyAmple f L) (s : Γ(L, ⊤)) :
IsAffineHom ((nonvanishingOpen X L s).ι ≫ f)
Sources
Section29.45 Integral and finite morphisms#
Section 29.45 of the Stacks Project, Tag 01WG. 16 tags here are carried by 7 declarations of the repository (all in StacksFrontier) and 22 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 01WH, a definition
Tag 01WH in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.IsIntegralHomregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 262 (StacksFrontier): “(1) integral morphism”. References: EGA II (6.1.1).AlgebraicGeometry.IsFiniteregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 263 (StacksFrontier): “(2) finite morphism”. References: EGA I (6.4.5); EGA II (6.1.1); EGA IV (21.5.3), “partial”.
Tag 02K8, a lemma
Tag 02K8 in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.IsIntegralHom.hasAffinePropertyregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 171 (StacksFrontier): “the affine-local property used for (1) ⇔ (2): over an affine target, integral means affine source and integral map on global sections”. References: EGA II (6.1.1), “Integral morphism”; EGA II (6.1.2), “integral branch”; EGA II (6.1.4).AlgebraicGeometry.HasAffineProperty.iff_of_iSup_eq_topregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 174 (StacksFrontier): “(1) ⇔ (2), for an affine open covering, applied to the affine-local property of integral morphisms”.AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_topregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 176 (StacksFrontier): “(1) ⇔ (3), for an open covering, integrality being local at the target”.AlgebraicGeometry.IsIntegralHom.instMorphismRestrictregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 178 (StacksFrontier): “theMoreoverclause: restriction to the preimage of an open subscheme”. References: EGA II (6.1.5), “(iii), special case”; EGA II (6.1.6), “integral clause”.
Tag 01WI, a lemma
Tag 01WI in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.IsFinite.instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTopregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 269 (StacksFrontier): “(1) ⟺ (2): being finite is the affine-local propertyXaffine with a finite ring map on global sections”. References: EGA I (6.4.5), “more general”; EGA II (6.1.1), “Finite morphism”; EGA II (6.1.2), “finite branch”; EGA II (6.1.4); EGA II (6.3.10); SGA 3 V (4.1.3), “partial”.AlgebraicGeometry.HasAffineProperty.iff_of_openCoverregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 272 (StacksFrontier): “(1) ⟺ (2), checked on an affine open cover of the target, applied to IsFinite”.AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCoverregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 274 (StacksFrontier): “(1) ⟺ (3), checked on an open cover of the target, applied to IsFinite”.AlgebraicGeometry.IsFinite.instMorphismRestrictregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 276 (StacksFrontier): “moreover: the restriction f⁻¹(U) → U of a finite morphism is finite”. References: EGA II (6.1.5), “(iii), special case”; EGA II (6.1.6), “finite clause”; EGA II (6.3.10), “partial”; EGA III (4.8.5), “ordinary schemes”; SGA 3 VIB (10.1), “finiteness, special case”.
Tag 01WJ, a lemma
Tag 01WJ in the Stacks Project.
AlgebraicGeometry.IsFinite.of_isIntegralHom_of_locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Integral/FiniteCriterion.lean, line 43. The attribute's comment: “only the second assertion, that an integral morphism which is locally of finite type is finite; the first assertion, that a finite morphism is integral, is not stated here and is part of AlgebraicGeometry.IsFinite.iff_isIntegralHom_and_locallyOfFiniteType”. References: EGA II (6.1.1), “partial”.
An integral morphism of schemes which is locally of finite type is finite.
theorem IsFinite.of_isIntegralHom_of_locallyOfFiniteType
[IsIntegralHom f] [LocallyOfFiniteType f] : IsFinite f
Declarations registered for the tag:
AlgebraicGeometry.IsFinite.iff_isIntegralHom_and_locallyOfFiniteTyperegistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Morphisms/Integral/FiniteCriterion.lean, line 32 (StacksFrontier): “A finite morphism is integral, and an integral morphism which is locally of finite type is finite.”. References: EGA II (6.1.1).
Tag 01WK, a lemma
Tag 01WK in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.IsFinite.instCompSchemeregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 279 (StacksFrontier): “finite morphisms”. References: EGA II (6.1.5), “(ii), finite branch”; EGA IV (21.10.15), “Condition a)”.AlgebraicGeometry.IsIntegralHom.instCompSchemeregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 280 (StacksFrontier): “integral morphisms”. References: EGA II (6.1.5), “(ii), integral branch”.
Tag 01WL, a lemma
Tag 01WL in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.IsFinite.instIsStableUnderBaseChangeSchemeregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 282 (StacksFrontier): “finite morphisms”. References: EGA I (6.4.12), “more general”; EGA I (6.4.6), “more general”; EGA II (6.1.5), “(iii), finite branch”; EGA III (2.6.2.1), “more general”; EGA IV (2.7.1), “implication”; EGA IV (21.10.16), “f₁ is finite”; SGA 1 VIII (5.7), “preservation (finite)”; SGA 1 VIII (6.6); SGA 3 VIB (10.1), “partial”; SGA 4 VIII (5.4), “more general”.AlgebraicGeometry.IsIntegralHom.instIsStableUnderBaseChangeSchemeregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 283 (StacksFrontier): “integral morphisms”. References: EGA II (6.1.5), “(iii), integral branch”; EGA IV (2.7.1), “implication”; SGA 1 VIII (5.7), “preservation (integral)”.
Tag 01WM, a lemma
Tag 01WM in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.IsIntegralHom.iff_universallyClosed_and_isAffineHomregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Morphisms/Integral/UniversallyClosedCriterion.lean, line 17 (StacksFrontier): “A morphism of schemes is integral if and only if it is affine and universally closed.”. References: EGA II (6.1.10), “more general”; EGA II (6.1.2), “forward implication”; EGA II (7.3.11), “special case”; EGA IV (18.12.8); EGA IV (18.12.9), “partial”.
Tag 02NT, a lemma
Tag 02NT in the Stacks Project.
AlgebraicGeometry.isClosed_singleton_asFiber_of_isIntegral, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Integral/Fiber.lean, line 44.
Stacks Project, Tag 02NT. Every point of the source of an integral morphism is closed in the fibre over its image.
lemma isClosed_singleton_asFiber_of_isIntegral (f : X ⟶ S) [IsIntegralHom f] (x : X) :
IsClosed ({f.asFiber x} : Set (f.fiber (f x)))
Tag 0ECG, a lemma
Tag 0ECG in the Stacks Project.
AlgebraicGeometry.topologicalKrullDim_le_of_isIntegralHom, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Integral/Dimension.lean, line 49. The attribute's comment: “dimension inequality”. References: EGA 0 (16.1.5), “dim(B) ≤ dim(A)”.
The dimension of the source of an integral morphism is at most the dimension of its target.
lemma topologicalKrullDim_le_of_isIntegralHom {X Y : Scheme.{u}} (f : X ⟶ Y)
[IsIntegralHom f] :
topologicalKrullDim X ≤ topologicalKrullDim Y
AlgebraicGeometry.topologicalKrullDim_eq_of_isIntegralHom_of_surjective, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Integral/Dimension.lean, line 68. The attribute's comment: “surjective case”. References: EGA 0 (16.1.5), “equality case”.
A surjective integral morphism has source and target of the same dimension.
lemma topologicalKrullDim_eq_of_isIntegralHom_of_surjective {X Y : Scheme.{u}} (f : X ⟶ Y)
[IsIntegralHom f] [Surjective f] :
topologicalKrullDim X = topologicalKrullDim Y
Tag 02NU, a lemma
Tag 02NU in the Stacks Project.
AlgebraicGeometry.quasiFinite_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Integral/FiniteQuasiFinite.lean, line 36.
A finite morphism of schemes is quasi-finite: it is locally of finite type, quasi-compact and locally quasi-finite.
theorem quasiFinite_of_isFinite {X S : Scheme.{u}} (f : X ⟶ S) [IsFinite f] :
(LocallyOfFiniteType f ∧ QuasiCompact f) ∧ LocallyQuasiFinite f
Tag 01WN, a lemma
Tag 01WN in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.IsFinite.iff_isProper_and_isAffineHomregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Stacks01WN.lean, line 11 (StacksFrontier). References: EGA II (7.3.12), “more general”; EGA III (4.4.2), “more general”; EGA IV (7.9.1), “more general”; SGA 6 XII (1.6), “special case”.
Tag 035C, a lemma
Tag 035C in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.IsFinite.instOfIsClosedImmersionregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 343 (StacksFrontier): “a closed immersion is finite”. References: EGA I (6.3.4), “more general”; EGA I (10.14.3), “special case”; EGA II (6.1.5), “(i), finite clause”; EGA II (6.2.4), “(i)”; EGA IV (1.5.4), “more general”.AlgebraicGeometry.IsFinite.instIsIntegralHomregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 344 (StacksFrontier): “a finite morphism is integral”. References: EGA II (6.1.1), “partial”.
Tag 0CYI, a lemma
Tag 0CYI in the Stacks Project.
AlgebraicGeometry.isFinite_sigmaDesc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Misc/FiniteCoproduct.lean, line 61.
A morphism from a finite coproduct of schemes is finite when its restriction to every component is finite.
instance isFinite_sigmaDesc {ι : Type v} [Finite ι]
{X : AlgebraicGeometry.Scheme.{u}} {Y : ι → AlgebraicGeometry.Scheme.{u}}
{f : ∀ i, Y i ⟶ X} [∀ i, AlgebraicGeometry.IsFinite (f i)] :
AlgebraicGeometry.IsFinite (Limits.Sigma.desc f)
Tag 035D, a lemma
Tag 035D in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.IsFinite.instHasOfPostcompPropertySchemeIsSeparatedregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 346 (StacksFrontier): “part (1)”. References: EGA II (6.1.5), “(v), finite branch”.AlgebraicGeometry.IsIntegralHom.instHasOfPostcompPropertySchemeIsSeparatedregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 347 (StacksFrontier): “part (2)”. References: EGA I (5.5.12), “(i), special case”; EGA II (6.1.5), “(v), integral branch”.
Tag 03BB, a lemma
Tag 03BB in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.IsClosedImmersion.iff_isFinite_and_monoregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch29.lean, line 131 (StacksFrontier). References: EGA I (6.3.4), “more general”; EGA I (10.14.3), “special case”; EGA II (1.6.2), “more general”; EGA II (6.1.5), “(i), finite clause”; EGA IV (5.4.2), “special case”; EGA IV (8.11.5), “special case”; EGA IV (1.5.4), “more general”; EGA IV (18.12.6), “(a)⇔(b), special case”; SGA 1 V (3.6), “monomorphism”; SGA 3 V (4.1.3), “more general”; SGA 3 VIB (1.4.2), “(i) ⇒ (ii)”.
Tag 0B3I, a lemma
Tag 0B3I in the Stacks Project.
Stacks.FiniteMorphismProjective.isProjective_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiniteMorphismProjective/Projective.lean, line 86. References: EGA II (5.5.5), “more general”; EGA II (6.1.11).
A finite morphism is projective. For a finite
f : X ⟶ Sover an arbitrary base scheme,Xis, overS, a closed subscheme of the projective bundle𝐏(f_*𝒪_X)of a quasi-coherent module of finite type.The module is
f_*𝒪_X, quasi-coherent by Tag 01SA and of finite type by Tag 01PB, and the closed immersion isStacks.FiniteMorphismProjective.embedding, which is a morphism over the base byStacks.FiniteMorphismProjective.embedding_comp_toBaseand a closed immersion byStacks.FiniteMorphismProjective.isClosedImmersion_embedding.
public theorem isProjective_of_isFinite {X S : Scheme.{u}} (f : X ⟶ S) [IsFinite f] :
AlgebraicGeometry.IsProjective f
Sources
Section29.46 Universal homeomorphisms#
Section 29.46 of the Stacks Project, Tag 04DC. 5 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 04DD, a definition
Tag 04DD in the Stacks Project.
AlgebraicGeometry.UniversalHomeomorphism, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversalHomeomorphism/Defs/Basic.lean, line 44. References: EGA IV (2.4.2), “universal homeomorphism”; SGA 4 VIII (1.4).
A morphism of schemes is a universal homeomorphism if every base change is a homeomorphism on the underlying topological spaces.
class UniversalHomeomorphism {X Y : Scheme.{u}} (f : X ⟶ Y) : Prop
Tag 04DF, a lemma
Tag 04DF in the Stacks Project.
AlgebraicGeometry.universalHomeomorphism_iff_integral_universallyInjective_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversalHomeomorphism/Defs/Integral.lean, line 43. References: EGA IV (18.12.11), “integral case”; EGA IV (2.4.5), “(i)”; EGA IV (15.2.4), “more general”; SGA 4 VIII (1.4).
A morphism of schemes is a universal homeomorphism if and only if it is integral, universally injective, and surjective.
theorem universalHomeomorphism_iff_integral_universallyInjective_surjective
{X Y : Scheme.{u}} (f : X ⟶ Y) :
UniversalHomeomorphism f ↔
IsIntegralHom f ∧ UniversallyInjective f ∧ Surjective f
Tag 054M, a lemma
Tag 054M in the Stacks Project.
AlgebraicGeometry.universalHomeomorphism_nilradical_subschemeι, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversalHomeomorphism/Reduction.lean, line 41. References: EGA IV (2.4.8), “(ii) univ. homeo”.
The reduction of a scheme is universally homeomorphic to the scheme through its canonical closed immersion.
instance universalHomeomorphism_nilradical_subschemeι (X : Scheme.{u}) :
UniversalHomeomorphism X.nilradical.subschemeι
Tag 0896, a lemma
Tag 0896 in the Stacks Project.
AlgebraicGeometry.isClosedImmersion_of_infinitesimal_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/DifferentialsAndValuative/ClosedImmersionInfinitesimal.lean, line 214.
A closed immersion can be detected after a closed, point-bijective base change under a finite-type or finite-presentation hypothesis.
public theorem isClosedImmersion_of_infinitesimal_baseChange
{X S S' : Scheme.{u}} (f : X ⟶ S) (g : S' ⟶ S)
[IsClosedImmersion g] (hg : Function.Bijective g.base)
[IsClosedImmersion (pullback.snd f g)]
(hfinite : (LocallyOfFiniteType f ∧ QuasiCompact f) ∨ FinitePresentation g) :
IsClosedImmersion f
Tag 0H2M, a lemma
Tag 0H2M in the Stacks Project.
AlgebraicGeometry.universalHomeomorphism_hasTwoOutOfThreeProperty, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversalHomeomorphism/Defs/TwoOutOfThree.lean, line 128.
Universal homeomorphisms of schemes satisfy the two-out-of-three property.
instance universalHomeomorphism_hasTwoOutOfThreeProperty :
MorphismProperty.HasTwoOutOfThreeProperty
(@UniversalHomeomorphism.{u} : MorphismProperty Scheme.{u})
Sources
Section29.47 Universal homeomorphisms of affine schemes#
Section 29.47 of the Stacks Project, Tag 0CN6. 11 tags here are carried by 22 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0CN7, a lemma
Tag 0CN7 in the Stacks Project.
AlgebraicGeometry.universallyClosed_specMap_subalgebra, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversalHomeomorphism/Affine/Subalgebra.lean, line 83. The attribute's comment: “universally_closed”.
Stacks 0CN7. If the morphism on spectra associated to an algebra is universally closed, the same holds for the morphism associated to any subalgebra.
lemma universallyClosed_specMap_subalgebra
{A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
(B' : Subalgebra A B)
[UniversallyClosed (Spec.map (CommRingCat.ofHom (algebraMap A B)))] :
UniversallyClosed (Spec.map (CommRingCat.ofHom (algebraMap A B')))
AlgebraicGeometry.universallyInjective_specMap_subalgebra, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversalHomeomorphism/Affine/Subalgebra.lean, line 99. The attribute's comment: “universally_closed_and_injective”.
Stacks 0CN7. Universal injectivity of the map on spectra passes from an algebra to any of its subalgebras, provided the original map is universally closed and universally injective.
lemma universallyInjective_specMap_subalgebra
{A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
[UniversallyClosed (Scheme.Spec.map (CommRingCat.ofHom (algebraMap A B)).op)]
[UniversallyInjective (Scheme.Spec.map (CommRingCat.ofHom (algebraMap A B)).op)]
(B' : Subalgebra A B) :
UniversallyInjective (Scheme.Spec.map (CommRingCat.ofHom (algebraMap A B')).op)
AlgebraicGeometry.universalHomeomorphism_specMap_subalgebra, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversalHomeomorphism/Affine/Subalgebra.lean, line 155. The attribute's comment: “universal_homeomorphism”.
Stacks 0CN7. If the map on spectra of an algebra is a universal homeomorphism, then so is the map on spectra of any intermediate subalgebra.
lemma universalHomeomorphism_specMap_subalgebra
{A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
[UniversalHomeomorphism
(Scheme.Spec.map (CommRingCat.ofHom (algebraMap A B)).op)]
(B' : Subalgebra A B) :
UniversalHomeomorphism
(Scheme.Spec.map (CommRingCat.ofHom (algebraMap A B')).op)
AlgebraicGeometry.isIso_residueFieldMap_specMap_subalgebra, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversalHomeomorphism/Affine/Subalgebra.lean, line 218. The attribute's comment: “universal_homeomorphism_residue_fields”.
Stacks 0CN7. If a universal homeomorphism between affine spectra induces isomorphisms on residue fields, then so does the map associated to any intermediate subalgebra.
lemma isIso_residueFieldMap_specMap_subalgebra
{A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
[UniversalHomeomorphism
(Scheme.Spec.map (CommRingCat.ofHom (algebraMap A B)).op)]
(hres : ∀ x : Spec (.of B),
IsIso ((Scheme.Spec.map (CommRingCat.ofHom (algebraMap A B)).op).residueFieldMap x))
(B' : Subalgebra A B) :
∀ x : Spec (.of B'),
IsIso ((Scheme.Spec.map (CommRingCat.ofHom (algebraMap A B')).op).residueFieldMap x)
Tag 0CN8, a lemma
Tag 0CN8 in the Stacks Project.
AlgebraicGeometry.universallyClosed_specMap_of_isColimit, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversalHomeomorphism/Affine/FilteredColimit.lean, line 127. The attribute's comment: “universally_closed”.
Stacks 0CN8. A filtered colimit of commutative
A-algebras whose spectrum morphisms toSpec Aare universally closed again has universally closed spectrum morphism toSpec A.
lemma universallyClosed_specMap_of_isColimit
(A : Type u) [CommRing A] {J : Type v} [Category.{w} J] [IsFiltered J]
(F : Functor J (CommAlgCat.{u} A)) (c : Cocone F) (hc : IsColimit c)
(h : ∀ j, UniversallyClosed
(Scheme.Spec.map (CommRingCat.ofHom (algebraMap A (F.obj j))).op)) :
UniversallyClosed
(Scheme.Spec.map (CommRingCat.ofHom (algebraMap A c.pt)).op)
AlgebraicGeometry.universallyInjective_specMap_of_isColimit, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversalHomeomorphism/Affine/FilteredColimit.lean, line 159. The attribute's comment: “closed_injective”.
Stacks 0CN8. A filtered colimit of commutative
A-algebras whose spectrum morphisms toSpec Aare universally injective again has universally injective spectrum morphism toSpec A.
lemma universallyInjective_specMap_of_isColimit
(A : Type u) [CommRing A] {J : Type v} [Category.{w} J] [IsFiltered J]
(F : Functor J (CommAlgCat.{u} A)) (c : Cocone F) (hc : IsColimit c)
(h : ∀ j, UniversallyInjective
(Scheme.Spec.map (CommRingCat.ofHom (algebraMap A (F.obj j))).op)) :
UniversallyInjective
(Scheme.Spec.map (CommRingCat.ofHom (algebraMap A c.pt)).op)
AlgebraicGeometry.universalHomeomorphism_specMap_of_isColimit, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversalHomeomorphism/Affine/FilteredColimit.lean, line 255. The attribute's comment: “universal_homeomorphism”.
Stacks 0CN8. A filtered colimit of commutative
A-algebras whose spectrum morphisms toSpec Aare universal homeomorphisms again has universal-homeomorphic spectrum morphism toSpec A.
lemma universalHomeomorphism_specMap_of_isColimit
(A : Type u) [CommRing A] {J : Type v} [Category.{w} J] [IsFiltered J]
(F : Functor J (CommAlgCat.{u} A)) (c : Cocone F) (hc : IsColimit c)
(h : ∀ j, UniversalHomeomorphism
(Scheme.Spec.map (CommRingCat.ofHom (algebraMap A (F.obj j))).op)) :
UniversalHomeomorphism
(Scheme.Spec.map (CommRingCat.ofHom (algebraMap A c.pt)).op)
AlgebraicGeometry.isIso_residueFieldMap_specMap_of_colimitPresentation, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversalHomeomorphism/Affine/FilteredColimit.lean, line 357. The attribute's comment: “homeomorphism_equal_residue_fields”.
Stacks 0CN8. A filtered colimit of affine maps which induce isomorphisms on residue fields still induces an isomorphism on the residue field at every point.
lemma isIso_residueFieldMap_specMap_of_colimitPresentation
{A : Type u} [CommRing A] {J : Type v} [Category.{w} J] [IsFiltered J]
{B : CommAlgCat.{u} A} (pres : ColimitPresentation J B)
(hresidue : ∀ i x, IsIso
((Scheme.Spec.map (CommRingCat.ofHom
(algebraMap A ↥(pres.diag.obj i))).op).residueFieldMap x)) :
∀ x, IsIso
((Scheme.Spec.map (CommRingCat.ofHom (algebraMap A ↥B)).op).residueFieldMap x)
Tag 0CN9, a lemma
Tag 0CN9 in the Stacks Project.
IsLocalization.exists_numerator_not_mem_of_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversalHomeomorphism/Affine/Denominators.lean, line 71.
Stacks 0CN9. Special-element conditions over a localization can be witnessed by a numerator before localization.
theorem exists_numerator_not_mem_of_localization
{B : Type u} [CommRing B] (A : Subring B) (S : Submonoid A)
{n : ℕ} (b : Fin n → B) (x : Localization (S.map A.subtype))
(hx : x ∉ Set.range
(IsLocalization.map (M := S) (S := Localization S) (T := S.map A.subtype)
(Localization (S.map A.subtype)) A.subtype S.le_comap_map))
(hbx : ∀ i, algebraMap B (Localization (S.map A.subtype)) (b i) *
x ^ (i.val + 1) ∈ Set.range
(IsLocalization.map (M := S) (S := Localization S) (T := S.map A.subtype)
(Localization (S.map A.subtype)) A.subtype S.le_comap_map)) :
∃ (s : S) (y : B),
x = IsLocalization.mk' (Localization (S.map A.subtype)) y
⟨A.subtype s.1, Submonoid.mem_map_of_mem A.subtype s.2⟩ ∧
y ∉ A ∧ ∀ i, b i * y ^ (i.val + 1) ∈ A
Tag 0CNA, a lemma
Tag 0CNA in the Stacks Project.
Subring.exists_not_mem_and_sq_mem_and_cube_mem_of_pow_mem_of_succ_pow_mem, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversalHomeomorphism/Affine/Powers.lean, line 63.
Stacks 0CNA. If an element outside a subring has two consecutive powers, with the first exponent at least two, in the subring, then some element outside the subring has its square and cube in the subring.
lemma exists_not_mem_and_sq_mem_and_cube_mem_of_pow_mem_of_succ_pow_mem
{B : Type u} [CommRing B] (A : Subring B) {b : B} {n : ℕ} (hb : b ∉ A) (hn : 2 ≤ n)
(hpow : b ^ n ∈ A) (hpow_succ : b ^ (n + 1) ∈ A) :
∃ b' : B, b' ∉ A ∧ b' ^ 2 ∈ A ∧ b' ^ 3 ∈ A
Tag 0CNB, a lemma
Tag 0CNB in the Stacks Project.
AlgebraicGeometry.exists_not_mem_and_sq_mem_and_cube_mem_of_universalHomeomorphism_of_residueFieldMap_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversalHomeomorphism/Affine/SquareCube.lean, line 767.
A proper subring extension which is a universal homeomorphism on spectra and induces isomorphisms on residue fields contains an element outside the subring whose square and cube are in the subring.
theorem exists_not_mem_and_sq_mem_and_cube_mem_of_universalHomeomorphism_of_residueFieldMap_isIso
{B : Type u} [CommRing B] (A : Subring B)
[UniversalHomeomorphism
(Scheme.Spec.map (CommRingCat.ofHom A.subtype).op)]
(hres : ∀ x : Spec (CommRingCat.of B),
IsIso ((Scheme.Spec.map (CommRingCat.ofHom A.subtype).op).residueFieldMap x))
(hA : A ≠ ⊤) :
∃ b : B, b ∉ A ∧ b ^ 2 ∈ A ∧ b ^ 3 ∈ A
Tag 0CNC, a lemma
Tag 0CNC in the Stacks Project.
AlgebraicGeometry.exists_special_element_of_universalHomeomorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversalHomeomorphism/Affine/SpecialElement.lean, line 703.
Stacks Project, Tag 0CNC. A proper extension inducing a universal homeomorphism on spectra contains either a square-and-cube special element or a prime-power special element.
theorem exists_special_element_of_universalHomeomorphism
{B : Type u} [CommRing B] (A : Subring B)
[UniversalHomeomorphism
(Scheme.Spec.map (CommRingCat.ofHom A.subtype).op)]
(hA : A ≠ ⊤) :
(∃ b : B, b ∉ A ∧ b ^ 2 ∈ A ∧ b ^ 3 ∈ A) ∨
(∃ p : ℕ, Nat.Prime p ∧
∃ b : B, b ∉ A ∧ (p : B) * b ∈ A ∧ b ^ p ∈ A)
Tag 0CND, a proposition
Tag 0CND in the Stacks Project.
AlgebraicGeometry.universalHomeomorphism_and_residueFieldIso_iff_finite_adjoin_square_cube, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversalHomeomorphism/Affine/TowerResidue.lean, line 341.
An injective extension induces a universal homeomorphism with unchanged residue fields if and only if each finite subset is contained in an algebra generated by a sequence whose successive elements have square and cube in the algebra generated by their predecessors.
public theorem universalHomeomorphism_and_residueFieldIso_iff_finite_adjoin_square_cube
{A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
(hAB : Function.Injective (algebraMap A B)) :
let f := Scheme.Spec.map (CommRingCat.ofHom (algebraMap A B)).op
(UniversalHomeomorphism f ∧ (∀ x, IsIso (f.residueFieldMap x))) ↔
∀ E : Finset B, ∃ (n : ℕ) (b : Fin n → B),
(↑E : Set B) ⊆ Algebra.adjoin A (Set.range b) ∧
∀ i : Fin n,
b i ^ 2 ∈ Algebra.adjoin A
(Set.range (fun j : Fin i ↦ b (Fin.castLE i.isLt.le j))) ∧
b i ^ 3 ∈ Algebra.adjoin A
(Set.range (fun j : Fin i ↦ b (Fin.castLE i.isLt.le j)))
Tag 0CNE, a proposition
Tag 0CNE in the Stacks Project.
AlgebraicGeometry.universalHomeomorphism_spec_iff_finite_adjoin_tower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversalHomeomorphism/Affine/Tower.lean, line 364.
An inclusion of rings induces a universal homeomorphism on spectra exactly when every finite set is contained in a finite, successively elementary extension.
theorem universalHomeomorphism_spec_iff_finite_adjoin_tower
(A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
(hAB : Function.Injective (algebraMap A B)) :
UniversalHomeomorphism
(Scheme.Spec.map (CommRingCat.ofHom (algebraMap A B)).op) ↔
∀ E : Finset B, ∃ (n : ℕ) (b : Fin n → B),
((E : Set B) ⊆ Algebra.adjoin A (Set.range b)) ∧
∀ i : Fin n,
(((b i) ^ 2 ∈ Algebra.adjoin A
(Set.range fun j : { j : Fin n // j < i } ↦ b j)) ∧
((b i) ^ 3 ∈ Algebra.adjoin A
(Set.range fun j : { j : Fin n // j < i } ↦ b j))) ∨
(∃ p : ℕ, p.Prime ∧
(((p : B) * b i ∈ Algebra.adjoin A
(Set.range fun j : { j : Fin n // j < i } ↦ b j)) ∧
((b i) ^ p ∈ Algebra.adjoin A
(Set.range fun j : { j : Fin n // j < i } ↦ b j))))
Tag 0CNF, a lemma
Tag 0CNF in the Stacks Project.
AlgebraicGeometry.universalHomeomorphism_iff_locallyNilpotent_ker_and_pow_mem_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversalHomeomorphism/Affine/InvertPrime.lean, line 321.
A ring map that is an isomorphism after inverting a prime induces a universal homeomorphism on spectra precisely when its kernel is locally nilpotent and every target element has a prime-power multiple and prime-power power in its image.
theorem universalHomeomorphism_iff_locallyNilpotent_ker_and_pow_mem_range
{A B : Type u} [CommRing A] [CommRing B] (φ : A →+* B)
(p : ℕ) (hp : Nat.Prime p)
(hφ : Function.Bijective
(IsLocalization.Away.map (Localization.Away (p : A))
(Localization.Away (φ (p : A))) φ (p : A))) :
UniversalHomeomorphism
(Scheme.Spec.map (CommRingCat.ofHom φ).op) ↔
(RingHom.ker φ).LocallyNilpotent ∧
∀ b : B, ∃ n : ℕ,
(p : B) ^ n * b ∈ Set.range φ ∧ b ^ (p ^ n) ∈ Set.range φ
Tag 0EUI, a lemma
Tag 0EUI in the Stacks Project.
AlgebraicGeometry.universalHomeomorphism_spec_quotient_of_pPower_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversalHomeomorphism/Affine/PrimePowerAlg.lean, line 188. The attribute's comment: “p_power_multiple”.
If
pis prime andp ^ p * x = y ^ p, adjoining a common prime-power root as in Stacks Project, Tag 0EUI, induces a universal homeomorphism on spectra.
theorem universalHomeomorphism_spec_quotient_of_pPower_mul
{A : Type u} [CommRing A] (x y : A) (p : ℕ) (hp : p.Prime)
(hxy : (p : A) ^ p * x = y ^ p) :
let B := Polynomial A ⧸ Ideal.span
{Polynomial.X ^ p - Polynomial.C x,
Polynomial.C (p : A) * Polynomial.X - Polynomial.C y}
UniversalHomeomorphism
(Scheme.Spec.map (CommRingCat.ofHom (algebraMap A B)).op)
AlgebraicGeometry.squareCubeSpecMap_universalHomeomorphism, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversalHomeomorphism/Affine/SquareCubeAlg.lean, line 468. The attribute's comment: “square_cube”.
The square-cube extension induces a universal homeomorphism on spectra.
public lemma squareCubeSpecMap_universalHomeomorphism
(A : Type u) [CommRing A] (x y : A) (hxy : x ^ 3 = y ^ 2) :
UniversalHomeomorphism (squareCubeSpecMap A x y)
AlgebraicGeometry.isIso_residueFieldMap_squareCubeSpecMap, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversalHomeomorphism/Affine/SquareCubeAlg.lean, line 482. The attribute's comment: “square_cube”.
The square-cube extension induces an isomorphism on the residue field at every point.
public lemma isIso_residueFieldMap_squareCubeSpecMap
(A : Type u) [CommRing A] (x y : A) (hxy : x ^ 3 = y ^ 2)
(z : Spec (.of (SquareCubeAlgebra A x y))) :
IsIso ((squareCubeSpecMap A x y).residueFieldMap z)
Tag 0EUJ, a lemma
Tag 0EUJ in the Stacks Project.
AlgebraicGeometry.isFilteredColimit_finitePresentation_universalHomeomorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/DifferentialsAndValuative/UniversalHomeomorphismFilteredColimit.lean, line 152. The attribute's comment: “universal_homeomorphism_filtered_colimit”.
A ring map inducing a universal homeomorphism on spectra is a filtered colimit of finitely presented ring maps which induce universal homeomorphisms on spectra.
public theorem isFilteredColimit_finitePresentation_universalHomeomorphism
{A B : Type u} [CommRing A] [CommRing B] (f : A →+* B)
(hf : UniversalHomeomorphism
(Scheme.Spec.map (CommRingCat.ofHom f).op)) :
ObjectProperty.ind.{u}
(fun C : Under (CommRingCat.of A) ↦
C.hom.hom.FinitePresentation ∧
UniversalHomeomorphism (Scheme.Spec.map C.hom.op))
(Under.mk (CommRingCat.ofHom f))
AlgebraicGeometry.ind_finitePresentation_residueFieldMap_isIso_universalHomeomorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/DifferentialsAndValuative/UniversalHomeomorphismFilteredColimit.lean, line 263. The attribute's comment: “residue_field_isomorphism_filtered_colimit”.
A ring map which is a universal homeomorphism on spectra and induces isomorphisms on residue fields is a filtered colimit of finitely presented ring maps with both properties.
public theorem ind_finitePresentation_residueFieldMap_isIso_universalHomeomorphism
{A B : Type u} [CommRing A] [CommRing B] (f : A →+* B)
(hres : ∀ x : Spec (.of B),
IsIso ((Scheme.Spec.map (CommRingCat.ofHom f).op).residueFieldMap x))
(huh : UniversalHomeomorphism
(Scheme.Spec.map (CommRingCat.ofHom f).op)) :
ObjectProperty.ind.{u}
(fun C : Under (CommRingCat.of A) ↦
C.hom.hom.FinitePresentation ∧
(UniversalHomeomorphism (Scheme.Spec.map C.hom.op) ∧
∀ x : Spec C.right,
IsIso ((Scheme.Spec.map C.hom.op).residueFieldMap x)))
(Under.mk (CommRingCat.ofHom f))
AlgebraicGeometry.exists_universalHomeomorphism_specMap_of_isColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversalHomeomorphism/Affine/FiniteStage.lean, line 481. The attribute's comment: “universal homeomorphism at a finite stage”.
Stacks 0EUJ. Let a commutative
A-algebra of finite type be presented as a filtered colimit ofA-algebras of finite presentation with surjective transition maps. If its morphism on spectra overSpec Ais a universal homeomorphism, then so is the one of every sufficiently late stage of the diagram.
theorem exists_universalHomeomorphism_specMap_of_isColimit
(A : Type u) [CommRing A] {J : Type v} [Category.{w} J] [IsFiltered J]
(F : J ⥤ CommAlgCat.{u} A) (c : Cocone F) (hc : IsColimit c)
[Algebra.FiniteType A c.pt]
(hfp : ∀ i, Algebra.FinitePresentation A (F.obj i))
(hsurj : ∀ {i j : J} (f : i ⟶ j), Function.Surjective (F.map f))
[UniversalHomeomorphism (Scheme.Spec.map (CommRingCat.ofHom (algebraMap A c.pt)).op)] :
∃ i : J, ∀ {j : J} (_ : i ⟶ j),
UniversalHomeomorphism
(Scheme.Spec.map (CommRingCat.ofHom (algebraMap A (F.obj j))).op)
AlgebraicGeometry.exists_universalHomeomorphism_and_isIso_residueFieldMap_of_isColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversalHomeomorphism/Affine/FiniteStage.lean, line 525. The attribute's comment: “universal homeomorphism with equal residue fields at a finite stage”.
Stacks 0EUJ. Let a commutative
A-algebra of finite type be presented as a filtered colimit ofA-algebras of finite presentation with surjective transition maps. If its morphism on spectra overSpec Ais a universal homeomorphism which induces isomorphisms on residue fields, then the same holds at every sufficiently late stage of the diagram.
theorem exists_universalHomeomorphism_and_isIso_residueFieldMap_of_isColimit
(A : Type u) [CommRing A] {J : Type v} [Category.{w} J] [IsFiltered J]
(F : J ⥤ CommAlgCat.{u} A) (c : Cocone F) (hc : IsColimit c)
[Algebra.FiniteType A c.pt]
(hfp : ∀ i, Algebra.FinitePresentation A (F.obj i))
(hsurj : ∀ {i j : J} (f : i ⟶ j), Function.Surjective (F.map f))
[UniversalHomeomorphism (Scheme.Spec.map (CommRingCat.ofHom (algebraMap A c.pt)).op)]
(hres : ∀ x : Spec (.of c.pt), IsIso ((Scheme.Spec.map
(CommRingCat.ofHom (algebraMap A c.pt)).op).residueFieldMap x)) :
∃ i : J, ∀ {j : J} (_ : i ⟶ j),
UniversalHomeomorphism
(Scheme.Spec.map (CommRingCat.ofHom (algebraMap A (F.obj j))).op) ∧
∀ x : Spec (.of (F.obj j)), IsIso ((Scheme.Spec.map
(CommRingCat.ofHom (algebraMap A (F.obj j))).op).residueFieldMap x)
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.