37.12 Smoothness over a… to 37.27 Irreducible components of…
Section37.12 Smoothness over a Noetherian base#
Section 37.12 of the Stacks Project, Tag 02HW. 4 tags here are carried by 4 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 02HX, a lemma
Tag 02HX in the Stacks Project.
Declarations registered for the tag:
InfinitesimalLifting.infinitesimal_lifting_criterion_for_smoothness, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/SmoothnessOverNoetherianBase.lean, line 49 (StacksFrontier).
Tag 02HY, a lemma
Tag 02HY in the Stacks Project.
AlgebraicGeometry.smooth_iff_lifts_finiteType_smallExtensions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/SmoothnessOverNoetherianBase.lean, line 172. References: EGA IV (17.5.4); SGA 1 III (3.1), “(i)<=>(iii), Noetherian”.
A locally finite type morphism to a locally Noetherian scheme is smooth exactly when it lifts against all Artinian small extensions whose map to the base is of finite type.
public theorem smooth_iff_lifts_finiteType_smallExtensions
{X S : Scheme.{u}} (f : X ⟶ S)
[IsLocallyNoetherian S] [LocallyOfFiniteType f] :
Smooth f ↔
∀ ⦃B' B : CommRingCat.{u}⦄ (φ : B' ⟶ B),
InfinitesimalLifting.IsSmallExtension φ →
∀ (α : Spec B ⟶ X) (β : Spec B' ⟶ S),
(LocallyOfFiniteType β ∧ QuasiCompact β) →
α ≫ f = Spec.map φ ≫ β →
∃ γ : Spec B' ⟶ X, Spec.map φ ≫ γ = α ∧ γ ≫ f = β
Tag 0A43, a lemma
Tag 0A43 in the Stacks Project.
AlgebraicGeometry.smoothAt_of_smooth_infinitesimalNeighbourhoods, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/SmoothnessOverNoetherianBase.lean, line 339. The attribute's comment: “smooth”.
Let
f : X ⟶ Sbe a morphism locally of finite type to a locally Noetherian scheme and leti : Z ⟶ Sbe a closed subscheme. If the base changeXₙ = Zₙ ×_S X ⟶ Zₙoffto thenth infinitesimal neighbourhood ofZis smooth for everyn, thenfis smooth at every point off⁻¹(Z).
public theorem smoothAt_of_smooth_infinitesimalNeighbourhoods
{X S Z : Scheme.{u}} [IsLocallyNoetherian S]
(f : X ⟶ S) (i : Z ⟶ S) [LocallyOfFiniteType f] [IsClosedImmersion i]
(hsmooth : ∀ n : ℕ, Smooth (pullback.snd f (Stacks.Thickenings.nthOrderToBase i n)))
(x : X) (hx : f x ∈ Set.range i) :
InfinitesimalLifting.SmoothAt f x
AlgebraicGeometry.etaleAt_of_etale_infinitesimalNeighbourhoods, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/SmoothnessOverNoetherianBase.lean, line 386. The attribute's comment: “etale”.
Let
f : X ⟶ Sbe a morphism locally of finite type to a locally Noetherian scheme and leti : Z ⟶ Sbe a closed subscheme. If the base changeXₙ = Zₙ ×_S X ⟶ Zₙoffto thenth infinitesimal neighbourhood ofZis étale for everyn, thenfis étale at every point off⁻¹(Z).
public theorem etaleAt_of_etale_infinitesimalNeighbourhoods
{X S Z : Scheme.{u}} [IsLocallyNoetherian S]
(f : X ⟶ S) (i : Z ⟶ S) [LocallyOfFiniteType f] [IsClosedImmersion i]
(hetale : ∀ n : ℕ, Etale (pullback.snd f (Stacks.Thickenings.nthOrderToBase i n)))
(x : X) (hx : f x ∈ Set.range i) :
EtaleAt f x
Tag 0D4G, a lemma
Tag 0D4G in the Stacks Project.
AlgebraicGeometry.isFlatAt_of_flat_infinitesimalNeighbourhoods, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/InfinitesimalNeighbourhood/Flatness.lean, line 380.
Flatness over a closed subscheme can be checked on every infinitesimal neighbourhood of that subscheme when the schemes are locally Noetherian.
theorem isFlatAt_of_flat_infinitesimalNeighbourhoods
{X S Z : Scheme.{u}} [IsLocallyNoetherian X] [IsLocallyNoetherian S]
(f : X ⟶ S) (i : Z ⟶ S) [IsClosedImmersion i]
(hflat : ∀ n : ℕ, Flat (pullback.snd f (Stacks.Thickenings.nthOrderToBase i n)))
(x : X) (hx : f x ∈ Set.range i) :
IsFlatAt f.toLRSHom.toShHom x
Sources
Section37.13 The naive cotangent complex#
Section 37.13 of the Stacks Project, Tag 0D0G. 16 tags here are carried by 50 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0D0H, a definition
Tag 0D0H in the Stacks Project.
AlgebraicGeometry.Scheme.naiveCotangentComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/NaiveCotangentComplex.lean, line 70.
Stacks 0D0H. The naive cotangent complex
NL_f = NL_{X/Y}of a morphism of schemesf : X ⟶ Y: the naive cotangent complex of Stacks 08TN of the underlying morphism of ringed spaces off, that is,NL_{𝒪_X / f^{-1}𝒪_Y}.
noncomputable def naiveCotangentComplex :
CochainComplex (_root_.SheafOfModules.{u}
(Stacks.SheafOfModules.Tensor.ringSheaf
(J := Opens.grothendieckTopology X.toRingedSpace.carrier) X.toRingedSpace.sheaf)) ℤ
Tag 0D0I, a lemma
Tag 0D0I in the Stacks Project.
Stacks.NaiveCotangentAffineQuasiIso.quasiIso_comparisonMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/NaiveCotangentAffineQuasiIso.lean, line 739. The attribute's comment: “the canonical map (NL_{A/R})~ to NL_{X/Y}|_V is an isomorphism in D(O_V)”.
If
UandVare affine, the canonical mapcomparisonMap f hVUfrom the sheaf associated toNL_{A/R}to the restriction ofNL_{X/Y}toVis a quasi-isomorphism.
theorem quasiIso_comparisonMap (hU : IsAffineOpen U) (hV : IsAffineOpen V) :
QuasiIso (comparisonMap f hVU)
Tag 0D0J, a lemma
Tag 0D0J in the Stacks Project.
AlgebraicGeometry.Scheme.isZero_homology_naiveCotangentComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/NaiveCotangentCohomologySheaves.lean, line 51. The attribute's comment: “the vanishing outside degrees -1 and 0 only; quasi-coherence and H^0 = Omega are proved separately”.
Stacks 0D0J, vanishing clause. The cohomology sheaves of the naive cotangent complex
NL_{X/Y}of a morphism of schemes vanish outside degrees-1and0: the complex has no terms in those degrees, so it is exact there.
theorem isZero_homology_naiveCotangentComplex (i : ℤ) (hneg : i ≠ -1) (hzero : i ≠ 0) :
IsZero ((naiveCotangentComplex f).homology i)
AlgebraicGeometry.Scheme.naiveCotangentExtZeroAddEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/NaiveCotangentExtZero.lean, line 237. The attribute's comment: “the Ext^0 reading of the degree-zero identification: Ext^0(NL_{X/Y}, G) = Hom(Omega_{X/Y}, G) for a morphism of schemes and an arbitrary sheaf of coefficients, the naive cotangent complex living in cohomological degrees at most zero”. References: SGA 7 VI (4.16), “identification Ext⁰(X₀”.
Ext⁰_{𝒪_X}(NL_{X/Y}, 𝒢) = Hom_{𝒪_X}(Ω_{X/Y}, 𝒢). The naive cotangent complex of a morphism of schemes lives in cohomological degrees≤ 0, soExt⁰out of it is the group of homomorphisms out of its degree0cohomology sheaf, and that sheaf is the sheaf of relative differentials by [Stacks Project, Tag 0D0J].This is the
Ext⁰term of the infinitesimal-automorphism clause of [Stacks Project, Tag 0DY9]: the source writes that clause's group first asExt⁰_{𝒪_X}(NL_{X/k}, 𝒪_X)and then asHom_{𝒪_X}(Ω_{X/k}, 𝒪_X), and this is the passage between the two.fis an arbitrary morphism of schemes and𝒢an arbitrary sheaf of𝒪_X-modules.
def naiveCotangentExtZeroAddEquiv {X Y : Scheme.{u}} (f : X ⟶ Y) (G : X.Modules) :
naiveCotangentExt f G 0 ≃+ (Hom.relativeDifferentials f ⟶ G)
AlgebraicGeometry.Scheme.isQuasicoherent_homology_naiveCotangentComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/NaiveCotangentHomologyQuasicoherent.lean, line 158. The attribute's comment: “quasi-coherence of the cohomology sheaves; not H^0 = Omega, not the vanishing”.
Stacks 0D0J, quasi-coherence clause. Every cohomology sheaf of the naive cotangent complex
NL_{X/Y}of a morphism of schemes is a quasi-coherent sheaf of𝒪_X-modules: in degree-1by the affine-local argument, in degree0because it isΩ_{X/Y}, and in every other degree because it is zero.
theorem isQuasicoherent_homology_naiveCotangentComplex {X Y : Scheme.{u}} (f : X ⟶ Y) (i : ℤ) :
((naiveCotangentComplex f).homology i).IsQuasicoherent
AlgebraicGeometry.Scheme.naiveCotangentComplexHomologyZeroIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/NaiveCotangentHomologyZeroDifferentials.lean, line 66. The attribute's comment: “the degree-zero identification H^0 of NL with Omega; not quasi-coherence, not the vanishing in the other degrees”.
Stacks 0D0J, degree zero. The degree
0cohomology sheaf of the naive cotangent complexNL_{X/Y}of a morphism of schemes is the sheaf of relative differentialsΩ_{X/Y}.
noncomputable def naiveCotangentComplexHomologyZeroIso :
(naiveCotangentComplex f).homology 0 ≅ Hom.relativeDifferentials f
Tag 0D0K, a lemma
Tag 0D0K in the Stacks Project.
Stacks.NaiveCotangentFinitePresentation.exists_affine_quasiIso_associatedDouble_naiveCotangentComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/NaiveCotangentFinitePresentation.lean, line 660. The attribute's comment: “the whole statement. locally on X is read as: for every point x of X there are affine opens V ∋ x of X and U of Y with V ⊆ f^{-1}U, and the complex of quasi-coherent O_V-modules is produced on that V. The source says NL_{X/Y} is quasi-isomorphic TO the two-term complex; what is produced here is a quasi-isomorphism FROM the two-term complex to NL_{X/Y}|_V, which is the same content, a quasi-isomorphism being invertible in D(O_V). The two-term complex is NL(P) sheafified, for a presentation of Gamma(X, V) over Gamma(Y, U) with finitely many variables and finitely many relations, which exists because f is locally of finite presentation; its degree-0 term is finite free on the variables and its degree-(-1) term I/I^2 is generated by the classes of the relations and no better, which is why the two degrees are given DIFFERENT finiteness assertions -- degree 0 IsFinitePresentation, degree -1 IsFiniteType -- exactly as the tag states. The quasi-isomorphism is the sheafification of the comparison NL(P) -> NL_{A/R} of [Stacks, Tag 00S1], taken in its HOMOTOPY EQUIVALENCE form so that it survives an additive functor, composed with the canonical map (NL_{A/R})~ -> NL_{X/Y}|_V of [Stacks, Tag 0D0I]; the target is Scheme.naiveCotangentComplex f ([Stacks, Tag 0D0H]) restricted along V.iota. The sole hypothesis is [LocallyOfFinitePresentation f], which is the source's own: [Stacks, Tag 0D0K] is the lemma for a morphism locally of finite presentation. Every other input is proved: [Stacks, Tag 00S1] in isHomotopyEquiv_nlMapCanonical, [Stacks, Tag 0D0I] in Stacks.NaiveCotangentAffineQuasiIso.quasiIso_comparisonMap, and the finiteness of the two terms in finitePresentation_cotangentSpace and finite_cotangent”.
Stacks 0D0K. Let
f : X ⟶ Ybe locally of finite presentation and letxbe a point ofX. Then there are affine opensV ∋ xofXandUofYwithV ⊆ f^{-1}U, a two-term complexδ : M₁ ⟶ M₀ofΓ(X, V)-modules, and a quasi-isomorphism from the complex of sheaves of𝒪_V-modules associated toδto the restriction ofNL_{X/Y}toV, such that the degree-0term of that complex of sheaves is quasi-coherent of finite presentation and its degree--1term is quasi-coherent of finite type.The two-term complex is
NL(P)for a presentationA = R[x_1, …, x_n]/(g_1, …, g_m)ofA = Γ(X, V)overR = Γ(Y, U)with finitely many variables and finitely many relations, which exists becausefis locally of finite presentation. Its degree-0term is finite free on the variables, hence finitely presented, and its degree--1termI/I²is generated by the classes of the relations, hence finite — and no better, which is why the two degrees are given different finiteness assertions. The quasi-isomorphism is the sheafification of the comparisonNL(P) ⟶ NL_{A/R}of Stacks 00S1, which is a homotopy equivalence and therefore survives any additive functor, followed by the canonical map(NL_{A/R})~ ⟶ NL_{X/Y}|_Vof Stacks 0D0I.
theorem exists_affine_quasiIso_associatedDouble_naiveCotangentComplex (f : X ⟶ Y)
[LocallyOfFinitePresentation f] (x : X) :
∃ (U : Y.Opens) (V : X.Opens) (_ : IsAffineOpen U) (_ : IsAffineOpen V) (_ : x ∈ V)
(_ : V ≤ f ⁻¹ᵁ U) (M₁ M₀ : ModuleCat.{u} Γ(X, V)) (δ : M₁ ⟶ M₀)
(ψ : associatedDouble δ ⟶ restrictedNaiveCotangentComplex f (V := V)),
QuasiIso ψ ∧ ((associatedDouble δ).X 0).IsFinitePresentation ∧
((associatedDouble δ).X (-1)).IsFiniteType ∧
((associatedDouble δ).X 0).IsQuasicoherent ∧
((associatedDouble δ).X (-1)).IsQuasicoherent
Tag 0D0L, a lemma
Tag 0D0L in the Stacks Project.
Stacks.Smooth.formallySmooth_iff_isZero_homology_negOne_and_isLocallyProjective_homology_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/NaiveCotangentFormallySmoothConverse.lean, line 212.
A morphism of schemes
f : X ⟶ Yis formally smooth if and only if the degree-1cohomology sheaf of its naive cotangent complex vanishes and its degree0cohomology sheaf is locally projective.
theorem formallySmooth_iff_isZero_homology_negOne_and_isLocallyProjective_homology_zero :
AlgebraicGeometry.FormallySmooth f ↔
(IsZero ((Scheme.naiveCotangentComplex f).homology (-1)) ∧
Scheme.Modules.IsLocallyProjective ((Scheme.naiveCotangentComplex f).homology 0))
Tag 0D0M, a lemma
Tag 0D0M in the Stacks Project.
Stacks.Smooth.formallyEtale_iff_isZero_homology_naiveCotangentComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/NaiveCotangentFormallyEtale.lean, line 299.
[Stacks Project, Tag 0D0M]. A morphism of schemes
f : X ⟶ Sis formally étale if and only if both cohomology sheaves of its naive cotangent complex vanish,H^{-1}(NL_{X/S}) = H^0(NL_{X/S}) = 0.The forward implication is
Stacks.Smooth.isZero_homology_naiveCotangentComplex_of_formallyEtaleand the converse isStacks.Smooth.formallyEtale_of_isZero_homology_naiveCotangentComplex.
theorem formallyEtale_iff_isZero_homology_naiveCotangentComplex :
FormallyEtale f ↔
IsZero ((Scheme.naiveCotangentComplex f).homology (-1)) ∧
IsZero ((Scheme.naiveCotangentComplex f).homology 0)
Tag 0D0N, a lemma
Tag 0D0N in the Stacks Project.
Stacks.Smooth.smooth_iff_isZero_homology_negOne_and_isFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/NaiveCotangentSmoothCriterion.lean, line 172.
Smoothness read on the naive cotangent complex. A morphism of schemes
f : X ⟶ Sis smooth if and only if it is locally of finite presentation,H⁻¹(NL_{X/S}) = 0, andΩ_{X/S} = H⁰(NL_{X/S})is finite locally free.
theorem smooth_iff_isZero_homology_negOne_and_isFiniteLocallyFree :
AlgebraicGeometry.Smooth f ↔
(AlgebraicGeometry.LocallyOfFinitePresentation f ∧
IsZero ((Scheme.naiveCotangentComplex f).homology (-1)) ∧
SheafOfModules.IsFiniteLocallyFree (R := X.ringCatSheaf)
(Scheme.Hom.relativeDifferentials f))
Stacks.Smooth.smooth_iff_isZero_homology_negOne_and_isFiniteLocallyFree_homology_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/NaiveCotangentSmoothCriterion.lean, line 193. The attribute's comment: “the third clause read on H^0(NL_{X/S}) rather than on Omega_{X/S}”.
Smoothness read on the naive cotangent complex, with the third clause on
H⁰(NL_{X/S}). A morphism of schemesf : X ⟶ Sis smooth if and only if it is locally of finite presentation,H⁻¹(NL_{X/S}) = 0, andH⁰(NL_{X/S})is finite locally free.
theorem smooth_iff_isZero_homology_negOne_and_isFiniteLocallyFree_homology_zero :
AlgebraicGeometry.Smooth f ↔
(AlgebraicGeometry.LocallyOfFinitePresentation f ∧
IsZero ((Scheme.naiveCotangentComplex f).homology (-1)) ∧
SheafOfModules.IsFiniteLocallyFree (R := X.ringCatSheaf)
((Scheme.naiveCotangentComplex f).homology 0))
Tag 0G7Z, a lemma
Tag 0G7Z in the Stacks Project.
AlgebraicGeometry.etale_iff_locallyOfFinitePresentation_and_isZero_naiveCotangentHomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/NaiveCotangentEtale.lean, line 239.
Étale morphisms by the naive cotangent complex. A morphism of schemes
f : X ⟶ Sis étale if and only if it is locally of finite presentation and both cohomology sheavesH⁻¹(NL_{X/S})andH⁰(NL_{X/S})of its naive cotangent complex vanish.
theorem etale_iff_locallyOfFinitePresentation_and_isZero_naiveCotangentHomology (f : X ⟶ S) :
Etale f ↔
(LocallyOfFinitePresentation f ∧
IsZero ((Scheme.naiveCotangentComplex f).homology (-1)) ∧
IsZero ((Scheme.naiveCotangentComplex f).homology 0))
Tag 0FV2, a lemma
Tag 0FV2 in the Stacks Project.
Stacks.Conormal.Sites.homologyNegOneIsoConormalSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ConormalComparison/NaiveCotangentImmersionShift.lean, line 153. The attribute's comment: “degree -1 clause: H^{-1}(NL_{Z/X}) is the conormal sheaf C_{Z/X}”.
Stacks 0FV2, degree
-1clause. For an immersion of schemesi : Z ⟶ Xthe degree-1cohomology sheaf of the naive cotangent complexNL_{Z/X}is the conormal sheaf𝒞_{Z/X}ofZinX.Three identifications are composed.
NL_{Z/X}is the naive cotangent complex of the canonical polynomial presentation of𝒪_Zoveri^{-1}𝒪_X, so its degree-1term is the conormal sheaf of that presentation and not ofi^{-1}𝒪_X ⟶ 𝒪_Zitself; Stacks 08TL for the trivial presentation (Stacks.SheafOfModules.quasiIso_trivialNaiveCotangentComplexComparison) identifies the cohomology of the two complexes. The complex of the trivial presentation isI/I² ⟶ 0, so its degree-1cohomology isI/I²on the nose (Stacks.Conormal.Sites.trivialHomologyNegOneIso). FinallyStacks.Conormal.Sites.sitesConormalSheafIsoConormalSheafidentifies that sites-levelI/I²with the geometric conormal sheaf𝒞_{Z/X}.
def homologyNegOneIsoConormalSheaf :
(AlgebraicGeometry.Scheme.naiveCotangentComplex i).homology (-1) ≅
(Stacks.Conormal.conormalSheaf i : Z.Modules)
Stacks.Conormal.Sites.quasiIso_conormalShiftComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ConormalComparison/NaiveCotangentImmersionShift.lean, line 243. The attribute's comment: “shift clause as a quasi-isomorphism of complexes C_{Z/X}[1] ⟶ NL_{Z/X}”.
Stacks 0FV2, the shift. For an immersion of schemes
i : Z ⟶ Xthe canonical chain map from𝒞_{Z/X}[1]— the cochain complex with the conormal sheaf ofZinXin degree-1and zero in every other degree — to the naive cotangent complexNL_{Z/X}is a quasi-isomorphism.The source states the conclusion as an isomorphism
NL_{Z/X} ≅ 𝒞_{Z/X}[1]inD(𝒪_Z). A quasi-isomorphism of cochain complexes of sheaves of𝒪_Z-modules is the scheme-level content of that statement: it is a map of honest complexes which the localisation functor to the derived category inverts. The statement is given in that form, and the clause label says so.
theorem quasiIso_conormalShiftComparison : QuasiIso (conormalShiftComparison i)
AlgebraicGeometry.Scheme.isZero_homology_zero_naiveCotangentComplex_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/NaiveCotangentImmersionDegreeZero.lean, line 204. The attribute's comment: “degreewise form of the shift statement, degree 0 clause only: H^0(NL_{Z/X}) = 0; NOT the identification of H^{-1}(NL_{Z/X}) with the conormal sheaf”.
Stacks 0FV2, degree
0clause. Leti : Z ⟶ Xbe an immersion of schemes. Then the degree0cohomology sheaf of the naive cotangent complexNL_{Z/X}vanishes.The source states that
NL_{Z/X}is isomorphic toC_{Z/X}[1]inD(𝒪_Z), withC_{Z/X}the conormal sheaf ofZinX. Since both sides are complexes concentrated in one degree, that assertion is the conjunction of the two degreewise statementsH⁻¹(NL_{Z/X}) ≅ C_{Z/X}andH⁰(NL_{Z/X}) = 0. The second is what is proved here; the first is not proved, here or anywhere in this library, and the attribute is scoped accordingly.
theorem isZero_homology_zero_naiveCotangentComplex_of_isImmersion {Z X : Scheme.{u}}
(i : Z ⟶ X) [IsImmersion i] :
Limits.IsZero ((naiveCotangentComplex i).homology 0)
Tag 0E44, a lemma
Tag 0E44 in the Stacks Project.
Stacks.NaiveCotangentSixTermSequence.pullbackToTotalMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentSixTermFirstTerms.lean, line 346. The attribute's comment: “the canonical map f^*NL_{Y/Z} -> NL_{X/Z}, the chain map inducing the first and fourth arrows of the six term sequence”.
Stacks 0E44, the second arrow. The canonical map
f^*NL_{Y/Z} ⟶ NL_{X/Z}of a pair of composable morphisms of schemes: the canonical map of Stacks 0E1Z of the underlying morphisms of ringed spaces, read onNL_{X/Z} = NL_{f ≫ g}throughtotalCompIso.
noncomputable def pullbackToTotalMap :
pullbackNaiveCotangentComplex f g ⟶ Scheme.naiveCotangentComplex (f ≫ g)
Stacks.NaiveCotangentSixTermSequence.totalToRelativeMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentSixTermFirstTerms.lean, line 354. The attribute's comment: “the canonical map NL_{X/Z} -> NL_{X/Y}, the chain map inducing the second and fifth arrows of the six term sequence”.
Stacks 0E44, the third arrow. The canonical map
NL_{X/Z} ⟶ NL_{X/Y}of a pair of composable morphisms of schemes.
noncomputable def totalToRelativeMap :
Scheme.naiveCotangentComplex (f ≫ g) ⟶ Scheme.naiveCotangentComplex f
Stacks.NaiveCotangentSixTermSequence.exact_sixTerm_negOne_total, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentSixTermFirstTerms.lean, line 432. The attribute's comment: “exactness of the six term sequence at its second term, H^{-1}(NL_{X/Z})”.
Stacks 0E44, exactness at
H^{-1}(NL_{X/Z}). For morphisms of schemesf : X ⟶ Yandg : Y ⟶ Zthe sequence
H^{-1}(f^*NL_{Y/Z}) ⟶ H^{-1}(NL_{X/Z}) ⟶ H^{-1}(NL_{X/Y})of cohomology sheaves is exact at the middle term. This is the corresponding assertion of Stacks 0E1Z for the underlying morphisms of ringed spaces.
theorem exact_sixTerm_negOne_total :
(ShortComplex.mk (HomologicalComplex.homologyMap (pullbackToTotalMap f g) (-1))
(HomologicalComplex.homologyMap (totalToRelativeMap f g) (-1))
(homologyMap_pullbackToTotalMap_comp_totalToRelativeMap f g (-1))).Exact
Stacks.NaiveCotangentSixTermSequence.jacobiZariskiConnecting, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentSixTermFirstTerms.lean, line 444. The attribute's comment: “the connecting map H^{-1}(NL_{X/Y}) -> H^0(f^*NL_{Y/Z}), the third arrow of the six term sequence”.
Stacks 0E44, the connecting map
∂ : H^{-1}(NL_{X/Y}) ⟶ H^0(f^*NL_{Y/Z})of the six term sequence, for morphisms of schemesf : X ⟶ Yandg : Y ⟶ Z: the connecting map of Stacks 0E1Z of the underlying morphisms of ringed spaces.
noncomputable def jacobiZariskiConnecting :
(Scheme.naiveCotangentComplex f).homology (-1) ⟶
(pullbackNaiveCotangentComplex f g).homology 0
Stacks.NaiveCotangentSixTermSequence.exact_sixTerm_negOne_relative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentSixTermFirstTerms.lean, line 484. The attribute's comment: “exactness of the six term sequence at its third term, H^{-1}(NL_{X/Y})”.
Stacks 0E44, exactness at
H^{-1}(NL_{X/Y}). For morphisms of schemesf : X ⟶ Yandg : Y ⟶ Zthe sequence
H^{-1}(NL_{X/Z}) ⟶ H^{-1}(NL_{X/Y}) --∂--> H^0(f^*NL_{Y/Z})of cohomology sheaves is exact at the middle term.
theorem exact_sixTerm_negOne_relative :
(ShortComplex.mk (HomologicalComplex.homologyMap (totalToRelativeMap f g) (-1))
(jacobiZariskiConnecting f g)
(homologyMap_totalToRelativeMap_comp_connecting f g)).Exact
Stacks.NaiveCotangentSixTermSequence.pullbackHomologyZeroIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentSixTermFirstTerms.lean, line 546. The attribute's comment: “the fourth term: the identification H^0(f^NL_{Y/Z}) = f^Omega_{Y/Z} for the inverse-image-then-extend-scalars model of the pullback, the model the first four terms are written over”.
Stacks 0E44, the fourth term. The degree
0cohomology sheaf off^*NL_{Y/Z}isf^*Ω_{Y/Z}.The pullback is the one of Stacks 08TM and 0E1Z, the inverse image with scalars extended, which is the model the first four terms of the sequence are written over;
pullbackComplexIsoidentifies it with Mathlib'sAlgebraicGeometry.Scheme.Modules.pullback, for which the degree0identification isStacks.NaiveCotangentSixTermSequence.modulePullbackNaiveCotangentComplexHomologyZeroIso. It is this identification that makes the connecting map land inf^*Ω_{Y/Z}, so that the three terms proved here and the three degree0terms are one sequence.
noncomputable def pullbackHomologyZeroIso :
(pullbackNaiveCotangentComplex f g).homology 0 ≅
(Scheme.Modules.pullback f).obj (Scheme.Hom.relativeDifferentials g)
Stacks.NaiveCotangentSixTermSequence.connectingDifferentials, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentSixTermFirstTerms.lean, line 556. The attribute's comment: “the connecting map with its target written as f^*Omega_{Y/Z}”.
Stacks 0E44, the third arrow with its target written as
f^*Ω_{Y/Z}. The connecting map of the six term sequence, read through the identification of its targetH^0(f^*NL_{Y/Z})withf^*Ω_{Y/Z}.
noncomputable def connectingDifferentials :
(Scheme.naiveCotangentComplex f).homology (-1) ⟶
(Scheme.Modules.pullback f).obj (Scheme.Hom.relativeDifferentials g)
Stacks.NaiveCotangentSixTermSequence.exact_sixTerm_zero_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentSixTermFirstTerms.lean, line 569. The attribute's comment: “exactness of the six term sequence at its fourth term, H^0(f^NL_{Y/Z}) = f^Omega_{Y/Z}”.
Stacks 0E44, exactness at
H^0(f^*NL_{Y/Z}). For morphisms of schemesf : X ⟶ Yandg : Y ⟶ Zthe sequence
H^{-1}(NL_{X/Y}) --∂--> H^0(f^*NL_{Y/Z}) ⟶ H^0(NL_{X/Z})of cohomology sheaves is exact at the middle term.
theorem exact_sixTerm_zero_pullback :
(ShortComplex.mk (jacobiZariskiConnecting f g)
(HomologicalComplex.homologyMap (pullbackToTotalMap f g) 0)
(connecting_comp_homologyMap_pullbackToTotalMap f g)).Exact
Stacks.NaiveCotangentSixTermSequence.exact_sixTerm_zero_total, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentSixTermFirstTerms.lean, line 588. The attribute's comment: “exactness of the six term sequence at its fifth term, H^0(NL_{X/Z}) = Omega_{X/Z}”.
Stacks 0E44, exactness at
H^0(NL_{X/Z}). For morphisms of schemesf : X ⟶ Yandg : Y ⟶ Zthe sequence
H^0(f^*NL_{Y/Z}) ⟶ H^0(NL_{X/Z}) ⟶ H^0(NL_{X/Y})of cohomology sheaves is exact at the middle term. With the degree
0identifications of Stacks 0D0J andpullbackHomologyZeroIsothis is exactness atΩ_{X/Z}; it is stated on the cohomology sheaves so that it is the same sequence as the three nodes above.
theorem exact_sixTerm_zero_total :
(ShortComplex.mk (HomologicalComplex.homologyMap (pullbackToTotalMap f g) 0)
(HomologicalComplex.homologyMap (totalToRelativeMap f g) 0)
(homologyMap_pullbackToTotalMap_comp_totalToRelativeMap f g 0)).Exact
Stacks.NaiveCotangentSixTermSequence.epi_homologyMap_totalToRelativeMap_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentSixTermFirstTerms.lean, line 600. The attribute's comment: “the final -> 0 of the six term sequence, its exactness at H^0(NL_{X/Y}) = Omega_{X/Y}”.
Stacks 0E44, the final
⟶ 0. The canonical mapNL_{X/Z} ⟶ NL_{X/Y}is surjective on degree0cohomology sheaves, that is, the six term sequence is exact atH^0(NL_{X/Y}). With the degree0identification of Stacks 0D0J this is exactness atΩ_{X/Y}.
theorem epi_homologyMap_totalToRelativeMap_zero :
Epi (HomologicalComplex.homologyMap (totalToRelativeMap f g) 0)
Stacks.NaiveCotangentSixTermSequence.isZero_homology_modulePullbackNaiveCotangentComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentSixTermSequence.lean, line 166. The attribute's comment: “the vanishing of H^i(f^*NL_{Y/Z}) outside degrees -1 and 0 only”.
Stacks 0E44, the extent of the sequence. The cohomology sheaves of
f^*NL_{Y/Z}vanish outside degrees-1and0. Together with the same statement forNL_{X/Z}andNL_{X/Y}(AlgebraicGeometry.Scheme.isZero_homology_naiveCotangentComplex) this is why the sequence of Stacks 0E44 has six terms, starting atH^{-1}(f^*NL_{Y/Z})and ending at0after the degree0cohomology sheaf ofNL_{X/Y}.
theorem isZero_homology_modulePullbackNaiveCotangentComplex (i : ℤ) (hneg : i ≠ -1)
(hzero : i ≠ 0) :
IsZero ((modulePullbackNaiveCotangentComplex f g).homology i)
Stacks.NaiveCotangentSixTermSequence.modulePullbackNaiveCotangentComplexHomologyZeroIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentSixTermSequence.lean, line 180. The attribute's comment: “the fourth term for Mathlib's model of the pullback: the identification H^0(f^NL_{Y/Z}) = f^Omega_{Y/Z}, which Stacks.NaiveCotangentSixTermSequence.pullbackHomologyZeroIso carries to the model the sequence itself is written over”.
Stacks 0E44, the fourth term. The degree
0cohomology sheaf off^*NL_{Y/Z}isf^*Ω_{Y/Z}. The pullback of sheaves of modules alongfis a left adjoint, hence preserves the cokernel that computes the degree0cohomology sheaf of a complex with nothing above degree0, andH^0(NL_{Y/Z})isΩ_{Y/Z}by Stacks 0D0J.
noncomputable def modulePullbackNaiveCotangentComplexHomologyZeroIso :
(modulePullbackNaiveCotangentComplex f g).homology 0 ≅
(Scheme.Modules.pullback f).obj (Scheme.Hom.relativeDifferentials g)
Stacks.NaiveCotangentSixTermSequence.differentialsSequence_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentSixTermSequence.lean, line 202. The attribute's comment: “the last three terms and their exactness, for the canonical maps of relative differentials of 01UX; the six term sequence itself, with the arrows induced by the canonical maps of naive cotangent complexes throughout, is in StacksFrontier.AlgebraicGeometry.MoreMorphisms.NaiveCotangentSixTermFirstTerms”.
Stacks 0E44, the last three terms. For morphisms of schemes
f : X ⟶ Yandg : Y ⟶ Zthe last three terms of the six term sequence of cohomology sheaves,
f^*Ω_{Y/Z} ⟶ Ω_{X/Z} ⟶ Ω_{X/Y} ⟶ 0,form an exact sequence: the composite of the two canonical maps of relative differentials is zero, the resulting short complex is exact at
Ω_{X/Z}, and the second map is an epimorphism. The three terms are the degree0cohomology sheaves off^*NL_{Y/Z}, ofNL_{X/Z}and ofNL_{X/Y}, bymodulePullbackNaiveCotangentComplexHomologyZeroIsoand by Stacks 0D0J.
theorem differentialsSequence_exact :
∃ h : Scheme.Hom.relativeDifferentialsMap f g (f ≫ g) (𝟙 Z)
(Category.comp_id (f ≫ g)).symm ≫ f.toRelativeDifferentials g = 0,
(ShortComplex.mk _ _ h).Exact ∧ Epi (f.toRelativeDifferentials g)
Tag 0FV3, a lemma
Tag 0FV3 in the Stacks Project.
Stacks.NaiveCotangentCompositionTriangle.coneMap_comp_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentCompositionTriangle.lean, line 150. The attribute's comment: “the canonical map f^NL_{Y/Z} -> C(NL_{X/Z} -> NL_{X/Y})[-1] of 0E1Z and its compatibility, up to the sign of the cocone projection, with the canonical map f^NL_{Y/Z} -> NL_{X/Z}; NOT its invertibility, which is where the complete intersection hypothesis enters and which is isIso_Q_map_coneMap_of_lci”.
Stacks 0FV3, the comparison. The canonical map
f^*NL_{Y/Z} ⟶ C(NL_{X/Z} ⟶ NL_{X/Y})[-1]of Stacks 0E1Z, composed with the projection of the mapping cocone ontoNL_{X/Z}, is the negative of the canonical mapf^*NL_{Y/Z} ⟶ NL_{X/Z}. This is what makes the comparison a lift of that canonical map; the sign is the one between the projection out of the mapping cocone and the projection of Stacks 0E1Z.
theorem coneMap_comp_fst :
ringedSpaceNaiveCotangentConeMap f g ≫ mappingCocone.fst (relativeNaiveCotangentMap f g) =
-pulledNaiveCotangentMap f g
Stacks.NaiveCotangentCompositionTriangle.triangle_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentCompositionTriangle.lean, line 182. The attribute's comment: “the distinguished triangle C(NL_{X/Z} -> NL_{X/Y})[-1] -> NL_{X/Z} -> NL_{X/Y} -> C(NL_{X/Z} -> NL_{X/Y})[-1][1] of D(O_X), whose second morphism is the canonical map, together with the canonical map of 0E1Z into its first vertex (coneMap_comp_fst); NOT the invertibility of that comparison, which is where the complete intersection hypothesis enters, and NOT the recovery of the six-term exact sequence of 0E44 -- those two are isIso_Q_map_coneMap_of_lci and lciTriangle_recovers_sixTerm, and the triangle with f^*NL_{Y/Z} as its first vertex is lciTriangle_distinguished”.
Stacks 0FV3, the triangle. The triangle on the canonical map
NL_{X/Z} ⟶ NL_{X/Y}, with the shift by-1of its cone as first vertex, is a distinguished triangle ofD(𝒪_X).
theorem triangle_distinguished : triangle f g ∈ distTriang _
Stacks.NaiveCotangentCompositionTriangle.isIso_Q_map_coneMap_of_lci, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentCompositionTriangleLci.lean, line 126. The attribute's comment: “the canonical map f^*NL_{Y/Z} -> C(NL_{X/Z} -> NL_{X/Y})[-1] of 0E1Z is an ISOMORPHISM in D(O_X) when X -> Y is a complete intersection morphism, which is the reduction the source's proof makes”.
Stacks 0FV3, the isomorphism. For morphisms of schemes
f : X ⟶ Yandg : Y ⟶ Zwithfa local complete intersection morphism, the canonical map
f^*NL_{Y/Z} ⟶ C(NL_{X/Z} ⟶ NL_{X/Y})[-1]of Stacks 0E1Z is an isomorphism in
D(𝒪_X).This is the reduction the source makes: the triangle of Stacks 0FV3 is the triangle of the mapping cocone of
NL_{X/Z} ⟶ NL_{X/Y}with its first vertex replaced byf^*NL_{Y/Z}along this isomorphism. The map is surjective onH^{-1}and an isomorphism onH⁰for an arbitrary pair of composable morphisms of ringed spaces; injectivity onH^{-1}is what the complete intersection hypothesis supplies, through Stacks 07D4 at the stalks.
theorem isIso_Q_map_coneMap_of_lci (hf : IsLocalCompleteIntersectionMorphism f) :
IsIso (DerivedCategory.Q.map
(ringedSpaceNaiveCotangentConeMap f.toLRSHom.toShHom g.toLRSHom.toShHom))
Stacks.NaiveCotangentCompositionTriangle.lciTriangle_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentCompositionTriangleLci.lean, line 170. The attribute's comment: “the canonical distinguished triangle f^NL_{Y/Z} -> NL_{X/Z} -> NL_{X/Y} -> f^NL_{Y/Z}[1] of D(O_X) for a complete intersection morphism X -> Y, with its first two morphisms the canonical maps (lciTriangle_mor₁, lciTriangle_mor₂)”. References: SGA 6 VIII (2.6), “more general”.
Stacks 0FV3. For morphisms of schemes
f : X ⟶ Yandg : Y ⟶ Zwithfa local complete intersection morphism, the canonical triangle
f^*NL_{Y/Z} ⟶ NL_{X/Z} ⟶ NL_{X/Y} ⟶ f^*NL_{Y/Z}[1]is a distinguished triangle of
D(𝒪_X): it is the triangle of the mapping cocone of the canonical mapNL_{X/Z} ⟶ NL_{X/Y}, which is distinguished, with its first vertex replaced along the comparison of Stacks 0E1Z, an isomorphism byisIso_Q_map_coneMap_of_lci. Its first two morphisms are the canonical maps, bylciTriangle_mor₁andlciTriangle_mor₂.
theorem lciTriangle_distinguished (hf : IsLocalCompleteIntersectionMorphism f) :
lciTriangle f g hf ∈ distTriang _
Stacks.NaiveCotangentCompositionTriangle.lciTriangle_recovers_sixTerm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentCompositionTriangleLci.lean, line 197. The attribute's comment: “the recovery of the six-term exact sequence of 0E44 from lciTriangle: its first two morphisms are the images under Q of the canonical chain maps f^*NL_{Y/Z} -> NL_{X/Z} and NL_{X/Z} -> NL_{X/Y}, and the six-term sequence of the maps those induce on cohomology sheaves, with the connecting morphism of the long exact sequence of the cone, is exact at its four interior terms and ends in -> 0”.
Stacks 0FV3: the triangle recovers the six-term exact sequence of Stacks 0E44. The long exact sequence of cohomology sheaves of the triangle
f^*NL_{Y/Z} ⟶ NL_{X/Z} ⟶ NL_{X/Y} ⟶ f^*NL_{Y/Z}[1]is the six-term exact sequence
H^{-1}(f^*NL_{Y/Z}) ⟶ H^{-1}(NL_{X/Z}) ⟶ H^{-1}(NL_{X/Y}) --∂--> H⁰(f^*NL_{Y/Z}) ⟶H⁰(NL_{X/Z}) ⟶ H⁰(NL_{X/Y}) ⟶ 0:its five assertions are exactness at the four interior terms and the final
⟶ 0. The two arrows are the maps induced by the canonical chain maps, whose images underDerivedCategory.Qare the first two morphisms of the triangle bylciTriangle_mor₁andlciTriangle_mor₂, and the connecting morphism isStacks.SheafOfModules.ringedSpaceJacobiZariskiConnecting, the connecting morphism of the long exact sequence of the cone read through the comparison of Stacks 0E1Z. The sequence has six terms and no more because all three vertices have vanishing cohomology outside degrees-1and0.
theorem lciTriangle_recovers_sixTerm (hf : IsLocalCompleteIntersectionMorphism f) :
(lciTriangle f g hf).mor₁ =
DerivedCategory.Q.map
(pulledNaiveCotangentMap f.toLRSHom.toShHom g.toLRSHom.toShHom) ∧
(lciTriangle f g hf).mor₂ =
DerivedCategory.Q.map
(relativeNaiveCotangentMap f.toLRSHom.toShHom g.toLRSHom.toShHom) ∧
(ringedSpaceJacobiZariskiHomologySequence f.toLRSHom.toShHom
g.toLRSHom.toShHom (-1)).Exact ∧
(ShortComplex.mk
(HomologicalComplex.homologyMap
(relativeNaiveCotangentMap f.toLRSHom.toShHom g.toLRSHom.toShHom) (-1))
(ringedSpaceJacobiZariskiConnecting f.toLRSHom.toShHom g.toLRSHom.toShHom)
(homologyMap_comp_ringedSpaceJacobiZariskiConnecting
f.toLRSHom.toShHom g.toLRSHom.toShHom)).Exact ∧
(ShortComplex.mk
(ringedSpaceJacobiZariskiConnecting f.toLRSHom.toShHom g.toLRSHom.toShHom)
(HomologicalComplex.homologyMap
(pulledNaiveCotangentMap f.toLRSHom.toShHom g.toLRSHom.toShHom) 0)
(ringedSpaceJacobiZariskiConnecting_comp_homologyMap
f.toLRSHom.toShHom g.toLRSHom.toShHom)).Exact ∧
(ringedSpaceJacobiZariskiHomologySequence f.toLRSHom.toShHom
g.toLRSHom.toShHom 0).Exact ∧
Epi (HomologicalComplex.homologyMap
(relativeNaiveCotangentMap f.toLRSHom.toShHom g.toLRSHom.toShHom) 0)
Stacks.NaiveCotangentCompositionTriangle.connecting_comp_homologyMap_eq_homologyδOfTriangle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentLciTriangleSixTerm.lean, line 142. The attribute's comment: “the connecting map of the six-term sequence of 0E44, read along H^0 of the canonical map of 0E1Z, is the connecting morphism of the long exact sequence of the triangle of the mapping cocone of NL_{X/Z} -> NL_{X/Y}”.
The connecting map of Stacks 0E44 is a triangle connecting morphism. Composed with the map induced on
H⁰by the canonical map of Stacks 0E1Z it is the connecting morphism of the long exact sequence of the triangle
C(NL_{X/Z} ⟶ NL_{X/Y})[-1] ⟶ NL_{X/Z} ⟶ NL_{X/Y} ⟶ C(NL_{X/Z} ⟶ NL_{X/Y})[-1][1]of the mapping cocone, whose image in
D(𝒪_X)is the triangle of Stacks 0FV3 before its first vertex is replaced byf^*NL_{Y/Z}along that same map.
theorem connecting_comp_homologyMap_eq_homologyδOfTriangle :
jacobiZariskiConnecting f g ≫ HomologicalComplex.homologyMap
(ringedSpaceNaiveCotangentConeMap (ringedSpaceHom f) (ringedSpaceHom g)) 0 =
CochainComplex.homologyδOfTriangle
(CochainComplex.mappingCocone.triangle (iteratedRelativeMap f g)) (-1) 0 (by omega)
Stacks.NaiveCotangentCompositionTriangle.lciSchemeTriangle_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentLciTriangleSixTerm.lean, line 226. The attribute's comment: “the canonical distinguished triangle f^NL_{Y/Z} -> NL_{X/Z} -> NL_{X/Y} -> f^NL_{Y/Z}[1] of D(O_X) for a complete intersection morphism X -> Y, written over the complexes and the two canonical chain maps of the six-term sequence of 0E44 (lciSchemeTriangle_mor₁, lciSchemeTriangle_mor₂)”. References: SGA 6 VIII (2.6), “more general”.
Stacks 0FV3. For morphisms of schemes
f : X ⟶ Yandg : Y ⟶ Zwithfa local complete intersection morphism, the canonical triangle
f^*NL_{Y/Z} ⟶ NL_{X/Z} ⟶ NL_{X/Y} ⟶ f^*NL_{Y/Z}[1]is a distinguished triangle of
D(𝒪_X), withNL_{X/Z}the naive cotangent complex off ≫ gand its first two morphisms the two canonical chain maps of the six-term exact sequence of Stacks 0E44.It is the triangle of
Stacks.NaiveCotangentCompositionTriangle.lciTrianglewith its second vertex transported along the identification ofNL_{f ≫ g}with its iterated spelling.
theorem lciSchemeTriangle_distinguished (hf : IsLocalCompleteIntersectionMorphism f) :
lciSchemeTriangle f g hf ∈ distTriang _
Stacks.NaiveCotangentCompositionTriangle.δ_lciSchemeTriangle_comp_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentLciTriangleSixTerm.lean, line 262. The attribute's comment: “the connecting morphism of the triangle, read along H^0 of the canonical map of 0E1Z, is the negative of the connecting morphism of the long exact sequence of the triangle of the mapping cocone of NL_{X/Z} -> NL_{X/Y}”.
The connecting morphism of the triangle of Stacks 0FV3. Composed with the map induced on
H⁰by the canonical map of Stacks 0E1Z it is the negative of the connecting morphism of the triangle of the mapping cocone ofNL_{X/Z} ⟶ NL_{X/Y}. The sign is the one between the projection out of the mapping cocone and the projection through which Stacks 0E1Z characterises its canonical map; it is the price of the triangle's first morphism being the canonical mapf^*NL_{Y/Z} ⟶ NL_{X/Z}with no sign.
theorem δ_lciSchemeTriangle_comp_map (hf : IsLocalCompleteIntersectionMorphism f) :
DerivedCategory.HomologySequence.δ (lciSchemeTriangle f g hf) (-1) 0 (by omega) ≫
(DerivedCategory.homologyFunctor (_root_.SheafOfModules.{u}
(Stacks.SheafOfModules.Tensor.ringSheaf
(J := Opens.grothendieckTopology (X.toRingedSpace : TopCat))
X.toRingedSpace.sheaf)) (0 : ℤ)).map (DerivedCategory.Q.map
(ringedSpaceNaiveCotangentConeMap (ringedSpaceHom f) (ringedSpaceHom g))) =
-(DerivedCategory.HomologySequence.δ
(triangle (ringedSpaceHom f) (ringedSpaceHom g)) (-1) 0 (by omega))
Stacks.NaiveCotangentCompositionTriangle.lciSchemeTriangle_recovers_sixTerm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentLciTriangleSixTerm.lean, line 307. The attribute's comment: “the recovery of the six-term exact sequence of 0E44 from lciSchemeTriangle: its first two morphisms are the images under Q of the two canonical chain maps of 0E44, its connecting morphism and the connecting map of 0E44 are both the connecting morphism of the long exact sequence of the triangle of the mapping cocone read along H^0 of the canonical map of 0E1Z, and the six-term sequence of those arrows is exact at its four interior terms and ends in -> 0”.
Stacks 0FV3: the triangle recovers the six-term exact sequence of Stacks 0E44. For morphisms of schemes
f : X ⟶ Yandg : Y ⟶ Zwithfa local complete intersection morphism, the long exact sequence of cohomology sheaves of the distinguished triangle
f^*NL_{Y/Z} ⟶ NL_{X/Z} ⟶ NL_{X/Y} ⟶ f^*NL_{Y/Z}[1]is the six-term exact sequence
H^{-1}(f^*NL_{Y/Z}) ⟶ H^{-1}(NL_{X/Z}) ⟶ H^{-1}(NL_{X/Y}) --∂--> f^*Ω_{Y/Z} ⟶ Ω_{X/Z} ⟶Ω_{X/Y} ⟶ 0of Stacks 0E44. The nine assertions below are: its first two morphisms are the images under
DerivedCategory.Qof the two canonical chain mapspullbackToTotalMapandtotalToRelativeMapof Stacks 0E44, which induce four of the five arrows; its connecting morphism and the connecting mapjacobiZariskiConnectingof Stacks 0E44 both become, along the map induced onH⁰by the canonical map of Stacks 0E1Z, the connecting morphism of the long exact sequence of the triangle of the mapping cocone — up to the sign of the cocone projection; and the sequence of those arrows is exact at its four interior terms and ends in⟶ 0. The last three terms aref^*Ω_{Y/Z},Ω_{X/Z}andΩ_{X/Y}byStacks.NaiveCotangentSixTermSequence.pullbackHomologyZeroIsoand Stacks 0D0J.
theorem lciSchemeTriangle_recovers_sixTerm (hf : IsLocalCompleteIntersectionMorphism f) :
(lciSchemeTriangle f g hf).mor₁ = DerivedCategory.Q.map (pullbackToTotalMap f g) ∧
(lciSchemeTriangle f g hf).mor₂ = DerivedCategory.Q.map (totalToRelativeMap f g) ∧
DerivedCategory.HomologySequence.δ (lciSchemeTriangle f g hf) (-1) 0 (by omega) ≫
(DerivedCategory.homologyFunctor (_root_.SheafOfModules.{u}
(Stacks.SheafOfModules.Tensor.ringSheaf
(J := Opens.grothendieckTopology (X.toRingedSpace : TopCat))
X.toRingedSpace.sheaf)) (0 : ℤ)).map (DerivedCategory.Q.map
(ringedSpaceNaiveCotangentConeMap (ringedSpaceHom f) (ringedSpaceHom g))) =
-(DerivedCategory.HomologySequence.δ
(triangle (ringedSpaceHom f) (ringedSpaceHom g)) (-1) 0 (by omega)) ∧
jacobiZariskiConnecting f g ≫ HomologicalComplex.homologyMap
(ringedSpaceNaiveCotangentConeMap (ringedSpaceHom f) (ringedSpaceHom g)) 0 =
CochainComplex.homologyδOfTriangle
(CochainComplex.mappingCocone.triangle (iteratedRelativeMap f g)) (-1) 0 (by omega) ∧
(ShortComplex.mk (HomologicalComplex.homologyMap (pullbackToTotalMap f g) (-1))
(HomologicalComplex.homologyMap (totalToRelativeMap f g) (-1))
(homologyMap_pullbackToTotalMap_comp_totalToRelativeMap f g (-1))).Exact ∧
(ShortComplex.mk (HomologicalComplex.homologyMap (totalToRelativeMap f g) (-1))
(jacobiZariskiConnecting f g)
(homologyMap_totalToRelativeMap_comp_connecting f g)).Exact ∧
(ShortComplex.mk (jacobiZariskiConnecting f g)
(HomologicalComplex.homologyMap (pullbackToTotalMap f g) 0)
(connecting_comp_homologyMap_pullbackToTotalMap f g)).Exact ∧
(ShortComplex.mk (HomologicalComplex.homologyMap (pullbackToTotalMap f g) 0)
(HomologicalComplex.homologyMap (totalToRelativeMap f g) 0)
(homologyMap_pullbackToTotalMap_comp_totalToRelativeMap f g 0)).Exact ∧
Epi (HomologicalComplex.homologyMap (totalToRelativeMap f g) 0)
Tag 0G80, a lemma
Tag 0G80 in the Stacks Project.
AlgebraicGeometry.Smooth.of_comp_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Smooth/CancelEtale.lean, line 51.
Let
X → Y → Zbe morphisms of schemes. IfX → Zis smooth andY → Zis étale, thenX → Yis smooth.
public theorem Smooth.of_comp_of_etale {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
[Smooth (f ≫ g)] [Etale g] : Smooth f
Tag 0FV4, a lemma
Tag 0FV4 in the Stacks Project.
Stacks.NaiveCotangentFormallySmoothComparison.quasiIso_naiveCotangentToDifferentialsSingle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentFormallySmoothComparison.lean, line 260. The attribute's comment: “the 0D0L input NL_{P/Y} = Omega_{P/Y} as a quasi-isomorphism of complexes”.
The 0D0L input of [Stacks Project, Tag 0FV4]. For a formally smooth morphism of schemes
g : P ⟶ Ythe canonical chain mapNL_{P/Y} ⟶ Ω_{P/Y}[0]is a quasi-isomorphism: the naive cotangent complex ofgis identified with its sheaf of relative differentials placed in degree0.This is the step the proof of 0FV4 records as
NL_{P/Y} = Ω_{P/Y}. Its two ingredients are the clauses of [Stacks Project, Tag 0D0L] proved for a formally smooth morphism, namely the vanishing of the cohomology sheaves outside degree0(Stacks.Smooth.isZero_homology_naiveCotangentComplex_of_formallySmooth, which rests onStacks.Smooth.isZero_homology_negOne_naiveCotangentComplex_of_formallySmooth), together with the degree-zero identificationH⁰(NL_{P/Y}) = Ω_{P/Y}of [Stacks Project, Tag 0D0J]. Those are statements about cohomology sheaves; what is added here is the chain map itself, which is what 0FV4 uses.As in
Stacks.Conormal.Sites.quasiIso_conormalShiftComparison— the corresponding step of 0FV4 coming from [Stacks Project, Tag 0FV2] — the conclusion is given as a quasi-isomorphism of complexes of sheaves of𝒪_P-modules, which is the chain-level content of the source's identification inD(𝒪_P): a map of honest complexes that the localisation functor to the derived category inverts.The other three steps of 0FV4's proof are not covered; see the
Scopesection of this file.
theorem quasiIso_naiveCotangentToDifferentialsSingle
(hg : Stacks.Smooth.FormallySmoothScheme g) :
QuasiIso (naiveCotangentToDifferentialsSingle g)
Stacks.NaiveCotangentFormallySmoothComparison.isIso_Q_map_naiveCotangentToDifferentialsSingle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentFormallySmoothComparison.lean, line 285. The attribute's comment: “the 0D0L input: NL_{P/Y} -> Omega_{P/Y}[0] is invertible in D(O_P)”.
The 0D0L input of [Stacks Project, Tag 0FV4], read in
D(𝒪_P). For a formally smooth morphism of schemesg : P ⟶ Ythe canonical chain mapNL_{P/Y} ⟶ Ω_{P/Y}[0]becomes an isomorphism in the derived category of sheaves of𝒪_P-modules; that is,NL_{P/Y}andΩ_{P/Y}[0]are canonically isomorphic objects ofD(𝒪_P).This is the form
NL_{P/Y} = Ω_{P/Y}in which the proof of 0FV4 uses the step. Its content is that ofquasiIso_naiveCotangentToDifferentialsSingle, the localisation functor to the derived category inverting exactly the quasi-isomorphisms; what is added is that the two complexes are compared as objects ofD(𝒪_P)rather than by their cohomology sheaves. The derived category is the one ofHasDerivedCategory.standard, taken as a local instance.Only this one step of 0FV4 is covered; see the
Scopesection of this file.
theorem isIso_Q_map_naiveCotangentToDifferentialsSingle
(hg : Stacks.Smooth.FormallySmoothScheme g) :
IsIso (DerivedCategory.Q.map (naiveCotangentToDifferentialsSingle g))
Stacks.NaiveCotangentImmersionFormallySmooth.naiveCotangentIsoConormalDifferentialComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentImmersionFormallySmooth.lean, line 129. The attribute's comment: “the canonical isomorphism NL_{X/Y} = (C_{X/P} -> i^*Omega_{P/Y}) in D(O_X), with C_{X/P} in degree -1, for f = g . i with i an immersion and g formally smooth”. References: SGA 6 VIII (2.2), “more general”.
[Stacks Project, Tag 0FV4]. Let
f : X ⟶ Ybe a morphism of schemes which factors asf = g ∘ iwithi : X ⟶ Pan immersion andg : P ⟶ Yformally smooth (for example smooth, by [Stacks Project, Tag 02H6]). Then there is a canonical isomorphism
NL_{X/Y} ≅ (𝒞_{X/P} ⟶ i^*Ω_{P/Y})in
D(𝒪_X), where the conormal sheaf𝒞_{X/P}is placed in degree-1.The right-hand side is
Stacks.ConormalSequenceRight.conormalDifferentialComplex i g: the two-term complex whose degree-1term is the conormal sheaf of [Stacks Project, Tag 01R2], whose degree0term isi^*Ω_{P/Y}, and whose only differential is the first arrow of the conormal sequence of [Stacks Project, Tag 01UZ].See the
Routesection of this file; the proof does not go through the distinguished triangle of [Stacks Project, Tag 0FV3] and so has no sign to track.
def naiveCotangentIsoConormalDifferentialComplex (f : X ⟶ Y) (hf : f = i ≫ g)
(hg : Stacks.Smooth.FormallySmoothScheme g) :
DerivedCategory.Q.obj (Scheme.naiveCotangentComplex f : CochainComplex X.Modules ℤ) ≅
DerivedCategory.Q.obj (Stacks.ConormalSequenceRight.conormalDifferentialComplex i g)
Stacks.NaiveCotangentPullbackFormallySmooth.isZero_homology_negOne_modulePullbackNaiveCotangentComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentPullbackFormallySmooth.lean, line 339. The attribute's comment: “the pullback step: H^{-1}(i^*NL_{P/Y}) = 0, the detail the source omits”.
The pullback step of [Stacks Project, Tag 0FV4]: the vanishing
H^{-1}(i^*NL_{P/Y}) = 0. For a formally smooth morphism of schemesg : P ⟶ Yand an arbitrary morphismi : X ⟶ Pthe degree-1cohomology sheaf of the termwise pullback alongiofNL_{P/Y}vanishes.This is the step the source records as a small detail omitted, and obtains from local projectivity of
Ω_{P/Y}— the locally projective clause of [Stacks Project, Tag 0D0L] — through [Stacks Project, Tag 0FUY]. The pullback of sheaves of modules is only right exact, so this does not follow from the vanishingH^{-1}(NL_{P/Y}) = 0before pullback; what makes it true is that local projectivity splits the one differential ofNL_{P/Y}at every stalk, and a split monomorphism stays one under any functor. See theRoutesection of this file.Only this step of 0FV4 is covered; see the
Scopesection of this file.
theorem isZero_homology_negOne_modulePullbackNaiveCotangentComplex
(hg : Stacks.Smooth.FormallySmoothScheme g) :
IsZero ((modulePullbackNaiveCotangentComplex i g).homology (-1))
Stacks.NaiveCotangentPullbackFormallySmooth.quasiIso_pullbackNaiveCotangentToDifferentialsSingle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentPullbackFormallySmooth.lean, line 385. The attribute's comment: “the pullback step: i^NL_{P/Y} -> i^Omega_{P/Y}[0] is a quasi-isomorphism”.
The pullback step of [Stacks Project, Tag 0FV4]. For a formally smooth morphism of schemes
g : P ⟶ Yand an arbitrary morphismi : X ⟶ Pthe canonical chain mapi^*NL_{P/Y} ⟶ i^*Ω_{P/Y}[0]is a quasi-isomorphism: the pullback alongiof the naive cotangent complex ofgis identified with the pullback of its sheaf of relative differentials, placed in degree0.This is the form
NL_{P/Y} = Ω_{P/Y}in which the proof of 0FV4 uses the tag after pulling back alongi, and it is the step that does not follow fromStacks.NaiveCotangentFormallySmoothComparison.quasiIso_naiveCotangentToDifferentialsSingle, the same statement before pullback, the pullback of sheaves of modules not being exact. Its three ingredients are the vanishingisZero_homology_negOne_modulePullbackNaiveCotangentComplexproved above, and the two clauses of [Stacks Project, Tag 0E44] available inStacksFrontier.AlgebraicGeometry.MoreMorphisms.NaiveCotangentSixTermSequence: the identificationH^0(i^*NL_{P/Y}) = i^*Ω_{P/Y}and the vanishing of the cohomology sheaves outside degrees-1and0.Only this step of 0FV4 is covered; see the
Scopesection of this file.
theorem quasiIso_pullbackNaiveCotangentToDifferentialsSingle
(hg : Stacks.Smooth.FormallySmoothScheme g) :
QuasiIso (pullbackNaiveCotangentToDifferentialsSingle i g)
Stacks.NaiveCotangentPullbackFormallySmooth.isIso_Q_map_pullbackNaiveCotangentToDifferentialsSingle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentPullbackFormallySmooth.lean, line 415. The attribute's comment: “the pullback step in D(O_X): i^NL_{P/Y} = i^Omega_{P/Y}[0]”.
The pullback step of [Stacks Project, Tag 0FV4], read in
D(𝒪_X). For a formally smooth morphism of schemesg : P ⟶ Yand an arbitrary morphismi : X ⟶ Pthe canonical chain mapi^*NL_{P/Y} ⟶ i^*Ω_{P/Y}[0]becomes an isomorphism in the derived category of sheaves of𝒪_X-modules; that is,i^*NL_{P/Y}andi^*Ω_{P/Y}[0]are canonically isomorphic objects ofD(𝒪_X).This is the form in which the proof of 0FV4 uses the step: the first vertex of its distinguished triangle is
i^*NL_{P/Y}, and what the proof needs of it is that it isi^*Ω_{P/Y}in degree0. Its content is that ofquasiIso_pullbackNaiveCotangentToDifferentialsSingle, the localisation functor to the derived category inverting exactly the quasi-isomorphisms. The derived category is the one ofHasDerivedCategory.standard, taken as a local instance.Only this step of 0FV4 is covered; see the
Scopesection of this file.
theorem isIso_Q_map_pullbackNaiveCotangentToDifferentialsSingle
(hg : Stacks.Smooth.FormallySmoothScheme g) :
IsIso (DerivedCategory.Q.map (pullbackNaiveCotangentToDifferentialsSingle i g))
Tag 0FV5, a lemma
Tag 0FV5 in the Stacks Project.
Stacks.NaiveCotangentBaseChange.isIso_homologyMap_zero_baseChangeMapOfComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentBaseChangeHomologyCartesian.lean, line 476. The attribute's comment: “the degree-zero ISOMORPHISM, for a CARTESIAN square (hsq : IsPullback g' f' f g) and NO other hypothesis -- in particular no flatness. The canonical map is CONSTRUCTED, not assumed: Stacks.NaiveCotangentFlatBaseChange.baseChangeMapOfComparison is the source's own composite of the [Stacks, Tag 08TM] identification of (g')^*NL_{X/Y} with a base change (Stacks.SheafOfModules.pulledNaiveCotangentComparison), the base-change map NL_{B/A} (x)_B C -> NL_{C/A} of [Stacks, Tag 0E1Y] (Stacks.SheafOfModules.spaceBaseChangeNaiveCotangentMap) for the tower (g')^-1 f^-1 O_Y -> (g')^-1 O_X -> O_{X'}, and the relative map NL_{C/A} -> NL_{C/B} (Stacks.SheafOfModules.spaceRelativeNaiveCotangentComplexMap) for the tower through (f')^-1 O_{Y'}. The base-ring comparison it is taken against is the CANONICAL one of the square, AlgebraicGeometry.BaseChangeStalk.baseRingComparison, with its compatibility AlgebraicGeometry.BaseChangeStalk.baseRingComparison_comp; it is built from the square and is not a Classical.choose of a non-unique existence statement. It is the same map the flat statements [Stacks, Tag 0FJZ] and [Stacks, Tag 0FK0] are about. PROVED: the reduction to the stalks ([Stacks, Tag 08TL], through AlgebraicGeometry.SheafOfModules.isIso_homologyMap_iff_forall_stalk); the degreewise vanishing outside degrees -1 and 0; and the stalkwise statement isBijectiveOnCokernel_stalkFunctor_map_baseChangeMapOfComparison, which is Stacks.NaiveCotangentTowerStalk.isBijectiveOnCokernel_stalkFunctor_map_towerComposite read through the stalk identification of the naive cotangent complex ([Stacks, Tag 0D09], the stalk-level form of [Stacks, Tag 0D0I]) and fed with the ring-level ARBITRARY base change [Stacks, Tag 0FUZ] NaiveCotangent.naiveCotangentComplex_baseChange_homology, composed with localization of the target [Stacks, Tag 00S7] in NaiveCotangent.isH₀IsoH₁Surj_nlExtensionBaseChangeMap_of_isLocalization_tensor. The one geometric input is the identification of O_{X',x'} as a localization of O_{Y',f'(x')} (x)_{O_{Y,y}} O_{X,g'(x')}, AlgebraicGeometry.BaseChangeStalk.stalk_isLocalization_of_isPullback_inverseImage_comm ([Stacks, Tag 01JR]), and that is the one place cartesianness is used. The companion clause, the H^{-1} surjection, is Stacks.NaiveCotangentBaseChange.epi_homologyMap_negOne_baseChangeMapOfComparison”.
Stacks 0FV5, the degree-zero isomorphism. For a cartesian square of schemes the canonical map
(g')^*NL_{X/Y} ⟶ NL_{X'/Y'}induces an isomorphism on degree-zero cohomology.No flatness is assumed anywhere, and the canonical map is constructed and not assumed: it is
Stacks.NaiveCotangentFlatBaseChange.baseChangeMapOfComparisontaken against the canonical base-ring comparisonAlgebraicGeometry.BaseChangeStalk.baseRingComparisonof the square.
theorem isIso_homologyMap_zero_baseChangeMapOfComparison (f : X ⟶ Y) (g : Y' ⟶ Y) (f' : X' ⟶ Y')
(g' : X' ⟶ X) (hsq : IsPullback g' f' f g) :
IsIso (HomologicalComplex.homologyMap
(baseChangeMapOfComparison f f' g' (baseRingComparison f f' g' g hsq.w)
(baseRingComparison_comp f f' g' g hsq.w)) 0)
Stacks.NaiveCotangentBaseChange.epi_homologyMap_negOne_baseChangeMapOfComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentBaseChangeHomologyCartesian.lean, line 514. The attribute's comment: “the degree-minus-one SURJECTION, for a CARTESIAN square (hsq : IsPullback g' f' f g) and NO other hypothesis -- in particular no flatness. The canonical map is the one described on Stacks.NaiveCotangentBaseChange.isIso_homologyMap_zero_baseChangeMapOfComparison, the same constructed map Stacks.NaiveCotangentFlatBaseChange.baseChangeMapOfComparison taken against the canonical base-ring comparison of the square. PROVED: the reduction of EPIMORPHY to the stalks (AlgebraicGeometry.SheafOfModules.epi_homologyMap_iff_forall_stalk, the epimorphy counterpart of [Stacks, Tag 08TL]); the degreewise vanishing outside degrees -1 and 0; and the stalkwise statement isSurjectiveOnKernel_stalkFunctor_map_baseChangeMapOfComparison, which is Stacks.NaiveCotangentTowerStalk.isSurjectiveOnKernel_stalkFunctor_map_towerComposite fed with the ring-level ARBITRARY base change [Stacks, Tag 0FUZ]. Only SURJECTIVITY on the degree -1 cycles is assumed and only a surjection is concluded, which is what the source asserts and all that [Stacks, Tag 0FUZ] supplies: injectivity there is the half flatness would buy, and is the content of the stronger [Stacks, Tag 0FJZ] / [Stacks, Tag 0FK0]. The companion clause, the H^0 isomorphism, is Stacks.NaiveCotangentBaseChange.isIso_homologyMap_zero_baseChangeMapOfComparison”.
Stacks 0FV5, the degree-minus-one surjection. For a cartesian square of schemes the canonical map
(g')^*NL_{X/Y} ⟶ NL_{X'/Y'}induces a surjection on degree-minus-one cohomology.No flatness is assumed anywhere, and nothing is claimed about injectivity in degree
-1: the source'sH^{-1}assertion is a surjection and not an isomorphism, and that is exactly what the ring-level statement provides.
theorem epi_homologyMap_negOne_baseChangeMapOfComparison (f : X ⟶ Y) (g : Y' ⟶ Y) (f' : X' ⟶ Y')
(g' : X' ⟶ X) (hsq : IsPullback g' f' f g) :
Epi (HomologicalComplex.homologyMap
(baseChangeMapOfComparison f f' g' (baseRingComparison f f' g' g hsq.w)
(baseRingComparison_comp f f' g' g hsq.w)) (-1))
AlgebraicGeometry.Scheme.isIso_baseChangeNaiveCotangentHomologyZeroMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/NaiveCotangentBaseChangeHomology.lean, line 677. The attribute's comment: “the degree-zero ISOMORPHISM, for a CARTESIAN square, with no hypothesis beyond the cartesianness the source itself assumes. The map is AlgebraicGeometry.Scheme.baseChangeNaiveCotangentHomologyZeroMap, the canonical map (g')^*Omega_{X/Y} -> Omega_{X'/Y'} of [Stacks, Tag 01UV] (AlgebraicGeometry.Scheme.Hom.relativeDifferentialsMap, characterized there by compatibility with the universal derivations) read through the degree-zero identification H^0(NL) = Omega of [Stacks, Tag 0D0J] (AlgebraicGeometry.Scheme.naiveCotangentComplexHomologyZeroIso) at both ends. Like the source's own map it is defined from COMMUTATIVITY alone, and cartesianness is used only for invertibility, through [Stacks, Tag 01V0] (AlgebraicGeometry.Scheme.Hom.isIso_relativeDifferentialsMap_of_isPullback, which is itself proved outright from the cartesian-stalk localization and KaehlerDifferential.tensorKaehlerEquivOfFormallyEtalePushout). This is a SECOND, independent route to the tag's H^0 clause, through the sheaf of relative differentials. The tag's two clauses for the canonical map of COMPLEXES are proved outright at Stacks.NaiveCotangentBaseChange.isIso_homologyMap_zero_baseChangeMapOfComparison and Stacks.NaiveCotangentBaseChange.epi_homologyMap_negOne_baseChangeMapOfComparison, which take the same canonical base-ring comparison of the square that [Stacks, Tag 0FJZ] does. NOT covered here: that the map of this statement is the one induced on H^0 by that map of complexes. Comparing the two needs the identification of Mathlib's AlgebraicGeometry.Scheme.Modules.pullback -- the functor Omega and its canonical maps are stated over -- with the inverse-image-then-extend-scalars model that map of complexes is stated over, which is the open input recorded at StacksFrontier/AlgebraicGeometry/EtaleAlgebra/FlatBaseChange/StructureSheaf.lean”.
Stacks Project, Tag 0FV5, the degree-zero isomorphism. For a cartesian square of schemes the canonical map
(g')^*H^0(NL_{X/Y}) ⟶ H^0(NL_{X'/Y'})is an isomorphism.The map is
AlgebraicGeometry.Scheme.baseChangeNaiveCotangentHomologyZeroMap, defined for every commutative square; cartesianness is used only here, through Stacks 01V0. See the tag clause for what this statement does and does not cover.
theorem isIso_baseChangeNaiveCotangentHomologyZeroMap (f : X ⟶ Y) (g : Y' ⟶ Y) (f' : X' ⟶ Y')
(g' : X' ⟶ X) (hcart : IsPullback g' f' f g) :
IsIso (baseChangeNaiveCotangentHomologyZeroMap f g f' g' hcart.w)
Tag 0FJZ, a lemma
Tag 0FJZ in the Stacks Project.
Stacks.NaiveCotangentFlatBaseChange.quasiIso_baseChangeMapOfComparison_of_flat_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentFlatBaseChange.lean, line 239. The attribute's comment: “the flat-base-change quasi-isomorphism, with no hypotheses beyond a CARTESIAN square (hsq : IsPullback g' f' f g) and [Flat g]. The canonical map is CONSTRUCTED, not assumed: Stacks.NaiveCotangentFlatBaseChange.baseChangeMapOfComparison is the source's own composite of the [Stacks, Tag 08TM] identification of (g')^*NL_{X/Y} with a base change (Stacks.SheafOfModules.pulledNaiveCotangentComparison), the base-change map NL_{B/A} (x)_B C -> NL_{C/A} of [Stacks, Tag 0E1Y] (Stacks.SheafOfModules.spaceBaseChangeNaiveCotangentMap) for the tower (g')^-1 f^-1 O_Y -> (g')^-1 O_X -> O_{X'}, and the relative map NL_{C/A} -> NL_{C/B} (Stacks.SheafOfModules.spaceRelativeNaiveCotangentComplexMap) for the tower through (f')^-1 O_{Y'}. The base-ring comparison it is taken against is the CANONICAL one of the square, AlgebraicGeometry.BaseChangeStalk.baseRingComparison, together with its compatibility AlgebraicGeometry.BaseChangeStalk.baseRingComparison_comp; it is built from the square and is not a Classical.choose of a non-unique existence statement. PROVED: the construction of the map; the degreewise vanishing outside degrees -1 and 0 (isZero_pulledComplex_X); the reduction of quasi-isomorphy to the stalks (quasiIso_baseChangeMapOfComparison_of_forall_stalk, resting on [Stacks, Tag 08TL] AlgebraicGeometry.SheafOfModules.quasiIso_of_forall_stalk_quasiIso); and the stalkwise statement itself, Stacks.NaiveCotangentFlatBaseChangeStalk.quasiIso_stalkFunctor_map_baseChangeMapOfComparison. That stalkwise statement is Stacks.NaiveCotangentTowerStalk.quasiIso_stalkFunctor_map_towerComposite fed with the ring-level flat base change NaiveCotangent.isQuasiIso_nlExtensionBaseChangeMap_of_flat_base ([Stacks, Tag 00S4]), read through the stalk identification of the naive cotangent complex ([Stacks, Tag 0D09], Stacks.SheafOfModules.stalkLegNegOne / stalkLegZero / stalkLeg_d). Its two ring-level inputs are both discharged here: the flatness of the stalk of the canonical base-ring comparison, which AlgebraicGeometry.BaseChangeStalk.stalkFunctor_map_baseRingComparison identifies with the stalk map of g conjugated by three isomorphisms and which Mathlib's AlgebraicGeometry.Flat.stalkMap then makes flat, so [Flat g] does work here and is not decorative; and the identification of O_{X',x'} as a localization of O_{Y',y'} (x)_{O_{Y,y}} O_{X,x}, which is AlgebraicGeometry.BaseChangeStalk.stalk_isLocalization_of_isPullback_inverseImage_comm ([Stacks, Tag 01JR]) and is the one place cartesianness of the square is used. SCOPE: the statement is about the undecorated comparison (g')^*NL_{X/Y} -> NL_{X'/Y'}; nothing is claimed here about the derived pullback L(g')^*NL_{X/Y}”.
Flat base change. For a cartesian square of schemes whose lower horizontal morphism
g : Y' ⟶ Yis flat, the canonical comparison(g')^*NL_{X/Y} ⟶ NL_{X'/Y'}, taken against the canonical base-ring comparisonAlgebraicGeometry.BaseChangeStalk.baseRingComparisonof the square, is a quasi-isomorphism.
theorem quasiIso_baseChangeMapOfComparison_of_flat_base (f : X ⟶ Y) (g : Y' ⟶ Y) (f' : X' ⟶ Y')
(g' : X' ⟶ X) (hsq : IsPullback g' f' f g) [AlgebraicGeometry.Flat g] :
QuasiIso (baseChangeMapOfComparison f f' g'
(AlgebraicGeometry.BaseChangeStalk.baseRingComparison f f' g' g hsq.w)
(AlgebraicGeometry.BaseChangeStalk.baseRingComparison_comp f f' g' g hsq.w))
Tag 0FK0, a lemma
Tag 0FK0 in the Stacks Project.
Stacks.NaiveCotangentDerivedFlatBaseChange.isIso_derivedBaseChangeMapOfComparison_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentDerivedFlatBaseChange.lean, line 206. The attribute's comment: “the SECOND clause -- the DERIVED comparison L(g')^* NL_{X/Y} -> NL_{X'/Y'} is a quasi-isomorphism when NL_{X/Y} has tor-amplitude in [-1,0] -- with no hypotheses beyond a CARTESIAN square (hsq : IsPullback g' f' f g), [Flat f] and that tor-amplitude. The first clause is Stacks.NaiveCotangentFlatBaseChange.quasiIso_baseChangeMapOfComparison_of_flat_algebra. The DERIVED PULLBACK is not assumed: it is Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback, the total left derived functor of termwise pullback of [Stacks, Tag 06YJ], which exists for every morphism of ringed spaces, and the comparison L(g')^* K -> (g')^* K at a complex is Stacks.DerivedPullback.Composition.derivedPullbackComparisonOnComplex. TOR AMPLITUDE is the ringed-space notion of [Stacks, Tag 08CG], Stacks.Cohomology.TorAmplitude.HasTorAmplitude, tested against EVERY O_X-module. The map is CONSTRUCTED, not assumed: derivedBaseChangeMapOfComparison is the Tag 06YJ comparison, then the identification pulledComplexIso of Mathlib's termwise pullback with the inverse-image-then-extend-scalars model, then the first clause's map of complexes Stacks.NaiveCotangentFlatBaseChange.baseChangeMapOfComparison, taken against the CANONICAL base-ring comparison AlgebraicGeometry.BaseChangeStalk.baseRingComparison of the square. PROVED HERE: that NL_{X/Y} is K-flat under the tor-amplitude hypothesis (kFlat_naiveCotangentComplex_of_hasTorAmplitude), which is the whole content of the clause beyond the first -- its degree 0 term is flat because each stalk is the free cotangent space of the canonical presentation of the stalk map (Stacks.SheafOfModules.isFlat_naiveCotangentComplex_X_zero, [Stacks, Tag 05NE] plus Algebra.Generators.cotangentSpaceBasis), so its degree -1 term is flat by the ringed-space form of [Stacks, Tag 0653] (Stacks.Cohomology.TorAmplitude.DoubleFlat.isFlat_X_negOne_of_hasTorAmplitude, the stupid filtration of a two-term complex fed to [Stacks, Tag 08CJ] (1)), and a bounded-above complex of flat modules is K-flat by [Stacks, Tag 06YQ]; and that a K-flat complex inverts the Tag 06YJ comparison (isIso_derivedPullbackComparisonOnComplex_of_kFlat). The two models of (g')^* are identified by RingedSpaceModuleAdjunction.modulePullbackIsoTwoStep, proved here from uniqueness of left adjoints, which closes the input that StacksFrontier/AlgebraicGeometry/EtaleAlgebra/FlatBaseChange/StructureSheaf.lean had recorded as open. SCOPE: the undecorated first clause is on Stacks.NaiveCotangentFlatBaseChange.quasiIso_baseChangeMapOfComparison_of_flat_algebra; the two declarations together are the whole tag”.
Stacks 0FK0, the derived clause. For a cartesian square of schemes whose right vertical morphism
f : X ⟶ Yis flat and whose naive cotangent complexNL_{X/Y}has Tor amplitude in[-1, 0], the canonical derived comparisonL(g')^*NL_{X/Y} ⟶ NL_{X'/Y'}is an isomorphism inD(𝒪_{X'}).The Tor amplitude makes
NL_{X/Y}K-flat, so the comparisonL(g')^*NL_{X/Y} ⟶ (g')^*NL_{X/Y}is invertible by Stacks 06YJ; the remaining factor is the base change map of complexes, which is a quasi-isomorphism by the first clause.
theorem isIso_derivedBaseChangeMapOfComparison_of_flat (f : X ⟶ Y) (g : Y' ⟶ Y) (f' : X' ⟶ Y')
(g' : X' ⟶ X) (hsq : IsPullback g' f' f g) [AlgebraicGeometry.Flat f]
(htor : Stacks.Cohomology.TorAmplitude.HasTorAmplitude X.toRingedSpace
(DerivedCategory.Q.obj (Scheme.naiveCotangentComplex f)) (-1) 0) :
IsIso (derivedBaseChangeMapOfComparison f f' g'
(AlgebraicGeometry.BaseChangeStalk.baseRingComparison f f' g' g hsq.w)
(AlgebraicGeometry.BaseChangeStalk.baseRingComparison_comp f f' g' g hsq.w))
Stacks.NaiveCotangentFlatBaseChange.quasiIso_baseChangeMapOfComparison_of_flat_algebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NaiveCotangentFlatBaseChange.lean, line 296. The attribute's comment: “the FIRST clause -- the quasi-isomorphism when X -> Y is flat -- with no hypotheses beyond a CARTESIAN square (hsq : IsPullback g' f' f g) and [Flat f]. The canonical map is CONSTRUCTED, not assumed, exactly as on Stacks.NaiveCotangentFlatBaseChange.quasiIso_baseChangeMapOfComparison_of_flat_base: Stacks.NaiveCotangentFlatBaseChange.baseChangeMapOfComparison is the source's own composite of the [Stacks, Tag 08TM] identification of (g')^*NL_{X/Y} with a base change (Stacks.SheafOfModules.pulledNaiveCotangentComparison), the base-change map NL_{B/A} (x)_B C -> NL_{C/A} of [Stacks, Tag 0E1Y] (Stacks.SheafOfModules.spaceBaseChangeNaiveCotangentMap) for the tower (g')^-1 f^-1 O_Y -> (g')^-1 O_X -> O_{X'}, and the relative map NL_{C/A} -> NL_{C/B} (Stacks.SheafOfModules.spaceRelativeNaiveCotangentComplexMap) for the tower through (f')^-1 O_{Y'}. The base-ring comparison it is taken against is the CANONICAL one of the square, AlgebraicGeometry.BaseChangeStalk.baseRingComparison, together with its compatibility AlgebraicGeometry.BaseChangeStalk.baseRingComparison_comp; it is built from the square and is not a Classical.choose of a non-unique existence statement. PROVED: the construction of the map; the degreewise vanishing outside degrees -1 and 0 (isZero_pulledComplex_X); the reduction of quasi-isomorphy to the stalks (quasiIso_baseChangeMapOfComparison_of_forall_stalk, resting on [Stacks, Tag 08TL] AlgebraicGeometry.SheafOfModules.quasiIso_of_forall_stalk_quasiIso); and the stalkwise statement itself, Stacks.NaiveCotangentFlatAlgebraBaseChangeStalk .quasiIso_stalkFunctor_map_baseChangeMapOfComparison. That stalkwise statement is Stacks.NaiveCotangentTowerStalk.quasiIso_stalkFunctor_map_towerComposite fed with the ring-level base change for a flat algebra NaiveCotangent.isQuasiIso_nlExtensionBaseChangeMap_of_flat_algebra, read through the stalk identification of the naive cotangent complex ([Stacks, Tag 0D09] / [Stacks, Tag 0098]). That ring-level statement is proved here from the two elementwise inputs of [Stacks, Tag 0FJU]: surjectivity on the degree -1 cycles and bijectivity on the cokernels, which hold for an arbitrary base change by [Stacks, Tag 0FUZ] (NaiveCotangent.naiveCotangentComplex_baseChange_homology), and injectivity on those cycles, which is what flatness of the algebra buys (NaiveCotangent.cotangent_intrinsic_baseChange_cycle_injective_of_flat); then flat base change to the pushout is composed with localization of the target over a fixed base ([Stacks, Tag 00S7]). Its two geometric inputs are both discharged here: the flatness of the stalk of the first map of the tower, which AlgebraicGeometry.BaseChangeStalk.stalkInverseImageBaseRingIso_hom_comp_stalkMap identifies with the stalk map of f conjugated by two isomorphisms and which Mathlib's AlgebraicGeometry.Flat.stalkMap then makes flat, so [Flat f] does work here and is not decorative; and the identification of O_{X',x'} as a localization of O_{Y',y'} (x)_{O_{Y,y}} O_{X,x}, which is AlgebraicGeometry.BaseChangeStalk.stalk_isLocalization_of_isPullback_inverseImage_comm ([Stacks, Tag 01JR]) and is the one place cartesianness of the square is used. SCOPE: the statement is about the undecorated comparison (g')^*NL_{X/Y} -> NL_{X'/Y'}, which is the tag's first clause; nothing is claimed here about the tag's second clause, the DERIVED comparison L(g')^*NL_{X/Y} -> NL_{X'/Y'} under Tor amplitude in [-1,0]”.
Base change along a flat morphism. For a cartesian square of schemes whose right vertical morphism
f : X ⟶ Yis flat, the canonical comparison(g')^*NL_{X/Y} ⟶ NL_{X'/Y'}, taken against the canonical base-ring comparisonAlgebraicGeometry.BaseChangeStalk.baseRingComparisonof the square, is a quasi-isomorphism.
theorem quasiIso_baseChangeMapOfComparison_of_flat_algebra (f : X ⟶ Y) (g : Y' ⟶ Y)
(f' : X' ⟶ Y') (g' : X' ⟶ X) (hsq : IsPullback g' f' f g) [AlgebraicGeometry.Flat f] :
QuasiIso (baseChangeMapOfComparison f f' g'
(AlgebraicGeometry.BaseChangeStalk.baseRingComparison f f' g' g hsq.w)
(AlgebraicGeometry.BaseChangeStalk.baseRingComparison_comp f f' g' g hsq.w))
Sources
Section37.14 Pushouts in the category of schemes, I#
Section 37.14 of the Stacks Project, Tag 07RS. 6 tags here are carried by 30 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0ET0, a lemma
Tag 0ET0 in the Stacks Project.
Stacks.Pushout.isPushout_spec_map_of_isPullback_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Pushout/SchemePushout.lean, line 88.
Stacks Project, Tag 0ET0. A fibre product of rings over a surjective map is sent by
Specto a pushout of schemes: ifp : A' ⟶ Ais surjective and the square with sidesp',q',q,pis cartesian inCommRingCat, then its image underSpecis a pushout square of schemes.
theorem isPushout_spec_map_of_isPullback_of_surjective
{A A' B B' : CommRingCat.{u}} (p : A' ⟶ A) (q : B ⟶ A)
(p' : B' ⟶ B) (q' : B' ⟶ A') (h : IsPullback p' q' q p)
(hp : Function.Surjective p) :
IsPushout (Spec.map p) (Spec.map q) (Spec.map q') (Spec.map p')
Tag 0BMP, a lemma
Tag 0BMP in the Stacks Project.
AlgebraicGeometry.isColimit_of_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/FpqcLocalColimit.lean, line 195.
Stacks Project, Tag 0BMP. The colimit property for a cocone of schemes can be checked on an fpqc covering of its vertex and on all pairwise overlaps.
public theorem isColimit_of_fpqc {J : Type v} [Category.{w} J]
{F : J ⥤ Scheme.{u}} (c : Cocone F) {I : Type*}
(W' : I → Scheme.{u}) (f : ∀ i, W' i ⟶ c.pt)
(hfpqc : Presieve.ofArrows W' f ∈ Scheme.fpqcPrecoverage c.pt)
(hlocal : ∀ i, Nonempty (IsColimit (baseChangeCocone c (f i))))
(hoverlap : ∀ i j, Nonempty (IsColimit
(baseChangeCocone c (pullback.fst (f i) (f j) ≫ f i)))) :
Nonempty (IsColimit c)
Tag 07RT, a lemma
Tag 07RT in the Stacks Project.
Stacks.Pushout.exists_isPushout_isPullback_isThickening_of_isFiniteOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushoutFiniteOrder.lean, line 154. The attribute's comment: “the existence of the pushout, that Y ⊂ Y' is a thickening and that the square is cartesian; for a thickening of finite order”.
Stacks Project, Tag 07RT for a finite-order thickening, on an explicitly constructed apex. For a finite-order thickening
i : X ⟶ X'and an affine morphismf : X ⟶ Ythere is a schemeQwith mapsA : X' ⟶ QandB : Y ⟶ Qwhose square is cocartesian, is simultaneously cartesian, and hasBa thickening.
theorem exists_isPushout_isPullback_isThickening_of_isFiniteOrderThickening (i : X ⟶ X')
(f : X ⟶ Y) (hi : IsFiniteOrderThickening i) [IsAffineHom f] :
∃ (Q : Scheme.{u}) (A : X' ⟶ Q) (B : Y ⟶ Q),
IsPushout i f A B ∧ IsPullback i f A B ∧ IsThickening B
Stacks.Pushout.hasPushout_of_isFiniteOrderThickening_of_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushoutFiniteOrder.lean, line 168. The attribute's comment: “the existence of the pushout, for a thickening of finite order”.
Stacks Project, Tag 07RT, first assertion, for a finite-order thickening. A finite-order thickening and an affine morphism have a pushout in the category of schemes.
theorem hasPushout_of_isFiniteOrderThickening_of_isAffineHom (i : X ⟶ X') (f : X ⟶ Y)
(hi : IsFiniteOrderThickening i) [IsAffineHom f] : HasPushout i f
Stacks.Pushout.isPullback_pushout_of_isFiniteOrderThickening_of_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushoutFiniteOrder.lean, line 178. The attribute's comment: “that the square is cartesian, X = Y ×_{Y'} X'; for a thickening of finite order”.
Stacks Project, Tag 07RT, third assertion, for a finite-order thickening. The pushout square of a finite-order thickening and an affine morphism is also cartesian, that is,
X = Y ×_{Y'} X'; stated for Mathlib's canonical pushout.
theorem isPullback_pushout_of_isFiniteOrderThickening_of_isAffineHom (i : X ⟶ X') (f : X ⟶ Y)
(hi : IsFiniteOrderThickening i) [IsAffineHom f] [HasPushout i f] :
IsPullback i f (pushout.inl i f) (pushout.inr i f)
Stacks.Pushout.pushout_inr_isThickening_of_isFiniteOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushoutFiniteOrder.lean, line 191. The attribute's comment: “that Y ⊂ Y' is a thickening, for a thickening of finite order”.
Stacks Project, Tag 07RT, second assertion, for a finite-order thickening. The map from
Yinto the pushout of a finite-order thickeningi : X ⟶ X'and an affine morphismf : X ⟶ Yis again a thickening; stated for Mathlib's canonical pushout.
theorem pushout_inr_isThickening_of_isFiniteOrderThickening (i : X ⟶ X') (f : X ⟶ Y)
(hi : IsFiniteOrderThickening i) [IsAffineHom f] [HasPushout i f] :
IsThickening (pushout.inr i f)
Stacks.Pushout.pushout_structureSheaf_isPullback_of_isFiniteOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushoutFiniteOrder.lean, line 207. The attribute's comment: “the description of 𝒪_{Y'} as 𝒪_Y ×_{f_𝒪_X} f'_𝒪_{X'}; for a thickening of finite order”.
Stacks Project, Tag 07RT, fourth assertion, for a finite-order thickening. On every open
Uof the pushout of a finite-order thickeningi : X ⟶ X'and an affine morphismf : X ⟶ Ythe ring of sections is the fibre product of the rings of sections over the two preimages ofUinYandX'above the ring of sections over their common preimage inX; this is𝒪_{Y'} = 𝒪_Y ×_{f_*𝒪_X} f'_*𝒪_{X'}.
theorem pushout_structureSheaf_isPullback_of_isFiniteOrderThickening (i : X ⟶ X') (f : X ⟶ Y)
(hi : IsFiniteOrderThickening i) [IsAffineHom f] [HasPushout i f] (U : (pushout i f).Opens) :
IsPullback ((pushout.inr i f).app U) ((pushout.inl i f).app U)
(f.app (pushout.inr i f ⁻¹ᵁ U))
(i.app (pushout.inl i f ⁻¹ᵁ U) ≫ eqToHom (congrArg (fun V : X.Opens ↦ Γ(X, V))
(congrArg (fun g : X ⟶ pushout i f ↦ g ⁻¹ᵁ U)
(pushout.condition (f := i) (g := f)))))
Stacks.Pushout.exists_isPushout_isPullback_isThickening_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushoutUnconditional.lean, line 77. The attribute's comment: “the existence of the pushout, that Y ⊂ Y' is a thickening and that the square is cartesian, X = Y ×_{Y'} X'”.
Stacks Project, Tag 07RT for an arbitrary thickening, on an explicitly constructed apex. For a thickening
i : X ⟶ X'and an affine morphismf : X ⟶ Ythere is a schemeQwith mapsA : X' ⟶ QandB : Y ⟶ Qwhose square is cocartesian, is simultaneously cartesian, and hasBa thickening.
theorem exists_isPushout_isPullback_isThickening_of_isThickening (i : X ⟶ X') (f : X ⟶ Y)
(hi : IsThickening i) [IsAffineHom f] :
∃ (Q : Scheme.{u}) (A : X' ⟶ Q) (B : Y ⟶ Q),
IsPushout i f A B ∧ IsPullback i f A B ∧ IsThickening B
Stacks.Pushout.hasPushout_of_isThickening_of_isAffineHom', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushoutUnconditional.lean, line 91. The attribute's comment: “the existence of the pushout”.
Stacks Project, Tag 07RT, first assertion. A thickening and an affine morphism have a pushout in the category of schemes.
theorem hasPushout_of_isThickening_of_isAffineHom' (i : X ⟶ X') (f : X ⟶ Y)
(hi : IsThickening i) [IsAffineHom f] : HasPushout i f
Stacks.Pushout.pushout_inr_isThickening', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushoutUnconditional.lean, line 99. The attribute's comment: “that Y ⊂ Y' is a thickening”.
Stacks Project, Tag 07RT, second assertion. The map from
Yinto the pushout of a thickeningi : X ⟶ X'and an affine morphismf : X ⟶ Yis again a thickening; stated for Mathlib's canonical pushout.
theorem pushout_inr_isThickening' (i : X ⟶ X') (f : X ⟶ Y) (hi : IsThickening i) [IsAffineHom f]
[HasPushout i f] : IsThickening (pushout.inr i f)
Stacks.Pushout.isPullback_pushout_of_isThickening_of_isAffineHom', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushoutUnconditional.lean, line 107. The attribute's comment: “that the square is cartesian, X = Y ×_{Y'} X'”.
Stacks Project, Tag 07RT, third assertion. The pushout square of a thickening and an affine morphism is also cartesian, that is,
X = Y ×_{Y'} X'; stated for Mathlib's canonical pushout.
theorem isPullback_pushout_of_isThickening_of_isAffineHom' (i : X ⟶ X') (f : X ⟶ Y)
(hi : IsThickening i) [IsAffineHom f] [HasPushout i f] :
IsPullback i f (pushout.inl i f) (pushout.inr i f)
Stacks.Pushout.pushout_structureSheaf_isPullback', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushoutUnconditional.lean, line 117. The attribute's comment: “the description of 𝒪_{Y'} as 𝒪_Y ×_{f_𝒪_X} f'_𝒪_{X'}”.
Stacks Project, Tag 07RT, fourth assertion. On every open
Uof the pushout of a thickeningi : X ⟶ X'and an affine morphismf : X ⟶ Ythe ring of sections is the fibre product of the rings of sections over the two preimages ofUinYandX'above the ring of sections over their common preimage inX; this is𝒪_{Y'} = 𝒪_Y ×_{f_*𝒪_X} f'_*𝒪_{X'}.
theorem pushout_structureSheaf_isPullback' (i : X ⟶ X') (f : X ⟶ Y) (hi : IsThickening i)
[IsAffineHom f] [HasPushout i f] (U : (pushout i f).Opens) :
IsPullback ((pushout.inr i f).app U) ((pushout.inl i f).app U)
(f.app (pushout.inr i f ⁻¹ᵁ U))
(i.app (pushout.inl i f ⁻¹ᵁ U) ≫ eqToHom (congrArg (fun V : X.Opens ↦ Γ(X, V))
(congrArg (fun g : X ⟶ pushout i f ↦ g ⁻¹ᵁ U)
(pushout.condition (f := i) (g := f)))))
Tag 07RV, a lemma
Tag 07RV in the Stacks Project.
Stacks.Pushout.baseChangeFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushoutGluing.lean, line 165. The attribute's comment: “the base-change functor F”.
Base change from schemes over the pushout to compatible schemes over its two constituent pieces.
noncomputable def baseChangeFunctor {X X' Y : Scheme.{u}}
(i : X ⟶ X') (f : X ⟶ Y) (hi : IsThickening i) [IsAffineHom f] :
letI := hasPushout_of_isThickening i f hi
Over (pushout i f) ⥤ gluingData i f
Stacks.Pushout.gluingFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushoutGluing.lean, line 486. The attribute's comment: “the left adjoint G”.
Gluing compatible schemes over
YandX'to a scheme over their pushout. Its objectwise pushout property is stated below.
noncomputable def gluingFunctor {X X' Y : Scheme.{u}}
(i : X ⟶ X') (f : X ⟶ Y)
(hi : IsThickening i) [IsAffineHom f] :
letI := hasPushout_of_isThickening i f hi
gluingData i f ⥤ Over (pushout i f)
Stacks.Pushout.gluingFunctor_obj_isPushout, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushoutGluing.lean, line 562. The attribute's comment: “the left adjoint sends a triple to the pushout V ⨿_{V ×_Y X} U'”.
The glued scheme is the pushout of its two components along their identified restrictions to
X, with the induced map to the ambient pushout.
theorem gluingFunctor_obj_isPushout {X X' Y : Scheme.{u}}
(i : X ⟶ X') (f : X ⟶ Y)
(hi : IsThickening i) [IsAffineHom f]
(T : gluingData i f) :
letI := hasPushout_of_isThickening i f hi
∃ (v : T.obj.left.left ⟶ ((gluingFunctor i f hi).obj T).left)
(u' : T.obj.right.left ⟶ ((gluingFunctor i f hi).obj T).left),
IsPushout (gluingSourceMap i f T) (pullback.fst T.obj.right.hom i) v u' ∧
v ≫ ((gluingFunctor i f hi).obj T).hom =
T.obj.left.hom ≫ pushout.inr i f ∧
u' ≫ ((gluingFunctor i f hi).obj T).hom =
T.obj.right.hom ≫ pushout.inl i f
Stacks.Pushout.gluingAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushoutGluing.lean, line 1018. The attribute's comment: “the adjunction G ⊣ F”.
Stacks Project, Tag 07RV, the adjunction. Gluing is left adjoint to base change: a morphism from the glued scheme
V ⨿_U U'to a schemeZoverY'is the same thing as a morphism of compatible pairs from(V, U', φ)to the base change ofZ.The bijection is the universal property of the pushout on one side and of the two fibre products on the other.
noncomputable def gluingAdjunction {X X' Y : Scheme.{u}}
(i : X ⟶ X') (f : X ⟶ Y)
(hi : IsThickening i) [IsAffineHom f] :
letI := hasPushout_of_isThickening i f hi
gluingFunctor i f hi ⊣ baseChangeFunctor i f hi
Stacks.Pushout.gluingCompBaseChangeIsoId, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushoutGluing.lean, line 1528. The attribute's comment: “the composition F ∘ G is isomorphic to the identity functor”.
Stacks Project, Tag 07RV, the last assertion. The composition of gluing with base change is isomorphic to the identity functor: a compatible pair
(V, U', φ)is recovered from the glued schemeV ⨿_{V ×_Y X} U'by base change alongY ⟶ Y'andX' ⟶ Y'.The isomorphism is the unit of
Stacks.Pushout.gluingAdjunction, which is exactly the comparison map of the source.
noncomputable def gluingCompBaseChangeIsoId {X X' Y : Scheme.{u}}
(i : X ⟶ X') (f : X ⟶ Y)
(hi : IsThickening i) [IsAffineHom f] :
letI := hasPushout_of_isThickening i f hi
gluingFunctor i f hi ⋙ baseChangeFunctor i f hi ≅ 𝟭 (gluingData i f)
Tag 08KU, a lemma
Tag 08KU in the Stacks Project.
Stacks.Pushout.isEquivalence_flatBaseChangeTripleFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushout08KU.lean, line 916. The attribute's comment: “the equivalence of the first clause”.
Stacks Project, Tag 08KU, the equivalence of the first clause. For a thickening
i : X ⟶ X', an affine morphismf : X ⟶ Y, the pushoutY' = Y ⨿_X X'and anyg : V' ⟶ Y', the comparison functor of the tag — a quasi-coherent𝒪_{V'}-module flat overY'goes to its restrictions toV = Y ×_{Y'} V'and toU' = X' ×_{Y'} V'together with the canonical isomorphism of their restrictions toU = X ×_{Y'} V'— is an equivalence of categories onto the triples(𝒢, ℱ', φ)with𝒢quasi-coherent onVand flat overY,ℱ'quasi-coherent onU'and flat overX', andφan isomorphism of their restrictions toU.The pushout
Y' = Y ⨿_X X'is not assumed to exist: for a thickeningiand an affinefit does, by the first assertion of [Stacks Project, Tag 07RT],Stacks.Pushout.hasPushout_of_isThickening_of_isAffineHom, whose [Stacks Project, Tag 06AD] hypothesis is discharged byStacks.Thickenings.forall_isAffine_of_isThickening; that is the instance the statement binds for itself.
theorem isEquivalence_flatBaseChangeTripleFunctor (hi : IsThickening i) [IsAffineHom f] :
letI := hasPushout_of_isThickening_of_isAffineHom forall_isAffine_of_isThickening i f hi
∀ g : V' ⟶ pushout i f, (flatBaseChangeTripleFunctor i f g hi).IsEquivalence
Stacks.Pushout.baseChangeTripleFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushoutModules.lean, line 182. The attribute's comment: “the comparison functor of the tag, on all modules on V'”.
The comparison functor, sending a module on
V'to its two restrictions toVand toU'together with the canonical isomorphismStacks.Pushout.overlapComparisonbetween their restrictions toU.
noncomputable def baseChangeTripleFunctor (hi : IsThickening i) [IsAffineHom f] :
letI := hasPushout_of_isThickening_of_isAffineHom forall_isAffine_of_isThickening i f hi
∀ g : V' ⟶ pushout i f, V'.Modules ⥤ GluingTriple i f g
Stacks.Pushout.isFiniteType_baseChangeTripleFunctor_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushoutModules.lean, line 203. The attribute's comment: “the finite type clause, for an arbitrary module on V'”.
If a module on
V'is of finite type, then both components of its comparison triple, its restrictions toVand toU', are of finite type.
theorem isFiniteType_baseChangeTripleFunctor_obj (hi : IsThickening i) [IsAffineHom f] :
letI := hasPushout_of_isThickening_of_isAffineHom forall_isAffine_of_isThickening i f hi
∀ (g : V' ⟶ pushout i f) (M : V'.Modules) [M.IsFiniteType],
((baseChangeTripleFunctor i f hi g).obj M).target.IsFiniteType ∧
((baseChangeTripleFunctor i f hi g).obj M).ambient.IsFiniteType
Stacks.Pushout.isFinitePresentation_baseChangeTripleFunctor_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushoutModules.lean, line 220. The attribute's comment: “the finite presentation clause, for an arbitrary module on V'”.
If a module on
V'is of finite presentation, then both components of its comparison triple, its restrictions toVand toU', are of finite presentation.
theorem isFinitePresentation_baseChangeTripleFunctor_obj (hi : IsThickening i) [IsAffineHom f] :
letI := hasPushout_of_isThickening_of_isAffineHom forall_isAffine_of_isThickening i f hi
∀ (g : V' ⟶ pushout i f) (M : V'.Modules) [M.IsFinitePresentation],
((baseChangeTripleFunctor i f hi g).obj M).target.IsFinitePresentation ∧
((baseChangeTripleFunctor i f hi g).obj M).ambient.IsFinitePresentation
Stacks.Pushout.isFiniteType_iff_baseChangeTripleFunctor_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushoutModules.lean, line 583. The attribute's comment: “the finite type clause”.
A quasi-coherent module on
V'flat overY'is of finite type if and only if both components of its comparison triple, its restrictions toVand toU', are of finite type.
theorem isFiniteType_iff_baseChangeTripleFunctor_obj (hi : IsThickening i) [IsAffineHom f] :
letI := hasPushout_of_isThickening_of_isAffineHom forall_isAffine_of_isThickening i f hi
∀ (g : V' ⟶ pushout i f) (M : FlatQuasicoherentModule g),
M.obj.IsFiniteType ↔
((baseChangeTripleFunctor i f hi g).obj M.obj).target.IsFiniteType ∧
((baseChangeTripleFunctor i f hi g).obj M.obj).ambient.IsFiniteType
Stacks.Pushout.isFinitePresentation_iff_baseChangeTripleFunctor_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushoutModules.lean, line 1158. The attribute's comment: “the finite presentation clause”.
If
V' ⟶ Y'is locally of finite presentation, a quasi-coherent module onV'flat overY'is of finite presentation if and only if both components of its comparison triple, its restrictions toVand toU', are of finite presentation.
theorem isFinitePresentation_iff_baseChangeTripleFunctor_obj (hi : IsThickening i)
[IsAffineHom f] :
letI := hasPushout_of_isThickening_of_isAffineHom forall_isAffine_of_isThickening i f hi
∀ (g : V' ⟶ pushout i f), LocallyOfFinitePresentation g →
∀ M : FlatQuasicoherentModule g,
M.obj.IsFinitePresentation ↔
((baseChangeTripleFunctor i f hi g).obj M.obj).target.IsFinitePresentation ∧
((baseChangeTripleFunctor i f hi g).obj M.obj).ambient.IsFinitePresentation
Tag 07RX, a lemma
Tag 07RX in the Stacks Project.
Stacks.Pushout.gluingAdjunction_counit_app_isIso_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushout07RXFlat.lean, line 383. The attribute's comment: “the closing paragraph: the counit G(F(W')) ⟶ W' is an isomorphism for W' flat over Y', for the adjunction of Tag 07RV over Mathlib's canonical pushout”.
[Stacks, Tag 07RX], the closing paragraph, first assertion. If
W'is flat over the pushoutY' = Y ⨿_X X'of a thickeningi : X ⟶ X'and an affine morphismf : X ⟶ Y, then the adjunction mappingG(F(W')) ⟶ W'is an isomorphism:W'is glued from its two base changes toYand toX'.
theorem gluingAdjunction_counit_app_isIso_of_flat (i : X ⟶ X') (f : X ⟶ Y)
(hi : IsThickening i) [IsAffineHom f] :
letI := hasPushout_of_isThickening i f hi
∀ W' : Over (pushout i f), Flat W'.hom →
IsIso ((gluingAdjunction i f hi).counit.app W')
Stacks.Pushout.flatGluingEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushout07RXFlat.lean, line 494. The attribute's comment: “the closing paragraph: F and G are mutually quasi-inverse between the schemes flat over Y' and the triples with both components flat, for Tag 07RV over Mathlib's canonical pushout”.
[Stacks, Tag 07RX], the closing paragraph, second assertion. For the pushout
Y' = Y ⨿_X X'of a thickeningi : X ⟶ X'and an affine morphismf : X ⟶ Y, the functorsFandGof [Stacks Project, Tag 07RV] are mutually quasi-inverse between the category of schemes flat overY'and the category of triples(V, U', φ)withV ⟶ YandU' ⟶ X'flat.Both functors restrict to those subcategories, so the adjunction of Tag 07RV does; its unit is invertible by the last assertion of that tag and its counit by
Stacks.Pushout.gluingAdjunction_counit_app_isIso_of_flat.
noncomputable def flatGluingEquivalence (i : X ⟶ X') (f : X ⟶ Y) (hi : IsThickening i)
[IsAffineHom f] :
letI := hasPushout_of_isThickening i f hi
FlatGluingEquivalenceData i f hi
Stacks.Pushout.etale_gluingFunctor_obj_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushoutEtale.lean, line 160. The attribute's comment: “clause (5): étale, for the gluing functor of Tag 07RV over Mathlib's canonical pushout”.
Stacks 07RX, clause (5). The glued scheme of Tag 07RV over Mathlib's canonical pushout is étale over the pushout exactly when both of its pieces are étale over their bases.
theorem etale_gluingFunctor_obj_iff {X X' Y : Scheme.{u}} (i : X ⟶ X') (f : X ⟶ Y)
(hi : IsThickening i) [IsAffineHom f] (T : gluingData i f) :
letI := hasPushout_of_isThickening i f hi
Etale ((gluingFunctor i f hi).obj T).hom ↔
(Etale T.obj.left.hom ∧ Etale T.obj.right.hom)
Stacks.Pushout.locallyOfFiniteType_gluingFunctor_obj_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushoutGluingUnconditional.lean, line 78. The attribute's comment: “clause (1): locally of finite type, for the gluing functor of Tag 07RV over Mathlib's canonical pushout”.
[Stacks, Tag 07RX], clause (1). The scheme glued from a triple
(V, U', φ)across the pushoutY' = Y ⨿_X X'of a thickeningi : X ⟶ X'and an affine morphismf : X ⟶ Yis locally of finite type overY'if and only if bothV ⟶ YandU' ⟶ X'are.
theorem locallyOfFiniteType_gluingFunctor_obj_iff (i : X ⟶ X') (f : X ⟶ Y)
(hi : IsThickening i) [IsAffineHom f] (T : gluingData i f) :
letI := hasPushout_of_isThickening i f hi
LocallyOfFiniteType ((gluingFunctor i f hi).obj T).hom ↔
(LocallyOfFiniteType T.obj.left.hom ∧ LocallyOfFiniteType T.obj.right.hom)
Stacks.Pushout.flat_gluingFunctor_obj_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushoutGluingUnconditional.lean, line 92. The attribute's comment: “clause (2): flat, for the gluing functor of Tag 07RV over Mathlib's canonical pushout”.
[Stacks, Tag 07RX], clause (2). The scheme glued from a triple
(V, U', φ)across the pushoutY' = Y ⨿_X X'of a thickeningi : X ⟶ X'and an affine morphismf : X ⟶ Yis flat overY'if and only if bothV ⟶ YandU' ⟶ X'are flat.
theorem flat_gluingFunctor_obj_iff (i : X ⟶ X') (f : X ⟶ Y)
(hi : IsThickening i) [IsAffineHom f] (T : gluingData i f) :
letI := hasPushout_of_isThickening i f hi
Flat ((gluingFunctor i f hi).obj T).hom ↔
(Flat T.obj.left.hom ∧ Flat T.obj.right.hom)
Stacks.Pushout.flat_and_locallyOfFinitePresentation_gluingFunctor_obj_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushoutGluingUnconditional.lean, line 106. The attribute's comment: “clause (3): flat and locally of finite presentation, for the gluing functor of Tag 07RV over Mathlib's canonical pushout”.
[Stacks, Tag 07RX], clause (3). The scheme glued from a triple
(V, U', φ)across the pushoutY' = Y ⨿_X X'of a thickeningi : X ⟶ X'and an affine morphismf : X ⟶ Yis flat and locally of finite presentation overY'if and only if bothV ⟶ YandU' ⟶ X'are.
theorem flat_and_locallyOfFinitePresentation_gluingFunctor_obj_iff (i : X ⟶ X') (f : X ⟶ Y)
(hi : IsThickening i) [IsAffineHom f] (T : gluingData i f) :
letI := hasPushout_of_isThickening i f hi
(Flat ((gluingFunctor i f hi).obj T).hom ∧
LocallyOfFinitePresentation ((gluingFunctor i f hi).obj T).hom) ↔
((Flat T.obj.left.hom ∧ LocallyOfFinitePresentation T.obj.left.hom) ∧
(Flat T.obj.right.hom ∧ LocallyOfFinitePresentation T.obj.right.hom))
Stacks.Pushout.smooth_gluingFunctor_obj_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningPushoutGluingUnconditional.lean, line 123. The attribute's comment: “clause (4): smooth, for the gluing functor of Tag 07RV over Mathlib's canonical pushout”.
[Stacks, Tag 07RX], clause (4). The scheme glued from a triple
(V, U', φ)across the pushoutY' = Y ⨿_X X'of a thickeningi : X ⟶ X'and an affine morphismf : X ⟶ Yis smooth overY'if and only if bothV ⟶ YandU' ⟶ X'are smooth.
theorem smooth_gluingFunctor_obj_iff (i : X ⟶ X') (f : X ⟶ Y)
(hi : IsThickening i) [IsAffineHom f] (T : gluingData i f) :
letI := hasPushout_of_isThickening i f hi
Smooth ((gluingFunctor i f hi).obj T).hom ↔
(Smooth T.obj.left.hom ∧ Smooth T.obj.right.hom)
Sources
Section37.15 Openness of the flat locus#
Section 37.15 of the Stacks Project, Tag 0398. 2 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0399, a theorem
Tag 0399 in the Stacks Project.
AlgebraicGeometry.isOpen_setOf_flatOverAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/FlatLocus.lean, line 331. References: EGA IV (11.3.1), “U open”; EGA IV (15.4.1), “partial”.
Stacks Project, Tag 0399. The locus where a finitely presented quasi-coherent module is flat over the target of a locally finitely presented morphism is open.
public theorem isOpen_setOf_flatOverAt
{X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFinitePresentation f]
(F : X.Modules) [F.IsQuasicoherent] [F.IsFinitePresentation] :
IsOpen {x : X | IsFlatOverAt f.toLRSHom.toShHom F x}
Tag 047C, a lemma
Tag 047C in the Stacks Project.
AlgebraicGeometry.modulePullback_isFlatOverAt_of_isFlatOverAt, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FlatMorphisms/FlatLocusBaseChange.lean, line 131. The attribute's comment: “part (1)”.
Stacks Project, Tag 047C (1). For a cartesian square of schemes a quasi-coherent module which is flat over the base at the image of a point pulls back to a module which is flat over the new base at that point. Nothing is assumed of the base morphism, so this holds for an arbitrary base change. This is a restatement of
AlgebraicGeometry.modulePullback_isFlatOverAt.
public lemma modulePullback_isFlatOverAt_of_isFlatOverAt
{X S S' X' : Scheme.{u}} {f : X ⟶ S} {g : S' ⟶ S}
{g' : X' ⟶ X} {f' : X' ⟶ S'} (h : IsPullback g' f' f g)
(F : SheafOfModules.{u} (structureSheafRing X.toRingedSpace)) [F.IsQuasicoherent]
(x' : X') (hF : IsFlatOverAt f.toLRSHom.toShHom F (g' x')) :
IsFlatOverAt f'.toLRSHom.toShHom ((modulePullback g'.toLRSHom.toShHom).obj F) x'
AlgebraicGeometry.isFlatOverAt_of_modulePullback, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FlatMorphisms/FlatLocusBaseChange.lean, line 142. The attribute's comment: “part (2)”. References: SGA 3 V (7.4), “(i) descent”.
Stacks Project, Tag 047C (2). Relative flatness of the pullback of a quasi-coherent module along a cartesian square descends at a point at which the base morphism is flat.
public lemma isFlatOverAt_of_modulePullback
{X S S' X' : Scheme.{u}} {f : X ⟶ S} {g : S' ⟶ S}
{g' : X' ⟶ X} {f' : X' ⟶ S'} (h : IsPullback g' f' f g)
(F : SheafOfModules.{u} (structureSheafRing X.toRingedSpace)) [F.IsQuasicoherent]
(x' : X') (hg : IsFlatAt g.toLRSHom.toShHom (f' x'))
(hF : IsFlatOverAt f'.toLRSHom.toShHom
((modulePullback g'.toLRSHom.toShHom).obj F) x') :
IsFlatOverAt f.toLRSHom.toShHom F (g' x')
AlgebraicGeometry.setOf_isFlatOverAt_modulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FlatMorphisms/FlatLocusBaseChange.lean, line 180. The attribute's comment: “flat locus”.
Stacks Project, Tag 047C (flat locus). Under flat base change the relative flat locus of a quasi-coherent module is the preimage of the relative flat locus of the module itself.
public theorem setOf_isFlatOverAt_modulePullback
{X S S' X' : Scheme.{u}} {f : X ⟶ S} {g : S' ⟶ S}
{g' : X' ⟶ X} {f' : X' ⟶ S'} (h : IsPullback g' f' f g)
(F : SheafOfModules.{u} (structureSheafRing X.toRingedSpace)) [F.IsQuasicoherent]
[Flat g] :
{x' : X' | IsFlatOverAt f'.toLRSHom.toShHom
((modulePullback g'.toLRSHom.toShHom).obj F) x'} =
g' ⁻¹' {x : X | IsFlatOverAt f.toLRSHom.toShHom F x}
AlgebraicGeometry.isOpen_setOf_isFlatOverAt_modulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FlatMorphisms/FlatLocusBaseChange.lean, line 202. The attribute's comment: “open locus after base change”. References: EGA IV (11.3.1), “more general”.
Stacks Project, Tag 047C (open locus). The relative flat locus of the pullback of a finitely presented quasi-coherent module along any base change of a morphism locally of finite presentation is open. Together with
AlgebraicGeometry.setOf_isFlatOverAt_modulePullbackthis says that the open subset of [Stacks, Tag 0399] commutes with flat base change.
public theorem isOpen_setOf_isFlatOverAt_modulePullback
{X S S' X' : Scheme.{u}} {f : X ⟶ S} {g : S' ⟶ S}
{g' : X' ⟶ X} {f' : X' ⟶ S'} (h : IsPullback g' f' f g)
(F : SheafOfModules.{u} (structureSheafRing X.toRingedSpace)) [F.IsQuasicoherent]
[F.IsFinitePresentation] [LocallyOfFinitePresentation f] :
IsOpen {x' : X' | IsFlatOverAt f'.toLRSHom.toShHom
((modulePullback g'.toLRSHom.toShHom).obj F) x'}
Sources
Section37.16 Critère de platitude par fibres#
Section 37.16 of the Stacks Project, Tag 039A. 8 tags here are carried by 14 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 039B, a theorem
Tag 039B in the Stacks Project.
Stacks.Flatness.isFlatOverBaseAndFiberAt_iff_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Flat/FibrewiseFiber.lean, line 703. The attribute's comment: “Noetherian fibrewise criterion”. References: EGA IV (11.3.10), “1°) a) ⇔ b)”.
For morphisms
f : X ⟶ Yandg : Y ⟶ Sof locally Noetherian schemes and a coherent𝒪_X-moduleFwith nonzero stalk atx, flatness over the base together with flatness on the fibre is equivalent to flatness ofYover the base atf xtogether with flatness ofFoverYatx.
public theorem isFlatOverBaseAndFiberAt_iff_of_isLocallyNoetherian {X Y S : Scheme.{u}}
(f : X ⟶ Y) (g : Y ⟶ S)
(F : SheafOfModules.{u} (structureSheafRing X.toRingedSpace))
[IsLocallyNoetherian S] [IsLocallyNoetherian X] [IsLocallyNoetherian Y]
[F.IsQuasicoherent] [Stacks.SheafOfModules.IsCoherent F]
(x : X)
(hx : ∃ a : TopCat.Presheaf.stalk (C := AddCommGrpCat.{u}) F.val.presheaf x,
a ≠ 0) :
IsFlatOverBaseAndFiberAt f g F x ↔ IsFlatOverIntermediateAt f g F x
Tag 039C, a theorem
Tag 039C in the Stacks Project.
Stacks.Flatness.isFlatOverBaseAndFiberAt_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Flat/FibrewiseFiber.lean, line 634. The attribute's comment: “fibrewise criterion”. References: EGA IV (11.3.10), “2°) a) ⇔ b)”.
At a point where a quasi-coherent module of finite presentation has nonzero stalk, flatness over the base together with flatness on the fibre is equivalent to flatness of the intermediate scheme over the base together with flatness over the intermediate scheme.
public theorem isFlatOverBaseAndFiberAt_iff {X Y S : Scheme.{u}}
(f : X ⟶ Y) (g : Y ⟶ S)
(F : SheafOfModules.{u} (structureSheafRing X.toRingedSpace))
[LocallyOfFinitePresentation (f ≫ g)] [F.IsFinitePresentation]
[LocallyOfFiniteType g]
(x : X)
(hx : ∃ a : TopCat.Presheaf.stalk (C := AddCommGrpCat.{u}) F.val.presheaf x,
a ≠ 0) :
IsFlatOverBaseAndFiberAt f g F x ↔ IsFlatOverIntermediateAt f g F x
Stacks.Flatness.isOpen_isFlatOverBaseAndFiberAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Flat/FibrewiseOpenLocus.lean, line 93. The attribute's comment: “openness of the common locus”. References: EGA IV (11.3.10), “2°) open locus”.
Stacks Project, Tag 039C. The set of points of the support of a quasi-coherent module of finite presentation at which the two equivalent conditions of the fibrewise criterion for flatness hold is open in the support.
public theorem isOpen_isFlatOverBaseAndFiberAt {X Y S : Scheme.{u}}
(f : X ⟶ Y) (g : Y ⟶ S)
(F : SheafOfModules.{u} (structureSheafRing X.toRingedSpace))
[LocallyOfFinitePresentation (f ≫ g)] [F.IsFinitePresentation] [LocallyOfFiniteType g] :
IsOpen {x : SheafOfModules.supp F |
IsFlatOverBaseAndFiberAt f g F x.1 ∧ IsFlatOverIntermediateAt f g F x.1}
Tag 039D, a lemma
Tag 039D in the Stacks Project.
AlgebraicGeometry.flat_of_flat_fiberHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FlatMorphisms/FibrewiseCriterion.lean, line 130. The attribute's comment: “flatness of the morphism”.
Stacks Project, Tag 039D. Let
f : X ⟶ Ybe a morphism of schemes over a baseS, given byg : Y ⟶ S. IfS,X,Yare locally Noetherian,Xis flat overSand every induced morphism of fibresX_s ⟶ Y_sis flat, thenfis flat.
public theorem flat_of_flat_fiberHom {X Y S : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ S)
[IsLocallyNoetherian S] [IsLocallyNoetherian X] [IsLocallyNoetherian Y] [Flat (f ≫ g)]
(hfib : ∀ s : S, Flat (Stacks.Flatness.fiberHom f g s)) :
Flat f
AlgebraicGeometry.flat_of_flat_fiberHom_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FlatMorphisms/FibrewiseCriterion.lean, line 141. The attribute's comment: “flatness of the intermediate scheme over the base”.
Stacks Project, Tag 039D. In the situation of
AlgebraicGeometry.flat_of_flat_fiberHom, iffis in addition surjective thenYis flat over the base.
public theorem flat_of_flat_fiberHom_of_surjective {X Y S : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ S)
[IsLocallyNoetherian S] [IsLocallyNoetherian X] [IsLocallyNoetherian Y] [Flat (f ≫ g)]
[Surjective f] (hfib : ∀ s : S, Flat (Stacks.Flatness.fiberHom f g s)) :
Flat g
Tag 039E, a lemma
Tag 039E in the Stacks Project.
Stacks.Flatness.flat_of_flat_fiberHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Flat/FibrewiseMorphism.lean, line 220. The attribute's comment: “flatness of the morphism”. References: EGA IV (20.5.7), “partial”; SGA 1 I (5.9), “partial”.
Stacks Project, Tag 039E. Let
f : X ⟶ Yandg : Y ⟶ Sbe morphisms of schemes withXlocally of finite presentation and flat overS, withYlocally of finite type overS, and with the morphismX_s ⟶ Y_sof fibres flat for every pointsofS. Thenfis flat.
public theorem flat_of_flat_fiberHom {X Y S : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ S)
[LocallyOfFinitePresentation (f ≫ g)] [LocallyOfFiniteType g]
[AlgebraicGeometry.Flat (f ≫ g)]
(hfib : ∀ s : S, AlgebraicGeometry.Flat (fiberHom f g s)) :
AlgebraicGeometry.Flat f
Stacks.Flatness.flat_of_flat_fiberHom_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Flat/FibrewiseMorphism.lean, line 232. The attribute's comment: “flatness of the target over the base”.
Stacks Project, Tag 039E. In the situation of
Stacks.Flatness.flat_of_flat_fiberHom, iffis moreover surjective thenYis flat overS.
public theorem flat_of_flat_fiberHom_of_surjective {X Y S : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ S)
[LocallyOfFinitePresentation (f ≫ g)] [LocallyOfFiniteType g]
[AlgebraicGeometry.Flat (f ≫ g)] [AlgebraicGeometry.Surjective f]
(hfib : ∀ s : S, AlgebraicGeometry.Flat (fiberHom f g s)) :
AlgebraicGeometry.Flat g
Tag 05VJ, a lemma
Tag 05VJ in the Stacks Project.
AlgebraicGeometry.isOpen_setOf_isFlatOverAt_of_locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FlatMorphisms/FlatLocusBaseChange.lean, line 318. The attribute's comment: “open locus”.
Stacks Project, Tag 05VJ (open locus). For a morphism
f : X ⟶ Yof schemes over a base withXlocally of finite presentation over the base andYlocally of finite type over it, the locus where a finitely presented quasi-coherent𝒪_X-module is flat overYis open, becausefis then itself locally of finite presentation.
public theorem isOpen_setOf_isFlatOverAt_of_locallyOfFiniteType {X Y S : Scheme.{u}}
(f : X ⟶ Y) (pY : Y ⟶ S)
(F : SheafOfModules.{u} (structureSheafRing X.toRingedSpace)) [F.IsQuasicoherent]
[F.IsFinitePresentation] [LocallyOfFinitePresentation (f ≫ pY)] [LocallyOfFiniteType pY] :
IsOpen {x : X | IsFlatOverAt f.toLRSHom.toShHom F x}
AlgebraicGeometry.setOf_isFlatOverAt_modulePullback_of_isFlatOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FlatMorphisms/FlatLocusBaseChange.lean, line 335. The attribute's comment: “base change”.
Stacks Project, Tag 05VJ (base change). For a morphism
f : X ⟶ Yof schemes over a baseSwithXlocally of finite presentation overSandYlocally of finite type overS, and a finitely presented quasi-coherent𝒪_X-module flat overS, the locus where the module is flat overYcommutes with an arbitrary base changeS' ⟶ S: the corresponding locus upstairs is the preimage of the original one.
public theorem setOf_isFlatOverAt_modulePullback_of_isFlatOver
{X Y S S' X' Y' : Scheme.{u}} {f : X ⟶ Y} {pY : Y ⟶ S} {g : S' ⟶ S}
{qY : Y' ⟶ Y} {pY' : Y' ⟶ S'} {qX : X' ⟶ X} {f' : X' ⟶ Y'}
(hY : IsPullback qY pY' pY g) (hX : IsPullback qX f' f qY)
(F : SheafOfModules.{u} (structureSheafRing X.toRingedSpace)) [F.IsQuasicoherent]
[F.IsFinitePresentation] [LocallyOfFinitePresentation (f ≫ pY)] [LocallyOfFiniteType pY]
(hF : IsFlatOver (f ≫ pY).toLRSHom.toShHom F) :
{x' : X' | IsFlatOverAt f'.toLRSHom.toShHom
((modulePullback qX.toLRSHom.toShHom).obj F) x'} =
qX ⁻¹' {x : X | IsFlatOverAt f.toLRSHom.toShHom F x}
Tag 05VK, a lemma
Tag 05VK in the Stacks Project.
AlgebraicGeometry.isOpen_setOf_isFlatAt_of_locallyOfFinitePresentation_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FlatMorphisms/FibrewiseCriterion.lean, line 159. The attribute's comment: “open locus”. References: SGA 3 VIB (1.3), “partial”; SGA 3 X (4.4), “partial”; SGA 3 XV (7.2), “partial”.
Stacks Project, Tag 05VK (open locus). For a morphism
f : X ⟶ Yof schemes over a base withXlocally of finite presentation over the base andYlocally of finite type over it, the locus of points ofXat whichfis flat is open.Flatness of
Xover the base, which the source assumes, is not needed here: the two finiteness hypotheses already makeflocally of finite presentation, so Tag 0399 applies tofitself.
public theorem isOpen_setOf_isFlatAt_of_locallyOfFinitePresentation_comp {X Y S : Scheme.{u}}
(f : X ⟶ Y) (pY : Y ⟶ S) [LocallyOfFinitePresentation (f ≫ pY)] [LocallyOfFiniteType pY] :
IsOpen {x : X | IsFlatAt f.toLRSHom.toShHom x}
AlgebraicGeometry.setOf_isFlatAt_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FlatMorphisms/FibrewiseCriterion.lean, line 173. The attribute's comment: “base change”. References: EGA IV (20.5.7), “more general”; SGA 3 VIB (2.5), “flatness clause”; SGA 3 XV (7.2), “partial”.
Stacks Project, Tag 05VK (base change). For a morphism
f : X ⟶ Yof schemes over a baseSwithXlocally of finite presentation and flat overSandYlocally of finite type overS, the locus of points at whichfis flat commutes with an arbitrary base changeS' ⟶ S: the corresponding locus upstairs is the preimage of the original one.
public theorem setOf_isFlatAt_baseChange {X Y S S' X' Y' : Scheme.{u}} {f : X ⟶ Y} {pY : Y ⟶ S}
{g : S' ⟶ S} {qY : Y' ⟶ Y} {pY' : Y' ⟶ S'} {qX : X' ⟶ X} {f' : X' ⟶ Y'}
(hY : IsPullback qY pY' pY g) (hX : IsPullback qX f' f qY)
[LocallyOfFinitePresentation (f ≫ pY)] [LocallyOfFiniteType pY] [Flat (f ≫ pY)] :
{x' : X' | IsFlatAt f'.toLRSHom.toShHom x'} =
qX ⁻¹' {x : X | IsFlatAt f.toLRSHom.toShHom x}
Tag 080Q, a lemma
Tag 080Q in the Stacks Project.
AlgebraicGeometry.Scheme.Modules.exists_iso_free_over_of_flat_over_at_of_flat_fiber_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiberRank/FlatFibreFiniteFree.lean, line 178.
Stacks Project, Tag 080Q. Let
f : X ⟶ Sbe a morphism of finite presentation and letFbe a finitely presented𝒪_X-module. IfFis flat overSatxand the stalk atxof the restriction ofFto the fibre offthroughxis a flat module over the local ring of that fibre, thenFis free of finite rank on an open neighbourhood ofx.
theorem exists_iso_free_over_of_flat_over_at_of_flat_fiber_stalk {X S : Scheme.{u}} (f : X ⟶ S)
(hf : AlgebraicGeometry.FinitePresentation f) (F : X.Modules) [F.IsFinitePresentation]
(x : X)
(hflat : AlgebraicGeometry.IsFlatOverAt (Scheme.Hom.toLRSHom f).toShHom F x)
(hfiber :
letI := Stacks.Flatness.stalkModule
((Scheme.Modules.pullback (f.fiberι (f x))).obj F) (f.asFiber x)
Module.Flat (ToType ((f.fiber (f x)).presheaf.stalk (f.asFiber x)))
(ToType (TopCat.Presheaf.stalk (C := AddCommGrpCat.{u})
((Scheme.Modules.pullback (f.fiberι (f x))).obj F).val.presheaf (f.asFiber x)))) :
∃ U : X.Opens, x ∈ U ∧ ∃ n : ℕ,
Nonempty (F.over U ≅ SheafOfModules.free (ULift.{u} (Fin n)))
Tag 0CZR, a lemma
Tag 0CZR in the Stacks Project.
AlgebraicGeometry.Scheme.Modules.isOpen_freeLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiberRank/FreeLocusBaseChange.lean, line 85. The attribute's comment: “openness”.
Stacks Project, Tag 0CZR (openness). The locus of points at which a sheaf of modules on a scheme is free of finite rank on a neighbourhood is open: the trivialising neighbourhood of a point of the locus is contained in the locus.
public theorem isOpen_freeLocus {X : Scheme.{u}} (F : X.Modules) :
IsOpen (freeLocus F)
AlgebraicGeometry.Scheme.Modules.freeLocus_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiberRank/FreeLocusBaseChange.lean, line 197. The attribute's comment: “base change”.
Stacks Project, Tag 0CZR (base change). Let
f : X ⟶ Sbe locally of finite presentation and letFbe a finitely presented𝒪_X-module flat overS. The formation of the locus of points at whichFis free of finite rank on a neighbourhood commutes with an arbitrary base changeg : S' ⟶ S: the locus of the pulled-back module is the preimage of the original locus under the projection.
public theorem freeLocus_pullback {X S S' : Scheme.{u}} (f : X ⟶ S)
(F : X.Modules) [F.IsFinitePresentation] [LocallyOfFinitePresentation f]
(hF : AlgebraicGeometry.IsFlatOver f.toLRSHom.toShHom F) (g : S' ⟶ S) :
freeLocus ((Scheme.Modules.pullback (pullback.fst f g)).obj F) =
pullback.fst f g ⁻¹' freeLocus F
Sources
Section37.17 Closed immersions between smooth schemes#
Section 37.17 of the Stacks Project, Tag 0H1G. 3 tags here are carried by 10 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0FUE, a lemma
Tag 0FUE in the Stacks Project.
Stacks.AlgebraicGeometry.exists_etale_coordinateSubspaceEmbedding_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SmoothClosedImmersionCoordinates.lean, line 1010.
Stacks Project, Tag 0FUE. Let
Sbe a scheme and leti : Y ⟶ Xbe a closed immersion of schemes smooth overS. For everyy : Ythere are integersm, n ≥ 0, an openU ⊆ Xwhose inverse imageV = i⁻¹(U)containsy, an étale morphismπ : U ⟶ 𝐀^{m+n}_SoverSand a morphismq : V ⟶ 𝐀^m_Smakingcommute with cartesian right-hand square, i.e.Y ←── V ──→ 𝐀^m_S │ │ │ ↓ ↓ ↓ X ←── U ──→ 𝐀^{m+n}_SV = π⁻¹(𝐀^m_S).
theorem exists_etale_coordinateSubspaceEmbedding_isPullback
{S X Y : Scheme.{u}} (f : X ⟶ S) (i : Y ⟶ X)
[IsClosedImmersion i] [Smooth f] [Smooth (i ≫ f)] (y : Y) :
∃ (m n : ℕ) (U : X.Opens) (_ : y ∈ i ⁻¹ᵁ U)
(π : U.toScheme ⟶ AffineSpace (ULift.{u} (Fin (m + n))) S)
(q : (i ⁻¹ᵁ U).toScheme ⟶ AffineSpace (ULift.{u} (Fin m)) S),
Etale π ∧
π ≫ (AffineSpace.over (ULift.{u} (Fin (m + n))) S).hom = U.ι ≫ f ∧
IsPullback
(i.resLE U (i ⁻¹ᵁ U) le_rfl) q π (coordinateSubspaceEmbedding S m n)
Tag 0H1H, a remark
Tag 0H1H in the Stacks Project.
Stacks.MoreMorphisms.coordinateEmbedding_ker_eq_span, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/CoordinateBlowup.lean, line 139. The attribute's comment: “ideal of the center”.
The scheme-theoretic centre is cut out by exactly the last
ncoordinates.
public theorem coordinateEmbedding_ker_eq_span :
coordinateRingIdeal R m n = RingHom.ker (coordinateProjection R m n)
Stacks.MoreMorphisms.coordinateChart_equiv_polynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/CoordinateBlowup.lean, line 406. The attribute's comment: “polynomial affine blowup charts”.
The
i-th standard blowup chart is polynomial affine space, with its original coordinates given byx_k,y_i, andy_j = y_i t_j.
public theorem coordinateChart_equiv_polynomial :
∃ e : coordinateChartAlgebra R m n i ≃+*
MvPolynomial (coordinateChartVariables m n i) R,
(∀ r : R,
e (algebraMap R (coordinateChartAlgebra R m n i) r) = C r) ∧
(∀ k : Fin m,
e (algebraMap (MvPolynomial (Fin m ⊕ Fin n) R)
(coordinateChartAlgebra R m n i) (X (Sum.inl k))) = X (Sum.inl k)) ∧
(e (algebraMap (MvPolynomial (Fin m ⊕ Fin n) R)
(coordinateChartAlgebra R m n i) (X (Sum.inr i))) = X (Sum.inr (Sum.inl ()))) ∧
(∀ j : Fin n, ∀ h : j ≠ i,
e (algebraMap (MvPolynomial (Fin m ⊕ Fin n) R)
(coordinateChartAlgebra R m n i) (X (Sum.inr j))) =
X (Sum.inr (Sum.inl ())) * X (Sum.inr (Sum.inr ⟨j, h⟩)))
Stacks.MoreMorphisms.coordinateChart_exceptionalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/CoordinateBlowup.lean, line 435. The attribute's comment: “equation of the exceptional divisor in each chart”.
On the
i-th affine chart, the exceptional ideal is generated by the single coordinatey_i.
public theorem coordinateChart_exceptionalIdeal (i : Fin n) :
Ideal.map (algebraMap (MvPolynomial (Fin m ⊕ Fin n) R) (coordinateChartAlgebra R m n i))
(coordinateRingIdeal R m n) =
Ideal.span {(algebraMap (MvPolynomial (Fin m ⊕ Fin n) R) (coordinateChartAlgebra R m n i)
(X (Sum.inr i)))}
Stacks.MoreMorphisms.blowUp_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/CoordinateBlowupSmooth.lean, line 548. The attribute's comment: “smoothness of the blowup”.
Stacks Project, Tag 0H1H. The blowup of affine
(m + n)-space along the coordinate affinem-subspace is smooth over the base ring.The hypothesis
0 < nis the one the source carries and is not used; seeStacks.MoreMorphisms.blowUp_smooth_of_posfor the same statement without it.
public theorem blowUp_smooth (_hn : 0 < n) :
Smooth (blowUpToBase (coordinateIdeal R m n) ≫
Spec.map (CommRingCat.ofHom (C : R →+* MvPolynomial (Fin m ⊕ Fin n) R)))
Stacks.MoreMorphisms.exceptionalDivisor_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/CoordinateExceptionalSmooth.lean, line 552. The attribute's comment: “smoothness of the exceptional divisor”.
The exceptional divisor of the blowup of affine
(m + n)-space along the coordinate affinem-subspace is smooth over the base ring.The hypothesis
0 < nis the one the source carries and is not used; seeStacks.MoreMorphisms.exceptionalDivisor_smooth_of_posfor the same theorem without it.
public theorem exceptionalDivisor_smooth (_hn : 0 < n) :
Smooth ((exceptionalIdeal (coordinateIdeal R m n)).subschemeι ≫
blowUpToBase (coordinateIdeal R m n) ≫
Spec.map (CommRingCat.ofHom (C : R →+* MvPolynomial (Fin m ⊕ Fin n) R)))
Stacks.MoreMorphisms.exists_coordinateReesPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/CoordinateReesPresentation.lean, line 43. The attribute's comment: “the Rees algebra is A[T]/(y_i T_j - y_j T_i)”.
The Rees algebra of
A = R[x₁,…,x_m,y₁,…,y_n]with respect to the ideal(y₁,…,y_n)isA[T₁,…,T_n]/(y_i T_j − y_j T_i), withT_igoing to the degree-one elementy_i.
public theorem exists_coordinateReesPresentation :
∃ E : (MvPolynomial (Fin n) (MvPolynomial (Fin m ⊕ Fin n) R) ⧸
Ideal.span (Set.range fun p : Fin n × Fin n ↦
C (X (Sum.inr p.1)) * X p.2 - C (X (Sum.inr p.2)) * X p.1))
≃ₐ[MvPolynomial (Fin m ⊕ Fin n) R] reesAlgebra (coordinateRingIdeal R m n),
∀ j : Fin n,
(E (Ideal.Quotient.mk _ (X j)) : Polynomial (MvPolynomial (Fin m ⊕ Fin n) R)) =
Polynomial.monomial 1 (X (Sum.inr j))
Stacks.MoreMorphisms.coordinateEmbedding_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/CoordinateSubspace.lean, line 78. The attribute's comment: “coordinate closed immersion”.
The coordinate affine subspace is closed in the ambient affine space.
public theorem coordinateEmbedding_isClosedImmersion (R : Type*) [CommRing R] (m n : ℕ) :
IsClosedImmersion (coordinateEmbedding R m n)
Tag 0FUT, a lemma
Tag 0FUT in the Stacks Project.
Stacks.AlgebraicGeometry.smooth_exceptionalDivisor_isoProjectiveBundle_twistOne_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ExceptionalProjectiveBundle.lean, line 408. The attribute's comment: “all four assertions, for a closed immersion of schemes smooth over the base”.
Stacks Project, Tag 0FUT. Let
Sbe a scheme and leti : Z ⟶ Xbe a closed immersion of schemes smooth overS, with ideal sheafℐ = ker(i) ⊂ 𝒪_X. Letb : X' ⟶ Xbe the blowup ofXinℐandE ⊆ X'its exceptional divisor. ThenX'andEare smooth overS; the morphismp : E ⟶ Zis canonically isomorphic to the projective space bundle𝐏(ℐ/ℐ²) ⟶ Z; and the relative𝒪_E(1)of that bundle structure is the restriction of𝒪_{X'}(-E)toE.The morphisms to the centre are the two morphisms
p : E ⟶ Zandq : 𝐏(ℐ/ℐ²) ⟶ ZoverX, each determined by its composite with the closed immersioni, and the third assertion is that the identificationE ≅ 𝐏(ℐ/ℐ²)carriesptoq.This is
Stacks.AlgebraicGeometry.smooth_exceptionalDivisor_isoProjectiveBundle_twistOneread at the ideal sheafi.kerof the closed immersion, whose closed subschemeV(i.ker)receivesZby the canonical isomorphismAlgebraicGeometry.Scheme.Hom.toImageonto the scheme-theoretic image; smoothness transports along that isomorphism, andpandqare read onZthrough its inverse.
theorem smooth_exceptionalDivisor_isoProjectiveBundle_twistOne_of_isClosedImmersion
(i : Z ⟶ X) [IsClosedImmersion i] [Smooth f] [Smooth (i ≫ f)] :
Smooth (blowUpToBase i.ker ≫ f) ∧
Smooth ((exceptionalIdeal i.ker).subschemeι ≫ blowUpToBase i.ker ≫ f) ∧
∃ (p : exceptionalDivisor i.ker ⟶ Z)
(q : projectiveBundle i.ker.subscheme
(Stacks.Conormal.conormalSheafDegreeOne i.ker.subschemeι) ⟶ Z)
(e : exceptionalDivisor i.ker ≅
projectiveBundle i.ker.subscheme
(Stacks.Conormal.conormalSheafDegreeOne i.ker.subschemeι)),
p ≫ i = (exceptionalIdeal i.ker).subschemeι ≫ blowUpToBase i.ker ∧
q ≫ i = projectiveBundleToBase i.ker.subscheme
(Stacks.Conormal.conormalSheafDegreeOne i.ker.subschemeι) ≫ i.ker.subschemeι ∧
e.hom ≫ q = p ∧
Nonempty ((Scheme.Modules.pullback e.hom).obj
(Situation.twistSheaf (symmetricSituationOfQuasicoherent i.ker.subscheme
(Stacks.Conormal.conormalSheafDegreeOne i.ker.subschemeι)) 1)
≅ (Scheme.Modules.pullback (exceptionalIdeal i.ker).subschemeι).obj
(exceptionalIdealModule i.ker))
Stacks.AlgebraicGeometry.smooth_blowUpToBase_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/SmoothCentre.lean, line 377. The attribute's comment: “smoothness of the blowup”. References: SGA 7 II (2.1), “more general”; SGA 7 XVIII (2.1), “Smoothness of tilde X”; SGA 7 XVIII (3.1), “more general”.
Stacks Project, Tag 0FUT, first assertion. Let
Sbe a scheme and leti : Z ⟶ Xbe a closed immersion of schemes smooth overS. Then the blowup ofXinZis smooth overS.
theorem smooth_blowUpToBase_comp {S X Z : Scheme.{u}} (f : X ⟶ S) (i : Z ⟶ X)
[IsClosedImmersion i] [Smooth f] [Smooth (i ≫ f)] :
Smooth (blowUpToBase i.ker ≫ f)
Sources
Section37.18 Flat modules and relative assassins#
Section 37.18 of the Stacks Project, Tag 0GSF. 6 tags here are carried by 10 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0GSG, a lemma
Tag 0GSG in the Stacks Project.
Module.Flat.injective_of_injective_mapQ_maximalIdeal_of_valuationRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/InjectiveModMaximalIdealOverValuationRing.lean, line 187. The attribute's comment: “injectivity”.
The injectivity half of Stacks 0GSG. Let
Abe a valuation ring, letA → Bbe a local homomorphism of local rings which is essentially of finite type, and letu : N → Mbe a map of finiteB-modules withMflat overA. Ifū : N/𝔪_A N → M/𝔪_A Mis injective thenuis injective.
theorem injective_of_injective_mapQ_maximalIdeal_of_valuationRing
{A : Type u₁} {B : Type u₂} {N : Type u₃} {M : Type u₄}
[CommRing A] [IsDomain A] [ValuationRing A]
[CommRing B] [Algebra A B] [IsLocalRing B] [IsLocalHom (algebraMap A B)]
[Algebra.EssFiniteType A B]
[AddCommGroup N] [Module A N] [Module B N] [IsScalarTower A B N] [Module.Finite B N]
[AddCommGroup M] [Module A M] [Module B M] [IsScalarTower A B M] [Module.Finite B M]
[Module.Flat A M]
(u : N →ₗ[B] M)
(hu : Function.Injective
(Submodule.mapQ (maximalIdeal A • (⊤ : Submodule A N))
(maximalIdeal A • (⊤ : Submodule A M)) (u.restrictScalars A)
(Submodule.smul_top_le_comap_smul_top (maximalIdeal A) (u.restrictScalars A)))) :
Function.Injective u
Module.Flat.flat_quotient_range_of_injective_mapQ_maximalIdeal_of_valuationRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/InjectiveModMaximalIdealOverValuationRing.lean, line 208. The attribute's comment: “flatness of the cokernel”.
The cokernel half of Stacks 0GSG. Let
Abe a valuation ring, letA → Bbe a local homomorphism of local rings which is essentially of finite type, and letu : N → Mbe a map of finiteB-modules withMflat overA. Ifū : N/𝔪_A N → M/𝔪_A Mis injective thenM/u(N)is flat overA.
theorem flat_quotient_range_of_injective_mapQ_maximalIdeal_of_valuationRing
{A : Type u₁} {B : Type u₂} {N : Type u₃} {M : Type u₄}
[CommRing A] [IsDomain A] [ValuationRing A]
[CommRing B] [Algebra A B] [IsLocalRing B] [IsLocalHom (algebraMap A B)]
[Algebra.EssFiniteType A B]
[AddCommGroup N] [Module A N] [Module B N] [IsScalarTower A B N] [Module.Finite B N]
[AddCommGroup M] [Module A M] [Module B M] [IsScalarTower A B M] [Module.Finite B M]
[Module.Flat A M]
(u : N →ₗ[B] M)
(hu : Function.Injective
(Submodule.mapQ (maximalIdeal A • (⊤ : Submodule A N))
(maximalIdeal A • (⊤ : Submodule A M)) (u.restrictScalars A)
(Submodule.smul_top_le_comap_smul_top (maximalIdeal A) (u.restrictScalars A)))) :
Module.Flat A (M ⧸ LinearMap.range u)
Tag 0GSH, a lemma
Tag 0GSH in the Stacks Project.
Stacks.RelativeAssassin.exists_valuation_base_change_generic_component, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RelativeAssassin/ValuationBaseChange.lean, line 191.
A valuation-ring base change through a prescribed generic point of a component of the fibre of the integral closure of a point.
theorem exists_valuation_base_change_generic_component
{X S : Scheme.{u}} (f : X ⟶ S) (y : X)
(Y : X.IdealSheafData)
(hY : Y = Scheme.IdealSheafData.vanishingIdeal
(Closeds.closure ({y} : Set X)))
(s : S) (x : X)
(ξ : (Y.subschemeι ≫ f).fiber s)
(hξ : closure ({ξ} : Set ((Y.subschemeι ≫ f).fiber s)) ∈
irreducibleComponents ((Y.subschemeι ≫ f).fiber s))
(hx : Y.subschemeι ((Y.subschemeι ≫ f).fiberι s ξ) = x) :
∃ (A : Type u) (_ : CommRing A) (_ : IsDomain A) (_ : ValuationRing A)
(g : Spec (.of A) ⟶ S),
g (genericPoint (Spec (.of A))) = f y ∧
g (closedPoint A) = s ∧
(let X' := (pullback f g : Scheme.{u})
let p : X' ⟶ X := pullback.fst f g
let q : X' ⟶ Spec (.of A) := pullback.snd f g
let Z : X'.IdealSheafData := Y.comap p
let j : Z.subscheme ⟶ X' := Z.subschemeι
∃ η : (j ≫ q).fiber (genericPoint (Spec (.of A))),
closure ({η} : Set ((j ≫ q).fiber (genericPoint (Spec (.of A))))) ∈
irreducibleComponents ((j ≫ q).fiber (genericPoint (Spec (.of A)))) ∧
p (j ((j ≫ q).fiberι (genericPoint (Spec (.of A))) η)) = y ∧
(let y' : X' := j ((j ≫ q).fiberι (genericPoint (Spec (.of A))) η)
let Y' : X'.IdealSheafData :=
Scheme.IdealSheafData.vanishingIdeal (Closeds.closure ({y'} : Set X'))
IsIntegral Y'.subscheme ∧
∃ ξ' : (Y'.subschemeι ≫ q).fiber (closedPoint A),
closure ({ξ'} : Set ((Y'.subschemeι ≫ q).fiber (closedPoint A))) ∈
irreducibleComponents ((Y'.subschemeι ≫ q).fiber (closedPoint A)) ∧
p (Y'.subschemeι ((Y'.subschemeι ≫ q).fiberι (closedPoint A) ξ')) = x))
Tag 0GSI, a lemma
Tag 0GSI in the Stacks Project.
Stacks.RelativeAssassin.topologicalKrullDimAt_fiber_eq_fiber_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RelativeAssassin/FlatFibreDimension.lean, line 894. The attribute's comment: “the fibre dimension equality”. References: EGA IV (12.1.1.4), “fibre dimension equality”; EGA IV (12.1.1.5), “dim(Z'_y)=dim(Z'_{y'})”.
Fibre dimension at a generic point of the fibre of a closure. Let
f : X ⟶ Sbe locally of finite type,Fa quasi-coherent finite type𝒪_X-module andya point ofAss_{X/S}(F). LetYbe the reduced closed subscheme supported on the closure ofy. At a generic pointxof an irreducible component of the fibre ofYoversat whose imageFis flat overS, the local dimension of that fibre equals the dimension of the fibre ofYoverf y.
theorem topologicalKrullDimAt_fiber_eq_fiber_of_flat
{X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
(F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
(y : X) (hy : y ∈ Stacks.Divisors.relativeAssassin f F) (s : S) :
let Y := Scheme.IdealSheafData.vanishingIdeal
(⟨closure ({y} : Set X), isClosed_closure⟩ : Closeds X)
let g : Y.subscheme ⟶ S := Y.subschemeι ≫ f
∀ x : g.fiber s,
(∃ Z : irreducibleComponents (g.fiber s), IsGenericPoint x (Z : Set (g.fiber s))) →
AlgebraicGeometry.IsFlatOverAt f.toLRSHom.toShHom F (Y.subschemeι (g.fiberι s x)) →
topologicalKrullDimAt (g.fiber s) x = topologicalKrullDim (g.fiber (f y))
Stacks.RelativeAssassin.mem_relativeAssassin_of_isGenericPoint_fibre_closure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RelativeAssassin/FlatFibreSpecialization.lean, line 228. The attribute's comment: “the relative assassin conclusion”. References: EGA IV (12.1.1.4), “z ∈ Ass(F_y)”; EGA IV (12.1.1.5), “z ∈ Ass(F_y)”.
Relative associated points at generic points of the fibres of a closure. Let
f : X ⟶ Sbe locally of finite type,Fa quasi-coherent finite type𝒪_X-module andya point ofAss_{X/S}(F). LetYbe the reduced closed subscheme supported on the closure ofyand letξbe a generic point of an irreducible component of the fibre ofYover a pointsofS. IfFis flat overSat the image ofξinX, that image lies inAss_{X/S}(F).
theorem mem_relativeAssassin_of_isGenericPoint_fibre_closure
{X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
(F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
(y : X) (hy : y ∈ Stacks.Divisors.relativeAssassin f F)
(Y : X.IdealSheafData)
(hY : Y = Scheme.IdealSheafData.vanishingIdeal (Closeds.closure ({y} : Set X)))
(s : S) (ξ : (Y.subschemeι ≫ f).fiber s)
(hξ : closure ({ξ} : Set ((Y.subschemeι ≫ f).fiber s)) ∈
irreducibleComponents ((Y.subschemeι ≫ f).fiber s))
(hflat : IsFlatOverAt f.toLRSHom.toShHom F
(Y.subschemeι ((Y.subschemeι ≫ f).fiberι s ξ))) :
Y.subschemeι ((Y.subschemeι ≫ f).fiberι s ξ)
∈ Stacks.Divisors.relativeAssassin f F
Tag 0H3X, a lemma
Tag 0H3X in the Stacks Project.
Stacks.RelativeAssassin.topologicalKrullDim_supp_fiber_le_of_generic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RelativeAssassin/FlatFibreSupportDimension.lean, line 390.
Stacks Project, Tag 0H3X. The dimension of the support of a finite type quasi-coherent module flat over an irreducible base does not increase from the generic fibre to any other fibre.
theorem topologicalKrullDim_supp_fiber_le_of_generic
{X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
(F : X.Modules) [F.IsFiniteType] [F.IsQuasicoherent]
(hF : AlgebraicGeometry.IsFlatOver f.toLRSHom.toShHom F)
[IrreducibleSpace S] (η : S) (hη : IsGenericPoint η Set.univ)
(r : WithBot ℕ∞)
(hdim : topologicalKrullDim
(SheafOfModules.supp ((Scheme.Modules.pullback (f.fiberι η)).obj F)) ≤
r)
(s : S) :
topologicalKrullDim
(SheafOfModules.supp ((Scheme.Modules.pullback (f.fiberι s)).obj F)) ≤
r
Tag 0GSJ, a lemma
Tag 0GSJ in the Stacks Project.
Stacks.RelativeAssassin.isDominant_closureSubschemeMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RelativeAssassin/ClosureRelativeDimension.lean, line 131. The attribute's comment: “dominance of the canonical map”.
The canonical map from the reduced closure of a point to the reduced closure of its image is dominant.
theorem isDominant_closureSubschemeMap
{X S : Scheme.{u}} (f : X ⟶ S) (y : X) :
let Y := Scheme.IdealSheafData.vanishingIdeal
(Closeds.closure ({y} : Set X))
let T := Scheme.IdealSheafData.vanishingIdeal
(Closeds.closure ({f y} : Set S))
let h : Y.subscheme ⟶ T.subscheme :=
Scheme.IdealSheafData.subschemeMap Y T f (by
rw [Scheme.IdealSheafData.map_vanishingIdeal]
apply le_of_eq
apply congrArg Scheme.IdealSheafData.vanishingIdeal
apply Closeds.ext
change closure ({f y} : Set S) = closure (f '' closure ({y} : Set X))
exact ((closure_image_closure f.continuous).trans (by simp)).symm)
IsDominant h
Stacks.RelativeAssassin.relativeDimension_closureSubschemeMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RelativeAssassin/ClosureRelativeDimension.lean, line 212. The attribute's comment: “part (2)”. References: EGA IV (12.1.1.4), “equidimensional Z'→Y'”; EGA IV (12.1.1.5), “equidimensionality”.
If the module is flat at component-generic fibre points, the canonical map from the reduced closure of a relative associated point to the reduced closure of its image has constant relative dimension.
theorem relativeDimension_closureSubschemeMap
{X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
(F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
(y : X) (hy : y ∈ Stacks.Divisors.relativeAssassin f F) :
let Y := Scheme.IdealSheafData.vanishingIdeal
(Closeds.closure ({y} : Set X))
let T := Scheme.IdealSheafData.vanishingIdeal
(Closeds.closure ({f y} : Set S))
let h : Y.subscheme ⟶ T.subscheme :=
Scheme.IdealSheafData.subschemeMap Y T f (by
rw [Scheme.IdealSheafData.map_vanishingIdeal]
apply le_of_eq
apply congrArg Scheme.IdealSheafData.vanishingIdeal
apply Closeds.ext
change closure ({f y} : Set S) = closure (f '' closure ({y} : Set X))
exact ((closure_image_closure f.continuous).trans (by simp)).symm)
(∀ t : T.subscheme, ∀ x : h.fiber t,
(∃ Z : irreducibleComponents (h.fiber t),
IsGenericPoint x (Z : Set (h.fiber t))) →
AlgebraicGeometry.IsFlatOverAt f.toLRSHom.toShHom F
(Y.subschemeι (h.fiberι t x))) →
let hh : LocallyOfFiniteType h := by
have : LocallyOfFiniteType (h ≫ T.subschemeι) := by
rw [Scheme.IdealSheafData.subschemeMap_subschemeι]
infer_instance
exact locallyOfFiniteType_of_comp h T.subschemeι
letI : LocallyOfFiniteType h := hh
∃ d : ℕ, RelativeDimension h d
Declarations registered for the tag:
Stacks.RelativeAssassin.mem_relativeAssassin_of_isGenericPoint_fibre_closure, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/MoreMorphisms/RelativeAssassin/ClosureRelativeDimension.lean, line 125 (StacksFrontier): “part (1)”.
Tag 0GSK, a remark
Tag 0GSK in the Stacks Project.
Stacks.RelativeAssassin.relativeDimension_of_isGenericPoint_of_trdeg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RelativeAssassin/RelativeDimensionCriteria.lean, line 324. The attribute's comment: “first set of hypotheses”.
Stacks Project, Tag 0GSK, first set of hypotheses. Let
f : X ⟶ Sbe locally of finite type withXintegral of generic pointξ, and letFbe a quasi-coherent𝒪_X-module of finite type whose support is all ofXand which is flat overSat every generic point of every fibre. If the transcendence degree ofκ(ξ)overκ(f ξ)isd, thenfhas relative dimensiondin the sense of Tag 02NJ.Only the irreducibility of
Xis used, not its reducedness, and the flatness hypothesis is the one the source's last sentence allows; flatness ofFoverSeverywhere, which the source's list asks for, gives it asfun s z _ => hF _.
theorem relativeDimension_of_isGenericPoint_of_trdeg (f : X ⟶ S) [LocallyOfFiniteType f]
[IsIntegral X] (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
(hsupp : SheafOfModules.supp F = Set.univ)
(hflat : ∀ (s : S) (z : f.fiber s), z ∈ genericPoints (f.fiber s) →
AlgebraicGeometry.IsFlatOverAt f.toLRSHom.toShHom F (f.fiberι s z))
(ξ : X) (hξ : IsGenericPoint ξ (Set.univ : Set X)) (d : ℕ)
(hd : letI := (f.residueFieldMap ξ).hom.toAlgebra
Cardinal.toENat (Algebra.trdeg (S.residueField (f ξ)) (X.residueField ξ)) = (d : ℕ∞)) :
AlgebraicGeometry.RelativeDimension f d
Stacks.RelativeAssassin.relativeDimension_of_dense_fiber_of_component_dim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RelativeAssassin/RelativeDimensionCriteria.lean, line 442. The attribute's comment: “second set of hypotheses”.
Stacks Project, Tag 0GSK, second set of hypotheses. Let
f : X ⟶ Sbe locally of finite type and letFbe a quasi-coherent𝒪_X-module of finite type whose support is all ofXand which is flat overSat every generic point of every fibre. If the fibre over a pointηofSis dense inXand every irreducible component of that fibre has dimensiond, thenfhas relative dimensiondin the sense of Tag 02NJ.The source asks in addition that
Sbe irreducible withηits generic point, which is what makes the density plausible; the argument uses only the density itself, so that hypothesis is dropped here and the source's statement is the case of an irreducibleSand its generic point. The flatness hypothesis is again the weakened one of the source's last sentence.
theorem relativeDimension_of_dense_fiber_of_component_dim (f : X ⟶ S) [LocallyOfFiniteType f]
(F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
(hsupp : SheafOfModules.supp F = Set.univ)
(hflat : ∀ (s : S) (z : f.fiber s), z ∈ genericPoints (f.fiber s) →
AlgebraicGeometry.IsFlatOverAt f.toLRSHom.toShHom F (f.fiberι s z))
(η : S) (hdense : Dense (f ⁻¹' ({η} : Set S))) (d : ℕ)
(hdim : ∀ Z ∈ irreducibleComponents (f.fiber η), topologicalKrullDim Z = (d : WithBot ℕ∞)) :
AlgebraicGeometry.RelativeDimension f d
Sources
Section37.19 Normalization revisited#
Section 37.19 of the Stacks Project, Tag 081J. 3 tags here are carried by 10 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 081K, a lemma
Tag 081K in the Stacks Project.
Stacks.IntegralClosure.SmoothPullback.bijective_toIntegralClosure_sections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Smooth/IntegralClosure.lean, line 183. The attribute's comment: “affine-open comparison map. The equality of subsheaves is asserted over a pair of affine opens V ⊆ Y, U ⊆ S with V ⊆ g⁻¹U, as bijectivity of the canonical map out of the base change of the sections of the integral closure, the quasi-coherent algebra being presented as f_*𝒪_X for f quasi-compact and quasi-separated. The identification of the sections of the pullback is sectionsBaseChangeEquiv, pinned by sectionsBaseChangeEquiv_tmul_one and sectionsBaseChangeEquiv_one_tmul. The same assertion in terms of the integral-closure subalgebra itself is range_integralClosureAlgebraι_app_pullback. The sheaf-level equality is not asserted here. See the module docstring.”. References: EGA IV (18.12.15); EGA IV (6.14.5), “smooth, affine opens”.
Stacks Project, Tag 081K, over a pair of affine opens. Let
g : Y ⟶ Sbe a smooth morphism, let𝒜 = f_*𝒪_Xbe a quasi-coherent sheaf of𝒪_S-algebras and let𝒜'be the integral closure of𝒪_Sin𝒜. Over an affine openV ⊆ Ylying over an affine openU ⊆ S, the canonical map from𝒜'(U) ⊗_{Γ(S, U)} Γ(Y, V)to the integral closure ofΓ(Y, V)in(g^*𝒜)(V) = Γ(X ×_S Y, q⁻¹V)is bijective.
public theorem bijective_toIntegralClosure_sections [QuasiCompact f] [QuasiSeparated f] [Smooth g]
{U : S.Opens} {V : Y.Opens} (hU : IsAffineOpen U) (hV : IsAffineOpen V)
(hVU : V ≤ g ⁻¹ᵁ U) :
letI := (f.app U).hom.toAlgebra
letI := (g.appLE U V hVU).hom.toAlgebra
letI := ((pullback.snd f g).app V).hom.toAlgebra
Function.Bijective
((sectionsBaseChangeEquiv f g hU hV hVU).mapIntegralClosure.toAlgHom.comp
(TensorProduct.toIntegralClosure Γ(S, U) Γ(Y, V) Γ(X, f ⁻¹ᵁ U)))
Stacks.IntegralClosure.SmoothPullback.range_integralClosureAlgebraι_app_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Smooth/IntegralClosure.lean, line 211. The attribute's comment: “affine sections of the integral-closure subalgebra. Both sides are read over a pair of affine opens V ⊆ Y, U ⊆ S with V ⊆ g⁻¹U: the left is the sections of the integral-closure subalgebra of Stacks 035F in the pullback, the right the image of the base change of 𝒜'(U), which is the sections of that subalgebra over U by AlgebraicGeometry.Scheme.QuasicoherentAlgebra.range_integralClosureAlgebraι_app_of_isAffineOpen. The pullback is presented as f_*𝒪_{X ×_S Y}, not as algebraPullback g; the two agree by Stacks.AffineAlgebraEquivalence.isIso_baseChangeAlgebraHom, whose sections over an open are not computed in this repository, so the sheaf-level equality is not asserted here. See the module docstring.”. References: EGA IV (18.12.15); EGA IV (6.14.5), “smooth, affine opens”.
Stacks Project, Tag 081K, over a pair of affine opens and in terms of the integral-closure subalgebra itself. For
gsmooth and𝒜 = f_*𝒪_Xwithfaffine, the sections overVof the integral closure of𝒪_Ying^*𝒜are the image ofΓ(Y, V) ⊗_{Γ(S, U)} 𝒜'(U).
public theorem range_integralClosureAlgebraι_app_pullback [IsAffineHom f] [Smooth g]
{U : S.Opens} {V : Y.Opens} (hU : IsAffineOpen U) (hV : IsAffineOpen V)
(hVU : V ≤ g ⁻¹ᵁ U) :
haveI := IsSeparated.of_isAffineHom f
haveI : IsAffineHom (pullback.snd f g) := MorphismProperty.IsStableUnderBaseChange.of_isPullback
(IsPullback.of_hasPullback f g) ‹IsAffineHom f›
letI := (f.app U).hom.toAlgebra
letI := (g.appLE U V hVU).hom.toAlgebra
letI := ((pullback.snd f g).app V).hom.toAlgebra
Set.range ((integralClosureAlgebraι
(pushforwardAlgebra (pullback.snd f g))).right.hom.app (op V)) =
Set.range ((sectionsBaseChangeEquiv f g hU hV hVU).toAlgHom.comp
(Algebra.TensorProduct.map (AlgHom.id Γ(Y, V) Γ(Y, V))
(integralClosure Γ(S, U) Γ(X, f ⁻¹ᵁ U)).val))
Stacks.IntegralClosure.SheafLevel.range_integralClosureAlgebraι_app_algebraPullback_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Smooth/IntegralClosurePullback.lean, line 435. The attribute's comment: “the whole statement, in the development's own terms: the integral closure integralClosureAlgebra of the structure sheaf, the pullback algebraPullback of algebra sheaves, an arbitrary quasi-coherent 𝒜, an arbitrary open of Y, and no hypothesis beyond g smooth. The two subsheaves of g^*𝒜 are compared by the ranges of their sections, which is how the development writes an inclusion of algebra sheaves. The mathematics is range_integralClosureAlgebraι_app_pullback_eq, where Stacks 03GG and 03GV are consumed; what is added here is the transport image_range_integralClosureAlgebraι_app of the integral closure along an isomorphism of algebra sheaves, together with normalizationAlgebraIso and Stacks.AlgebraPullbackQcoh.baseChangeAlgebraHom_naturality.”. References: EGA IV (18.12.15).
Stacks Project, Tag 081K. Let
g : Y ⟶ Sbe a smooth morphism of schemes, let𝒜be a quasi-coherent sheaf of commutative𝒪_S-algebras and let𝒜' = integralClosureAlgebra 𝒜be the integral closure of𝒪_Sin𝒜. Then the integral closure of𝒪_Ying^*𝒜isg^*𝒜': the two subsheavesintegralClosureAlgebra (g^*𝒜)andg^*𝒜'ofg^*𝒜have the same sections over every openWofY. No hypothesis is placed on𝒜beyond quasi-coherence, and none ongbeyond smoothness.
public theorem range_integralClosureAlgebraι_app_algebraPullback_eq (W : Y.Opens) :
Set.range ((integralClosureAlgebraι ((algebraPullback g).obj A)).right.hom.app (op W)) =
Set.range (((algebraPullback g).map (integralClosureAlgebraι A)).right.hom.app (op W))
Stacks.IntegralClosure.SheafLevel.range_integralClosureAlgebraι_app_pullback_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Smooth/IntegralClosureSheaf.lean, line 329. The attribute's comment: “the equality of subsheaves, over an arbitrary open of Y. The quasi-coherent algebra is presented as f_* 𝒪_X for f affine rather than as an abstract quasi-coherent algebra, and the pullback as a direct image from a fibre product rather than through algebraPullback; the latter two agree by isIso_baseChangeAlgebraHom_fromNormalization, and the integral-closure subalgebra 𝒜' is identified with the relative normalization by range_integralClosureAlgebraι_app_eq_range_normalizationAlgebraι_app. The affine-open comparison map, which is where Stacks 03GG is consumed, is Stacks.IntegralClosure.SmoothPullback.bijective_toIntegralClosure_sections. Transport of the integral-closure subalgebra along an isomorphism of algebra sheaves, which removes the presentation of 𝒜 as f_* 𝒪_X, is Stacks.IntegralClosure.SheafLevel.image_range_integralClosureAlgebraι_app, and the resulting presentation-free form of this clause is Stacks.IntegralClosure.SheafLevel.range_integralClosureAlgebraι_app_algebraPullback_eq. See the module docstring.”. References: EGA IV (18.12.15); EGA IV (6.14.5), “smooth base change”.
Let
g : Y ⟶ Sbe a smooth morphism, let𝒜 = f_* 𝒪_Xbe a quasi-coherent sheaf of𝒪_S-algebras withf : X ⟶ Saffine, and let𝒜' ⊆ 𝒜be the integral closure of𝒪_Sin𝒜. Theng^*𝒜'is the integral closure of𝒪_Ying^*𝒜: insideg^*𝒜 = (X ×_S Y)_* 𝒪, the two subsheaves have the same sections over every openWofY. Here𝒜'is presented as(f.fromNormalization)_* 𝒪, byrange_integralClosureAlgebraι_app_eq_range_normalizationAlgebraι_app, and its pullback as the direct image of the structure sheaf off.normalization ×_S Y, which isg^*𝒜'byisIso_baseChangeAlgebraHom_fromNormalization.
public theorem range_integralClosureAlgebraι_app_pullback_eq [IsAffineHom f] (W : Y.Opens) :
Set.range ((integralClosureAlgebraι
(pushforwardAlgebra (pullback.snd f g))).right.hom.app (op W)) =
Set.range ((baseChangeNormalizationAlgebraι f g).right.hom.app (op W))
Stacks.IntegralClosure.SheafLevel.range_integralClosureAlgebraι_app_pullback_relativeSpec_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Smooth/IntegralClosureSheaf.lean, line 383. The attribute's comment: “the equality of subsheaves for an arbitrary quasi-coherent 𝒪_S-algebra 𝒜, over an arbitrary open of Y. 𝒜 enters through its relative spectrum, so that 𝒜 itself is (relativeSpecToBase 𝒜)_* 𝒪 up to the isomorphism Stacks.AffineAlgebraEquivalence.pushforwardAlgebraIso. Invariance of the integral-closure subalgebra under an isomorphism of algebra sheaves, which lets the statement be read off integralClosureAlgebra 𝒜 directly, is Stacks.IntegralClosure.SheafLevel.image_range_integralClosureAlgebraι_app, and the resulting statement — the equality of the subsheaves integralClosureAlgebra (g^*𝒜) and g^*(integralClosureAlgebra 𝒜) of g^*𝒜 — is Stacks.IntegralClosure.SheafLevel.range_integralClosureAlgebraι_app_algebraPullback_eq. See the module docstring and range_integralClosureAlgebraι_app_pullback_eq.”. References: EGA IV (18.12.15).
Let
g : Y ⟶ Sbe smooth and let𝒜be any quasi-coherent sheaf of𝒪_S-algebras, with𝒜' ⊆ 𝒜the integral closure of𝒪_Sin𝒜. WritingX = Spec_S(𝒜)for the relative spectrum, so that𝒜 ≅ (relativeSpecToBase 𝒜)_* 𝒪_XbyStacks.AffineAlgebraEquivalence.pushforwardAlgebraIsoandg^*𝒜 ≅ (X ×_S Y)_* 𝒪byisIso_baseChangeAlgebraHom_selfatX, the integral closure of𝒪_Ying^*𝒜isg^*𝒜': the two subsheaves have the same sections over every openWofY. No hypothesis is placed on𝒜beyond quasi-coherence.
public theorem range_integralClosureAlgebraι_app_pullback_relativeSpec_eq (W : Y.Opens) :
haveI : IsSeparated (relativeSpecToBase A) := IsSeparated.of_isAffineHom _
Set.range ((integralClosureAlgebraι (pushforwardAlgebra
(pullback.snd (relativeSpecToBase A) g))).right.hom.app (op W)) =
Set.range ((baseChangeNormalizationAlgebraι (relativeSpecToBase A) g).right.hom.app
(op W))
Tag 07TD, a lemma
Tag 07TD in the Stacks Project.
AlgebraicGeometry.isPullback_normalizationSchemeMap_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/EtaleBaseChange.lean, line 113. The attribute's comment: “the isomorphism X^ν = X ×_Y Y^ν, for an étale morphism”.
Let
φ : X ⟶ Ybe an étale morphism of schemes and assume every quasi-compact open ofYhas finitely many irreducible components. Then the square formed by the normalization morphisms ofXandY, the morphism of normalizations induced byφandφitself is cartesian, that is,X^ν = X ×_Y Y^ν.
theorem isPullback_normalizationSchemeMap_of_etale :
IsPullback
(normalizationSchemeMap φ (finite_irreducibleComponents_of_smooth φ hY) hY)
(X.normalization (finite_irreducibleComponents_of_smooth φ hY))
(Y.normalization hY) φ
AlgebraicGeometry.isPullback_normalizationSchemeMap_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/SmoothBaseChange.lean, line 251. The attribute's comment: “the isomorphism X^ν = X ×_Y Y^ν”. References: SGA 3 X (8.9), “more general”.
Stacks Project, Tag 07TD, the isomorphism
X^ν = X ×_Y Y^ν. Letφ : X ⟶ Ybe a smooth morphism of schemes and assume every quasi-compact open ofYhas finitely many irreducible components. Then the square formed by the normalization morphisms ofXandY, the morphism of normalizations induced byφandφitself is cartesian.The finiteness hypothesis on
Xis the one ascending alongφfromhY, which is the other assertion of the tag,AlgebraicGeometry.finite_irreducibleComponents_of_smooth.
theorem isPullback_normalizationSchemeMap_of_smooth {X Y : Scheme.{u}} (φ : X ⟶ Y) [Smooth φ]
(hY : ∀ U : Y.Opens, IsCompact (U : Set Y) → (irreducibleComponents U).Finite) :
IsPullback
(normalizationSchemeMap φ (finite_irreducibleComponents_of_smooth φ hY) hY)
(X.normalization (finite_irreducibleComponents_of_smooth φ hY))
(Y.normalization hY) φ
AlgebraicGeometry.finite_irreducibleComponents_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/SingularLocus/IrreducibleComponents.lean, line 60. The attribute's comment: “finiteness of irreducible components”.
Stacks Project, Tag 07TD. Local finiteness of irreducible components ascends along a smooth morphism.
public theorem finite_irreducibleComponents_of_smooth {X Y : Scheme.{u}} (f : X ⟶ Y)
[Smooth f]
(hY : ∀ U : Y.Opens, IsCompact (U : Set Y) → (irreducibleComponents U).Finite) :
∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite
Tag 0CBM, a lemma
Tag 0CBM in the Stacks Project.
AlgebraicGeometry.normalization_baseChange_henselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/Henselization.lean, line 294. The attribute's comment: “henselization”.
The base change of the normalization morphism of a locally Noetherian scheme
Xto the spectrum of the henselization of the local ring ofXat a point is the normalization morphism of that spectrum.
public theorem normalization_baseChange_henselization (X : Scheme.{u}) [IsLocallyNoetherian X]
(x : X) (Ah : Type u) [CommRing Ah] [IsLocalRing Ah] [Algebra (X.presheaf.stalk x) Ah]
[IsHenselization (X.presheaf.stalk x) (ResidueField (X.presheaf.stalk x)) Ah] :
haveI : IsNoetherianRing Ah :=
IsLocalRing.isNoetherianRing_of_isHenselization (A := X.presheaf.stalk x) (B := Ah)
(ResidueField (X.presheaf.stalk x))
Nonempty
(Over.mk (pullback.snd
(Scheme.normalization X (finite_irreducibleComponents_of_isCompact X))
(Spec.map (CommRingCat.ofHom (algebraMap (X.presheaf.stalk x) Ah)) ≫
X.fromSpecStalk x)) ≅
Over.mk (Scheme.normalization (Spec (.of Ah))
(finite_irreducibleComponents_of_isCompact (Spec (.of Ah)))))
AlgebraicGeometry.normalization_baseChange_strictHenselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/Henselization.lean, line 313. The attribute's comment: “strict_henselization”.
The base change of the normalization morphism of a locally Noetherian scheme
Xto the spectrum of a strict henselization of the local ring ofXat a point is the normalization morphism of that spectrum.
public theorem normalization_baseChange_strictHenselization (X : Scheme.{u})
[IsLocallyNoetherian X] (x : X) (Ash : Type u) [CommRing Ash] [IsLocalRing Ash]
[Algebra (X.presheaf.stalk x) Ash] (ksep : Type v) [Field ksep]
[Algebra (ResidueField (X.presheaf.stalk x)) ksep]
[IsSepClosure (ResidueField (X.presheaf.stalk x)) ksep]
[IsHenselization (X.presheaf.stalk x) ksep Ash] :
haveI : IsNoetherianRing Ash :=
IsLocalRing.isNoetherianRing_of_isHenselization (A := X.presheaf.stalk x) (B := Ash) ksep
Nonempty
(Over.mk (pullback.snd
(Scheme.normalization X (finite_irreducibleComponents_of_isCompact X))
(Spec.map (CommRingCat.ofHom (algebraMap (X.presheaf.stalk x) Ash)) ≫
X.fromSpecStalk x)) ≅
Over.mk (Scheme.normalization (Spec (.of Ash))
(finite_irreducibleComponents_of_isCompact (Spec (.of Ash)))))
Sources
Section37.20 Normal morphisms#
Section 37.20 of the Stacks Project, Tag 038Z. 5 tags here are carried by 9 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0390, a definition
Tag 0390 in the Stacks Project.
AlgebraicGeometry.Scheme.Hom.IsNormalAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/NormalMorphism.lean, line 48. The attribute's comment: “part (1)”. References: EGA IV (6.8.1).
A morphism of schemes is normal at
xif it is flat atxand its fibre over the image ofxis geometrically normal at the point induced byx.
public abbrev IsNormalAt {X Y : Scheme.{u}} (f : X ⟶ Y) (x : X) : Prop
AlgebraicGeometry.Scheme.Hom.IsNormal, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/NormalMorphism.lean, line 54. The attribute's comment: “part (2)”. References: EGA IV (6.8.1).
A morphism of schemes is normal if it is normal at every point of its source.
public abbrev IsNormal {X Y : Scheme.{u}} (f : X ⟶ Y) : Prop
Tag 0391, a lemma
Tag 0391 in the Stacks Project.
AlgebraicGeometry.Scheme.Hom.isNormal_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NormalMorphism/Characterization.lean, line 70. The attribute's comment: “stated without the source's standing hypothesis that all fibres are locally Noetherian, which neither implication uses”. References: SGA 6 XII (1.6).
A morphism of schemes is normal exactly when it is flat and each of its fibres is a geometrically normal scheme over the residue field of its base point.
public theorem isNormal_iff {X Y : Scheme.{u}} (f : X ⟶ Y) :
IsNormal f ↔ Flat f ∧ ∀ s : Y, IsGeometricallyNormal (f.fiberToSpecResidueField s)
AlgebraicGeometry.Scheme.Hom.isNormal_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NormalMorphism/Characterization.lean, line 78.
Stacks Project, Tag 0391. For a morphism of schemes all of whose fibres are locally Noetherian, being normal is equivalent to being flat with geometrically normal fibres.
public theorem isNormal_tfae {X Y : Scheme.{u}} (f : X ⟶ Y)
(_hfib : locallyNoetherianFibers f) :
List.TFAE
[IsNormal f, Flat f ∧ ∀ s : Y, IsGeometricallyNormal (f.fiberToSpecResidueField s)]
Tag 056W, a lemma
Tag 056W in the Stacks Project.
AlgebraicGeometry.Scheme.Hom.isNormal_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Smooth/Normal.lean, line 56. References: EGA IV (18.10.5), “more general”.
Stacks Project, Tag 056W. A smooth morphism of schemes is normal: it is flat at every point and all of its fibres are geometrically normal.
public theorem isNormal_of_smooth {X Y : Scheme.{u}} (f : X ⟶ Y) [Smooth f] : f.IsNormal
Tag 0392, a lemma
Tag 0392 in the Stacks Project.
AlgebraicGeometry.locallyNoetherianFibers_isLocalAtSource_fppf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NormalMorphism/LocallyNoetherianFibres.lean, line 112. The attribute's comment: “fppf local on the source”.
Stacks Project, Tag 0392. Having locally Noetherian fibres is local on the source for the fppf topology.
public instance locallyNoetherianFibers_isLocalAtSource_fppf :
(locallyNoetherianFibers : MorphismProperty Scheme.{u}).IsLocalAtSource
Scheme.fppfPrecoverage
AlgebraicGeometry.locallyNoetherianFibers_isLocalAtTarget_fppf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NormalMorphism/LocallyNoetherianFibres.lean, line 124. The attribute's comment: “fppf local on the target”.
Stacks Project, Tag 0392. Having locally Noetherian fibres is local on the target for the fppf topology.
public instance locallyNoetherianFibers_isLocalAtTarget_fppf :
(locallyNoetherianFibers : MorphismProperty Scheme.{u}).IsLocalAtTarget
Scheme.fppfPrecoverage
Tag 0393, a lemma
Tag 0393 in the Stacks Project.
AlgebraicGeometry.normalWithLocallyNoetherianFibers_isLocalAtTarget_fppf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NormalMorphism/FppfLocalTarget.lean, line 198. The attribute's comment: “fppf local on the target”.
Having locally Noetherian fibres and being normal is local on the target for the fppf topology.
public instance normalWithLocallyNoetherianFibers_isLocalAtTarget_fppf :
(normalWithLocallyNoetherianFibers : MorphismProperty Scheme.{u}).IsLocalAtTarget
Scheme.fppfPrecoverage
AlgebraicGeometry.normalWithLocallyNoetherianFibers_isLocalAtSource_smooth, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NormalMorphism/SmoothLocalSource.lean, line 186. The attribute's comment: “smooth local on the source”.
Having locally Noetherian fibres and being normal is local on the source for the smooth topology.
public instance normalWithLocallyNoetherianFibers_isLocalAtSource_smooth :
(normalWithLocallyNoetherianFibers : MorphismProperty Scheme.{u}).IsLocalAtSource
(Scheme.precoverage (@Smooth : MorphismProperty Scheme.{u}))
Sources
Section37.21 Regular morphisms#
Section 37.21 of the Stacks Project, Tag 07R6. 4 tags here are carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 07R7, a definition
Tag 07R7 in the Stacks Project.
AlgebraicGeometry.Scheme.Hom.IsRegularAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/RegularMorphism.lean, line 48. The attribute's comment: “part (1)”. References: EGA IV (6.8.1).
Stacks Project, Tag 07R7, part (1). Regularity of a scheme morphism at a point.
public abbrev IsRegularAt {X Y : Scheme.{u}} (f : X ⟶ Y) (x : X) : Prop
AlgebraicGeometry.Scheme.Hom.IsRegular, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/RegularMorphism.lean, line 54. The attribute's comment: “part (2)”. References: EGA IV (6.8.1).
Stacks Project, Tag 07R7, part (2). Regularity at every source point.
public abbrev IsRegular {X Y : Scheme.{u}} (f : X ⟶ Y) : Prop
Tag 07R8, a lemma
Tag 07R8 in the Stacks Project.
AlgebraicGeometry.Scheme.Hom.regular_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularMorphism/Characterization.lean, line 596.
The five characterizations of a regular morphism with locally Noetherian fibres.
public theorem Scheme.Hom.regular_tfae {X Y : Scheme.{u}} (f : X ⟶ Y)
(h : ∀ y : Y, IsLocallyNoetherian (f.fiber y)) :
List.TFAE [
Scheme.Hom.IsRegular f,
Flat f ∧ ∀ y : Y,
IsGeometricallyRegular (f.fiberToSpecResidueField y),
∀ (U : X.Opens) (_ : IsAffineOpen U) (V : Y.Opens) (_ : IsAffineOpen V)
(hUV : U ≤ f ⁻¹ᵁ V),
IsRegularRingHom (f.appLE V U hUV).hom,
∃ (J : Type u) (V : J → Y.Opens),
IsOpenCover V ∧
∀ j, ∃ (I : Type u) (U : I → X.Opens)
(hU : (⨆ i, U i) = f ⁻¹ᵁ V j),
∀ i, Scheme.Hom.IsRegular
(f.resLE (V j) (U i) ((le_iSup U i).trans hU.le)),
∃ (J : Type u) (V : J → Y.Opens),
IsOpenCover V ∧
(∀ j, IsAffineOpen (V j)) ∧
∀ j, ∃ (I : Type u) (U : I → X.Opens)
(hU : (⨆ i, U i) = f ⁻¹ᵁ V j),
(∀ i, IsAffineOpen (U i)) ∧
∀ i,
let hUV : U i ≤ f ⁻¹ᵁ V j := (le_iSup U i).trans hU.le
IsRegularRingHom (f.appLE (V j) (U i) hUV).hom]
Tag 07R9, a lemma
Tag 07R9 in the Stacks Project.
AlgebraicGeometry.Scheme.Hom.isRegular_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularMorphism/Smooth.lean, line 41. References: EGA IV (17.5.2), “Necessity”; EGA IV (6.8.6), “Implication a) ⇒ b)”.
A smooth morphism of schemes is regular.
public theorem Scheme.Hom.isRegular_of_smooth {X Y : Scheme.{u}} (f : X ⟶ Y) [Smooth f] :
f.IsRegular
Tag 07RA, a lemma
Tag 07RA in the Stacks Project.
AlgebraicGeometry.regularWithLocallyNoetherianFibers_isLocalAtTarget_fppf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularMorphism/FppfLocalTarget.lean, line 168. The attribute's comment: “fppf local on the target”.
Stacks Project, Tag 07RA. Having locally Noetherian fibres and being regular is local on the target for the fppf topology.
public instance regularWithLocallyNoetherianFibers_isLocalAtTarget_fppf :
(regularWithLocallyNoetherianFibers : MorphismProperty Scheme.{u}).IsLocalAtTarget
Scheme.fppfPrecoverage
AlgebraicGeometry.regularWithLocallyNoetherianFibers_isLocalAtSource_smooth, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularMorphism/SmoothLocalSource.lean, line 126. The attribute's comment: “smooth local on the source”.
Stacks Project, Tag 07RA. Having locally Noetherian fibres and being regular is local on the source for the smooth topology.
public instance regularWithLocallyNoetherianFibers_isLocalAtSource_smooth :
(regularWithLocallyNoetherianFibers : MorphismProperty Scheme.{u}).IsLocalAtSource
(Scheme.precoverage (@Smooth : MorphismProperty Scheme.{u}))
Sources
Section37.22 Cohen-Macaulay morphisms#
Section 37.22 of the Stacks Project, Tag 045Q. 11 tags here are carried by 26 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 045R, a definition
Tag 045R in the Stacks Project.
AlgebraicGeometry.flat_of_isCohenMacaulay, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Slicing/MaximalSlice.lean, line 379. The attribute's comment: “flatness of a Cohen-Macaulay morphism”.
A Cohen--Macaulay morphism is flat: flatness of the stalk map at a point is the first conjunct of Cohen--Macaulayness there, and flatness of a morphism is flatness of every stalk map.
theorem flat_of_isCohenMacaulay {X Y : Scheme.{u}}
(f : X ⟶ Y) (hf : ∀ y : Y, IsLocallyNoetherian (f.fiber y))
(hcm : Scheme.Hom.IsCohenMacaulay f hf) : Flat f
AlgebraicGeometry.Scheme.Hom.IsCohenMacaulayAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/Defs.lean, line 73. The attribute's comment: “part (1)”. References: EGA IV (6.8.1), “(ii)”; SGA 1 II (4.19).
A morphism of schemes with locally Noetherian fibres is Cohen–Macaulay at
xif it is flat atxand the local ring of the fibre overf xat the point corresponding toxis Cohen–Macaulay.
public abbrev IsCohenMacaulayAt {X Y : Scheme.{u}} (f : X ⟶ Y)
(hf : ∀ y : Y, IsLocallyNoetherian (f.fiber y)) (x : X) : Prop
AlgebraicGeometry.Scheme.Hom.IsCohenMacaulay, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/Defs.lean, line 82. The attribute's comment: “part (2)”. References: EGA IV (6.8.1), “(ii), global”.
A morphism of schemes with locally Noetherian fibres is Cohen–Macaulay if it is Cohen–Macaulay at every point of its source.
public abbrev IsCohenMacaulay {X Y : Scheme.{u}} (f : X ⟶ Y)
(hf : ∀ y : Y, IsLocallyNoetherian (f.fiber y)) : Prop
Tag 045S, a lemma
Tag 045S in the Stacks Project.
AlgebraicGeometry.isCohenMacaulay_iff_flat_and_fibers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/Fibres.lean, line 59. References: EGA IV (19.2.9), “more general”.
A morphism with locally Noetherian fibres is Cohen–Macaulay precisely when it is flat and every fibre is a Cohen–Macaulay scheme.
public theorem isCohenMacaulay_iff_flat_and_fibers {X Y : Scheme.{u}} (f : X ⟶ Y)
(hf : ∀ y : Y, IsLocallyNoetherian (f.fiber y)) :
Scheme.Hom.IsCohenMacaulay f hf ↔
Flat f ∧ (∀ y : Y, IsCohenMacaulay (f.fiber y))
Tag 0AFG, a lemma
Tag 0AFG in the Stacks Project.
AlgebraicGeometry.topologicalKrullDimAt_eq_add_topologicalKrullDimAt_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/CohenMacaulayDimensionFormula.lean, line 225.
Stacks Project, Tag 0AFG. For a Cohen-Macaulay morphism locally of finite type between locally Noetherian schemes, the dimension of the source at a point is the dimension of the target at its image plus the dimension of the fibre at that point.
public theorem topologicalKrullDimAt_eq_add_topologicalKrullDimAt_fiber {X Y : Scheme.{u}}
[IsLocallyNoetherian X] [IsLocallyNoetherian Y] (f : X ⟶ Y) [LocallyOfFiniteType f]
(hfib : ∀ y : Y, IsLocallyNoetherian (f.fiber y))
(hcm : Scheme.Hom.IsCohenMacaulay f hfib) (x : X) :
topologicalKrullDimAt X x =
topologicalKrullDimAt Y (f x) +
topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x)
Tag 0C0W, a lemma
Tag 0C0W in the Stacks Project.
AlgebraicGeometry.isCohenMacaulayAt_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/Composition.lean, line 338. The attribute's comment: “part (1)”. References: EGA IV (6.8.3), “(i), Cohen-Macaulay”; EGA IV (6.6.1), “a) of (i)”.
The composite of morphisms Cohen–Macaulay at the relevant points is Cohen–Macaulay at the point of the source.
public theorem isCohenMacaulayAt_comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
(hf : ∀ y : Y, IsLocallyNoetherian (f.fiber y))
(hg : ∀ z : Z, IsLocallyNoetherian (g.fiber z))
(hgf : ∀ z : Z, IsLocallyNoetherian ((f ≫ g).fiber z)) (x : X)
(hfx : Scheme.Hom.IsCohenMacaulayAt f hf x)
(hgy : Scheme.Hom.IsCohenMacaulayAt g hg (f x)) :
Scheme.Hom.IsCohenMacaulayAt (f ≫ g) hgf x
AlgebraicGeometry.isCohenMacaulay_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/Composition.lean, line 352. The attribute's comment: “part (2)”.
The composite of Cohen–Macaulay morphisms is Cohen–Macaulay.
public theorem isCohenMacaulay_comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
(hf : ∀ y : Y, IsLocallyNoetherian (f.fiber y))
(hg : ∀ z : Z, IsLocallyNoetherian (g.fiber z))
(hgf : ∀ z : Z, IsLocallyNoetherian ((f ≫ g).fiber z))
(hfm : Scheme.Hom.IsCohenMacaulay f hf)
(hgm : Scheme.Hom.IsCohenMacaulay g hg) :
Scheme.Hom.IsCohenMacaulay (f ≫ g) hgf
AlgebraicGeometry.isCohenMacaulayAt_left_of_comp_of_flatAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/Composition.lean, line 364. The attribute's comment: “part (3), first conclusion”.
If the composite is Cohen–Macaulay at
xandfis flat atx, thenfis Cohen–Macaulay atx.
public theorem isCohenMacaulayAt_left_of_comp_of_flatAt {X Y Z : Scheme.{u}}
(f : X ⟶ Y) (g : Y ⟶ Z)
(hf : ∀ y : Y, IsLocallyNoetherian (f.fiber y))
(hgf : ∀ z : Z, IsLocallyNoetherian ((f ≫ g).fiber z)) (x : X)
(hcomp : Scheme.Hom.IsCohenMacaulayAt (f ≫ g) hgf x)
(hflat : IsFlatAt f.toLRSHom.toShHom x) :
Scheme.Hom.IsCohenMacaulayAt f hf x
AlgebraicGeometry.isCohenMacaulayAt_right_of_comp_of_flatAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/Composition.lean, line 380. The attribute's comment: “part (3), second conclusion”.
If the composite is Cohen–Macaulay at
xandfis flat atx, thengis Cohen–Macaulay atf x.
public theorem isCohenMacaulayAt_right_of_comp_of_flatAt {X Y Z : Scheme.{u}}
(f : X ⟶ Y) (g : Y ⟶ Z)
(hg : ∀ z : Z, IsLocallyNoetherian (g.fiber z))
(hgf : ∀ z : Z, IsLocallyNoetherian ((f ≫ g).fiber z)) (x : X)
(hcomp : Scheme.Hom.IsCohenMacaulayAt (f ≫ g) hgf x)
(hflat : IsFlatAt f.toLRSHom.toShHom x) :
Scheme.Hom.IsCohenMacaulayAt g hg (f x)
AlgebraicGeometry.isCohenMacaulay_left_of_comp_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/Composition.lean, line 395. The attribute's comment: “part (4), first conclusion”.
If the composite is Cohen–Macaulay and
fis flat, thenfis Cohen–Macaulay.
public theorem isCohenMacaulay_left_of_comp_of_flat {X Y Z : Scheme.{u}}
(f : X ⟶ Y) (g : Y ⟶ Z)
(hf : ∀ y : Y, IsLocallyNoetherian (f.fiber y))
(hgf : ∀ z : Z, IsLocallyNoetherian ((f ≫ g).fiber z))
(hcomp : Scheme.Hom.IsCohenMacaulay (f ≫ g) hgf)
(hflat : Flat f) : Scheme.Hom.IsCohenMacaulay f hf
AlgebraicGeometry.isCohenMacaulayAt_right_of_comp_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/Composition.lean, line 408. The attribute's comment: “part (4), second conclusion”. References: EGA IV (6.6.1), “a) of (ii)”; EGA IV (6.8.3), “(ii), Cohen-Macaulay”.
If the composite is Cohen–Macaulay and
fis flat, thengis Cohen–Macaulay at every point in the image off.
public theorem isCohenMacaulayAt_right_of_comp_of_flat {X Y Z : Scheme.{u}}
(f : X ⟶ Y) (g : Y ⟶ Z)
(hg : ∀ z : Z, IsLocallyNoetherian (g.fiber z))
(hgf : ∀ z : Z, IsLocallyNoetherian ((f ≫ g).fiber z))
(hcomp : Scheme.Hom.IsCohenMacaulay (f ≫ g) hgf)
(hflat : Flat f) (x : X) :
Scheme.Hom.IsCohenMacaulayAt g hg (f x)
Tag 0C0X, a lemma
Tag 0C0X in the Stacks Project.
AlgebraicGeometry.isCohenMacaulay_of_isCohenMacaulay_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/FlatSource.lean, line 57. The attribute's comment: “the morphism is Cohen-Macaulay”.
Stacks Project, Tag 0C0X. A flat morphism of locally Noetherian schemes whose source is Cohen–Macaulay is a Cohen–Macaulay morphism.
public theorem isCohenMacaulay_of_isCohenMacaulay_source {X Y : Scheme.{u}}
(f : X ⟶ Y) [IsLocallyNoetherian X] [IsLocallyNoetherian Y] [Flat f]
(hX : IsCohenMacaulay X) :
f.IsCohenMacaulay (isLocallyNoetherian_fiber f)
AlgebraicGeometry.isCohenMacaulayLocalRing_targetStalk_of_isCohenMacaulay_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/FlatSource.lean, line 99. The attribute's comment: “the target local rings are Cohen-Macaulay”. References: EGA IV (7.5.3), “(iii), special case”.
Stacks Project, Tag 0C0X. For a flat morphism of locally Noetherian schemes whose source is Cohen–Macaulay, the local ring of the target at the image of any point of the source is Cohen–Macaulay.
public theorem isCohenMacaulayLocalRing_targetStalk_of_isCohenMacaulay_source {X Y : Scheme.{u}}
(f : X ⟶ Y) [IsLocallyNoetherian X] [IsLocallyNoetherian Y] [Flat f]
(hX : IsCohenMacaulay X) (x : X) :
IsCohenMacaulayLocalRing (Y.presheaf.stalk (f x))
Tag 045T, a lemma
Tag 045T in the Stacks Project.
AlgebraicGeometry.isCohenMacaulayAt_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/BaseChange.lean, line 263. The attribute's comment: “part (1)”. References: EGA IV (6.8.3), “(iii) CM, h loc fin type”.
Stacks Project, Tag 045T (1). Cohen–Macaulayness at a point is preserved under locally finite-type base change.
public theorem isCohenMacaulayAt_pullback {X Y Y' : Scheme.{u}}
(f : X ⟶ Y) (g : Y' ⟶ Y) [LocallyOfFiniteType g]
(hf : ∀ y : Y, IsLocallyNoetherian (f.fiber y)) (x' : (pullback f g : Scheme))
(h : Scheme.Hom.IsCohenMacaulayAt f hf ((pullback.fst f g).base x')) :
Scheme.Hom.IsCohenMacaulayAt (pullback.snd f g)
(fun y' => isLocallyNoetherian_fiber_pullback f g hf y') x'
AlgebraicGeometry.isCohenMacaulayAt_of_pullback_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/BaseChange.lean, line 276. The attribute's comment: “part (2)”.
Stacks Project, Tag 045T (2). Cohen–Macaulayness descends from a base change when the original morphism is flat at the point in question.
public theorem isCohenMacaulayAt_of_pullback_of_flat {X Y Y' : Scheme.{u}}
(f : X ⟶ Y) (g : Y' ⟶ Y) [LocallyOfFiniteType g]
(hf : ∀ y : Y, IsLocallyNoetherian (f.fiber y)) (x' : (pullback f g : Scheme))
(hflat : IsFlatAt f.toLRSHom.toShHom ((pullback.fst f g).base x'))
(h : Scheme.Hom.IsCohenMacaulayAt (pullback.snd f g)
(fun y' => isLocallyNoetherian_fiber_pullback f g hf y') x') :
Scheme.Hom.IsCohenMacaulayAt f hf ((pullback.fst f g).base x')
AlgebraicGeometry.isCohenMacaulayAt_of_pullback_of_flat_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/BaseChange.lean, line 289. The attribute's comment: “part (3)”. References: EGA IV (6.8.3), “(iii) converse, CM”.
Stacks Project, Tag 045T (3). Cohen–Macaulayness descends from a base change flat at the relevant base point.
public theorem isCohenMacaulayAt_of_pullback_of_flat_base {X Y Y' : Scheme.{u}}
(f : X ⟶ Y) (g : Y' ⟶ Y) [LocallyOfFiniteType g]
(hf : ∀ y : Y, IsLocallyNoetherian (f.fiber y)) (x' : (pullback f g : Scheme))
(hflat : IsFlatAt g.toLRSHom.toShHom ((pullback.snd f g).base x'))
(h : Scheme.Hom.IsCohenMacaulayAt (pullback.snd f g)
(fun y' => isLocallyNoetherian_fiber_pullback f g hf y') x') :
Scheme.Hom.IsCohenMacaulayAt f hf ((pullback.fst f g).base x')
Tag 045U, a lemma
Tag 045U in the Stacks Project.
AlgebraicGeometry.isCohenMacaulayAt_set_eq_fiberLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/Locus.lean, line 47. The attribute's comment: “fibre_local_ring_characterization”.
The Cohen–Macaulay locus of a flat, locally finitely presented morphism is exactly the locus where the local ring of its fibre is Cohen–Macaulay.
public theorem isCohenMacaulayAt_set_eq_fiberLocalRing
{X S : Scheme.{u}} (f : X ⟶ S) [Flat f] [LocallyOfFinitePresentation f] :
let hf : ∀ y : S, IsLocallyNoetherian (f.fiber y) := fun y =>
isLocallyNoetherian_fiber_of_locallyOfFinitePresentation f y
{x : X | Scheme.Hom.IsCohenMacaulayAt f hf x} =
{x : X | letI := hf (f x)
IsCohenMacaulayLocalRing ((f.fiber (f x)).presheaf.stalk (f.asFiber x))}
AlgebraicGeometry.dense_cohenMacaulayAt_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/Locus.lean, line 122. The attribute's comment: “cm_locus_fibrewise_dense”. References: SGA 4 XVIII (2.3), “fibrewise density”.
The Cohen–Macaulay locus of a flat, locally finitely presented morphism is dense in every fibre.
public theorem dense_cohenMacaulayAt_fiber
{X S : Scheme.{u}} (f : X ⟶ S) [Flat f] [LocallyOfFinitePresentation f] :
let hf : ∀ s : S, IsLocallyNoetherian (f.fiber s) := fun s =>
isLocallyNoetherian_fiber_of_locallyOfFinitePresentation f s
∀ s : S, Dense ((f.fiberι s) ⁻¹' {x : X | Scheme.Hom.IsCohenMacaulayAt f hf x})
AlgebraicGeometry.isCohenMacaulayAt_pullback_locus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/LocusBaseChange.lean, line 267. The attribute's comment: “cm_locus_base_change”. References: EGA IV (6.8.2), “(ii), special case”.
Stacks Project, Tag 045U (base change). The Cohen–Macaulay locus of a flat, locally finitely presented morphism commutes with arbitrary base change.
public theorem isCohenMacaulayAt_pullback_locus {X S S' : Scheme.{u}}
(f : X ⟶ S) (g : S' ⟶ S) [Flat f] [LocallyOfFinitePresentation f] :
let f' := pullback.snd f g
let g' := pullback.fst f g
let hf : ∀ s : S, IsLocallyNoetherian (f.fiber s) := fun s =>
isLocallyNoetherian_fiber_of_locallyOfFinitePresentation f s
let hf' : ∀ s' : S', IsLocallyNoetherian (f'.fiber s') := fun s' =>
isLocallyNoetherian_fiber_of_locallyOfFinitePresentation f' s'
{x' : (pullback f g : Scheme) | Scheme.Hom.IsCohenMacaulayAt f' hf' x'} =
g'.base ⁻¹' {x : X | Scheme.Hom.IsCohenMacaulayAt f hf x}
AlgebraicGeometry.isOpen_setOf_isCohenMacaulayAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/LocusOpen.lean, line 151. The attribute's comment: “cm_locus_open”. References: EGA IV (12.1.7), “(iii), flat case”; EGA IV (6.11.3), “special case”.
Stacks Project, Tag 045U (Cohen–Macaulay locus). For a flat morphism locally of finite presentation, the locus of points at which the morphism is Cohen–Macaulay is open.
public theorem isOpen_setOf_isCohenMacaulayAt
{X S : Scheme.{u}} (f : X ⟶ S) [Flat f] [LocallyOfFinitePresentation f] :
let hf : ∀ y : S, IsLocallyNoetherian (f.fiber y) := fun y =>
isLocallyNoetherian_fiber_of_locallyOfFinitePresentation f y
IsOpen {x : X | Scheme.Hom.IsCohenMacaulayAt f hf x}
Tag 0BUU, a lemma
Tag 0BUU in the Stacks Project.
AlgebraicGeometry.exists_nat_topologicalKrullDimAt_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/AffineSpaceCriterion.lean, line 863. The attribute's comment: “finiteness of the fibre dimension”.
The local dimension of a fibre of a locally finitely presented morphism is finite.
public theorem exists_nat_topologicalKrullDimAt_fiber {X S : Scheme.{u}} (f : X ⟶ S)
[LocallyOfFinitePresentation f] (x : X) :
∃ n : ℕ,
topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) = (n : WithBot ℕ∞)
AlgebraicGeometry.isCohenMacaulayAt_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/AffineSpaceCriterion.lean, line 882. The attribute's comment: “the four equivalent conditions”. References: EGA IV (15.4.3), “F = O_X, f flat”; SGA 4 XVIII (2.4).
Let
f : X ⟶ Sbe flat and locally of finite presentation and letnbe the dimension of the fibre offthroughxatx. Thenfis Cohen–Macaulay atxif and only if some open neighbourhood ofxcarries a locally quasi-finiteS-morphism to affinen-space overSthat is flat atx, if and only if some open neighbourhood carries a locally quasi-finite flat such morphism, if and only if everyS-morphism to affinen-space from an open neighbourhood ofxthat is quasi-finite atxis flat atx.
public theorem isCohenMacaulayAt_tfae {X S : Scheme.{u}} (f : X ⟶ S)
[Flat f] [LocallyOfFinitePresentation f] (x : X) (n : ℕ)
(hn : topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) = (n : WithBot ℕ∞)) :
List.TFAE [
Scheme.Hom.IsCohenMacaulayAt f
(fun s => isLocallyNoetherian_fiber_of_locallyOfFinitePresentation f s) x,
∃ (U : X.Opens) (hx : x ∈ U.1)
(g : U.toScheme ⟶ AffineSpace (ULift.{u} (Fin n)) S),
(g ≫ (AffineSpace (ULift.{u} (Fin n)) S ↘ S) = U.ι ≫ f) ∧
(LocallyOfFiniteType g ∧ LocallyQuasiFinite g) ∧
AlgebraicGeometry.IsFlatAt g.toLRSHom.toShHom ⟨x, hx⟩,
∃ (U : X.Opens) (_hx : x ∈ U.1)
(g : U.toScheme ⟶ AffineSpace (ULift.{u} (Fin n)) S),
(g ≫ (AffineSpace (ULift.{u} (Fin n)) S ↘ S) = U.ι ≫ f) ∧
(LocallyOfFiniteType g ∧ LocallyQuasiFinite g) ∧ Flat g,
∀ (U : X.Opens) (hx : x ∈ U.1)
(g : U.toScheme ⟶ AffineSpace (ULift.{u} (Fin n)) S),
(g ≫ (AffineSpace (ULift.{u} (Fin n)) S ↘ S) = U.ι ≫ f) →
(AlgebraicGeometry.quasiFiniteAt g ⟨x, hx⟩ →
AlgebraicGeometry.IsFlatAt g.toLRSHom.toShHom ⟨x, hx⟩)]
Tag 054T, a lemma
Tag 054T in the Stacks Project.
AlgebraicGeometry.exists_open_relativeDimension_fiberwise_dense, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/FibrewiseDenseRelativeDimension.lean, line 188.
Stacks Project, Tag 054T. A flat morphism locally of finite presentation admits open pieces of every nonnegative relative dimension whose union is dense in every fibre.
public theorem exists_open_relativeDimension_fiberwise_dense
{X S : Scheme.{u}} (f : X ⟶ S) [Flat f] [LocallyOfFinitePresentation f] :
∃ U : ℕ → X.Opens,
(∀ s : S, Dense ((f.fiberι s) ⁻¹' (((iSup U : X.Opens) : Set X)))) ∧
(∀ d : ℕ, RelativeDimension ((U d).ι ≫ f) d)
Tag 054U, a lemma
Tag 054U in the Stacks Project.
AlgebraicGeometry.topologicalKrullDimAt_fiber_eq_of_specialization_of_mem_genericPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/FibreDimensionSpecialization.lean, line 52. References: EGA IV (12.2.1.1), “partial”.
Stacks Project, Tag 054U. For a flat morphism locally of finite presentation, local dimension in the fibres is constant along a specialization whose endpoint is generic in an irreducible component of its fibre.
public theorem topologicalKrullDimAt_fiber_eq_of_specialization_of_mem_genericPoints
{X S : Scheme.{u}} (f : X ⟶ S) [Flat f] [LocallyOfFinitePresentation f]
{x' x : X} (hxx : x' ⤳ x)
(hx : f.asFiber x ∈ genericPoints (f.fiber (f x))) :
topologicalKrullDimAt (f.fiber (f x')) (f.asFiber x') =
topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x)
Tag 045V, a lemma
Tag 045V in the Stacks Project.
AlgebraicGeometry.cohenMacaulayWithLocallyNoetherianFibers_isLocalAtTarget_fppf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/FppfLocalTarget.lean, line 186. The attribute's comment: “fppf local on the target”.
Stacks Project, Tag 045V. Having locally Noetherian fibres and being Cohen–Macaulay is local on the target for the fppf topology.
public instance cohenMacaulayWithLocallyNoetherianFibers_isLocalAtTarget_fppf :
(cohenMacaulayWithLocallyNoetherianFibers : MorphismProperty Scheme.{u}).IsLocalAtTarget
Scheme.fppfPrecoverage
AlgebraicGeometry.cohenMacaulayWithLocallyNoetherianFibers_isLocalAtSource_syntomic, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/FppfLocalTarget.lean, line 256. The attribute's comment: “syntomic local on the source”.
Stacks Project, Tag 045V. Having locally Noetherian fibres and being Cohen–Macaulay is local on the source for the syntomic topology.
public instance cohenMacaulayWithLocallyNoetherianFibers_isLocalAtSource_syntomic :
(cohenMacaulayWithLocallyNoetherianFibers : MorphismProperty Scheme.{u}).IsLocalAtSource
(Scheme.precoverage (@Syntomic : MorphismProperty Scheme.{u}))
Sources
Section37.23 Slicing Cohen-Macaulay morphisms#
Section 37.23 of the Stacks Project, Tag 056X. 6 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 056Y, a lemma
Tag 056Y in the Stacks Project.
Stacks.AlgebraicGeometry.exists_affineOpen_effectiveCartierDivisor_of_isRegular_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/CohenMacaulaySlice/EffectiveCartierSlice.lean, line 214.
Let
f : X ⟶ Sbe locally of finite presentation and flat atx : X, and lethbe an element of the maximal ideal of𝒪_{X, x}whose image in the local ring of the fibreX_{f x}atxis a nonzerodivisor. Then there is an affine openU ∋ xand a global sectionaofUwhose germ atxish, such that the zero schemeV(a) ⊆ Uis an effective Cartier divisor containingxwhich is flat and locally of finite presentation overS.
theorem exists_affineOpen_effectiveCartierDivisor_of_isRegular_fiber (f : X ⟶ S)
[LocallyOfFinitePresentation f] (x : X) (h : X.presheaf.stalk x)
(hh : h ∈ IsLocalRing.maximalIdeal (X.presheaf.stalk x))
(hflat : IsFlatAt f.toLRSHom.toShHom x)
(hregular : IsRegular (((f.fiberι (f x)).stalkMap (f.asFiber x)).hom
((f.fiberι_asFiber x).symm ▸ h))) :
∃ (U : X.affineOpens) (hx : x ∈ U.1) (a : Γ(U.1.toScheme, ⊤)),
let y : U.1.toScheme := ⟨x, hx⟩
let I : U.1.toScheme.IdealSheafData :=
Scheme.IdealSheafData.ofIdealTop (Ideal.span {a})
(U.1.ι.stalkMap y).hom ((show U.1.ι y = x by rfl).symm ▸ h) =
U.1.toScheme.presheaf.germ ⊤ y (by trivial) a ∧
y ∈ I.support ∧
Stacks.Divisors.IsEffectiveCartierDivisor I ∧
Flat (I.subschemeι ≫ U.1.ι ≫ f) ∧
LocallyOfFinitePresentation (I.subschemeι ≫ U.1.ι ≫ f)
Tag 06LI, a lemma
Tag 06LI in the Stacks Project.
Stacks.AlgebraicGeometry.exists_affineOpen_regularImmersion_flat_of_isRegular_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/CohenMacaulaySlice/RegularSliceThroughPoint.lean, line 74. References: EGA IV (11.3.8), “c) ⇒ b') for F = O_X”.
Stacks Project, Lemma 37.24.1 (Tag 06LI). Let
f : X ⟶ Sbe locally of finite presentation and flat atx : X, and leth : Fin r → 𝒪_{X, x}be a family whose image in the local ring of the fibreX_{f x}atxis a regular sequence. Then there is an affine openUcontainingxand global sectionsa : Fin r → Γ(U, ⊤)whose germs atxare theh i, such thatxlies on the zero schemeV(a), the closed immersion ofV(a)intoUis a regular immersion,V(a)is flat and locally of finite presentation overS, and the base change of the immersion along anyS' ⟶ Sis again a regular immersion.
theorem exists_affineOpen_regularImmersion_flat_of_isRegular_fiber
{X S : Scheme.{u}} (f : X ⟶ S) (x : X) {r : ℕ}
(h : Fin r → X.presheaf.stalk x) [LocallyOfFinitePresentation f]
(hflat : IsFlatAt f.toLRSHom.toShHom x)
(hregular : RingTheory.Sequence.IsRegular
((f.fiber (f x)).presheaf.stalk (f.asFiber x))
(List.ofFn fun i : Fin r =>
((f.fiberι (f x)).stalkMap (f.asFiber x)).hom ((f.fiberι_asFiber x).symm ▸ h i))) :
∃ (U : X.affineOpens) (hx : x ∈ U.1) (a : Fin r → Γ(U.1.toScheme, ⊤)),
let y : U.1.toScheme := ⟨x, hx⟩
let I : U.1.toScheme.IdealSheafData :=
Scheme.IdealSheafData.ofIdealTop (Ideal.ofList (List.ofFn a))
(∀ i : Fin r, (U.1.ι.stalkMap y).hom ((show U.1.ι y = x by rfl).symm ▸ h i) =
U.1.toScheme.presheaf.germ ⊤ y (by trivial) (a i)) ∧
y ∈ I.support ∧
IsRegularImmersion I.subschemeι ∧
Flat (I.subschemeι ≫ U.1.ι ≫ f) ∧
LocallyOfFinitePresentation (I.subschemeι ≫ U.1.ι ≫ f) ∧
∀ (S' : Scheme.{u}) (g : S' ⟶ S),
IsRegularImmersion (pullback.snd I.subschemeι (pullback.fst (U.1.ι ≫ f) g))
Tag 056Z, a lemma
Tag 056Z in the Stacks Project.
Stacks.AlgebraicGeometry.exists_affineOpen_effectiveCartierDivisor_of_one_le_depth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/CohenMacaulaySlice/EffectiveCartierSlice.lean, line 367. References: EGA IV (19.9.6), “n = 1, F = O_X”.
Let
f : X ⟶ Sbe locally of finite presentation and flat atx : X, and assume the local ring of the fibreX_{f x}atxhas depth at least one. Then some affine open neighbourhood ofxcarries an effective Cartier divisor throughxwhich is flat and locally of finite presentation overS.
theorem exists_affineOpen_effectiveCartierDivisor_of_one_le_depth (f : X ⟶ S)
[LocallyOfFinitePresentation f] (x : X) (hflat : IsFlatAt f.toLRSHom.toShHom x)
(hdepth : (1 : ℕ∞) ≤
Module.depth ((f.fiber (f x)).presheaf.stalk (f.asFiber x))
(IsLocalRing.maximalIdeal ((f.fiber (f x)).presheaf.stalk (f.asFiber x)))
((f.fiber (f x)).presheaf.stalk (f.asFiber x))) :
∃ (U : X.affineOpens) (I : U.1.toScheme.IdealSheafData),
x ∈ Set.range (I.subschemeι ≫ U.1.ι) ∧
Stacks.Divisors.IsEffectiveCartierDivisor I ∧
Flat (I.subschemeι ≫ U.1.ι ≫ f) ∧
LocallyOfFinitePresentation (I.subschemeι ≫ U.1.ι ≫ f)
Tag 0570, a lemma
Tag 0570 in the Stacks Project.
Stacks.AlgebraicGeometry.exists_regularImmersion_flat_locallyQuasiFinite_singleton_fiber_of_isCohenMacaulayAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/CohenMacaulaySlice/RegularSliceThroughPoint.lean, line 110. References: EGA IV (19.2.9), “x closed in fibre”; EGA IV (17.16.1).
Stacks Project, Lemma 37.24.6 (Tag 0570). Let
f : X ⟶ Sbe locally of finite presentation, letx : Xbe a point at whichfis Cohen–Macaulay, and assumexis closed in its fibreX_{f x}. Then there is a regular immersioni : Z ⟶ Xthroughxsuch thatZis flat, locally of finite presentation and locally quasi-finite overS, and such that the fibre ofZoverf xis set-theoretically the single point ofZabovex.
theorem exists_regularImmersion_flat_locallyQuasiFinite_singleton_fiber_of_isCohenMacaulayAt
{X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFinitePresentation f] (x : X)
(hCM : ∃ hf : ∀ y : S, IsLocallyNoetherian (f.fiber y),
Scheme.Hom.IsCohenMacaulayAt f hf x)
(hclosed : IsClosed ({f.asFiber x} : Set (f.fiber (f x)))) :
∃ (Z : Scheme.{u}) (i : Z ⟶ X) (z : Z) (hi : IsImmersion i),
letI := hi
i z = x ∧ IsRegularImmersion i ∧
Flat (i ≫ f) ∧ LocallyOfFinitePresentation (i ≫ f) ∧
LocallyQuasiFinite (i ≫ f) ∧
{z' : Z | (i ≫ f) z' = f x} = {z}
AlgebraicGeometry.hasQuasiFiniteSlices, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/QuasiFiniteSlices.lean, line 508. The attribute's comment: “the weak form: only an immersion through the point which is flat, locally of finite presentation and locally quasi-finite over the base, which is what Tag 0571 consumes. The regular-immersion clause and the singleton-fibre clause (c) are not proved.”.
The slicing lemma, in the weak form
AlgebraicGeometry.HasQuasiFiniteSlices: a point which is closed in its fibre and at which a morphism locally of finite presentation is Cohen-Macaulay admits an immersion through it which is flat, locally of finite presentation and locally quasi-finite over the base.The regular-immersion clause and the singleton-fibre clause
Z_s = {x}of Tag 0570 are not proved;AlgebraicGeometry.HasQuasiFiniteSlicedrops both, and the weaker statement is what [Stacks, Tag 0571] uses.
theorem hasQuasiFiniteSlices : HasQuasiFiniteSlices.{u}
Tag 0571, a lemma
Tag 0571 in the Stacks Project.
AlgebraicGeometry.exists_flat_locallyQuasiFinite_factorization_through, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/QuasiFiniteSlices.lean, line 559.
A point in the image of a flat morphism
f : X ⟶ Slocally of finite presentation lies in the image of someg : S' ⟶ Swhich factors ash ≫ fthroughfand is flat, locally of finite presentation and locally quasi-finite.
theorem exists_flat_locallyQuasiFinite_factorization_through
{X S : Scheme.{u}} (f : X ⟶ S) [Flat f] [LocallyOfFinitePresentation f]
(s : S) (hs : s ∈ Set.range f) :
∃ (S' : Scheme.{u}) (g : S' ⟶ S) (h : S' ⟶ X),
h ≫ f = g ∧ Flat g ∧ LocallyOfFinitePresentation g ∧
LocallyOfFiniteType g ∧ LocallyQuasiFinite g ∧ s ∈ Set.range g
Tag 0572, a lemma
Tag 0572 in the Stacks Project.
AlgebraicGeometry.hasLocallyQuasiFiniteRefinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/LocallyQuasiFiniteRefinement.lean, line 126.
Stacks Project, Tag 0572. An fppf covering
𝒰of a schemeSis refined by an fppf covering{T_j ⟶ S}, indexed by the points ofS, each member of which is locally quasi-finite overS.
theorem hasLocallyQuasiFiniteRefinement {S : Scheme.{u}}
(𝒰 : S.Cover.{v} Scheme.fppfPrecoverage) :
HasLocallyQuasiFiniteRefinement 𝒰
Sources
Section37.24 Generic fibres#
Section 37.24 of the Stacks Project, Tag 054V. 8 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 054W, a lemma
Tag 054W in the Stacks Project.
AlgebraicGeometry.exists_open_preimage_eq_bot_of_isEmpty_generic_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ConnectedComponentSection/CoveringFibres.lean, line 154.
Stacks Project, Tag 054W. Let
f : X ⟶ Ybe a finite type morphism withYirreducible with generic pointη. If the fibre overηis empty, then the base change offto some nonempty open subsetVofYis empty, that is,f ⁻¹ᵁ V = ⊥.
theorem exists_open_preimage_eq_bot_of_isEmpty_generic_fiber
{X Y : Scheme.{u}} (f : X ⟶ Y)
[LocallyOfFiniteType f] [QuasiCompact f]
(η : Y) (hη : IsGenericPoint η Set.univ) (hempty : IsEmpty (f.fiber η)) :
∃ V : Y.Opens, Nonempty V ∧ f ⁻¹ᵁ V = ⊥
Tag 05F5, a lemma
Tag 05F5 in the Stacks Project.
AlgebraicGeometry.exists_nonempty_open_surjective_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/Surjective.lean, line 45. References: EGA IV (1.8.6), “first assertion”.
Stacks Project, Tag 05F5. A finite type morphism to an irreducible scheme with nonempty generic fibre is surjective over some nonempty open subscheme of the target.
theorem exists_nonempty_open_surjective_baseChange
{X Y : Scheme.{u}} (f : X ⟶ Y) [IrreducibleSpace Y]
[LocallyOfFiniteType f] [QuasiCompact f]
(η : Y) (hη : IsGenericPoint η Set.univ) (h : Nonempty (f.fiber η)) :
∃ V : Y.Opens, (V : Set Y).Nonempty ∧ Surjective (pullback.snd f V.ι)
Tag 054X, a lemma
Tag 054X in the Stacks Project.
AlgebraicGeometry.exists_open_isNowhereDense_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyIntegral/NowhereDenseGenericFibre.lean, line 444.
Stacks Project, Tag 054X. A closed subset that is nowhere dense in the generic fibre of a finite type morphism remains nowhere dense in all fibres over a nonempty open subset of the irreducible base.
The base is replaced by its reduction, which is a universal homeomorphism onto it (Stacks 054M), so the base change of
fis a homeomorphism ontoX; nowhere density in fibres is invariant under that, and the reduced base is handled byAlgebraicGeometry.exists_open_isNowhereDense_fiber_of_isReduced.
theorem exists_open_isNowhereDense_fiber {X Y : Scheme.{u}} (f : X ⟶ Y) [IrreducibleSpace Y]
[LocallyOfFiniteType f] [QuasiCompact f] (Z : Set X) (hZ : IsClosed Z) (η : Y)
(hη : IsGenericPoint η Set.univ) (hηZ : IsNowhereDense ((f.fiberι η) ⁻¹' Z)) :
∃ V : Set Y, IsOpen V ∧ V.Nonempty ∧
∀ y ∈ V, IsNowhereDense ((f.fiberι y) ⁻¹' Z)
Tag 0573, a lemma
Tag 0573 in the Stacks Project.
AlgebraicGeometry.exists_open_isSchemeTheoreticallyDense_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/GenericFibre/SchemeTheoreticDenseFibre.lean, line 71.
Stacks Project, Tag 0573. Let
f : X ⟶ Ybe a finite type morphism of schemes withYirreducible with generic pointη, and letU ⊆ Xbe an open subscheme whose trace on the fibre overηis scheme-theoretically dense there. Then there is a nonempty openV ⊆ Ysuch that the trace ofUon the fibre overyis scheme-theoretically dense for everyy ∈ V.
public theorem exists_open_isSchemeTheoreticallyDense_fiber {X Y : Scheme.{u}} (f : X ⟶ Y)
[IrreducibleSpace Y] [LocallyOfFiniteType f] [QuasiCompact f] (U : X.Opens) (η : Y)
(hη : IsGenericPoint η Set.univ)
(hηU : Scheme.Opens.IsSchemeTheoreticallyDense (f.fiberι η ⁻¹ᵁ U)) :
∃ V : Y.Opens, (V : Set Y).Nonempty ∧ ∀ y ∈ V,
Scheme.Opens.IsSchemeTheoreticallyDense (f.fiberι y ⁻¹ᵁ U)
Tag 054Y, a lemma
Tag 054Y in the Stacks Project.
AlgebraicGeometry.exists_open_fiber_covered_by_closures, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ConnectedComponentSection/CoveringFibres.lean, line 117.
Stacks Project, Tag 054Y. Let
f : X ⟶ Ybe a finite type morphism withYirreducible with generic pointη. If the subsetsZ icover the generic fibre, then over some nonempty open subset ofYthe closures inXof their images cover every fibre.
theorem exists_open_fiber_covered_by_closures
{X Y : Scheme.{u}} (f : X ⟶ Y)
[LocallyOfFiniteType f] [QuasiCompact f]
(η : Y) (hη : IsGenericPoint η Set.univ)
{ι : Type v}
(Z : ι → Set (f.fiber η))
(hcover : ∀ x : f.fiber η, ∃ i, x ∈ Z i) :
∃ V : Set Y, IsOpen V ∧ V.Nonempty ∧
∀ y ∈ V, ∀ x : f.fiber y,
∃ i, f.fiberι y x ∈ closure (f.fiberι η '' Z i)
Tag 054Z, a lemma
Tag 054Z in the Stacks Project.
AlgebraicGeometry.comap_nilradical_fiberι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/GenericFibreReduction.lean, line 99.
The reduction of the fibre over a generic point of an irreducible component is the base change of the reduction of the source.
theorem comap_nilradical_fiberι {X Y : Scheme.{u}} (f : X ⟶ Y)
(η : Y) (hη : η ∈ genericPoints Y) :
X.nilradical.comap (f.fiberι η) = (f.fiber η).nilradical
Tag 0550, a lemma
Tag 0550 in the Stacks Project.
AlgebraicGeometry.exists_finiteUniversalHomeomorphism_geometricallyReduced_genericFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/GenericFibre/GeometricallyReducedGenericFibre.lean, line 978.
Stacks Project, Tag 0550. A finite type morphism over an irreducible base admits, locally on the base, a finite universal homeomorphic cover whose reduced pullback is flat and finitely presented with geometrically reduced generic fibre.
public theorem exists_finiteUniversalHomeomorphism_geometricallyReduced_genericFiber
{X Y : Scheme.{u}} (f : X ⟶ Y) [IrreducibleSpace Y]
[LocallyOfFiniteType f] [QuasiCompact f] :
∃ (V : Y.Opens) (_ : V.1.Nonempty)
(Y' : Scheme.{u}) (g : Y' ⟶ V.toScheme)
(_ : IsFinite g) (_ : UniversalHomeomorphism g)
(_ : IsIntegral Y') (_ : IsAffine Y'),
let X_V := pullback V.ι f
let P := pullback (g ≫ V.ι) f
let X' := P.nilradical.subscheme
let r : X' ⟶ P := P.nilradical.subschemeι
let f' : X' ⟶ Y' := r ≫ pullback.fst (g ≫ V.ι) f
let g' : X' ⟶ X_V := pullback.lift
(f' ≫ g) (r ≫ pullback.snd (g ≫ V.ι) f) (by
dsimp [f']
rw [Category.assoc, Category.assoc, pullback.condition]
rfl)
IsFinite g' ∧ UniversalHomeomorphism g' ∧ Flat f' ∧
AlgebraicGeometry.FinitePresentation f' ∧
∀ η : Y', IsGenericPoint η Set.univ →
GeometricallyReduced (f'.fiberToSpecResidueField η)
Tag 0551, a lemma
Tag 0551 in the Stacks Project.
AlgebraicGeometry.exists_nonemptyOpen_finiteEtale_cover_geometricallyIrreducible_genericFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/GenericFibre/GeometricallyIrreducible.lean, line 574.
Stacks Project, Tag 0551. After passing to a nonempty open of an irreducible base, a finite type morphism has a finite etale surjective base change from an irreducible affine scheme whose generic fibre has geometrically irreducible irreducible components.
theorem exists_nonemptyOpen_finiteEtale_cover_geometricallyIrreducible_genericFiber
{X Y : Scheme.{u}} (f : X ⟶ Y) [IrreducibleSpace Y]
[LocallyOfFiniteType f] [QuasiCompact f] :
∃ (V : Y.Opens) (_ : V.1.Nonempty)
(Y' : Scheme.{u}) (g : Y' ⟶ V.toScheme)
(_ : Surjective g) (_ : IsFinite g) (_ : Etale g)
(_ : IrreducibleSpace Y') (_ : IsAffine Y'),
let X_V := pullback V.ι f
let fV : X_V ⟶ V.toScheme := pullback.fst V.ι f
let X' := pullback (g ≫ V.ι) f
let f' : X' ⟶ Y' := pullback.fst (g ≫ V.ι) f
let g' : X' ⟶ X_V := pullback.lift
(pullback.fst (g ≫ V.ι) f ≫ g)
(pullback.snd (g ≫ V.ι) f) (by
rw [Category.assoc]
exact pullback.condition)
IsPullback g' f' fV g ∧
Surjective g' ∧ IsFinite g' ∧ Etale g' ∧
∀ (η : Y'), IsGenericPoint η Set.univ →
∀ Z : irreducibleComponents (f'.fiber η),
GeometricallyIrreducible
((Scheme.IdealSheafData.vanishingIdeal (X := f'.fiber η)
⟨Z.1, isClosed_of_mem_irreducibleComponents Z.1 Z.2⟩).subschemeι ≫
f'.fiberToSpecResidueField η)
Sources
Section37.25 Relative assassins#
Section 37.25 of the Stacks Project, Tag 05KM. 5 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 05F1, a lemma
Tag 05F1 in the Stacks Project.
Stacks.RelativeAssassin.exists_open_closure_genericPoints_fibre_mem_relativeAssassin, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RelativeAssassin/GenericFibrePoints.lean, line 315.
Stacks Project, Tag 05F1. Let
f : X ⟶ Sbe locally of finite type, letFbe a quasi-coherent𝒪_X-module of finite type and letξbe a point ofAss_{X/S}(F). There is a nonempty openVof the closure ofξsuch that for everysin the image ofVthe generic points of the fibreV_slie inAss_{X/S}(F).
public theorem exists_open_closure_genericPoints_fibre_mem_relativeAssassin
{X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
(F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
(ξ : X) (hξ : ξ ∈ Stacks.Divisors.relativeAssassin f F) :
∃ V : Set (closure ({ξ} : Set X)), IsOpen V ∧ V.Nonempty ∧
∀ s ∈ f '' (Subtype.val '' V),
∀ η : genericPoints ((f.fiberι s) ⁻¹' (Subtype.val '' V) : Set (f.fiber s)),
f.fiberι s η.1.1 ∈ Stacks.Divisors.relativeAssassin f F
Tag 05KN, a lemma
Tag 05KN in the Stacks Project.
Stacks.RelativeAssassin.exists_open_forall_not_associatedPoints_fibre_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RelativeAssassin/GenericFibrePoints.lean, line 425. References: EGA IV (1.8.6), “second assertion”.
Stacks Project, Tag 05KN. Let
f : X ⟶ Ybe a finite type morphism,Fa quasi-coherent𝒪_X-module of finite type andU ⊆ Xopen, and letYbe irreducible with generic pointη. If the associated points ofFon the fibre overηare not all contained inU, then the same failure of containment holds on the fibre over every point of some nonempty open ofY.
public theorem exists_open_forall_not_associatedPoints_fibre_subset {X Y : Scheme.{u}}
(f : X ⟶ Y) [LocallyOfFiniteType f] [QuasiCompact f]
(F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType] (U : X.Opens)
[IrreducibleSpace Y] (η : Y) (hη : IsGenericPoint η Set.univ)
(hηU : ¬ Stacks.Divisors.associatedPoints
((Scheme.Modules.pullback (f.fiberι η)).obj F) ⊆ f.fiberι η ⁻¹' (U : Set X)) :
∃ V : Y.Opens, (V : Set Y).Nonempty ∧ ∀ y ∈ V,
¬ Stacks.Divisors.associatedPoints
((Scheme.Modules.pullback (f.fiberι y)).obj F) ⊆ f.fiberι y ⁻¹' (U : Set X)
Tag 05KP, a lemma
Tag 05KP in the Stacks Project.
Stacks.Divisors.exists_open_associatedPoints_fiber_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RelativeAssassin/FibrewiseContainment.lean, line 480.
Stacks Project, Tag 05KP. Let
f : X ⟶ Ybe a finite type morphism of schemes,Fa finite type quasi-coherent module onXandU ⊆ Xopen. IfYis irreducible with generic pointηand all associated points ofFrestricted to the fibre overηlie inU, then there is a nonempty openV ⊆ Ysuch that the same containment holds in the fibre over every point ofV.The target is replaced by its reduction, which is integral because the closed immersion of the reduction is a homeomorphism, and the containment is transported across that base change by Stacks 05KQ.
theorem exists_open_associatedPoints_fiber_subset {X Y : Scheme.{u}} (f : X ⟶ Y)
(F : X.Modules) [LocallyOfFiniteType f] [QuasiCompact f] [F.IsQuasicoherent]
[F.IsFiniteType] [IrreducibleSpace Y] (U : X.Opens) (η : Y)
(hη : IsGenericPoint η Set.univ)
(hηU : associatedPoints ((Scheme.Modules.pullback (f.fiberι η)).obj F) ⊆
(f.fiberι η) ⁻¹' (U : Set X)) :
∃ V : Y.Opens, (V : Set Y).Nonempty ∧ ∀ y ∈ V,
associatedPoints ((Scheme.Modules.pullback (f.fiberι y)).obj F) ⊆
(f.fiberι y) ⁻¹' (U : Set X)
Tag 05KQ, a lemma
Tag 05KQ in the Stacks Project.
Stacks.RelativeAssassin.associatedPoints_fiber_subset_preimage_iff_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RelativeAssassin/FiberBaseChange.lean, line 70.
Stacks Project, Tag 05KQ. After arbitrary base change, the associated points of the pullback module on a fibre lie in the pulled-back open exactly when they did so on the original fibre.
theorem associatedPoints_fiber_subset_preimage_iff_baseChange
{X S S' : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
(F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
(U : X.Opens) (g : S' ⟶ S) (s' : S') :
Stacks.Divisors.associatedPoints
((Scheme.Modules.pullback (f.fiberι (g s'))).obj F) ⊆
(f.fiberι (g s')) ⁻¹' (U : Set X) ↔
Stacks.Divisors.associatedPoints
((Scheme.Modules.pullback ((pullback.snd f g).fiberι s')).obj
((Scheme.Modules.pullback (pullback.fst f g)).obj F)) ⊆
((pullback.snd f g).fiberι s') ⁻¹'
((pullback.fst f g) ⁻¹' (U : Set X))
Tag 05KR, a lemma
Tag 05KR in the Stacks Project.
Stacks.RelativeAssassin.isLocallyConstructible_fibrewiseContainment, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RelativeAssassin/ContainmentConstructible.lean, line 491.
Stacks Project, Tag 05KR. Let
f : X ⟶ Ybe a morphism of finite presentation, letFbe a quasi-coherent𝒪_X-module of finite presentation and letU ⊆ Xbe an open subscheme withU ⟶ Yquasi-compact. Then the set of pointsyofYover which every associated point of the fibreF_ylies in the fibreU_yis locally constructible inY.
theorem isLocallyConstructible_fibrewiseContainment (f : X ⟶ Y)
(hf : AlgebraicGeometry.FinitePresentation f) (F : X.Modules) [F.IsQuasicoherent]
[F.IsFinitePresentation] (U : X.Opens) [QuasiCompact (U.ι ≫ f)] :
IsLocallyConstructible (fibrewiseContainment f F U)
Sources
Section37.26 Reduced fibres#
Section 37.26 of the Stacks Project, Tag 0574. 7 tags here are carried by 9 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0575, a lemma
Tag 0575 in the Stacks Project.
AlgebraicGeometry.exists_open_forall_not_isReduced_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/Reduced.lean, line 614. References: EGA IV (9.7.2), “more general”.
Stacks Project, Tag 0575. If the generic fibre of a finite type morphism to an irreducible scheme is nonreduced, then every fibre over a suitable nonempty open subset of the target is nonreduced.
theorem exists_open_forall_not_isReduced_fiber
{X Y : AlgebraicGeometry.Scheme.{u}} (f : X ⟶ Y)
[IrreducibleSpace Y] [AlgebraicGeometry.LocallyOfFiniteType f]
[AlgebraicGeometry.QuasiCompact f] (η : Y) (hη : IsGenericPoint η Set.univ)
(h : ¬ AlgebraicGeometry.IsReduced (f.fiber η)) :
∃ V : Set Y, IsOpen V ∧ V.Nonempty ∧
∀ y ∈ V, ¬ AlgebraicGeometry.IsReduced (f.fiber y)
Tag 0576, a lemma
Tag 0576 in the Stacks Project.
AlgebraicGeometry.geometricallyReduced_fiber_set_eq_preimage_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/Reduced.lean, line 641.
The locus of geometrically reduced fibres commutes with arbitrary base change.
theorem geometricallyReduced_fiber_set_eq_preimage_of_isPullback
{X Y X' Y' : Scheme.{u}} (f : X ⟶ Y) (f' : X' ⟶ Y') (i : X' ⟶ X) (g : Y' ⟶ Y)
(h : IsPullback i f' f g) :
{y' : Y' | GeometricallyReduced (f'.fiberToSpecResidueField y')} =
g ⁻¹' {y : Y | GeometricallyReduced (f.fiberToSpecResidueField y)}
Tag 0577, a lemma
Tag 0577 in the Stacks Project.
AlgebraicGeometry.exists_open_forall_not_geometricallyReduced_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/NonReducedGenericFibre.lean, line 43.
If the generic fibre of a finite type morphism to an irreducible scheme is not geometrically reduced, then every fibre over a suitable nonempty open subset of the target is not geometrically reduced.
theorem exists_open_forall_not_geometricallyReduced_fiber
{X Y : Scheme.{u}} (f : X ⟶ Y)
[IrreducibleSpace Y] [LocallyOfFiniteType f]
[QuasiCompact f] (η : Y) (hη : IsGenericPoint η Set.univ)
(h : ¬ GeometricallyReduced (f.fiberToSpecResidueField η)) :
∃ V : Set Y, IsOpen V ∧ V.Nonempty ∧
∀ y ∈ V, ¬ GeometricallyReduced (f.fiberToSpecResidueField y)
Tag 0578, a lemma
Tag 0578 in the Stacks Project.
AlgebraicGeometry.exists_opens_nonempty_geometricallyReduced_morphismRestrict_of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ReducedFibre/OpenLocus.lean, line 707.
Stacks Project, Tag 0578. Let
f : X ⟶ Ybe a morphism of finite type onto an irreducible scheme with generic pointη. If the fibre offoverηis geometrically reduced, then there is a nonempty open subschemeV ⊆ Ysuch thatX_V ⟶ Vhas geometrically reduced fibres.Finite presentation is reached by the source's own bridge, Stacks 052A. The base is replaced by its reduction
r : Y_red ⟶ Y, which is a universal homeomorphism, so it carries opens and generic points across and, by Stacks 0576, carries the geometrically reduced fibre locus of the base change back to that off. Over the reduced base generic flatnessAlgebraicGeometry.exists_dense_open_flat_finitePresentation_structureSheafsupplies a dense openU ⊆ Y_redover which the base change is of finite presentation; the generic point lies inUbecauseUis dense, so the finite presentation case applies overUand produces an open subset ofUinside the locus and containing the generic point. Its image inYunder the open immersion ofUfollowed by the homeomorphismris open, nonempty and inside the locus off.
theorem exists_opens_nonempty_geometricallyReduced_morphismRestrict_of_finiteType
{X Y : Scheme.{u}} (f : X ⟶ Y) [IrreducibleSpace Y]
[LocallyOfFiniteType f] [QuasiCompact f] (η : Y)
(hη : IsGenericPoint η (Set.univ : Set Y))
[GeometricallyReduced (f.fiberToSpecResidueField η)] :
∃ V : Y.Opens, Nonempty V ∧ GeometricallyReduced (f ∣_ V)
Tag 0579, a lemma
Tag 0579 in the Stacks Project.
AlgebraicGeometry.isLocallyConstructible_geometricallyReduced_fiber_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Fibres/ReducedFibreLocus.lean, line 164. The attribute's comment: “affine Noetherian case: X and S affine with S locally Noetherian. The source states the lemma for an arbitrary quasi-compact morphism locally of finite presentation.”. References: EGA IV (9.9.3), “affine Noeth., reduced”; EGA IV (9.9.5), “reduced fibres, affine”; EGA IV (9.7.7), “(iii), affine Noeth.”.
The affine Noetherian case of Stacks 0579. For a morphism
g : X ⟶ Sof finite presentation between affine schemes withSlocally Noetherian, the set of points ofSwhose fibre is geometrically reduced is locally constructible.Comparing
gwithSpec Γ(X, ⊤) ⟶ Spec Γ(S, ⊤)gives a cartesian square with isomorphisms along the top and bottom, so Stacks 0576 identifies the locus with the inverse image of the locus of the latter; that locus isAlgebra.geometricallyReducedFibreLocus Γ(S, ⊤) Γ(X, ⊤)byAlgebraicGeometry.geometricallyReduced_fiberToSpecResidueField_specMap_iff, which is constructible byAlgebra.isConstructible_geometricallyReducedFibreLocus'; and Stacks 054I takes local constructibility back along the isomorphism.
theorem isLocallyConstructible_geometricallyReduced_fiber_of_isAffine {X S : Scheme.{u}}
(g : X ⟶ S) [IsAffine X] [IsAffine S] [IsLocallyNoetherian S] (hg : FinitePresentation g) :
IsLocallyConstructible {y : S | GeometricallyReduced (g.fiberToSpecResidueField y)}
AlgebraicGeometry.isLocallyConstructible_geometricallyReduced_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ReducedFibre/OpenLocus.lean, line 610. References: EGA IV (9.7.7), “more general”.
Stacks Project, Tag 0579. Let
f : X ⟶ Ybe a quasi-compact morphism of schemes which is locally of finite presentation. Then the set of points ofYwhose fibre is geometrically reduced is locally constructible inY.Local constructibility is tested on the affine opens of
Y(AlgebraicGeometry.isLocallyConstructible_iff_forall_affineOpens). Over an affine openUthe restrictionf ∣_ Uis again quasi-compact and locally of finite presentation, and its geometrically reduced fibre locus is the inverse image of that offby Stacks 0576, soAlgebraicGeometry.isConstructible_geometricallyReduced_fiber_of_isAffine_targetapplies.
theorem isLocallyConstructible_geometricallyReduced_fiber {X Y : Scheme.{u}} (f : X ⟶ Y)
[QuasiCompact f] [LocallyOfFinitePresentation f] :
IsLocallyConstructible {y : Y | GeometricallyReduced (f.fiberToSpecResidueField y)}
Tag 0C0D, a lemma
Tag 0C0D in the Stacks Project.
AlgebraicGeometry.isReduced_of_isProper_over_dvr_of_isReduced_specialFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ReducedFibre/ProperOverDvr.lean, line 572. The attribute's comment: “total space”.
Stacks Project, Tag 0C0D (total space). A proper scheme over a discrete valuation ring is reduced if every irreducible component dominates the base and the special fibre is reduced.
theorem isReduced_of_isProper_over_dvr_of_isReduced_specialFiber
{R : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
{X : Scheme.{u}} (f : X ⟶ Spec (.of R)) [IsProper f]
(hcomponents : ∀ Z ∈ irreducibleComponents X, Dense (f '' Z))
[IsReduced (f.fiber (IsLocalRing.closedPoint (CommRingCat.of R)))] :
IsReduced X
AlgebraicGeometry.isReduced_genericFiber_of_isProper_over_dvr_of_isReduced_specialFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ReducedFibre/ProperOverDvr.lean, line 592. The attribute's comment: “generic fibre”.
Stacks Project, Tag 0C0D (generic fibre). A proper scheme over a discrete valuation ring has reduced generic fibre if every irreducible component dominates the base and the special fibre is reduced.
theorem isReduced_genericFiber_of_isProper_over_dvr_of_isReduced_specialFiber
{R : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
{X : Scheme.{u}} (f : X ⟶ Spec (.of R)) [IsProper f]
(hcomponents : ∀ Z ∈ irreducibleComponents X, Dense (f '' Z))
[IsReduced (f.fiber (IsLocalRing.closedPoint (CommRingCat.of R)))] :
IsReduced (f.fiber (⟨⊥, inferInstance⟩ : PrimeSpectrum R))
Tag 0C0E, a lemma
Tag 0C0E in the Stacks Project.
AlgebraicGeometry.isOpen_geometricallyReduced_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ReducedFibre/OpenLocus.lean, line 527.
Stacks Project, Tag 0C0E. The geometrically reduced fibres of a flat, proper, finitely presented morphism form an open locus in the base.
theorem isOpen_geometricallyReduced_fiber
{X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsProper f]
(hfp : FinitePresentation f) :
IsOpen {y : Y | GeometricallyReduced (f.fiberToSpecResidueField y)}
Sources
Section37.27 Irreducible components of fibres#
Section 37.27 of the Stacks Project, Tag 0553. 7 tags here are carried by 10 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0554, a lemma
Tag 0554 in the Stacks Project.
AlgebraicGeometry.exists_open_ncard_irreducibleComponents_fiber_ge, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NowhereDenseFibres/ComponentCount.lean, line 257. References: EGA IV (9.7.1), “irreducible components”.
Stacks Project, Tag 0554. For a finite type morphism to a scheme with a chosen dense generic point, the number of irreducible components of the fibres is at least the number for the generic fibre over a nonempty open subset of the base.
theorem exists_open_ncard_irreducibleComponents_fiber_ge {X Y : Scheme.{u}} (f : X ⟶ Y)
[LocallyOfFiniteType f] [QuasiCompact f] (η : Y) (hη : IsGenericPoint η Set.univ)
(n : ℕ) (hcomp : (irreducibleComponents (f.fiber η)).ncard = n) :
∃ V : Set Y, IsOpen V ∧ V.Nonempty ∧
∀ y ∈ V, n ≤ (irreducibleComponents (f.fiber y)).ncard
Tag 0555, a lemma
Tag 0555 in the Stacks Project.
AlgebraicGeometry.geometricallyIrreducibleFiberLocus_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/IrreducibleComponents.lean, line 193. The attribute's comment: “the locus pulls back under the chosen fibre product”.
Stacks Project, Tag 0555. The points with geometrically irreducible fibre pull back exactly under an arbitrary base change.
theorem geometricallyIrreducibleFiberLocus_baseChange
{X Y Y' : Scheme.{u}} (f : X ⟶ Y) (g : Y' ⟶ Y) :
{y' : Y' | GeometricallyIrreducible
((pullback.snd f g).fiberToSpecResidueField y')} =
g ⁻¹' {y : Y | GeometricallyIrreducible (f.fiberToSpecResidueField y)}
AlgebraicGeometry.geometricallyIrreducibleFiberLocus_eq_preimage_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/IrreducibleComponents.lean, line 205. The attribute's comment: “the locus pulls back under an arbitrary cartesian square”.
Stacks Project, Tag 0555. The points with geometrically irreducible fibre pull back exactly under an arbitrary cartesian square, not only under the chosen fibre product.
theorem geometricallyIrreducibleFiberLocus_eq_preimage_of_isPullback
{X Y X' Y' : Scheme.{u}} (f : X ⟶ Y) (f' : X' ⟶ Y') (i : X' ⟶ X) (g : Y' ⟶ Y)
(h : IsPullback i f' f g) :
{y' : Y' | GeometricallyIrreducible (f'.fiberToSpecResidueField y')} =
g ⁻¹' {y : Y | GeometricallyIrreducible (f.fiberToSpecResidueField y)}
Tag 0556, a lemma
Tag 0556 in the Stacks Project.
AlgebraicGeometry.geometricIrreducibleComponentCount, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/IrreducibleComponents.lean, line 114. The attribute's comment: “the function”. References: EGA IV (4.5.2), “more general”; EGA IV (4.7.4), “more general”.
The number, as an extended natural number, of geometrically irreducible components of each fibre of a morphism of schemes.
def geometricIrreducibleComponentCount {X Y : Scheme.{u}} (f : X ⟶ Y) : Y → ℕ∞
AlgebraicGeometry.encard_irreducibleComponents_geometricFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/IrreducibleComponents.lean, line 121. The attribute's comment: “well-definedness”. References: EGA IV (4.5.1), “partial”.
The number of irreducible components of the geometric fibre can be computed after extension to any separably closed field containing the residue field.
theorem encard_irreducibleComponents_geometricFiber {X Y : Scheme.{u}} (f : X ⟶ Y)
(y : Y) (K : Type u) [Field K] [Algebra (Y.residueField y) K] [IsSepClosed K] :
(irreducibleComponents (geometricFiber f y K)).encard =
geometricIrreducibleComponentCount f y
AlgebraicGeometry.geometricIrreducibleComponentCount_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/IrreducibleComponents.lean, line 158. The attribute's comment: “base change”.
Formation of the function counting geometrically irreducible components of fibres commutes with arbitrary base change.
theorem geometricIrreducibleComponentCount_pullback {X Y Y' : Scheme.{u}}
(f : X ⟶ Y) (g : Y' ⟶ Y) :
geometricIrreducibleComponentCount (pullback.snd f g) =
geometricIrreducibleComponentCount f ∘ g
Tag 0557, a lemma
Tag 0557 in the Stacks Project.
MvPolynomial.exists_away_irreducible_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/PolynomialIrreducibility.lean, line 313. References: EGA IV (9.7.5); EGA IV (9.7.4), “c ⇒ b”.
Stacks Project, Tag 0557. An absolutely irreducible polynomial over a domain remains irreducible under every specialization to a field after restricting to a nonempty principal open subset.
theorem exists_away_irreducible_map
(A : Type u) [CommRing A] [IsDomain A]
(K : Type v) [Field K] [Algebra A K] [IsFractionRing A K]
(Kbar : Type w) [Field Kbar] [Algebra K Kbar] [IsAlgClosed Kbar]
(ι : Type x) [Finite ι] (P : MvPolynomial ι A)
(hP : Irreducible (P.map ((algebraMap K Kbar).comp (algebraMap A K)))) :
∃ f : A, f ≠ 0 ∧
∀ (κ : Type y) [Field κ] (φ : Localization.Away f →+* κ),
Irreducible (P.map (φ.comp (algebraMap A (Localization.Away f))))
Tag 0559, a lemma
Tag 0559 in the Stacks Project.
AlgebraicGeometry.geometricallyIrreducibleAfterShrinking, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/GenericFibre/GenericResidueField.lean, line 336.
Stacks Project, Tag 0559. A morphism of finite type onto an irreducible base whose fibre over the generic point is geometrically irreducible has geometrically irreducible fibres over a nonempty open subscheme of the base.
theorem geometricallyIrreducibleAfterShrinking :
GeometricallyIrreducibleAfterShrinking.{u}
Tag 055A, a lemma
Tag 055A in the Stacks Project.
AlgebraicGeometry.exists_open_geometricIrreducibleComponentCount_constant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/GenericFibre/ShrinkingConsequences.lean, line 60.
Stacks Project, Tag 055A. The number of geometrically irreducible components of the fibres of a finite type morphism is constant on a nonempty open subset of the closure of any point of the target.
theorem exists_open_geometricIrreducibleComponentCount_constant {X Y : Scheme.{u}} (f : X ⟶ Y)
[LocallyOfFiniteType f] [QuasiCompact f] (y : Y) :
∃ V : Opens (↑(closure ({y} : Set Y))), Nonempty V ∧
∃ n : ℕ∞, ∀ z : V, geometricIrreducibleComponentCount f z.1.1 = n
Tag 055B, a lemma
Tag 055B in the Stacks Project.
AlgebraicGeometry.isLocallyConstructible_level_geometricIrreducibleComponentCount, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/GenericFibre/ShrinkingConsequences.lean, line 70. References: EGA IV (9.7.9), “n(s) (irreducible)”; SGA 4 XIV (1.11), “special case”.
Stacks Project, Tag 055B. Every level set of the number of geometrically irreducible components of the fibres of a morphism of finite presentation is locally constructible.
theorem isLocallyConstructible_level_geometricIrreducibleComponentCount {X Y : Scheme.{u}}
(f : X ⟶ Y) (hf : FinitePresentation f) (n : ℕ∞) :
IsLocallyConstructible {y : Y | geometricIrreducibleComponentCount f y = n}
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.