35.26 Properties of morphisms… to 35.39 Descent data in terms of…
Section35.26 Properties of morphisms local on the source#
Section 35.26 of the Stacks Project, Tag 036F. 5 tags here are carried by 21 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 036G, a definition
Tag 036G in the Stacks Project.
Declarations registered for the tag:
CategoryTheory.MorphismProperty.IsLocalAtSourceregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Descent/LocalOnSource/Defs.lean, line 55 (StacksFrontier). References: SGA 4 IV (8.5.4).
Tag 04QV, a lemma
Tag 04QV in the Stacks Project.
AlgebraicGeometry.precomp_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSource/Precomposition.lean, line 84. The attribute's comment: “fpqc case”.
Stacks Project, Tag 04QV, fpqc case. A property of morphisms of schemes which is fpqc local on the source is preserved by precomposition with a flat morphism.
theorem precomp_of_flat (P : MorphismProperty Scheme.{u})
[P.IsLocalAtSource Scheme.fpqcPrecoverage]
{X' X Y : Scheme.{u}} (a : X' ⟶ X) (f : X ⟶ Y)
(ha : Flat a) (hf : P f) : P (a ≫ f)
AlgebraicGeometry.precomp_of_flat_locallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSource/Precomposition.lean, line 104. The attribute's comment: “fppf case”.
Stacks Project, Tag 04QV, fppf case. A property of morphisms of schemes which is fppf local on the source is preserved by precomposition with a flat morphism which is locally of finite presentation.
theorem precomp_of_flat_locallyOfFinitePresentation
(P : MorphismProperty Scheme.{u}) [P.IsLocalAtSource Scheme.fppfPrecoverage]
{X' X Y : Scheme.{u}} (a : X' ⟶ X) (f : X ⟶ Y)
(ha : Flat a) (ha' : LocallyOfFinitePresentation a) (hf : P f) :
P (a ≫ f)
AlgebraicGeometry.precomp_of_syntomic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSource/Precomposition.lean, line 115. The attribute's comment: “syntomic case”.
Stacks Project, Tag 04QV, syntomic case. A property of morphisms of schemes which is syntomic local on the source is preserved by precomposition with a syntomic morphism.
theorem precomp_of_syntomic (P : MorphismProperty Scheme.{u})
[P.IsLocalAtSource (Scheme.precoverage (@Syntomic.{u}))]
{X' X Y : Scheme.{u}} (a : X' ⟶ X) (f : X ⟶ Y)
(ha : Syntomic a) (hf : P f) : P (a ≫ f)
AlgebraicGeometry.precomp_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSource/Precomposition.lean, line 125. The attribute's comment: “smooth case”.
Stacks Project, Tag 04QV, smooth case. A property of morphisms of schemes which is smooth local on the source is preserved by precomposition with a smooth morphism.
theorem precomp_of_smooth (P : MorphismProperty Scheme.{u})
[P.IsLocalAtSource (Scheme.precoverage @Smooth)]
{X' X Y : Scheme.{u}} (a : X' ⟶ X) (f : X ⟶ Y)
(ha : Smooth a) (hf : P f) : P (a ≫ f)
AlgebraicGeometry.precomp_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSource/Precomposition.lean, line 134. The attribute's comment: “étale case”.
Stacks Project, Tag 04QV, étale case. A property of morphisms of schemes which is étale local on the source is preserved by precomposition with an étale morphism.
theorem precomp_of_etale (P : MorphismProperty Scheme.{u})
[P.IsLocalAtSource Scheme.etalePrecoverage]
{X' X Y : Scheme.{u}} (a : X' ⟶ X) (f : X ⟶ Y)
(ha : Etale a) (hf : P f) : P (a ≫ f)
AlgebraicGeometry.precomp_of_isOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSource/Precomposition.lean, line 144. The attribute's comment: “Zariski case”.
Stacks Project, Tag 04QV, Zariski case. A property of morphisms of schemes which is Zariski local on the source is preserved by precomposition with an open immersion.
theorem precomp_of_isOpenImmersion (P : MorphismProperty Scheme.{u})
[P.IsLocalAtSource Scheme.zariskiPrecoverage]
{X' X Y : Scheme.{u}} (a : X' ⟶ X) (f : X ⟶ Y)
(ha : IsOpenImmersion a) (hf : P f) : P (a ≫ f)
Tag 0CEY, a lemma
Tag 0CEY in the Stacks Project.
AlgebraicGeometry.largestOpen, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSource/LargestOpen.lean, line 80. The attribute's comment: “open locus”.
Stacks Project, Tag 0CEY. The largest open of the source of
f : X ⟶ Yon which the restriction offhas the propertyP, defined as the supremum of all opensUofXwithP (U.ι ≫ f).That this open is itself such a locus requires
Pto be local on the source for one of the four topologies of the source lemma; seelargestOpen_isGreatest_fppfand its variants.
def largestOpen (P : MorphismProperty Scheme.{u}) {X Y : Scheme.{u}}
(f : X ⟶ Y) : X.Opens
AlgebraicGeometry.largestOpen_isGreatest_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSource/LargestOpen.lean, line 164. The attribute's comment: “fppf largest locus”.
Stacks Project, Tag 0CEY for the fppf topology. For
Plocal on the source in the fppf topology,largestOpen P fis a locus forPand is the greatest open that is one.
theorem largestOpen_isGreatest_fppf (P : MorphismProperty Scheme.{u})
[P.IsLocalAtSource Scheme.fppfPrecoverage] {X Y : Scheme.{u}} (f : X ⟶ Y) :
IsGreatest {U : X.Opens | P (U.ι ≫ f)} (largestOpen P f)
AlgebraicGeometry.largestOpen_isGreatest_syntomic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSource/LargestOpen.lean, line 173. The attribute's comment: “syntomic largest locus”.
Stacks Project, Tag 0CEY for the syntomic topology. For
Plocal on the source in the syntomic topology,largestOpen P fis a locus forPand is the greatest open that is one.
theorem largestOpen_isGreatest_syntomic (P : MorphismProperty Scheme.{u})
[P.IsLocalAtSource (Scheme.precoverage (@Syntomic.{u}))]
{X Y : Scheme.{u}} (f : X ⟶ Y) :
IsGreatest {U : X.Opens | P (U.ι ≫ f)} (largestOpen P f)
AlgebraicGeometry.largestOpen_isGreatest_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSource/LargestOpen.lean, line 183. The attribute's comment: “smooth largest locus”.
Stacks Project, Tag 0CEY for the smooth topology. For
Plocal on the source in the smooth topology,largestOpen P fis a locus forPand is the greatest open that is one.
theorem largestOpen_isGreatest_smooth (P : MorphismProperty Scheme.{u})
[P.IsLocalAtSource (Scheme.precoverage (@Smooth : MorphismProperty Scheme.{u}))]
{X Y : Scheme.{u}} (f : X ⟶ Y) :
IsGreatest {U : X.Opens | P (U.ι ≫ f)} (largestOpen P f)
AlgebraicGeometry.largestOpen_isGreatest_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSource/LargestOpen.lean, line 193. The attribute's comment: “étale largest locus”.
Stacks Project, Tag 0CEY for the étale topology. For
Plocal on the source in the étale topology,largestOpen P fis a locus forPand is the greatest open that is one.
theorem largestOpen_isGreatest_etale (P : MorphismProperty Scheme.{u})
[P.IsLocalAtSource Scheme.etalePrecoverage] {X Y : Scheme.{u}} (f : X ⟶ Y) :
IsGreatest {U : X.Opens | P (U.ι ≫ f)} (largestOpen P f)
AlgebraicGeometry.preimage_largestOpen_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSource/LargestOpen.lean, line 203. The attribute's comment: “fppf inverse image”.
Stacks Project, Tag 0CEY for the fppf topology: the largest locus of an fppf-local property pulls back to the largest locus of the composite along a flat morphism locally of finite presentation.
theorem preimage_largestOpen_fppf (P : MorphismProperty Scheme.{u})
[P.IsLocalAtSource Scheme.fppfPrecoverage]
{X' X Y : Scheme.{u}} (g : X' ⟶ X) (f : X ⟶ Y)
[Flat g] [LocallyOfFinitePresentation g] :
g ⁻¹ᵁ largestOpen P f = largestOpen P (g ≫ f)
AlgebraicGeometry.preimage_largestOpen_syntomic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSource/LargestOpen.lean, line 228. The attribute's comment: “syntomic inverse image”.
Stacks Project, Tag 0CEY for the syntomic topology: the largest locus of a syntomic-local property pulls back to the largest locus of the composite along a syntomic morphism.
theorem preimage_largestOpen_syntomic (P : MorphismProperty Scheme.{u})
[P.IsLocalAtSource (Scheme.precoverage (@Syntomic.{u}))]
{X' X Y : Scheme.{u}} (g : X' ⟶ X) (f : X ⟶ Y) (hg : Syntomic g) :
g ⁻¹ᵁ largestOpen P f = largestOpen P (g ≫ f)
AlgebraicGeometry.preimage_largestOpen_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSource/LargestOpen.lean, line 243. The attribute's comment: “smooth inverse image”.
Stacks Project, Tag 0CEY for the smooth topology: the largest locus of a smooth-local property pulls back to the largest locus of the composite along a smooth morphism.
theorem preimage_largestOpen_smooth (P : MorphismProperty Scheme.{u})
[P.IsLocalAtSource (Scheme.precoverage (@Smooth : MorphismProperty Scheme.{u}))]
{X' X Y : Scheme.{u}} (g : X' ⟶ X) (f : X ⟶ Y) [Smooth g] :
g ⁻¹ᵁ largestOpen P f = largestOpen P (g ≫ f)
AlgebraicGeometry.preimage_largestOpen_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSource/LargestOpen.lean, line 255. The attribute's comment: “étale inverse image”.
Stacks Project, Tag 0CEY for the étale topology: the largest locus of an étale-local property pulls back to the largest locus of the composite along an étale morphism.
theorem preimage_largestOpen_etale (P : MorphismProperty Scheme.{u})
[P.IsLocalAtSource Scheme.etalePrecoverage]
{X' X Y : Scheme.{u}} (g : X' ⟶ X) (f : X ⟶ Y) [Etale g] :
g ⁻¹ᵁ largestOpen P f = largestOpen P (g ≫ f)
Tag 036H, a lemma
Tag 036H in the Stacks Project.
AlgebraicGeometry.isLocalAtSource_fpqc_of_affine_descent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSourceTopologies/AffineCriteria.lean, line 113. The attribute's comment: “fpqc case”.
A property of morphisms of schemes which is Zariski local on the source and on the target, which is preserved by precomposition with flat morphisms, and which descends along surjective flat morphisms of affine schemes, is fpqc local on the source.
theorem isLocalAtSource_fpqc_of_affine_descent (P : MorphismProperty Scheme.{u})
[P.RespectsLeft (@Flat.{u})] [IsZariskiLocalAtSource P] [IsZariskiLocalAtTarget P]
(hAffine : ∀ {X' X Y : Scheme.{u}} [IsAffine X'] [IsAffine X] [IsAffine Y]
(g : X' ⟶ X) (f : X ⟶ Y), Surjective g → Flat g → P (g ≫ f) → P f) :
P.IsLocalAtSource Scheme.fpqcPrecoverage
AlgebraicGeometry.isLocalAtSource_fppf_of_affine_descent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSourceTopologies/AffineCriteria.lean, line 138. The attribute's comment: “fppf case”.
A property of morphisms of schemes which is Zariski local on the source and on the target, which is preserved by precomposition with flat morphisms locally of finite presentation, and which descends along surjective flat morphisms locally of finite presentation of affine schemes, is fppf local on the source.
theorem isLocalAtSource_fppf_of_affine_descent (P : MorphismProperty Scheme.{u})
[P.RespectsLeft (@Flat ⊓ @LocallyOfFinitePresentation : MorphismProperty Scheme.{u})]
[IsZariskiLocalAtSource P] [IsZariskiLocalAtTarget P]
(hAffine : ∀ {X' X Y : Scheme.{u}} [IsAffine X'] [IsAffine X] [IsAffine Y]
(g : X' ⟶ X) (f : X ⟶ Y), Surjective g → Flat g → LocallyOfFinitePresentation g →
P (g ≫ f) → P f) :
P.IsLocalAtSource Scheme.fppfPrecoverage
AlgebraicGeometry.isLocalAtSource_smooth_of_affine_descent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSourceTopologies/AffineCriteria.lean, line 163. The attribute's comment: “smooth case”.
A property of morphisms of schemes which is Zariski local on the source and on the target, which is preserved by precomposition with smooth morphisms, and which descends along surjective smooth morphisms of affine schemes, is smooth local on the source.
theorem isLocalAtSource_smooth_of_affine_descent (P : MorphismProperty Scheme.{u})
[P.RespectsLeft (@Smooth.{u})] [IsZariskiLocalAtSource P] [IsZariskiLocalAtTarget P]
(hAffine : ∀ {X' X Y : Scheme.{u}} [IsAffine X'] [IsAffine X] [IsAffine Y]
(g : X' ⟶ X) (f : X ⟶ Y), Surjective g → Smooth g → P (g ≫ f) → P f) :
P.IsLocalAtSource (Scheme.precoverage (@Smooth.{u}))
AlgebraicGeometry.isLocalAtSource_etale_of_affine_descent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleSourceLocality.lean, line 131. The attribute's comment: “étale case”.
Stacks Project, Tag 036H, étale case. A property of morphisms of schemes which is Zariski local on the source and on the target, which is preserved by precomposition with étale morphisms, and which descends along surjective étale morphisms of affine schemes, is étale local on the source.
theorem isLocalAtSource_etale_of_affine_descent (P : MorphismProperty Scheme.{u})
[P.RespectsLeft (@Etale.{u})] [IsZariskiLocalAtSource P] [IsZariskiLocalAtTarget P]
(hAffine : ∀ {X' X Y : Scheme.{u}} [IsAffine X'] [IsAffine X] [IsAffine Y]
(g : X' ⟶ X) (f : X ⟶ Y), Surjective g → Etale g → P (g ≫ f) → P f) :
P.IsLocalAtSource Scheme.etalePrecoverage
AlgebraicGeometry.isLocalAtSource_syntomic_of_affine_descent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/SyntomicScheme.lean, line 170. The attribute's comment: “syntomic case”.
Stacks Project, Tag 036H, syntomic case. A property of morphisms of schemes which is Zariski local on the source and on the target, which is preserved by precomposition with syntomic morphisms, and which descends along surjective syntomic morphisms of affine schemes, is syntomic local on the source.
theorem isLocalAtSource_syntomic_of_affine_descent (P : MorphismProperty Scheme.{u})
[P.RespectsLeft (@Syntomic.{u})] [IsZariskiLocalAtSource P] [IsZariskiLocalAtTarget P]
(hAffine : ∀ {X' X Y : Scheme.{u}} [IsAffine X'] [IsAffine X] [IsAffine Y]
(g : X' ⟶ X) (f : X ⟶ Y), Surjective g → Syntomic g → P (g ≫ f) → P f) :
P.IsLocalAtSource (Scheme.precoverage (@Syntomic.{u}))
Tag 036I, a remark
Tag 036I in the Stacks Project.
AlgebraicGeometry.isLocalAtSource_of_standard_descent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/StandardForm/SourceDescent.lean, line 248.
Stacks Project, Tag 036I. In condition (4) of Tag 036H one may assume that the morphism is a (surjective) standard smooth morphism when
τ = smooth, a (surjective) standard syntomic morphism whenτ = syntomic, and a (surjective) standard étale morphism whenτ = étale.The three conjuncts are the statements of the smooth, syntomic and étale cases of Tag 036H with condition (4) so strengthened; they are
AlgebraicGeometry.isLocalAtSource_smooth_of_standard_descent,AlgebraicGeometry.isLocalAtSource_syntomic_of_standard_descentandAlgebraicGeometry.isLocalAtSource_etale_of_standard_descent.
theorem isLocalAtSource_of_standard_descent :
(∀ (P : MorphismProperty Scheme.{u}) [P.RespectsLeft (@Smooth.{u})]
[IsZariskiLocalAtSource P] [IsZariskiLocalAtTarget P],
(∀ {X' X Y : Scheme.{u}} [IsAffine X'] [IsAffine X] [IsAffine Y]
(g : X' ⟶ X) (f : X ⟶ Y), Surjective g → IsStandardSmooth g → P (g ≫ f) → P f) →
P.IsLocalAtSource (Scheme.precoverage (@Smooth.{u}))) ∧
(∀ (P : MorphismProperty Scheme.{u}) [P.RespectsLeft (@Syntomic.{u})]
[IsZariskiLocalAtSource P] [IsZariskiLocalAtTarget P],
(∀ {X' X Y : Scheme.{u}} [IsAffine X'] [IsAffine X] [IsAffine Y]
(g : X' ⟶ X) (f : X ⟶ Y), Surjective g → IsStandardSyntomic g → P (g ≫ f) → P f) →
P.IsLocalAtSource (Scheme.precoverage (@Syntomic.{u}))) ∧
∀ (P : MorphismProperty Scheme.{u}) [P.RespectsLeft (@Etale.{u})]
[IsZariskiLocalAtSource P] [IsZariskiLocalAtTarget P],
(∀ {X' X Y : Scheme.{u}} [IsAffine X'] [IsAffine X] [IsAffine Y]
(g : X' ⟶ X) (f : X ⟶ Y), Surjective g → IsStandardEtale g → P (g ≫ f) → P f) →
P.IsLocalAtSource Scheme.etalePrecoverage
Sources
Section35.27 Properties of morphisms local in the fpqc topology on the source#
Section 35.27 of the Stacks Project, Tag 036J. 2 tags here are carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 036K, a lemma
Tag 036K in the Stacks Project.
AlgebraicGeometry.flat_isLocalAtSource_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSource/Fpqc.lean, line 74.
Flatness of scheme morphisms is fpqc-local on the source.
public instance flat_isLocalAtSource_fpqc :
MorphismProperty.IsLocalAtSource (@Flat : MorphismProperty Scheme.{u})
Scheme.fpqcPrecoverage
Tag 036L, a lemma
Tag 036L in the Stacks Project.
AlgebraicGeometry.stalkwiseInjective_isLocalAtSource_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSource/Fpqc.lean, line 102.
Injectivity of all the local-ring maps of a scheme morphism is fpqc-local on its source.
public instance stalkwiseInjective_isLocalAtSource_fpqc :
MorphismProperty.IsLocalAtSource
(stalkwise (fun f => Function.Injective f) : MorphismProperty Scheme.{u})
Scheme.fpqcPrecoverage
Sources
Section35.28 Properties of morphisms local in the fppf topology on the source#
Section 35.28 of the Stacks Project, Tag 036M. 4 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 036N, a lemma
Tag 036N in the Stacks Project.
AlgebraicGeometry.locallyOfFinitePresentation_isLocalAtSource, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSourceTopologies/Fppf.lean, line 57.
Being locally of finite presentation is local on the source for the fppf topology.
instance locallyOfFinitePresentation_isLocalAtSource :
MorphismProperty.IsLocalAtSource (@LocallyOfFinitePresentation.{u})
Scheme.fppfPrecoverage
Tag 036O, a lemma
Tag 036O in the Stacks Project.
AlgebraicGeometry.locallyOfFiniteType_isLocalAtSource, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSourceTopologies/Fppf.lean, line 83.
Being locally of finite type is local on the source for the fppf topology.
instance locallyOfFiniteType_isLocalAtSource :
MorphismProperty.IsLocalAtSource (@LocallyOfFiniteType.{u}) Scheme.fppfPrecoverage
Tag 036P, a lemma
Tag 036P in the Stacks Project.
AlgebraicGeometry.isLocalAtSource_fppf_isOpenMap, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSourceTopologies/Fppf.lean, line 110.
Being an open morphism is local on the source for the fppf topology.
instance isLocalAtSource_fppf_isOpenMap :
(topologically IsOpenMap : MorphismProperty Scheme.{u}).IsLocalAtSource
Scheme.fppfPrecoverage
Tag 036Q, a lemma
Tag 036Q in the Stacks Project.
AlgebraicGeometry.universallyOpen_isLocalAtSource, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSourceTopologies/Fppf.lean, line 125.
Being universally open is local on the source for the fppf topology.
instance universallyOpen_isLocalAtSource :
MorphismProperty.IsLocalAtSource (@UniversallyOpen.{u}) Scheme.fppfPrecoverage
Sources
Section35.29 Properties of morphisms local in the syntomic topology on the source#
Section 35.29 of the Stacks Project, Tag 036R. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 036S, a lemma
Tag 036S in the Stacks Project.
AlgebraicGeometry.Syntomic.isLocalAtSource_syntomicPrecoverage, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSourceTopologies/Syntomic.lean, line 42.
Being syntomic is local on the source for the syntomic topology: a morphism of schemes is syntomic exactly when its composites with the members of a syntomic covering of its source are.
instance Syntomic.isLocalAtSource_syntomicPrecoverage :
MorphismProperty.IsLocalAtSource (@Syntomic.{u} : MorphismProperty Scheme.{u})
(Scheme.precoverage (@Syntomic.{u}))
Sources
Section35.30 Properties of morphisms local in the smooth topology on the source#
Section 35.30 of the Stacks Project, Tag 036T. 1 tag here is carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 036U, a lemma
Tag 036U in the Stacks Project.
AlgebraicGeometry.smooth_isLocalAtSource, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSourceTopologies/Smooth.lean, line 52.
Stacks Project, Tag 036U. Being a smooth morphism of schemes is local on the source for the smooth topology.
instance smooth_isLocalAtSource :
MorphismProperty.IsLocalAtSource (@Smooth.{u}) (Scheme.precoverage (@Smooth.{u}))
AlgebraicGeometry.Smooth.isLocalAtSource_smoothPrecoverage, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/SmoothSourceLocality.lean, line 108. References: SGA 4 IV (8.5.5), “special case”.
Stacks 036U. Smoothness of morphisms of schemes is local on the source for the smooth topology: a morphism is smooth exactly when its composites with the members of a smooth covering of its source are smooth.
The affine descent hypothesis of the smooth case of Stacks 036H is the smooth case of Stacks 02KM, which holds without any affineness assumption.
instance Smooth.isLocalAtSource_smoothPrecoverage :
MorphismProperty.IsLocalAtSource (@Smooth : MorphismProperty Scheme.{u})
(Scheme.precoverage (@Smooth : MorphismProperty Scheme.{u}))
Sources
Section35.31 Properties of morphisms local in the étale topology on the source#
Section 35.31 of the Stacks Project, Tag 036V. 3 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 036W, a lemma
Tag 036W in the Stacks Project.
AlgebraicGeometry.etale_isLocalAtSource, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSourceTopologies/Etale.lean, line 62.
Stacks Project, Tag 036W. Being an étale morphism of schemes is local on the source for the étale topology.
instance etale_isLocalAtSource :
MorphismProperty.IsLocalAtSource (@Etale.{u}) Scheme.etalePrecoverage
Tag 03X4, a lemma
Tag 03X4 in the Stacks Project.
AlgebraicGeometry.locallyQuasiFinite_isLocalAtSource_etale, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSourceTopologies/Etale.lean, line 82.
Stacks Project, Tag 03X4. Being locally quasi-finite is local on the source for the étale topology.
instance locallyQuasiFinite_isLocalAtSource_etale :
MorphismProperty.IsLocalAtSource
((@LocallyOfFiniteType.{u} ⊓ @LocallyQuasiFinite.{u} : MorphismProperty Scheme.{u}))
Scheme.etalePrecoverage
Tag 03YV, a lemma
Tag 03YV in the Stacks Project.
AlgebraicGeometry.unramified_isLocalAtSource, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSourceTopologies/Unramified.lean, line 94. The attribute's comment: “unramified”.
Stacks Project, Tag 03YV, unramified case. Unramifiedness of morphisms of schemes is local on the source for the étale topology.
instance unramified_isLocalAtSource :
MorphismProperty.IsLocalAtSource (@Unramified.{u}) Scheme.etalePrecoverage
AlgebraicGeometry.gUnramified_isLocalAtSource_etale, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSourceTopologies/Unramified.lean, line 126. The attribute's comment: “g_unramified”. References: SGA 4 IV (8.5.5), “special case”.
Stacks Project, Tag 03YV, G-unramified case. G-unramifiedness of morphisms of schemes is local on the source for the étale topology.
instance gUnramified_isLocalAtSource_etale :
MorphismProperty.IsLocalAtSource (@GUnramified.{u}) Scheme.etalePrecoverage
Sources
Section35.32 Properties of morphisms étale local on source-and-target#
Section 35.32 of the Stacks Project, Tag 04QW. 10 tags here are carried by 30 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 04QX, an example
Tag 04QX in the Stacks Project.
AlgebraicGeometry.targetIsLocallyNoetherian, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/Noetherian.lean, line 91. The attribute's comment: “target_noetherian_property”.
Stacks Project, Tag 04QX. The property of a morphism of schemes that its target is locally Noetherian.
abbrev targetIsLocallyNoetherian : CategoryTheory.MorphismProperty Scheme.{u}
AlgebraicGeometry.targetIsLocallyNoetherian_not_respectsRight_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/Noetherian.lean, line 217. The attribute's comment: “target_noetherian_not_stable_under_etale_postcomposition”.
The property that the target is locally Noetherian is not stable under postcomposition with an étale morphism.
theorem targetIsLocallyNoetherian_not_respectsRight_etale :
¬ (targetIsLocallyNoetherian : MorphismProperty Scheme.{u}).RespectsRight
(@Etale : MorphismProperty Scheme.{u})
Tag 04QY, an example
Tag 04QY in the Stacks Project.
AlgebraicGeometry.IsNoetherianOnSpecializations, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/Noetherian.lean, line 97. The attribute's comment: “specialization_noetherian_property”.
Stacks Project, Tag 04QY. Every specialization of a point in the image of a scheme morphism has a Noetherian local ring on the target.
abbrev IsNoetherianOnSpecializations {X Y : Scheme.{u}} (f : X ⟶ Y) : Prop
AlgebraicGeometry.isNoetherianOnSpecializations_isLocalAtTarget, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/Noetherian.lean, line 156. The attribute's comment: “etale_local_target”.
The specialization-Noetherian property is local on the target for étale coverings.
instance isNoetherianOnSpecializations_isLocalAtTarget :
MorphismProperty.IsLocalAtTarget
(@IsNoetherianOnSpecializations : MorphismProperty Scheme.{u})
Scheme.etalePrecoverage
AlgebraicGeometry.isNoetherianOnSpecializations_isLocalAtSource, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/Noetherian.lean, line 187. The attribute's comment: “etale_local_source”.
The specialization-Noetherian property is local on the source for étale coverings.
instance isNoetherianOnSpecializations_isLocalAtSource :
MorphismProperty.IsLocalAtSource
(@IsNoetherianOnSpecializations : MorphismProperty Scheme.{u})
Scheme.etalePrecoverage
AlgebraicGeometry.ManyVariableExample.exists_commSq_isNoetherianOnSpecializations_not, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/Noetherian.lean, line 362. The attribute's comment: “counterexample”.
Stacks Project, Tag 04QY. There is a commutative square with surjective étale vertical arrows whose top morphism has the specialization-Noetherian property while its bottom morphism does not. Together with étale locality on the source and on the target, this is the example's point: the two localities do not add up to locality on source-and-target.
theorem exists_commSq_isNoetherianOnSpecializations_not :
∃ (U V X Y : Scheme.{0}) (a : U ⟶ X) (b : V ⟶ Y) (h : U ⟶ V) (f : X ⟶ Y),
a ≫ f = h ≫ b ∧ Surjective a ∧ Etale a ∧ Surjective b ∧ Etale b ∧
IsNoetherianOnSpecializations h ∧ ¬ IsNoetherianOnSpecializations f
Tag 04QZ, a definition
Tag 04QZ in the Stacks Project.
AlgebraicGeometry.IsEtaleLocalOnSourceAndTarget, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/Defs.lean, line 46.
A property of morphisms of schemes is étale local on the source and target if it is preserved by étale precomposition and étale base change, and can be checked in a commutative square of étale neighbourhoods around every point of the source.
structure IsEtaleLocalOnSourceAndTarget (P : MorphismProperty Scheme.{u}) : Prop
Tag 04R0, a lemma
Tag 04R0 in the Stacks Project.
AlgebraicGeometry.IsEtaleLocalOnSourceAndTarget.of_comp_etale, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/Basic.lean, line 76. The attribute's comment: “cancel_etale”.
An étale morphism can be cancelled on the right of a composite for a property which is étale local on the source and target.
lemma of_comp_etale {P : MorphismProperty Scheme.{u}}
(hP : IsEtaleLocalOnSourceAndTarget P)
{X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
(hg : Etale g) (hfg : P (f ≫ g)) : P f
AlgebraicGeometry.IsEtaleLocalOnSourceAndTarget.postcomp_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/Basic.lean, line 91. The attribute's comment: “postcompose_etale”.
A property that is étale local on the source and target is preserved by postcomposition with an étale morphism.
theorem postcomp_of_etale (P : MorphismProperty Scheme.{u})
(hP : IsEtaleLocalOnSourceAndTarget P) {X Y Z : Scheme.{u}} (f : X ⟶ Y) (hf : P f)
(g : Y ⟶ Z) (hg : Etale g) : P (f ≫ g)
AlgebraicGeometry.IsEtaleLocalOnSourceAndTarget.isLocalAtSource_etalePrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/Basic.lean, line 109. The attribute's comment: “local_source”.
A morphism property étale local on the source and target is étale local on the source.
theorem isLocalAtSource_etalePrecoverage (P : MorphismProperty Scheme.{u})
(hP : IsEtaleLocalOnSourceAndTarget P) :
P.IsLocalAtSource Scheme.etalePrecoverage
AlgebraicGeometry.IsEtaleLocalOnSourceAndTarget.isLocalAtTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/Basic.lean, line 142. The attribute's comment: “local_target”.
A property of scheme morphisms that is étale local on the source and target is étale local on the target.
theorem isLocalAtTarget (P : MorphismProperty Scheme.{u})
(hP : IsEtaleLocalOnSourceAndTarget P) :
P.IsLocalAtTarget Scheme.etalePrecoverage
Tag 04R1, a lemma
Tag 04R1 in the Stacks Project.
AlgebraicGeometry.IsEtaleLocalOnSourceAndTarget.iff_forall_etale_diagrams, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/Characterization.lean, line 62. The attribute's comment: “part (c)”.
A property étale local on source and target holds iff it holds in every commuting square whose vertical maps are étale.
theorem iff_forall_etale_diagrams (hP : IsEtaleLocalOnSourceAndTarget P) :
P f ↔
∀ {U V : Scheme.{u}} (a : U ⟶ X) (b : V ⟶ Y) (h : U ⟶ V),
Etale a → Etale b → h ≫ b = a ≫ f → P h
AlgebraicGeometry.IsEtaleLocalOnSourceAndTarget.iff_exists_surjective_etale_diagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/Characterization.lean, line 74. The attribute's comment: “part (d)”.
It suffices to test one commuting étale square whose map to the source is surjective.
theorem iff_exists_surjective_etale_diagram (hP : IsEtaleLocalOnSourceAndTarget P) :
P f ↔
∃ (U V : Scheme.{u}) (a : U ⟶ X) (b : V ⟶ Y) (h : U ⟶ V),
Etale a ∧ Etale b ∧ Function.Surjective a.base ∧
h ≫ b = a ≫ f ∧ P h
AlgebraicGeometry.IsEtaleLocalOnSourceAndTarget.iff_exists_etale_target_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/Characterization.lean, line 101. The attribute's comment: “part (e)”.
An étale-local property can be tested after an étale covering of the target.
theorem iff_exists_etale_target_cover (hP : IsEtaleLocalOnSourceAndTarget P) :
P f ↔
∃ 𝒰 : Y.Cover.{u} Scheme.etalePrecoverage,
∀ i : 𝒰.I₀, P (pullback.fst (𝒰.f i) f)
AlgebraicGeometry.IsEtaleLocalOnSourceAndTarget.iff_exists_etale_source_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/Characterization.lean, line 118. The attribute's comment: “part (f)”.
An étale-local property can be tested after an étale covering of the source.
theorem iff_exists_etale_source_cover (hP : IsEtaleLocalOnSourceAndTarget P) :
P f ↔
∃ 𝒰 : X.Cover.{u} Scheme.etalePrecoverage,
∀ i : 𝒰.I₀, P (𝒰.f i ≫ f)
AlgebraicGeometry.IsEtaleLocalOnSourceAndTarget.iff_exists_bi_etale_covers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/Characterization.lean, line 134. The attribute's comment: “part (g)”.
An étale-local property can be tested after covering the target and then the base-changed source by étale morphisms.
theorem iff_exists_bi_etale_covers (hP : IsEtaleLocalOnSourceAndTarget P) :
P f ↔
∃ 𝒰 : Y.Cover.{u} Scheme.etalePrecoverage,
∀ i : 𝒰.I₀,
∃ 𝒱 : (pullback (𝒰.f i) f).Cover.{u} Scheme.etalePrecoverage,
∀ j : 𝒱.I₀, P (𝒱.f j ≫ pullback.fst (𝒰.f i) f)
Declarations registered for the tag:
AlgebraicGeometry.IsEtaleLocalOnSourceAndTarget.iff_forall_exists_etale_neighborhoodregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/Characterization.lean, line 54 (StacksFrontier): “part (b)”.
Tag 04R2, a lemma
Tag 04R2 in the Stacks Project.
AlgebraicGeometry.isEtaleLocalOnSourceAndTarget_of_isLocalAtSource_isLocalAtTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/Criterion.lean, line 480.
A morphism property that is étale local on each of the source and target separately, and is preserved by postcomposition with open immersions, is étale local on the source and target together.
theorem isEtaleLocalOnSourceAndTarget_of_isLocalAtSource_isLocalAtTarget
(P : MorphismProperty Scheme.{u})
[P.IsLocalAtSource Scheme.etalePrecoverage]
[P.IsLocalAtTarget Scheme.etalePrecoverage]
[P.RespectsRight (@IsOpenImmersion : MorphismProperty Scheme.{u})] :
IsEtaleLocalOnSourceAndTarget P
Tag 04R3, a remark
Tag 04R3 in the Stacks Project.
AlgebraicGeometry.etale_isEtaleLocalOnSourceAndTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/EtaleLocalAtSource.lean, line 69. The attribute's comment: “etale”. References: EGA IV (17.3.2), “partial”.
Stacks 04R3, the étale case. Being an étale morphism of schemes is étale local on the source and target.
The local criterion is reduced, through
AlgebraicGeometry.Etale.iff_flat_and_formallyUnramified, to the flat and locally-of-finite-presentation cases of [Stacks Project, Tag 04R3] together with its unramified case, from which formal unramifiedness is extracted by [Stacks Project, Tag 02HE].
theorem etale_isEtaleLocalOnSourceAndTarget :
IsEtaleLocalOnSourceAndTarget (@Etale.{u} : MorphismProperty Scheme.{u})
AlgebraicGeometry.LocallyOfFinitePresentation.isEtaleLocalOnSourceAndTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/FinitePresentationLocalAtSource.lean, line 82. The attribute's comment: “locally_finite_presentation”.
Being a morphism of schemes locally of finite presentation is étale local on the source and target.
theorem LocallyOfFinitePresentation.isEtaleLocalOnSourceAndTarget :
IsEtaleLocalOnSourceAndTarget
(@LocallyOfFinitePresentation : MorphismProperty Scheme.{u})
AlgebraicGeometry.LocallyOfFiniteType.isEtaleLocalOnSourceAndTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/FiniteTypeLocalAtSource.lean, line 156. The attribute's comment: “locally finite type”.
Stacks Project, Tag 04R3, the case of being locally of finite type. Being a morphism of schemes locally of finite type is étale local on the source and target.
theorem LocallyOfFiniteType.isEtaleLocalOnSourceAndTarget :
IsEtaleLocalOnSourceAndTarget
(@LocallyOfFiniteType : MorphismProperty Scheme.{u})
AlgebraicGeometry.Flat.isEtaleLocalOnSourceAndTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/FlatLocalAtSource.lean, line 92. The attribute's comment: “flat”.
Stacks Project, Tag 04R3, flat case. Being a flat morphism of schemes is étale local on the source and target.
theorem Flat.isEtaleLocalOnSourceAndTarget :
IsEtaleLocalOnSourceAndTarget (@Flat : MorphismProperty Scheme.{u})
AlgebraicGeometry.isEtaleLocalOnSourceAndTarget_gUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/Properties.lean, line 523. The attribute's comment: “g_unramified”. References: EGA IV (17.3.2), “Remark 17.3.2(iii)”.
Stacks Project, Tag 04R3, item (10). Being a G-unramified morphism of schemes is étale local on the source and target.
This is the criterion of Tag 04R2 applied to G-unramifiedness: it is étale local on the source and on the target by the two instances above, and postcomposition with an open immersion preserves it. The source cites Tag 03YV for the first and Tag 02VM for the second; the two localities used here are the ones proved in this file, which is enough, since Tag 04R2 asks for étale locality only.
theorem isEtaleLocalOnSourceAndTarget_gUnramified :
IsEtaleLocalOnSourceAndTarget (@GUnramified.{u} : MorphismProperty Scheme.{u})
AlgebraicGeometry.locallyOfFiniteType_inf_locallyQuasiFinite_isEtaleLocalOnSourceAndTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/QuasiFiniteLocalAtSource.lean, line 96. The attribute's comment: “locally quasi-finite”.
Stacks 04R3, the case of being locally quasi-finite. Being a morphism of schemes locally of finite type and locally quasi-finite is étale local on the source and target.
theorem locallyOfFiniteType_inf_locallyQuasiFinite_isEtaleLocalOnSourceAndTarget :
IsEtaleLocalOnSourceAndTarget
((@LocallyOfFiniteType.{u} : MorphismProperty Scheme.{u}) ⊓
(@LocallyQuasiFinite.{u} : MorphismProperty Scheme.{u}))
AlgebraicGeometry.Smooth.isEtaleLocalOnSourceAndTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/SmoothLocalAtSource.lean, line 108. The attribute's comment: “smooth”. References: SGA 1 II (1.3), “special case”.
Stacks Project, Tag 04R3, smooth case. Being a smooth morphism of schemes is étale local on the source and target.
theorem Smooth.isEtaleLocalOnSourceAndTarget :
IsEtaleLocalOnSourceAndTarget (@Smooth : MorphismProperty Scheme.{u})
AlgebraicGeometry.UniversallyOpen.isEtaleLocalOnSourceAndTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/UniversallyOpenLocalAtSource.lean, line 57. The attribute's comment: “universally open”. References: SGA 4 IV (8.5.5), “special case”.
Being a universally open morphism of schemes is étale local on the source and target.
theorem UniversallyOpen.isEtaleLocalOnSourceAndTarget :
IsEtaleLocalOnSourceAndTarget (@UniversallyOpen : MorphismProperty Scheme.{u})
AlgebraicGeometry.Unramified.isEtaleLocalOnSourceAndTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/UnramifiedLocalAtSource.lean, line 168. The attribute's comment: “unramified”.
Stacks Project, Tag 04R3, unramified case. Being an unramified morphism of schemes is étale local on the source and target.
This is the formal half of Tag 04R2 applied to unramifiedness: it is local on the source for the étale topology by the instance above, stable under arbitrary base change by Tag 02GA, and preserved by postcomposition with an étale morphism.
theorem Unramified.isEtaleLocalOnSourceAndTarget :
IsEtaleLocalOnSourceAndTarget (@Unramified : MorphismProperty Scheme.{u})
AlgebraicGeometry.syntomic_isEtaleLocalOnSourceAndTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Syntomic.lean, line 109. The attribute's comment: “syntomic”.
Stacks Project, Tag 04R3, syntomic case. Being a syntomic morphism of schemes is étale local on the source and target.
The geometric content of Tag 04R2 is not needed: postcomposition with an étale morphism preserves syntomicity outright, by
AlgebraicGeometry.Syntomic.respectsRight_etale, and base change is Tag 01UI. The local criterion comes from étale source-locality of syntomic morphisms of schemes,AlgebraicGeometry.Syntomic.isLocalAtSource_etalePrecoverage.
theorem syntomic_isEtaleLocalOnSourceAndTarget :
IsEtaleLocalOnSourceAndTarget (@Syntomic.{u} : MorphismProperty Scheme.{u})
Tag 0CEZ, a lemma
Tag 0CEZ in the Stacks Project.
AlgebraicGeometry.mem_largestOpen_iff_of_etaleAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSource/LargestOpenEtaleSquare.lean, line 107.
Stacks Project, Tag 0CEZ. Étale morphisms on both sides of a commutative square preserve membership in the largest open locus of a property étale local on the source and target.
public theorem mem_largestOpen_iff_of_etaleAt
(P : MorphismProperty Scheme.{u})
(hP : IsEtaleLocalOnSourceAndTarget P)
{X' X Y' Y : Scheme.{u}}
(f : X ⟶ Y) (f' : X' ⟶ Y') (g : Y' ⟶ Y) (g' : X' ⟶ X)
(hcomm : g' ≫ f = f' ≫ g) (x' : X')
(hg' : EtaleAt g' x')
(hg : EtaleAt g (f'.base x')) :
g'.base x' ∈ largestOpen P f ↔ x' ∈ largestOpen P f'
Tag 0CF0, a lemma
Tag 0CF0 in the Stacks Project.
MvPolynomial.eq_univ_or_finite_compl_of_invariant_coordinateShear, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSource/AffineSpaceOrbits.lean, line 401.
A nonempty open subset of affine
n-space, forn ≥ 2, invariant under every elementary coordinate shear, is either all of affine space or has finite complement consisting of closed points whose coordinates are algebraic over the prime field (and in the latter case the field has positive characteristic).
lemma eq_univ_or_finite_compl_of_invariant_coordinateShear
{k : Type*} [Field k] {n : ℕ} (hn : 2 ≤ n)
(W : Set (PrimeSpectrum (MvPolynomial (Fin n) k)))
(hWopen : IsOpen W) (hWnonempty : W.Nonempty)
(hWinv : ∀ (i j : Fin n) (hij : i ≠ j) (d : ℕ),
PrimeSpectrum.comap (coordinateShear (R := k) i j hij d).toRingHom ⁻¹' W = W) :
W = Set.univ ∨
(0 < ringChar k ∧ Wᶜ.Finite ∧ ∀ q ∈ Wᶜ, q.asIdeal.IsMaximal ∧
∃ ι : ZMod (ringChar k) →+* q.asIdeal.ResidueField,
∀ i : Fin n, @IsIntegral (ZMod (ringChar k)) q.asIdeal.ResidueField _ _ ι.toAlgebra
(algebraMap (MvPolynomial (Fin n) k) q.asIdeal.ResidueField
(MvPolynomial.X i)))
Tag 0CF1, a lemma
Tag 0CF1 in the Stacks Project.
AlgebraicGeometry.mem_largestOpen_iff_of_smoothAt_etaleAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSource/LargestOpenSmoothSquare.lean, line 634.
Stacks Project, Tag 0CF1. If the right vertical morphism of a commutative square is smooth at the relevant point and the comparison morphism to the fibre product is étale at the chosen point, the two source points lie in their largest open loci simultaneously.
public theorem mem_largestOpen_iff_of_smoothAt_etaleAt
(P : MorphismProperty Scheme.{u})
[P.IsLocalAtSource Scheme.etalePrecoverage]
[P.IsLocalAtTarget
(Scheme.precoverage (@Smooth : MorphismProperty Scheme.{u}))]
[P.RespectsRight (@IsOpenImmersion : MorphismProperty Scheme.{u})]
{X' X Y' Y : Scheme.{u}}
(f : X ⟶ Y) (f' : X' ⟶ Y') (g : Y' ⟶ Y) (g' : X' ⟶ X)
(hcomm : g' ≫ f = f' ≫ g) (x' : X')
(hg : InfinitesimalLifting.SmoothAt g (f'.base x'))
(hg' : EtaleAt
(pullback.lift g' f' hcomm) x') :
g'.base x' ∈ AlgebraicGeometry.largestOpen P f ↔
x' ∈ AlgebraicGeometry.largestOpen P f'
Sources
Section35.33 Properties of morphisms of germs local on source-and-target#
Section 35.33 of the Stacks Project, Tag 04R5. 8 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 04NB, a definition
Tag 04NB in the Stacks Project.
AlgebraicGeometry.MorphismOfGerms.IsEtaleLocalOnSourceAndTarget, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germ/Local.lean, line 66.
A property of morphisms of germs of schemes is étale local on the source and target if it is invariant under commutative squares with étale vertical arrows.
structure MorphismOfGerms.IsEtaleLocalOnSourceAndTarget
(Q : ∀ {X Y : GermOfScheme.{u}}, MorphismOfGerms X Y → Prop) : Prop
Tag 04R6, a lemma
Tag 04R6 in the Stacks Project.
AlgebraicGeometry.MorphismOfGerms.hasRepresentativeWithProperty_isEtaleLocalOnSourceAndTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germ/InducedProperty.lean, line 108.
Étale locality on the source and target of a property of morphisms of schemes passes to the property it induces on morphisms of germs.
theorem hasRepresentativeWithProperty_isEtaleLocalOnSourceAndTarget
(P : MorphismProperty Scheme.{u})
(hP : AlgebraicGeometry.IsEtaleLocalOnSourceAndTarget P) :
IsEtaleLocalOnSourceAndTarget (HasRepresentativeWithProperty P)
Tag 04R7, a lemma
Tag 04R7 in the Stacks Project.
AlgebraicGeometry.IsEtaleLocalOnSourceAndTarget.iff_forall_hasRepresentativeWithProperty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germ/EtaleLocalCriterion.lean, line 53.
A property of morphisms of schemes which is étale local on the source and target holds for a morphism exactly when the associated property of morphisms of germs holds for every induced morphism of germs.
theorem IsEtaleLocalOnSourceAndTarget.iff_forall_hasRepresentativeWithProperty
(P : MorphismProperty Scheme.{u}) (hP : IsEtaleLocalOnSourceAndTarget P)
{X Y : Scheme.{u}} (f : X ⟶ Y) :
P f ↔ ∀ x : X, MorphismOfGerms.HasRepresentativeWithProperty P
(MorphismOfGerms.ofSchemeHom f x)
Tag 04ND, a lemma
Tag 04ND in the Stacks Project.
AlgebraicGeometry.MorphismOfGerms.isEtaleLocalOnSourceAndTarget_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/GermSourceAndTarget/Flat.lean, line 461.
Flatness of the map on local rings of a morphism of germs is étale local on both source and target.
theorem isEtaleLocalOnSourceAndTarget_isFlat :
IsEtaleLocalOnSourceAndTarget (@IsFlat.{u})
Tag 04NI, a lemma
Tag 04NI in the Stacks Project.
AlgebraicGeometry.etale_fiberMap, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/Fiber.lean, line 164.
Stacks Project, Tag 04NI. The morphism between corresponding fibres in a commutative square with étale vertical arrows is étale.
public lemma etale_fiberMap (f' : U' ⟶ V') (g' : U' ⟶ U)
(g : V' ⟶ V) (f : U ⟶ V) (h : g' ≫ f = f' ≫ g) (v' : V')
[Etale g'] [Etale g] : Etale (fiberMap f' g' g f h v')
Tag 04NJ, a lemma
Tag 04NJ in the Stacks Project.
AlgebraicGeometry.fiberLocalRingDimension_isEtaleLocalOnSourceAndTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germs/FiberLocalRingDimension.lean, line 282.
The dimension of the local ring of the fibre of a morphism of germs at its distinguished point is étale local on the source and target germs.
public theorem fiberLocalRingDimension_isEtaleLocalOnSourceAndTarget (d : ℕ∞) :
MorphismOfGerms.IsEtaleLocalOnSourceAndTarget
(@HasFiberLocalRingDimension.{u} d)
Tag 04NK, a lemma
Tag 04NK in the Stacks Project.
AlgebraicGeometry.MorphismOfGerms.residueFieldTranscendenceDegree_isEtaleLocalOnSourceAndTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germ/TranscendenceDegree.lean, line 563.
Stacks Project, Tag 04NK. Residue-field transcendence degree at a point is étale local on the source and target of a morphism of germs.
public theorem residueFieldTranscendenceDegree_isEtaleLocalOnSourceAndTarget
(r : ℕ∞) :
IsEtaleLocalOnSourceAndTarget
(@HasResidueFieldTranscendenceDegree.{u} r)
Tag 04NL, a lemma
Tag 04NL in the Stacks Project.
AlgebraicGeometry.fiberDimensionAt_isEtaleLocalOnSourceAndTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germs/FiberDimension.lean, line 185.
Stacks Project, Tag 04NL. Dimension at a point of a fibre is étale local on the source and target of a morphism of germs.
public theorem fiberDimensionAt_isEtaleLocalOnSourceAndTarget (d : ℕ∞) :
MorphismOfGerms.IsEtaleLocalOnSourceAndTarget (@HasFiberDimensionAt.{u} d)
Sources
Section35.34 Descent data for schemes over schemes#
Section 35.34 of the Stacks Project, Tag 023U. 11 tags here are carried by 23 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 023V, a definition
Tag 023V in the Stacks Project.
AlgebraicGeometry.DescentDatum, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Scheme/SingleMorphism.lean, line 105. The attribute's comment: “(1) descent datum for V/X/S, (2) descent datum relative to X ⟶ S”. References: SGA 3 IV (2.1), “descent datum”.
Descent data for schemes relative to a single morphism
f : X ⟶ S: a schemeVoverXtogether with an isomorphismV ×_S X ≅ X ×_S Vof schemes overX ×_S Xsatisfying the cocycle condition. This is the one-member family case ofAlgebraicGeometry.DescentData.
abbrev DescentDatum (f : X ⟶ S)
AlgebraicGeometry.DescentDatum.Hom, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Scheme/SingleMorphism.lean, line 115. The attribute's comment: “(3) morphisms of descent data relative to X ⟶ S”. References: SGA 3 IV (2.1), “partial”.
A morphism of descent data relative to
f : X ⟶ S: a morphism ofX-schemes commuting with the two gluing isomorphisms.
abbrev Hom (D E : DescentDatum f)
Tag 02VP, a remark
Tag 02VP in the Stacks Project.
AlgebraicGeometry.DescentData, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Scheme/DescentData.lean, line 149. The attribute's comment: “remark reading the gluing isomorphism as pr_0^V → pr_1^V over X ×_S X”. References: SGA 3 IV (2.1), “descent datum”.
Descent data for schemes relative to a family of morphisms with common target.
structure DescentData
Tag 023W, a definition
Tag 023W in the Stacks Project.
AlgebraicGeometry.DescentData, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Scheme/DescentData.lean, line 149. The attribute's comment: “(1) descent data”. References: SGA 3 IV (2.1), “descent datum”.
Descent data for schemes relative to a family of morphisms with common target.
structure DescentData
AlgebraicGeometry.DescentData.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Scheme/DescentData.lean, line 197. The attribute's comment: “(2) morphisms of descent data”.
A morphism of descent data is a family of maps over the family members, compatible with the gluing isomorphisms.
structure Hom (D E : DescentData f)
Tag 02VQ, a remark
Tag 02VQ in the Stacks Project.
AlgebraicGeometry.DescentData, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Scheme/DescentData.lean, line 149. The attribute's comment: “the gluing isomorphisms read over the pairwise fibre product, with the cocycle”. References: SGA 3 IV (2.1), “descent datum”.
Descent data for schemes relative to a family of morphisms with common target.
structure DescentData
Tag 023X, a lemma
Tag 023X in the Stacks Project.
AlgebraicGeometry.DescentData.familyCoproductEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Scheme/FamilyCoproduct.lean, line 705.
Descent data relative to a family
X i ⟶ Sare canonically equivalent to descent data relative to the single morphism(∐ i, X i) ⟶ S. Under this equivalence both objects and gluing maps are formed by coproduct, as specified byFamilyCoproductEquivalence.
noncomputable def familyCoproductEquivalence :
FamilyCoproductEquivalence f
Tag 023Y, a lemma
Tag 023Y in the Stacks Project.
AlgebraicGeometry.DescentData.pullbackFunctorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/PullbackFullyFaithful/PullbackFunctorIso.lean, line 248. The attribute's comment: “part (2)”.
The canonical natural isomorphism between the pullback functors associated to two morphisms which complete the same commutative square. Its components are the pullbacks of the original gluing isomorphisms along the maps induced by
(f₀, f₁).
def pullbackFunctorIso {S S' X X' : Scheme.{u}} (a : X ⟶ S) (a' : X' ⟶ S') (h : S' ⟶ S)
(f₀ f₁ : X' ⟶ X) (comm₀ : f₀ ≫ a = a' ≫ h) (comm₁ : f₁ ≫ a = a' ≫ h) :
PullbackFunctorIso a a' h f₀ f₁ comm₀ comm₁
(pullbackFunctor a a' h f₀ comm₀) (pullbackFunctor a a' h f₁ comm₁)
AlgebraicGeometry.DescentData.pullbackFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Scheme/PullbackSquare.lean, line 107. The attribute's comment: “part (1)”.
Pullback of descent data along a commutative square of schemes. On underlying schemes this is base change along
f; the gluing isomorphism is pulled back along the induced map of self-fibre products.
noncomputable def pullbackFunctor
{S S' X X' : Scheme.{u}} (a : X ⟶ S) (a' : X' ⟶ S') (h : S' ⟶ S)
(f : X' ⟶ X) (comm : f ≫ a = a' ≫ h) :
PullbackFunctor a a' h f comm
Tag 02VR, a definition
Tag 02VR in the Stacks Project.
AlgebraicGeometry.DescentData.pullbackFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Scheme/PullbackSquare.lean, line 107. The attribute's comment: “the pullback functor on descent data”.
Pullback of descent data along a commutative square of schemes. On underlying schemes this is base change along
f; the gluing isomorphism is pulled back along the induced map of self-fibre products.
noncomputable def pullbackFunctor
{S S' X X' : Scheme.{u}} (a : X ⟶ S) (a' : X' ⟶ S') (h : S' ⟶ S)
(f : X' ⟶ X) (comm : f ≫ a = a' ≫ h) :
PullbackFunctor a a' h f comm
Tag 02VS, a lemma
Tag 02VS in the Stacks Project.
AlgebraicGeometry.MorphismOfSchemeFamilies.pullbackFunctorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FamilyPullbackFunctorIso.lean, line 78. The attribute's comment: “part (3)”.
Stacks Project, Tag 02VS, part (3). Two morphisms of families of morphisms with fixed target which have the same morphism
hof base schemes induce canonically isomorphic pullback functors on descent data, whatever their index maps and component morphisms are.
def pullbackFunctorIso :
(pullbackFunctor (ofHomOver 𝒰 𝒱 h φ)).functor ≅
(pullbackFunctor (ofHomOver 𝒰 𝒱 h ψ)).functor
AlgebraicGeometry.MorphismOfSchemeFamilies.pullbackCompatibility, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germs/PullbackCompatibility.lean, line 723. The attribute's comment: “compatibility”.
Pullback of descent data commutes canonically with the equivalence between a family and its coproduct morphism.
public noncomputable def pullbackCompatibility
(F : MorphismOfSchemeFamilies.{u}) : PullbackCompatibility F
AlgebraicGeometry.MorphismOfSchemeFamilies.pullbackFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Scheme/PullbackFunctor.lean, line 120. The attribute's comment: “pullback_functor”.
The pullback of descent data along a morphism of families is functorial.
public noncomputable def pullbackFunctor (F : MorphismOfSchemeFamilies.{u}) :
PullbackFunctor F
AlgebraicGeometry.MorphismOfSchemeFamilies.pulledBackDatum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Scheme/PulledBackDatum.lean, line 1061. The attribute's comment: “pulled_back_datum”.
Pull a descent datum back componentwise along a morphism of families. If the morphism has index map
αand component mapsgᵢ, its objects aregᵢ * Y_(α i)and its gluing isomorphisms are the pullbacks of the original gluing isomorphisms alonggᵢ × gᵢ'.
noncomputable def pulledBackDatum (F : MorphismOfSchemeFamilies.{u})
(D : DescentData F.targetFamily.f) :
DescentData F.sourceFamily.f
AlgebraicGeometry.MorphismOfSchemeFamilies.pulledBackDatum_obj, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Scheme/PulledBackDatum.lean, line 1089. The attribute's comment: “pulled_back_datum”.
The component of the pulled-back datum at
iis the pullback of the component atF.familyHom.s₀ i.
lemma pulledBackDatum_obj (F : MorphismOfSchemeFamilies.{u})
(D : DescentData F.targetFamily.f) (i : F.sourceFamily.I₀) :
(pulledBackDatum F D).obj i =
(Over.pullback (F.familyHom.h₀ i)).obj (D.obj (F.familyHom.s₀ i))
AlgebraicGeometry.MorphismOfSchemeFamilies.pulledBackDatum_gluing, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Scheme/PulledBackDatum.lean, line 1151. The attribute's comment: “pulled_back_datum”.
On each pair of indices, the gluing isomorphism of the pulled-back datum is the pullback of the original gluing isomorphism along the two component morphisms.
lemma pulledBackDatum_gluing (F : MorphismOfSchemeFamilies.{u})
(D : DescentData F.targetFamily.f) (i i' : F.sourceFamily.I₀) :
((pulledBackDatum F D).gluingPullbackIso i i').hom ≫
pulledBackDatumTargetMap F D i i' =
pulledBackDatumSourceMap F D i i' ≫
(D.gluingPullbackIso (F.familyHom.s₀ i) (F.familyHom.s₀ i')).hom
Tag 02VT, a definition
Tag 02VT in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.MorphismOfSchemeFamilies.pullbackFunctor, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Descent/Scheme/PullbackFunctor.lean, line 759 (StacksFrontier).
Tag 023Z, a definition
Tag 023Z in the Stacks Project.
AlgebraicGeometry.DescentData.trivialFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germs/EffectiveDescentData.lean, line 51. The attribute's comment: “part (1)”.
The functor sending a scheme over
Sto its trivial descent datum relative to the singleton family consisting of𝟙 S.
def trivialFunctor (S : Scheme.{u}) :
Over S ⥤ DescentData (S := S) (X := fun _ : Unit ↦ S) (fun _ ↦ 𝟙 S)
AlgebraicGeometry.DescentData.canonicalFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germs/EffectiveDescentData.lean, line 71. The attribute's comment: “part (2)”.
The functor sending a scheme over
Sto its canonical descent datum relative tof : X ⟶ S, obtained by pulling back its trivial descent datum.
def canonicalFunctor {S X : Scheme.{u}} (f : X ⟶ S) :
Over S ⥤ DescentData (S := S) (X := fun _ : Unit ↦ X) (fun _ ↦ f)
AlgebraicGeometry.DescentData.IsEffective, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germs/EffectiveDescentData.lean, line 80. The attribute's comment: “part (3)”. References: SGA 3 IV (3.5.1).
A descent datum relative to
f : X ⟶ Sis effective if it is isomorphic to the canonical descent datum of a scheme overS.
abbrev IsEffective
(D : DescentData (S := S) (X := fun _ : Unit ↦ X) (fun _ ↦ f)) : Prop
Tag 02VU, a definition
Tag 02VU in the Stacks Project.
AlgebraicGeometry.DescentData.canonicalFamilyFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/CanonicalFamilyDatum.lean, line 127. The attribute's comment: “(1) canonical descent datum on the family X i ×_S U”.
The canonical descent datum relative to a family. The functor sending a scheme
UoverSto the descent datum relative to{X i ⟶ S}whose member overX iis the base change ofUalongX i ⟶ S, obtained by pulling back the trivial descent datum ofU.
def canonicalFamilyFunctor (f : ∀ i, X i ⟶ S) : Over S ⥤ DescentData f
AlgebraicGeometry.DescentData.IsEffectiveFamily, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/CanonicalFamilyDatum.lean, line 140. The attribute's comment: “(2) effective descent datum relative to a family”. References: SGA 3 IV (3.5.1).
Effectivity of a descent datum relative to a family. A descent datum relative to
{X i ⟶ S}is effective if it is isomorphic to the canonical descent datum of a scheme overS.
abbrev IsEffectiveFamily {f : ∀ i, X i ⟶ S} (D : DescentData f) : Prop
AlgebraicGeometry.canonicalFamilyDescentFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSourceTopologies/CanonicalDatum.lean, line 256. The attribute's comment: “part (1)”.
The canonical descent datum functor for an arbitrarily indexed family of schemes over
S: it sends a schemeUoverSto the descent datum whose components are the fibre products ofUwith the members of the family, with the gluing isomorphisms that preserve the projection toU.
def canonicalFamilyDescentFunctor {I : Type v} {S : Scheme.{u}}
{X : I → Scheme.{u}} (f : ∀ i, X i ⟶ S) :
CanonicalDescentFunctor f
AlgebraicGeometry.DescentData.IsFamilyEffective, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSourceTopologies/CanonicalDatum.lean, line 292. The attribute's comment: “part (2)”. References: SGA 3 IV (3.5.1).
A descent datum relative to a family is effective if it is isomorphic to the canonical descent datum of some scheme over the common base.
abbrev IsFamilyEffective (D : DescentData f) : Prop
Sources
Section35.35 Fully faithfulness of the pullback functors#
Section 35.35 of the Stacks Project, Tag 02VV. 12 tags here are carried by 16 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 02VX, a lemma
Tag 02VX in the Stacks Project.
AlgebraicGeometry.Flat.faithful_overPullback_of_surjective, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSourceTopologies/BaseChangeFaithful.lean, line 49.
Stacks Project, Tag 02VX. Base change along a surjective flat morphism of schemes is a faithful functor on the category of schemes over the base.
instance Flat.faithful_overPullback_of_surjective {S' S : Scheme.{u}} (h : S' ⟶ S)
[Flat h] [Surjective h] : (Over.pullback h).Faithful
Tag 0240, a lemma
Tag 0240 in the Stacks Project.
AlgebraicGeometry.pullbackFunctor_faithful, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germs/PullbackFaithful.lean, line 42.
Stacks Project, Tag 0240. Pullback of descent data along a surjective flat morphism is faithful.
theorem pullbackFunctor_faithful
{S S' X X' : Scheme.{u}} {a : X ⟶ S} {a' : X' ⟶ S'} {h : S' ⟶ S}
{f : X' ⟶ X} {comm : f ≫ a = a' ≫ h}
(P : DescentData.PullbackFunctor a a' h f comm) [Surjective f] [Flat f] :
P.functor.Faithful
Tag 0241, a lemma
Tag 0241 in the Stacks Project.
AlgebraicGeometry.pullbackFunctor_fullyFaithful_of_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germs/PullbackFullyFaithful.lean, line 504.
Stacks Project, Tag 0241. Pullback along an fpqc covering over a fixed base scheme is fully faithful on descent data.
public theorem pullbackFunctor_fullyFaithful_of_fpqc
{S X X' : Scheme.{u}} {a : X ⟶ S} {a' : X' ⟶ S} {f : X' ⟶ X}
{comm : f ≫ a = a' ≫ (𝟙 S)}
(P : DescentData.PullbackFunctor a a' (𝟙 S) f comm)
(hcover : Presieve.singleton f ∈ Scheme.fpqcPrecoverage X) :
Nonempty P.functor.FullyFaithful
Tag 0242, a lemma
Tag 0242 in the Stacks Project.
AlgebraicGeometry.DescentData.selfPullbackFunctorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/PullbackFullyFaithful/Equivalence.lean, line 47.
Pullback of descent data along a selfmap
f : X ⟶ XoverSis isomorphic to the identity functor on the category of descent data relative toX ⟶ S.
def selfPullbackFunctorIso {S X : Scheme.{u}} (a : X ⟶ S) (f : X ⟶ X) (hf : f ≫ a = a) :
(pullbackFunctor a a (𝟙 S) f (by simpa using hf)).functor ≅ 𝟭 _
Tag 0243, a lemma
Tag 0243 in the Stacks Project.
AlgebraicGeometry.pullbackFunctor_isEquivalence_of_exists_reverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/PullbackFullyFaithful/Equivalence.lean, line 68.
Pullback of descent data along
f : X' ⟶ Xis an equivalence if there is a morphismX ⟶ X'over the same base scheme.
theorem pullbackFunctor_isEquivalence_of_exists_reverse
{S X X' : Scheme.{u}} (a : X ⟶ S) (a' : X' ⟶ S) (f : X' ⟶ X)
(comm : f ≫ a = a') (h : ∃ g : X ⟶ X', g ≫ a' = a) :
(DescentData.pullbackFunctor a a' (𝟙 S) f (by simpa using comm)).functor.IsEquivalence
Tag 040J, a lemma
Tag 040J in the Stacks Project.
AlgebraicGeometry.pullbackFunctor_faithful_of_source_surjective_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/PullbackFullyFaithful/SourceFaithful.lean, line 70.
Stacks Project, Tag 040J. Pullback of descent data along a morphism whose source is surjective and flat over the base is faithful.
theorem pullbackFunctor_faithful_of_source_surjective_flat
{S X X' : Scheme.{u}} (a : X ⟶ S) (a' : X' ⟶ S) (f : X ⟶ X') (comm : f ≫ a' = a)
[Surjective a] [Flat a] :
(DescentData.pullbackFunctor a' a (𝟙 S) f (by simpa using comm)).functor.Faithful
Tag 040K, a lemma
Tag 040K in the Stacks Project.
AlgebraicGeometry.pullbackFunctor_fullyFaithful_of_source_fpqc, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/PullbackFullyFaithful/SourceFullyFaithful.lean, line 59. References: SGA 1 VIII (5.2).
Pullback along a morphism
X ⟶ X'overSis fully faithful on descent data ifX ⟶ Sis an fpqc covering.
lemma pullbackFunctor_fullyFaithful_of_source_fpqc
{S X X' : Scheme.{u}} (a : X ⟶ S) (a' : X' ⟶ S) (f : X ⟶ X') (comm : f ≫ a' = a)
(hcover : Presieve.singleton a ∈ Scheme.fpqcPrecoverage S) :
Nonempty
(DescentData.pullbackFunctor a' a (𝟙 S) f
(by simpa using comm)).functor.FullyFaithful
Tag 02VZ, a lemma
Tag 02VZ in the Stacks Project.
AlgebraicGeometry.pullbackFunctor_fullyFaithful_of_fpqcRefinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germs/PullbackFpqcRefinement.lean, line 91.
An fpqc refinement of each member of a family induces a fully faithful pullback functor on descent data.
public theorem pullbackFunctor_fullyFaithful_of_fpqcRefinement
{S : Scheme.{u}} (U V : PreZeroHypercover.{u} S)
(α : U.HomOver V (𝟙 S))
(hfpqc : ∀ j : V.I₀,
Presieve.ofArrows
(fun i : {i : U.I₀ // α.s₀ i = j} ↦ U.X i)
(fun i ↦ α.h₀ i.val ≫ eqToHom (congrArg V.X i.property)) ∈
Scheme.fpqcPrecoverage (V.X j)) :
Nonempty ((MorphismOfSchemeFamilies.pullbackFunctor
{ sourceBase := S, targetBase := S,
sourceFamily := U, targetFamily := V,
baseHom := 𝟙 S, familyHom := α }).functor.FullyFaithful)
Tag 02VY, a lemma
Tag 02VY in the Stacks Project.
AlgebraicGeometry.pullbackFunctor_isEquivalence_of_zariskiRefinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Scheme/ZariskiRefinementEquivalence.lean, line 1158.
A fibrewise Zariski refinement induces an equivalence on descent data.
public theorem pullbackFunctor_isEquivalence_of_zariskiRefinement
{S : Scheme.{u}} (U V : PreZeroHypercover.{u} S)
(α : U.HomOver V (𝟙 S))
(hZar : ∀ j : V.I₀,
Presieve.ofArrows
(fun i : {i : U.I₀ // α.s₀ i = j} ↦ U.X i)
(fun i ↦ α.h₀ i.val ≫ eqToHom (congrArg V.X i.property)) ∈
Scheme.zariskiPrecoverage (V.X j)) :
Nonempty ((MorphismOfSchemeFamilies.pullbackFunctor
{ sourceBase := S, targetBase := S,
sourceFamily := U, targetFamily := V,
baseHom := 𝟙 S, familyHom := α }).functor.IsEquivalence)
AlgebraicGeometry.descentData_equivalence_of_zariskiCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Scheme/ZariskiRefinementEquivalence.lean, line 1204.
Schemes over a base are equivalent to descent data for any Zariski cover.
public theorem descentData_equivalence_of_zariskiCovering
{S : Scheme.{u}} (U : PreZeroHypercover.{u} S)
(hZar : Presieve.ofArrows U.X U.f ∈ Scheme.zariskiPrecoverage S) :
Nonempty (Over S ≌ DescentData U.f)
Tag 02W0, a lemma
Tag 02W0 in the Stacks Project.
AlgebraicGeometry.DescentData.canonicalFunctor_fullyFaithful_of_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germs/CanonicalFullyFaithful.lean, line 66. The attribute's comment: “in particular, for a covering by a single morphism”. References: SGA 1 VIII (5.2), “more general”.
If the single morphism
f : X ⟶ Sis an fpqc covering ofS, then the canonical descent datum functorOver S ⥤ DescentDatum fis fully faithful, so schemes overSform a full subcategory of the descent data relative tof.
theorem canonicalFunctor_fullyFaithful_of_fpqc (f : X ⟶ S)
(hcover : Presieve.singleton f ∈ Scheme.fpqcPrecoverage.coverings S) :
Nonempty (canonicalFunctor f).FullyFaithful
AlgebraicGeometry.pullbackFunctor_fullyFaithful_of_refinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/PullbackFullyFaithful/Refinement.lean, line 76.
Stacks 02W0. Let
UandVbe families of schemes overSand letαexhibitUas a refinement ofVover the identity ofS. IfUis an fpqc covering ofS, then the pullback functor from descent data relative toVto descent data relative toUis fully faithful.
theorem pullbackFunctor_fullyFaithful_of_refinement
{S : Scheme.{u}} (U V : PreZeroHypercover.{u} S)
(α : U.HomOver V (𝟙 S))
(hU : Presieve.ofArrows U.X U.f ∈ Scheme.fpqcPrecoverage S) :
Nonempty ((MorphismOfSchemeFamilies.pullbackFunctor
{ sourceBase := S, targetBase := S,
sourceFamily := U, targetFamily := V,
baseHom := 𝟙 S, familyHom := α }).functor.FullyFaithful)
AlgebraicGeometry.fullyFaithful_canonicalFunctor_comp_familyCoproduct_inverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/PullbackFullyFaithful/Refinement.lean, line 108. The attribute's comment: “the schemes over the base as a full subcategory of the descent data”. References: SGA 1 VIII (5.2), “more general”.
Stacks 02W0, final sentence: the schemes over
Sform a full subcategory of the category of descent data relative to an fpqc coveringUofS. The embedding is the canonical descent datum of the coproduct morphism ofU, read as a descent datum for the family through the family–coproduct equivalence.
theorem fullyFaithful_canonicalFunctor_comp_familyCoproduct_inverse
{S : Scheme.{u}} (U : PreZeroHypercover.{u} S)
(hU : Presieve.ofArrows U.X U.f ∈ Scheme.fpqcPrecoverage S) :
Nonempty ((DescentData.canonicalFunctor (Sigma.desc U.f) ⋙
(DescentData.familyCoproductEquivalence U.f).equivalence.inverse).FullyFaithful)
Tag 040L, a remark
Tag 040L in the Stacks Project.
AlgebraicGeometry.isSheaf_relativeHom_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germs/MorphismDescent.lean, line 103. The attribute's comment: “the functor T ↦ Mor_T(X_T, Y_T) on the schemes over S satisfies the sheaf condition for the fpqc topology”. References: SGA 1 VIII (5.2); SGA 3 IV (4.5.13), “Hom_S(X, special case”; SGA 3 VIII (1.7.1), “more general”.
Let
XandYbe schemes overS. The relative morphism functorMor_S(X, Y) : (Sch/S)ᵒᵖ ⥤ Set, which sends anS-schemeTto the set of morphismsX_T ⟶ Y_ToverT, satisfies the sheaf condition for the fpqc topology on the schemes overS.
theorem isSheaf_relativeHom_fpqc (X Y : Over S) :
Presheaf.IsSheaf (Scheme.fpqcTopology.{u}.over S) (relativeHom X Y)
Tag 0AP4, a lemma
Tag 0AP4 in the Stacks Project.
AlgebraicGeometry.DescentDatum.isEffective_of_forall_exists_restrictOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Scheme/DescendedScheme.lean, line 1186. References: SGA 1 VIII (7.2), “local eff ⇒ effective”.
Effectivity of a descent datum is local on the scheme it is carried by. Let
f : X ⟶ Sbe a surjective, quasi-compact, flat morphism of schemes and let(V, φ)be a descent datum relative toX/S. If every point ofVhas an invariant open neighbourhoodW ⊆ Vsuch that the restricted datum(W, φ|_{W ×_S X})is effective, then(V, φ)is effective.
theorem isEffective_of_forall_exists_restrictOpen {S X : Scheme.{u}} {f : X ⟶ S}
[Surjective f] [Flat f] [QuasiCompact f] (D : DescentDatum f)
(h : ∀ v : D.over.left, ∃ (W : D.over.left.Opens) (hW : D.IsTransitionInvariant W),
v ∈ W ∧ DescentData.IsEffective (D.restrictOpen W hW)) :
DescentData.IsEffective D
AlgebraicGeometry.DescentDatum.isEffective_of_forall_exists_restrictOpen_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Scheme/LocalEffectivity.lean, line 59.
Effectivity of a descent datum is local on the scheme it is carried by. Let
f : X ⟶ Sbe a surjective, quasi-compact, flat morphism of schemes and let(V, φ)be a descent datum relative toX/S. Suppose that for everyv ∈ Vthere is an open subschemev ∈ W ⊆ Vwithφ(W ×_S X) ⊆ X ×_S Wand such that the descent datum(W, φ|_{W ×_S X})is effective. Then(V, φ)is effective.Only the inclusion
φ(W ×_S X) ⊆ X ×_S Wis asked for. The reverse inclusion, which makesφ|_{W ×_S X}an isomorphism ontoX ×_S Wand so the gluing isomorphism of the restricted datum, follows from the cocycle condition byAlgebraicGeometry.DescentDatum.isTransitionInvariant_of_le.
theorem isEffective_of_forall_exists_restrictOpen_le {S X : Scheme.{u}} {f : X ⟶ S}
[Surjective f] [Flat f] [QuasiCompact f] (D : DescentDatum f)
(h : ∀ v : D.over.left, ∃ (W : D.over.left.Opens)
(hW : D.transitionPullbackIso.hom ''ᵁ (pullback.fst (D.over.hom ≫ f) f ⁻¹ᵁ W) ≤
pullback.snd f (D.over.hom ≫ f) ⁻¹ᵁ W),
v ∈ W ∧
DescentData.IsEffective (D.restrictOpen W (D.isTransitionInvariant_of_le W hW))) :
DescentData.IsEffective D
Sources
Section35.36 Descending types of morphisms#
Section 35.36 of the Stacks Project, Tag 02W1. 2 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 02W2, a definition
Tag 02W2 in the Stacks Project.
AlgebraicGeometry.SatisfiesDescent, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSourceTopologies/MorphismDescent.lean, line 47.
Stacks Project, Tag 02W2. Morphisms with property
Psatisfy descent for the coverings of a precoverageKif every descent datum relative to aK-covering whose components areP-morphisms is effective.
abbrev SatisfiesDescent (P : MorphismProperty Scheme.{u}) (K : Precoverage Scheme.{u}) : Prop
Tag 02W3, a lemma
Tag 02W3 in the Stacks Project.
AlgebraicGeometry.DescentData.isFamilyEffective_affineBase_of_affineSingleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/DescendingTypesOfMorphisms.lean, line 142. The attribute's comment: “the case of an affine base, for τ = fppf, étale, smooth and syntomic”.
Stacks Project, Tag 02W3, the case of an affine base, for the fppf, étale, smooth and syntomic coverings. Let
Pbe a property of morphisms of schemes over a base which is stable under any base change and such that a nonempty finite disjoint union of morphisms withPagain hasP. Letτbe one of fppf, étale, smooth and syntomic, and suppose that for every surjective morphism of affine schemes which is flat of finite presentation, étale, smooth or syntomic according toτ, every descent datum relative to it whose member hasPis effective. Then every descent datum relative to aτ-covering of an affine scheme whose members havePis effective.
theorem isFamilyEffective_affineBase_of_affineSingleton
{P : MorphismProperty Scheme.{u}} [P.IsStableUnderBaseChange]
(τ : CoveringTopology) (hτ : τ ≠ .zariski)
(hcoprod : ∀ {J : Type u} [Finite J] [Nonempty J] {Y Z : J → Scheme.{u}}
(g : ∀ j, Y j ⟶ Z j), (∀ j, P (g j)) → P (Limits.Sigma.map g))
(haffine : ∀ {A T : Scheme.{u}} [IsAffine A] [IsAffine T] (a : A ⟶ T),
Surjective a → coveringMorphismProperty τ a →
∀ E : DescentDatum a, P (E.obj ()).hom → E.IsEffective)
{S : Scheme.{u}} [IsAffine S] (𝒰 : PreZeroHypercover.{u} S)
(h𝒰 : 𝒰.presieve₀ ∈ Scheme.precoverage (coveringMorphismProperty τ) S)
(D : DescentData 𝒰.f) (hP : ∀ i, P (D.obj i).hom) :
D.IsFamilyEffective
AlgebraicGeometry.DescentData.isFamilyEffective_affineBase_fpqc_of_affineSingleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/DescendingTypesOfMorphisms.lean, line 174. The attribute's comment: “the case of an affine base, for τ = fpqc”.
Stacks Project, Tag 02W3, the case of an affine base, for the fpqc coverings. Let
Pbe a property of morphisms of schemes over a base which is stable under any base change and such that a nonempty finite disjoint union of morphisms withPagain hasP. Suppose that for every surjective flat morphism of affine schemes, every descent datum relative to it whose member hasPis effective. Then every descent datum relative to an fpqc covering of an affine scheme whose members havePis effective.
theorem isFamilyEffective_affineBase_fpqc_of_affineSingleton
{P : MorphismProperty Scheme.{u}} [P.IsStableUnderBaseChange]
(hcoprod : ∀ {J : Type u} [Finite J] [Nonempty J] {Y Z : J → Scheme.{u}}
(g : ∀ j, Y j ⟶ Z j), (∀ j, P (g j)) → P (Limits.Sigma.map g))
(haffine : ∀ {A T : Scheme.{u}} [IsAffine A] [IsAffine T] (a : A ⟶ T),
Surjective a → Flat a → ∀ E : DescentDatum a, P (E.obj ()).hom → E.IsEffective)
{S : Scheme.{u}} [IsAffine S] (𝒰 : PreZeroHypercover.{u} S)
(h𝒰 : 𝒰.presieve₀ ∈ Scheme.fpqcPrecoverage S)
(D : DescentData 𝒰.f) (hP : ∀ i, P (D.obj i).hom) :
D.IsFamilyEffective
AlgebraicGeometry.DescentData.isFamilyEffective_of_affineSingleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/DescendingTypesOfMorphismsGeneralBase.lean, line 121. The attribute's comment: “for τ = fppf, étale, smooth and syntomic, over an arbitrary base, for a covering family indexed in the universe of the schemes”.
Stacks Project, Tag 02W3, for the fppf, étale, smooth and syntomic coverings. Let
Pbe a property of morphisms of schemes over a base which is stable under any base change and such that a nonempty finite disjoint union of morphisms withPagain hasP. Letτbe one of fppf, étale, smooth and syntomic, and suppose that for every surjective morphism of affine schemes which is flat of finite presentation, étale, smooth or syntomic according toτ, every descent datum relative to it whose member hasPis effective. Then every descent datum relative to aτ-covering of an arbitrary scheme whose members havePis effective.
theorem isFamilyEffective_of_affineSingleton [P.IsStableUnderBaseChange]
(τ : CoveringTopology) (hτ : τ ≠ .zariski)
(hcoprod : ∀ {J : Type u} [Finite J] [Nonempty J] {Y Z : J → Scheme.{u}}
(g : ∀ j, Y j ⟶ Z j), (∀ j, P (g j)) → P (Limits.Sigma.map g))
(haffine : ∀ {A T : Scheme.{u}} [IsAffine A] [IsAffine T] (a : A ⟶ T),
Surjective a → coveringMorphismProperty τ a →
∀ E : DescentDatum a, P (E.obj ()).hom → E.IsEffective)
{S : Scheme.{u}} (𝒰 : PreZeroHypercover.{u} S)
(h𝒰 : 𝒰.presieve₀ ∈ Scheme.precoverage (coveringMorphismProperty τ) S)
(D : DescentData 𝒰.f) (hP : ∀ i, P (D.obj i).hom) :
D.IsFamilyEffective
AlgebraicGeometry.DescentData.isFamilyEffective_fpqc_of_affineSingleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/DescendingTypesOfMorphismsGeneralBase.lean, line 150. The attribute's comment: “for τ = fpqc, over an arbitrary base, for a covering family indexed in the universe of the schemes”.
Stacks Project, Tag 02W3, for the fpqc coverings. Let
Pbe a property of morphisms of schemes over a base which is stable under any base change and such that a nonempty finite disjoint union of morphisms withPagain hasP. Suppose that for every surjective flat morphism of affine schemes, every descent datum relative to it whose member hasPis effective. Then every descent datum relative to an fpqc covering of an arbitrary scheme whose members havePis effective.
theorem isFamilyEffective_fpqc_of_affineSingleton [P.IsStableUnderBaseChange]
(hcoprod : ∀ {J : Type u} [Finite J] [Nonempty J] {Y Z : J → Scheme.{u}}
(g : ∀ j, Y j ⟶ Z j), (∀ j, P (g j)) → P (Limits.Sigma.map g))
(haffine : ∀ {A T : Scheme.{u}} [IsAffine A] [IsAffine T] (a : A ⟶ T),
Surjective a → Flat a → ∀ E : DescentDatum a, P (E.obj ()).hom → E.IsEffective)
{S : Scheme.{u}} (𝒰 : PreZeroHypercover.{u} S)
(h𝒰 : 𝒰.presieve₀ ∈ Scheme.fpqcPrecoverage S)
(D : DescentData 𝒰.f) (hP : ∀ i, P (D.obj i).hom) :
D.IsFamilyEffective
AlgebraicGeometry.DescentData.isFamilyEffective_of_affineSingleton_of_anyIndex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/DescendingTypesOfMorphismsGeneralBase.lean, line 178. The attribute's comment: “for τ = fppf, étale, smooth and syntomic, over an arbitrary base, for a covering family indexed in an arbitrary universe”.
Stacks Project, Tag 02W3, for the fppf, étale, smooth and syntomic coverings, with no restriction on the index type of the covering family. Let
Pbe a property of morphisms of schemes over a base which is stable under any base change and such that a nonempty finite disjoint union of morphisms withPagain hasP. Letτbe one of fppf, étale, smooth and syntomic, and suppose that for every surjective morphism of affine schemes which is flat of finite presentation, étale, smooth or syntomic according toτ, every descent datum relative to it whose member hasPis effective. Then every descent datum relative to aτ-covering of an arbitrary scheme, indexed by a type in an arbitrary universe, whose members havePis effective.
theorem isFamilyEffective_of_affineSingleton_of_anyIndex [P.IsStableUnderBaseChange]
(τ : CoveringTopology) (hτ : τ ≠ .zariski)
(hcoprod : ∀ {J : Type u} [Finite J] [Nonempty J] {Y Z : J → Scheme.{u}}
(g : ∀ j, Y j ⟶ Z j), (∀ j, P (g j)) → P (Limits.Sigma.map g))
(haffine : ∀ {A T : Scheme.{u}} [IsAffine A] [IsAffine T] (a : A ⟶ T),
Surjective a → coveringMorphismProperty τ a →
∀ E : DescentDatum a, P (E.obj ()).hom → E.IsEffective)
{I : Type v} {S : Scheme.{u}} {X : I → Scheme.{u}} (f : ∀ i, X i ⟶ S)
(hf : Presieve.ofArrows X f ∈ Scheme.precoverage (coveringMorphismProperty τ) S)
(D : DescentData f) (hP : ∀ i, P (D.obj i).hom) :
D.IsFamilyEffective
AlgebraicGeometry.DescentData.isFamilyEffective_fpqc_of_affineSingleton_of_anyIndex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/DescendingTypesOfMorphismsGeneralBase.lean, line 210. The attribute's comment: “for τ = fpqc, over an arbitrary base, for a covering family indexed in an arbitrary universe”.
Stacks Project, Tag 02W3, for the fpqc coverings, with no restriction on the index type of the covering family. Let
Pbe a property of morphisms of schemes over a base which is stable under any base change and such that a nonempty finite disjoint union of morphisms withPagain hasP. Suppose that for every surjective flat morphism of affine schemes, every descent datum relative to it whose member hasPis effective. Then every descent datum relative to an fpqc covering of an arbitrary scheme, indexed by a type in an arbitrary universe, whose members havePis effective.
theorem isFamilyEffective_fpqc_of_affineSingleton_of_anyIndex [P.IsStableUnderBaseChange]
(hcoprod : ∀ {J : Type u} [Finite J] [Nonempty J] {Y Z : J → Scheme.{u}}
(g : ∀ j, Y j ⟶ Z j), (∀ j, P (g j)) → P (Limits.Sigma.map g))
(haffine : ∀ {A T : Scheme.{u}} [IsAffine A] [IsAffine T] (a : A ⟶ T),
Surjective a → Flat a → ∀ E : DescentDatum a, P (E.obj ()).hom → E.IsEffective)
{I : Type v} {S : Scheme.{u}} {X : I → Scheme.{u}} (f : ∀ i, X i ⟶ S)
(hf : Presieve.ofArrows X f ∈ Scheme.fpqcPrecoverage S)
(D : DescentData f) (hP : ∀ i, P (D.obj i).hom) :
D.IsFamilyEffective
AlgebraicGeometry.DescentData.isFamilyEffective_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FpqcDescentReduction.lean, line 76. The attribute's comment: “the fpqc case over an affine base”.
Let
Pbe stable under base change and closed under finite disjoint unions, and let every descent datum relative to a surjective flat morphism of affine schemes whose component hasPbe effective. Then over an affine base every descent datum relative to an fpqc covering whose components havePis effective.
theorem isFamilyEffective_of_isAffine
[P.IsStableUnderBaseChange]
(hcoprod : ∀ {J : Type u} [Finite J] [Nonempty J] {Y Z : J → Scheme.{u}}
(a : ∀ j, Y j ⟶ Z j), (∀ j, P (a j)) → P (Limits.Sigma.map a))
(haffine : ∀ {T Z : Scheme.{u}} [IsAffine T] [IsAffine Z] (a : Z ⟶ T),
Surjective a → Flat a → ∀ E : DescentDatum a, P (E.obj ()).hom → E.IsEffective)
[IsAffine S] (f : ∀ i, X i ⟶ S)
(hf : Presieve.ofArrows X f ∈ Scheme.fpqcPrecoverage S)
(D : DescentData f) (hP : ∀ i, P (D.obj i).hom) :
D.IsFamilyEffective
Sources
Section35.37 Descending affine morphisms#
Section 35.37 of the Stacks Project, Tag 0244. 2 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0245, a lemma
Tag 0245 in the Stacks Project.
AlgebraicGeometry.DescentData.isFamilyEffective_of_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AffineFpqcFamilyEffective.lean, line 100. The attribute's comment: “for a covering family indexed in the universe of the schemes”. References: SGA 3 IX (2.3), “partial”; SGA 3 VIII (1.7.2), “more general”; SGA 3 X (5.4), “special case”; SGA 3 XXIV (3.11.2), “partial”.
Let
Sbe a scheme, let{X i ⟶ S}be a covering family ofSfor the fpqc topology, and letDbe a descent datum relative to that family all of whose structure morphismsV i ⟶ X iare affine. ThenDis effective: it is isomorphic to the canonical descent datum of a scheme overS.
theorem DescentData.isFamilyEffective_of_isAffineHom {S : Scheme.{u}} {I : Type u}
{X : I → Scheme.{u}} (f : ∀ i, X i ⟶ S)
(hf : Presieve.ofArrows X f ∈ Scheme.fpqcPrecoverage S) (D : DescentData f)
(hD : ∀ i, IsAffineHom (D.obj i).hom) :
D.IsFamilyEffective
AlgebraicGeometry.DescentData.isFamilyEffective_of_forall_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AffineHomFpqcDescent.lean, line 85. The attribute's comment: “the case of an affine base”. References: SGA 3 IX (2.3), “partial”; SGA 3 VIII (1.7.2), “(ii), special case”; SGA 3 XXIV (3.11.2), “special case”.
Stacks, Tag 0245 over an affine base. Let
Sbe an affine scheme, let{X i ⟶ S}be an fpqc covering family and letDbe a descent datum relative to it whose structure morphism over eachX iis affine. ThenDis effective: it is isomorphic to the canonical descent datum of a scheme overS.
theorem isFamilyEffective_of_forall_isAffineHom {ι : Type u} {S : Scheme.{u}} [IsAffine S]
{X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ S)
(hf : Presieve.ofArrows X f ∈ Scheme.fpqcPrecoverage S)
(D : DescentData f) (hP : ∀ i, IsAffineHom (D.obj i).hom) :
D.IsFamilyEffective
AlgebraicGeometry.DescentData.isFamilyEffective_of_isAffineHom_of_anyIndex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FamilyEffectivityLargeIndex.lean, line 211. The attribute's comment: “for a covering family indexed in an arbitrary universe”. References: SGA 3 IX (2.3), “partial”.
Effective descent for affine morphisms along an fpqc covering family indexed in an arbitrary universe. Let
Sbe a scheme, let{X i ⟶ S}be a covering family ofSfor the fpqc topology, indexed by a type in an arbitrary universe, and letDbe a descent datum relative to that family all of whose structure morphismsV i ⟶ X iare affine. ThenDis effective: it is isomorphic to the canonical descent datum of a scheme overS.
theorem isFamilyEffective_of_isAffineHom_of_anyIndex {I : Type v} {S : Scheme.{u}}
{X : I → Scheme.{u}} (f : ∀ i, X i ⟶ S)
(hf : Presieve.ofArrows X f ∈ Scheme.fpqcPrecoverage S) (D : DescentData f)
(hD : ∀ i, IsAffineHom (D.obj i).hom) : D.IsFamilyEffective
Tag 03I0, a lemma
Tag 03I0 in the Stacks Project.
AlgebraicGeometry.DescentData.isFamilyEffective_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/ClosedImmersionFpqcDescent.lean, line 78. References: SGA 3 IV (4.7), “partial”; SGA 3 IV (6.4.1), “partial”; SGA 3 VIII (6.4), “Object effectivity”.
A descent datum relative to an fpqc covering whose components are closed immersions is effective. Let
Sbe a scheme, let{X i ⟶ S}be an fpqc covering and letDbe a descent datum relative to it whose structure morphism over eachX iis a closed immersion. ThenDis isomorphic to the canonical descent datum of a scheme overS.A closed immersion is affine, so this is effective descent for affine morphisms along an fpqc covering, Stacks 0245, at a smaller class of morphisms.
theorem isFamilyEffective_of_isClosedImmersion {I : Type v} {S : Scheme.{u}}
{X : I → Scheme.{u}} (f : ∀ i, X i ⟶ S)
(hf : Presieve.ofArrows X f ∈ Scheme.fpqcPrecoverage S) (D : DescentData f)
(hD : ∀ i, IsClosedImmersion (D.obj i).hom) :
D.IsFamilyEffective
Sources
Section35.38 Descending quasi-affine morphisms#
Section 35.38 of the Stacks Project, Tag 0246. 1 tag here is carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0247, a lemma
Tag 0247 in the Stacks Project.
AlgebraicGeometry.Space.isEffectiveDescentAlongSurjectiveEtale_isQuasiAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiAffineEtaleDescent.lean, line 350. The attribute's comment: “effective descent along a surjective étale chart of the site”. References: SGA 1 VIII (7.9), “surjective étale cover”.
Quasi-affine morphisms descend effectively along the surjective étale morphisms of the big fppf site of
S. If the base change of a morphism of sheavesf : X ⟶ Yalong a surjective étale chartq : c ⟶ aof a representableyoneda.obj a ⟶ Yis representable by quasi-affine morphisms, then so isX ×[Y] yoneda.obj a ⟶ yoneda.obj a.
theorem isEffectiveDescentAlongSurjectiveEtale_isQuasiAffineHom
(B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
IsEffectiveDescentAlongSurjectiveEtale B S hS
(@_root_.AlgebraicGeometry.IsQuasiAffineHom.{u} : MorphismProperty Scheme.{u})
AlgebraicGeometry.DescentData.isFamilyEffective_of_isQuasiAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiAffineFpqcDescent.lean, line 106. References: SGA 1 VIII (7.9), “partial”; SGA 3 IV (4.7), “partial”; SGA 3 IX (2.3), “Effectivity clause”; SGA 3 VIII (1.7.2), “more general”; SGA 3 X (5.4), “special case”; SGA 3 XXIV (3.11.2), “partial”.
Stacks, Tag 0247. Let
Sbe a scheme, let{X i ⟶ S}be an fpqc covering family, indexed by a type in an arbitrary universe, and letDbe a descent datum relative to it each of whose component morphismsV i ⟶ X iis quasi-affine. ThenDis effective: it is isomorphic to the canonical descent datum of a scheme overS.Quasi-affineness is stable under arbitrary base change (Stacks 01SO) and, being Zariski local on the target, closed under finite disjoint unions, so the general-base fpqc reduction of Stacks 02W3,
AlgebraicGeometry.DescentData.isFamilyEffective_fpqc_of_affineSingleton_of_anyIndex, reduces the statement to a covering given by a single surjective flat morphism of affine schemes. That case is the affine-hull argument ofAlgebraicGeometry.DescentDatum.isEffective_of_isIndQuasiAffineHom, applied to a quasi-affine, hence ind-quasi-affine (Stacks 0F1W), morphism.
theorem isFamilyEffective_of_isQuasiAffineHom {I : Type v} {S : Scheme.{u}}
{X : I → Scheme.{u}} (f : ∀ i, X i ⟶ S)
(hf : Presieve.ofArrows X f ∈ Scheme.fpqcPrecoverage S)
(D : DescentData f) (hD : ∀ i, IsQuasiAffineHom (D.obj i).hom) :
D.IsFamilyEffective
Sources
Section35.39 Descent data in terms of sheaves#
Section 35.39 of the Stacks Project, Tag 02W4. 2 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 02W5, a lemma
Tag 02W5 in the Stacks Project.
CategoryTheory.GrothendieckTopology.locallyRepresentableEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Descent/LocallyRepresentableSheaves.lean, line 381. The attribute's comment: “the equivalence of categories”. References: SGA 3 IV (4.6.8).
Let
(C, J)be a site, let{f i : X i ⟶ S}be a covering of an objectSofC, and letGrange over the sheaves of types on the slice siteC/S. The sheaves for which every producth_{X i} ⨯ Gis representable are equivalent to the descent data for the covering with representable components, via the functor sending a sheaf to its canonical descent datum.
noncomputable def locallyRepresentableEquivalence
[HasLimitsOfSize.{max u v, max u v} (Type v)] (hf : Sieve.ofArrows X f ∈ J S) :
(locallyRepresentable J f).FullSubcategory ≌
(descentDataRepresentable J f).FullSubcategory
CategoryTheory.GrothendieckTopology.representableByProdYoneda, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Descent/LocallyRepresentableSheaves.lean, line 393. The attribute's comment: “part (1): the representing objects are the components of the descent datum”.
The object representing the product
h_{X i} ⨯ Gis the object overX irepresenting thei-th component of the canonical descent datum ofG, viewed as an object overS.
noncomputable def representableByProdYoneda (G : Sheaf (J.over S) (Type v)) (i : ι)
{Z : Over (X i)}
(r : ((((J.pseudofunctorOver (Type v)).toDescentData f).obj G).obj i).obj.RepresentableBy Z) :
(CategoryTheory.yoneda.obj (Over.mk (f i)) ⨯ G.obj).RepresentableBy
((Over.map (f i)).obj Z)
CategoryTheory.GrothendieckTopology.effectiveDescentData_toDescentData_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Descent/LocallyRepresentableSheaves.lean, line 412. The attribute's comment: “part (2): representable if and only if effective”. References: SGA 3 IV (4.6.8), “partial”.
The canonical descent datum of a sheaf
GonC/Srelative to a covering{f i : X i ⟶ S}is effective if and only ifGis representable.
theorem effectiveDescentData_toDescentData_iff [J.Subcanonical]
[HasLimitsOfSize.{max u v, max u v} (Type v)] (hf : Sieve.ofArrows X f ∈ J S)
(G : Sheaf (J.over S) (Type v)) :
effectiveDescentData J f (((J.pseudofunctorOver (Type v)).toDescentData f).obj G) ↔
G.obj.IsRepresentable
CategoryTheory.GrothendieckTopology.effectiveDescentDataSheafified_toDescentData_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Descent/LocallyRepresentableSheavesSheafified.lean, line 148. The attribute's comment: “part (2), for sheafified ULift Yoneda”. References: SGA 3 IV (4.6.8), “partial”.
Stacks 02W5, part (2), for sheaves of large sets. Let
(C, J)be a subcanonical site withC : Type uandCategory.{v} C, let{f i : X i ⟶ S}be a covering of an objectSofC, and letGbe a sheaf ofType (max u v)-valued sets on the slice siteC/S. Then the canonical descent datum ofGis effective — isomorphic to the descent datum of a sheafified representable — if and only if the underlying presheaf ofGis representable.
theorem effectiveDescentDataSheafified_toDescentData_iff [J.Subcanonical]
[HasWeakSheafify (J.over S) (Type max u v)] (hf : Sieve.ofArrows X f ∈ J S)
(G : Sheaf (J.over S) (Type max u v)) :
effectiveDescentDataSheafified J f
(((J.pseudofunctorOver (Type max u v)).toDescentData f).obj G) ↔
G.obj.IsRepresentable
Tag 02W6, a remark
Tag 02W6 in the Stacks Project.
CategoryTheory.isRepresentable_overMap_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Descent/LocallyRepresentableSheaves.lean, line 292.
Let
Sbe an object of a categoryC, letTbe an object overSand letFbe a presheaf of types onC/S. Then the producth_T ⨯ Fis representable if and only if the restriction ofFtoC/T.leftis representable.
theorem isRepresentable_overMap_iff {C : Type u} [Category.{v} C] {S : C} (T : Over S)
(F : (Over S)ᵒᵖ ⥤ Type v) :
((Over.map T.hom).op ⋙ F).IsRepresentable ↔ (yoneda.obj T ⨯ F).IsRepresentable
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.